From a3407e27e60104fa8ea2e62433f9920a41a22757 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 19:40:55 +0200 Subject: Splitting interp_open_constr into two variants, with or without type classes. This simplifies the API as before, inference of instances of type classes was iff a type constraint was given. We then export these both versions of interp_open_constr. --- plugins/ltac/tacinterp.ml | 8 ++++---- plugins/ltac/tacinterp.mli | 8 ++++++++ 2 files changed, 12 insertions(+), 4 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a9ec779d11..b105074e82 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -673,10 +673,10 @@ let pure_open_constr_flags = { (* Interprets an open constr *) let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = - let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () - else open_constr_use_classes_flags () in - interp_gen expected_type ist false flags env sigma c + interp_gen expected_type ist false (open_constr_no_classes_flags ()) env sigma c + +let interp_open_constr_with_classes ?(expected_type=WithoutTypeConstraint) ist env sigma c = + interp_gen expected_type ist false (open_constr_use_classes_flags ()) env sigma c let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 2ec45312ea..c80b1738f8 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -78,6 +78,14 @@ val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings +val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + +val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings -- cgit v1.2.3 From 94126f45582b7f02a6c16284cdc627b7b0fe53ac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 19:44:21 +0200 Subject: Factorizing interp_gen through a function interpreting glob_constr. The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure. --- plugins/ltac/tacinterp.ml | 56 +++++++++++++++++++--------------------------- plugins/ltac/tacinterp.mli | 9 +++++++- 2 files changed, 31 insertions(+), 34 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b105074e82..902fa34428 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -577,57 +577,47 @@ let extract_ltac_constr_context ist env sigma = (** Significantly simpler than [interp_constr], to interpret an untyped constr, it suffices to adjoin a closure environment. *) -let interp_uconstr ist env sigma = function - | (term,None) -> - { closure = extract_ltac_constr_context ist env sigma; term } - | (_,Some ce) -> - let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in +let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(allow_patvar=false) (term,term_expr_opt) = + let closure = extract_ltac_constr_context ist env sigma in + match term_expr_opt with + | None -> { closure ; term } + | Some term_expr -> + (* If at toplevel (term_expr_opt<>None), the error can be due to + an incorrect context at globalization time: we retype with the + now known intros/lettac/inversion hypothesis names *) + let constr_context = + Id.Set.union + (Id.Map.domain closure.typed) + (Id.Map.domain closure.untyped) + in let ltacvars = { - Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); + ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; ltac_extra = Genintern.Store.empty; } in - { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } + { closure ; term = intern_gen kind ~allow_patvar ~ltacvars env term_expr } -let interp_gen kind ist allow_patvar flags env sigma (c,ce) = - let constrvars = extract_ltac_constr_context ist env sigma in +let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c + +let interp_gen kind ist allow_patvar flags env sigma c = + let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in + let { closure = constrvars ; term } = + interp_glob_closure ist env sigma ~kind:kind_for_intern ~allow_patvar c in let vars = { Pretyping.ltac_constrs = constrvars.typed; Pretyping.ltac_uconstrs = constrvars.untyped; Pretyping.ltac_idents = constrvars.idents; Pretyping.ltac_genargs = ist.lfun; } in - let c = match ce with - | None -> c - (* If at toplevel (ce<>None), the error can be due to an incorrect - context at globalization time: we retype with the now known - intros/lettac/inversion hypothesis names *) - | Some c -> - let constr_context = - Id.Set.union - (Id.Map.domain constrvars.typed) - (Id.Set.union - (Id.Map.domain constrvars.untyped) - (Id.Map.domain constrvars.idents)) - in - let ltacvars = { - ltac_vars = constr_context; - ltac_bound = Id.Map.domain ist.lfun; - ltac_extra = Genintern.Store.empty; - } in - let kind_for_intern = - match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in - intern_gen kind_for_intern ~allow_patvar ~ltacvars env c - in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do this with the kludge of an empty proofview, and rely on the invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in + let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = - catch_error trace (understand_ltac flags env sigma vars kind) c + catch_error trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index c80b1738f8..fd2c5574bb 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -72,11 +72,18 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Id.t Loc.located -> Id.t +val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> + ?kind:Pretyping.typing_constraint -> ?allow_patvar:bool -> glob_constr_and_expr -> + Glob_term.closed_glob_constr + +val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Glob_term.closed_glob_constr + val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr bindings -> Evd.evar_map * constr bindings + glob_constr_and_expr bindings -> Evd.evar_map * constr bindings val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> -- cgit v1.2.3