{-# LANGUAGE ExistentialQuantification #-}
module Inferno.Infer.Exhaustiveness
( mkEnumText,
Pattern (W),
exhaustive,
checkUsefullness,
cInf,
cEnum,
cOne,
cEmpty,
cTuple,
)
where
import Data.List (intercalate)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as Text
import Inferno.Types.VersionControl (VCObjectHash)
import Prettyprinter (Pretty (pretty), align, tupled, (<+>))
data Con = COne | CEmpty | CTuple Int | forall a. (Show a, Pretty a, Enum a) => CInf a | CEnum VCObjectHash Text
instance Eq Con where
Con
COne == :: Con -> Con -> Bool
== Con
COne = Bool
True
Con
CEmpty == Con
CEmpty = Bool
True
(CTuple Int
i) == (CTuple Int
j) = Int
i forall a. Eq a => a -> a -> Bool
== Int
j
(CEnum VCObjectHash
e Text
_) == (CEnum VCObjectHash
f Text
_) = VCObjectHash
e forall a. Eq a => a -> a -> Bool
== VCObjectHash
f
(CInf a
a) == (CInf a
b) = (forall a. Show a => a -> String
show a
a) forall a. Eq a => a -> a -> Bool
== (forall a. Show a => a -> String
show a
b)
Con
_ == Con
_ = Bool
False
instance Ord Con where
compare :: Con -> Con -> Ordering
compare Con
a Con
b = forall a. Ord a => a -> a -> Ordering
compare (Con -> String
mkOrd Con
a) (Con -> String
mkOrd Con
b)
where
mkOrd :: Con -> String
mkOrd = \case
Con
COne -> String
"one"
Con
CEmpty -> String
"empty"
CTuple Int
n -> forall a. Show a => a -> String
show Int
n
CInf a
v -> forall a. Show a => a -> String
show a
v
CEnum VCObjectHash
_ Text
e -> forall a. Show a => a -> String
show Text
e
data Pattern = C Con [Pattern] | W deriving (Pattern -> Pattern -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pattern -> Pattern -> Bool
$c/= :: Pattern -> Pattern -> Bool
== :: Pattern -> Pattern -> Bool
$c== :: Pattern -> Pattern -> Bool
Eq, Eq Pattern
Pattern -> Pattern -> Bool
Pattern -> Pattern -> Ordering
Pattern -> Pattern -> Pattern
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Pattern -> Pattern -> Pattern
$cmin :: Pattern -> Pattern -> Pattern
max :: Pattern -> Pattern -> Pattern
$cmax :: Pattern -> Pattern -> Pattern
>= :: Pattern -> Pattern -> Bool
$c>= :: Pattern -> Pattern -> Bool
> :: Pattern -> Pattern -> Bool
$c> :: Pattern -> Pattern -> Bool
<= :: Pattern -> Pattern -> Bool
$c<= :: Pattern -> Pattern -> Bool
< :: Pattern -> Pattern -> Bool
$c< :: Pattern -> Pattern -> Bool
compare :: Pattern -> Pattern -> Ordering
$ccompare :: Pattern -> Pattern -> Ordering
Ord)
instance Show Pattern where
show :: Pattern -> String
show = \case
Pattern
W -> String
"_"
C Con
COne [Pattern
x] -> String
"one " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Pattern
x
C Con
CEmpty [Pattern]
_ -> String
"empty"
C (CTuple Int
_) [Pattern]
xs -> String
"(" forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pattern]
xs) forall a. Semigroup a => a -> a -> a
<> String
")"
C (CInf a
x) [Pattern]
_ -> forall a. Show a => a -> String
show a
x
C (CEnum VCObjectHash
_ Text
x) [Pattern]
_ -> String
"#" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Text
x
C Con
_ [Pattern]
_ -> String
"undefined"
instance Pretty Pattern where
pretty :: forall ann. Pattern -> Doc ann
pretty = \case
Pattern
W -> Doc ann
"_"
C Con
COne [Pattern
x] -> Doc ann
"one" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty Pattern
x)
C Con
CEmpty [Pattern]
_ -> Doc ann
"empty"
C (CTuple Int
_) [Pattern]
xs -> forall ann. [Doc ann] -> Doc ann
tupled (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Pattern]
xs)
C (CInf a
x) [Pattern]
_ -> forall a ann. Pretty a => a -> Doc ann
pretty a
x
C (CEnum VCObjectHash
_ Text
x) [Pattern]
_ -> Doc ann
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Text
x
C Con
_ [Pattern]
_ -> Doc ann
"undefined"
type PMatrix = [[Pattern]]
cSize :: Con -> Int
cSize :: Con -> Int
cSize = \case
Con
COne -> Int
1
Con
CEmpty -> Int
0
CTuple Int
s -> Int
s
CInf a
_ -> Int
0
CEnum VCObjectHash
_ Text
_ -> Int
0
specialize :: Con -> PMatrix -> PMatrix
specialize :: Con -> PMatrix -> PMatrix
specialize Con
_ [] = []
specialize Con
c ((Pattern
pi1 : [Pattern]
pis) : PMatrix
rest) = case Pattern
pi1 of
C Con
c' [Pattern]
rs ->
if Con
c forall a. Eq a => a -> a -> Bool
== Con
c'
then ([Pattern]
rs forall a. [a] -> [a] -> [a]
++ [Pattern]
pis) forall a. a -> [a] -> [a]
: Con -> PMatrix -> PMatrix
specialize Con
c PMatrix
rest
else Con -> PMatrix -> PMatrix
specialize Con
c PMatrix
rest
Pattern
W -> (forall a. Int -> a -> [a]
replicate (Con -> Int
cSize Con
c) Pattern
W forall a. [a] -> [a] -> [a]
++ [Pattern]
pis) forall a. a -> [a] -> [a]
: Con -> PMatrix -> PMatrix
specialize Con
c PMatrix
rest
specialize Con
_ ([] : PMatrix
_) = forall a. HasCallStack => String -> a
error String
"malformed PMatrix"
specializeVec :: Con -> [Pattern] -> Maybe [Pattern]
specializeVec :: Con -> [Pattern] -> Maybe [Pattern]
specializeVec Con
c [Pattern]
p = case Con -> PMatrix -> PMatrix
specialize Con
c [[Pattern]
p] of
[[Pattern]
p'] -> forall a. a -> Maybe a
Just [Pattern]
p'
PMatrix
_ -> forall a. Maybe a
Nothing
col :: PMatrix -> [Pattern]
col :: PMatrix -> [Pattern]
col [] = []
col ([] : PMatrix
_) = []
col ((Pattern
x : [Pattern]
_) : PMatrix
rest) = Pattern
x forall a. a -> [a] -> [a]
: PMatrix -> [Pattern]
col PMatrix
rest
conNames :: [Pattern] -> Set Con
conNames :: [Pattern] -> Set Con
conNames [] = forall a. Set a
Set.empty
conNames (Pattern
p : [Pattern]
ps) = case Pattern
p of
C Con
c [Pattern]
_ -> forall a. Ord a => a -> Set a -> Set a
Set.insert Con
c forall a b. (a -> b) -> a -> b
$ [Pattern] -> Set Con
conNames [Pattern]
ps
Pattern
W -> [Pattern] -> Set Con
conNames [Pattern]
ps
data IsComplete = Complete | Incomplete Pattern
isComplete :: IsComplete -> Bool
isComplete :: IsComplete -> Bool
isComplete IsComplete
Complete = Bool
True
isComplete IsComplete
_ = Bool
False
isCompleteSignature :: Map VCObjectHash (Set (VCObjectHash, Text)) -> Set Con -> IsComplete
isCompleteSignature :: Map VCObjectHash (Set (VCObjectHash, Text))
-> Set Con -> IsComplete
isCompleteSignature Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs Set Con
s =
if forall a. Set a -> Bool
Set.null Set Con
s
then Pattern -> IsComplete
Incomplete Pattern
W
else case forall a. Set a -> a
Set.findMin Set Con
s of
Con
CEmpty -> if Set Con
s forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Con
COne, Con
CEmpty] then IsComplete
Complete else Pattern -> IsComplete
Incomplete forall a b. (a -> b) -> a -> b
$ Con -> [Pattern] -> Pattern
C Con
COne [Pattern
W]
Con
COne -> if Set Con
s forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Con
COne, Con
CEmpty] then IsComplete
Complete else Pattern -> IsComplete
Incomplete forall a b. (a -> b) -> a -> b
$ Con -> [Pattern] -> Pattern
C Con
CEmpty []
CTuple Int
_ -> IsComplete
Complete
CEnum VCObjectHash
e Text
_ ->
let e_sig :: Set Con
e_sig = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry VCObjectHash -> Text -> Con
CEnum) forall a b. (a -> b) -> a -> b
$ Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs forall k a. Ord k => Map k a -> k -> a
Map.! VCObjectHash
e
in if Set Con
s forall a. Eq a => a -> a -> Bool
== Set Con
e_sig
then IsComplete
Complete
else Pattern -> IsComplete
Incomplete forall a b. (a -> b) -> a -> b
$ Con -> [Pattern] -> Pattern
C (forall a. Set a -> a
Set.findMin forall a b. (a -> b) -> a -> b
$ Set Con
e_sig forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Con
s) []
CInf a
n -> Pattern -> IsComplete
Incomplete forall a b. (a -> b) -> a -> b
$ Con -> [Pattern] -> Pattern
C (forall a. (Show a, Pretty a, Enum a) => a -> Con
findSucc a
n) []
where
findSucc :: (Show a, Pretty a, Enum a) => a -> Con
findSucc :: forall a. (Show a, Pretty a, Enum a) => a -> Con
findSucc a
n = let sn :: Con
sn = (forall a. (Show a, Pretty a, Enum a) => a -> Con
CInf forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ a
n) in if Con
sn forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Con
s then forall a. (Show a, Pretty a, Enum a) => a -> Con
findSucc (forall a. Enum a => a -> a
succ a
n) else Con
sn
isUseful :: Map VCObjectHash (Set (VCObjectHash, Text)) -> PMatrix -> [Pattern] -> Bool
isUseful :: Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
_ [] [Pattern]
_ = Bool
True
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
_ ([] : PMatrix
_) [Pattern]
_ = Bool
False
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
_ PMatrix
_ [] = Bool
False
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
p q :: [Pattern]
q@(Pattern
q1 : [Pattern]
qs) = case Pattern
q1 of
C Con
c [Pattern]
_ ->
let sP :: PMatrix
sP = Con -> PMatrix -> PMatrix
specialize Con
c PMatrix
p
in case Con -> [Pattern] -> Maybe [Pattern]
specializeVec Con
c [Pattern]
q of
Just [Pattern]
sq -> Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
sP [Pattern]
sq
Maybe [Pattern]
Nothing -> forall a. HasCallStack => String -> a
error String
"unreachable specializeVec"
Pattern
W ->
let sig :: Set Con
sig = [Pattern] -> Set Con
conNames forall a b. (a -> b) -> a -> b
$ PMatrix -> [Pattern]
col PMatrix
p
in if IsComplete -> Bool
isComplete forall a b. (a -> b) -> a -> b
$ Map VCObjectHash (Set (VCObjectHash, Text))
-> Set Con -> IsComplete
isCompleteSignature Map VCObjectHash (Set (VCObjectHash, Text))
sigs Set Con
sig
then
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
( \Con
ck -> case Con -> [Pattern] -> Maybe [Pattern]
specializeVec Con
ck [Pattern]
q of
Just [Pattern]
sq ->
let sP :: PMatrix
sP = Con -> PMatrix -> PMatrix
specialize Con
ck PMatrix
p
in Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
sP [Pattern]
sq
Maybe [Pattern]
Nothing -> Bool
False
)
Set Con
sig
else Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
sigs (PMatrix -> PMatrix
defaultMatrix PMatrix
p) [Pattern]
qs
defaultMatrix :: PMatrix -> PMatrix
defaultMatrix :: PMatrix -> PMatrix
defaultMatrix [] = []
defaultMatrix ((C Con
_ [Pattern]
_ : [Pattern]
_) : PMatrix
rest) = PMatrix -> PMatrix
defaultMatrix PMatrix
rest
defaultMatrix ((Pattern
W : [Pattern]
pis) : PMatrix
rest) = [Pattern]
pis forall a. a -> [a] -> [a]
: PMatrix -> PMatrix
defaultMatrix PMatrix
rest
defaultMatrix PMatrix
_ = forall a. HasCallStack => String -> a
error String
"malformed PMatrix"
cTuple :: [Pattern] -> Pattern
cTuple :: [Pattern] -> Pattern
cTuple [Pattern]
xs = Con -> [Pattern] -> Pattern
C (Int -> Con
CTuple (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern]
xs)) [Pattern]
xs
cOne :: Pattern -> Pattern
cOne :: Pattern -> Pattern
cOne Pattern
x = Con -> [Pattern] -> Pattern
C Con
COne [Pattern
x]
cEmpty :: Pattern
cEmpty :: Pattern
cEmpty = Con -> [Pattern] -> Pattern
C Con
CEmpty []
cEnum :: VCObjectHash -> Text -> Pattern
cEnum :: VCObjectHash -> Text -> Pattern
cEnum VCObjectHash
h Text
t = Con -> [Pattern] -> Pattern
C (VCObjectHash -> Text -> Con
CEnum VCObjectHash
h Text
t) []
cInf :: (Show a, Pretty a, Enum a) => a -> Pattern
cInf :: forall a. (Show a, Pretty a, Enum a) => a -> Pattern
cInf a
n = Con -> [Pattern] -> Pattern
C (forall a. (Show a, Pretty a, Enum a) => a -> Con
CInf a
n) []
exhaustive :: Map VCObjectHash (Set (VCObjectHash, Text)) -> PMatrix -> Maybe [Pattern]
exhaustive :: Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> Maybe [Pattern]
exhaustive Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
pm = Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> Int -> Maybe [Pattern]
i Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
pm Int
1
where
i :: Map VCObjectHash (Set (VCObjectHash, Text)) -> PMatrix -> Int -> Maybe [Pattern]
i :: Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> Int -> Maybe [Pattern]
i Map VCObjectHash (Set (VCObjectHash, Text))
_ [] Int
n = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
n Pattern
W
i Map VCObjectHash (Set (VCObjectHash, Text))
_ ([] : PMatrix
_) Int
0 = forall a. Maybe a
Nothing
i Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs PMatrix
p Int
n =
let sig :: Set Con
sig = [Pattern] -> Set Con
conNames forall a b. (a -> b) -> a -> b
$ PMatrix -> [Pattern]
col PMatrix
p
in case Map VCObjectHash (Set (VCObjectHash, Text))
-> Set Con -> IsComplete
isCompleteSignature Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs Set Con
sig of
IsComplete
Complete -> [Con] -> Maybe [Pattern]
go forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Con
sig
Incomplete Pattern
somePat -> (Pattern
somePat forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> Int -> Maybe [Pattern]
i Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs (PMatrix -> PMatrix
defaultMatrix PMatrix
p) (Int
n forall a. Num a => a -> a -> a
-Int
1)
where
go :: [Con] -> Maybe [Pattern]
go [] = forall a. Maybe a
Nothing
go (Con
ck : [Con]
rest) =
let sP :: PMatrix
sP = Con -> PMatrix -> PMatrix
specialize Con
ck PMatrix
p
in case Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> Int -> Maybe [Pattern]
i Map VCObjectHash (Set (VCObjectHash, Text))
sigs PMatrix
sP (Con -> Int
cSize Con
ck forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
- Int
1) of
Maybe [Pattern]
Nothing -> [Con] -> Maybe [Pattern]
go [Con]
rest
Just [Pattern]
pat ->
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
[Con -> [Pattern] -> Pattern
C Con
ck forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (Con -> Int
cSize Con
ck) [Pattern]
pat] forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (Con -> Int
cSize Con
ck) [Pattern]
pat
checkUsefullness :: Map VCObjectHash (Set (VCObjectHash, Text)) -> PMatrix -> [(Int, Int)]
checkUsefullness :: Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [(Int, Int)]
checkUsefullness Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs PMatrix
p = forall {a}. Num a => a -> PMatrix -> PMatrix -> [(a, Int)]
go Int
0 [] PMatrix
p
where
go :: a -> PMatrix -> PMatrix -> [(a, Int)]
go a
_ PMatrix
_ [] = []
go a
n PMatrix
preceding ([Pattern]
p_i : PMatrix
rest) =
if Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs PMatrix
preceding [Pattern]
p_i
then a -> PMatrix -> PMatrix -> [(a, Int)]
go (a
n forall a. Num a => a -> a -> a
+ a
1) (PMatrix
preceding forall a. [a] -> [a] -> [a]
++ [[Pattern]
p_i]) PMatrix
rest
else (a
n, [Pattern] -> Int -> PMatrix -> Int
findOverlap [Pattern]
p_i Int
0 PMatrix
preceding) forall a. a -> [a] -> [a]
: a -> PMatrix -> PMatrix -> [(a, Int)]
go (a
n forall a. Num a => a -> a -> a
+ a
1) (PMatrix
preceding forall a. [a] -> [a] -> [a]
++ [[Pattern]
p_i]) PMatrix
rest
findOverlap :: [Pattern] -> Int -> PMatrix -> Int
findOverlap :: [Pattern] -> Int -> PMatrix -> Int
findOverlap [Pattern]
_ Int
n [] = Int
n
findOverlap [Pattern]
p_i Int
n ([Pattern]
x : PMatrix
xs) =
if Map VCObjectHash (Set (VCObjectHash, Text))
-> PMatrix -> [Pattern] -> Bool
isUseful Map VCObjectHash (Set (VCObjectHash, Text))
enum_sigs [[Pattern]
x] [Pattern]
p_i
then [Pattern] -> Int -> PMatrix -> Int
findOverlap [Pattern]
p_i (Int
n forall a. Num a => a -> a -> a
+ Int
1) PMatrix
xs
else Int
n
newtype EnumText = EnumText Text
mkEnumText :: Text -> EnumText
mkEnumText :: Text -> EnumText
mkEnumText = Text -> EnumText
EnumText
instance Show EnumText where
show :: EnumText -> String
show (EnumText Text
t) = forall a. Show a => a -> String
show Text
t
instance Pretty EnumText where
pretty :: forall ann. EnumText -> Doc ann
pretty (EnumText Text
t) = forall a ann. Pretty a => a -> Doc ann
pretty forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Text
t
instance Enum EnumText where
toEnum :: Int -> EnumText
toEnum = forall a. HasCallStack => a
undefined
fromEnum :: EnumText -> Int
fromEnum = forall a. HasCallStack => a
undefined
succ :: EnumText -> EnumText
succ (EnumText Text
t) =
Text -> EnumText
EnumText forall a b. (a -> b) -> a -> b
$
if Text -> Bool
Text.null Text
t
then Text
"a"
else Text
t forall a. Semigroup a => a -> a -> a
<> Text
t