diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 67 | ||||
| -rw-r--r-- | tactics/auto.mli | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 22 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 136 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 34 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 75 | ||||
| -rw-r--r-- | tactics/eauto.mli | 6 | ||||
| -rw-r--r-- | tactics/elim.ml | 18 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 9 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 21 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 8 | ||||
| -rw-r--r-- | tactics/equality.ml | 168 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 15 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 71 | ||||
| -rw-r--r-- | tactics/ftactic.mli | 6 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 38 | ||||
| -rw-r--r-- | tactics/leminv.ml | 5 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 46 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 8 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 4 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 28 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 368 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 8 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 26 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 66 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 10 | ||||
| -rw-r--r-- | tactics/tactics.ml | 930 | ||||
| -rw-r--r-- | tactics/tactics.mli | 12 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 184 |
30 files changed, 1315 insertions, 1084 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index a6b53d76cc..4fb4b32632 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -76,7 +76,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = (** [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in (** Still, we need to update the universes *) let clenv, c = @@ -96,11 +96,11 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = in clenv, c let unify_resolve poly flags ((c : raw_hint), clenv) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in Clenvtac.clenv_refine false clenv - end + end } let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h @@ -119,10 +119,12 @@ let exact poly (c,clenv) = let ctx = Evd.evar_universe_context clenv.evd in ctx, c in - Proofview.Goal.enter begin fun gl -> - let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c') - end + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let sigma = Evd.merge_universe_context sigma ctx in + Sigma.Unsafe.of_pair (exact_check c', sigma) + end } (* Util *) @@ -150,11 +152,12 @@ let conclPattern concl pat tac = with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "conclPattern") in - Proofview.Goal.enter (fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in constr_bindings env sigma >>= fun constr_bindings -> - Hook.get forward_interp_tactic constr_bindings tac) + Hook.get forward_interp_tactic constr_bindings tac + end } (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -319,8 +322,8 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + ( Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in @@ -328,15 +331,15 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) - end) + end }) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE (trivial_resolve dbg mod_delta db_list local_db concl))) - end + end } and my_find_search_nodelta db_list local_db hdc concl = List.map (fun hint -> (None,hint)) @@ -413,26 +416,26 @@ and trivial_resolve dbg mod_delta db_list local_db cl = "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in let d = mk_trivial_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let full_trivial ?(debug=Off) lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in let d = mk_trivial_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let gen_trivial ?(debug=Off) lems = function | None -> full_trivial ~debug lems @@ -457,7 +460,7 @@ let possible_resolve dbg mod_delta db_list local_db cl = let extend_local_db decl db gl = let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db (* Introduce an hypothesis, then call the continuation tactic [kont] @@ -465,10 +468,10 @@ let extend_local_db decl db gl = let intro_register dbg kont db = Tacticals.New.tclTHEN (dbg_intro dbg) - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let extend_local_db decl db = extend_local_db decl db gl in Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)) - end) + end }) (* n is the max depth of search *) (* local_db contains the local Hypotheses *) @@ -481,14 +484,14 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.enter begin fun gl -> + ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) (possible_resolve d mod_delta db_list local_db concl)) - end)) + end })) end [] in search d n local_db @@ -496,15 +499,15 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in let d = mk_auto_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let delta_auto = if Flags.profile then @@ -519,15 +522,15 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in let d = mk_auto_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let full_auto ?(debug=Off) n = delta_full_auto ~debug false n let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n diff --git a/tactics/auto.mli b/tactics/auto.mli index cae180ce76..1132478aac 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,11 +26,9 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - [ `NF ] Proofview.Goal.t -> clausenv * constr + ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic - val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 3a9d40de03..e4ff1c9069 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -18,6 +18,8 @@ open Util open Tacexpr open Mod_subst open Locus +open Sigma.Notations +open Proofview.Notations (* Rewriting rules *) type rew_rule = { rew_lemma: constr; @@ -91,14 +93,16 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in - let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl -> + let try_rewrite dir ctx c tc = + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (general_rewrite_maybe_in dir c' tc) - ) in + let tac = general_rewrite_maybe_in dir c' tc in + Sigma.Unsafe.of_pair (tac, sigma) + end } in let lrul = List.map (fun h -> let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in @@ -120,7 +124,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in let general_rewrite_in id = @@ -163,7 +167,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = (List.fold_left (fun tac bas -> Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) idl - end + end } let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] @@ -188,10 +192,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids - end) + end }) let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT()) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f3a4863444..4f0ffa024e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -39,6 +39,10 @@ let typeclasses_dependency_order = ref false let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d let get_typeclasses_dependency_order () = !typeclasses_dependency_order +let typeclasses_iterative_deepening = ref false +let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d +let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening + open Goptions let _ = @@ -59,6 +63,15 @@ let _ = optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "use iterative deepening strategy"; + optkey = ["Typeclasses";"Iterative";"Deepening"]; + optread = get_typeclasses_iterative_deepening; + optwrite = set_typeclasses_iterative_deepening; } + (** We transform the evars that are concerned by this resolution (according to predicate p) into goals. Invariant: function p only manipulates and returns undefined evars *) @@ -127,17 +140,17 @@ let rec eq_constr_mod_evars x y = | _, _ -> compare_constr eq_constr_mod_evars x y let progress_evars t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.nf_enter begin fun gl' -> + Proofview.Goal.nf_enter { enter = begin fun gl' -> let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars concl newconcl then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") else Proofview.tclUNIT () - end + end } in t <*> check - end + end } let e_give_exact flags poly (c,clenv) gl = @@ -145,23 +158,25 @@ let e_give_exact flags poly (c,clenv) gl = let c, gl = if poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in - let clenv' = connect_clenv gl clenv' in + let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in let c = Vars.subst_univs_level_constr subst c in - c, {gl with sigma = clenv'.evd} + c, {gl with sigma = evd} else c, gl in let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl -let unify_e_resolve poly flags (c,clenv) gls = +let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in Clenvtac.clenv_refine true ~with_classes:false clenv' + end } -let unify_resolve poly flags (c,clenv) gls = +let unify_resolve poly flags = { enter = begin fun gls (c,clenv) -> let clenv', _ = connect_hint_clenv poly c clenv gls in let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in Clenvtac.clenv_refine false ~with_classes:false clenv' + end } let clenv_of_prods poly nprods (c, clenv) gl = let (c, _, _) = c in @@ -175,16 +190,17 @@ let clenv_of_prods poly nprods (c, clenv) gl = else None let with_prods nprods poly (c, clenv) f = - Proofview.Goal.nf_enter (fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> match clenv_of_prods poly nprods (c, clenv) gl with | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") - | Some clenv' -> f (c, clenv') gl) + | Some clenv' -> f.enter gl (c, clenv') + end } (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db db_list local_db goal = let tacl = - Eauto.registered_e_assumption :: + Proofview.V82.of_tactic Eauto.registered_e_assumption :: (tclTHEN (Proofview.V82.of_tactic Tactics.intro) (function g'-> let d = pf_last_hyp g' in @@ -267,7 +283,8 @@ type autoinfo = { hints : hint_db; is_evar: existential_key option; auto_path : global_reference option list; auto_cut : hints_path } type autogoal = goal * autoinfo -type 'ans fk = unit -> 'ans +type failure = NotApplicable | ReachedLimit +type 'ans fk = failure -> 'ans type ('a,'ans) sk = 'a -> 'ans fk -> 'ans type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } @@ -282,7 +299,7 @@ type 'a optionk = | Somek of 'a * 'a optionk fk type ('a,'b) optionk2 = - | Nonek2 + | Nonek2 of failure | Somek2 of 'a * 'b * ('a,'b) optionk2 fk let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) = @@ -364,7 +381,7 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : ' with e when catchable e -> None in match res with | Some gls -> sk (f gls hints) fk - | None -> fk () } + | None -> fk NotApplicable } let intro_tac : atac = lift_tactic (Proofview.V82.of_tactic Tactics.intro) @@ -385,8 +402,19 @@ let normevars_tac : atac = let info' = { info with auto_last_tac = lazy (str"normevars") } in sk {it = [gl', info']; sigma = sigma';} fk } +let merge_failures x y = + match x, y with + | _, ReachedLimit + | ReachedLimit, _ -> ReachedLimit + | NotApplicable, NotApplicable -> NotApplicable + let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } + { skft = fun sk fk gls -> x.skft sk + (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } + +let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = + { skft = fun sk fk gls -> x.skft sk + (fun f -> (y f).skft sk fk gls) gls } let is_Prop env sigma concl = let ty = Retyping.get_type_of env sigma concl in @@ -463,7 +491,7 @@ let hints_tac hints = in g, info) 1 newgls in let glsv = {it = gls'; sigma = s';} in let fk' = - (fun () -> + (fun e -> let do_backtrack = if unique then occur_existential concl else if info.unique then true @@ -471,22 +499,25 @@ let hints_tac hints = needs_backtrack env s' info.is_evar concl else true in + let e' = match foundone with None -> e | Some e' -> merge_failures e e' in if !typeclasses_debug then msg_debug ((if do_backtrack then str"Backtracking after " else str "Not backtracking after ") ++ Lazy.force pp); - if do_backtrack then aux (succ i) true tl - else fk ()) + if do_backtrack then aux (succ i) (Some e') tl + else fk e') in sk glsv fk') | [] -> - if not foundone && !typeclasses_debug then + if foundone == None && !typeclasses_debug then msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); - fk () - in aux 1 false poss } + match foundone with + | Some e -> fk e + | None -> fk NotApplicable + in aux 1 None poss } let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = let rec aux s (acc : autogoal list list) fk = function @@ -509,11 +540,11 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk | [] -> Somek2 (List.rev acc, s, fk) in fun {it = gls; sigma = s; } fk -> let rec aux' = function - | Nonek2 -> fk () + | Nonek2 e -> fk e | Somek2 (res, s', fk') -> let goals' = List.concat res in - sk {it = goals'; sigma = s'; } (fun () -> aux' (fk' ())) - in aux' (aux s [] (fun () -> Nonek2) gls) + sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) + in aux' (aux s [] (fun e -> Nonek2 e) gls) let then_tac (first : atac) (second : atac) : atac = { skft = fun sk fk -> first.skft (then_list second sk) fk } @@ -528,16 +559,38 @@ let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res gl (fun _ -> Nonek) -let fail_tac : atac = - { skft = fun sk fk _ -> fk () } +let fail_tac reason : atac = + { skft = fun sk fk _ -> fk reason } let rec fix (t : 'a tac) : 'a tac = then_tac t { skft = fun sk fk -> (fix t).skft sk fk } let rec fix_limit limit (t : 'a tac) : 'a tac = - if Int.equal limit 0 then fail_tac + if Int.equal limit 0 then fail_tac ReachedLimit else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } +let fix_iterative' t = + let rec aux depth = + { skft = fun sk fk gls -> + (fix_limit depth t).skft sk + (function NotApplicable as e -> fk e + | ReachedLimit -> (aux (succ depth)).skft sk fk gls) gls } + in aux 1 + +let fix_iterative t = + let rec aux depth = + or_else_tac (fix_limit depth t) + (function + | NotApplicable as e -> fail_tac e + | ReachedLimit -> aux (succ depth)) + in aux 1 + +let fix_iterative_limit limit (t : 'a tac) : 'a tac = + let rec aux depth = + if Int.equal depth limit then fail_tac ReachedLimit + else or_tac (fix_limit depth t) { skft = fun sk fk -> (aux (succ depth)).skft sk fk } + in aux 1 + let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) cut ev g = let hints = make_autogoal_hints only_classes ~st g in (g.it, { hints = hints ; is_evar = ev; unique = unique; @@ -581,16 +634,14 @@ let eauto_tac hints = then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) let eauto_tac ?limit hints = - match limit with - | None -> fix (eauto_tac hints) - | Some limit -> fix_limit limit (eauto_tac hints) - -let eauto ?(only_classes=true) ?st ?limit hints g = - let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in - match run_tac (eauto_tac ?limit hints) gl with - | None -> raise Not_found - | Some {it = goals; sigma = s; } -> - {it = List.map fst goals; sigma = s;} + if get_typeclasses_iterative_deepening () then + match limit with + | None -> fix_iterative (eauto_tac hints) + | Some limit -> fix_iterative_limit limit (eauto_tac hints) + else + match limit with + | None -> fix (eauto_tac hints) + | Some limit -> fix_limit limit (eauto_tac hints) let real_eauto ?limit unique st hints p evd = let res = @@ -600,7 +651,7 @@ let real_eauto ?limit unique st hints p evd = | None -> evd | Some (evd', fk) -> if unique then - (match get_result (fk ()) with + (match get_result (fk NotApplicable) with | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" | None -> evd') else evd' @@ -609,6 +660,13 @@ let resolve_all_evars_once debug limit unique p evd = let db = searchtable_map typeclasses_db in real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd +let eauto ?(only_classes=true) ?st ?limit hints g = + let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in + match run_tac (eauto_tac ?limit hints) gl with + | None -> raise Not_found + | Some {it = goals; sigma = s; } -> + {it = List.map fst goals; sigma = s;} + (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, it should not be shared, but only used locally. *) @@ -846,5 +904,5 @@ let autoapply c i gl = (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in + let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),ce) } in Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 22f218b4fb..5ccf4a9e4f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -13,6 +13,8 @@ open Tactics open Coqlib open Reductionops open Misctypes +open Sigma.Notations +open Proofview.Notations (* Absurd *) @@ -22,18 +24,20 @@ let mk_absurd_proof t = mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) let absurd c = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map sigma in let j = Retyping.get_judgment_of env sigma c in let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let t = j.Environ.utj_val in + let tac = Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; elim_type (build_coq_False ()); Simple.apply (mk_absurd_proof t) - ] - end + ] in + Sigma.Unsafe.of_pair (tac, sigma) + end } let absurd c = absurd c @@ -45,14 +49,14 @@ let filter_hyp f tac = | [] -> Proofview.tclZERO Not_found | (id,_,t)::rest when f t -> tac id | _::rest -> seek rest in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek hyps - end + end } let contradiction_context = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") @@ -64,11 +68,11 @@ let contradiction_context = else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> (Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) - end) + end }) begin function (e, info) -> match e with | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e @@ -77,7 +81,7 @@ let contradiction_context = in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek_neg hyps - end + end } let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with @@ -87,8 +91,8 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in @@ -110,7 +114,7 @@ let contradiction_term (c,lbind as cl) = | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end - end + end } let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 20a7448dcb..2241fb821c 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -28,33 +28,41 @@ open Misctypes open Locus open Locusops open Hints +open Proofview.Notations DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state -let e_give_exact ?(flags=eauto_unif_flags) c gl = - let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in +let e_give_exact ?(flags=eauto_unif_flags) c = + Proofview.Goal.nf_enter { enter = begin fun gl -> + let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl - else Proofview.V82.of_tactic (exact_check c) gl + Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) + else exact_check c + end } let assumption id = e_give_exact (mkVar id) -let e_assumption gl = - tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl +let e_assumption = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) + end } TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ] +| [ "eassumption" ] -> [ e_assumption ] END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ] +| [ "eexact" constr(c) ] -> [ e_give_exact c ] END -let registered_e_assumption gl = - tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl) - (pf_ids_of_hyps gl)) gl +let registered_e_assumption = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) + (Tacmach.New.pf_ids_of_hyps gl)) + end } (************************************************************************) (* PROLOG tactic *) @@ -83,7 +91,7 @@ let one_step l gl = [Proofview.V82.of_tactic Tactics.intro] @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl))) @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l) - @ (List.map assumption (pf_ids_of_hyps gl)) + @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) let rec prolog l n gl = if n <= 0 then error "prolog - failure"; @@ -119,15 +127,14 @@ open Unification let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) let unify_e_resolve poly flags (c,clenv) = - Proofview.Goal.nf_enter begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv', c = connect_hint_clenv poly c clenv gl in Proofview.V82.tactic (fun gls -> let clenv' = clenv_unique_resolver ~flags clenv' gls in tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) - end + end } let hintmap_of hdc concl = match hdc with @@ -143,19 +150,21 @@ let e_exact poly flags (c,clenv) = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) - -let rec e_trivial_fail_db db_list local_db goal = + +let rec e_trivial_fail_db db_list local_db = + let next = Proofview.Goal.nf_enter { enter = begin fun gl -> + let d = Tacmach.New.pf_last_hyp gl in + let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in + e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db) + end } in + Proofview.Goal.enter { enter = begin fun gl -> let tacl = registered_e_assumption :: - (tclTHEN (Proofview.V82.of_tactic Tactics.intro) - (function g'-> - let d = pf_last_hyp g' in - let hintl = make_resolve_hyp (pf_env g') (project g') d in - (e_trivial_fail_db db_list - (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: - (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + (Tacticals.New.tclTHEN Tactics.intro next) :: + (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) in - tclFIRST (List.map tclCOMPLETE tacl) goal + Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) + end } and e_my_find_search db_list local_db hdc concl = let hint_of_db = hintmap_of hdc concl in @@ -174,14 +183,14 @@ and e_my_find_search db_list local_db hdc concl = let tac = function | Res_pf (term,cl) -> unify_resolve poly st (term,cl) | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl)) + | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> - Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl))) - (e_trivial_fail_db db_list local_db)) + Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) + (e_trivial_fail_db db_list local_db) | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_hint t tac) in + let tac = run_hint t tac in (tac, lazy (pr_hint t))) in List.map tac_of_hint hintl @@ -234,7 +243,7 @@ module SearchProblem = struct | [] -> [] | (tac, cost, pptac) :: tacl -> try - let lgls = apply_tac_list tac glls in + let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls, cost, pptac) :: aux tacl @@ -272,7 +281,7 @@ module SearchProblem = struct prev = ps; local_lemmas = s.local_lemmas}) l in let intro_tac = - let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in + let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in List.map (fun (lgls, cost, pp) -> let g' = first_goal lgls in @@ -567,7 +576,7 @@ let unfold_head env (ids, csts) c = in aux c let autounfold_one db cl = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let st = @@ -586,7 +595,7 @@ let autounfold_one db cl = | Some hyp -> change_in_hyp None (make_change_arg c') hyp | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") - end + end } (* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) (* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 7073e8a2b8..b55c70fa12 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -21,11 +21,11 @@ val wit_auto_using : Genarg.genarg_type -val e_assumption : tactic +val e_assumption : unit Proofview.tactic -val registered_e_assumption : tactic +val registered_e_assumption : unit Proofview.tactic -val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic +val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list -> hint_db_name list option -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml index 4841d2c252..d3aa160925 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -84,7 +84,7 @@ let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) let general_decompose recognizer c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let typc = type_of c in tclTHENS (cut typc) @@ -93,11 +93,11 @@ let general_decompose recognizer c = (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> Proofview.V82.tactic (clear [id])))); Proofview.V82.tactic (exact_no_check c) ] - end + end } let head_in indl t gl = let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in try let ity,_ = if !up_to_delta @@ -107,10 +107,10 @@ let head_in indl t gl = with Not_found -> false let decompose_these c l = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in general_decompose (fun (_,t) -> head_in indl t gl) c - end + end } let decompose_and c = general_decompose @@ -138,7 +138,7 @@ let induction_trailer abs_i abs_j bargs = (tclDO (abs_j - abs_i) intro) (onLastHypId (fun id -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = @@ -156,11 +156,11 @@ let induction_trailer abs_i abs_j bargs = (tclTHENLIST [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids)); simple_elimination (mkVar id)]) - end + end } )) let double_ind h1 h2 = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in let abs = @@ -173,7 +173,7 @@ let double_ind h1 h2 = (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) - end + end } let h_double_induction = double_ind diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 8a6d93cf7c..59cce19ef3 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -18,6 +18,7 @@ open Indrec open Declarations open Typeops open Ind_tables +open Sigma.Notations (* Induction/recursion schemes *) @@ -102,10 +103,10 @@ let rec_dep_scheme_kind_from_type = let build_case_analysis_scheme_in_type dep sort ind = let env = Global.env () in - let sigma = Evd.from_env env in - let sigma, indu = Evd.fresh_inductive_instance env sigma ind in - let sigma, c = build_case_analysis_scheme env sigma indu dep sort in - c, Evd.evar_universe_context sigma + let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in + let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in + let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep sort in + c, Evd.evar_universe_context (Sigma.to_evar_map sigma) let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 4fb76bb828..74e5e036a2 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -27,6 +27,7 @@ open Constr_matching open Hipattern open Tacmach.New open Coqlib +open Proofview.Notations (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -146,7 +147,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with intros_reflexivity; ] | a1 :: largs, a2 :: rargs -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in @@ -154,13 +155,13 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in (tclTHENS (elim_type decide) subtacs) - end + end } | _ -> invalid_arg "List.fold_right2" let solveEqBranch rectype = Proofview.tclORELSE begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -169,7 +170,7 @@ let solveEqBranch rectype = let rargs = getargs rhs and largs = getargs lhs in solveArg [] eqonleft op largs rargs - end + end } end begin function (e, info) -> match e with | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") @@ -185,7 +186,7 @@ let hd_app c = match kind_of_term c with let decideGralEquality = Proofview.tclORELSE begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app (pf_compute gl typ) in @@ -196,7 +197,7 @@ let decideGralEquality = (tclTHEN (mkBranches c1 c2) (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) - end + end } end begin function (e, info) -> match e with | PatternMatchingFailure -> @@ -207,20 +208,20 @@ let decideGralEquality = let decideEqualityGoal = tclTHEN intros decideGralEquality let decideEquality rectype = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let decide = mkGenDecideEqGoal rectype gl in (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) - end + end } (* The tactic Compare *) let compare c1 c2 = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro (tclTHEN (onLastHyp simplest_case) clear_last)); decideEquality rectype]) - end + end } diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index d08c7615a9..64a68ba6bc 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -58,6 +58,7 @@ open Namegen open Inductiveops open Ind_tables open Indrec +open Sigma.Notations let hid = Id.of_string "H" let xid = Id.of_string "X" @@ -630,9 +631,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (**********************************************************************) let build_r2l_rew_scheme dep env ind k = - let sigma, indu = Evd.fresh_inductive_instance env (Evd.from_env env) ind in - let sigma', c = build_case_analysis_scheme env sigma indu dep k in - c, Evd.evar_universe_context sigma' + let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in + let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in + let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in + c, Evd.evar_universe_context (Sigma.to_evar_map sigma) let build_l2r_rew_scheme = build_l2r_rew_scheme let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme diff --git a/tactics/equality.ml b/tactics/equality.ml index fe0ca61c66..92ebcb2724 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -40,6 +40,7 @@ open Eqschemes open Locus open Locusops open Misctypes +open Sigma.Notations open Proofview.Notations open Unification @@ -158,7 +159,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let try_occ (evd', c') = Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} in - let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in + let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = w_unify_to_subterm_all ~flags env eqclause.evd ((if l2r then c1 else c2),concl) @@ -206,10 +207,10 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_elim with_evars frzevars cls c e = - Proofview.Goal.enter begin fun gl -> - let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in + Proofview.Goal.enter { enter = begin fun gl -> + let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_conv_closed_unif_flags c in general_elim_clause with_evars flags cls c e - end + end } (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars frzevars cls rew elim = @@ -244,7 +245,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = (general_elim_clause with_evars frzevars cls c elim)) tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let instantiate_lemma concl = if not all then instantiate_lemma gl c t l l2r concl else instantiate_lemma_all frzevars gl c t l l2r concl @@ -256,7 +257,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) else tclMAP try_clause cs - end + end } (* The next function decides in particular whether to try a regular rewrite or a generalized rewrite. @@ -275,7 +276,7 @@ let jmeq_same_dom gl = function let rels, t = decompose_prod_assum t in let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in match decompose_app t with - | _, [dom1; _; dom2;_] -> is_conv env (Proofview.Goal.sigma gl) dom1 dom2 + | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2 | _ -> false (* find_elim determines which elimination principle is necessary to @@ -316,8 +317,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Safe_typing.empty_private_constants + let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + Sigma ((elim, Safe_typing.empty_private_constants), sigma, p) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -335,10 +336,10 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | Ind (ind,u) -> let c, eff = find_scheme scheme_name ind in (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let sigma, elim = - Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) + let Sigma (elim, sigma, p) = + Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, eff + Sigma ((elim, eff), sigma, p) | _ -> assert false let type_of_clause cls gl = match cls with @@ -346,17 +347,20 @@ let type_of_clause cls gl = match cls with | Some id -> pf_get_hyp_typ id gl let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in - let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> + let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in + let tac = + Proofview.tclEFFECTS effs <*> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} - end + in + Sigma (tac, sigma, p) + end } let adjust_rewriting_direction args lft2rgt = match args with @@ -379,8 +383,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac if occs != AllOccurrences then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in @@ -407,7 +411,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac | None -> Proofview.tclZERO ~info e (* error "The provided term does not end with an equality or a declared rewrite relation." *) end - end + end } let general_rewrite_ebindings = general_rewrite_ebindings_clause None @@ -469,9 +473,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let ids_of_hyps = pf_ids_of_hyps gl in Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> do_hyps_atleastonce (ids gl) - end + end } in if cl.concl_occs == NoOccurrences then do_hyps else tclIFTHENTRYELSEMUST @@ -479,25 +483,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl = do_hyps let apply_special_clear_request clear_flag f = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try - let sigma,(c,bl) = f env sigma in + let ((c, bl), sigma) = run_delayed env sigma f in apply_clear_request clear_flag (use_clear_hyp_by_default ()) c with e when catchable_exception e -> tclIDTAC - end + end } let general_multi_rewrite with_evars l cl tac = let do1 l2r f = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma,c = f env sigma in + let (c, sigma) = run_delayed env sigma f in tclWITHHOLES with_evars (general_rewrite_clause l2r with_evars ?tac c cl) sigma - end + end } in let rec doN l2r c = function | Precisely n when n <= 0 -> Proofview.tclUNIT () @@ -560,14 +564,14 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> Proofview.tclUNIT () | Some tac -> tclCOMPLETE tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let get_type_of = pf_apply get_type_of gl in let t1 = get_type_of c1 and t2 = get_type_of c2 in let evd = - if unsafe then Some (Proofview.Goal.sigma gl) + if unsafe then Some (Tacmach.New.project gl) else - try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Proofview.Goal.sigma gl)) + try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl)) with Evarconv.UnableToUnify _ -> None in match evd with @@ -586,7 +590,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = tclTHEN (apply sym) assumption; try_prove_eq ]))) - end + end } let replace c1 c2 = replace_using_leibniz onConcl c2 c1 false false None @@ -869,7 +873,7 @@ let rec build_discriminator env sigma dirn c sort = function *) let gen_absurdity id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in let hyp_typ = pf_nf_evar gl hyp_typ in if is_empty_type hyp_typ @@ -877,7 +881,7 @@ let gen_absurdity id = simplest_elim (mkVar id) else tclZEROMSG (str "Not the negation of an equality.") - end + end } (* Precondition: eq is leibniz equality @@ -933,7 +937,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in match find_positions env sigma t1 t2 with @@ -942,10 +946,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = | Inl (cpath, (_,dirn), _) -> let sort = pf_apply get_type_of gl concl in discr_positions env sigma u eq_clause cpath dirn sort - end + end } let onEquality with_evars tac (c,lbindc) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in @@ -957,11 +961,11 @@ let onEquality with_evars tac (c,lbindc) = tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') - end + end } let onNegatedEquality with_evars tac = - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match kind_of_term (hnf_constr env sigma ccl) with @@ -971,7 +975,7 @@ let onNegatedEquality with_evars tac = onEquality with_evars tac (mkVar id,NoBindings))) | _ -> tclZEROMSG (str "Not a negated primitive equality.") - end + end } let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -1097,7 +1101,7 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let rec sigrec_clausal_form siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) @@ -1240,7 +1244,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined") let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) let inject_if_homogenous_dependent_pair ty = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> try let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) @@ -1278,7 +1282,7 @@ let inject_if_homogenous_dependent_pair ty = ])] with Exit -> Proofview.tclUNIT () - end + end } (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it expands then only when the whdnf has a constructor of an inductive type @@ -1352,7 +1356,7 @@ let postInjEqTac clear_flag ipats c n = then intro_patterns_bound_to n MoveLast ipats else intro_patterns_to MoveLast ipats in tclTHEN clear_tac intro_tac - | None -> tclIDTAC + | None -> apply_clear_request clear_flag false c let injEq clear_flag ipats = let l2r = @@ -1370,7 +1374,7 @@ let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sort = pf_apply get_type_of gl (Proofview.Goal.concl gl) in let sigma = clause.evd in let env = Proofview.Goal.env gl in @@ -1382,7 +1386,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = | Inr posns -> inject_at_positions env sigma true u clause posns (ntac (clenv_value clause)) - end + end } let dEqThen with_evars ntac = function | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) @@ -1393,10 +1397,10 @@ let dEq with_evars = (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decompe_eq tac data cl = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let cl = pf_apply make_clenv_binding gl cl NoBindings in decompEqThen (fun _ -> tac) data cl - end + end } let _ = declare_intro_decomp_eq intro_decompe_eq @@ -1447,6 +1451,7 @@ let decomp_tuple_term env c t = in decomprec (mkRel 1) c t let subst_tuple_term env sigma dep_pair1 dep_pair2 b = + let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma dep_pair1 in (* We find all possible decompositions *) let decomps1 = decomp_tuple_term env dep_pair1 typ in @@ -1471,7 +1476,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Retype to get universes right *) let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in let sigma, _ = Typing.type_of env sigma body in - sigma,body,expected_goal + Sigma.Unsafe.of_pair ((body, expected_goal), sigma) (* Like "replace" but decompose dependent equalities *) (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *) @@ -1479,34 +1484,42 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* on for further iterated sigma-tuples *) let cutSubstInConcl l2r eqn = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in - let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in + let tac = tclTHENFIRST (tclTHENLIST [ - (Proofview.Unsafe.tclEVARS sigma); (change_concl typ); (* Put in pattern form *) (replace_core onConcl l2r eqn) ]) (change_concl expected) (* Put in normalized form *) - end + in + Sigma (tac, sigma, p) + end } let cutSubstInHyp l2r eqn id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in - let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in - tclTHENFIRST + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in + let tac = + tclTHENFIRST (tclTHENLIST [ - (Proofview.Unsafe.tclEVARS sigma); (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)) - end + in + Sigma (tac, sigma, p) + end } let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with @@ -1528,11 +1541,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] - end + end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) let rewriteInHyp l2r c id = rewriteClause l2r c (Some id) @@ -1558,7 +1571,7 @@ user = raise user error specific to rewrite (* Substitutions tactics (JCF) *) let unfold_body x = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let (_, xval, _) = Context.lookup_named x hyps in @@ -1575,7 +1588,7 @@ let unfold_body x = let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in tclTHENLIST [tclMAP reducth hl; reductc] end - end + end } let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && @@ -1598,7 +1611,7 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in @@ -1624,13 +1637,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) - end + end } (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one_var dep_proof_ok x = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let (_,xval,_) = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) @@ -1649,7 +1662,7 @@ let subst_one_var dep_proof_ok x = str".") with FoundHyp res -> res in subst_one dep_proof_ok x res - end + end } let subst_gen dep_proof_ok ids = tclTHEN Proofview.V82.nf_evar_goals (tclMAP (subst_one_var dep_proof_ok) ids) @@ -1671,7 +1684,7 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -let regular_subst_tactic = ref false +let regular_subst_tactic = ref true let _ = declare_bool_option @@ -1709,7 +1722,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* Second step: treat equations *) let process hyp = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let find_eq_data_decompose = find_eq_data_decompose gl in let (_,_,c) = pf_get_hyp hyp gl in @@ -1723,19 +1736,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () - end + end } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ids = find_equations gl in tclMAP process ids - end + end } else (* Old implementation, not able to manage configurations like a=b, a=t, or situations like "a = S b, b = S a", or also accidentally unfolding let-ins *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = try @@ -1752,7 +1765,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let ids = List.map_filter test hyps in let ids = List.uniquize ids in subst_gen flags.rewrite_dependent_proof ids - end + end } (* Rewrite the first assumption for which a condition holds and gives the direction of the rewrite *) @@ -1788,10 +1801,11 @@ let rewrite_assumption_cond cond_eq_term cl = with | Failure _ | UserError _ -> arec rest gl end in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in let hyps = Proofview.Goal.hyps gl in arec hyps gl - end + end } (* Generalize "subst x" to substitution of subterm appearing as an equation in the context, but not clearing the hypothesis *) diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index c3fe6b6574..4c4d745035 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -14,6 +14,8 @@ open Tacexpr open Refiner open Evd open Locus +open Sigma.Notations +open Proofview.Notations (* The instantiate tactic *) @@ -68,15 +70,18 @@ let instantiate_tac_by_name id c = let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let id = match name with | Names.Anonymous -> let id = Namegen.id_of_name_using_hdchar env typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) - | Names.Name id -> id in - let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) + | Names.Name id -> id + in + let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + let tac = (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) - end + in + Sigma (tac, sigma, p) + end } diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1d594aa7c9..92682fc7a0 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -19,8 +19,10 @@ open Tactics open Errors open Util open Evd +open Termops open Equality open Misctypes +open Sigma.Notations open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -269,7 +271,7 @@ let add_rewrite_hint bases ort t lcsr = let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = - let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in + let ctx = UState.context_set ctx in if poly then ctx else (Global.push_context_set false ctx; Univ.ContextSet.empty) in @@ -313,7 +315,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in + let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in let id = @@ -346,7 +348,7 @@ END (* Refine *) let refine_tac simple {Glob_term.closure=closure;term=term} = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = Pretyping.all_no_fail_flags in @@ -356,13 +358,17 @@ let refine_tac simple {Glob_term.closure=closure;term=term} = Pretyping.ltac_uconstrs = closure.Glob_term.untyped; Pretyping.ltac_idents = closure.Glob_term.idents; } in - let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in + let update = { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = Pretyping.understand_ltac flags env sigma lvar tycon term in + Sigma.Unsafe.of_pair (c, sigma) + end } in let refine = Proofview.Refine.refine ~unsafe:false update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> Proofview.shelve_unifiable - end + end } TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> [ refine_tac false c ] @@ -621,8 +627,9 @@ let out_arg = function | ArgArg x -> x let hResolve id c occ t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in @@ -640,10 +647,11 @@ let hResolve id c occ t = let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) + let tac = (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let hResolve_auto id c t = let rec resolve_auto n = @@ -665,8 +673,8 @@ END *) let hget_evar n = - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list concl in if List.length evl < n then @@ -675,7 +683,7 @@ let hget_evar n = let ev = List.nth evl (n-1) in let ev_type = existential_type sigma ev in change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) - end + end } TACTIC EXTEND hget_evar | [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ] @@ -694,12 +702,12 @@ END exception Found of unit Proofview.tactic let rewrite_except h = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) hyps - end + end } let refl_equal = @@ -713,27 +721,27 @@ let refl_equal = should be replaced by a call to the tactic but I don't know how to call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); - Proofview.Goal.nf_enter begin fun gl -> + [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in change_concl (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)) - end; + end }; simplest_case a] - end + end } let case_eq_intros_rewrite x = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let n = nb_prod (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let n' = nb_prod concl in @@ -742,9 +750,9 @@ let case_eq_intros_rewrite x = Tacticals.New.tclDO (n'-n-1) intro; introduction h; rewrite_except h] - end + end } ] - end + end } let rec find_a_destructable_match t = match kind_of_term t with @@ -764,15 +772,15 @@ let destauto t = with Found tac -> tac let destauto_in id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype - end + end } TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.nf_enter (fun gl -> destauto (Proofview.Goal.concl gl)) ] +| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END @@ -780,10 +788,11 @@ END (* ********************************************************************* *) let eq_constr x y = - Proofview.Goal.enter (fun gl -> - let evd = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let evd = Tacmach.New.project gl in if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () - else Tacticals.New.tclFAIL 0 (str "Not equal")) + else Tacticals.New.tclFAIL 0 (str "Not equal") + end } TACTIC EXTEND constr_eq | [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] @@ -994,14 +1003,14 @@ TACTIC EXTEND guard END let decompose l c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let to_ind c = if isInd c then Univ.out_punivs (destInd c) else error "not an inductive type" in let l = List.map to_ind l in Elim.h_decompose l c - end + end } TACTIC EXTEND decompose | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli index 4835156748..4496499229 100644 --- a/tactics/ftactic.mli +++ b/tactics/ftactic.mli @@ -37,12 +37,14 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t +val nf_enter : (([ `NF ], 'r) Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal. The resulting tactic is focussed. *) +(** FIXME: Should be polymorphic over the stage. *) -val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t +val enter : (([ `LZ ], 'r) Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) +(** FIXME: Should be polymorphic over the stage. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 27d25056e1..281e6b9bb9 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -119,11 +119,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr -> +val find_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) @@ -144,7 +144,7 @@ val is_matching_sigma : constr -> bool val match_eqdec : constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr) +val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) val is_matching_not : constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index ef115aea0e..ed1a627956 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -27,6 +27,7 @@ open Elim open Equality open Misctypes open Tacexpr +open Sigma.Notations open Proofview.Notations let clear hyps = Proofview.V82.tactic (clear hyps) @@ -269,14 +270,14 @@ Nota: with Inversion_clear, only four useless hypotheses let generalizeRewriteIntros as_mode tac depids id = Proofview.tclENV >>= fun env -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let dids = dependent_hyps env id depids gl in let reintros = if as_mode then intros_replacing else intros_possibly_replacing in (tclTHENLIST [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) reintros (ids_of_named_context dids)]) - end + end } let error_too_many_names pats = let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in @@ -284,10 +285,10 @@ let error_too_many_names pats = tclZEROMSG ~loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c env Evd.empty)))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (fst (run_delayed env Evd.empty c)))) pats ++ str ".") -let rec get_names (allow_conj,issimple) (loc,pat as x) = match pat with +let get_names (allow_conj,issimple) (loc, pat as x) = match pat with | IntroNaming IntroAnonymous | IntroForthcoming _ -> error "Anonymous pattern not allowed for inversion equations." | IntroNaming (IntroFresh _) -> @@ -338,7 +339,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in let substHypIfVariable tac id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in @@ -346,7 +347,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 | _ -> tac id - end + end } in let deq_trailer id clear_flag _ neqns = assert (clear_flag == None); @@ -373,7 +374,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = id let nLastDecls i tac = - Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i)) + Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end } (* Introduction of the equations on arguments othin: discriminates Simple Inversion, Inversion and Inversion_clear @@ -381,7 +382,7 @@ let nLastDecls i tac = Some thin: the equations are rewritten, and cleared if thin is true *) let rewrite_equations as_mode othin neqns names ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in let avoid = if as_mode then List.map pi1 nodepids else [] in @@ -414,7 +415,7 @@ let rewrite_equations as_mode othin neqns names ba = [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids)]) - end + end } let interp_inversion_kind = function | SimpleInversion -> None @@ -431,8 +432,9 @@ let rewrite_equations_tac as_mode othin id neqns names ba = tac let raw_inversion inv_kind id status names = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in @@ -457,11 +459,11 @@ let raw_inversion inv_kind id status names = in let refined id = let prf = mkApp (mkVar id, args) in - Proofview.Refine.refine (fun h -> h, prf) + Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } in let neqns = List.length realargs in let as_mode = names != None in - tclTHEN (Proofview.Unsafe.tclEVARS sigma) + let tac = (tclTHENS (assert_before Anonymous cut_concl) [case_tac names @@ -469,7 +471,9 @@ let raw_inversion inv_kind id status names = (rewrite_equations_tac as_mode inv_kind id neqns)) (Some elim_predicate) ind (c, t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with @@ -511,12 +515,12 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * back to their places in the hyp-list. *) let invIn k names ids id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in let nb_prod_init = nb_prod concl in let intros_replace_ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in let nb_of_new_hyp = nb_prod concl - (List.length hyps + nb_prod_init) @@ -525,7 +529,7 @@ let invIn k names ids id = intros_replacing ids else tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) - end + end } in Proofview.tclORELSE (tclTHENLIST @@ -533,7 +537,7 @@ let invIn k names ids id = inversion k NoDep names id; intros_replace_ids]) (wrap_inv_error id) - end + end } let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 8ca622171f..75e69bc091 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,6 +27,7 @@ open Declare open Tacticals.New open Tactics open Decl_kinds +open Proofview.Notations let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ @@ -269,7 +270,7 @@ let lemInv id c gls = let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id let lemInvIn id c ids = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let intros_replace_ids = let concl = Proofview.Goal.concl gl in @@ -281,7 +282,7 @@ let lemInvIn id c ids = in ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c))) (intros_replace_ids))) - end + end } let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a230ea251a..2dfebc9a3c 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -34,6 +34,8 @@ open Elimschemes open Environ open Termops open Libnames +open Sigma.Notations +open Proofview.Notations (** Typeclass-based generalized rewriting. *) @@ -84,7 +86,9 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let s = Typeclasses.set_resolvable Evd.Store.empty false in - let evd', t = Evarutil.new_evar ~store:s env evd t in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in + let evd' = Sigma.to_evar_map evd' in let ev, _ = destEvar t in (evd', Evar.Set.add ev cstrs), t @@ -1498,7 +1502,7 @@ let rec insert_dependent env decl accu hyps = match hyps with insert_dependent env decl (ndecl :: accu) rem let assert_replacing id newt tac = - let prf = Proofview.Goal.nf_enter begin fun gl -> + let prf = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ctx = Environ.named_context env in @@ -1508,14 +1512,14 @@ let assert_replacing id newt tac = | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Proofview.Refine.refine ~unsafe:false begin fun sigma -> - let sigma, ev = Evarutil.new_evar env' sigma concl in - let sigma, ev' = Evarutil.new_evar env sigma newt in + Proofview.Refine.refine ~unsafe:false { run = begin fun sigma -> + let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in + let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map (n, _, _) = if Id.equal n id then ev' else mkVar n in let (e, _) = destEvar ev in - sigma, mkEvar (e, Array.map_of_list map nc) - end - end in + Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q) + end } + end } in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = @@ -1533,7 +1537,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match clause, prf with | Some id, Some p -> - let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1541,14 +1545,14 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = convert_hyp_no_check (id, None, newt) | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let make sigma = - let (sigma, ev) = Evarutil.new_evar env sigma newt in - sigma, mkApp (p, [| ev |]) - in + let make = { run = begin fun sigma -> + let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in + Sigma (mkApp (p, [| ev |]), sigma, q) + end } in Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls - end + end } | None, None -> Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast @@ -1559,10 +1563,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = | None -> Proofview.tclUNIT () | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ty = match clause with | None -> concl | Some id -> Environ.named_type id env @@ -1587,7 +1591,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) - end + end } let tactic_init_setoid () = try init_setoid (); tclIDTAC @@ -2034,9 +2038,9 @@ let not_declared env ty rel = str ty ++ str" relation. Maybe you need to require the Setoid library") let setoid_proof ty fn fallback = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in Proofview.tclORELSE begin @@ -2063,7 +2067,7 @@ let setoid_proof ty fn fallback = | e' -> Proofview.tclZERO ~info e' end end - end + end } let tac_open ((evm,_), c) tac = Proofview.V82.tactic diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 09a98bc8cc..c1e4d72e38 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -49,7 +49,7 @@ let pr_tacname t = let tac_tab = ref MLTacMap.empty -let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = +let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = let () = if MLTacMap.mem s !tac_tab then if overwrite then @@ -60,9 +60,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic s = +let interp_ml_tactic { mltac_name = s; mltac_index = i } = try - MLTacMap.find s !tac_tab + let tacs = MLTacMap.find s !tac_tab in + let () = if Array.length tacs <= i then raise Not_found in + tacs.(i) with Not_found -> Errors.errorlabstrm "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 2df6bb04a2..47d9efda57 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -64,8 +64,8 @@ type ml_tactic = typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic (** Type of external tactics, used by [TacML]. *) -val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit +val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 1778221b02..ac1229f2f7 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -672,7 +672,7 @@ and intern_tactic_seq onlytac ist = function and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with | TacCall _ | Reference _ - | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) + | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) @@ -709,13 +709,6 @@ and intern_tacarg strict onlytac ist = function | TacGeneric arg -> let (_, arg) = Genintern.generic_intern ist arg in TacGeneric arg - | TacDynamic(loc,t) as x -> - if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x - else if Dyn.has_tag t "constr" then - if onlytac then error_tactic_expected loc else x - else - let tag = Dyn.tag t in - anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">") (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist = function @@ -746,16 +739,8 @@ and intern_genarg ist x = map_raw wit_constr intern_constr ist x | ConstrMayEvalArgType -> map_raw wit_constr_may_eval intern_constr_may_eval ist x - | QuantHypArgType -> - map_raw wit_quant_hyp intern_quantified_hypothesis ist x - | RedExprArgType -> - map_raw wit_red_expr intern_red_expr ist x | OpenConstrArgType -> map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x - | ConstrWithBindingsArgType -> - map_raw wit_constr_with_bindings intern_constr_with_bindings ist x - | BindingsArgType -> - map_raw wit_bindings intern_bindings ist x | ListArgType _ -> let list_unpacker wit l = let map x = @@ -855,10 +840,13 @@ let () = let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); - Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)) - -let () = - Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)) + Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); + Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); + Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); + Genintern.register_intern0 wit_red_expr (lift intern_red_expr); + Genintern.register_intern0 wit_bindings (lift intern_bindings); + Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings); + () (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 59420e4e01..6ac16bd76a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -40,6 +40,7 @@ open Misctypes open Locus open Tacintern open Taccoerce +open Sigma.Notations open Proofview.Notations let safe_msgnl s = @@ -85,7 +86,7 @@ type tacvalue = Id.t option list * glob_tactic_expr | VRec of value Id.Map.t ref * glob_tactic_expr -let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) = +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = Genarg.create_arg None "tacvalue" let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -209,17 +210,6 @@ let pr_inspect env expr result = let constr_of_id env id = Term.mkVar (let _ = Environ.lookup_named id env in id) -(* To embed tactics *) - -let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), - (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = - Dyn.create "tactic" - -let ((value_in : value -> Dyn.t), - (value_out : Dyn.t -> value)) = Dyn.create "value" - -let valueIn t = TacDynamic (Loc.ghost, value_in t) - (** Generic arguments : table of interpretation functions *) let push_trace call ist = match TacStore.get ist.extra f_trace with @@ -633,10 +623,10 @@ let pf_interp_constr ist gl = let new_interp_constr ist c k = let open Proofview in - Proofview.Goal.enter begin fun gl -> - let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in + Proofview.Goal.enter { enter = begin fun gl -> + let (sigma, c) = interp_constr ist (Goal.env gl) (Tacmach.New.project gl) c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) - end + end } let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = @@ -791,11 +781,11 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) v) end else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in Ftactic.nf_enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c) + Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Tacmach.New.project gl) c) end else if has_type v (topwit wit_unit) then Ftactic.return (str "()") @@ -803,18 +793,18 @@ let rec message_of_value v = Ftactic.return (int (out_gen (topwit wit_int) v)) else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = pr_constr_env env sigma (snd (c env Evd.empty)) in + let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in Ftactic.nf_enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p) + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Tacmach.New.project gl) c) p) end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end + Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) c) end else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_closed_glob_env (pf_env gl) - (Proofview.Goal.sigma gl) c) + (Tacmach.New.project gl) c) end else match Value.to_list v with | Some l -> @@ -866,7 +856,11 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn (c,ipat) -> - let c = fun env sigma -> interp_open_constr ist env sigma c in + let c = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn (c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x @@ -969,13 +963,21 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in - let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in + Sigma.Unsafe.of_pair (c, sigma) + } in (loc,f) let interp_induction_arg ist gl arg = match arg with | keep,ElimOnConstr c -> - keep,ElimOnConstr (fun env sigma -> interp_constr_with_bindings ist env sigma c) + keep,ElimOnConstr { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr_with_bindings ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err_loc (loc, "", @@ -985,11 +987,13 @@ let interp_induction_arg ist gl arg = let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') - else keep, ElimOnConstr (fun env sigma -> - try sigma, (constr_of_id env id', NoBindings) + else + (keep, ElimOnConstr { delayed = begin fun env sigma -> + try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> user_err_loc (loc, "interp_induction_arg", - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")) + pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") + end }) in try (** FIXME: should be moved to taccoerce *) @@ -1007,16 +1011,18 @@ let interp_induction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr (fun env sigma -> sigma,(c,NoBindings)) + | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in - let f env sigma = + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in - sigma,(c,NoBindings) in + Sigma.Unsafe.of_pair ((c,NoBindings), sigma) + } in keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and @@ -1081,9 +1087,6 @@ let rec read_match_rule lfun ist env sigma = function (* misc *) -let mk_constr_value ist gl c = - let (sigma,c_interp) = pf_interp_constr ist gl c in - sigma, Value.of_constr c_interp let mk_open_constr_value ist gl c = let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in sigma, Value.of_constr c_interp @@ -1159,9 +1162,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end | TacAbstract (tac,ido) -> - Proofview.Goal.nf_enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT (Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac) - end + end } | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1206,12 +1209,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAlias (loc,s,l) -> let body = Tacenv.interp_alias s in let rec f x = match genarg_tag x with - | QuantHypArgType | RedExprArgType - | ConstrWithBindingsArgType - | BindingsArgType + | ConstrArgType + | ListArgType ConstrArgType | OptArgType _ | PairArgType _ -> (** generic handler *) Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in @@ -1220,7 +1222,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | _ as tag -> (** Special treatment. TODO: use generic handler *) Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in match tag with | IntOrVarArgType -> @@ -1231,11 +1233,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | VarArgType -> Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x)) | GenArgType -> f (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> - let (sigma,v) = - Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl - in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) | OpenConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in @@ -1246,15 +1243,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (out_gen (glbwit wit_constr_may_eval) x) in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) - | ListArgType ConstrArgType -> - let wit = glbwit (wit_list wit_constr) in - let (sigma,l_interp) = Tacmach.New.of_old begin fun gl -> - Evd.MonadR.List.map_right - (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c) - (out_gen wit x) - (project gl) - end gl in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in Ftactic.return ( @@ -1337,9 +1325,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacML (loc,opn,l) -> let trace = push_trace (loc,LtacMLCall tac) ist in let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let goal_sigma = Proofview.Goal.sigma gl in + let goal_sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in let tac = Tacenv.interp_ml_tactic opn in @@ -1351,7 +1339,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) - end + end } and force_vrec ist v : typed_generic_argument Ftactic.t = let v = Value.normalize v in @@ -1386,7 +1374,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = match arg with | TacGeneric arg -> Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let goal = Proofview.Goal.goal gl in let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) @@ -1394,7 +1382,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = | Reference r -> interp_ltac_reference dloc false ist r | ConstrMayEval c -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) @@ -1414,12 +1402,12 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = interp_app loc ist fv largs | TacFreshId l -> Ftactic.enter begin fun gl -> - let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in + let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Tacmach.New.project gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) end | TacPretype c -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let {closure;term} = interp_uconstr ist env c in let vars = { @@ -1440,17 +1428,6 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = Proofview.tclUNIT (Value.of_int i) end | Tacexp t -> val_interp ist t - | TacDynamic(_,t) -> - let tg = (Dyn.tag t) in - if String.equal tg "tactic" then - val_interp ist (tactic_out t ist) - else if String.equal tg "value" then - Ftactic.return (value_out t) - else if String.equal tg "constr" then - Ftactic.return (Value.of_constr (constr_out t)) - else - Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" - (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">") (* Interprets an application node *) and interp_app loc ist fv largs : typed_generic_argument Ftactic.t = @@ -1598,7 +1575,7 @@ and interp_match ist lz constr lmr = end end >>= fun constr -> Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) @@ -1607,7 +1584,7 @@ and interp_match ist lz constr lmr = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in let hyps = if lr then List.rev hyps else hyps in @@ -1650,29 +1627,12 @@ and interp_genarg ist env sigma concl gl x = let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (out_gen (glbwit wit_constr_may_eval) x) in evdref := sigma; in_gen (topwit wit_constr_may_eval) c_interp - | QuantHypArgType -> - in_gen (topwit wit_quant_hyp) - (interp_declared_or_quantified_hypothesis ist env sigma - (out_gen (glbwit wit_quant_hyp) x)) - | RedExprArgType -> - let (sigma,r_interp) = - interp_red_expr ist env !evdref (out_gen (glbwit wit_red_expr) x) - in - evdref := sigma; - in_gen (topwit wit_red_expr) r_interp | OpenConstrArgType -> let expected_type = WithoutTypeConstraint in in_gen (topwit wit_open_constr) (interp_open_constr ~expected_type ist env !evdref (snd (out_gen (glbwit wit_open_constr) x))) - | ConstrWithBindingsArgType -> - in_gen (topwit wit_constr_with_bindings) - (pack_sigma (interp_constr_with_bindings ist env !evdref - (out_gen (glbwit wit_constr_with_bindings) x))) - | BindingsArgType -> - in_gen (topwit wit_bindings) - (pack_sigma (interp_bindings ist env !evdref (out_gen (glbwit wit_bindings) x))) | ListArgType ConstrArgType -> let (sigma,v) = interp_genarg_constr_list ist env !evdref x in evdref := sigma; @@ -1754,7 +1714,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = end >>= fun result -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in @@ -1790,9 +1750,9 @@ and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in Tacticals.New.tclWITHHOLES false (name_atomic ~env @@ -1800,17 +1760,17 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) (Tactics.intros_patterns l')) sigma - end + end } | TacIntroMove (ido,hto) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let mloc = interp_move_location ist env sigma hto in let ido = Option.map (interp_ident ist env sigma) ido in name_atomic ~env (TacIntroMove(ido,mloc)) (Tactics.intro_move ido mloc) - end + end } | TacExact c -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin @@ -1825,9 +1785,9 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in (k,(loc,f))) cb @@ -1838,12 +1798,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in sigma, Tactics.apply_delayed_in a ev id l cl in Tacticals.New.tclWITHHOLES ev tac sigma - end + end } end | TacElim (ev,(keep,cb),cbo) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1851,10 +1811,10 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacCase (ev,(keep,cb)) -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let named_tac = @@ -1862,16 +1822,16 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacCase(ev,(keep,cb))) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacFix (idopt,n) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacFix(idopt,n)) (Proofview.V82.tactic (Tactics.fix idopt n)) - end + end } | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin @@ -1890,14 +1850,14 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacCofix idopt -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacCofix (idopt)) (Proofview.V82.tactic (Tactics.cofix idopt)) - end + end } | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin @@ -1916,9 +1876,9 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacAssert (b,t,ipat,c) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in @@ -1928,17 +1888,17 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacAssert(b,t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma - end + end } | TacGeneralize cl -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma - end + (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma + end } | TacGeneralizeDep c -> (new_interp_constr ist c) (fun c -> name_atomic (* spiwack: probably needs a goal environment *) @@ -1947,9 +1907,9 @@ and interp_atomic ist tac : unit Proofview.tactic = ) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in if Locusops.is_nowhere clp then @@ -1980,7 +1940,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) ((sigma,sigma'),c) clp eqpat) sigma') - end + end } (* Automation tactics *) | TacTrivial (debug,lems,l) -> @@ -1990,16 +1950,16 @@ and interp_atomic ist tac : unit Proofview.tactic = ++strbrk"does not print traces anymore." ++ spc() ++strbrk"Use \"Info 1 trivial\", instead.") end; - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let lems = interp_auto_lemmas ist env sigma lems in name_atomic ~env (TacTrivial(debug,List.map snd lems,l)) (Auto.h_trivial ~debug lems (Option.map (List.map (interp_hint_base ist)) l)) - end + end } | TacAuto (debug,n,lems,l) -> begin if debug == Tacexpr.Info then msg_warning @@ -2007,25 +1967,25 @@ and interp_atomic ist tac : unit Proofview.tactic = ++strbrk"does not print traces anymore." ++ spc() ++strbrk"Use \"Info 1 auto\", instead.") end; - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let lems = interp_auto_lemmas ist env sigma lems in name_atomic ~env (TacAuto(debug,n,List.map snd lems,l)) (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) lems (Option.map (List.map (interp_hint_base ist)) l)) - end + end } (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l = List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) @@ -2047,7 +2007,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.induction_destruct isrec ev (l,el))) - end + end } | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2056,25 +2016,25 @@ and interp_atomic ist tac : unit Proofview.tactic = (Elim.h_double_induction h1 h2) (* Context management *) | TacClear (b,l) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) else (* spiwack: until the tactic is in the monad *) let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac - end + end } | TacClearBody l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in name_atomic ~env (TacClearBody l) (Tactics.clear_body l) - end + end } | TacMove (id1,id2) -> Proofview.V82.tactic begin fun gl -> Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) @@ -2082,9 +2042,9 @@ and interp_atomic ist tac : unit Proofview.tactic = gl end | TacRename l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (id1,id2) -> interp_hyp ist env sigma id1, @@ -2093,20 +2053,20 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacRename l) (Tactics.rename_hyp l) - end + end } (* Constructors *) | TacSplit (ev,bll) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in let named_tac = let tac = Tactics.split_with_bindings ev bll in name_atomic ~env (TacSplit (ev, bll)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) @@ -2132,16 +2092,20 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in + let sigma = Sigma.to_evar_map sigma in let ist = { ist with lfun = lfun' } in - if is_onhyps && is_onconcl - then interp_type ist (pf_env gl) sigma c - else interp_constr ist (pf_env gl) sigma c - in + let (sigma, c) = + if is_onhyps && is_onconcl + then interp_type ist (pf_env gl) sigma c + else interp_constr ist (pf_env gl) sigma c + in + Sigma.Unsafe.of_pair (c, sigma) + end } in (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) gl end @@ -2150,47 +2114,54 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin Proofview.V82.nf_evar_goals <*> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in Proofview.V82.tactic begin fun gl -> let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in - try interp_constr ist env sigma c + try + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - in + end } in (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) gl end - end + end } end (* Equivalence relations *) | TacSymmetry c -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma c in name_atomic ~env (TacSymmetry cl) (Tactics.intros_symmetry cl) - end + end } (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let l' = List.map (fun (b,m,(keep,c)) -> - let f env sigma = interp_open_constr_with_bindings ist env sigma c in + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma cl in name_atomic ~env (TacRewrite (ev,l,cl,by)) @@ -2198,11 +2169,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)) - end + end } | TacInversion (DepInversion (k,c,ids),hyp) -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c_interp) = match c with | None -> sigma , None @@ -2218,11 +2189,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) (Inv.dinv k c_interp ids_interp dqhyps)) sigma - end + end } | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in @@ -2230,11 +2201,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) (Inv.inv_clause k ids_interp hyps dqhyps)) sigma - end + end } | TacInversion (InversionUsing (c,idl),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c_interp) = interp_constr ist env sigma c in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in @@ -2242,7 +2213,7 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) (Leminv.lemInv_clause dqhyps c_interp hyps) - end + end } (* Initial call for interpretation *) @@ -2263,7 +2234,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in @@ -2272,7 +2243,7 @@ let interp_tac_gen lfun avoid_ids debug t = interp_tactic ist (intern_pure_tactic { ltacvars; genv = env } t) - end + end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t let _ = Proof_global.set_interp_tac interp @@ -2292,9 +2263,9 @@ let hide_interp global t ot = Proofview.tclENV >>= fun env -> hide_interp env else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> hide_interp (Proofview.Goal.env gl) - end + end } (***************************************************************************) (** Register standard arguments *) @@ -2323,20 +2294,32 @@ let () = let () = declare_uniform wit_pre_ident +let lift f = (); fun ist gl x -> (project gl, f ist (pf_env gl) (project gl) x) +let lifts f = (); fun ist gl x -> f ist (pf_env gl) (project gl) x + +let interp_bindings' ist gl bl = + let (sigma, bl) = interp_bindings ist (pf_env gl) (project gl) bl in + (project gl, pack_sigma (sigma, bl)) + +let interp_constr_with_bindings' ist gl c = + let (sigma, c) = interp_constr_with_bindings ist (pf_env gl) (project gl) c in + (project gl, pack_sigma (sigma, c)) + let () = - let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) (project gl) ref) in - Geninterp.register_interp0 wit_ref interp; - let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in - Geninterp.register_interp0 wit_intro_pattern interp; - let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) (project gl) pat) in - Geninterp.register_interp0 wit_clause_dft_concl interp; - let interp ist gl s = interp_sort (project gl) s in - Geninterp.register_interp0 wit_sort interp + Geninterp.register_interp0 wit_ref (lift interp_reference); + Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern); + Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause); + Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); + Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c); + Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr); + Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); + Geninterp.register_interp0 wit_bindings interp_bindings'; + Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings' let () = let interp ist gl tac = let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in - (project gl, TacArg (dloc, valueIn (of_tacvalue f))) + (project gl, TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f))) in Geninterp.register_interp0 wit_tactic interp @@ -2358,17 +2341,6 @@ let interp_redexp env sigma r = interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) -(* Embed tactics in raw or glob tactic expr *) - -let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) -let tacticIn t = - globTacticIn (fun ist -> - try glob_tactic (t ist) - with e when Errors.noncritical e -> anomaly ~label:"tacticIn" - (str "Incorrect tactic expression. Received exception is:" ++ - Errors.print e)) - -(***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = @@ -2394,9 +2366,9 @@ let _ = Hook.set Auto.extern_interp let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> + let tac _ ist = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let map = function | None -> None | Some id -> @@ -2407,5 +2379,5 @@ let lift_constr_tac_to_ml_tac vars tac = in let args = List.map_filter map vars in tac args ist - end in + end } in tac diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 7605c91554..88802bf350 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -45,14 +45,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env -> (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) -(** To embed several objects in Coqast.t *) -val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t -val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr) - -val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr -val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr -val valueIn : value -> raw_tactic_arg - (** Sets the debugger mode *) val set_debug : debug_info -> unit diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index afffaffbe9..6d32aa81b9 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -266,13 +266,6 @@ and subst_tacarg subst = function | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (subst_tactic subst t) | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) - | TacDynamic(the_loc,t) as x -> - (match Dyn.tag t with - | "tactic" | "value" -> x - | "constr" -> - TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) - | s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" - (str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) and subst_match_rule subst = function @@ -296,21 +289,9 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x)) | ConstrMayEvalArgType -> in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x)) - | QuantHypArgType -> - in_gen (glbwit wit_quant_hyp) - (subst_declared_or_quantified_hypothesis subst - (out_gen (glbwit wit_quant_hyp) x)) - | RedExprArgType -> - in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x)) | OpenConstrArgType -> in_gen (glbwit wit_open_constr) ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x))) - | ConstrWithBindingsArgType -> - in_gen (glbwit wit_constr_with_bindings) - (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x)) - | BindingsArgType -> - in_gen (glbwit wit_bindings) - (subst_bindings subst (out_gen (glbwit wit_bindings) x)) | ListArgType _ -> let list_unpacker wit l = let map x = @@ -347,4 +328,9 @@ let () = Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_sort (fun _ v -> v); Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); - Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c) + Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c); + Genintern.register_subst0 wit_red_expr subst_redexp; + Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis; + Genintern.register_subst0 wit_bindings subst_bindings; + Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings; + () diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 4cce891a2a..e181c8e14e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,6 +16,7 @@ open Context open Declarations open Tacmach open Clenv +open Sigma.Notations (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -225,12 +226,18 @@ let gl_make_elim ind gl = pf_apply Evd.fresh_global gl gr let gl_make_case_dep ind gl = - pf_apply Indrec.build_case_analysis_scheme gl ind true + let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true (elimination_sort_of_goal gl) + in + (Sigma.to_evar_map sigma, r) let gl_make_case_nodep ind gl = - pf_apply Indrec.build_case_analysis_scheme gl ind false + let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in + let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false (elimination_sort_of_goal gl) + in + (Sigma.to_evar_map sigma, r) let make_elim_branch_assumptions ba gl = let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc = @@ -538,66 +545,65 @@ module New = struct mkVar (nthHypId m gl) let onNthHypId m tac = - Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end + Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end } let onNthHyp m tac = - Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end + Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end } let onLastHypId = onNthHypId 1 let onLastHyp = onNthHyp 1 let onNthDecl m tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclUNIT (nthDecl m gl) >>= tac - end + end } let onLastDecl = onNthDecl 1 let ifOnHyp pred tac1 tac2 id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in if pred (id,typ) then tac1 id else tac2 id - end + end } - let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl)) + let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end } let afterHyp id tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in tac rem - end + end } let fullGoal gl = let hyps = Tacmach.New.pf_ids_of_hyps gl in None :: List.map Option.make hyps let tryAllHyps tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclFIRST_PROGRESS_ON tac hyps - end + end } let tryAllHypsAndConcl tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> tclFIRST_PROGRESS_ON tac (fullGoal gl) - end + end } let onClause tac cl = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) - end + end } (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter - begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.nf_enter { enter = begin fun gl -> let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in @@ -649,10 +655,10 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end + end }) end } let elimination_then tac c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with @@ -660,7 +666,7 @@ module New = struct | Some _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) - end + end } let case_then_using = general_elim_then_using gl_make_case_dep false @@ -669,16 +675,16 @@ module New = struct general_elim_then_using gl_make_case_nodep false let elim_on_ba tac ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in tac branches - end + end } let case_on_ba tac ba = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in tac branches - end + end } let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) @@ -695,11 +701,11 @@ module New = struct | Some id -> elimination_sort_of_hyp id gl let pf_constr_of_global ref tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma, c) = Evd.fresh_global env sigma ref in Proofview.Unsafe.tclEVARS sigma <*> (tac c) - end + end } end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4e860892d0..80e01a8d07 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,7 +223,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : [ `NF ] Proofview.Goal.t -> int -> named_context + val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -234,7 +234,7 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `NF ] Proofview.Goal.t -> named_context) -> + val onHyps : ([ `NF ], named_context) Proofview.Goal.enter -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic @@ -242,9 +242,9 @@ module New : sig val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic val onClause : (identifier option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family - val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family - val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_hyp : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family val elimination_then : (branch_args -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 131730ebc0..2e7adc513a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -26,7 +26,7 @@ open Evd open Pfedit open Tacred open Genredexpr -open Tacmach +open Tacmach.New open Logic open Clenv open Refiner @@ -43,21 +43,13 @@ open Locus open Locusops open Misctypes open Proofview.Notations - -let nb_prod x = - let rec count n c = - match kind_of_term c with - Prod(_,_,t) -> count (n+1) t - | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_,_) -> count n c - | _ -> n - in count 0 x +open Sigma.Notations let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost -let typ_of = Retyping.get_type_of +let typ_of env sigma c = Retyping.get_type_of env (Sigma.to_evar_map sigma) c open Goptions @@ -126,13 +118,26 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } +(* Shrinking of abstract proofs. *) + +let shrink_abstract = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "shrinking of abstracted proofs"; + optkey = ["Shrink"; "Abstract"]; + optread = (fun () -> !shrink_abstract) ; + optwrite = (fun b -> shrink_abstract := b) } + (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. Kept as false for compatibility. *) -let bracketing_last_or_and_intro_pattern = ref false +let bracketing_last_or_and_intro_pattern = ref true let use_bracketing_last_or_and_intro_pattern () = !bracketing_last_or_and_intro_pattern @@ -144,7 +149,7 @@ let _ = optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; - optread = (fun () -> !bracketing_last_or_and_intro_pattern) ; + optread = (fun () -> !bracketing_last_or_and_intro_pattern); optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } (*********************************************) @@ -158,21 +163,22 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store (id, c, t) b = - Proofview.Refine.refine ~unsafe:true begin fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in let ctx = named_context_val env in let nctx = push_named_context_val (id, c, t) ctx in let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar id) b in let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - sigma, mkNamedLambda_or_LetIn (id, c, t) ev - end + Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma) + end } let introduction ?(check=true) id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in @@ -184,44 +190,48 @@ let introduction ?(check=true) id = | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b | LetIn (_, c, t, b) -> unsafe_intro env store (id, Some c, t) b | _ -> raise (RefinerError IntroNeedsProduct) - end + end } let refine = Tacmach.refine let convert_concl ?(check=true) ty k = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in - Proofview.Refine.refine ~unsafe:true begin fun sigma -> - let sigma = + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let Sigma ((), sigma, p) = if check then begin + let sigma = Sigma.to_evar_map sigma in ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; - sigma - end else sigma in - let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ~store ty in - (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty)) - end - end + Sigma.Unsafe.of_pair ((), sigma) + end else Sigma.here () sigma in + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in + let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in + Sigma (ans, sigma, p +> q) + end } + end } let convert_hyp ?(check=true) d = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.raw_concl gl in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in - Proofview.Refine.refine ~unsafe:true (fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty) - end + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Evarutil.new_evar env sigma ~principal:true ~store ty + end } + end } let convert_concl_no_check = convert_concl ~check:false let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> try let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in if b then Proofview.Unsafe.tclEVARS sigma @@ -229,7 +239,7 @@ let convert_gen pb x y = with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") -end +end } let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y @@ -262,7 +272,7 @@ let error_replacing_dependency env sigma id err = errorlabstrm "" (replacing_dependency_msg env sigma id err) let thin l gl = - try thin l gl + try Tacmach.thin l gl with Evarutil.ClearDependencyError (id,err) -> error_clear_dependency (pf_env gl) (project gl) id err @@ -302,7 +312,7 @@ let rename_hyp repl = match dom with | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -334,10 +344,12 @@ let rename_hyp repl = let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in let instance = List.map (fun (id, _, _) -> mkVar id) hyps in - Proofview.Refine.refine ~unsafe:true begin fun sigma -> - Evarutil.new_evar_instance nctx sigma nconcl ~store instance - end - end + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in + Sigma.Unsafe.of_pair (c, sigma) + end } + end } (**************************************************************) (* Fresh names *) @@ -382,7 +394,7 @@ let find_name mayrepl decl naming gl = match naming with | NamingAvoid idl -> (* this case must be compatible with [find_intro_names] below. *) let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> @@ -398,16 +410,16 @@ let find_name mayrepl decl naming gl = match naming with (**************************************************************) let assert_before_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENLAST (Proofview.V82.tactic (fun gl -> - try internal_cut b id t gl + try Tacmach.internal_cut b id t gl with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) @@ -416,16 +428,16 @@ let assert_before na = assert_before_gen false (naming_of_name na) let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id)) let assert_after_then_gen b naming t tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (Anonymous,None,t) naming gl in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (fun gl -> - try internal_cut_rev b id t gl + try Tacmach.internal_cut_rev b id t gl with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end + end } let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) @@ -462,7 +474,7 @@ let cofix ido gl = match ido with type tactic_reduction = env -> evar_map -> constr -> constr let pf_reduce_decl redfun where (id,c,ty) gl = - let redfun' = pf_reduce redfun gl in + let redfun' = Tacmach.pf_reduce redfun gl in match c with | None -> if where == InHypValueOnly then @@ -542,11 +554,11 @@ let bind_red_expr_occurrences occs nbcl redexp = certain hypothesis *) let reduct_in_concl (redfun,sty) gl = - Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl + Proofview.V82.of_tactic (convert_concl_no_check (Tacmach.pf_reduce redfun gl (Tacmach.pf_concl gl)) sty) gl let reduct_in_hyp ?(check=false) redfun (id,where) gl = Proofview.V82.of_tactic (convert_hyp ~check - (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl + (pf_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl)) gl let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -573,13 +585,13 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl = let e_reduct_in_concl (redfun,sty) gl = Proofview.V82.of_tactic - (let sigma, c' = (pf_apply redfun gl (pf_concl gl)) in + (let sigma, c' = (Tacmach.pf_apply redfun gl (Tacmach.pf_concl gl)) in Proofview.Unsafe.tclEVARS sigma <*> convert_concl_no_check c' sty) gl let e_reduct_in_hyp ?(check=false) redfun (id,where) gl = Proofview.V82.of_tactic - (let sigma, decl' = pf_e_reduce_decl redfun where (pf_get_hyp gl id) gl in + (let sigma, decl' = pf_e_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl in Proofview.Unsafe.tclEVARS sigma <*> convert_hyp ~check decl') gl @@ -590,17 +602,13 @@ let e_reduct_option ?(check=false) redfun = function (** Versions with evars to maintain the unification of universes resulting from conversions. *) -let tclWITHEVARS f k = - Proofview.Goal.enter begin fun gl -> - let evm, c' = f gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k c') - end - let e_change_in_concl (redfun,sty) = - tclWITHEVARS - (fun gl -> redfun (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) - (Proofview.Goal.raw_concl gl)) - (fun c -> convert_concl_no_check c sty) + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in + Sigma.Unsafe.of_pair (convert_concl_no_check c sty, sigma) + end } let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma = match c with @@ -619,16 +627,18 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma', (id,Some b',ty') let e_change_in_hyp redfun (id,where) = - tclWITHEVARS - (fun gl -> e_pf_change_decl redfun where - (Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl)) - (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)) - convert_hyp + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let sigma, c = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + Sigma.Unsafe.of_pair (convert_hyp c, sigma) + end } -type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr +type change_arg = Pattern.patvar_map -> constr Sigma.run -let make_change_arg c = - fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c) +let make_change_arg c pats = + { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -650,7 +660,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc = (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = - let sigma, t' = t sigma in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (t', sigma, p) = t.run sigma in + let sigma = Sigma.to_evar_map sigma in check_types env sigma mayneedglobalcheck deep t' c; let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); @@ -685,7 +697,7 @@ let change_option occl t = function | None -> change_in_concl occl t let change chg c cls gl = - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in + let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in Proofview.V82.of_tactic (Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> change_option (bind_change_occurrences occs chg) c (Some (id,where)) @@ -726,12 +738,12 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl goal = - let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in + let cl = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in let tac = tclMAP (fun (where,redexp) -> e_reduct_option ~check - (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in + (Redexpr.reduction_of_red_expr (Tacmach.pf_env goal) redexp) where) redexps in if check then with_check tac goal else tac goal (* Unfolding occurrences of a constant *) @@ -768,9 +780,9 @@ let build_intro_tac id dest tac = match dest with Proofview.V82.tactic (move_hyp id dest); tac id] let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = nf_evar (Proofview.Goal.sigma gl) concl in + let concl = nf_evar (Tacmach.New.project gl) concl in match kind_of_term concl with | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> let name = find_name false (name,None,t) name_flag gl in @@ -794,7 +806,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end - end + end } let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false @@ -858,14 +870,14 @@ let get_previous_hyp_position id gl = aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let intro_replacing id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let next_hyp = get_next_hyp_position id gl in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (thin_for_replacing [id]); introduction id; Proofview.V82.tactic (move_hyp id next_hyp); ] - end + end } (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' @@ -877,7 +889,7 @@ let intro_replacing id = (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -886,16 +898,16 @@ let intros_possibly_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) - end + end } (* This version assumes that replacement is actually possible *) let intros_replacing ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Proofview.V82.tactic (thin_for_replacing ids)) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) - end + end } (* User-level introduction tactics *) @@ -913,7 +925,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = env (project gl) ccl)) | x -> x in - try aux (pf_concl gl) + try aux (Tacmach.pf_concl gl) with Redelimination -> None let is_quantified_hypothesis id g = @@ -939,10 +951,10 @@ let depth_of_quantified_hypothesis red h gl = str".") let intros_until_gen red h = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in Tacticals.New.tclDO n (if red then introf else intro) - end + end } let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) @@ -950,7 +962,7 @@ let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true -let tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl +let tclCHECKVAR id gl = ignore (Tacmach.pf_get_hyp gl id); tclIDTAC gl let try_intros_until_id_check id = Tacticals.New.tclORELSE (intros_until_id id) (Proofview.V82.tactic (tclCHECKVAR id)) @@ -965,12 +977,15 @@ let rec intros_move = function Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false) (intros_move rest) +let run_delayed env sigma c = + Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma } + (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> - let (sigma',cbl) = f env sigma in + let (cbl, sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') @@ -980,20 +995,20 @@ let onOpenInductionArg env sigma tac = function (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let pending = (sigma,sigma) in tac clear_flag (pending,(c,NoBindings)) - end)) + end })) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + (Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let pending = (sigma,sigma) in tac clear_flag (pending,(mkVar id,NoBindings)) - end) + end }) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -1017,10 +1032,12 @@ let map_induction_arg f = function (* tactic "cut" (actually modus ponens) *) (****************************************) +let normalize_cut = false + let cut c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_nf_concl gl in let is_sort = try @@ -1035,16 +1052,16 @@ let cut c = if is_sort then let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in (** Backward compat: normalize [c]. *) - let c = local_strong whd_betaiota sigma c in - Proofview.Refine.refine ~unsafe:true begin fun h -> - let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in - let (h, x) = Evarutil.new_evar env h c in - let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - (h, mkApp (f, [|x|])) - end + let c = if normalize_cut then local_strong whd_betaiota sigma c else c in + Proofview.Refine.refine ~unsafe:true { run = begin fun h -> + let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in + let Sigma (x, h, q) = Evarutil.new_evar env h c in + let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in + Sigma (f, h, p +> q) + end } else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") - end + end } let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in @@ -1088,7 +1105,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) if not with_evars && occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Proofview.V82.tactic (refine_no_check new_hyp_prf) in + let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN @@ -1153,12 +1170,12 @@ let enforce_prop_bound_names rename tac = mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t') | _ -> print_int i; Pp.msg (print_constr t); assert false in let rename_branch i = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in change_concl (aux env sigma i t) - end in + end } in (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) tac (Array.map rename_branch nn) @@ -1173,9 +1190,9 @@ let rec contract_letin_in_lam_header c = let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = @@ -1186,7 +1203,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) - end + end } (* * Elimination tactic with bindings and using an arbitrary @@ -1203,20 +1220,20 @@ type eliminator = { } let general_elim_clause_gen elimtac indclause elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in let elimt = Retyping.get_type_of env sigma elimc in let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause - end + end } let general_elim with_evars clear_flag (c, lbindc) elim = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in @@ -1224,28 +1241,30 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) - end + end } (* Case analysis tactics *) let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let t = Retyping.get_type_of env sigma c in - let (mind,_) = reduce_to_quantified_ind env sigma t in + let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in + let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in - let sigma, elim = + let Sigma (elim, sigma, p) = if occur_term c concl then build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + let tac = (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) - end + in + Sigma (tac, sigma, p) + end } let general_case_analysis with_evars clear_flag (c,lbindc as cx) = match kind_of_term c with @@ -1278,11 +1297,13 @@ let find_eliminator c gl = let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> - let evd, elim = find_eliminator c gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) + (Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma, elim = find_eliminator c gl in + let tac = (general_elim with_evars clear_flag cx elim) - end) + in + Sigma.Unsafe.of_pair (tac, sigma) + end }) begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default @@ -1329,9 +1350,9 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta (nth_arg i elimclause.templval.rebus) in @@ -1352,7 +1373,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) - end + end } let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1407,9 +1428,9 @@ let make_projection env sigma params cstr sign elim i n c u = in elim let descend_in_conjunctions avoid tac (err, info) c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in try let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in @@ -1424,13 +1445,14 @@ let descend_in_conjunctions avoid tac (err, info) c = let elim = try DefinedRecord (Recordops.lookup_projections ind) with Not_found -> - let elim = build_case_analysis_scheme env sigma (ind,u) false sort in - NotADefinedRecordUseScheme (snd elim) in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in + NotADefinedRecordUseScheme elim in Tacticals.New.tclFIRST (List.init n (fun i -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match make_projection env sigma params cstr sign elim i n c u with | None -> Tacticals.New.tclFAIL 0 (mt()) | Some (p,pt) -> @@ -1439,31 +1461,33 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end)) + end })) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err - end + end } (****************************************************) (* Resolution tactics *) (****************************************************) let solve_remaining_apply_goals = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in if !apply_solve_class_goals then try let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let evd = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in - if Typeclasses.is_class_type sigma concl then - let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS evd') - (Proofview.V82.tactic (refine_no_check c')) - else Proofview.tclUNIT () - with Not_found -> Proofview.tclUNIT () - else Proofview.tclUNIT () - end + if Typeclasses.is_class_type evd concl then + let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in + let tac = + (Proofview.V82.tactic (Tacmach.refine_no_check c')) + in + Sigma.Unsafe.of_pair (tac, evd') + else Sigma.here (Proofview.tclUNIT ()) sigma + with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma + else Sigma.here (Proofview.tclUNIT ()) sigma + end } let tclORELSEOPT t k = Proofview.tclORELSE t @@ -1474,23 +1498,23 @@ let tclORELSEOPT t k = | Some tac -> tac) let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod concl in + let concl_nprod = nb_prod_modulo_zeta concl in let rec try_main_apply with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try - let n = nb_prod thm_ty - nprod in + let n = nb_prod_modulo_zeta thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags @@ -1537,14 +1561,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) | PretypeError _|RefinerError _|UserError _|Failure _ -> Some (try_red_apply thm_ty0 (e, info)) | _ -> None) - end + end } in Tacticals.New.tclTHENLIST [ try_main_apply with_destruct c; solve_remaining_apply_goals; apply_clear_request clear_flag (use_clear_hyp_by_default ()) c ] - end + end } let rec apply_with_bindings_gen b e = function | [] -> Proofview.tclUNIT () @@ -1556,13 +1580,13 @@ let rec apply_with_bindings_gen b e = function let apply_with_delayed_bindings_gen b e l = let one k (loc, f) = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma, cb = f env sigma in + let (cb, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES e (general_apply b b e k (loc,cb)) sigma - end + end } in let rec aux = function | [] -> Proofview.tclUNIT () @@ -1625,18 +1649,18 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) = let apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,(d,lbind))) tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (Anonymous,None,t') naming gl in let rec aux idstoclear with_destruct c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in try let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause @@ -1651,22 +1675,22 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) - end + end } in aux [] with_destruct d - end + end } let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,f)) tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let sigma, c = f env sigma in + let sigma = Tacmach.New.project gl in + let (c, sigma) = run_delayed env sigma f in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,c)) tac) sigma - end + end } (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1686,20 +1710,20 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam *) let cut_and_apply c = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in - Proofview.Refine.refine begin fun sigma -> + Proofview.Refine.refine { run = begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in - let (sigma, f) = Evarutil.new_evar env sigma typ in - let (sigma, x) = Evarutil.new_evar env sigma c1 in + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in let ans = mkApp (f, [|mkApp (c, [|x|])|]) in - (sigma, ans) - end + Sigma (ans, sigma, p +> q) + end } | _ -> error "lapply needs a non-dependent product." - end + end } (********************************************************************) (* Exact tactics *) @@ -1712,33 +1736,36 @@ let cut_and_apply c = (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) let new_exact_no_check c = - Proofview.Refine.refine ~unsafe:true (fun h -> (h, c)) + Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } let exact_check c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in - Proofview.Unsafe.tclEVARS sigma <*> + let tac = Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } -let exact_no_check = refine_no_check +let exact_no_check = Tacmach.refine_no_check let vm_cast_no_check c gl = - let concl = pf_concl gl in - refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl + let concl = Tacmach.pf_concl gl in + Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl let native_cast_no_check c gl = - let concl = pf_concl gl in - refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl + let concl = Tacmach.pf_concl gl in + Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl let exact_proof c gl = - let c,ctx = Constrintern.interp_casted_constr (pf_env gl) (project gl) c (pf_concl gl) - in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl + let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl) + in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl let assumption = let rec arec gl only_eq = function @@ -1749,7 +1776,7 @@ let assumption = else Tacticals.New.tclZEROMSG (str "No such assumption.") | (id, c, t)::rest -> let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = if only_eq then (sigma, Constr.equal t concl) else @@ -1758,13 +1785,13 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id)) + Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar id) h } else arec gl only_eq rest in - let assumption_tac gl = + let assumption_tac = { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in arec gl true hyps - in + end } in Proofview.Goal.nf_enter assumption_tac (*****************************************************************) @@ -1807,7 +1834,7 @@ let check_decl env (_, c, ty) msg = msg e let clear_body ids = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let ctx = named_context env in @@ -1840,10 +1867,10 @@ let clear_body ids = check_is_type env concl msg in check_hyps <*> check_concl <*> - Proofview.Refine.refine ~unsafe:true begin fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl - end - end + end } + end } let clear_wildcards ids = Proofview.V82.tactic (tclMAP (fun (loc,id) gl -> @@ -1873,7 +1900,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in + let clause = Tacmach.pf_apply make_clenv_binding g (c,Tacmach.pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1890,20 +1917,20 @@ let specialize (c,lbind) g = tclEVARS clause.evd, term in match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with - | Var id when Id.List.mem id (pf_ids_of_hyps g) -> + | Var id when Id.List.mem id (Tacmach.pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (Tacmach.pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (Tacmach.pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) let keep hyps = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let cl,_ = @@ -1916,7 +1943,7 @@ let keep hyps = ~init:([],[]) (Proofview.Goal.env gl) in Proofview.V82.tactic (fun gl -> thin cl gl) - end + end } (************************) (* Introduction tactics *) @@ -1933,7 +1960,8 @@ let check_number_of_constructors expctdnumopt i nconstr = if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let cl = Tacmach.New.pf_nf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -1943,16 +1971,19 @@ let constructor_tac with_evars expctdnumopt i lbind = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; - let sigma, cons = Evd.fresh_constructor_instance - (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in + let Sigma (cons, sigma, p) = Sigma.fresh_constructor_instance + (Proofview.Goal.env gl) sigma (fst mind, i) in let cons = mkConstructU cons in let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in + let tac = (Tacticals.New.tclTHENLIST - [Proofview.Unsafe.tclEVARS sigma; + [ convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) - end + in + Sigma (tac, sigma, p) + end } let one_constructor i lbind = constructor_tac false None i lbind @@ -1969,7 +2000,7 @@ let rec tclANY tac = function let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let cl = Tacmach.New.pf_nf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -1979,7 +2010,7 @@ let any_constructor with_evars tacopt = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; tclANY tac (List.interval 1 nconstr) - end + end } let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -2030,7 +2061,7 @@ let my_find_eq_data_decompose gl t = | Constr_matching.PatternMatchingFailure -> None let intro_decomp_eq loc l thin tac id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2041,10 +2072,10 @@ let intro_decomp_eq loc l thin tac id = (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") - end + end } let intro_or_and_pattern loc bracketed ll thin tac id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2055,7 +2086,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id = (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id]))) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv (Array.of_list ll)) - end + end } let rewrite_hyp assert_style l2r id = let rew_on l2r = @@ -2063,7 +2094,7 @@ let rewrite_hyp assert_style l2r id = let subst_on l2r x rhs = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in @@ -2085,7 +2116,7 @@ let rewrite_hyp assert_style l2r id = Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) | _ -> Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) - end + end } let rec prepare_naming loc = function | IntroIdentifier id -> NamingMustBe (loc,id) @@ -2221,7 +2252,10 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with Proofview.tclUNIT () (* apply_in_once do a replacement *) else Proofview.V82.tactic (clear [id]) in - let f env sigma = let (sigma,c) = f env sigma in (sigma,(c,NoBindings)) in + let f = { delayed = fun env sigma -> + let Sigma (c, sigma, p) = f.delayed env sigma in + Sigma ((c, NoBindings), sigma, p) + } in apply_in_delayed_once false true true true naming id (None,(loc,f)) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) @@ -2286,7 +2320,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars let tac (naming,lemma) tac id = apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) else get_previous_hyp_position id gl in @@ -2297,7 +2331,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id - end + end } (* if sidecond_first then @@ -2308,7 +2342,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars *) let apply_in simple with_evars id lemmas ipat = - let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, fun _ sigma -> sigma, l)) lemmas in + let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = @@ -2339,16 +2373,17 @@ let decode_hyp = function *) let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let (sigma, t) = match ty with - | Some t -> (sigma, t) + let env = Proofview.Goal.env gl in + let Sigma (t, sigma, p) = match ty with + | Some t -> Sigma.here t sigma | None -> let t = typ_of env sigma c in - Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t + let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in + Sigma.Unsafe.of_pair (c, sigma) in - let eq_tac gl = match with_eq with + let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl @@ -2356,26 +2391,31 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = | IntroIdentifier id -> id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env sigma eqdata.eq in - let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in + let sigma = Sigma.to_evar_map sigma in let sigma, _ = Typing.type_of env sigma term in - sigma, term, + let ans = term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) (clear_body [heq;id]) + in + Sigma.Unsafe.of_pair (ans, sigma) | None -> - (sigma, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in - let (sigma,newcl,eq_tac) = eq_tac gl in - Tacticals.New.tclTHENLIST - [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check newcl DEFAULTcast; + Sigma.here (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) sigma + in + let tac = + Tacticals.New.tclTHENLIST + [ convert_concl_no_check newcl DEFAULTcast; intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ] - end + in + Sigma (tac, sigma, p +> q) + end } let insert_before decls lasthyp env = match lasthyp with @@ -2403,55 +2443,57 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env sigma eqdata.eq in - let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in - let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in - (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) + let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in + Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) | None -> let newenv = insert_before [id,body,t] lastlhyp env in - let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in - (sigma,mkNamedLetIn id c t x) + let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in + Sigma (mkNamedLetIn id c t x, sigma, p) let letin_tac with_eq id c ty occs = - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let abs = AbstractExact (id,c,ty,occs,true) in let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in (* We keep the original term to match *) - letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty - end + let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in + Sigma.here tac sigma + end } let letin_pat_tac with_eq id c occs = - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in - let sigma,c = match res with + let Sigma (c, sigma, p) = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c - | Some (sigma,c) -> (sigma,c) in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) + | Some res -> res in + let tac = (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) - end + in + Sigma (tac, sigma, p) + end } (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *) let forward b usetac ipat c = match usetac with | None -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in let hd = head_ident c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (Proofview.V82.tactic (exact_no_check c)) - end + end } | Some tac -> if b then Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac @@ -2481,25 +2523,25 @@ let apply_type hdcty argl gl = let bring_hyps hyps = if List.is_empty hyps then Tacticals.New.tclIDTAC else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (instance_from_named_context hyps) in - Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = + Proofview.Refine.refine { run = begin fun sigma -> + let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in - (sigma, (mkApp (ev, args))) - end - end + Sigma (mkApp (ev, args), sigma, p) + end } + end } let revert hyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) - end + end } (* Compute a name for a generalization *) @@ -2533,9 +2575,9 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_unsafe_type_of gl c in - let env = pf_env gl in - generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl + let t = Tacmach.pf_unsafe_type_of gl c in + let env = Tacmach.pf_env gl in + generalize_goal_gen env (Tacmach.pf_ids_of_hyps gl) i o t cl let generalize_dep ?(with_let=false) c gl = let env = pf_env gl in @@ -2557,11 +2599,11 @@ let generalize_dep ?(with_let=false) c gl = -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in let body = if with_let then match kind_of_term c with - | Var id -> pi2 (pf_get_hyp gl id) + | Var id -> pi2 (Tacmach.pf_get_hyp gl id) | _ -> None else None in @@ -2578,17 +2620,18 @@ let generalize_dep ?(with_let=false) c gl = let generalize_gen_let lconstr gl = let newcl, evd = List.fold_right_i (generalize_goal gl) 0 lconstr - (pf_concl gl,project gl) + (Tacmach.pf_concl gl,Tacmach.project gl) in tclTHEN (tclEVARS evd) (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> if Option.is_empty b then Some c else None) lconstr)) gl let new_generalize_gen_let lconstr = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in let (newcl, sigma), args = @@ -2599,15 +2642,18 @@ let new_generalize_gen_let lconstr = generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in - (sigma, (applist (ev, args))) - end - end + let tac = + Proofview.Refine.refine { run = begin fun sigma -> + let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in + Sigma ((applist (ev, args)), sigma, p) + end } + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let generalize_gen lconstr = - generalize_gen_let (List.map (fun ((occs,c),na) -> + generalize_gen_let (List.map (fun (occs_c,na) -> + let (occs,c) = Redexpr.out_with_occurrences occs_c in (occs,c,None),na) lconstr) let new_generalize_gen lconstr = @@ -2698,7 +2744,7 @@ let check_unused_names names = (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr (snd (c (Global.env()) Evd.empty)))) names) + (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names) let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -2778,7 +2824,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = match ra with | (RecArg,deprec,recvarname) :: (IndArg,depind,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (recpat,names) = match names with | [loc,IntroNaming (IntroIdentifier id) as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in @@ -2786,37 +2832,37 @@ let induct_discharge dests avoid' tac (avoid,ra) names = | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [recpat] (fun ids thin -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin) - end) - end + end }) + end } | (IndArg,dep,hyprecname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) - end + end } | (RecArg,dep,recvarname) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | (OtherArg,dep,_) :: ra' -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end + end } | [] -> check_unused_names names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) @@ -2828,6 +2874,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names = substitutions aussi sur l'argument voisin *) let expand_projections env sigma c = + let sigma = Sigma.to_evar_map sigma in let rec aux env c = match kind_of_term c with | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) [] @@ -2838,7 +2885,7 @@ let expand_projections env sigma c = (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in @@ -2891,7 +2938,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid)) in atomize_one (List.length argl) [] [] [] - end + end } (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps @@ -3194,19 +3241,19 @@ let decompose_indapp f args = | _ -> f, args let mk_term_eq env sigma ty t ty' t' = + let sigma = Sigma.to_evar_map sigma in if Reductionops.is_conv env sigma ty ty' then mkEq ty t t', mkRefl ty' t' else mkHEq ty t ty' t', mkHRefl ty' t' -let make_abstract_generalize gl id concl dep ctx body c eqs args refls = - let meta = Evarutil.new_meta() in +let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = + Proofview.Refine.refine { run = begin fun sigma -> let eqslen = List.length eqs in - let term, typ = mkVar id, pf_get_hyp_typ gl id in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) let abshypeq, abshypt = if dep then - let eq, refl = mk_term_eq (push_rel_context ctx (pf_env gl)) (project gl) (lift 1 c) (mkRel 1) typ term in + let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in mkProd (Anonymous, eq, lift 1 concl), [| refl |] else concl, [||] in @@ -3218,7 +3265,7 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn genarg ctx in (* The goal will become this product. *) - let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in + let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instantiated hyp. *) @@ -3226,7 +3273,8 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) - mkApp (appeqs, abshypt) + Sigma (mkApp (appeqs, abshypt), sigma, p) + end } let hyps_of_vars env sign nogen hyps = if Id.Set.is_empty hyps then [] @@ -3267,9 +3315,9 @@ let is_defined_variable env id = match lookup_named id env with | (_, Some _, _) -> true let abstract_args gl generalize_vars dep id defined f args = - let sigma = ref (project gl) in - let env = pf_env gl in - let concl = pf_concl gl in + let sigma = ref (Tacmach.project gl) in + let env = Tacmach.pf_env gl in + let concl = Tacmach.pf_concl gl in let dep = dep || dependent (mkVar id) concl in let avoid = ref [] in let get_id name = @@ -3287,7 +3335,7 @@ let abstract_args gl generalize_vars dep id defined f args = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in List.hd rel, c in - let argty = pf_unsafe_type_of gl arg in + let argty = Tacmach.pf_unsafe_type_of gl arg in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in let () = sigma := sigma' in let lenctx = List.length ctx in @@ -3328,7 +3376,7 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let tyf' = pf_unsafe_type_of gl f' in + let tyf' = Tacmach.pf_unsafe_type_of gl f' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in @@ -3340,15 +3388,17 @@ let abstract_args gl generalize_vars dep id defined f args = else [] in let body, c' = - if defined then Some c', typ_of ctxenv !sigma c' + if defined then Some c', Retyping.get_type_of ctxenv !sigma c' else None, c' in - let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in - Some (term, !sigma, dep, succ (List.length ctx), vars) + let typ = Tacmach.pf_get_hyp_typ gl id in + let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in + let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in + Some (tac, dep, succ (List.length ctx), vars) else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.jmeq_module_name; let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in @@ -3366,17 +3416,15 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in match newc with | None -> Proofview.tclUNIT () - | Some (newc, sigma, dep, n, vars) -> + | Some (tac, dep, n, vars) -> let tac = if dep then - Tacticals.New.tclTHENLIST - [Proofview.Unsafe.tclEVARS sigma; - Proofview.V82.tactic (refine newc); + Tacticals.New.tclTHENLIST [ + tac; rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] - else Tacticals.New.tclTHENLIST - [Proofview.Unsafe.tclEVARS sigma; - Proofview.V82.tactic (refine newc); + else Tacticals.New.tclTHENLIST [ + tac; Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro] in @@ -3386,15 +3434,15 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) - end + end } let rec compare_upto_variables x y = if (isVar x || isRel x) && (isVar y || isRel y) then true else compare_constr compare_upto_variables x y let specialize_eqs id gl = - let env = pf_env gl in - let ty = pf_get_hyp_typ gl id in + let env = Tacmach.pf_env gl in + let ty = Tacmach.pf_get_hyp_typ gl id in let evars = ref (project gl) in let unif env evars c1 c2 = compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 @@ -3658,18 +3706,23 @@ let guess_elim isrec dep s hyp0 gl = let evd, elimc = if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl else + let env = Tacmach.New.pf_env gl in + let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in if use_dependent_propositions_elimination () && dep then - Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s + let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in + (Sigma.to_evar_map sigma, ind) else - Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in + let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in + (Sigma.to_evar_map sigma, ind) + in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess + Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3714,7 +3767,7 @@ let is_functional_induction elimc gl = let get_eliminator elim dep s gl = match elim with | ElimUsing (elim,indsign) -> - Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign + Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in @@ -3737,10 +3790,10 @@ let recolle_clenv i params args elimclause gl = let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in (* parameters correspond to first elts of lid. *) let clauses_params = - List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i)) + List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(i)) 0 params in let clauses_args = - List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(k+i)) + List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(k+i)) 0 args in let clauses = clauses_params@clauses_args in (* iteration of clenv_fchain with all infos we have. *) @@ -3767,7 +3820,7 @@ let induction_tac with_evars params indvars elim gl = let elimc = contract_letin_in_lam_header elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in let elimclause = - pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in + Tacmach.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in (* elimclause' is built from elimclause by instanciating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) @@ -3779,9 +3832,10 @@ let induction_tac with_evars params indvars elim gl = induction applies with the induction hypotheses *) let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map sigma in let concl = Tacmach.New.pf_nf_concl gl in let statuslists,lhyp0,toclear,deps,avoid,dep = cook_sign hyp0 inhyps indvars env in let dep = dep || Option.cata (fun id -> occur_var env id concl) false hyp0 in @@ -3792,9 +3846,9 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in let names = compute_induction_names (Array.length indsign) names in + let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; (* Generalize dependent hyps (but not args) *) if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr); (* side-conditions in elim (resp case) schemes come last (resp first) *) @@ -3804,15 +3858,17 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac = (Array.map2 (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists)) indsign names) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim))) - end + end } let msg_not_right_number_induction_arguments scheme = str"Not the right number of induction arguments (expected " ++ @@ -3829,7 +3885,7 @@ let msg_not_right_number_induction_arguments scheme = must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac *) let induction_without_atomization isrec with_evars elim names lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in let nargs_indarg_farg = scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in @@ -3860,11 +3916,11 @@ let induction_without_atomization isrec with_evars elim names lid = ]) in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context None [] elim indvars names induct_tac - end + end } (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls gl = - if occur_var (pf_env gl) id (pf_concl gl) && + if occur_var (Tacmach.pf_env gl) id (Tacmach.pf_concl gl) && cls.concl_occs == NoOccurrences then errorlabstrm "" (str "Conclusion must be mentioned: it depends on " ++ pr_id id @@ -3882,6 +3938,7 @@ let clear_unselected_context id inhyps cls gl = | None -> tclIDTAC gl let use_bindings env sigma elim must_be_closed (c,lbind) typ = + let sigma = Sigma.to_evar_map sigma in let typ = if elim == None then (* w/o an scheme, the term has to be applied at least until @@ -3903,7 +3960,8 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = if must_be_closed && occur_meta (clenv_value indclause) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) - pose_all_metas_as_evars env indclause.evd (clenv_value indclause) + let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in + Sigma.Unsafe.of_pair (c, sigma) with e when catchable_exception e -> try find_clause (try_red_product env sigma typ) with Redelimination -> raise e in @@ -3921,6 +3979,7 @@ let check_expected_type env sigma (elimc,bl) elimt = fun t -> Evarconv.e_cumul env (ref sigma) t u let check_enough_applied env sigma elim = + let sigma = Sigma.to_evar_map sigma in (* A heuristic to decide whether the induction arg is enough applied *) match elim with | None -> @@ -3928,7 +3987,7 @@ let check_enough_applied env sigma elim = fun u -> let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t | Some elimc -> - let elimt = typ_of env sigma (fst elimc) in + let elimt = Retyping.get_type_of env sigma (fst elimc) in let scheme = compute_elim_sig ~elimc elimt in match scheme.indref with | None -> @@ -3941,13 +4000,13 @@ let check_enough_applied env sigma elim = let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.raw_concl gl in let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in - let (sigma',c) = use_bindings env sigma elim false (c0,lbind) t0 in + let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with @@ -3957,7 +4016,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in - let (sigma,c0) = finish_evar_resolution ~flags env sigma (pending,c0) in + let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in + let tac = (if isrec then (* Historically, induction has side conditions last *) Tacticals.New.tclTHENFIRST @@ -3965,12 +4025,13 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* and destruct has side conditions first *) Tacticals.New.tclTHENLAST) (Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; - Proofview.Refine.refine ~unsafe:true (fun sigma -> + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> let b = not with_evars && with_eq != None in - let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in - let t = Retyping.get_type_of env sigma c in - mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)); + let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in + let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in + let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in + Sigma (ans, sigma, p +> q) + end }; Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable); if is_arg_pure_hyp then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0])) @@ -3978,19 +4039,24 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) tac + in + Sigma (tac, sigma, q) - | Some (sigma',c) -> + | Some (Sigma (c, sigma', q)) -> (* pattern found *) let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) let env = reset_with_named_context sign env in + let tac = Tacticals.New.tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma'; - Proofview.Refine.refine ~unsafe:true (fun sigma -> - mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None); + Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None + end }; tac ] - end + in + Sigma (tac, sigma', p +> q) + end } let has_generic_occurrences_but_goal cls id env ccl = clause_with_generic_context_selection cls && @@ -4002,7 +4068,7 @@ let induction_gen clear_flag isrec with_evars elim let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.raw_concl gl in @@ -4037,7 +4103,7 @@ let induction_gen clear_flag isrec with_evars elim isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) - end + end } (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4062,7 +4128,7 @@ let induction_gen_l isrec with_evars elim names lc = atomize_list l' | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4073,7 +4139,7 @@ let induction_gen_l isrec with_evars elim names lc = Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') - end in + end } in Tacticals.New.tclTHENLIST [ (atomize_list lc); @@ -4090,18 +4156,21 @@ let induction_destruct isrec with_evars (lc,elim) = match lc with | [] -> assert false (* ensured by syntax, but if called inside caml? *) | [c,(eqname,names as allnames),cls] -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match elim with | Some elim when is_functional_induction elim gl -> (* Standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) if not (Option.is_empty cls) then error "'in' clause not supported here."; let finish_evar_resolution f = - let (sigma',(c,lbind)) = f env sigma in + let ((c, lbind), sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in - snd (finish_evar_resolution env sigma' (pending,c)),lbind in + let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in + (c, lbind) + in let c = map_induction_arg finish_evar_resolution c in onInductionArg (fun _clear_flag (c,lbind) -> @@ -4112,11 +4181,11 @@ let induction_destruct isrec with_evars (lc,elim) = (* standard induction *) onOpenInductionArg env sigma (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c - end + end } | _ -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in match elim with | None -> (* Several arguments, without "using" clause *) @@ -4130,20 +4199,23 @@ let induction_destruct isrec with_evars (lc,elim) = (onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag isrec with_evars None (a,b) cl) a) (Tacticals.New.tclMAP (fun (a,b,cl) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a - end) l) + end }) l) | Some elim -> (* Several induction hyps with induction scheme *) let finish_evar_resolution f = - let (sigma',(c,lbind)) = f env sigma in + let ((c, lbind), sigma') = run_delayed env sigma f in let pending = (sigma,sigma') in if lbind != NoBindings then error "'with' clause not supported here."; - snd (finish_evar_resolution env sigma' (pending,c)) in + let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let Sigma (c, _, _) = finish_evar_resolution env sigma' (pending,c) in + c + in let lc = List.map (on_pi1 (map_induction_arg finish_evar_resolution)) lc in let newlc = List.map (fun (x,(eqn,names),cls) -> @@ -4160,7 +4232,7 @@ let induction_destruct isrec with_evars (lc,elim) = error "'as' clause with multiple arguments and 'using' clause can only occur last."; let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc - end + end } let induction ev clr c l e = induction_gen clr true ev e @@ -4202,7 +4274,7 @@ let simple_destruct = function *) let elim_scheme_type elim t = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in match kind_of_term (last_arg clause.templval.rebus) with | Meta mv -> @@ -4212,23 +4284,24 @@ let elim_scheme_type elim t = (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type") - end + end } let elim_type t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) - end + Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) + end } let case_type t = - Proofview.Goal.enter begin fun gl -> - let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in - let evd, elimc = - Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl) - in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) - end + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Tacmach.New.pf_env gl in + let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in + let s = Tacticals.New.elimination_sort_of_goal gl in + let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in + Sigma (elim_scheme_type elimc t, evd, p) + end } (************************************************) @@ -4241,14 +4314,14 @@ let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make () let maybe_betadeltaiota_concl allowred gl = let concl = Tacmach.New.pf_nf_concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in if not allowred then concl else let env = Proofview.Goal.env gl in whd_betadeltaiota env sigma concl let reflexivity_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4256,7 +4329,7 @@ let reflexivity_red allowred = match match_with_equality_type concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings - end + end } let reflexivity = Proofview.tclORELSE @@ -4298,7 +4371,7 @@ let match_with_equation c = Proofview.tclZERO NoEquationFound let symmetry_red allowred = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4310,7 +4383,7 @@ let symmetry_red allowred = (convert_concl_no_check concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind - end + end } let symmetry = Proofview.tclORELSE @@ -4324,7 +4397,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE @@ -4342,7 +4415,7 @@ let symmetry_in id = | NoEquationFound -> Hook.get forward_setoid_symmetry_in id | e -> Proofview.tclZERO ~info e end - end + end } let intros_symmetry = Tacticals.New.onClause @@ -4367,7 +4440,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4375,7 +4448,7 @@ let prove_transitivity hdcncl eq_kind t = mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), @@ -4387,10 +4460,10 @@ let prove_transitivity hdcncl eq_kind t = [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; assumption ])) - end + end } let transitivity_red allowred t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4407,7 +4480,7 @@ let transitivity_red allowred t = match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") | Some t -> prove_transitivity eq eq_kind t - end + end } let transitivity_gen t = Proofview.tclORELSE @@ -4433,14 +4506,59 @@ let interpretable_as_section_decl evd d1 d2 = match d2,d1 with e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 | (_,None,t1), (_,_,t2) -> e_eq_constr_univs evd t1 t2 +let rec decompose len c t accu = + if len = 0 then (c, t, accu) + else match kind_of_term c, kind_of_term t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t ((na, None, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t ((na, Some b, u) :: accu) + | _ -> assert false + +let rec shrink ctx sign c t accu = match ctx, sign with +| [], [] -> (c, t, accu) +| p :: ctx, (id, _, _) :: sign -> + if noccurn 1 c then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = mkLambda_or_LetIn p c in + let t = mkProd_or_LetIn p t in + let accu = match p with + | (_, None, _) -> mkVar id :: accu + | (_, Some _, _) -> accu + in + shrink ctx sign c t accu +| _ -> assert false + +let shrink_entry sign const = + let open Entries in + let typ = match const.const_entry_type with + | None -> assert false + | Some t -> t + in + (** The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.const_entry_body) in + let ((body, uctx), eff) = Future.force const.const_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + let const = { const with + const_entry_body = Future.from_val ((body, uctx), eff); + const_entry_type = Some typ; + } in + (const, args) + let abstract_subproof id gk tac = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context() and global_sign = Proofview.Goal.hyps gl in - let evdref = ref (Proofview.Goal.sigma gl) in + let sigma = Sigma.to_evar_map sigma in + let evdref = ref sigma in let sign,secsign = List.fold_right (fun (id,_,_ as d) (s1,s2) -> @@ -4474,6 +4592,10 @@ let abstract_subproof id gk tac = let (_, info) = Errors.push src in iraise (e, info) in + let const, args = + if !shrink_abstract then shrink_entry sign const + else (const, List.rev (instance_from_named_context sign)) + in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in (** ppedrot: seems legit to have abstracted subproofs as local*) @@ -4485,14 +4607,13 @@ let abstract_subproof id gk tac = let eff = private_con_of_con (Global.safe_env ()) cst in let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in - let args = List.rev (instance_from_named_context sign) in let solve = - Proofview.Unsafe.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in - if not safe then Proofview.mark_as_unsafe <*> solve else solve - end + let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in + Sigma.Unsafe.of_pair (tac, evd) + end } let anon_id = Id.of_string "anonymous" @@ -4512,7 +4633,8 @@ let tclABSTRACT name_op tac = abstract_subproof s gk tac let unify ?(state=full_transparent_state) x y = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in try let core_flags = { (default_unify_flags ()).core_unify_flags with @@ -4524,22 +4646,18 @@ let unify ?(state=full_transparent_state) x y = merge_unify_flags = core_flags; subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } in - let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y - in Proofview.Unsafe.tclEVARS evd - with e when Errors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Not unifiable") - end + let sigma = Sigma.to_evar_map sigma in + let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in + Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma) + with e when Errors.noncritical e -> + Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma + end } module Simple = struct (** Simplified version of some of the above tactics *) let intro x = intro_move (Some x) MoveLast - let generalize_gen cl = - generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl) - let generalize cl = - generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous)) - cl) - let apply c = apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))] let eapply c = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 896b33727c..f5695ff06e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -126,7 +126,7 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic @@ -206,6 +206,8 @@ val apply_delayed_in : (clear_flag * delayed_open_constr_with_bindings located) list -> intro_pattern option -> unit Proofview.tactic +val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map + (** {6 Elimination tactics. } *) (* @@ -384,7 +386,8 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic + val new_generalize : constr list -> unit Proofview.tactic val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic @@ -416,9 +419,6 @@ module Simple : sig (** Simplified version of some of the above tactics *) val intro : Id.t -> unit Proofview.tactic - val generalize : constr list -> tactic - val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic - val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic @@ -431,7 +431,7 @@ end module New : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic + val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c] followed by beta-iota-reduction of the conclusion. *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index b4c7bffa9c..537d10dd55 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -14,10 +14,13 @@ open Names open Pp open Genarg open Stdarg +open Tacexpr open Tacinterp open Tactics open Errors open Util +open Tacticals.New +open Proofview.Notations DECLARE PLUGIN "tauto" @@ -51,6 +54,13 @@ type tauto_flags = { strict_unit : bool; } +let wit_tauto_flags : tauto_flags uniform_genarg_type = + Genarg.create_arg None "tauto_flags" + +let assoc_flags ist = + let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in + try Genarg.out_gen (topwit wit_tauto_flags) v with _ -> assert false + (* Whether inner not are unfolded *) let negation_unfolding = ref true @@ -78,26 +88,70 @@ let _ = optread = (fun () -> !iff_unfolding); optwrite = (:=) iff_unfolding } +(** Base tactics *) + +let idtac = Proofview.tclUNIT () +let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ())) + +let intro = Tactics.intro + +let assert_ ?by c = + let tac = match by with + | None -> None + | Some tac -> Some (tclCOMPLETE tac) + in + Proofview.tclINDEPENDENT (Tactics.forward true tac None c) + +let apply c = Tactics.apply c + +let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl) + +let assumption = Tactics.assumption + +let split = Tactics.split_with_bindings false [Misctypes.NoBindings] + (** Test *) let make_lfun l = let fold accu (id, v) = Id.Map.add (Id.of_string id) v accu in List.fold_left fold Id.Map.empty l -let is_empty ist = - if is_empty_type (assoc_var "X1" ist) then - <:tactic<idtac>> - else - <:tactic<fail>> +let register_tauto_tactic tac name = + let name = { mltac_plugin = "tauto"; mltac_tactic = name; } in + let entry = { mltac_name = name; mltac_index = 0 } in + Tacenv.register_ml_tactic name [| tac |]; + TacML (Loc.ghost, entry, []) + +let tacticIn_ist tac name = + let tac _ ist = + let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in + let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in + let (tac, ist) = tac ist in + interp_tac_gen ist.lfun avoid debug tac + in + register_tauto_tactic tac name + +let tacticIn tac name = + tacticIn_ist (fun ist -> tac ist, ist) name + +let push_ist ist args = + let fold accu (id, arg) = Id.Map.add (Id.of_string id) arg accu in + let lfun = List.fold_left fold ist.lfun args in + { ist with lfun = lfun } + +let is_empty _ ist = + if is_empty_type (assoc_var "X1" ist) then idtac else fail + +let t_is_empty = register_tauto_tactic is_empty "is_empty" (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) -let is_unit_or_eq flags ist = +let is_unit_or_eq _ ist = + let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test (assoc_var "X1" ist) then - <:tactic<idtac>> - else - <:tactic<fail>> + if test (assoc_var "X1" ist) then idtac else fail + +let t_is_unit_or_eq = register_tauto_tactic is_unit_or_eq "is_unit_or_eq" let is_record t = let (hdapp,args) = decompose_app t in @@ -116,23 +170,22 @@ let bugged_is_binary t = Int.equal mib.Declarations.mind_nparams 2 | _ -> false -let iter_tac tacl = - List.fold_right (fun tac tacs -> <:tactic< $tac; $tacs >>) tacl - (** Dealing with conjunction *) -let is_conj flags ist = +let is_conj _ ist = + let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) && is_conjunction ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind - then - <:tactic<idtac>> - else - <:tactic<fail>> + then idtac + else fail + +let t_is_conj = register_tauto_tactic is_conj "is_conj" -let flatten_contravariant_conj flags ist = +let flatten_contravariant_conj _ ist = + let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in @@ -141,39 +194,38 @@ let flatten_contravariant_conj flags ist = ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let newtyp = valueIn (Value.of_constr (List.fold_right mkArrow args c)) in - let hyp = valueIn (Value.of_constr hyp) in - let intros = - iter_tac (List.map (fun _ -> <:tactic< intro >>) args) - <:tactic< idtac >> in - <:tactic< - let newtyp := $newtyp in - let hyp := $hyp in - assert newtyp by ($intros; apply hyp; split; assumption); - clear hyp - >> - | _ -> - <:tactic<fail>> + let newtyp = List.fold_right mkArrow args c in + let intros = tclMAP (fun _ -> intro) args in + let by = tclTHENLIST [intros; apply hyp; split; assumption] in + tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)] + | _ -> fail + +let t_flatten_contravariant_conj = + register_tauto_tactic flatten_contravariant_conj "flatten_contravariant_conj" (** Dealing with disjunction *) let constructor i = let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in + (** Take care of the index: this is the second entry in constructor. *) + let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in Tacexpr.TacML (Loc.ghost, name, [i]) -let is_disj flags ist = +let is_disj _ ist = + let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary t) && is_disjunction ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t - then - <:tactic<idtac>> - else - <:tactic<fail>> + then idtac + else fail + +let t_is_disj = register_tauto_tactic is_disj "is_disj" -let flatten_contravariant_disj flags ist = +let flatten_contravariant_disj _ ist = + let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in @@ -182,18 +234,19 @@ let flatten_contravariant_disj flags ist = ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let hyp = valueIn (Value.of_constr hyp) in - iter_tac (List.map_i (fun i arg -> - let typ = valueIn (Value.of_constr (mkArrow arg c)) in - let ci = constructor i in - <:tactic< - let typ := $typ in - let hyp := $hyp in - assert typ by (intro; apply hyp; $ci; assumption) - >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >> - | _ -> - <:tactic<fail>> - + let map i arg = + let typ = mkArrow arg c in + let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in + let by = tclTHENLIST [intro; apply hyp; ci; assumption] in + assert_ ~by typ + in + let tacs = List.mapi map args in + let tac0 = clear (destVar hyp) in + tclTHEN (tclTHENLIST tacs) tac0 + | _ -> fail + +let t_flatten_contravariant_disj = + register_tauto_tactic flatten_contravariant_disj "flatten_contravariant_disj" (** Main tactic *) @@ -204,9 +257,9 @@ let not_dep_intros ist = | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro end >> -let axioms flags ist = - let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags) - and t_is_empty = tacticIn is_empty in +let t_not_dep_intros = tacticIn not_dep_intros "not_dep_intros" + +let axioms ist = let c1 = constructor 1 in <:tactic< match reverse goal with @@ -215,14 +268,9 @@ let axioms flags ist = | _:?X1 |- ?X1 => assumption end >> +let t_axioms = tacticIn axioms "axioms" -let simplif flags ist = - let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags) - and t_is_conj = tacticIn (is_conj flags) - and t_flatten_contravariant_conj = tacticIn (flatten_contravariant_conj flags) - and t_flatten_contravariant_disj = tacticIn (flatten_contravariant_disj flags) - and t_is_disj = tacticIn (is_disj flags) - and t_not_dep_intros = tacticIn not_dep_intros in +let simplif ist = let c1 = constructor 1 in <:tactic< $t_not_dep_intros; @@ -259,11 +307,11 @@ let simplif flags ist = end; $t_not_dep_intros) >> -let rec tauto_intuit flags t_reduce solver = - let t_axioms = tacticIn (axioms flags) - and t_simplif = tacticIn (simplif flags) - and t_is_disj = tacticIn (is_disj flags) in - let lfun = make_lfun [("t_solver", solver)] in +let t_simplif = tacticIn simplif "simplif" + +let tauto_intuit flags t_reduce solver = + let flags = Genarg.in_gen (topwit wit_tauto_flags) flags in + let lfun = make_lfun [("t_solver", solver); ("tauto_flags", flags)] in let ist = { default_ist () with lfun = lfun; } in let vars = [Id.of_string "t_solver"] in (vars, ist, <:tactic< @@ -300,16 +348,16 @@ let reduction_not_iff _ist = | false, true -> <:tactic< unfold Coq.Init.Logic.iff in * >> | false, false -> <:tactic< idtac >> -let t_reduction_not_iff = tacticIn reduction_not_iff +let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff" let intuition_gen ist flags tac = - Proofview.Goal.enter begin fun gl -> + 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 eval_tactic_ist ist glb_intuition - end + end } let tauto_intuitionistic flags = Proofview.tclORELSE |