Documentation

Add a constant to the signature. Lifts the definition to top level.

A combination of addConstant and defaultDefn. The Language does not need to be supplied.

Set termination info of a defined function symbol.

Set CompiledClauses of a defined function symbol.

Set SplitTree of a defined function symbol.

Modify the clauses of a function.

Lifts clauses to the top-level and adds them to definition. Also adjusts the funCopatternLHS field if necessary.

Add a compiler pragma `{-# COMPILE backend name text #-}`

Add a section to the signature.

The current context will be stored as the cumulative module parameters for this section, and a module checkpoint entry will be added into the module checkpoint stack.

Get a section.

Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.

Lookup a section telescope.

If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.

Add display forms for a name f copied by a module application. Essentially if f can reduce to

λ xs → A.B.C.f vs

by unfolding module application copies (defCopy), then we add a display form

A.B.C.f vs ==> f xs

Invoking addDisplayForms x will add a display form for each copy x transitively reduces to. E.g. consider the following iterated module application. module M0 (n : Nat) where b : Bool b = n > 42 module M1 (n : Nat) = M0 (suc n) module M2 (n : Nat) = M1 (suc n) module M3 (n : Nat) = M2 (suc n)

For the first copy M1.b n = M0.b (suc n) we add the display form M0.b (suc n) --> M1.b n.

For the second copy M2.b n = M1.b (suc n) we first add display form M1.b (suc n) --> M2.b n and for the further unfolding we add display form M0.b (suc (suc n)) --> M2.b n.

For the third copy M3.b n = M2.b (suc n) we add display forms M2.b (suc n) --> M3.b n, M1.b (suc (suc n)) --> M3.b n and M0.b (suc (suc (suc n))) --> M3.b n.

Module application (followed by module parameter abstraction).

Add a display form to a definition (could be in this or imported signature).

Find all names used (recursively) by display forms of a given name.

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

Signature lookup errors.

An eliminator for SigError. All constructors except for SigAbstract are assumed to be impossible.

The computation getConstInfo sometimes tweaks the returned Definition, depending on the current Language and the Language of the Definition. This variant of getConstInfo does not perform any tweaks.

Get the original name of the projection (the current one could be from a module application).

Look up the polarity of a definition.

Look up polarity of a definition and compose with polarity represented by Comparison.

Set the polarity of a definition.

Look up the forced arguments of a definition.

Get argument occurrence info for argument i of definition d (never fails).

Sets the defArgOccurrences for the given identifier (which should already exist in the signature).

add data constructors to a datatype

Get the mutually recursive identifiers of a symbol from the signature.

Get the mutually recursive identifiers from a Definition.

Set the mutually recursive identifiers.

TODO: This produces data of quadratic size (which has to be processed upon serialization). Presumably qs is usually short, but in some cases (for instance for generated code) it may be long. It would be better to assign a unique identifier to each SCC, and store the names separately.

Check whether two definitions are mutually recursive.

A function, data, or record definition is definitely not recursive if it is not even mutually recursive with itself.

Get the number of parameters to the current module.

Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).

Compute the context variables to apply a definition to.

We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)

Example: module M₁ Γ where module M₁ Δ where f = ... module M₃ Θ where ... M₁.M₂.f [insert Γ raised by Θ]

Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.

Instantiate a closed definition with the correct part of the current context.

Return the abstract view of a definition, regardless of whether the definition would be treated abstractly.

Enter abstract mode. Abstract definition in the current module are transparent.

Not in abstract mode. All abstract definitions are opaque.

Ignore abstract mode. All abstract definitions are transparent.

Go under the given opaque block. The unfolding set will turn opaque definitions transparent.

Outside of any opaque blocks.

Enter the reducibility environment associated with a definition: The environment will have the same concreteness as the name, and we will be in the opaque block enclosing the name, if any.

Get type of a constant, instantiated to the current context.

The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.

Is it the name of a record projection or field or a projection-like function?

Is it a record projection or field or a projection-like function?

Is it a record projection or field or a projection-like function?

Is it a function marked INLINE?

Returns True if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

Returns True if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

Number of dropped initial arguments of a projection(-like) function.

Check whether a definition uses copatterns.

Apply a function f to its first argument, producing the proper postfix projection if f is a projection.