package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/lambdapi.core/Core/Sig_state/index.html
Module Core.Sig_state
Source
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
with ghost modules as dependencies.
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.
*)notations : float Sign.notation Term.SymMap.t;
(*Notations.
*)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.sym
add_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_notation ss s n
maps s
notation to n
in ss
.
add_builtin ss n s
generates a new signature state from ss
by mapping the builtin n
to s
.
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.
of_sign sign
creates a state from the signature sign
and open it as well as the ghost signatures.
find_sym
is the type of functions used to return the symbol corresponding to a qualified / non qualified name
find_sym ~prt ~prv b st 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.