|
Agda.Compiler.Epic.Forcing |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
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.
|
|
|
Returns the type of a constructor given its name
|
|
|
Returns how many parameters a datatype has
|
|
|
Is variable n used in a CompiledClause?
|
|
|
|
|
|
|
:: MonadTCM m | | => 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 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.
|
|
|
|
|
|
|
|
|
|
|
foldM' :: Monad m => a -> [b] -> (a -> b -> m a) -> m a | Source |
|
|
|
|
|
|
|
replaceForced (tpos, tele) forcedVars (cc, unification)
For each forceVar dig out the corresponding case and continue to remForced.
|
|
|
|
|
Substitute with the Substitution, this will adjust with the new bindings in the
CompiledClauses
|
|
|
Substitute variable n for term t in the body of cc
|
|
|
Perform a substitution in the body of cc
|
|
|
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.
|
|
Produced by Haddock version 2.6.1 |