DerivationTrees.CPTS

Documentation

class Unifyable a where

Methods

(===) :: a -> a -> Bool

Instances

Unifyable Term

Unifyable Binding

Unifyable V

class TeXable a where

Methods

texify :: a -> TeX

Instances

TeXable Term

TeXable Sort

data V

Constructors

V Name

Unbound

Instances

Eq V

Show V

Unifyable V

type Name = String

type Sort = String

type Colour = String

data Binding where

Constructors

:- :: V -> Term -> Binding

Base :: Name -> Binding

Mult :: Binding -> Binding

Instances

Eq Binding

Show Binding

Unifyable Binding

data Term where

Constructors

Lam :: Colour -> Binding -> Term -> Term

Pi :: Colour -> Binding -> Term -> Term

App :: Colour -> Term -> Term -> Term

Sub :: Term -> Binding -> Term

Var :: Name -> Term

Con :: Name -> Term

Sor :: Sort -> Term

Many :: Term -> Term

Instances

Eq Term

Show Term

TeXable Term

Unifyable Term

dS :: (Name, Term) -> Term -> Term

data Jug

Constructors

Jug

Fields

value :: Term

typ :: Term

env :: Env

Instances

Show Jug

data Drv where

Constructors

Ax :: Drv

St :: Sort -> Drv -> Drv

Wk :: Int -> Sort -> Drv -> Drv -> Drv

Ab :: Sort -> Drv -> Drv -> Drv

Ap :: Binding -> Drv -> Drv -> Drv

Pr :: Colour -> (Sort, Sort) -> Drv -> Drv -> Drv

Co :: Sort -> Term -> Drv -> Drv -> Drv

An :: (Derivation -> Derivation) -> Drv -> Drv

Ln :: Link -> Drv -> Drv

Instances

Show Drv

type Env = [Binding]

unbound :: Binding -> Bool

interpV :: V -> TeX

interpB :: Binding -> TeX

interpB' :: TeX -> Binding -> TeX

col :: Colour -> String -> [TeX] -> TeX

data Ctx

Constructors

ArrowLhs

TopLvl

ColonRhs

BinderRhs

ApplLhs

ApplRhs

SubsLhs

havePrn :: Ctx -> Term -> Bool

interpT :: Ctx -> Term -> TeX

(+:) :: Binding -> Env -> Env

interpE :: Env -> [TeX]

renam :: Term -> TeX

interpA :: Term -> Term -> (TeX, TeX)

interpJ :: Jug -> TeX

check :: Bool -> String -> a -> a

bToT :: Binding -> Term

rebind :: Term -> Term -> Binding

jug' :: Term -> Sort -> Env -> Jug

stp :: Drv -> Jug -> (TeX -> Rule (), [(Drv, Jug)])

interp :: Drv -> Jug -> Derivation

delay :: Alignment -> Int -> Drv -> Drv

halt :: String -> Drv

named :: String -> Drv -> Drv

abort :: Drv