F

Documentation

type TyName = Name Ty

type TmName = Name Tm

data Ty

Constructors

TyVar TyName

TyInt

Arr Ty Ty

All (Bind TyName Ty)

TyProd [Ty]

Instances

Show Ty

Methods

showsPrec :: Int -> Ty -> ShowS

show :: Ty -> String

showList :: [Ty] -> ShowS

Rep Ty

Methods

rep :: R Ty

Alpha Ty

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Ty -> Ty

fv' :: Collection f => AlphaCtx -> Ty -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Ty -> (Ty -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Ty -> m (Ty, Perm AnyName)

aeq' :: AlphaCtx -> Ty -> Ty -> Bool

acompare' :: AlphaCtx -> Ty -> Ty -> Ordering

close :: Alpha b => AlphaCtx -> b -> Ty -> Ty

open :: Alpha b => AlphaCtx -> b -> Ty -> Ty

isPat :: Ty -> Maybe [AnyName]

isTerm :: Ty -> Bool

isEmbed :: Ty -> Bool

nthpatrec :: Ty -> NthCont

findpatrec :: Ty -> AnyName -> FindResult

Display Ty

Methods

display :: Ty -> DM Doc

(Sat (ctx0 TyName), Sat (ctx0 Ty), Sat (ctx0 (Bind TyName Ty)), Sat (ctx0 [Ty])) => Rep1 ctx0 Ty

Methods

rep1 :: R1 ctx0 Ty

Subst Tm Ty

Methods

isvar :: Ty -> Maybe (SubstName Ty Tm)

isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Tm)

subst :: Name Tm -> Tm -> Ty -> Ty

substs :: [(Name Tm, Tm)] -> Ty -> Ty

substPat :: AlphaCtx -> Tm -> Ty -> Ty

substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Ty -> Ty

Subst Ty Prim

Methods

isvar :: Prim -> Maybe (SubstName Prim Ty)

isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Ty)

subst :: Name Ty -> Ty -> Prim -> Prim

substs :: [(Name Ty, Ty)] -> Prim -> Prim

substPat :: AlphaCtx -> Ty -> Prim -> Prim

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Prim -> Prim

Subst Ty Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Ty)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty)

subst :: Name Ty -> Ty -> Tm -> Tm

substs :: [(Name Ty, Ty)] -> Tm -> Tm

substPat :: AlphaCtx -> Ty -> Tm -> Tm

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm

Subst Ty Ty

Methods

isvar :: Ty -> Maybe (SubstName Ty Ty)

isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Ty)

subst :: Name Ty -> Ty -> Ty -> Ty

substs :: [(Name Ty, Ty)] -> Ty -> Ty

substPat :: AlphaCtx -> Ty -> Ty -> Ty

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ty -> Ty

data Tm

Constructors

TmInt Int

TmVar TmName

Fix (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)

App Tm Tm

TmProd [Tm]

TmPrj Tm Int

TmPrim Tm Prim Tm

TmIf0 Tm Tm Tm

TLam (Bind TyName Tm)

TApp Tm Ty

Ann Tm Ty

Instances

Show Tm

Methods

showsPrec :: Int -> Tm -> ShowS

show :: Tm -> String

showList :: [Tm] -> ShowS

Rep Tm

Methods

rep :: R Tm

Alpha Tm

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Tm -> Tm

fv' :: Collection f => AlphaCtx -> Tm -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Tm -> (Tm -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Tm -> m (Tm, Perm AnyName)

aeq' :: AlphaCtx -> Tm -> Tm -> Bool

acompare' :: AlphaCtx -> Tm -> Tm -> Ordering

close :: Alpha b => AlphaCtx -> b -> Tm -> Tm

open :: Alpha b => AlphaCtx -> b -> Tm -> Tm

isPat :: Tm -> Maybe [AnyName]

isTerm :: Tm -> Bool

isEmbed :: Tm -> Bool

nthpatrec :: Tm -> NthCont

findpatrec :: Tm -> AnyName -> FindResult

Display Tm

Methods

display :: Tm -> DM Doc

(Sat (ctx0 Int), Sat (ctx0 TmName), Sat (ctx0 (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)), Sat (ctx0 Tm), Sat (ctx0 [Tm]), Sat (ctx0 Prim), Sat (ctx0 (Bind TyName Tm)), Sat (ctx0 Ty)) => Rep1 ctx0 Tm

Methods

rep1 :: R1 ctx0 Tm

Subst Tm Prim

Methods

isvar :: Prim -> Maybe (SubstName Prim Tm)

isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Tm)

subst :: Name Tm -> Tm -> Prim -> Prim

substs :: [(Name Tm, Tm)] -> Prim -> Prim

substPat :: AlphaCtx -> Tm -> Prim -> Prim

substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Prim -> Prim

Subst Tm Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Tm)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Tm)

subst :: Name Tm -> Tm -> Tm -> Tm

substs :: [(Name Tm, Tm)] -> Tm -> Tm

substPat :: AlphaCtx -> Tm -> Tm -> Tm

substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Tm -> Tm

Subst Tm Ty

Methods

isvar :: Ty -> Maybe (SubstName Ty Tm)

isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Tm)

subst :: Name Tm -> Tm -> Ty -> Ty

substs :: [(Name Tm, Tm)] -> Ty -> Ty

substPat :: AlphaCtx -> Tm -> Ty -> Ty

substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Ty -> Ty

Subst Ty Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Ty)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty)

subst :: Name Ty -> Ty -> Tm -> Tm

substs :: [(Name Ty, Ty)] -> Tm -> Tm

substPat :: AlphaCtx -> Ty -> Tm -> Tm

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm

rTm1 :: forall ctx. ctx Int -> ctx TmName -> ctx (Bind (TmName, TmName, Embed (Ty, Ty)) Tm) -> (ctx Tm, ctx Tm) -> ctx [Tm] -> (ctx Tm, ctx Int) -> (ctx Tm, ctx Prim, ctx Tm) -> (ctx Tm, ctx Tm, ctx Tm) -> ctx (Bind TyName Tm) -> (ctx Tm, ctx Ty) -> (ctx Tm, ctx Ty) -> R1 ctx Tm

rTm :: R Tm

rTy1 :: forall ctx. ctx TyName -> () -> (ctx Ty, ctx Ty) -> ctx (Bind TyName Ty) -> ctx [Ty] -> R1 ctx Ty

rTy :: R Ty

x :: Name Tm

y :: Name Tm

z :: Name Tm

f :: Name Tm

n :: Name Tm

a :: Name Ty

b :: Name Ty

c :: Name Ty

polyid :: Tm

polyconst :: Tm

polyidty :: Ty

two :: Tm

onePlusOne :: Tm

sixfact :: Tm

ctrue :: Tm

twice :: Tm

type Delta = [TyName]

type Gamma = [(TmName, Ty)]

data Ctx

Constructors

Ctx

Fields

• getDelta :: Delta
• getGamma :: Gamma

emptyCtx :: Ctx

checkTyVar :: Ctx -> TyName -> M ()

lookupTmVar :: Ctx -> TmName -> M Ty

extendTy :: TyName -> Ctx -> Ctx

extendTm :: TmName -> Ty -> Ctx -> Ctx

tcty :: Ctx -> Ty -> M ()

typecheck :: Ctx -> Tm -> M Tm

value :: Tm -> Bool

steps :: [Tm] -> M [Tm]

step :: Tm -> M Tm

evaluate :: Tm -> M Tm