- removeForced :: MonadTCM m => CompiledClauses -> Type -> Compile m CompiledClauses
- constrType :: MonadTCM m => QName -> Compile m Type
- dataParameters :: MonadTCM m => QName -> Compile m Nat
- isIn :: MonadTCM m => Nat -> CompiledClauses -> Compile m Bool
- isInCase :: MonadTCM m => Nat -> (Nat, Case CompiledClauses) -> Compile m Bool
- isInTerm :: Nat -> Term -> Bool
- insertTele :: MonadTCM m => Int -> Maybe Type -> Term -> Telescope -> Compile m (Telescope, (Type, Type))
- unifyI :: MonadTCM m => Telescope -> [Nat] -> Type -> Args -> Args -> Compile m [Maybe Term]
- remForced :: MonadTCM m => CompiledClauses -> Telescope -> Compile m CompiledClauses
- data FoldState = FoldState {}
- foldM' :: Monad m => a -> [b] -> (a -> b -> m a) -> m a
- lift2 :: (MonadTrans t, Monad (t1 m), MonadTrans t1, Monad m) => m a -> t (t1 m) a
- modifyM :: MonadState a m => (a -> m a) -> m ()
- replaceForced :: MonadTCM m => (Nat, Telescope) -> [Nat] -> (CompiledClauses, [Maybe Term]) -> Compile m CompiledClauses
- raiseFromCC :: Nat -> Nat -> CompiledClauses -> CompiledClauses
- substCC :: MonadTCM m => [Nat] -> CompiledClauses -> StateT FoldState (Compile m) CompiledClauses
- substCCBody :: Nat -> Term -> CompiledClauses -> CompiledClauses
- substsCCBody :: [Term] -> CompiledClauses -> CompiledClauses
- findPosition :: Nat -> [Maybe Term] -> (Nat, Term)
Documentation
removeForced :: MonadTCM m => CompiledClauses -> Type -> Compile m CompiledClausesSource
Replace the uses of forced variables in a CompiledClauses with the function arguments that they correspond to. Note that this works on CompiledClauses where the term's variable indexes have been reversed, which means that the case variables match the variables in the term.
constrType :: MonadTCM m => QName -> Compile m TypeSource
Returns the type of a constructor given its name
dataParameters :: MonadTCM m => QName -> Compile m NatSource
Returns how many parameters a datatype has
isIn :: MonadTCM m => Nat -> CompiledClauses -> Compile m BoolSource
Is variable n used in a CompiledClause?
:: MonadTCM m | |
=> Int | ABS |
-> 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 |
-> Compile m (Telescope, (Type, Type)) | Returns (resulting telescope, the type at pos in tele, the return type of the inserted 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.
:: MonadTCM m | |
=> CompiledClauses | Remove cases on forced variables in this |
-> Telescope | The current context we are in |
-> Compile m CompiledClauses |
Remove forced variables cased on in the current top-level case in the CompiledClauses
FoldState | |
|
lift2 :: (MonadTrans t, Monad (t1 m), MonadTrans t1, Monad m) => m a -> t (t1 m) aSource
modifyM :: MonadState a m => (a -> m a) -> m ()Source
replaceForced :: MonadTCM m => (Nat, Telescope) -> [Nat] -> (CompiledClauses, [Maybe Term]) -> Compile m CompiledClausesSource
replaceForced (tpos, tele) forcedVars (cc, unification) For each forceVar dig out the corresponding case and continue to remForced.
raiseFromCC :: Nat -> Nat -> CompiledClauses -> CompiledClausesSource
substCC :: MonadTCM m => [Nat] -> CompiledClauses -> StateT FoldState (Compile m) CompiledClausesSource
Substitute with the Substitution, this will adjust with the new bindings in the CompiledClauses
substCCBody :: Nat -> Term -> CompiledClauses -> CompiledClausesSource
Substitute variable n for term t in the body of cc
substsCCBody :: [Term] -> CompiledClauses -> CompiledClausesSource
Perform a substitution in the body of cc