Parsing.ScopeSourceScoping. 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.termscope_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.termscope_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.
val scope_rule :
?find_sym:Core.Sig_state.find_sym ->
bool ->
Core.Sig_state.sig_state ->
Syntax.p_rule ->
Core.Term.sym_rulescope_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.binder) 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).