module Disco.Types.Rules (
Variance (..),
arity,
Qualifier (..),
bopQual,
Sort,
topSort,
Dir (..),
other,
isSubA,
isSubB,
isDirB,
supertypes,
subtypes,
dirtypes,
hasQual,
hasSort,
qualRules,
sortRules,
pickSortBaseTy,
)
where
import Control.Monad ((>=>))
import Data.List (foldl')
import Data.Map (Map)
import qualified Data.Map as M
import qualified Data.Set as S
import Disco.Types
import Disco.Types.Qualifiers
data Variance = Co | Contra
deriving (Int -> Variance -> ShowS
[Variance] -> ShowS
Variance -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Variance] -> ShowS
$cshowList :: [Variance] -> ShowS
show :: Variance -> String
$cshow :: Variance -> String
showsPrec :: Int -> Variance -> ShowS
$cshowsPrec :: Int -> Variance -> ShowS
Show, ReadPrec [Variance]
ReadPrec Variance
Int -> ReadS Variance
ReadS [Variance]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Variance]
$creadListPrec :: ReadPrec [Variance]
readPrec :: ReadPrec Variance
$creadPrec :: ReadPrec Variance
readList :: ReadS [Variance]
$creadList :: ReadS [Variance]
readsPrec :: Int -> ReadS Variance
$creadsPrec :: Int -> ReadS Variance
Read, Variance -> Variance -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Variance -> Variance -> Bool
$c/= :: Variance -> Variance -> Bool
== :: Variance -> Variance -> Bool
$c== :: Variance -> Variance -> Bool
Eq, Eq Variance
Variance -> Variance -> Bool
Variance -> Variance -> Ordering
Variance -> Variance -> Variance
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 :: Variance -> Variance -> Variance
$cmin :: Variance -> Variance -> Variance
max :: Variance -> Variance -> Variance
$cmax :: Variance -> Variance -> Variance
>= :: Variance -> Variance -> Bool
$c>= :: Variance -> Variance -> Bool
> :: Variance -> Variance -> Bool
$c> :: Variance -> Variance -> Bool
<= :: Variance -> Variance -> Bool
$c<= :: Variance -> Variance -> Bool
< :: Variance -> Variance -> Bool
$c< :: Variance -> Variance -> Bool
compare :: Variance -> Variance -> Ordering
$ccompare :: Variance -> Variance -> Ordering
Ord)
arity :: Con -> [Variance]
arity :: Con -> [Variance]
arity Con
CArr = [Variance
Contra, Variance
Co]
arity Con
CProd = [Variance
Co, Variance
Co]
arity Con
CSum = [Variance
Co, Variance
Co]
arity (CContainer Atom
_) = [Variance
Co]
arity Con
CMap = [Variance
Contra, Variance
Co]
arity Con
CGraph = [Variance
Co]
arity (CUser String
_) = forall a. HasCallStack => String -> a
error String
"Impossible! arity CUser"
data Dir = SubTy | SuperTy
deriving (Dir -> Dir -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Dir -> Dir -> Bool
$c/= :: Dir -> Dir -> Bool
== :: Dir -> Dir -> Bool
$c== :: Dir -> Dir -> Bool
Eq, Eq Dir
Dir -> Dir -> Bool
Dir -> Dir -> Ordering
Dir -> Dir -> Dir
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 :: Dir -> Dir -> Dir
$cmin :: Dir -> Dir -> Dir
max :: Dir -> Dir -> Dir
$cmax :: Dir -> Dir -> Dir
>= :: Dir -> Dir -> Bool
$c>= :: Dir -> Dir -> Bool
> :: Dir -> Dir -> Bool
$c> :: Dir -> Dir -> Bool
<= :: Dir -> Dir -> Bool
$c<= :: Dir -> Dir -> Bool
< :: Dir -> Dir -> Bool
$c< :: Dir -> Dir -> Bool
compare :: Dir -> Dir -> Ordering
$ccompare :: Dir -> Dir -> Ordering
Ord, ReadPrec [Dir]
ReadPrec Dir
Int -> ReadS Dir
ReadS [Dir]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Dir]
$creadListPrec :: ReadPrec [Dir]
readPrec :: ReadPrec Dir
$creadPrec :: ReadPrec Dir
readList :: ReadS [Dir]
$creadList :: ReadS [Dir]
readsPrec :: Int -> ReadS Dir
$creadsPrec :: Int -> ReadS Dir
Read, Int -> Dir -> ShowS
[Dir] -> ShowS
Dir -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dir] -> ShowS
$cshowList :: [Dir] -> ShowS
show :: Dir -> String
$cshow :: Dir -> String
showsPrec :: Int -> Dir -> ShowS
$cshowsPrec :: Int -> Dir -> ShowS
Show)
other :: Dir -> Dir
other :: Dir -> Dir
other Dir
SubTy = Dir
SuperTy
other Dir
SuperTy = Dir
SubTy
isSubA :: Atom -> Atom -> Bool
isSubA :: Atom -> Atom -> Bool
isSubA Atom
a1 Atom
a2 | Atom
a1 forall a. Eq a => a -> a -> Bool
== Atom
a2 = Bool
True
isSubA (ABase BaseTy
t1) (ABase BaseTy
t2) = BaseTy -> BaseTy -> Bool
isSubB BaseTy
t1 BaseTy
t2
isSubA Atom
_ Atom
_ = Bool
False
isSubB :: BaseTy -> BaseTy -> Bool
isSubB :: BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 | BaseTy
b1 forall a. Eq a => a -> a -> Bool
== BaseTy
b2 = Bool
True
isSubB BaseTy
N BaseTy
Z = Bool
True
isSubB BaseTy
N BaseTy
F = Bool
True
isSubB BaseTy
N BaseTy
Q = Bool
True
isSubB BaseTy
Z BaseTy
Q = Bool
True
isSubB BaseTy
F BaseTy
Q = Bool
True
isSubB BaseTy
B BaseTy
P = Bool
True
isSubB BaseTy
_ BaseTy
_ = Bool
False
isDirB :: Dir -> BaseTy -> BaseTy -> Bool
isDirB :: Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
SubTy BaseTy
b1 BaseTy
b2 = BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2
isDirB Dir
SuperTy BaseTy
b1 BaseTy
b2 = BaseTy -> BaseTy -> Bool
isSubB BaseTy
b2 BaseTy
b1
supertypes :: BaseTy -> [BaseTy]
supertypes :: BaseTy -> [BaseTy]
supertypes BaseTy
N = [BaseTy
N, BaseTy
Z, BaseTy
F, BaseTy
Q]
supertypes BaseTy
Z = [BaseTy
Z, BaseTy
Q]
supertypes BaseTy
F = [BaseTy
F, BaseTy
Q]
supertypes BaseTy
B = [BaseTy
B, BaseTy
P]
supertypes BaseTy
ty = [BaseTy
ty]
subtypes :: BaseTy -> [BaseTy]
subtypes :: BaseTy -> [BaseTy]
subtypes BaseTy
Q = [BaseTy
Q, BaseTy
F, BaseTy
Z, BaseTy
N]
subtypes BaseTy
F = [BaseTy
F, BaseTy
N]
subtypes BaseTy
Z = [BaseTy
Z, BaseTy
N]
subtypes BaseTy
P = [BaseTy
P, BaseTy
B]
subtypes BaseTy
ty = [BaseTy
ty]
dirtypes :: Dir -> BaseTy -> [BaseTy]
dirtypes :: Dir -> BaseTy -> [BaseTy]
dirtypes Dir
SubTy = BaseTy -> [BaseTy]
subtypes
dirtypes Dir
SuperTy = BaseTy -> [BaseTy]
supertypes
hasQual :: BaseTy -> Qualifier -> Bool
hasQual :: BaseTy -> Qualifier -> Bool
hasQual BaseTy
P Qualifier
QCmp = Bool
False
hasQual BaseTy
_ Qualifier
QCmp = Bool
True
hasQual BaseTy
P Qualifier
QBasic = Bool
False
hasQual BaseTy
_ Qualifier
QBasic = Bool
True
hasQual BaseTy
P Qualifier
QSimple = Bool
False
hasQual BaseTy
_ Qualifier
QSimple = Bool
True
hasQual BaseTy
b Qualifier
QNum = BaseTy
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
N, BaseTy
Z, BaseTy
F, BaseTy
Q]
hasQual BaseTy
b Qualifier
QSub = BaseTy
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
Z, BaseTy
Q]
hasQual BaseTy
b Qualifier
QDiv = BaseTy
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
F, BaseTy
Q]
hasQual BaseTy
b Qualifier
QEnum = BaseTy
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
N, BaseTy
Z, BaseTy
F, BaseTy
Q, BaseTy
C]
hasQual BaseTy
b Qualifier
QBool = BaseTy
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
B, BaseTy
P]
hasSort :: BaseTy -> Sort -> Bool
hasSort :: BaseTy -> Sort -> Bool
hasSort = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTy -> Qualifier -> Bool
hasQual
qualRulesMap :: Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap :: Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap =
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Con
CProd
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp, forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QSimple forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QSimple, forall a. a -> Maybe a
Just Qualifier
QSimple]
]
, Con
CSum
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp, forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QSimple forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QSimple, forall a. a -> Maybe a
Just Qualifier
QSimple]
]
, Con
CList
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QSimple forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QSimple]
]
, Con
CBag
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QSimple forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QSimple]
]
, Con
CSet
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QSimple forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QSimple]
]
, Con
CGraph
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp]
, Qualifier
QNum forall a b. a -> b -> (a, b)
==> [forall a. Maybe a
Nothing]
]
, Con
CMap
forall a b. a -> b -> (a, b)
==> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ Qualifier
QCmp forall a b. a -> b -> (a, b)
==> [forall a. a -> Maybe a
Just Qualifier
QCmp, forall a. a -> Maybe a
Just Qualifier
QCmp]
]
]
where
(==>) :: a -> b -> (a, b)
==> :: forall a b. a -> b -> (a, b)
(==>) = (,)
qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules Con
c Qualifier
QBasic = forall a. a -> Maybe a
Just (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> b -> a
const (forall a. a -> Maybe a
Just Qualifier
QBasic)) (Con -> [Variance]
arity Con
c))
qualRules Con
c Qualifier
q = (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Con
c forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualifier
q) Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap
sortRules :: Con -> Sort -> Maybe [Sort]
sortRules :: Con -> Sort -> Maybe [Sort]
sortRules Con
c Sort
s = do
[[Maybe Qualifier]]
needQuals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules Con
c) (forall a. Set a -> [a]
S.toList Sort
s)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Sort
srt -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
srt (forall a. Ord a => a -> Set a -> Set a
`S.insert` Sort
srt))) (forall a. a -> [a]
repeat Sort
topSort) [[Maybe Qualifier]]
needQuals
pickSortBaseTy :: Sort -> BaseTy
pickSortBaseTy :: Sort -> BaseTy
pickSortBaseTy Sort
s
| Qualifier
QDiv forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s Bool -> Bool -> Bool
&& Qualifier
QSub forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
Q
| Qualifier
QDiv forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
F
| Qualifier
QSub forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
Z
| Qualifier
QNum forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
| Qualifier
QCmp forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
| Qualifier
QEnum forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
| Qualifier
QBool forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
B
| Qualifier
QSimple forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
| Bool
otherwise = BaseTy
Unit