- dataParameters :: QName -> Compile TCM Nat
- dataParametersTCM :: QName -> TCM Nat
- piApplyM' :: Type -> Args -> TCM Type
- insertTele :: (QName, Args) -> Int -> Maybe Type -> Term -> Telescope -> Compile TCM (Telescope, (Telescope, Type, Type))
- unifyI :: Telescope -> [Nat] -> Type -> Args -> Args -> Compile TCM [Maybe Term]
- 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))
|:: (QName, Args)|
|-> Maybe Type|
If Just, it is the type to insert patterns from is nothing if we only want to delete a binding.
Term to replace at pos
|-> Compile TCM (Telescope, (Telescope, Type, Type))|
insertTele i xs t tele
tele := Gamma ; (i : T as) ; Delta
n := parameters T
xs' := xs
apply (take n as)
( 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.
Main function for removing pattern matching on forced variables
For a given expression, in a certain telescope (the list of Var) is a mapping of variable name to the telescope.
replace the forcedVar with pattern matching from the outside.
Given a term containg the forced var, dig out the variable by inserting the proper case-expressions.