{-# OPTIONS_GHC -Wunused-imports #-}

-- | Syntax of size expressions and constraints.

module Agda.TypeChecking.SizedTypes.Syntax where

import Prelude hiding ( null )

import GHC.Generics (Generic)
import Control.DeepSeq

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

import Agda.Syntax.Common

import Agda.TypeChecking.Monad.Base.Types
import Agda.TypeChecking.SizedTypes.Utils

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty as P

import Agda.Utils.Impossible

-- * Syntax

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

instance NFData Offset

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

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

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

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

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

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

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

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

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

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

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

type SizeExpr = SizeExpr' Rigid Flex

instance (NFData r, NFData f) => NFData (SizeExpr' r f)

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

instance NFData Cmp

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

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

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

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

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

type Constraint = Constraint' Rigid Flex

instance (NFData r, NFData f) => NFData (Constraint' r f)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- * Constraint simplification

type CTrans r f = Constraint' r f -> Maybe [Constraint' r f]

-- | Returns 'Nothing' if the constraint is contradictory.
simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 :: forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 CTrans r f
test Constraint' r f
c = do
  let err :: Maybe a
err = Maybe a
forall a. Maybe a
Nothing
  case Constraint' r f
c of
    -- rhs is Infty
    Constraint SizeExpr' r f
a           Cmp
Le  SizeExpr' r f
Infty -> [Constraint' r f] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint Const{}     Cmp
Lt  SizeExpr' r f
Infty -> [Constraint' r f] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Constraint SizeExpr' r f
Infty       Cmp
Lt  SizeExpr' r f
Infty -> Maybe [Constraint' r f]
forall a. Maybe a
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] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c { leftExpr = a { offset = 0 }}]

    -- rhs is Const
    Constraint (Const Offset
n)   Cmp
cmp (Const Offset
m) -> if Offset -> Cmp -> Offset -> Bool
compareOffset Offset
n Cmp
cmp Offset
m then [Constraint' r f] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else Maybe [Constraint' r f]
forall a. Maybe a
err
    Constraint SizeExpr' r f
Infty       Cmp
cmp  Const{}  -> Maybe [Constraint' r f]
forall a. Maybe a
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 Maybe [Constraint' r f]
forall a. Maybe a
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] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (f -> Offset -> SizeExpr' r f
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex f
x Offset
0) Cmp
Le (Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Cmp -> Offset -> Offset -> Offset
forall a. Cmp -> a -> a -> a
ifLe Cmp
cmp Offset
0 Offset
1))]
       else Maybe [Constraint' r f]
forall a. Maybe a
err

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

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

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

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

-- * Printing

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

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

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

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

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

-- * Wellformedness

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

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

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

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

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

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

-- * Computing variable sets

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

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

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

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

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

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

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

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

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

-- | Identifiers for rigid variables.
data NamedRigid = NamedRigid
  { NamedRigid -> String
rigidName  :: String   -- ^ Name for printing in debug messages.
  , NamedRigid -> Int
rigidIndex :: Int      -- ^ De Bruijn index.
  } deriving (Int -> NamedRigid -> ShowS
[NamedRigid] -> ShowS
NamedRigid -> String
(Int -> NamedRigid -> ShowS)
-> (NamedRigid -> String)
-> ([NamedRigid] -> ShowS)
-> Show NamedRigid
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NamedRigid -> ShowS
showsPrec :: Int -> NamedRigid -> ShowS
$cshow :: NamedRigid -> String
show :: NamedRigid -> String
$cshowList :: [NamedRigid] -> ShowS
showList :: [NamedRigid] -> ShowS
Show, (forall x. NamedRigid -> Rep NamedRigid x)
-> (forall x. Rep NamedRigid x -> NamedRigid) -> Generic NamedRigid
forall x. Rep NamedRigid x -> NamedRigid
forall x. NamedRigid -> Rep NamedRigid x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NamedRigid -> Rep NamedRigid x
from :: forall x. NamedRigid -> Rep NamedRigid x
$cto :: forall x. Rep NamedRigid x -> NamedRigid
to :: forall x. Rep NamedRigid x -> NamedRigid
Generic)

instance NFData NamedRigid

instance Eq NamedRigid where
  == :: NamedRigid -> NamedRigid -> Bool
(==) = Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool)
-> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` NamedRigid -> Int
rigidIndex

instance Ord NamedRigid where
  compare :: NamedRigid -> NamedRigid -> Ordering
compare = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` NamedRigid -> Int
rigidIndex

instance Pretty NamedRigid where
  pretty :: NamedRigid -> Doc
pretty = String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> (NamedRigid -> String) -> NamedRigid -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedRigid -> String
rigidName

instance Plus NamedRigid Int NamedRigid where
  plus :: NamedRigid -> Int -> NamedRigid
plus (NamedRigid String
x Int
i) Int
j = String -> Int -> NamedRigid
NamedRigid String
x (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)

-- | Size metas in size expressions.
data SizeMeta = SizeMeta
  { SizeMeta -> MetaId
sizeMetaId   :: MetaId
  -- TODO to fix issue 300?
  -- , sizeMetaPerm :: Permutation -- ^ Permutation from the current context
  --                               --   to the context of the meta.
  , SizeMeta -> [Int]
sizeMetaArgs :: [Int]       -- ^ De Bruijn indices.
  } deriving (Int -> SizeMeta -> ShowS
[SizeMeta] -> ShowS
SizeMeta -> String
(Int -> SizeMeta -> ShowS)
-> (SizeMeta -> String) -> ([SizeMeta] -> ShowS) -> Show SizeMeta
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SizeMeta -> ShowS
showsPrec :: Int -> SizeMeta -> ShowS
$cshow :: SizeMeta -> String
show :: SizeMeta -> String
$cshowList :: [SizeMeta] -> ShowS
showList :: [SizeMeta] -> ShowS
Show, (forall x. SizeMeta -> Rep SizeMeta x)
-> (forall x. Rep SizeMeta x -> SizeMeta) -> Generic SizeMeta
forall x. Rep SizeMeta x -> SizeMeta
forall x. SizeMeta -> Rep SizeMeta x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SizeMeta -> Rep SizeMeta x
from :: forall x. SizeMeta -> Rep SizeMeta x
$cto :: forall x. Rep SizeMeta x -> SizeMeta
to :: forall x. Rep SizeMeta x -> SizeMeta
Generic)

instance NFData SizeMeta

-- | An equality which ignores the meta arguments.
instance Eq  SizeMeta where
  == :: SizeMeta -> SizeMeta -> Bool
(==) = MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
(==) (MetaId -> MetaId -> Bool)
-> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SizeMeta -> MetaId
sizeMetaId

-- | An order which ignores the meta arguments.
instance Ord SizeMeta where
  compare :: SizeMeta -> SizeMeta -> Ordering
compare = MetaId -> MetaId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MetaId -> MetaId -> Ordering)
-> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SizeMeta -> MetaId
sizeMetaId

instance Pretty SizeMeta where
  pretty :: SizeMeta -> Doc
pretty = MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> (SizeMeta -> MetaId) -> SizeMeta -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId

-- | Size expression with de Bruijn indices.
type DBSizeExpr = SizeExpr' NamedRigid SizeMeta

type SizeConstraint = Constraint' NamedRigid SizeMeta

-- | Size constraint with de Bruijn indices.
data HypSizeConstraint = HypSizeConstraint
  { HypSizeConstraint -> Context
sizeContext    :: Context
  , HypSizeConstraint -> [Int]
sizeHypIds     :: [Nat] -- ^ DeBruijn indices
  , HypSizeConstraint -> [SizeConstraint]
sizeHypotheses :: [SizeConstraint]  -- ^ Living in @Context@.
  , HypSizeConstraint -> SizeConstraint
sizeConstraint :: SizeConstraint    -- ^ Living in @Context@.
  }
  deriving (Int -> HypSizeConstraint -> ShowS
[HypSizeConstraint] -> ShowS
HypSizeConstraint -> String
(Int -> HypSizeConstraint -> ShowS)
-> (HypSizeConstraint -> String)
-> ([HypSizeConstraint] -> ShowS)
-> Show HypSizeConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HypSizeConstraint -> ShowS
showsPrec :: Int -> HypSizeConstraint -> ShowS
$cshow :: HypSizeConstraint -> String
show :: HypSizeConstraint -> String
$cshowList :: [HypSizeConstraint] -> ShowS
showList :: [HypSizeConstraint] -> ShowS
Show, (forall x. HypSizeConstraint -> Rep HypSizeConstraint x)
-> (forall x. Rep HypSizeConstraint x -> HypSizeConstraint)
-> Generic HypSizeConstraint
forall x. Rep HypSizeConstraint x -> HypSizeConstraint
forall x. HypSizeConstraint -> Rep HypSizeConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HypSizeConstraint -> Rep HypSizeConstraint x
from :: forall x. HypSizeConstraint -> Rep HypSizeConstraint x
$cto :: forall x. Rep HypSizeConstraint x -> HypSizeConstraint
to :: forall x. Rep HypSizeConstraint x -> HypSizeConstraint
Generic)

instance Flexs HypSizeConstraint where
  type FlexOf HypSizeConstraint = SizeMeta
  flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
flexs (HypSizeConstraint Context
_ [Int]
_ [SizeConstraint]
hs SizeConstraint
c) = [SizeConstraint] -> Set (FlexOf [SizeConstraint])
forall a. Flexs a => a -> Set (FlexOf a)
flexs [SizeConstraint]
hs Set SizeMeta -> Set SizeMeta -> Set SizeMeta
forall a. Monoid a => a -> a -> a
`mappend` SizeConstraint -> Set (FlexOf SizeConstraint)
forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeConstraint
c

instance NFData HypSizeConstraint