Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Scoping: transforms p_term's into term's.
val scope_term :
bool ->
Core.Sig_state.sig_state ->
Core.Env.env ->
Core.Term.problem ->
(int -> Core.Term.meta option) ->
(string -> Core.Term.meta option) ->
Syntax.p_term ->
Core.Term.termscope prv ss env p mok mon t turns a pterm t into a term in the signature state ss, the environment env (for bound variables). mok k says if there already exists a meta with key k. mon n says if there already exists a meta with name n. Generated metas are added to p. prv indicates if private symbols are allowed.
val scope_term_with_params :
bool ->
Core.Sig_state.sig_state ->
Core.Env.env ->
Core.Term.problem ->
(int -> Core.Term.meta option) ->
(string -> Core.Term.meta option) ->
Syntax.p_term ->
Core.Term.termscope_term_with_params prv ss env p mok mon t is similar to scope_term
expo ss env p mok mon t except that t must be a product or an abstraction. In this case, no warnings are issued if the top binders are constant.
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_nbvariables do not appear in the LHS.pr_rhs : Core.Term.tbox;(*Body of the RHS, should only be unboxed once.
*)pr_names : (int, string) Stdlib.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.
val rule_of_pre_rule : pre_rule -> Core.Term.rulerule_of_pre_rule r converts a pre-rewrite rule into a rewrite rule.
val scope_rule :
bool ->
Core.Sig_state.sig_state ->
Syntax.p_rule ->
pre_rule Common.Pos.locscope_rule ur ss r turns a parser-level rewriting rule r, or a unification rule if ur is true, into a pre-rewriting rule.
val scope_rw_patt :
Core.Sig_state.sig_state ->
Core.Env.env ->
Syntax.p_rw_patt ->
(Core.Term.term, Core.Term.tbinder) Syntax.rw_pattscope_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).