{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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.Syntax.Common.Pretty

import Agda.Utils.Impossible

-- * Syntax

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

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

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

instance MeetSemiLattice Offset where
  meet :: Offset -> Offset -> Offset
meet = Offset -> Offset -> Offset
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 (Int -> Int -> Int
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
(Rigid -> Rigid -> Bool) -> (Rigid -> Rigid -> Bool) -> Eq Rigid
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rigid -> Rigid -> Bool
== :: Rigid -> Rigid -> Bool
$c/= :: Rigid -> Rigid -> Bool
/= :: Rigid -> Rigid -> Bool
Eq, Eq Rigid
Eq Rigid =>
(Rigid -> Rigid -> Ordering)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Rigid)
-> (Rigid -> Rigid -> Rigid)
-> Ord 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
$ccompare :: Rigid -> Rigid -> Ordering
compare :: Rigid -> Rigid -> Ordering
$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
>= :: Rigid -> Rigid -> Bool
$cmax :: Rigid -> Rigid -> Rigid
max :: Rigid -> Rigid -> Rigid
$cmin :: Rigid -> Rigid -> Rigid
min :: Rigid -> Rigid -> Rigid
Ord)

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

instance Pretty Rigid where
  pretty :: Rigid -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (Rigid -> String) -> Rigid -> Doc
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
(Flex -> Flex -> Bool) -> (Flex -> Flex -> Bool) -> Eq Flex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Flex -> Flex -> Bool
== :: Flex -> Flex -> Bool
$c/= :: Flex -> Flex -> Bool
/= :: Flex -> Flex -> Bool
Eq, Eq Flex
Eq Flex =>
(Flex -> Flex -> Ordering)
-> (Flex -> Flex -> Bool)
-> (Flex -> Flex -> Bool)
-> (Flex -> Flex -> Bool)
-> (Flex -> Flex -> Bool)
-> (Flex -> Flex -> Flex)
-> (Flex -> Flex -> Flex)
-> Ord 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
$ccompare :: Flex -> Flex -> Ordering
compare :: Flex -> Flex -> Ordering
$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
>= :: Flex -> Flex -> Bool
$cmax :: Flex -> Flex -> Flex
max :: Flex -> Flex -> Flex
$cmin :: Flex -> Flex -> Flex
min :: Flex -> Flex -> Flex
Ord)

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

instance Pretty Flex where
  pretty :: Flex -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (Flex -> String) -> Flex -> Doc
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 = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> (Flex -> Doc) -> Flex -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flex -> Doc
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
[SizeExpr' rigid flex] -> ShowS
SizeExpr' rigid flex -> String
(Int -> SizeExpr' rigid flex -> ShowS)
-> (SizeExpr' rigid flex -> String)
-> ([SizeExpr' rigid flex] -> ShowS)
-> Show (SizeExpr' rigid flex)
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
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> SizeExpr' rigid flex -> ShowS
showsPrec :: Int -> SizeExpr' rigid flex -> ShowS
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
SizeExpr' rigid flex -> String
show :: SizeExpr' rigid flex -> String
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[SizeExpr' rigid flex] -> ShowS
showList :: [SizeExpr' rigid flex] -> ShowS
Show, SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
(SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> Eq (SizeExpr' rigid flex)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
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
/= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
Eq, Eq (SizeExpr' rigid flex)
Eq (SizeExpr' rigid flex) =>
(SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering)
-> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
-> (SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex)
-> (SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex)
-> Ord (SizeExpr' rigid flex)
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
SizeExpr' rigid flex
-> SizeExpr' rigid flex -> SizeExpr' rigid 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
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
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
$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
>= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
$cmax :: 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
$cmin :: 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
Ord, (forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b)
-> (forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a)
-> Functor (SizeExpr' rigid)
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
$cfmap :: forall rigid a b.
(a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
fmap :: forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
$c<$ :: forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
<$ :: forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
Functor, (forall m. Monoid m => SizeExpr' rigid m -> m)
-> (forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m)
-> (forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m)
-> (forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b)
-> (forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b)
-> (forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b)
-> (forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b)
-> (forall a. (a -> a -> a) -> SizeExpr' rigid a -> a)
-> (forall a. (a -> a -> a) -> SizeExpr' rigid a -> a)
-> (forall a. SizeExpr' rigid a -> [a])
-> (forall a. SizeExpr' rigid a -> Bool)
-> (forall a. SizeExpr' rigid a -> Int)
-> (forall a. Eq a => a -> SizeExpr' rigid a -> Bool)
-> (forall a. Ord a => SizeExpr' rigid a -> a)
-> (forall a. Ord a => SizeExpr' rigid a -> a)
-> (forall a. Num a => SizeExpr' rigid a -> a)
-> (forall a. Num a => SizeExpr' rigid a -> a)
-> Foldable (SizeExpr' rigid)
forall a. Eq a => a -> SizeExpr' rigid a -> Bool
forall a. Num a => SizeExpr' rigid a -> a
forall a. Ord a => SizeExpr' rigid a -> a
forall m. Monoid m => SizeExpr' rigid m -> m
forall a. SizeExpr' rigid a -> Bool
forall a. SizeExpr' rigid a -> Int
forall a. SizeExpr' rigid a -> [a]
forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
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 b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
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
$cfold :: forall rigid m. Monoid m => SizeExpr' rigid m -> m
fold :: forall m. Monoid m => SizeExpr' rigid m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
$cfoldr1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldr1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldl1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
$ctoList :: forall rigid a. SizeExpr' rigid a -> [a]
toList :: forall a. SizeExpr' rigid a -> [a]
$cnull :: forall rigid a. SizeExpr' rigid a -> Bool
null :: forall a. SizeExpr' rigid a -> Bool
$clength :: forall rigid a. SizeExpr' rigid a -> Int
length :: forall a. SizeExpr' rigid a -> Int
$celem :: forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
elem :: forall a. Eq a => a -> SizeExpr' rigid a -> Bool
$cmaximum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
maximum :: forall a. Ord a => SizeExpr' rigid a -> a
$cminimum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
minimum :: forall a. Ord a => SizeExpr' rigid a -> a
$csum :: forall rigid a. Num a => SizeExpr' rigid a -> a
sum :: forall a. Num a => SizeExpr' rigid a -> a
$cproduct :: forall rigid a. Num a => SizeExpr' rigid a -> a
product :: forall a. Num a => SizeExpr' rigid a -> a
Foldable, Functor (SizeExpr' rigid)
Foldable (SizeExpr' rigid)
(Functor (SizeExpr' rigid), Foldable (SizeExpr' rigid)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a))
-> Traversable (SizeExpr' rigid)
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 (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
forall (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
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)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
$cmapM :: forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
sequence :: forall (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
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
(Int -> Cmp -> ShowS)
-> (Cmp -> String) -> ([Cmp] -> ShowS) -> Show Cmp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cmp -> ShowS
showsPrec :: Int -> Cmp -> ShowS
$cshow :: Cmp -> String
show :: Cmp -> String
$cshowList :: [Cmp] -> ShowS
showList :: [Cmp] -> ShowS
Show, Cmp -> Cmp -> Bool
(Cmp -> Cmp -> Bool) -> (Cmp -> Cmp -> Bool) -> Eq Cmp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Cmp -> Cmp -> Bool
== :: Cmp -> Cmp -> Bool
$c/= :: Cmp -> Cmp -> Bool
/= :: Cmp -> Cmp -> Bool
Eq, Cmp
Cmp -> Cmp -> Bounded Cmp
forall a. a -> a -> Bounded a
$cminBound :: Cmp
minBound :: Cmp
$cmaxBound :: Cmp
maxBound :: Cmp
Bounded, Int -> Cmp
Cmp -> Int
Cmp -> [Cmp]
Cmp -> Cmp
Cmp -> Cmp -> [Cmp]
Cmp -> Cmp -> Cmp -> [Cmp]
(Cmp -> Cmp)
-> (Cmp -> Cmp)
-> (Int -> Cmp)
-> (Cmp -> Int)
-> (Cmp -> [Cmp])
-> (Cmp -> Cmp -> [Cmp])
-> (Cmp -> Cmp -> [Cmp])
-> (Cmp -> Cmp -> Cmp -> [Cmp])
-> Enum 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
$csucc :: Cmp -> Cmp
succ :: Cmp -> Cmp
$cpred :: Cmp -> Cmp
pred :: Cmp -> Cmp
$ctoEnum :: Int -> Cmp
toEnum :: Int -> Cmp
$cfromEnum :: Cmp -> Int
fromEnum :: Cmp -> Int
$cenumFrom :: Cmp -> [Cmp]
enumFrom :: Cmp -> [Cmp]
$cenumFromThen :: Cmp -> Cmp -> [Cmp]
enumFromThen :: Cmp -> Cmp -> [Cmp]
$cenumFromTo :: Cmp -> Cmp -> [Cmp]
enumFromTo :: Cmp -> Cmp -> [Cmp]
$cenumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
Enum)

instance Dioid Cmp where
  compose :: Cmp -> Cmp -> Cmp
compose     = Cmp -> Cmp -> Cmp
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 = Cmp -> Cmp -> Cmp
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
[Constraint' rigid flex] -> ShowS
Constraint' rigid flex -> String
(Int -> Constraint' rigid flex -> ShowS)
-> (Constraint' rigid flex -> String)
-> ([Constraint' rigid flex] -> ShowS)
-> Show (Constraint' rigid flex)
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
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Constraint' rigid flex -> ShowS
showsPrec :: Int -> Constraint' rigid flex -> ShowS
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Constraint' rigid flex -> String
show :: Constraint' rigid flex -> String
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Constraint' rigid flex] -> ShowS
showList :: [Constraint' rigid flex] -> ShowS
Show, (forall a b.
 (a -> b) -> Constraint' rigid a -> Constraint' rigid b)
-> (forall a b. a -> Constraint' rigid b -> Constraint' rigid a)
-> Functor (Constraint' rigid)
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
$cfmap :: forall rigid a b.
(a -> b) -> Constraint' rigid a -> Constraint' rigid b
fmap :: forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
$c<$ :: forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
<$ :: forall a b. a -> Constraint' rigid b -> Constraint' rigid a
Functor, (forall m. Monoid m => Constraint' rigid m -> m)
-> (forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m)
-> (forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m)
-> (forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b)
-> (forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b)
-> (forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b)
-> (forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b)
-> (forall a. (a -> a -> a) -> Constraint' rigid a -> a)
-> (forall a. (a -> a -> a) -> Constraint' rigid a -> a)
-> (forall a. Constraint' rigid a -> [a])
-> (forall a. Constraint' rigid a -> Bool)
-> (forall a. Constraint' rigid a -> Int)
-> (forall a. Eq a => a -> Constraint' rigid a -> Bool)
-> (forall a. Ord a => Constraint' rigid a -> a)
-> (forall a. Ord a => Constraint' rigid a -> a)
-> (forall a. Num a => Constraint' rigid a -> a)
-> (forall a. Num a => Constraint' rigid a -> a)
-> Foldable (Constraint' rigid)
forall a. Eq a => a -> Constraint' rigid a -> Bool
forall a. Num a => Constraint' rigid a -> a
forall a. Ord a => Constraint' rigid a -> a
forall m. Monoid m => Constraint' rigid m -> m
forall a. Constraint' rigid a -> Bool
forall a. Constraint' rigid a -> Int
forall a. Constraint' rigid a -> [a]
forall a. (a -> a -> a) -> Constraint' rigid a -> a
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 rigid m. Monoid m => Constraint' rigid m -> m
forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
forall rigid a. Constraint' rigid a -> Bool
forall rigid a. Constraint' rigid a -> Int
forall rigid a. Constraint' rigid a -> [a]
forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
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
$cfold :: forall rigid m. Monoid m => Constraint' rigid m -> m
fold :: forall m. Monoid m => Constraint' rigid m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
$cfoldr1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldr1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldl1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
$ctoList :: forall rigid a. Constraint' rigid a -> [a]
toList :: forall a. Constraint' rigid a -> [a]
$cnull :: forall rigid a. Constraint' rigid a -> Bool
null :: forall a. Constraint' rigid a -> Bool
$clength :: forall rigid a. Constraint' rigid a -> Int
length :: forall a. Constraint' rigid a -> Int
$celem :: forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
elem :: forall a. Eq a => a -> Constraint' rigid a -> Bool
$cmaximum :: forall rigid a. Ord a => Constraint' rigid a -> a
maximum :: forall a. Ord a => Constraint' rigid a -> a
$cminimum :: forall rigid a. Ord a => Constraint' rigid a -> a
minimum :: forall a. Ord a => Constraint' rigid a -> a
$csum :: forall rigid a. Num a => Constraint' rigid a -> a
sum :: forall a. Num a => Constraint' rigid a -> a
$cproduct :: forall rigid a. Num a => Constraint' rigid a -> a
product :: forall a. Num a => Constraint' rigid a -> a
Foldable, Functor (Constraint' rigid)
Foldable (Constraint' rigid)
(Functor (Constraint' rigid), Foldable (Constraint' rigid)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a))
-> Traversable (Constraint' rigid)
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 (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
forall (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
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)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
$cmapM :: forall rigid (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
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
(Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool) -> Eq Polarity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
/= :: Polarity -> Polarity -> Bool
Eq, Eq Polarity
Eq Polarity =>
(Polarity -> Polarity -> Ordering)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Polarity)
-> (Polarity -> Polarity -> Polarity)
-> Ord 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
$ccompare :: Polarity -> Polarity -> Ordering
compare :: Polarity -> Polarity -> Ordering
$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
>= :: Polarity -> Polarity -> Bool
$cmax :: Polarity -> Polarity -> Polarity
max :: Polarity -> Polarity -> Polarity
$cmin :: Polarity -> Polarity -> Polarity
min :: Polarity -> Polarity -> Polarity
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 = Map flex Polarity
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 = (Polarity -> Polarity -> Polarity)
-> [(flex, Polarity)] -> Map flex Polarity
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Polarity -> Polarity -> Polarity
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(flex, Polarity)] -> Map flex Polarity)
-> ([PolarityAssignment flex] -> [(flex, Polarity)])
-> [PolarityAssignment flex]
-> Map flex Polarity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PolarityAssignment flex -> (flex, Polarity))
-> [PolarityAssignment flex] -> [(flex, Polarity)]
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 = Polarity -> flex -> Polarities flex -> Polarity
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
[Solution rigid flex] -> ShowS
Solution rigid flex -> String
(Int -> Solution rigid flex -> ShowS)
-> (Solution rigid flex -> String)
-> ([Solution rigid flex] -> ShowS)
-> Show (Solution rigid flex)
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
$cshowsPrec :: forall rigid flex.
(Show flex, Show rigid) =>
Int -> Solution rigid flex -> ShowS
showsPrec :: Int -> Solution rigid flex -> ShowS
$cshow :: forall rigid flex.
(Show flex, Show rigid) =>
Solution rigid flex -> String
show :: Solution rigid flex -> String
$cshowList :: forall rigid flex.
(Show flex, Show rigid) =>
[Solution rigid flex] -> ShowS
showList :: [Solution rigid flex] -> ShowS
Show, Solution rigid flex
Solution rigid flex -> Bool
Solution rigid flex
-> (Solution rigid flex -> Bool) -> Null (Solution rigid flex)
forall a. a -> (a -> Bool) -> Null a
forall rigid flex. Solution rigid flex
forall rigid flex. Solution rigid flex -> Bool
$cempty :: forall rigid flex. Solution rigid flex
empty :: Solution rigid flex
$cnull :: forall rigid flex. Solution rigid flex -> Bool
null :: Solution rigid flex -> Bool
Null)

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

emptySolution :: Solution r f
emptySolution :: forall rigid flex. Solution rigid flex
emptySolution = Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution Map f (SizeExpr' r f)
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 -> SizeExpr' r f
-> (SizeExpr' r f -> SizeExpr' r f)
-> Maybe (SizeExpr' r f)
-> SizeExpr' r f
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SizeExpr' r f
e (SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n) (Maybe (SizeExpr' r f) -> SizeExpr' r f)
-> Maybe (SizeExpr' r f) -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ f -> Map f (SizeExpr' r f) -> Maybe (SizeExpr' r f)
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') = SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (Solution r f -> SizeExpr' r f -> SizeExpr' r f
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol SizeExpr' r f
e) Cmp
cmp (Solution r f -> SizeExpr' r f -> SizeExpr' r f
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 = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> a) -> [a] -> [a])
-> (Solution r f -> a -> a) -> Solution r f -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution r f -> a -> a
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 = (a -> a) -> Map k a -> Map k a
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Map k a -> Map k a)
-> (Solution r f -> a -> a) -> Solution r f -> Map k a -> Map k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution r f -> a -> a
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 = Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution (Map f (SizeExpr' r f) -> Solution r f)
-> (Solution r f -> Map f (SizeExpr' r f))
-> Solution r f
-> Solution r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution r f -> Map f (SizeExpr' r f) -> Map f (SizeExpr' r f)
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
s (Map f (SizeExpr' r f) -> Map f (SizeExpr' r f))
-> (Solution r f -> Map f (SizeExpr' r f))
-> Solution r f
-> Map f (SizeExpr' r f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution r f -> Map f (SizeExpr' r f)
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 -> Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const   (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
m
      Rigid r
i Offset
n -> r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
m
      Flex f
x  Offset
n -> f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x  (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
m
      SizeExpr' r f
Infty     -> SizeExpr' r f
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 = TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f])
-> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> Constraint' r f -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' r f
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
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 -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint Const{}     Cmp
Lt  SizeExpr' r f
Infty -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
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 CTrans r f -> CTrans r f
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
Lt SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
    Constraint a :: SizeExpr' r f
a@Flex{}    Cmp
Lt  SizeExpr' r f
Infty -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c { leftExpr = a { 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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
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 (SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
Le (Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Cmp -> Offset -> Offset -> Offset
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0) Cmp
Le (Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Cmp -> Offset -> Offset -> Offset
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      else CTrans r f
test (SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (r -> Offset -> SizeExpr' r f
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 r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
j ->
      if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0) Cmp
Le (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Cmp -> Offset -> Offset -> Offset
forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1))]
       else [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Cmp -> Offset -> Offset -> Offset
forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1) Cmp
Le (r -> Offset -> SizeExpr' r f
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) -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty Cmp
Le (f -> Offset -> SizeExpr' r f
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      else [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Cmp -> Offset -> Offset -> Offset
forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1) Cmp
Le (f -> Offset -> SizeExpr' r f
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i Offset
0) Cmp
cmp (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
m)]
      else [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (f -> Offset -> SizeExpr' r f
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 [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
y Offset
0) Cmp
cmp (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
m)]
      else [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
y (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n) Cmp
cmp (f -> Offset -> SizeExpr' r f
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 Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m
compareOffset Offset
n Cmp
Lt Offset
m = Offset
n Offset -> Offset -> Bool
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)   = Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
n
  pretty (SizeExpr' r f
Infty)     = Doc
"∞"
  pretty (Rigid r
i Offset
0) = r -> Doc
forall a. Pretty a => a -> Doc
pretty r
i
  pretty (Rigid r
i Offset
n) = r -> Doc
forall a. Pretty a => a -> Doc
pretty r
i Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
forall a. String -> Doc a
text (String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Offset -> String
forall a. Show a => a -> String
show Offset
n)
  pretty (Flex  f
x Offset
0) = f -> Doc
forall a. Pretty a => a -> Doc
pretty f
x
  pretty (Flex  f
x Offset
n) = f -> Doc
forall a. Pretty a => a -> Doc
pretty f
x Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
forall a. String -> Doc a
text (String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Offset -> String
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) = Polarity -> Doc
forall a. Pretty a => a -> Doc
pretty Polarity
pol Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> flex -> Doc
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) = SizeExpr' r f -> Doc
forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Cmp -> Doc
forall a. Pretty a => a -> Doc
pretty Cmp
cmp Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> SizeExpr' r f -> 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 = (Offset -> Offset -> Bool
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
_     -> Offset -> Bool
forall a. ValidOffset a => a -> Bool
validOffset (SizeExpr' r f -> Offset
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 Offset -> Offset -> Bool
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   -> Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const   (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. TruncateOffset a => a -> a
truncateOffset Offset
n
      Rigid r
i Offset
n -> r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. TruncateOffset a => a -> a
truncateOffset Offset
n
      Flex  f
x Offset
n -> f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex  f
x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
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 = [Set (RigidOf a)] -> Set (RigidOf a)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set (RigidOf a)) -> [a] -> [Set (RigidOf a)]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set (RigidOf a)
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
_) = r -> Set r
forall a. a -> Set a
Set.singleton r
x

  rigids SizeExpr' r f
_           = Set r
Set (RigidOf (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) = Set r -> Set r -> Set r
forall a. Ord a => Set a -> Set a -> Set a
Set.union (SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' r f
l) (SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
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 = [Set (FlexOf a)] -> Set (FlexOf a)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set (FlexOf a)) -> [a] -> [Set (FlexOf a)]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set (FlexOf a)
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
_) = flex -> Set flex
forall a. a -> Set a
Set.singleton flex
x
  flexs SizeExpr' rigid flex
_          = Set flex
Set (FlexOf (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) = Set flex -> Set flex -> Set flex
forall a. Ord a => Set a -> Set a -> Set a
Set.union (SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeExpr' rigid flex
l) (SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeExpr' rigid flex
r)