package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.2.1.tbz
sha256=ba73f288e435130293408bd44732f1dfc5ec8a8db91c7453c9baf9c740095829
sha512=f88bb92fdb8aee8add60588673040fac012b2eab17c2a1d529c4b7c795cf0e1a9168122dc19889f04a31bda2bb2cf820237cbbe7e319121618aba3d134381756

doc/lambdapi.core/Core/Sign/index.html

Module Core.SignSource

Signature for symbols.

Sourcetype ind_data = {
  1. ind_cons : Term.sym list;
    (*

    Constructors.

    *)
  2. ind_prop : Term.sym;
    (*

    Induction principle.

    *)
  3. ind_nb_params : int;
    (*

    Number of parameters.

    *)
  4. ind_nb_types : int;
    (*

    Number of mutually defined types.

    *)
  5. ind_nb_cons : int;
    (*

    Number of constructors.

    *)
}

Data associated to inductive type symbols.

Sourcetype priority = float

The priority of an infix operator is a floating-point number.

Sourcetype notation =
  1. | Prefix of priority
  2. | Postfix of priority
  3. | Infix of Pratter.associativity * priority
  4. | Zero
  5. | Succ
  6. | Quant

Notations.

Sourcetype t = {
  1. sign_symbols : Term.sym Lplib.Extra.StrMap.t Timed.ref;
  2. sign_path : Common.Path.t;
  3. sign_deps : Term.rule list Lplib.Extra.StrMap.t Common.Path.Map.t Timed.ref;
    (*

    Maps a path to a list of pairs (symbol name, rule).

    *)
  4. sign_builtins : Term.sym Lplib.Extra.StrMap.t Timed.ref;
  5. sign_notations : notation Term.SymMap.t Timed.ref;
    (*

    Maps symbols to their notation if they have some.

    *)
  6. sign_ind : ind_data Term.SymMap.t Timed.ref;
  7. sign_cp_pos : Term.cp_pos list Term.SymMap.t Timed.ref;
    (*

    Maps a symbol to the critical pair positions it is heading in the rules.

    *)
}

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

Sourceval dummy : unit -> t

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

Sourceval find : t -> string -> Term.sym

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

Sourceval mem : t -> string -> bool

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

Sourceval loaded : t Common.Path.Map.t Timed.ref

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.

Sourceval loading : Common.Path.t list Timed.ref

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.

Sourceval current_path : unit -> Common.Path.t

current_path () returns the current signature path.

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.

Sourceval add_symbol : t -> Term.expo -> Term.prop -> Term.match_strat -> bool -> Common.Pos.strloc -> Term.term -> bool list -> Term.sym

add_symbol sign expo prop mstrat opaq name typ impl 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 definition and no rules. name should not already be used in sign. The created symbol is returned.

Sourceval strip_private : t -> unit

strip_private sign removes private symbols from signature sign.

Sourceval write : t -> string -> unit
Sourceval read : string -> t
Sourceval add_rule : t -> Term.sym -> Term.rule -> unit

add_rule sign sym r adds the new rule r to the symbol sym. 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.

Sourceval add_rules : t -> Term.sym -> Term.rule list -> unit

add_rules sign sym rs adds the new rules rs to the symbol sym. 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.

Sourceval add_builtin : t -> string -> Term.sym -> unit

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

Sourceval add_notation : t -> Term.sym -> notation -> unit

add_notation sign s n sets notation of s to n in sign.

Sourceval add_inductive : t -> Term.sym -> Term.sym list -> Term.sym -> int -> int -> unit

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.

Sourceval dependencies : t -> (Common.Path.t * t) list

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.