-- | Syntax of size expressions and constraints.

module Agda.TypeChecking.SizedTypes.Syntax where

import Prelude hiding ( null )


import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.TypeChecking.Monad.Base (TCM)
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.SizedTypes.Utils

import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- * Syntax

-- | Constant finite sizes @n >= 0@.
newtype Offset = O Int
  deriving (Offset -> Offset -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Offset -> Offset -> Bool
$c/= :: Offset -> Offset -> Bool
== :: Offset -> Offset -> Bool
$c== :: Offset -> Offset -> Bool
Eq, Eq Offset
Offset -> Offset -> Bool
Offset -> Offset -> Ordering
Offset -> Offset -> Offset
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 :: Offset -> Offset -> Offset
$cmin :: Offset -> Offset -> Offset
max :: Offset -> Offset -> Offset
$cmax :: Offset -> Offset -> Offset
>= :: Offset -> Offset -> Bool
$c>= :: Offset -> Offset -> Bool
> :: Offset -> Offset -> Bool
$c> :: Offset -> Offset -> Bool
<= :: Offset -> Offset -> Bool
$c<= :: Offset -> Offset -> Bool
< :: Offset -> Offset -> Bool
$c< :: Offset -> Offset -> Bool
compare :: Offset -> Offset -> Ordering
$ccompare :: Offset -> Offset -> Ordering
Ord, Integer -> Offset
Offset -> Offset
Offset -> Offset -> Offset
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Offset
$cfromInteger :: Integer -> Offset
signum :: Offset -> Offset
$csignum :: Offset -> Offset
abs :: Offset -> Offset
$cabs :: Offset -> Offset
negate :: Offset -> Offset
$cnegate :: Offset -> Offset
* :: Offset -> Offset -> Offset
$c* :: Offset -> Offset -> Offset
- :: Offset -> Offset -> Offset
$c- :: Offset -> Offset -> Offset
+ :: Offset -> Offset -> Offset
$c+ :: Offset -> Offset -> Offset
Num, Int -> Offset
Offset -> Int
Offset -> [Offset]
Offset -> Offset
Offset -> Offset -> [Offset]
Offset -> Offset -> Offset -> [Offset]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
$cenumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
enumFromTo :: Offset -> Offset -> [Offset]
$cenumFromTo :: Offset -> Offset -> [Offset]
enumFromThen :: Offset -> Offset -> [Offset]
$cenumFromThen :: Offset -> Offset -> [Offset]
enumFrom :: Offset -> [Offset]
$cenumFrom :: Offset -> [Offset]
fromEnum :: Offset -> Int
$cfromEnum :: Offset -> Int
toEnum :: Int -> Offset
$ctoEnum :: Int -> Offset
pred :: Offset -> Offset
$cpred :: Offset -> Offset
succ :: Offset -> Offset
$csucc :: Offset -> Offset
Enum)

-- This Show instance is ok because of the Num constraint.
instance Show Offset where
  show :: Offset -> String
show (O Int
n) = forall a. Show a => a -> String
show Int
n

instance Pretty Offset where
  pretty :: Offset -> Doc
pretty (O Int
n) = forall a. Pretty a => a -> Doc
pretty Int
n

instance MeetSemiLattice Offset where
  meet :: Offset -> Offset -> Offset
meet = forall a. Ord a => a -> a -> a
min

instance Plus Offset Offset Offset where
  plus :: Offset -> Offset -> Offset
plus (O Int
x) (O Int
y) = Int -> Offset
O (forall a b c. Plus a b c => a -> b -> c
plus Int
x Int
y)

-- | Fixed size variables @i@.
newtype Rigid  = RigidId { Rigid -> String
rigidId :: String }
  deriving (Rigid -> Rigid -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rigid -> Rigid -> Bool
$c/= :: Rigid -> Rigid -> Bool
== :: Rigid -> Rigid -> Bool
$c== :: Rigid -> Rigid -> Bool
Eq, Eq Rigid
Rigid -> Rigid -> Bool
Rigid -> Rigid -> Ordering
Rigid -> Rigid -> Rigid
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 :: Rigid -> Rigid -> Rigid
$cmin :: Rigid -> Rigid -> Rigid
max :: Rigid -> Rigid -> Rigid
$cmax :: Rigid -> Rigid -> Rigid
>= :: Rigid -> Rigid -> Bool
$c>= :: Rigid -> Rigid -> Bool
> :: Rigid -> Rigid -> Bool
$c> :: Rigid -> Rigid -> Bool
<= :: Rigid -> Rigid -> Bool
$c<= :: Rigid -> Rigid -> Bool
< :: Rigid -> Rigid -> Bool
$c< :: Rigid -> Rigid -> Bool
compare :: Rigid -> Rigid -> Ordering
$ccompare :: Rigid -> Rigid -> Ordering
Ord)

instance Show Rigid where
  show :: Rigid -> String
show (RigidId String
s) = String
"RigidId " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
s

instance Pretty Rigid where
  pretty :: Rigid -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rigid -> String
rigidId

-- | Size meta variables @X@ to solve for.
newtype Flex   = FlexId { Flex -> String
flexId :: String }
  deriving (Flex -> Flex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Flex -> Flex -> Bool
$c/= :: Flex -> Flex -> Bool
== :: Flex -> Flex -> Bool
$c== :: Flex -> Flex -> Bool
Eq, Eq Flex
Flex -> Flex -> Bool
Flex -> Flex -> Ordering
Flex -> Flex -> Flex
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 :: Flex -> Flex -> Flex
$cmin :: Flex -> Flex -> Flex
max :: Flex -> Flex -> Flex
$cmax :: Flex -> Flex -> Flex
>= :: Flex -> Flex -> Bool
$c>= :: Flex -> Flex -> Bool
> :: Flex -> Flex -> Bool
$c> :: Flex -> Flex -> Bool
<= :: Flex -> Flex -> Bool
$c<= :: Flex -> Flex -> Bool
< :: Flex -> Flex -> Bool
$c< :: Flex -> Flex -> Bool
compare :: Flex -> Flex -> Ordering
$ccompare :: Flex -> Flex -> Ordering
Ord)

instance Show Flex where
  show :: Flex -> String
show (FlexId String
s) = String
"FlexId " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
s

instance Pretty Flex where
  pretty :: Flex -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flex -> String
flexId

instance P.PrettyTCM Flex where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Flex -> m Doc
prettyTCM = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty

-- | Size expressions appearing in constraints.
data SizeExpr' rigid flex
  = Const { forall rigid flex. SizeExpr' rigid flex -> Offset
offset :: Offset }                   -- ^ Constant number @n@.
  | Rigid { forall rigid flex. SizeExpr' rigid flex -> rigid
rigid  :: rigid, offset :: Offset }  -- ^ Variable plus offset @i + n@.
  | Infty                                        -- ^ Infinity @∞@.
  | Flex  { forall rigid flex. SizeExpr' rigid flex -> flex
flex   :: flex, offset :: Offset }   -- ^ Meta variable @X + n@.
    deriving (Int -> SizeExpr' rigid flex -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show rigid, Show flex) =>
Int -> SizeExpr' rigid flex -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
[SizeExpr' rigid flex] -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
SizeExpr' rigid flex -> String
showList :: [SizeExpr' rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[SizeExpr' rigid flex] -> ShowS
show :: SizeExpr' rigid flex -> String
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
SizeExpr' rigid flex -> String
showsPrec :: Int -> SizeExpr' rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> SizeExpr' rigid flex -> ShowS
Show, SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
/= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c/= :: forall rigid flex.
(Eq rigid, Eq flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
== :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c== :: forall rigid flex.
(Eq rigid, Eq flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
Eq, SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
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
forall {rigid} {flex}.
(Ord rigid, Ord flex) =>
Eq (SizeExpr' rigid flex)
forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid flex
min :: SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid flex
$cmin :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid flex
max :: SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid flex
$cmax :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid flex
>= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c>= :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
> :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c> :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
<= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c<= :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
< :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$c< :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
Ord, forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
forall rigid a b.
(a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
$c<$ :: forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
fmap :: forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
$cfmap :: forall rigid a b.
(a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
Functor, forall a. SizeExpr' rigid a -> Bool
forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
forall rigid a. Num a => SizeExpr' rigid a -> a
forall rigid a. Ord a => SizeExpr' rigid a -> a
forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
forall rigid m. Monoid m => SizeExpr' rigid m -> m
forall rigid a. SizeExpr' rigid a -> Bool
forall rigid a. SizeExpr' rigid a -> Int
forall rigid a. SizeExpr' rigid a -> [a]
forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => SizeExpr' rigid a -> a
$cproduct :: forall rigid a. Num a => SizeExpr' rigid a -> a
sum :: forall a. Num a => SizeExpr' rigid a -> a
$csum :: forall rigid a. Num a => SizeExpr' rigid a -> a
minimum :: forall a. Ord a => SizeExpr' rigid a -> a
$cminimum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
maximum :: forall a. Ord a => SizeExpr' rigid a -> a
$cmaximum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
elem :: forall a. Eq a => a -> SizeExpr' rigid a -> Bool
$celem :: forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
length :: forall a. SizeExpr' rigid a -> Int
$clength :: forall rigid a. SizeExpr' rigid a -> Int
null :: forall a. SizeExpr' rigid a -> Bool
$cnull :: forall rigid a. SizeExpr' rigid a -> Bool
toList :: forall a. SizeExpr' rigid a -> [a]
$ctoList :: forall rigid a. SizeExpr' rigid a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldr1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
$cfoldr1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
$cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
$cfoldl :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
$cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
$cfoldr :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
$cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
$cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
fold :: forall m. Monoid m => SizeExpr' rigid m -> m
$cfold :: forall rigid m. Monoid m => SizeExpr' rigid m -> m
Foldable, forall rigid. Functor (SizeExpr' rigid)
forall rigid. Foldable (SizeExpr' rigid)
forall rigid (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
forall rigid (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
forall rigid (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
sequence :: forall (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
$cmapM :: forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
$ctraverse :: forall rigid (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
Traversable)

type SizeExpr = SizeExpr' Rigid Flex

-- | Comparison operator, e.g. for size expression.
data Cmp
  = Lt  -- ^ @<@.
  | Le  -- ^ @≤@.
  deriving (Int -> Cmp -> ShowS
[Cmp] -> ShowS
Cmp -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cmp] -> ShowS
$cshowList :: [Cmp] -> ShowS
show :: Cmp -> String
$cshow :: Cmp -> String
showsPrec :: Int -> Cmp -> ShowS
$cshowsPrec :: Int -> Cmp -> ShowS
Show, Cmp -> Cmp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cmp -> Cmp -> Bool
$c/= :: Cmp -> Cmp -> Bool
== :: Cmp -> Cmp -> Bool
$c== :: Cmp -> Cmp -> Bool
Eq, Cmp
forall a. a -> a -> Bounded a
maxBound :: Cmp
$cmaxBound :: Cmp
minBound :: Cmp
$cminBound :: Cmp
Bounded, Int -> Cmp
Cmp -> Int
Cmp -> [Cmp]
Cmp -> Cmp
Cmp -> Cmp -> [Cmp]
Cmp -> Cmp -> Cmp -> [Cmp]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
$cenumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
enumFromTo :: Cmp -> Cmp -> [Cmp]
$cenumFromTo :: Cmp -> Cmp -> [Cmp]
enumFromThen :: Cmp -> Cmp -> [Cmp]
$cenumFromThen :: Cmp -> Cmp -> [Cmp]
enumFrom :: Cmp -> [Cmp]
$cenumFrom :: Cmp -> [Cmp]
fromEnum :: Cmp -> Int
$cfromEnum :: Cmp -> Int
toEnum :: Int -> Cmp
$ctoEnum :: Int -> Cmp
pred :: Cmp -> Cmp
$cpred :: Cmp -> Cmp
succ :: Cmp -> Cmp
$csucc :: Cmp -> Cmp
Enum)

instance Dioid Cmp where
  compose :: Cmp -> Cmp -> Cmp
compose     = forall a. Ord a => a -> a -> a
min
  unitCompose :: Cmp
unitCompose = Cmp
Le

-- | Comparison operator is ordered @'Lt' < 'Le'@.
instance Ord Cmp where
  Cmp
Lt <= :: Cmp -> Cmp -> Bool
<= Cmp
x  = Bool
True
  Cmp
Le <= Cmp
Lt = Bool
False
  Cmp
Le <= Cmp
Le = Bool
True

instance MeetSemiLattice Cmp where
  meet :: Cmp -> Cmp -> Cmp
meet = forall a. Ord a => a -> a -> a
min

instance Top Cmp where
  top :: Cmp
top = Cmp
Le

-- | Constraint: an inequation between size expressions,
--   e.g. @X < ∞@ or @i + 3 ≤ j@.
data Constraint' rigid flex = Constraint
  { forall rigid flex. Constraint' rigid flex -> SizeExpr' rigid flex
leftExpr  :: SizeExpr' rigid flex
  , forall rigid flex. Constraint' rigid flex -> Cmp
cmp       :: Cmp
  , forall rigid flex. Constraint' rigid flex -> SizeExpr' rigid flex
rightExpr :: SizeExpr' rigid flex
  }
  deriving (Int -> Constraint' rigid flex -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show rigid, Show flex) =>
Int -> Constraint' rigid flex -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
[Constraint' rigid flex] -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
Constraint' rigid flex -> String
showList :: [Constraint' rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Constraint' rigid flex] -> ShowS
show :: Constraint' rigid flex -> String
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Constraint' rigid flex -> String
showsPrec :: Int -> Constraint' rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Constraint' rigid flex -> ShowS
Show, forall a b. a -> Constraint' rigid b -> Constraint' rigid a
forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
forall rigid a b.
(a -> b) -> Constraint' rigid a -> Constraint' rigid b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Constraint' rigid b -> Constraint' rigid a
$c<$ :: forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
fmap :: forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
$cfmap :: forall rigid a b.
(a -> b) -> Constraint' rigid a -> Constraint' rigid b
Functor, forall a. Constraint' rigid a -> Bool
forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
forall rigid a. Num a => Constraint' rigid a -> a
forall rigid a. Ord a => Constraint' rigid a -> a
forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
forall rigid m. Monoid m => Constraint' rigid m -> m
forall rigid a. Constraint' rigid a -> Bool
forall rigid a. Constraint' rigid a -> Int
forall rigid a. Constraint' rigid a -> [a]
forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Constraint' rigid a -> a
$cproduct :: forall rigid a. Num a => Constraint' rigid a -> a
sum :: forall a. Num a => Constraint' rigid a -> a
$csum :: forall rigid a. Num a => Constraint' rigid a -> a
minimum :: forall a. Ord a => Constraint' rigid a -> a
$cminimum :: forall rigid a. Ord a => Constraint' rigid a -> a
maximum :: forall a. Ord a => Constraint' rigid a -> a
$cmaximum :: forall rigid a. Ord a => Constraint' rigid a -> a
elem :: forall a. Eq a => a -> Constraint' rigid a -> Bool
$celem :: forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
length :: forall a. Constraint' rigid a -> Int
$clength :: forall rigid a. Constraint' rigid a -> Int
null :: forall a. Constraint' rigid a -> Bool
$cnull :: forall rigid a. Constraint' rigid a -> Bool
toList :: forall a. Constraint' rigid a -> [a]
$ctoList :: forall rigid a. Constraint' rigid a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldr1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
$cfoldr1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
$cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
$cfoldl :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
$cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
$cfoldr :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
$cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
$cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
fold :: forall m. Monoid m => Constraint' rigid m -> m
$cfold :: forall rigid m. Monoid m => Constraint' rigid m -> m
Foldable, forall rigid. Functor (Constraint' rigid)
forall rigid. Foldable (Constraint' rigid)
forall rigid (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
forall rigid (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
forall rigid (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
$cmapM :: forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
$ctraverse :: forall rigid (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
Traversable)

type Constraint = Constraint' Rigid Flex

-- * Polarities to specify solutions.
------------------------------------------------------------------------

-- | What type of solution are we looking for?
data Polarity = Least | Greatest
  deriving (Polarity -> Polarity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c== :: Polarity -> Polarity -> Bool
Eq, Eq Polarity
Polarity -> Polarity -> Bool
Polarity -> Polarity -> Ordering
Polarity -> Polarity -> Polarity
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 :: Polarity -> Polarity -> Polarity
$cmin :: Polarity -> Polarity -> Polarity
max :: Polarity -> Polarity -> Polarity
$cmax :: Polarity -> Polarity -> Polarity
>= :: Polarity -> Polarity -> Bool
$c>= :: Polarity -> Polarity -> Bool
> :: Polarity -> Polarity -> Bool
$c> :: Polarity -> Polarity -> Bool
<= :: Polarity -> Polarity -> Bool
$c<= :: Polarity -> Polarity -> Bool
< :: Polarity -> Polarity -> Bool
$c< :: Polarity -> Polarity -> Bool
compare :: Polarity -> Polarity -> Ordering
$ccompare :: Polarity -> Polarity -> Ordering
Ord)

-- | Assigning a polarity to a flexible variable.
data PolarityAssignment flex = PolarityAssignment Polarity flex

-- | Type of solution wanted for each flexible.
type Polarities flex = Map flex Polarity

emptyPolarities :: Polarities flex
emptyPolarities :: forall flex. Polarities flex
emptyPolarities = forall k a. Map k a
Map.empty

-- Used in size-solver (Andreas, 2021-08-20)
polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex
polaritiesFromAssignments :: forall flex.
Ord flex =>
[PolarityAssignment flex] -> Polarities flex
polaritiesFromAssignments = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\ (PolarityAssignment Polarity
p flex
x) -> (flex
x,Polarity
p))

-- | Default polarity is 'Least'.
getPolarity :: Ord flex => Polarities flex -> flex -> Polarity
getPolarity :: forall flex. Ord flex => Polarities flex -> flex -> Polarity
getPolarity Polarities flex
pols flex
x = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Polarity
Least flex
x Polarities flex
pols

-- * Solutions.
------------------------------------------------------------------------

-- | Partial substitution from flexible variables to size expression.
newtype Solution rigid flex = Solution { forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution :: Map flex (SizeExpr' rigid flex) }
  deriving (Int -> Solution rigid flex -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show flex, Show rigid) =>
Int -> Solution rigid flex -> ShowS
forall rigid flex.
(Show flex, Show rigid) =>
[Solution rigid flex] -> ShowS
forall rigid flex.
(Show flex, Show rigid) =>
Solution rigid flex -> String
showList :: [Solution rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show flex, Show rigid) =>
[Solution rigid flex] -> ShowS
show :: Solution rigid flex -> String
$cshow :: forall rigid flex.
(Show flex, Show rigid) =>
Solution rigid flex -> String
showsPrec :: Int -> Solution rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show flex, Show rigid) =>
Int -> Solution rigid flex -> ShowS
Show, Solution rigid flex
Solution rigid flex -> Bool
forall a. a -> (a -> Bool) -> Null a
forall rigid flex. Solution rigid flex
forall rigid flex. Solution rigid flex -> Bool
null :: Solution rigid flex -> Bool
$cnull :: forall rigid flex. Solution rigid flex -> Bool
empty :: Solution rigid flex
$cempty :: forall rigid flex. Solution rigid flex
Null)

instance (Pretty r, Pretty f) => Pretty (Solution r f) where
  pretty :: Solution r f -> Doc
pretty (Solution Map f (SizeExpr' r f)
sol) = forall a. Pretty a => [a] -> Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall k a. Map k a -> [(k, a)]
Map.toList Map f (SizeExpr' r f)
sol) forall a b. (a -> b) -> a -> b
$ \ (f
x, SizeExpr' r f
e) ->
    forall a. Pretty a => a -> Doc
pretty f
x Doc -> Doc -> Doc
<+> Doc
":=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
e

emptySolution :: Solution r f
emptySolution :: forall rigid flex. Solution rigid flex
emptySolution = forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution forall k a. Map k a
Map.empty

-- | Executing a substitution.
class Substitute r f a where
  subst :: Solution r f -> a -> a

instance Ord f => Substitute r f (SizeExpr' r f) where
  subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f
subst (Solution Map f (SizeExpr' r f)
sol) SizeExpr' r f
e =
    case SizeExpr' r f
e of
      Flex f
x Offset
n -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe SizeExpr' r f
e (forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup f
x Map f (SizeExpr' r f)
sol
      SizeExpr' r f
_        -> SizeExpr' r f
e

instance Ord f => Substitute r f (Constraint' r f) where
  subst :: Solution r f -> Constraint' r f -> Constraint' r f
subst Solution r f
sol (Constraint SizeExpr' r f
e Cmp
cmp SizeExpr' r f
e') = forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol SizeExpr' r f
e) Cmp
cmp (forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol SizeExpr' r f
e')

instance Substitute r f a => Substitute r f [a] where
  subst :: Solution r f -> [a] -> [a]
subst = forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r f a. Substitute r f a => Solution r f -> a -> a
subst

instance Substitute r f a => Substitute r f (Map k a) where
  subst :: Solution r f -> Map k a -> Map k a
subst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r f a. Substitute r f a => Solution r f -> a -> a
subst

instance Ord f => Substitute r f (Solution r f) where
  subst :: Solution r f -> Solution r f -> Solution r f
subst Solution r f
s = forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution

-- | Add offset to size expression.
instance Plus (SizeExpr' r f) Offset (SizeExpr' r f) where
  plus :: SizeExpr' r f -> Offset -> SizeExpr' r f
plus SizeExpr' r f
e Offset
m =
    case SizeExpr' r f
e of
      Const   Offset
n -> forall rigid flex. Offset -> SizeExpr' rigid flex
Const   forall a b. (a -> b) -> a -> b
$ Offset
n forall a. Num a => a -> a -> a
+ Offset
m
      Rigid r
i Offset
n -> forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i forall a b. (a -> b) -> a -> b
$ Offset
n forall a. Num a => a -> a -> a
+ Offset
m
      Flex f
x  Offset
n -> forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x  forall a b. (a -> b) -> a -> b
$ Offset
n forall a. Num a => a -> a -> a
+ Offset
m
      SizeExpr' r f
Infty     -> forall rigid flex. SizeExpr' rigid flex
Infty

-- | Error messages produced by the constraint simplification monad.

type Error = TCM Doc

-- * Constraint simplification

type CTrans r f = Constraint' r f -> Either Error [Constraint' r f]

-- | Returns an error message if we have a contradictory constraint.
simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 :: forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 CTrans r f
test Constraint' r f
c = do
  let err :: Either (TCMT IO Doc) [Constraint' r f]
err = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size constraint" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' r f
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>
                   TCMT IO Doc
"is inconsistent"
  case Constraint' r f
c of
    -- rhs is Infty
    Constraint SizeExpr' r f
a           Cmp
Le  SizeExpr' r f
Infty -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint Const{}     Cmp
Lt  SizeExpr' r f
Infty -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint SizeExpr' r f
Infty       Cmp
Lt  SizeExpr' r f
Infty -> Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Rigid r
i Offset
n) Cmp
Lt  SizeExpr' r f
Infty -> CTrans r f
test forall a b. (a -> b) -> a -> b
$ forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
Lt forall rigid flex. SizeExpr' rigid flex
Infty
    Constraint a :: SizeExpr' r f
a@Flex{}    Cmp
Lt  SizeExpr' r f
Infty -> forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c { leftExpr :: SizeExpr' r f
leftExpr = SizeExpr' r f
a { offset :: Offset
offset = Offset
0 }}]

    -- rhs is Const
    Constraint (Const Offset
n)   Cmp
cmp (Const Offset
m) -> if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m then forall (m :: * -> *) a. Monad m => a -> m a
return [] else Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint SizeExpr' r f
Infty       Cmp
cmp  Const{}  -> Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Rigid r
i Offset
n) Cmp
cmp (Const Offset
m) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m then
        CTrans r f
test (forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
Le (forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset
m forall a. Num a => a -> a -> a
- Offset
n forall a. Num a => a -> a -> a
- forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1)))
       else Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Flex f
x Offset
n)  Cmp
cmp (Const Offset
m) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m
       then forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0) Cmp
Le (forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset
m forall a. Num a => a -> a -> a
- Offset
n forall a. Num a => a -> a -> a
- forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1))]
       else Either (TCMT IO Doc) [Constraint' r f]
err

    -- rhs is Rigid
    Constraint SizeExpr' r f
Infty Cmp
cmp Rigid{} -> Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Const Offset
m) Cmp
cmp (Rigid r
i Offset
n) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then forall (m :: * -> *) a. Monad m => a -> m a
return []
      else CTrans r f
test (forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. Offset -> SizeExpr' rigid flex
Const forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0))
    Constraint (Rigid r
j Offset
m) Cmp
cmp (Rigid r
i Offset
n) | r
i forall a. Eq a => a -> a -> Bool
== r
j ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then forall (m :: * -> *) a. Monad m => a -> m a
return [] else Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Rigid r
j Offset
m) Cmp
cmp (Rigid r
i Offset
n) -> CTrans r f
test Constraint' r f
c
    Constraint (Flex f
x Offset
m)  Cmp
cmp (Rigid r
i Offset
n) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
       then forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0) Cmp
Le (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset
n forall a. Num a => a -> a -> a
- Offset
m forall a. Num a => a -> a -> a
- forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1))]
       else forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n forall a. Num a => a -> a -> a
+ forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1) Cmp
Le (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0)]

    -- rhs is Flex
    Constraint SizeExpr' r f
Infty Cmp
Le (Flex f
x Offset
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint forall rigid flex. SizeExpr' rigid flex
Infty Cmp
Le (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0)]
    Constraint SizeExpr' r f
Infty Cmp
Lt (Flex f
x Offset
n) -> Either (TCMT IO Doc) [Constraint' r f]
err
    Constraint (Const Offset
m) Cmp
cmp (Flex f
x Offset
n) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then forall (m :: * -> *) a. Monad m => a -> m a
return []
      else forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. Offset -> SizeExpr' rigid flex
Const forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n forall a. Num a => a -> a -> a
+ forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1) Cmp
Le (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0)]
    Constraint (Rigid r
i Offset
m) Cmp
cmp (Flex f
x Offset
n) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
      then forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
cmp (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x forall a b. (a -> b) -> a -> b
$ Offset
n forall a. Num a => a -> a -> a
- Offset
m)]
      else forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0)]
    Constraint (Flex f
y Offset
m) Cmp
cmp (Flex f
x Offset
n) ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
      then forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
y Offset
0) Cmp
cmp (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x forall a b. (a -> b) -> a -> b
$ Offset
n forall a. Num a => a -> a -> a
- Offset
m)]
      else forall (m :: * -> *) a. Monad m => a -> m a
return [forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
y forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0)]

-- | 'Le' acts as 'True', 'Lt' as 'False'.
ifLe :: Cmp -> a -> a -> a
ifLe :: forall a. Cmp -> a -> a -> a
ifLe Cmp
Le a
a a
b = a
a
ifLe Cmp
Lt a
a a
b = a
b

-- | Interpret 'Cmp' as relation on 'Offset'.
compareOffset :: Offset -> Cmp -> Offset -> Bool
compareOffset :: Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
Le Offset
m = Offset
n forall a. Ord a => a -> a -> Bool
<= Offset
m
compareOffset Offset
n Cmp
Lt Offset
m = Offset
n forall a. Ord a => a -> a -> Bool
<  Offset
m

-- * Printing

instance (Pretty r, Pretty f) => Pretty (SizeExpr' r f) where
  pretty :: SizeExpr' r f -> Doc
pretty (Const Offset
n)   = forall a. Pretty a => a -> Doc
pretty Offset
n
  pretty (SizeExpr' r f
Infty)     = Doc
"∞"
  pretty (Rigid r
i Offset
0) = forall a. Pretty a => a -> Doc
pretty r
i
  pretty (Rigid r
i Offset
n) = forall a. Pretty a => a -> Doc
pretty r
i forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (String
"+" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Offset
n)
  pretty (Flex  f
x Offset
0) = forall a. Pretty a => a -> Doc
pretty f
x
  pretty (Flex  f
x Offset
n) = forall a. Pretty a => a -> Doc
pretty f
x forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (String
"+" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Offset
n)

instance Pretty Polarity where
  pretty :: Polarity -> Doc
pretty Polarity
Least    = Doc
"-"
  pretty Polarity
Greatest = Doc
"+"

instance Pretty flex => Pretty (PolarityAssignment flex) where
  pretty :: PolarityAssignment flex -> Doc
pretty (PolarityAssignment Polarity
pol flex
flex) = forall a. Pretty a => a -> Doc
pretty Polarity
pol forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty flex
flex

instance Pretty Cmp where
  pretty :: Cmp -> Doc
pretty Cmp
Le = Doc
"≤"
  pretty Cmp
Lt = Doc
"<"

instance (Pretty r, Pretty f) => Pretty (Constraint' r f) where
  pretty :: Constraint' r f -> Doc
pretty (Constraint SizeExpr' r f
a Cmp
cmp SizeExpr' r f
b) = forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
a Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Cmp
cmp Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
b

-- * Wellformedness

-- | Offsets @+ n@ must be non-negative
class ValidOffset a where
  validOffset :: a -> Bool

instance ValidOffset Offset where
  validOffset :: Offset -> Bool
validOffset = (forall a. Ord a => a -> a -> Bool
>= Offset
0)

instance ValidOffset (SizeExpr' r f) where
  validOffset :: SizeExpr' r f -> Bool
validOffset SizeExpr' r f
e =
    case SizeExpr' r f
e of
      SizeExpr' r f
Infty -> Bool
True
      SizeExpr' r f
_     -> forall a. ValidOffset a => a -> Bool
validOffset (forall rigid flex. SizeExpr' rigid flex -> Offset
offset SizeExpr' r f
e)

-- | Make offsets non-negative by rounding up.
class TruncateOffset a where
  truncateOffset :: a -> a

instance TruncateOffset Offset where
  truncateOffset :: Offset -> Offset
truncateOffset Offset
n | Offset
n forall a. Ord a => a -> a -> Bool
>= Offset
0    = Offset
n
                   | Bool
otherwise = Offset
0

instance TruncateOffset (SizeExpr' r f) where
  truncateOffset :: SizeExpr' r f -> SizeExpr' r f
truncateOffset SizeExpr' r f
e =
    case SizeExpr' r f
e of
      SizeExpr' r f
Infty     -> SizeExpr' r f
e
      Const Offset
n   -> forall rigid flex. Offset -> SizeExpr' rigid flex
Const   forall a b. (a -> b) -> a -> b
$ forall a. TruncateOffset a => a -> a
truncateOffset Offset
n
      Rigid r
i Offset
n -> forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i forall a b. (a -> b) -> a -> b
$ forall a. TruncateOffset a => a -> a
truncateOffset Offset
n
      Flex  f
x Offset
n -> forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex  f
x forall a b. (a -> b) -> a -> b
$ forall a. TruncateOffset a => a -> a
truncateOffset Offset
n

-- * Computing variable sets

-- | The rigid variables contained in a pice of syntax.
class Ord (RigidOf a) => Rigids a where
  type RigidOf a
  rigids :: a -> Set (RigidOf a)

instance Rigids a => Rigids [a] where
  type RigidOf [a] = RigidOf a
  rigids :: [a] -> Set (RigidOf [a])
rigids [a]
as = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map forall a. Rigids a => a -> Set (RigidOf a)
rigids [a]
as)

instance Ord r => Rigids (SizeExpr' r f) where
  type RigidOf (SizeExpr' r f) = r
  rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
rigids (Rigid r
x Offset
_) = forall a. a -> Set a
Set.singleton r
x

  rigids SizeExpr' r f
_           = forall a. Set a
Set.empty

instance Ord r => Rigids (Constraint' r f) where
  type RigidOf (Constraint' r f) = r
  rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f))
rigids (Constraint SizeExpr' r f
l Cmp
_ SizeExpr' r f
r) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' r f
l) (forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' r f
r)

-- | The flexibe variables contained in a pice of syntax.
class Ord (FlexOf a) => Flexs a where
  type FlexOf a
  flexs :: a -> Set (FlexOf a)

instance Flexs a => Flexs [a] where
  type FlexOf [a] = FlexOf a
  flexs :: [a] -> Set (FlexOf [a])
flexs [a]
as = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map forall a. Flexs a => a -> Set (FlexOf a)
flexs [a]
as)

instance Ord flex => Flexs (SizeExpr' rigid flex) where
  type FlexOf (SizeExpr' rigid flex) = flex
  flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
flexs (Flex flex
x Offset
_) = forall a. a -> Set a
Set.singleton flex
x
  flexs SizeExpr' rigid flex
_          = forall a. Set a
Set.empty

instance Ord flex => Flexs (Constraint' rigid flex) where
  type FlexOf (Constraint' rigid flex) = flex
  flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex))
flexs (Constraint SizeExpr' rigid flex
l Cmp
_ SizeExpr' rigid flex
r) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeExpr' rigid flex
l) (forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeExpr' rigid flex
r)