{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.SizedTypes.Syntax where
import Prelude hiding ( null )
import Data.Foldable (Foldable)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (Traversable)
import Agda.TypeChecking.SizedTypes.Utils
import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty
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
/= :: Offset -> Offset -> Bool
$c/= :: Offset -> Offset -> Bool
== :: Offset -> Offset -> Bool
$c== :: 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
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
$cp1Ord :: Eq 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
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]
(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
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)
instance Show Offset where
show :: Offset -> String
show (O n :: Int
n) = Int -> String
forall a. Show a => a -> String
show Int
n
instance Pretty Offset where
pretty :: Offset -> Doc
pretty (O n :: 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 x :: Int
x) (O y :: Int
y) = Int -> Offset
O (Int -> Int -> Int
forall a b c. Plus a b c => a -> b -> c
plus Int
x Int
y)
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
/= :: Rigid -> Rigid -> Bool
$c/= :: Rigid -> Rigid -> Bool
== :: Rigid -> Rigid -> Bool
$c== :: 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
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
$cp1Ord :: Eq Rigid
Ord)
instance Show Rigid where
show :: Rigid -> String
show (RigidId s :: String
s) = "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
text (String -> Doc) -> (Rigid -> String) -> Rigid -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rigid -> String
rigidId
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
/= :: Flex -> Flex -> Bool
$c/= :: Flex -> Flex -> Bool
== :: Flex -> Flex -> Bool
$c== :: 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
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
$cp1Ord :: Eq Flex
Ord)
instance Show Flex where
show :: Flex -> String
show (FlexId s :: String
s) = "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
text (String -> Doc) -> (Flex -> String) -> Flex -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flex -> String
flexId
data SizeExpr' rigid flex
= Const { SizeExpr' rigid flex -> Offset
offset :: Offset }
| Rigid { SizeExpr' rigid flex -> rigid
rigid :: rigid, offset :: Offset }
| Infty
| Flex { SizeExpr' rigid flex -> flex
flex :: flex, offset :: Offset }
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
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
(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
/= :: 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, 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
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
$cp1Ord :: forall rigid flex.
(Ord rigid, Ord flex) =>
Eq (SizeExpr' rigid flex)
Ord, a -> SizeExpr' rigid b -> SizeExpr' rigid a
(a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
(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
<$ :: a -> SizeExpr' rigid b -> SizeExpr' rigid a
$c<$ :: forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
fmap :: (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
$cfmap :: forall rigid a b.
(a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
Functor, SizeExpr' rigid a -> Bool
(a -> m) -> SizeExpr' rigid a -> m
(a -> b -> b) -> b -> SizeExpr' rigid a -> b
(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
product :: SizeExpr' rigid a -> a
$cproduct :: forall rigid a. Num a => SizeExpr' rigid a -> a
sum :: SizeExpr' rigid a -> a
$csum :: forall rigid a. Num a => SizeExpr' rigid a -> a
minimum :: SizeExpr' rigid a -> a
$cminimum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
maximum :: SizeExpr' rigid a -> a
$cmaximum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
elem :: a -> SizeExpr' rigid a -> Bool
$celem :: forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
length :: SizeExpr' rigid a -> Int
$clength :: forall rigid a. SizeExpr' rigid a -> Int
null :: SizeExpr' rigid a -> Bool
$cnull :: forall rigid a. SizeExpr' rigid a -> Bool
toList :: SizeExpr' rigid a -> [a]
$ctoList :: forall rigid a. SizeExpr' rigid a -> [a]
foldl1 :: (a -> a -> a) -> SizeExpr' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldr1 :: (a -> a -> a) -> SizeExpr' rigid a -> a
$cfoldr1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
foldl' :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b
$cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
foldl :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b
$cfoldl :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
foldr' :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b
$cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
foldr :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b
$cfoldr :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
foldMap' :: (a -> m) -> SizeExpr' rigid a -> m
$cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
foldMap :: (a -> m) -> SizeExpr' rigid a -> m
$cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
fold :: SizeExpr' rigid m -> m
$cfold :: forall rigid m. Monoid m => SizeExpr' rigid m -> m
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)
(a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
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)
sequence :: SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
mapM :: (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 :: SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
traverse :: (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)
$cp2Traversable :: forall rigid. Foldable (SizeExpr' rigid)
$cp1Traversable :: forall rigid. Functor (SizeExpr' rigid)
Traversable)
type SizeExpr = SizeExpr' Rigid Flex
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
showList :: [Cmp] -> ShowS
$cshowList :: [Cmp] -> ShowS
show :: Cmp -> String
$cshow :: Cmp -> String
showsPrec :: Int -> Cmp -> ShowS
$cshowsPrec :: Int -> Cmp -> ShowS
Show, Cmp -> Cmp -> Bool
(Cmp -> Cmp -> Bool) -> (Cmp -> Cmp -> Bool) -> Eq Cmp
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
Cmp -> Cmp -> Bounded 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]
(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
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 = Cmp -> Cmp -> Cmp
forall a. Ord a => a -> a -> a
min
unitCompose :: Cmp
unitCompose = Cmp
Le
instance Ord Cmp where
Lt <= :: Cmp -> Cmp -> Bool
<= x :: Cmp
x = Bool
True
Le <= Lt = Bool
False
Le <= 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
data Constraint' rigid flex = Constraint
{ Constraint' rigid flex -> SizeExpr' rigid flex
leftExpr :: SizeExpr' rigid flex
, Constraint' rigid flex -> Cmp
cmp :: Cmp
, 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
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, a -> Constraint' rigid b -> Constraint' rigid a
(a -> b) -> Constraint' rigid a -> Constraint' rigid b
(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
<$ :: a -> Constraint' rigid b -> Constraint' rigid a
$c<$ :: forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b
$cfmap :: forall rigid a b.
(a -> b) -> Constraint' rigid a -> Constraint' rigid b
Functor, Constraint' rigid a -> Bool
(a -> m) -> Constraint' rigid a -> m
(a -> b -> b) -> b -> Constraint' rigid a -> b
(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 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 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
product :: Constraint' rigid a -> a
$cproduct :: forall rigid a. Num a => Constraint' rigid a -> a
sum :: Constraint' rigid a -> a
$csum :: forall rigid a. Num a => Constraint' rigid a -> a
minimum :: Constraint' rigid a -> a
$cminimum :: forall rigid a. Ord a => Constraint' rigid a -> a
maximum :: Constraint' rigid a -> a
$cmaximum :: forall rigid a. Ord a => Constraint' rigid a -> a
elem :: a -> Constraint' rigid a -> Bool
$celem :: forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
length :: Constraint' rigid a -> Int
$clength :: forall rigid a. Constraint' rigid a -> Int
null :: Constraint' rigid a -> Bool
$cnull :: forall rigid a. Constraint' rigid a -> Bool
toList :: Constraint' rigid a -> [a]
$ctoList :: forall rigid a. Constraint' rigid a -> [a]
foldl1 :: (a -> a -> a) -> Constraint' rigid a -> a
$cfoldl1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldr1 :: (a -> a -> a) -> Constraint' rigid a -> a
$cfoldr1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
foldl' :: (b -> a -> b) -> b -> Constraint' rigid a -> b
$cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
foldl :: (b -> a -> b) -> b -> Constraint' rigid a -> b
$cfoldl :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
foldr' :: (a -> b -> b) -> b -> Constraint' rigid a -> b
$cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
foldr :: (a -> b -> b) -> b -> Constraint' rigid a -> b
$cfoldr :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
foldMap' :: (a -> m) -> Constraint' rigid a -> m
$cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
foldMap :: (a -> m) -> Constraint' rigid a -> m
$cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
fold :: Constraint' rigid m -> m
$cfold :: forall rigid m. Monoid m => Constraint' rigid m -> m
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)
(a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
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)
sequence :: Constraint' rigid (m a) -> m (Constraint' rigid a)
$csequence :: forall rigid (m :: * -> *) a.
Monad m =>
Constraint' rigid (m a) -> m (Constraint' rigid a)
mapM :: (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 :: Constraint' rigid (f a) -> f (Constraint' rigid a)
$csequenceA :: forall rigid (f :: * -> *) a.
Applicative f =>
Constraint' rigid (f a) -> f (Constraint' rigid a)
traverse :: (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)
$cp2Traversable :: forall rigid. Foldable (Constraint' rigid)
$cp1Traversable :: forall rigid. Functor (Constraint' rigid)
Traversable)
type Constraint = Constraint' Rigid Flex
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
/= :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c== :: 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
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
$cp1Ord :: Eq Polarity
Ord)
data PolarityAssignment flex = PolarityAssignment Polarity flex
type Polarities flex = Map flex Polarity
emptyPolarities :: Polarities flex
emptyPolarities :: Polarities flex
emptyPolarities = Polarities flex
forall k a. Map k a
Map.empty
polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex
polaritiesFromAssignments :: [PolarityAssignment flex] -> Polarities flex
polaritiesFromAssignments = [(flex, Polarity)] -> Polarities flex
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(flex, Polarity)] -> Polarities flex)
-> ([PolarityAssignment flex] -> [(flex, Polarity)])
-> [PolarityAssignment flex]
-> Polarities flex
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 p :: Polarity
p x :: flex
x) -> (flex
x,Polarity
p))
getPolarity :: Ord flex => Polarities flex -> flex -> Polarity
getPolarity :: Polarities flex -> flex -> Polarity
getPolarity pols :: Polarities flex
pols x :: 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
newtype Solution rigid flex = Solution { 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
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
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
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 sol :: 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
$ \ (x :: f
x, e :: SizeExpr' r f
e) ->
f -> Doc
forall a. Pretty a => a -> Doc
pretty f
x Doc -> Doc -> Doc
<+> ":=" Doc -> Doc -> Doc
<+> SizeExpr' r f -> Doc
forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
e
emptySolution :: Solution r f
emptySolution :: Solution r f
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
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 sol :: Map f (SizeExpr' r f)
sol) e :: SizeExpr' r f
e =
case SizeExpr' r f
e of
Flex x :: f
x n :: 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
e
instance Ord f => Substitute r f (Constraint' r f) where
subst :: Solution r f -> Constraint' r f -> Constraint' r f
subst sol :: Solution r f
sol (Constraint e :: SizeExpr' r f
e cmp :: Cmp
cmp e' :: 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 (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 s :: 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
instance Plus (SizeExpr' r f) Offset (SizeExpr' r f) where
plus :: SizeExpr' r f -> Offset -> SizeExpr' r f
plus e :: SizeExpr' r f
e m :: Offset
m =
case SizeExpr' r f
e of
Const n :: 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 i :: r
i n :: 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 x :: f
x n :: 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
Infty -> SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
type CTrans r f = Constraint' r f -> Either String [Constraint' r f]
simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 :: CTrans r f -> CTrans r f
simplify1 test :: CTrans r f
test c :: Constraint' r f
c = do
let err :: Either String b
err = String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ "size constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Constraint' r f -> String
forall a. Pretty a => a -> String
prettyShow Constraint' r f
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is inconsistent"
case Constraint' r f
c of
Constraint a :: SizeExpr' r f
a Le Infty -> [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Constraint Const{} Lt Infty -> [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Constraint Infty Lt Infty -> Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Rigid i :: r
i n :: Offset
n) Lt 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 0) Cmp
Lt SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
Constraint a :: SizeExpr' r f
a@Flex{} Lt Infty -> [Constraint' r f] -> Either String [Constraint' r f]
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 = 0 }}]
Constraint (Const n :: Offset
n) cmp :: Cmp
cmp (Const m :: Offset
m) -> if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m then [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else Either String [Constraint' r f]
forall b. Either String b
err
Constraint Infty cmp :: Cmp
cmp Const{} -> Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Rigid i :: r
i n :: Offset
n) cmp :: Cmp
cmp (Const m :: 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 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 0 1)))
else Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Flex x :: f
x n :: Offset
n) cmp :: Cmp
cmp (Const m :: Offset
m) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m
then [Constraint' r f] -> Either String [Constraint' r f]
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 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 0 1))]
else Either String [Constraint' r f]
forall b. Either String b
err
Constraint Infty cmp :: Cmp
cmp Rigid{} -> Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Const m :: Offset
m) cmp :: Cmp
cmp (Rigid i :: r
i n :: Offset
n) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then [Constraint' r f] -> Either String [Constraint' r f]
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 0))
Constraint (Rigid j :: r
j m :: Offset
m) cmp :: Cmp
cmp (Rigid i :: r
i n :: 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 String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Rigid j :: r
j m :: Offset
m) cmp :: Cmp
cmp (Rigid i :: r
i n :: Offset
n) -> CTrans r f
test Constraint' r f
c
Constraint (Flex x :: f
x m :: Offset
m) cmp :: Cmp
cmp (Rigid i :: r
i n :: Offset
n) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
then [Constraint' r f] -> Either String [Constraint' r f]
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 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 0 1))]
else [Constraint' r f] -> Either String [Constraint' r f]
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 0 1) Cmp
Le (r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i 0)]
Constraint Infty Le (Flex x :: f
x n :: Offset
n) -> [Constraint' r f] -> Either String [Constraint' r f]
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 0)]
Constraint Infty Lt (Flex x :: f
x n :: Offset
n) -> Either String [Constraint' r f]
forall b. Either String b
err
Constraint (Const m :: Offset
m) cmp :: Cmp
cmp (Flex x :: f
x n :: Offset
n) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n then [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return []
else [Constraint' r f] -> Either String [Constraint' r f]
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 0 1) Cmp
Le (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x 0)]
Constraint (Rigid i :: r
i m :: Offset
m) cmp :: Cmp
cmp (Flex x :: f
x n :: Offset
n) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
then [Constraint' r f] -> Either String [Constraint' r f]
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 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 String [Constraint' r f]
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 0)]
Constraint (Flex y :: f
y m :: Offset
m) cmp :: Cmp
cmp (Flex x :: f
x n :: Offset
n) ->
if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
m Cmp
cmp Offset
n
then [Constraint' r f] -> Either String [Constraint' r f]
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 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 String [Constraint' r f]
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 0)]
ifLe :: Cmp -> a -> a -> a
ifLe :: Cmp -> a -> a -> a
ifLe Le a :: a
a b :: a
b = a
a
ifLe Lt a :: a
a b :: a
b = a
b
compareOffset :: Offset -> Cmp -> Offset -> Bool
compareOffset :: Offset -> Cmp -> Offset -> Bool
compareOffset n :: Offset
n Le m :: Offset
m = Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m
compareOffset n :: Offset
n Lt m :: Offset
m = Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
< Offset
m
instance (Pretty r, Pretty f) => Pretty (SizeExpr' r f) where
pretty :: SizeExpr' r f -> Doc
pretty (Const n :: Offset
n) = Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
n
pretty (SizeExpr' r f
Infty) = "∞"
pretty (Rigid i :: r
i 0) = r -> Doc
forall a. Pretty a => a -> Doc
pretty r
i
pretty (Rigid i :: r
i n :: 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
text ("+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Offset -> String
forall a. Show a => a -> String
show Offset
n)
pretty (Flex x :: f
x 0) = f -> Doc
forall a. Pretty a => a -> Doc
pretty f
x
pretty (Flex x :: f
x n :: 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
text ("+" 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 Least = "-"
pretty Greatest = "+"
instance Pretty flex => Pretty (PolarityAssignment flex) where
pretty :: PolarityAssignment flex -> Doc
pretty (PolarityAssignment pol :: Polarity
pol flex :: 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 Le = "≤"
pretty Lt = "<"
instance (Pretty r, Pretty f) => Pretty (Constraint' r f) where
pretty :: Constraint' r f -> Doc
pretty (Constraint a :: SizeExpr' r f
a cmp :: Cmp
cmp b :: SizeExpr' r f
b) = SizeExpr' r f -> Doc
forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
a Doc -> Doc -> Doc
<+> Cmp -> Doc
forall a. Pretty a => a -> Doc
pretty Cmp
cmp Doc -> Doc -> Doc
<+> SizeExpr' r f -> Doc
forall a. Pretty a => a -> Doc
pretty SizeExpr' r f
b
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
>= 0)
instance ValidOffset (SizeExpr' r f) where
validOffset :: SizeExpr' r f -> Bool
validOffset e :: SizeExpr' r f
e =
case SizeExpr' r f
e of
Infty -> Bool
True
_ -> 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)
class TruncateOffset a where
truncateOffset :: a -> a
instance TruncateOffset Offset where
truncateOffset :: Offset -> Offset
truncateOffset n :: Offset
n | Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 = Offset
n
| Bool
otherwise = 0
instance TruncateOffset (SizeExpr' r f) where
truncateOffset :: SizeExpr' r f -> SizeExpr' r f
truncateOffset e :: SizeExpr' r f
e =
case SizeExpr' r f
e of
Infty -> SizeExpr' r f
e
Const n :: 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 i :: r
i n :: 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 x :: f
x n :: 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
class Rigids r a where
rigids :: a -> Set r
instance (Ord r, Rigids r a) => Rigids r [a] where
rigids :: [a] -> Set r
rigids as :: [a]
as = [Set r] -> Set r
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set r) -> [a] -> [Set r]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set r
forall r a. Rigids r a => a -> Set r
rigids [a]
as)
instance Rigids r (SizeExpr' r f) where
rigids :: SizeExpr' r f -> Set r
rigids (Rigid x :: r
x _) = r -> Set r
forall a. a -> Set a
Set.singleton r
x
rigids _ = Set r
forall a. Set a
Set.empty
instance Ord r => Rigids r (Constraint' r f) where
rigids :: Constraint' r f -> Set r
rigids (Constraint l :: SizeExpr' r f
l _ r :: 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 r
forall r a. Rigids r a => a -> Set r
rigids SizeExpr' r f
l) (SizeExpr' r f -> Set r
forall r a. Rigids r a => a -> Set r
rigids SizeExpr' r f
r)
class Flexs flex a | a -> flex where
flexs :: a -> Set flex
instance (Ord flex, Flexs flex a) => Flexs flex [a] where
flexs :: [a] -> Set flex
flexs as :: [a]
as = [Set flex] -> Set flex
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set flex) -> [a] -> [Set flex]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set flex
forall flex a. Flexs flex a => a -> Set flex
flexs [a]
as)
instance Flexs flex (SizeExpr' rigid flex) where
flexs :: SizeExpr' rigid flex -> Set flex
flexs (Flex x :: flex
x _) = flex -> Set flex
forall a. a -> Set a
Set.singleton flex
x
flexs _ = Set flex
forall a. Set a
Set.empty
instance (Ord flex) => Flexs flex (Constraint' rigid flex) where
flexs :: Constraint' rigid flex -> Set flex
flexs (Constraint l :: SizeExpr' rigid flex
l _ r :: 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 flex
forall flex a. Flexs flex a => a -> Set flex
flexs SizeExpr' rigid flex
l) (SizeExpr' rigid flex -> Set flex
forall flex a. Flexs flex a => a -> Set flex
flexs SizeExpr' rigid flex
r)