-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Types.Rules
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- "Disco.Types.Rules" defines some generic rules about arity,
-- subtyping, and sorts for disco base types.
--
-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

module Disco.Types.Rules
  ( -- * Arity

    Variance(..), arity

    -- * Qualifiers
  , Qualifier(..), bopQual

    -- * Sorts
  , Sort, topSort

    -- * Subtyping rules

  , Dir(..), other

  , isSubA, isSubB, isDirB
  , supertypes, subtypes, dirtypes

    -- * Qualifier and sort rules

  , 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

------------------------------------------------------------
-- Arity
------------------------------------------------------------

-- | A particular type argument can be either co- or contravariant
--   with respect to subtyping.
data Variance = Co | Contra
  deriving (Int -> Variance -> ShowS
[Variance] -> ShowS
Variance -> String
(Int -> Variance -> ShowS)
-> (Variance -> String) -> ([Variance] -> ShowS) -> Show Variance
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]
(Int -> ReadS Variance)
-> ReadS [Variance]
-> ReadPrec Variance
-> ReadPrec [Variance]
-> Read 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
(Variance -> Variance -> Bool)
-> (Variance -> Variance -> Bool) -> Eq Variance
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
Eq Variance
-> (Variance -> Variance -> Ordering)
-> (Variance -> Variance -> Bool)
-> (Variance -> Variance -> Bool)
-> (Variance -> Variance -> Bool)
-> (Variance -> Variance -> Bool)
-> (Variance -> Variance -> Variance)
-> (Variance -> Variance -> Variance)
-> Ord 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
$cp1Ord :: Eq Variance
Ord)

-- | The arity of a type constructor is a list of variances,
--   expressing both how many type arguments the constructor takes,
--   and the variance of each argument.  This is used to decompose
--   subtyping constraints.
--
--   For example, @arity CArr = [Contra, Co]@ since function arrow is
--   contravariant in its first argument and covariant in its second.
--   That is, @S1 -> T1 <: S2 -> T2@ (@<:@ means "is a subtype of") if
--   and only if @S2 <: S1@ and @T1 <: T2@.
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
_)      = String -> [Variance]
forall a. HasCallStack => String -> a
error String
"Impossible! arity CUser"
  -- CUsers should always be replaced by their definitions before arity
  -- is called.

------------------------------------------------------------
-- Subtyping rules
------------------------------------------------------------

-- | A "direction" for the subtyping relation (either subtype or
--   supertype).
data Dir = SubTy | SuperTy
  deriving (Dir -> Dir -> Bool
(Dir -> Dir -> Bool) -> (Dir -> Dir -> Bool) -> Eq Dir
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
Eq Dir
-> (Dir -> Dir -> Ordering)
-> (Dir -> Dir -> Bool)
-> (Dir -> Dir -> Bool)
-> (Dir -> Dir -> Bool)
-> (Dir -> Dir -> Bool)
-> (Dir -> Dir -> Dir)
-> (Dir -> Dir -> Dir)
-> Ord 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
$cp1Ord :: Eq Dir
Ord, ReadPrec [Dir]
ReadPrec Dir
Int -> ReadS Dir
ReadS [Dir]
(Int -> ReadS Dir)
-> ReadS [Dir] -> ReadPrec Dir -> ReadPrec [Dir] -> Read 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
(Int -> Dir -> ShowS)
-> (Dir -> String) -> ([Dir] -> ShowS) -> Show Dir
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)

-- | Swap directions.
other :: Dir -> Dir
other :: Dir -> Dir
other Dir
SubTy   = Dir
SuperTy
other Dir
SuperTy = Dir
SubTy

--------------------------------------------------
-- Subtype checks

-- | Check whether one atomic type is a subtype of the other. Returns
--   @True@ if either they are equal, or if they are base types and
--   'isSubB' returns true.
isSubA :: Atom -> Atom -> Bool
isSubA :: Atom -> Atom -> Bool
isSubA Atom
a1 Atom
a2                 | Atom
a1 Atom -> Atom -> Bool
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

-- | Check whether one base type is a subtype of another.
isSubB :: BaseTy -> BaseTy -> Bool
isSubB :: BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 | BaseTy
b1 BaseTy -> BaseTy -> Bool
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

-- | Check whether one base type is a sub- or supertype of another.
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

-- | List all the supertypes of a given base type.
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]

-- | List all the subtypes of a given base type.
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]

-- | List all the sub- or supertypes of a given base type.
dirtypes :: Dir -> BaseTy -> [BaseTy]
dirtypes :: Dir -> BaseTy -> [BaseTy]
dirtypes Dir
SubTy   = BaseTy -> [BaseTy]
subtypes
dirtypes Dir
SuperTy = BaseTy -> [BaseTy]
supertypes

------------------------------------------------------------
-- Qualifier and sort rules
------------------------------------------------------------

-- | Check whether a given base type satisfies a qualifier.
hasQual :: BaseTy -> Qualifier -> Bool
hasQual :: BaseTy -> Qualifier -> Bool
hasQual BaseTy
P       Qualifier
QCmp    = Bool
False    -- can't compare Props
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 (Fin _) q     | q `elem` [QNum, QSub, QEnum] = True
-- hasQual (Fin n) QDiv  = isPrime n
hasQual BaseTy
b       Qualifier
QNum    = BaseTy
b BaseTy -> [BaseTy] -> Bool
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 BaseTy -> [BaseTy] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
Z, BaseTy
Q]
hasQual BaseTy
b       Qualifier
QDiv    = BaseTy
b BaseTy -> [BaseTy] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
F, BaseTy
Q]
hasQual BaseTy
b       Qualifier
QEnum   = BaseTy
b BaseTy -> [BaseTy] -> Bool
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 BaseTy -> [BaseTy] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
B, BaseTy
P]

-- | Check whether a base type has a certain sort, which simply
--   amounts to whether it satisfies every qualifier in the sort.
hasSort :: BaseTy -> Sort -> Bool
hasSort :: BaseTy -> Sort -> Bool
hasSort = (Qualifier -> Bool) -> Sort -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Qualifier -> Bool) -> Sort -> Bool)
-> (BaseTy -> Qualifier -> Bool) -> BaseTy -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTy -> Qualifier -> Bool
hasQual

-- | 'qualRulesMap' encodes some of the rules by which applications of
--   type constructors can satisfy various qualifiers.
--
--   Each constructor maps to a set of rules.  Each rule is a mapping
--   from a qualifier to the list of qualifiers needed on the type
--   constructor's arguments for the bigger type to satisfy the
--   qualifier.
--
--   Note in Disco we can get away with any given qualifier requiring
--   /at most one/ qualifier on each type argument.  Then we can
--   derive the 'sortRules' by combining 'qualRules'.  In general,
--   however, you could imagine some particular qualifier requiring a
--   set of qualifiers (i.e. a general sort) on a type argument.  In
--   that case one would just have to encode 'sortRules' directly.
qualRulesMap :: Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap :: Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap = [(Con, Map Qualifier [Maybe Qualifier])]
-> Map Con (Map Qualifier [Maybe Qualifier])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  [ Con
CProd Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp, Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QSimple Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple, Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple]
    ]
  , Con
CSum Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp, Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QSimple Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple, Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple]
    ]
  , Con
CList Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QSimple Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple]
    ]
  , Con
CBag Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QSimple Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple]
    ]
  , Con
CSet Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QSimple Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QSimple]
    ]
  , Con
CGraph Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp],
      Qualifier
QNum Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Maybe Qualifier
forall a. Maybe a
Nothing]
    ]
  , Con
CMap Con
-> Map Qualifier [Maybe Qualifier]
-> (Con, Map Qualifier [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [(Qualifier, [Maybe Qualifier])] -> Map Qualifier [Maybe Qualifier]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ Qualifier
QCmp Qualifier -> [Maybe Qualifier] -> (Qualifier, [Maybe Qualifier])
forall a b. a -> b -> (a, b)
==> [Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp, Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QCmp]
    ]
  ]
  where
    (==>) :: a -> b -> (a,b)
    ==> :: a -> b -> (a, b)
(==>) = (,)

  -- We could (theoretically) make graphs and maps also be simple values if we require the map's values are also simple.

  -- Eventually we can easily imagine adding an opt-in mode where
  -- numeric operations can be used on pairs and functions, then the
  -- qualRules would become dependent on what language extension/mode
  -- was chosen.  For example we could have rules like
  --
  -- [ CArr ==> M.fromList
  --   [ QNum ==> [Nothing, Just QNum]  -- (a -> b) can be +, * iff b can
  --   , QSub ==> [Nothing, Just QSub]  -- ditto for subtraction
  --   , QDiv ==> [Nothing, Just QDiv]  -- and division
  --   ]
  -- , CProd ==> M.fromList
  --   [ QNum ==> [Just QNum, Just QNum] -- (a,b) can be +, * iff a and b can
  --   , QSub ==> [Just QSub, Just QSub] -- etc.
  --   , QDiv ==> [Just QDiv, Just QDiv]
  --   ]
  -- ]

-- | Given a constructor T and a qualifier we want to hold of a type T
--   t1 t2 ..., return a list of qualifiers that need to hold of t1,
--   t2, ...
qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier]
-- T t1 t2 ... is basic (contains no Prop) iff t1, t2 ... all are.
qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules Con
c Qualifier
QBasic = [Maybe Qualifier] -> Maybe [Maybe Qualifier]
forall a. a -> Maybe a
Just ((Variance -> Maybe Qualifier) -> [Variance] -> [Maybe Qualifier]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Qualifier -> Variance -> Maybe Qualifier
forall a b. a -> b -> a
const (Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
Just Qualifier
QBasic)) (Con -> [Variance]
arity Con
c))
-- Otherwise, just look up in the qualRulesMap.
qualRules Con
c Qualifier
q      = (Con
-> Map Con (Map Qualifier [Maybe Qualifier])
-> Maybe (Map Qualifier [Maybe Qualifier])
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Con
c (Map Con (Map Qualifier [Maybe Qualifier])
 -> Maybe (Map Qualifier [Maybe Qualifier]))
-> (Map Qualifier [Maybe Qualifier] -> Maybe [Maybe Qualifier])
-> Map Con (Map Qualifier [Maybe Qualifier])
-> Maybe [Maybe Qualifier]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Qualifier
-> Map Qualifier [Maybe Qualifier] -> Maybe [Maybe Qualifier]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualifier
q) Map Con (Map Qualifier [Maybe Qualifier])
qualRulesMap

-- | @sortRules T s = [s1, ..., sn]@ means that sort @s@ holds of
--   type @(T t1 ... tn)@ if and only if  @s1 t1 /\ ... /\ sn tn@.
--   For now this is just derived directly from 'qualRules'.
--
--   This is the @arity@ function described in section 4.1 of Traytel et
--   al.
sortRules :: Con -> Sort -> Maybe [Sort]
sortRules :: Con -> Sort -> Maybe [Sort]
sortRules Con
c Sort
s = do
  -- If any of the quals q in sort s are not in the map corresponding
  -- to tycon c, there's no way to make c an instance of q, so fail
  -- (the mapM will succeed only if all lookups succeed)
  [[Maybe Qualifier]]
needQuals <- (Qualifier -> Maybe [Maybe Qualifier])
-> [Qualifier] -> Maybe [[Maybe Qualifier]]
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) (Sort -> [Qualifier]
forall a. Set a -> [a]
S.toList Sort
s)

  -- Otherwise we are left with a list (corresponding to all the quals
  -- in sort s) of lists (each one corresponds to the type args of c).
  -- We zip them together to produce a list of sorts.
  [Sort] -> Maybe [Sort]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Sort] -> Maybe [Sort]) -> [Sort] -> Maybe [Sort]
forall a b. (a -> b) -> a -> b
$ ([Sort] -> [Maybe Qualifier] -> [Sort])
-> [Sort] -> [[Maybe Qualifier]] -> [Sort]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Sort -> Maybe Qualifier -> Sort)
-> [Sort] -> [Maybe Qualifier] -> [Sort]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Sort
srt -> Sort -> (Qualifier -> Sort) -> Maybe Qualifier -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
srt (Qualifier -> Sort -> Sort
forall a. Ord a => a -> Set a -> Set a
`S.insert` Sort
srt))) (Sort -> [Sort]
forall a. a -> [a]
repeat Sort
topSort) [[Maybe Qualifier]]
needQuals

-- | Pick a base type (generally the "simplest") that satisfies a given sort.
pickSortBaseTy :: Sort -> BaseTy
pickSortBaseTy :: Sort -> BaseTy
pickSortBaseTy Sort
s
  | Qualifier
QDiv    Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s Bool -> Bool -> Bool
&& Qualifier
QSub Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
Q
  | Qualifier
QDiv    Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
F
  | Qualifier
QSub    Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
Z
  | Qualifier
QNum    Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
  | Qualifier
QCmp    Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
  | Qualifier
QEnum   Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
  | Qualifier
QBool   Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
B
  | Qualifier
QSimple Qualifier -> Sort -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Sort
s = BaseTy
N
  | Bool
otherwise            = BaseTy
Unit