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

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