Library
Module
Module type
Parameter
Class
Class type
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.term
scope ~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_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_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.rule
rule_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.loc
scope_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_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).