Agda.Compiler.Epic.Forcing

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?

isInCase :: MonadTCM m => Nat -> (Nat, Case CompiledClauses) -> Compile m Bool

isInTerm :: Nat -> Term -> Bool

insertTele

Arguments

:: 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.

unifyI :: MonadTCM m => Telescope -> [Nat] -> Type -> Args -> Args -> Compile m [Maybe Term]

remForced

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

clauseToFix :: CompiledClauses

clausesAbove :: CompiledClauses -> CompiledClauses

unification :: [Maybe Term]

theTelescope :: Telescope

telePos :: Nat

Instances

Show 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

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

findPosition :: Nat -> [Maybe Term] -> (Nat, Term)

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.