Agda.Compiler.Epic.Forcing
- 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 CompiledClauses
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 Type
Returns the type of a constructor given its name
dataParameters :: MonadTCM m => QName -> Compile m Nat
Returns how many parameters a datatype has
isIn :: MonadTCM m => Nat -> CompiledClauses -> Compile m Bool
Is variable n used in a CompiledClause?
Arguments
:: 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.
Arguments
:: 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
data FoldState
Constructors
FoldState | |
Fields
|
replaceForced :: MonadTCM m => (Nat, Telescope) -> [Nat] -> (CompiledClauses, [Maybe Term]) -> Compile m CompiledClauses
replaceForced (tpos, tele) forcedVars (cc, unification) For each forceVar dig out the corresponding case and continue to remForced.
raiseFromCC :: Nat -> Nat -> CompiledClauses -> CompiledClauses
substCC :: MonadTCM m => [Nat] -> CompiledClauses -> StateT FoldState (Compile m) CompiledClauses
Substitute with the Substitution, this will adjust with the new bindings in the CompiledClauses
substCCBody :: Nat -> Term -> CompiledClauses -> CompiledClauses
Substitute variable n for term t in the body of cc
substsCCBody :: [Term] -> CompiledClauses -> CompiledClauses
Perform a substitution in the body of cc