package lambdapi
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c
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.
create_sign path creates a signature with path path and the ghost module as dependency.
type sig_state = {signature : Sign.t;(*Current signature.
*)in_scope : Term.sym Lplib.Extra.StrMap.t;(*Symbols in scope.
*)alias_path : Common.Path.t Lplib.Extra.StrMap.t;(*Alias to path map.
*)path_alias : string Common.Path.Map.t;(*Path to alias map.
*)builtins : Term.sym Lplib.Extra.StrMap.t;(*Builtins.
*)open_paths : Common.Path.Set.t;(*Open modules.
*)
}State of the signature, including aliasing and accessible symbols.
val add_symbol :
sig_state ->
Term.expo ->
Term.prop ->
Term.match_strat ->
bool ->
Common.Pos.strloc ->
Common.Pos.popt ->
Term.term ->
bool list ->
Term.term option ->
sig_state * Term.symadd_symbol ss expo prop mstrat opaq id pos 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. pos is the position of the declaration without its definition. This new symbol is returned too.
add_builtin ss b s generates a new signature state from ss by mapping the builtin string b to the symbol s, and by updating the notation of s when b is a builtin used for printing.
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, possibly masking symbols with the same name.
of_sign sign creates a state from the signature sign and open it as well as the ghost signature.
find_sym is the type of functions used to return the symbol corresponding to a qualified / non qualified name
find_sym ~prt ~prv b ss qid returns the symbol corresponding to the possibly qualified identifier qid, or raises Fatal. The boolean b indicates if the error message should mention variables when qid is unqualified. ~prt indicates whether Term.expo.Protec symbols from other modules are allowed. ~prv indicates whether Term.expo.Privat symbols are allowed.