Agda.TypeChecking.SizedTypes.Utils

Documentation

debug :: IORef Bool

setDebugging :: Bool -> IO ()

trace :: String -> a -> a

traceM :: Applicative f => String -> f ()

class Eq a => Top a where

Minimal complete definition

top

Methods

top :: a

isTop :: a -> Bool

Instances

Top Cmp

Methods

top :: Cmp

isTop :: Cmp -> Bool

Top Label

Methods

top :: Label

isTop :: Label -> Bool

Top Weight

Methods

top :: Weight

isTop :: Weight -> Bool

(Ord r, Ord f, Top a) => Top (Edge' r f a)

Methods

top :: Edge' r f a

isTop :: Edge' r f a -> Bool

class Plus a b c where

Minimal complete definition

plus

Methods

plus :: a -> b -> c

Instances

Plus Int Int Int

Methods

plus :: Int -> Int -> Int

Plus Offset Offset Offset

Methods

plus :: Offset -> Offset -> Offset

Plus Offset Weight Weight

Methods

plus :: Offset -> Weight -> Weight

Plus Weight Offset Weight

Methods

plus :: Weight -> Offset -> Weight

Plus NamedRigid Int NamedRigid

Methods

plus :: NamedRigid -> Int -> NamedRigid

Plus (SizeExpr' r f) Offset (SizeExpr' r f)

Add offset to size expression.

Methods

plus :: SizeExpr' r f -> Offset -> SizeExpr' r f

Plus (SizeExpr' r f) Label (SizeExpr' r f)

Methods

plus :: SizeExpr' r f -> Label -> SizeExpr' r f

Plus (SizeExpr' r f) Weight (SizeExpr' r f)

Methods

plus :: SizeExpr' r f -> Weight -> SizeExpr' r f

class MeetSemiLattice a where

Minimal complete definition

meet

Methods

meet :: a -> a -> a

Instances

MeetSemiLattice Cmp

Methods

meet :: Cmp -> Cmp -> Cmp

MeetSemiLattice Offset

Methods

meet :: Offset -> Offset -> Offset

MeetSemiLattice Label

Methods

meet :: Label -> Label -> Label

MeetSemiLattice Weight

Methods

meet :: Weight -> Weight -> Weight

(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a)

Methods

meet :: Edge' r f a -> Edge' r f a -> Edge' r f a

class (MeetSemiLattice a, Top a) => Dioid a where

Semiring with idempotent + == dioid

Minimal complete definition

compose, unitCompose

Methods

compose

Arguments

:: a

-> a

-> a

E.g. +

unitCompose

Arguments

:: a

neutral element of compose, e.g. zero

Instances

Dioid Cmp

Methods

compose :: Cmp -> Cmp -> Cmp

unitCompose :: Cmp

Dioid Label

Methods

compose :: Label -> Label -> Label

unitCompose :: Label

Dioid Weight

Methods

compose :: Weight -> Weight -> Weight

unitCompose :: Weight

(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a)

Methods

compose :: Edge' r f a -> Edge' r f a -> Edge' r f a

unitCompose :: Edge' r f a