Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.SizedTypes.Syntax

Contents

Syntax
Polarities to specify solutions.
Solutions.
Constraint simplification
Printing
Wellformedness
Computing variable sets

Description

Syntax of size expressions and constraints.

Synopsis

Syntax

newtype Offset Source

Constant finite sizes n >= 0.

Constructors

O Int

Instances

Enum Offset Source
Eq Offset Source
Num Offset Source
Ord Offset Source
Show Offset Source
Arbitrary Offset Source
MeetSemiLattice Offset Source
TruncateOffset Offset Source
ValidOffset Offset Source
Negative Offset Source
Plus Offset Offset Offset Source
Plus Offset Weight Weight Source
Plus Weight Offset Weight Source
Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source	Add offset to size expression.

newtype Rigid Source

Fixed size variables i.

Constructors

RigidId
Fields rigidId :: String

Instances

Eq Rigid Source
Ord Rigid Source
Show Rigid Source

newtype Flex Source

Size meta variables X to solve for.

Constructors

FlexId
Fields flexId :: String

Instances

Eq Flex Source
Ord Flex Source
Show Flex Source

data SizeExpr' rigid flex Source

Size expressions appearing in constraints.

Constructors

Const	Constant number `n`.
Fields offset :: Offset
Rigid	Variable plus offset `i + n`.
Fields rigid :: rigid offset :: Offset
Infty	Infinity `∞`.
Flex	Meta variable `X + n`.
Fields flex :: flex offset :: Offset

Instances

Ord f => Substitute r f (SizeExpr' r f) Source
Flexs flex (SizeExpr' rigid flex) Source
Rigids r (SizeExpr' r f) Source
Subst Term (SizeExpr' NamedRigid SizeMeta) Source	Only for `raise`.
Functor (SizeExpr' rigid) Source
Foldable (SizeExpr' rigid) Source
Traversable (SizeExpr' rigid) Source
(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex) Source
(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex) Source
(Show r, Show f) => Show (SizeExpr' r f) Source
TruncateOffset (SizeExpr' r f) Source
ValidOffset (SizeExpr' r f) Source
Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source	Add offset to size expression.
Plus (SizeExpr' r f) Label (SizeExpr' r f) Source
Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source

type SizeExpr = SizeExpr' Rigid Flex Source

data Cmp Source

Comparison operator, e.g. for size expression.

Constructors

Lt	`<`.
Le	`≤`.

Instances

Bounded Cmp Source
Enum Cmp Source
Eq Cmp Source
Ord Cmp Source	Comparison operator is ordered `Lt < Le`.
Show Cmp Source
Arbitrary Cmp Source
Dioid Cmp Source
MeetSemiLattice Cmp Source
Top Cmp Source
AsWeightRelation Cmp Source

data Constraint' rigid flex Source

Constraint: an inequation between size expressions, e.g. X < ∞ or i + 3 ≤ j.

Constructors

Constraint
Fields leftExpr :: SizeExpr' rigid flex cmp :: Cmp rightExpr :: SizeExpr' rigid flex

Instances

PrettyTCM SizeConstraint Source	Assumes we are in the right context.
Subst Term SizeConstraint Source
Ord f => Substitute r f (Constraint' r f) Source
Ord flex => Flexs flex (Constraint' rigid flex) Source
Ord r => Rigids r (Constraint' r f) Source
Functor (Constraint' rigid) Source
Foldable (Constraint' rigid) Source
Traversable (Constraint' rigid) Source
(Show r, Show f) => Show (Constraint' r f) Source

type Constraint = Constraint' Rigid Flex Source

Polarities to specify solutions.

data Polarity Source

What type of solution are we looking for?

Constructors

Least
Greatest

Instances

Eq Polarity Source
Ord Polarity Source
Show Polarity Source

data PolarityAssignment flex Source

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex

Instances

Show flex => Show (PolarityAssignment flex) Source

type Polarities flex = Map flex Polarity Source

Type of solution wanted for each flexible.

emptyPolarities :: Polarities flex Source

polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex Source

getPolarity :: Ord flex => Polarities flex -> flex -> Polarity Source

Default polarity is Least.

Solutions.

type Solution rigid flex = Map flex (SizeExpr' rigid flex) Source

Partial substitution from flexible variables to size expression.

class Substitute r f a where Source

Executing a substitution.

Methods

subst :: Solution r f -> a -> a Source

Instances

Substitute r f a => Substitute r f [a] Source
Ord f => Substitute r f (Constraint' r f) Source
Ord f => Substitute r f (SizeExpr' r f) Source

Constraint simplification

type CTrans r f = Constraint' r f -> Either String [Constraint' r f] Source

simplify1 :: (Show f, Show r, Eq r) => CTrans r f -> CTrans r f Source

Returns Nothing if we have a contradictory constraint.

ifLe :: Cmp -> a -> a -> a Source

Le acts as True, Lt as False.

compareOffset :: Offset -> Cmp -> Offset -> Bool Source

Interpret Cmp as relation on Offset.

Printing

Wellformedness

class ValidOffset a where Source

Offsets + n must be non-negative

Methods

validOffset :: a -> Bool Source

Instances

ValidOffset Offset Source
ValidOffset (SizeExpr' r f) Source

class TruncateOffset a where Source

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a Source

Instances

TruncateOffset Offset Source
TruncateOffset (SizeExpr' r f) Source

Computing variable sets

class Rigids r a where Source

The rigid variables contained in a pice of syntax.

Methods

rigids :: a -> Set r Source

Instances

(Ord r, Rigids r a) => Rigids r [a] Source
Ord r => Rigids r (Constraint' r f) Source
Rigids r (SizeExpr' r f) Source

class Flexs flex a | a -> flex where Source

The flexibe variables contained in a pice of syntax.

Methods

flexs :: a -> Set flex Source

Instances

Flexs SizeMeta HypSizeConstraint Source
(Ord flex, Flexs flex a) => Flexs flex [a] Source
Ord flex => Flexs flex (Constraint' rigid flex) Source
Flexs flex (SizeExpr' rigid flex) Source