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.0.tbz
sha256=920de48ec6c2c3223b6b93879bb65d07ea24aa27f7f7176b3de16e5e467b9939
sha512=135f132730825adeb084669222e68bc999de97b12378fae6abcd9f91ae13093eab29fa49c854adb28d064d52c9890c0f5c8ff9d47a9916f66fe5e0fba3479759

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

Module Core.Sig_stateSource

Signature state.

This module provides a record type sig_state containing all the informations needed for scoping p_terms and printing terms, and functions on this type for manipulating it. In particular, it provides functions open_sign, add_symbol, add_binop, etc. taking a sig_state as argument and returning a new sig_state as result. These functions call the corresponding functions of Sign which should not be called directly but through the current module only, in order to setup the sig_state properly.

Sourceval create_sign : Common.Path.t -> Sign.t

create_sign path creates a signature with path path with ghost modules as dependencies.

Sourcetype sig_state = {
  1. signature : Sign.t;
    (*

    Current signature.

    *)
  2. in_scope : Term.sym Lplib.Extra.StrMap.t;
    (*

    Symbols in scope.

    *)
  3. alias_path : Common.Path.t Lplib.Extra.StrMap.t;
    (*

    Alias to path map.

    *)
  4. path_alias : string Common.Path.Map.t;
    (*

    Path to alias map.

    *)
  5. builtins : Term.sym Lplib.Extra.StrMap.t;
    (*

    Builtins.

    *)
  6. notations : Sign.notation Term.SymMap.t;
    (*

    Notations.

    *)
  7. open_paths : Common.Path.Set.t;
    (*

    Open modules.

    *)
}

State of the signature, including aliasing and accessible symbols.

Sourceval dummy : sig_state

Dummy sig_state.

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

add_symbol ss expo prop mstrat opaq id typ impl def generates a new signature state from ss by creating a new symbol with expo e, property p, strategy st, name x, type a, implicit arguments impl and optional definition def. This new symbol is returned too.

Sourceval add_notation : sig_state -> Term.sym -> Sign.notation -> sig_state

add_notation ss s n maps s notation to n in ss.

Sourceval add_builtin : sig_state -> string -> Term.sym -> sig_state

add_builtin ss n s generates a new signature state from ss by mapping the builtin n to s.

add_notations_from_builtins notmap bm add notations for symbols mapped to the builtins "0" and "+1".

Sourceval open_sign : sig_state -> Sign.t -> sig_state

open_sign ss sign extends the signature state ss with every symbol of the signature sign. This has the effect of putting these symbols in the scope when (possibly masking symbols with the same name). Builtins and notations are also handled in a similar way.

Sourceval of_sign : Sign.t -> sig_state

of_sign sign creates a state from the signature sign and open it as well as the ghost signatures.

Sourceval find_sym : prt:bool -> prv:bool -> sig_state -> Term.qident Common.Pos.loc -> Term.sym

find_sym ~prt ~prv b st qid returns the symbol corresponding to the qualified identifier qid. If fst qid.elt is empty, we search for the name snd qid.elt in the opened modules of st. The boolean b only indicates if the error message should mention variables, in the case where the module path is empty and the symbol is unbound. This is reported using the Fatal exception. Term.expo.Protec symbols from other modules are allowed in left-hand side of rewrite rules (only) iff ~prt is true. Term.expo.Privat symbols are allowed iff ~prv is true.