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

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

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

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

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

-- | Default polarity is 'Least'.
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

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

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

-- | Add offset to size expression.
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

-- * 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 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
    -- rhs is Infty
    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 }}]

    -- rhs is Const
    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

    -- rhs is Rigid
    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)]

    -- rhs is Flex
    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)]

-- | 'Le' acts as 'True', 'Lt' as 'False'.
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

-- | Interpret 'Cmp' as relation on 'Offset'.
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

-- * Printing

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

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

-- | Make offsets non-negative by rounding up.
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

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

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