From 404a8c619f76c572aec65f413baf087a374b37c3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Sep 2016 18:26:21 +0200 Subject: Generalizing the notion of constr substitution to generic arguments. This removes a dependency on wit_tactic in Constrintern. --- interp/constrintern.ml | 18 ++++-------------- interp/genintern.ml | 18 ++++++++++++++++++ interp/genintern.mli | 11 +++++++++++ 3 files changed, 33 insertions(+), 14 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 630f8d1402..fb11359e3c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -660,23 +660,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let open Tacexpr in - let open Genarg in - let wit = glbwit Constrarg.wit_tactic in - let body = - if has_type arg wit then out_gen wit arg - else assert false (** FIXME *) - in - let mk_env id (c, (tmp_scope, subscopes)) accu = + let mk_env (c, (tmp_scope, subscopes)) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in let gc = intern nenv c in - let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in - ((loc, id), c) :: accu + (gc, Some c) in - let bindings = Id.Map.fold mk_env terms [] in - let tac = TacLetIn (false, bindings, body) in - let arg = in_gen wit tac in - Some arg + let bindings = Id.Map.map mk_env terms in + Some (Genintern.generic_substitute_notation bindings arg) in GHole (loc, knd, naming, arg) | NBinderList (x,y,iter,terminator) -> diff --git a/interp/genintern.ml b/interp/genintern.ml index d6bfd347ff..693101a476 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -16,6 +16,7 @@ type glob_sign = { type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb +type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct @@ -31,8 +32,16 @@ struct let default _ = None end +module NtnSubstObj = +struct + type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun + let name = "notation_subst" + let default _ = None +end + module Intern = Register (InternObj) module Subst = Register (SubstObj) +module NtnSubst = Register (NtnSubstObj) let intern = Intern.obj let register_intern0 = Intern.register0 @@ -50,3 +59,12 @@ let generic_substitute subs (GenArg (Glbwit wit, v)) = in_gen (glbwit wit) (substitute wit subs v) let () = Hook.set Detyping.subst_genarg_hook generic_substitute + +(** Notation substitution *) + +let substitute_notation = NtnSubst.obj +let register_ntn_subst0 = NtnSubst.register0 + +let generic_substitute_notation env (GenArg (Glbwit wit, v)) = + let v = substitute_notation wit env v in + in_gen (glbwit wit) v diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b244b38d8..aabb85e009 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun val generic_substitute : glob_generic_argument subst_fun +(** {5 Notation functions} *) + +type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb + +val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun + +val generic_substitute_notation : glob_generic_argument ntn_subst_fun + (** Registering functions *) val register_intern0 : ('raw, 'glb, 'top) genarg_type -> @@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type -> val register_subst0 : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun -> unit + +val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb ntn_subst_fun -> unit -- cgit v1.2.3 From 975e7cd2ad032668c7df690c9bdaa8cdbb196569 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Sep 2016 16:09:17 +0200 Subject: Moving Ltac-specific generic arguments to their own file in the ltac/ folder. --- interp/constrarg.ml | 11 +---------- interp/constrarg.mli | 35 +++++++++++------------------------ 2 files changed, 12 insertions(+), 34 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ca828102b9..aaf33a956a 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -7,7 +7,6 @@ (************************************************************************) open Loc -open Tacexpr open Misctypes open Genarg open Geninterp @@ -27,14 +26,9 @@ let loc_of_or_by_notation f = function let wit_int_or_var = make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" -let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = +let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type = make0 "intropattern" -let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - make0 "tactic" - -let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" - let wit_ident = make0 "ident" @@ -61,9 +55,6 @@ let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = make0 "clause_dft_concl" -let wit_destruction_arg = - make0 "destruction_arg" - (** Aliases *) let wit_reference = wit_ref diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 6ccd944d43..32f2dc6f38 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -17,7 +17,6 @@ open Globnames open Genredexpr open Pattern open Constrexpr -open Tacexpr open Misctypes open Genarg @@ -28,7 +27,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type val wit_ident : Id.t uniform_genarg_type @@ -38,50 +37,38 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type +val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type -val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type +val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (constr_expr, glob_constr_and_expr, constr) genarg_type + (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type + Tacexpr.glob_constr_and_expr with_bindings, + constr with_bindings Pretyping.delayed_open) genarg_type val wit_bindings : (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type + Tacexpr.glob_constr_and_expr bindings, + constr bindings Pretyping.delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type - -(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their - toplevel interpretation. The one of [wit_ltac] forces the tactic and - discards the result. *) -val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type - val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type -val wit_destruction_arg : - (constr_expr with_bindings destruction_arg, - glob_constr_and_expr with_bindings destruction_arg, - delayed_open_constr_with_bindings destruction_arg) genarg_type - (** Aliases for compatibility *) val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type val wit_global : (reference, global_reference located or_var, global_reference) genarg_type val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -- cgit v1.2.3 From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Sep 2016 18:11:54 +0200 Subject: Untangling Tacexpr from lower strata. --- interp/constrarg.ml | 3 ++- interp/constrarg.mli | 23 ++++++++++++----------- interp/genintern.ml | 2 +- interp/genintern.mli | 2 +- 4 files changed, 16 insertions(+), 14 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index aaf33a956a..b8baa64019 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -8,6 +8,7 @@ open Loc open Misctypes +open Tactypes open Genarg open Geninterp @@ -26,7 +27,7 @@ let loc_of_or_by_notation f = function let wit_int_or_var = make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" -let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type = +let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = make0 "intropattern" let wit_ident = diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 32f2dc6f38..4b542675b9 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -18,6 +18,7 @@ open Genredexpr open Pattern open Constrexpr open Misctypes +open Tactypes open Genarg (** FIXME: nothing to do there. *) @@ -27,7 +28,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type +val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type val wit_ident : Id.t uniform_genarg_type @@ -37,26 +38,26 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type +val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type +val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type + (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, - Tacexpr.glob_constr_and_expr with_bindings, - constr with_bindings Pretyping.delayed_open) genarg_type + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, - Tacexpr.glob_constr_and_expr bindings, - constr bindings Pretyping.delayed_open) genarg_type + glob_constr_and_expr bindings, + constr bindings delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type @@ -67,8 +68,8 @@ val wit_reference : (reference, global_reference located or_var, global_referenc val wit_global : (reference, global_reference located or_var, global_reference) genarg_type val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/genintern.ml b/interp/genintern.ml index 693101a476..be7abfa995 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -16,7 +16,7 @@ type glob_sign = { type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb -type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct diff --git a/interp/genintern.mli b/interp/genintern.mli index aabb85e009..4b0354be39 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -34,7 +34,7 @@ val generic_substitute : glob_generic_argument subst_fun (** {5 Notation functions} *) -type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun -- cgit v1.2.3