package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/lambdapi.parsing/Parsing/Scope/index.html
Module Parsing.Scope
Source
Scoping. Convert parsed terms in core terms by finding out which identifiers are bound variables or function symbol declared in open modules.
val scope_term :
?find_sym:Core.Sig_state.find_sym ->
?typ:bool ->
?mok:(int -> Core.Term.meta option) ->
bool ->
Core.Sig_state.sig_state ->
Core.Env.env ->
Syntax.p_term ->
Core.Term.term
scope_term ~find_sym ~typ ~mok prv ss env t
turns a pterm t
into a term in the signature state ss
and environment env
(for bound variables). If prv
is true
, then the term must not contain any private subterms. If ~typ
is true
, then t
must be a type (defaults to false
). No new metavariables may appear in t
, but metavariables in the image of mok
may be used. The function mok
defaults to the function constant to None
. The function ~find_sym
is used to scope symbol identifiers.
val scope_search_pattern :
?find_sym:Core.Sig_state.find_sym ->
?typ:bool ->
?mok:(int -> Core.Term.meta option) ->
Core.Sig_state.sig_state ->
Core.Env.env ->
Syntax.p_term ->
Core.Term.term
scope_search_pattern ~find_sym ~typ prv ss env t
turns a pterm t
meant to be a search patter into a term in the signature state ss
and environment env
(for bound variables). If ~typ
is true
, then t
must be a type (defaults to false
). No new metavariables may appear in t
, but metavariables in the image of mok
may be used. The function mok
defaults to the function constant to None
. The function ~find_sym
is used to scope symbol identifiers.
type pre_rule = {
pr_sym : Core.Term.sym;
(*Head symbol of the LHS.
*)pr_lhs : Core.Term.term list;
(*Arguments of the LHS.
*)pr_vars : Core.Term.term_env Bindlib.mvar;
(*Pattern variables that appear in the RHS. The last
*)pr_xvars_nb
variables do not appear in the LHS.pr_rhs : Core.Term.tbox;
(*Body of the RHS, should only be unboxed once.
*)pr_names : (int, string) Hashtbl.t;
(*Gives the original name (if any) of pattern variable at given index.
*)pr_arities : int array;
(*Gives the arity of all the pattern variables in field
*)pr_vars
.pr_xvars_nb : int;
(*Number of variables that appear in the RHS but not in the LHS.
*)
}
Representation of a rewriting rule prior to SR-checking.
rule_of_pre_rule r
converts a pre-rewrite rule into a rewrite rule.
val scope_rule :
?find_sym:Core.Sig_state.find_sym ->
bool ->
Core.Sig_state.sig_state ->
Syntax.p_rule ->
pre_rule Common.Pos.loc
scope_rule ~find_sym ur ss r
turns a parser-level rewriting rule r
, or a unification rule if ur
is true, into a pre-rewriting rule. The function ~find_sym
is used to scope symbol identifiers.
val scope_rw_patt :
Core.Sig_state.sig_state ->
Core.Env.env ->
Syntax.p_rw_patt ->
(Core.Term.term, Core.Term.tbinder) Syntax.rw_patt
scope_rw_patt ss env t
turns a parser-level rewrite tactic specification s
into an actual rewrite specification (possibly containing variables of env
and using ss
for aliasing).