{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE UndecidableInstances       #-}

-- | Syntax of size expressions and constraints.

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

-- * 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
/= :: 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)

-- This Show instance is ok because of the Enum 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
/= :: 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 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
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
/= :: 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 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
text (String -> Doc) -> (Flex -> String) -> Flex -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flex -> String
flexId

-- | Size expressions appearing in constraints.
data SizeExpr' rigid flex
  = Const { SizeExpr' rigid flex -> Offset
offset :: Offset }                   -- ^ Constant number @n@.
  | Rigid { SizeExpr' rigid flex -> rigid
rigid  :: rigid, offset :: Offset }  -- ^ Variable plus offset @i + n@.
  | Infty                                        -- ^ Infinity @∞@.
  | 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
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

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

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

-- * 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
/= :: 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)

-- | 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 :: 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 Polarity
p flex
x) -> (flex
x,Polarity
p))

-- | Default polarity is 'Least'.
getPolarity :: Ord flex => Polarities flex -> flex -> Polarity
getPolarity :: 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 { 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 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
<+> 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

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

-- * Constraint simplification

type CTrans r f = Constraint' r f -> Either String [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 :: CTrans r f -> CTrans r f
simplify1 CTrans r f
test 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
$ String
"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]
++ String
" 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 String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint Const{}     Cmp
Lt  SizeExpr' r f
Infty -> [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint SizeExpr' r f
Infty       Cmp
Lt  SizeExpr' r f
Infty -> Either String [Constraint' r f]
forall b. Either String b
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 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 = 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 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 SizeExpr' r f
Infty       Cmp
cmp  Const{}  -> Either String [Constraint' r f]
forall b. Either String b
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 String [Constraint' r f]
forall b. Either String b
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 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
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 String [Constraint' r f]
forall b. Either String b
err

    -- rhs is Rigid
    Constraint SizeExpr' r f
Infty Cmp
cmp Rigid{} -> Either String [Constraint' r f]
forall b. Either String b
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 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 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 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 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 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
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 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 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 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 Offset
0)]
    Constraint SizeExpr' r f
Infty Cmp
Lt (Flex f
x Offset
n) -> Either String [Constraint' r f]
forall b. Either String b
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 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 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 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
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 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 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
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 Offset
0)]

-- | 'Le' acts as 'True', 'Lt' as 'False'.
ifLe :: Cmp -> a -> a -> a
ifLe :: 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
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
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
<+> 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

-- * 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 Rigids r a where
  rigids :: a -> Set r

instance (Ord r, Rigids r a) => Rigids r [a] where
  rigids :: [a] -> Set r
rigids [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 r
x Offset
_) = r -> Set r
forall a. a -> Set a
Set.singleton r
x
  rigids SizeExpr' r f
_           = 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 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 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)

-- | The flexibe variables contained in a pice of syntax.
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 [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 flex
x Offset
_) = flex -> Set flex
forall a. a -> Set a
Set.singleton flex
x
  flexs SizeExpr' rigid flex
_          = 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 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 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)