aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrarg.ml2
-rw-r--r--interp/constrarg.mli2
-rw-r--r--plugins/decl_mode/decl_expr.mli2
-rw-r--r--plugins/decl_mode/decl_interp.ml2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--plugins/firstorder/g_ground.ml48
-rw-r--r--plugins/quote/g_quote.ml413
-rw-r--r--plugins/setoid_ring/newring.ml13
-rw-r--r--plugins/setoid_ring/newring.mli4
-rw-r--r--printing/pptactic.ml10
-rw-r--r--printing/pptactic.mli2
-rw-r--r--tactics/extraargs.mli2
-rw-r--r--tactics/extratactics.ml416
-rw-r--r--tactics/g_class.ml42
-rw-r--r--tactics/tacinterp.ml7
-rw-r--r--tactics/tacinterp.mli2
-rw-r--r--tactics/tauto.ml47
17 files changed, 48 insertions, 50 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index b093d92e7..a48d68375 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -25,7 +25,7 @@ let wit_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 =
Genarg.make0 None "intropattern"
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
Genarg.make0 None "tactic"
let wit_ident =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index e1a5f4d7c..5c26af3c2 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -69,6 +69,6 @@ val wit_red_expr :
(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_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) 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
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 79ef3d186..9d78a51ef 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -99,4 +99,4 @@ type proof_instr =
(Term.constr statement,
Term.constr,
proof_pattern,
- Tacexpr.glob_tactic_expr) gen_proof_instr
+ Genarg.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 7cfca53c5..4874552d6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let interp_cut interp_it env sigma cut=
let nenv,nstat = interp_it env sigma cut.cut_stat in
- {cut with
+ { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
cut_stat=nstat;
cut_by=interp_justification_items nenv sigma cut.cut_by}
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index adfcb3e60..090b293f5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -496,7 +496,7 @@ let just_tac _then cut info gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
justification (tclTHEN items_tac method_tac) gls0
let instr_cut mkstat _thus _then cut gls0 =
@@ -546,7 +546,7 @@ let instr_rew _thus rew_side cut gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
let just_tac gls =
justification (tclTHEN items_tac method_tac) gls in
let (c_id,_) = match cut.cut_stat.st_label with
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 25509b4b5..3e8be3699 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -135,17 +135,17 @@ END
TACTIC EXTEND firstorder
[ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
- [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
+ [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
END
TACTIC EXTEND gintuition
[ "gintuition" tactic_opt(t) ] ->
- [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
+ [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
END
open Proofview.Notations
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fdc5c2bbd..7a3d7936a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -17,15 +17,14 @@ open Quote
DECLARE PLUGIN "quote_plugin"
let loc = Loc.ghost
-let cont = (loc, Id.of_string "cont")
-let x = (loc, Id.of_string "x")
+let cont = Id.of_string "cont"
+let x = Id.of_string "x"
-let make_cont (k : glob_tactic_expr) (c : Constr.t) =
+let make_cont (k : Genarg.Val.t) (c : Constr.t) =
let c = Tacinterp.Value.of_constr c in
- let tac = TacCall (loc, ArgVar cont, [Reference (ArgVar x)]) in
- let tac = TacLetIn (false, [(cont, Tacexp k)], TacArg (loc, tac)) in
- let ist = { lfun = Id.Map.singleton (snd x) c; extra = TacStore.empty; } in
- Tacinterp.eval_tactic_ist ist tac
+ let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
+ let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
+ Tacinterp.eval_tactic_ist ist (TacArg (loc, tac))
TACTIC EXTEND quote
[ "quote" ident(f) ] -> [ quote f [] ]
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a67cc7cb8..37a895976 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -176,19 +176,16 @@ let ltac_call tac (args:glob_tactic_arg list) =
let ltac_lcall tac args =
TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
-let ltac_letin (x, e1) e2 =
- TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2)
-
-let ltac_apply (f:glob_tactic_expr) (args: Tacinterp.Value.t list) =
+let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
let x = Reference (ArgVar (Loc.ghost, id)) in
(succ i, x :: vars, Id.Map.add id arg lfun)
in
let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+ let lfun = Id.Map.add (Id.of_string "F") f lfun in
let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
- Tacinterp.eval_tactic_ist ist
- (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args))
+ Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
let ltac_record flds =
TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
@@ -774,7 +771,7 @@ let ltac_ring_structure e =
[req;sth;ext;morph;th;cst_tac;pow_tac;
lemma1;lemma2;pretac;posttac]
-let ring_lookup (f:glob_tactic_expr) lH rl t =
+let ring_lookup (f : Value.t) lH rl t =
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
@@ -1046,7 +1043,7 @@ let ltac_field_structure e =
[req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
field_simpl_eq_in_ok;cond_ok;pretac;posttac]
-let field_lookup (f:glob_tactic_expr) lH rl t =
+let field_lookup (f : Value.t) lH rl t =
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 4bd3383d6..07a1ae833 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr
val from_name : ring_info Spmap.t ref
val ring_lookup :
- glob_tactic_expr ->
+ Genarg.Val.t ->
constr list ->
constr list -> constr -> unit Proofview.tactic
@@ -73,6 +73,6 @@ val add_field_theory :
val field_from_name : field_info Spmap.t ref
val field_lookup :
- glob_tactic_expr ->
+ Genarg.Val.t ->
constr list ->
constr list -> constr -> unit Proofview.tactic
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c00036bb3..ed85b2147 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -61,7 +61,7 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
let genarg_pprule = ref String.Map.empty
@@ -106,6 +106,8 @@ module Make
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
+ let pr_value _ _ = str "(* FIXME *)"
+
let pr_with_occurrences pr (occs,c) =
match occs with
| AllOccurrences ->
@@ -1308,10 +1310,10 @@ module Make
pr_generic = Genprint.generic_top_print;
pr_extend = pr_extend_rec
(pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
+ pr_value pr_constr_pattern;
pr_alias = pr_alias
(pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
+ pr_value pr_constr_pattern;
}
in
make_pr_tac
@@ -1330,7 +1332,7 @@ module Make
let pr_top_generic env = pr_top_generic_rec
(pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern
+ pr_value pr_constr_pattern
let pr_raw_extend env = pr_raw_extend_rec
pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 2bc64509f..31a5a5d4a 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
val declare_extra_genarg_pprule :
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7c206d95c..7df845e4b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -47,7 +47,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
val wit_by_arg_tac :
(raw_tactic_expr option,
glob_tactic_expr option,
- glob_tactic_expr option) Genarg.genarg_type
+ Genarg.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
(int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cdf29e4c6..151949c3c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -44,7 +44,7 @@ let with_delayed_uconstr ist c tac =
let replace_in_clause_maybe_by ist c1 c2 cl tac =
with_delayed_uconstr ist c1
- (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
+ (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
let replace_term ist dir_opt c cl =
with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
@@ -237,7 +237,7 @@ TACTIC EXTEND autorewrite
[ auto_multi_rewrite l ( cl) ]
| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
[
- auto_multi_rewrite_with (Tacinterp.eval_tactic t) l cl
+ auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
]
END
@@ -245,14 +245,14 @@ TACTIC EXTEND autorewrite_star
| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
[ auto_multi_rewrite ~conds:AllMatches l cl ]
| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
- [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ]
+ [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ]
END
(**********************************************************************)
(* Rewrite star *)
-let rewrite_star ist clause orient occs c (tac : glob_tactic_expr option) =
- let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
+let rewrite_star ist clause orient occs c (tac : Val.t option) =
+ let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
with_delayed_uconstr ist c
(fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
@@ -512,12 +512,12 @@ let add_transitivity_lemma left lem =
(* Vernacular syntax *)
TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.eval_tactic tac) ]
+| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ]
| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ]
END
TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.eval_tactic tac) ]
+| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ]
| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ]
END
@@ -883,7 +883,7 @@ END
TACTIC EXTEND unshelve
| [ "unshelve" tactic1(t) ] ->
[
- Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
+ Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
Proofview.Unsafe.tclSETGOALS (gls @ ogls)
]
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index e0c1f671f..766593543 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -14,7 +14,7 @@ open Class_tactics
DECLARE PLUGIN "g_class"
TACTIC EXTEND progress_evars
- [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ]
+ [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
END
(** Options: depth, debug and transparency settings. *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2af21fac6..cb4a9f320 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1458,7 +1458,7 @@ and tactic_of_value ist vle =
| (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
- eval_tactic ist tac
+ tactic_of_value ist tac
else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
(* Interprets the clauses of a recursive LetIn *)
@@ -2232,10 +2232,7 @@ let () =
()
let () =
- let interp ist tac =
- let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
- Ftactic.return (TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f)))
- in
+ let interp ist tac = Ftactic.return (Value.of_closure ist tac) in
Geninterp.register_interp0 wit_tactic interp
let () =
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 89d34231b..c5da3494c 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -88,6 +88,8 @@ val eval_tactic : glob_tactic_expr -> unit Proofview.tactic
val eval_tactic_ist : interp_sign -> glob_tactic_expr -> unit Proofview.tactic
(** Same as [eval_tactic], but with the provided [interp_sign]. *)
+val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
+
(** Globalization + interpretation *)
val interp_tac_gen : value Id.Map.t -> Id.t list ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4dc5388ee..5485f344b 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -352,7 +352,6 @@ let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff"
let intuition_gen ist flags tac =
Proofview.Goal.enter { enter = begin fun gl ->
- let tac = Value.of_closure ist tac in
let env = Proofview.Goal.env gl in
let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in
let glb_intuition = Tacintern.glob_tactic_env vars env intuition in
@@ -360,8 +359,9 @@ let intuition_gen ist flags tac =
end }
let tauto_intuitionistic flags =
+ let fail = Value.of_closure (default_ist ()) <:tactic<fail>> in
Proofview.tclORELSE
- (intuition_gen (default_ist ()) flags <:tactic<fail>>)
+ (intuition_gen (default_ist ()) flags fail)
begin function (e, info) -> match e with
| Refiner.FailError _ | UserError _ ->
Tacticals.New.tclZEROMSG (str "tauto failed.")
@@ -395,7 +395,8 @@ let tauto_gen flags =
let default_intuition_tac =
let tac _ _ = Auto.h_auto None [] None in
- register_tauto_tactic tac "auto_with"
+ let tac = register_tauto_tactic tac "auto_with" in
+ Value.of_closure (default_ist ()) tac
(* This is the uniform mode dealing with ->, not, iff and types isomorphic to
/\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:09:47 +0000