Module Parsing.ScopeSource

Scoping: transforms p_term's into term's.

Sourceval 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.term

scope 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.

Sourceval 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.term

scope_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.

Sourcetype pre_rule = {
  1. pr_sym : Core.Term.sym;
    (*

    Head symbol of the LHS.

    *)
  2. pr_lhs : Core.Term.term list;
    (*

    Arguments of the LHS.

    *)
  3. 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.

    *)
  4. pr_rhs : Core.Term.tbox;
    (*

    Body of the RHS, should only be unboxed once.

    *)
  5. pr_names : (int, string) Hashtbl.t;
    (*

    Gives the original name (if any) of pattern variable at given index.

    *)
  6. pr_arities : int array;
    (*

    Gives the arity of all the pattern variables in field pr_vars.

    *)
  7. 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.

Sourceval rule_of_pre_rule : pre_rule -> Core.Term.rule

rule_of_pre_rule r converts a pre-rewrite rule into a rewrite rule.

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.

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).