package lambdapi
-
lambdapi.tool
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. Convert parsed terms in core terms by finding out which identifiers are bound variables or function symbol declared in open modules.
val scope_term :
?typ:bool ->
?mok:(int -> Core.Term.meta option) ->
bool ->
Core.Sig_state.sig_state ->
Core.Env.env ->
Syntax.p_term ->
Core.Term.termscope ~typ ~mok prv expo ss env p t turns a pterm t into a term in the signature state ss and environment env (for bound variables). If expo is Public, 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
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 Common.Pos.loc -> 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).