Agda-2.2.10: A dependently typed functional programming language and proof assistant




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



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

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.

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.