From 9262f440e8d8b8559c5488b1333c023f7305d811 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 23:08:19 +0100 Subject: Allowing to pass arbitrary data in internalization environments. --- plugins/ltac/g_obligations.ml4 | 2 +- plugins/ltac/tacintern.ml | 24 ++++++++++++++---------- plugins/ltac/tacintern.mli | 4 +++- plugins/ltac/tacinterp.ml | 7 ++++--- 4 files changed, 22 insertions(+), 15 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 3e6e2db605..a301daa57b 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -31,7 +31,7 @@ let () = Obligations.default_tactic := tac let with_tac f tac = - let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let env = Genintern.empty_glob_sign (Global.env ()) in let tac = match tac with | None -> None | Some tac -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75227def0f..40a299f76d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -41,13 +41,12 @@ let error_tactic_expected ?loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} -let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; genv = Environ.empty_env } - -let make_empty_glob_sign () = - { fully_empty_glob_sign with genv = Global.env () } +let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env +let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -192,12 +191,13 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { Constrintern.ltac_vars = lfun; ltac_bound = Id.Set.empty; + ltac_extra = extra; } in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c @@ -313,6 +313,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = { Constrintern.ltac_vars = ltacvars; ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc @@ -344,7 +345,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let r = match r with | AN r -> r | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in - let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in + let sign = { + Constrintern.ltac_vars = ist.ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in let c = Constrintern.interp_reference sign r in match c with | GRef (_,r,None) -> @@ -708,8 +713,7 @@ let glob_tactic_env l env x = let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check - (intern_pure_tactic - { ltacvars; genv = env }) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x let split_ltac_fun = function diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 71ca354fa1..8ad52ca023 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -18,7 +18,9 @@ open Misctypes type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} val fully_empty_glob_sign : glob_sign diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b8c021f188..5f831f3260 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -587,6 +587,7 @@ let interp_uconstr ist env sigma = function let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; + ltac_extra = Genintern.Store.empty; } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } @@ -614,6 +615,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = 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 @@ -1966,8 +1968,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ist = { lfun = lfun; extra = extra } in let ltacvars = Id.Map.domain lfun in interp_tactic ist - (intern_pure_tactic { - ltacvars; genv = env } t) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -1976,7 +1977,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = let hide_interp env = - let ist = { ltacvars = Id.Set.empty; genv = env } in + let ist = Genintern.empty_glob_sign env in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with -- cgit v1.2.3 From 173f32406be06ad4dfcecf3cda6070543d68d715 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Dec 2016 14:07:28 +0100 Subject: Generalizing the tactic-in-term embedding to any generic argument. --- plugins/ltac/tacinterp.ml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5f831f3260..7f7a643387 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2100,17 +2100,13 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval ty env sigma lfun arg = + let eval lfun env sigma ty tac = let ist = { lfun = lfun; extra = TacStore.empty; } in - if Genarg.has_type arg (glbwit wit_tactic) then - let tac = Genarg.out_gen (glbwit wit_tactic) arg in - let tac = interp_tactic ist tac in - let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in - (EConstr.of_constr c, sigma) - else - failwith "not a tactic" + let tac = interp_tactic ist tac in + let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + (EConstr.of_constr c, sigma) in - Hook.set Pretyping.genarg_interp_hook eval + Pretyping.register_constr_interp0 wit_tactic eval (** Used in tactic extension **) -- cgit v1.2.3