Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.Forcing
Synopsis
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 {
clauseToFix :: CompiledClauses
clausesAbove :: CompiledClauses -> CompiledClauses
unification :: [Maybe Term]
theTelescope :: Telescope
telePos :: Nat
}
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?
isInCase :: MonadTCM m => Nat -> (Nat, Case CompiledClauses) -> Compile m BoolSource
isInTerm :: Nat -> Term -> BoolSource
insertTeleSource
:: MonadTCM m
=> IntABS pos in tele
-> Maybe TypeIf Just, it is the type to insert patterns from is nothing if we only want to delete a binding.
-> TermTerm to replace at pos
-> TelescopeThe 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.

unifyI :: MonadTCM m => Telescope -> [Nat] -> Type -> Args -> Args -> Compile m [Maybe Term]Source
remForcedSource
:: MonadTCM m
=> CompiledClausesRemove cases on forced variables in this
-> TelescopeThe current context we are in
-> Compile m CompiledClauses
Remove forced variables cased on in the current top-level case in the CompiledClauses
data FoldState Source
Constructors
FoldState
clauseToFix :: CompiledClauses
clausesAbove :: CompiledClauses -> CompiledClauses
unification :: [Maybe Term]
theTelescope :: Telescope
telePos :: Nat
foldM' :: Monad m => a -> [b] -> (a -> b -> m a) -> m aSource
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
findPosition :: Nat -> [Maybe Term] -> (Nat, Term)Source
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