Data associated to inductive type symbols.

Data associated to a symbol defined in another file.

Data associated to a dependency.

Representation of a signature. It roughly corresponds to a set of symbols, defined in a single module (or file).

The empty signature. WARNING: to be used for creating ghost signatures only. Use Sig_state functions otherwise. It's a thunk to force the creation of a new record on each call (and avoid unwanted sharing).

find sign name finds the symbol named name in sign if it exists, and raises the Not_found exception otherwise.

mem sign name checks whether a symbol named name exists in sign.

loaded stores the signatures of the known (already compiled or currently being compiled) modules. An important invariant is that all occurrences of a symbol are physically equal, even across signatures). This is ensured by making copies of terms when loading an object file.

find_sym path name returns the symbol identified by path and name in the known modules (already compiled or currently being compiled)

loading contains the modules that are being processed. They are stored in a stack due to dependencies. Note that the topmost element corresponds to the current module. If a module appears twice in the stack, then there is a circular dependency.

current_path () returns the current signature path.

Signature for symbols introduced by Lambdapi and not the user (e.g. unification/coercion rules, strings) and always loaded.

unlink sign removes references to external symbols (and thus signatures) in the signature sign. This function is used to minimize the size of object files, by preventing a recursive inclusion of all the dependencies. Note however that unlink processes sign in place, which means that the signature is invalidated in the process.

add_symbol sign expo prop mstrat opaq name pos typ impl notation adds in the signature sign a symbol with name name, exposition expo, property prop, matching strategy strat, opacity opaq, type typ, implicit arguments impl, no notation, no definition and no rules. name should not already be used in sign. pos is the position of the declaration (without its definition). The created symbol is returned.

strip_private sign removes private symbols from signature sign.

add_rule sign s r adds the new rule r to the symbol s. When the rule does not correspond to a symbol of signature sign, it is stored in its dependencies. /!\ does not update the decision tree or the critical pairs.

add_rules sign s rs adds the new rules rs to the symbol s. When the rules do not correspond to a symbol of signature sign, they are stored in its dependencies. /!\ does not update the decision tree or the critical pairs.

add_notation sign sym nota changes the notation of s to n in the signature sign.

add_builtin sign name sym binds the builtin name to sym in the signature sign. The previous binding, if any, is discarded.

add_inductive sign ind_sym ind_cons ind_prop ind_prop_args add to sign the inductive type ind_sym with constructors ind_cons, induction principle ind_prop with ind_prop_args arguments.

iterate f sign applies f on sign and its dependencies recursively.

dependencies sign returns an association list containing (the transitive closure of) the dependencies of the signature sign. Note that the order of the list gives one possible loading order for the signatures. Note also that sign itself appears at the end of the list.