Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.Epic.Forcing

Synopsis

- dataParameters :: QName -> Compile TCM Nat
- dataParametersTCM :: QName -> TCM Nat
- report :: MonadTrans t => Int -> TCM Doc -> t (TCMT IO) ()
- piApplyM' :: Type -> Args -> TCM Type
- insertTele :: (QName, Args) -> Int -> Maybe Type -> Term -> Telescope -> Compile TCM (Telescope, (Telescope, Type, Type))
- mkCon :: Integral a => QName -> a -> Term
- unifyI :: Telescope -> [Nat] -> Type -> Args -> Args -> Compile TCM [Maybe Term]
- takeTele :: (Eq a, Num a) => a -> Tele a1 -> Tele a1
- remForced :: [Fun] -> Compile TCM [Fun]
- forcedExpr :: [Var] -> Telescope -> Expr -> Compile TCM Expr
- replaceForced :: ([Var], [Var]) -> Telescope -> [Var] -> [Maybe Term] -> Expr -> Compile TCM Expr
- buildTerm :: Var -> Nat -> Term -> Compile TCM (Expr -> Expr, Var)
- findPosition :: Nat -> [Maybe Term] -> Compile TCM (Maybe (Nat, Term))

# Documentation

dataParameters :: QName -> Compile TCM Nat

Returns how many parameters a datatype has

dataParametersTCM :: QName -> TCM Nat

Returns how many parameters a datatype has

report :: MonadTrans t => Int -> TCM Doc -> t (TCMT IO) ()

piApplyM' :: Type -> Args -> TCM Type

insertTele

Arguments

:: (QName, Args) |
-> Int | ABS `pos` in tele
-> Maybe Type | If Just, it is the type to insert patterns from is nothing if we only want to delete a binding.
-> Term | Term to replace at pos
-> Telescope | The telescope `tele` where everything is at
-> Compile TCM (Telescope, (Telescope, Type, Type)) |

insertTele i xs t tele tpos tele := Gamma ; (i : T as) ; Delta n := parameters T xs' := xs `apply` (take n as) becomes tpos ( Gamma ; xs' ; Delta[i := t] --note that Delta still reference Gamma correctly , T as ^ (size xs') )

we raise the type since we have added xs' new bindings before Gamma, and as can only bind to Gamma.

mkCon :: Integral a => QName -> a -> Term

unifyI :: Telescope -> [Nat] -> Type -> Args -> Args -> Compile TCM [Maybe Term]

takeTele :: (Eq a, Num a) => a -> Tele a1 -> Tele a1

remForced :: [Fun] -> Compile TCM [Fun]

Main function for removing pattern matching on forced variables

forcedExpr :: [Var] -> Telescope -> Expr -> Compile TCM Expr

For a given expression, in a certain telescope (the list of Var) is a mapping of variable name to the telescope.

replaceForced :: ([Var], [Var]) -> Telescope -> [Var] -> [Maybe Term] -> Expr -> Compile TCM Expr

replace the forcedVar with pattern matching from the outside.

buildTerm :: Var -> Nat -> Term -> Compile TCM (Expr -> Expr, Var)

Given a term containg the forced var, dig out the variable by inserting the proper case-expressions.

findPosition :: Nat -> [Maybe Term] -> Compile TCM (Maybe (Nat, Term))

Find the location where a certain Variable index is by searching the constructors aswell. i.e find a term that can be transformed into a pattern that contains the same value the index. This fails if no such term is present.