-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

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

-- |
-- 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.
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
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)

-- | 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
_) = 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
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)

-- | 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 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 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 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]

-- | 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 = 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' 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 =
  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)
(==>) = (,)

-- 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 = 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))
-- Otherwise, just look up in the qualRulesMap.
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 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 <- 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)

  -- 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.
  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

-- | Pick a base type (generally the "simplest") that satisfies a given sort.
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