diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 48 | ||||
| -rw-r--r-- | tactics/auto.mli | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 8 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 8 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 37 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 4 | ||||
| -rw-r--r-- | tactics/eauto.ml | 28 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 3 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 4 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 12 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 9 | ||||
| -rw-r--r-- | tactics/eqschemes.mli | 12 | ||||
| -rw-r--r-- | tactics/equality.ml | 136 | ||||
| -rw-r--r-- | tactics/equality.mli | 24 | ||||
| -rw-r--r-- | tactics/hints.ml | 94 | ||||
| -rw-r--r-- | tactics/hints.mli | 19 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 96 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 7 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 14 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 10 | ||||
| -rw-r--r-- | tactics/inv.ml | 26 | ||||
| -rw-r--r-- | tactics/leminv.ml | 30 | ||||
| -rw-r--r-- | tactics/leminv.mli | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 20 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 37 | ||||
| -rw-r--r-- | tactics/tactics.ml | 444 | ||||
| -rw-r--r-- | tactics/tactics.mli | 23 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 38 | ||||
| -rw-r--r-- | tactics/term_dnet.mli | 2 |
29 files changed, 627 insertions, 574 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 7aa5114a4f..eec7a5f2ad 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -32,7 +32,7 @@ open Hints let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l let compute_secvars gl = - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in secvars_of_hyps hyps (* tell auto not to reuse already instantiated metas in unification (for @@ -187,35 +187,34 @@ let _ = add_option ["Info";"Trivial"] global_info_trivial; add_option ["Info";"Auto"] global_info_auto -let no_dbg () = (Off,0,ref []) +type debug_kind = ReportForTrivial | ReportForAuto + +let no_dbg (_,whatfor,_,_) = (Off,whatfor,0,ref []) let mk_trivial_dbg debug = let d = if debug == Debug || !global_debug_trivial then Debug else if debug == Info || !global_info_trivial then Info else Off - in (d,0,ref []) - -(** Note : we start the debug depth of auto at 1 to distinguish it - for trivial (whose depth is 0). *) + in (d,ReportForTrivial,0,ref []) let mk_auto_dbg debug = let d = if debug == Debug || !global_debug_auto then Debug else if debug == Info || !global_info_auto then Info else Off - in (d,1,ref []) + in (d,ReportForAuto,0,ref []) -let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace) +let incr_dbg = function (dbg,whatfor,depth,trace) -> (dbg,whatfor,depth+1,trace) (** A tracing tactic for debug/info trivial/auto *) -let tclLOG (dbg,depth,trace) pp tac = +let tclLOG (dbg,_,depth,trace) pp tac = match dbg with | Off -> tac | Debug -> (* For "debug (trivial/auto)", we directly output messages *) - let s = String.make depth '*' in + let s = String.make (depth+1) '*' in Proofview.V82.tactic begin fun gl -> try let out = Proofview.V82.of_tactic tac gl in @@ -256,23 +255,23 @@ and erase_subtree depth = function | (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l let pr_info_atom (d,pp) = - str (String.make (d-1) ' ') ++ pp () ++ str "." + str (String.make d ' ') ++ pp () ++ str "." let pr_info_trace = function - | (Info,_,{contents=(d,Some pp)::l}) -> + | (Info,_,_,{contents=(d,Some pp)::l}) -> Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_) -> Feedback.msg_info (str "idtac.") + | (Info,_,_,_) -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function - | (Off,_,_) -> () - | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)") - | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") - | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)") - | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)") + | (Off,_,_,_) -> () + | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)") + | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") + | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in @@ -317,7 +316,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = 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 + let decl = Tacmach.New.pf_last_hyp gl in let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list @@ -382,14 +381,14 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= (unify_resolve_gen poly flags (c,cl)) (* With "(debug) trivial", we shouldn't end here, and with "debug auto" we don't display the details of inner trivial *) - (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db) + (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db) | Unfold_nth c -> Proofview.Goal.enter begin fun gl -> if exists_evaluable_reference (Tacmach.New.pf_env gl) c then Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) else Tacticals.New.tclFAIL 0 (str"Unbound reference") end - | Extern tacast -> + | Extern tacast -> conclPattern concl p tacast in let pr_hint () = @@ -397,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint t ++ origin + let sigma, env = Pfedit.get_current_context () in + pr_hint env sigma t ++ origin in tclLOG dbg pr_hint (run_hint t tactic) @@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames = let delta_auto = if Flags.profile then - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n diff --git a/tactics/auto.mli b/tactics/auto.mli index b9cd4932ca..59809331e0 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -16,14 +16,14 @@ open Decl_kinds open Hints open Tactypes -val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t +val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - 'a Proofview.Goal.t -> clausenv * constr + Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ed612c0fc9..de98f63823 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,7 +9,7 @@ open Equality open Names open Pp -open Term +open Constr open Termops open CErrors open Util @@ -20,7 +20,7 @@ open Locus type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; - rew_ctx: Univ.universe_context_set; + rew_ctx: Univ.ContextSet.t; rew_l2r: bool; rew_tac: Genarg.glob_generic_argument option } @@ -73,12 +73,12 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index edbb7c6b71..44acf3c018 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -8,7 +8,7 @@ (** This files implements the autorewrite tactic. *) -open Term +open Constr open Equality (** Rewriting rules before tactic interpretation *) @@ -28,7 +28,7 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; - rew_ctx: Univ.universe_context_set; + rew_ctx: Univ.ContextSet.t; rew_l2r: bool; rew_tac: Genarg.glob_generic_argument option } @@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : string -> Pp.t +val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t open Clenv @@ -58,5 +58,5 @@ type hypinfo = { val find_applied_relation : ?loc:Loc.t -> bool -> - Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo + Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b98b103158..a95e6b941e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.enter begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (pf_concl gl) in + (pf_env gl) (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end in @@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = in tclFIRST (List.map tclCOMPLETE tacl) -and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl = +and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in @@ -467,24 +467,24 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> - str " with pattern " ++ Printer.pr_constr_pattern pat + str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat | _ -> mt () in match repr_hint t with - | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp)) - | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) + | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) + | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db secvars only_classes sigma concl = +and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes sigma concl + e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with Not_found -> [] -let e_possible_resolve db_list local_db secvars only_classes sigma concl = +let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd false only_classes sigma concl + e_my_find_search db_list local_db secvars hd false only_classes env sigma concl with Not_found -> [] let cut_of_hints h = @@ -718,7 +718,7 @@ module V85 = struct let concl = Goal.V82.concl s gl in let tacgl = {it = gl; sigma = s;} in let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in - let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in + let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in let unique = is_unique env s concl in let rec aux i foundone = function | (tac, _, extern, name, pp) :: tl -> @@ -996,7 +996,7 @@ module Search = struct Hint_db.transparent_state cached_hints == st then cached_hints else - let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g} + let hints = make_hints {it = Goal.goal g; sigma = project g} st only_classes sign in autogoal_cache := (cwd, only_classes, sign, hints); hints @@ -1041,7 +1041,6 @@ module Search = struct let fail_if_nonclass info = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in if is_class_type sigma (Proofview.Goal.concl gl) then Proofview.tclUNIT () @@ -1071,7 +1070,7 @@ module Search = struct else str" without backtracking")); let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal @@ -1089,7 +1088,7 @@ module Search = struct pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then - str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) else mt ()) in let msg = @@ -1110,7 +1109,7 @@ module Search = struct if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl'))); + pr_ev sigma' (Proofview.Goal.goal gl')); let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in let hints' = if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) @@ -1119,7 +1118,7 @@ module Search = struct make_autogoal_hints info.search_only_classes ~st gl' else info.search_hints in - let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in + let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in let info' = { search_depth = succ j :: i :: info.search_depth; last_tac = pp; @@ -1136,7 +1135,7 @@ module Search = struct (if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) ++ str", " ++ int j ++ str" subgoal(s)" ++ (Option.cata (fun k -> str " in addition to the first " ++ int k) (mt()) k))); @@ -1261,7 +1260,7 @@ module Search = struct if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") else - let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info @@ -1569,7 +1568,7 @@ let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = - let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env sigma gl in + let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in let (ev, _) = destEvar sigma t in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 5e2006ccc8..467754a848 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -53,7 +53,7 @@ let filter_hyp f tac = | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek hyps end @@ -98,7 +98,7 @@ let contradiction_context = end) | _ -> seek_neg rest in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek_neg hyps end diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2b5bbfcd1b..785d2f5150 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -10,13 +10,13 @@ open Pp open CErrors open Util open Names -open Nameops open Term open Termops open EConstr open Proof_type open Tacticals open Tacmach +open Evd open Tactics open Clenv open Auto @@ -32,7 +32,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let t2 = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) @@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) + (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end -and e_my_find_search sigma db_list local_db secvars hdc concl = +and e_my_find_search env sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in let hintl = List.map_append (fun db -> @@ -178,19 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - (tac, lazy (pr_hint t))) + (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl -and e_trivial_resolve sigma db_list local_db secvars gl = +and e_trivial_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in - try priority (e_my_find_search sigma db_list local_db secvars hd gl) + try priority (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve sigma db_list local_db secvars gl = +let e_possible_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) - (e_my_find_search sigma db_list local_db secvars hd gl) + (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] let find_first_goal gls = @@ -261,7 +261,7 @@ module SearchProblem = struct let g = find_first_goal lg in let hyps = pf_ids_of_hyps g in let secvars = secvars_of_hyps (pf_hyps g) in - let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in + let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ Id.print id)) in let assumption_tacs = let tacs = List.map map_assum hyps in let l = filter_tactics s.tacres tacs in @@ -290,7 +290,7 @@ module SearchProblem = struct let l = let concl = Reductionops.nf_evar (project g) (pf_concl g) in filter_tactics s.tacres - (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) + (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> @@ -404,8 +404,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; user_err Pp.(str "eauto: search failed") -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) +(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) +(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) @@ -439,7 +439,7 @@ let autounfolds db occs cls gl = in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in - let ids = Idset.filter (fun id -> List.mem id hyps) ids in + let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in Proofview.V82.of_tactic (unfold_option unfolds cls) gl diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 2d2a0c1b2a..e427adb15d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -13,7 +13,8 @@ (* This file builds schemes related to case analysis and recursion schemes *) -open Term +open Sorts +open Constr open Indrec open Declarations open Typeops diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index e3fe7ddae9..50b052f23b 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -13,10 +13,10 @@ open Ind_tables val optimize_non_type_induction_scheme : 'a Ind_tables.scheme_kind -> Indrec.dep_flag -> - Term.sorts_family -> + Sorts.family -> 'b -> Names.inductive -> - (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants + (Constr.constr * UState.t) * Safe_typing.private_constants val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index e16fcec7c7..8764ef085d 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -73,7 +73,7 @@ let generalize_right mk typ c1 c2 = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in Refine.refine ~typecheck:false begin fun sigma -> - let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in + let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in (sigma, mkApp (x, [|c2|])) @@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) = clear_last; intros] +let inj_flags = Some { + Equality.keep_proof_equalities = true; (* necessary *) + Equality.injection_in_context = true; (* does not matter here *) + Equality.injection_pattern_l2r_order = true; (* does not matter here *) + } + let discrHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in @@ -114,7 +120,7 @@ let idx = Id.of_string "x" let idy = Id.of_string "y" let mkGenDecideEqGoal rectype ops g = - let hypnames = pf_ids_of_hyps g in + let hypnames = pf_ids_set_of_hyps g in let xname = next_ident_away idx hypnames and yname = next_ident_away idy hypnames in (mkNamedProd xname rectype @@ -136,7 +142,7 @@ let eqCase tac = let injHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in - let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in + let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac let diseqCase hyps eqonleft = diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ce57682c66..d7667668e8 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -48,6 +48,7 @@ open CErrors open Util open Names open Term +open Constr open Vars open Declarations open Environ @@ -64,7 +65,7 @@ module RelDecl = Context.Rel.Declaration let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InProp | InSet -> hid | InType -> xid -let fresh env id = next_global_ident_away id [] +let fresh env id = next_global_ident_away id Id.Set.empty let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') @@ -106,8 +107,8 @@ let get_coq_eq ctx = let univ_of_eq env eq = let eq = EConstr.of_constr eq in - match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with - | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with + | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false) | _ -> assert false (**********************************************************************) @@ -141,7 +142,7 @@ let get_sym_eq_data env (ind,u) = let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in let paramsctxt1,_ = List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in - if not (List.equal Term.eq_constr params2 constrargs) then + if not (List.equal Constr.equal params2 constrargs) then error "Constructors arguments must repeat the parameters."; (* nrealargs_ctxt and nrealargs are the same here *) (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 4acfa7a281..90ae67c6cf 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -9,7 +9,7 @@ (** This file builds schemes relative to equality inductive types *) open Names -open Term +open Constr open Environ open Ind_tables @@ -22,14 +22,14 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_dep_scheme_kind : individual scheme_kind val rew_r2l_scheme_kind : individual scheme_kind -val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> +val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context -val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> +val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context * Safe_typing.private_constants val build_r2l_forward_rew_scheme : - bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context + bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : - bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context + bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context (** Builds a symmetry scheme for a symmetrical equality type *) @@ -43,5 +43,5 @@ val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) val congr_scheme_kind : individual scheme_kind -val build_congr : env -> constr * constr * Univ.universe_context_set -> inductive -> +val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive -> constr Evd.in_evar_universe_context diff --git a/tactics/equality.ml b/tactics/equality.ml index 3ea9538f38..9a1ac768c7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration (* Options *) +type inj_flags = { + keep_proof_equalities : bool; + injection_in_context : bool; + injection_pattern_l2r_order : bool; + } + let discriminate_introduction = ref true let discr_do_intro () = !discriminate_introduction @@ -63,7 +69,9 @@ let _ = let injection_pattern_l2r_order = ref true -let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order +let use_injection_pattern_l2r_order = function + | None -> !injection_pattern_l2r_order + | Some flags -> flags.injection_pattern_l2r_order let _ = declare_bool_option @@ -75,9 +83,9 @@ let _ = let injection_in_context = ref false -let use_injection_in_context () = - !injection_in_context - && Flags.version_strictly_greater Flags.V8_5 +let use_injection_in_context = function + | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | Some flags -> flags.injection_in_context let _ = declare_bool_option @@ -258,7 +266,7 @@ let rewrite_elim with_evars frzevars cls c e = end let tclNOTSAMEGOAL tac = - let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in + let goal gl = Proofview.Goal.goal gl in Proofview.Goal.nf_enter begin fun gl -> let sigma = project gl in let ev = goal gl in @@ -316,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = in let typ = match cls with | None -> pf_concl gl - | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl) + | Some id -> pf_get_hyp_typ id gl in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) @@ -366,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot = | Some true, None | Some false, Some _ -> let c1 = destConstRef pr1 in - let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in + let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in + let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in begin try let _ = Global.lookup_constant c1' in c1' with Not_found -> user_err ~hdr:"Equality.find_elim" - (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") + (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end | _ -> destConstRef pr1 end @@ -721,10 +729,17 @@ let _ = optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } -let find_positions env sigma ~no_discr t1 t2 = +let keep_proof_equalities = function + | None -> !keep_proof_equalities_for_injection + | Some flags -> flags.keep_proof_equalities + +(* [keep_proofs] is relevant for types in Prop with elimination in Type *) +(* In particular, it is relevant for injection but not for discriminate *) + +let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in - let s = get_sort_family_of env sigma ty1 in + let s = get_sort_family_of ~truncation_style:true env sigma ty1 in if Sorts.List.mem s sorts then [(List.rev posn,t1,t2)] else [] in @@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 = project env sorts posn t1_0 t2_0 in try - let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp] - else [InSet;InType] - in + let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in Inr (findrec sorts [] t1 t2) with DiscrFound (path,c1,c2) -> Inl (path,c1,c2) +let use_keep_proofs = function + | None -> !keep_proof_equalities_for_injection + | Some b -> b + let discriminable env sigma t1 t2 = - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with | Inl _ -> true | _ -> false -let injectable env sigma t1 t2 = - match find_positions env sigma ~no_discr:true t1 t2 with +let injectable env sigma ~keep_proofs t1 t2 = + match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with | Inl _ -> assert false | Inr [] | Inr [([],_,_)] -> false | Inr _ -> true @@ -953,7 +970,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in + let hyp_typ = pf_get_hyp_typ id gl in if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) @@ -1003,7 +1020,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = try @@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with | Inr _ -> tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> @@ -1069,9 +1086,8 @@ let discr with_evars = onEquality with_evars discrEq let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = -(* - tclORELSE -*) + tclTHEN (Proofview.tclUNIT ()) + (* Delay the interpretation of side-effect *) (if discr_do_intro () then (tclTHEN (tclREPEAT introf) @@ -1079,9 +1095,7 @@ let discrEverywhere with_evars = (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) else (* <= 8.2 compat *) tryAllHypsAndConcl (discrSimpleClause with_evars)) -(* (fun gls -> - user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities.")) -*) + let discr_tac with_evars = function | None -> discrEverywhere with_evars | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c @@ -1371,7 +1385,7 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = @@ -1403,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) -let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in - match find_positions env sigma ~no_discr:true t1 t2 with + match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with | Inl _ -> assert false | Inr [] -> let suggestion = - if !keep_proof_equalities_for_injection then + if keep_proofs then "" else " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) @@ -1422,21 +1436,22 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) + | [] -> raise (RefinerError (env, sigma, NoSuchHyp id)) | d :: right -> let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + aux MoveLast (Proofview.Goal.hyps gl) -let injEq ?(old=false) with_evars clear_flag ipats = +let injEq flags ?(old=false) with_evars clear_flag ipats = (* Decide which compatibility mode to use *) let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with - | None when not old && use_injection_in_context () -> + | None when not old && use_injection_in_context flags -> Some [], true, true, true | None -> None, false, false, false - | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in + | _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in (* Built the post tactic depending on compatibility mode *) let post_tac c n = match ipats_style with @@ -1456,26 +1471,26 @@ let injEq ?(old=false) with_evars clear_flag ipats = tclTHEN clear_tac intro_tac end | None -> tclIDTAC in - injEqThen post_tac l2r + injEqThen (keep_proof_equalities flags) post_tac l2r -let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats) +let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats) -let injClause ipats with_evars = function - | None -> onNegatedEquality with_evars (injEq with_evars None ipats) - | Some c -> onInductionArg (inj ipats with_evars) c +let injClause flags ipats with_evars = function + | None -> onNegatedEquality with_evars (injEq flags with_evars None ipats) + | Some c -> onInductionArg (inj flags ipats with_evars) c -let simpleInjClause with_evars = function - | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None) - | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c +let simpleInjClause flags with_evars = function + | None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c -let injConcl = injClause None false None -let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) +let injConcl flags = injClause flags None false None +let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> discr_positions env sigma u clause cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) @@ -1485,18 +1500,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = (ntac (clenv_value clause)) end -let dEqThen with_evars ntac = function - | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) - | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c +let dEqThen ~keep_proofs with_evars ntac = function + | None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None)) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c -let dEq with_evars = - dEqThen with_evars (fun clear_flag c x -> +let dEq ~keep_proofs with_evars = + dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decomp_eq tac data (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen (fun _ -> tac) data cl + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl end let _ = declare_intro_decomp_eq intro_decomp_eq @@ -1568,7 +1583,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) - let expected_goal = nf_betaiota sigma expected_goal in + let expected_goal = nf_betaiota env sigma expected_goal in (* 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 @@ -1701,8 +1716,8 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in (* The set of hypotheses using x *) let dephyps = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> @@ -1734,7 +1749,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let decl = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else @@ -1746,7 +1760,7 @@ let subst_one_var dep_proof_ok x = let test hyp _ = is_eq_x gl x hyp in Context.Named.fold_outside test ~init:() hyps; user_err ~hdr:"Subst" - (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in subst_one dep_proof_ok x res @@ -1775,7 +1789,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* First step: find hypotheses to treat in linear time *) let find_equations gl = - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = project gl in let find_eq_data_decompose = find_eq_data_decompose gl in @@ -1801,7 +1814,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* Second step: treat equations *) let process hyp = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in @@ -1810,9 +1822,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) -> + | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) -> + | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () diff --git a/tactics/equality.mli b/tactics/equality.mli index a4d1c0f9bd..65da2e7dc0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -67,23 +67,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta val replace : constr -> constr -> unit Proofview.tactic val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic +type inj_flags = { + keep_proof_equalities : bool; (* One may want it or not *) + injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *) + injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *) + } + val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val inj : intro_patterns option -> evars_flag -> + +(* Below, if flag is [None], it takes the value from the dynamic value of the option *) +val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic -val injClause : intro_patterns option -> evars_flag -> +val injClause : inj_flags option -> intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val injHyp : clear_flag -> Id.t -> unit Proofview.tactic -val injConcl : unit Proofview.tactic -val simpleInjClause : evars_flag -> +val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic +val injConcl : inj_flags option -> unit Proofview.tactic +val simpleInjClause : inj_flags option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) @@ -100,7 +108,7 @@ val rewriteInConcl : bool -> constr -> unit Proofview.tactic val discriminable : env -> evar_map -> constr -> constr -> bool (* Tells if tactic "injection" is applicable *) -val injectable : env -> evar_map -> constr -> constr -> bool +val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool (* Subst *) diff --git a/tactics/hints.ml b/tactics/hints.ml index a572508d47..7f9b5ef34e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -56,7 +56,9 @@ let head_constr_bound sigma t = | _ -> raise Bound let head_constr sigma c = - try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.") + try head_constr_bound sigma c + with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \ + (co)inductive type, (co)inductive type constructor, or projection.") let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in @@ -126,14 +128,14 @@ type hints_path = global_reference hints_path_gen type hint_term = | IsGlobRef of global_reference - | IsConstr of constr * Univ.universe_context_set + | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { obj : 'a; uid : KerName.t; } -type raw_hint = constr * types * Univ.universe_context_set +type raw_hint = constr * types * Univ.ContextSet.t type hint = (raw_hint * clausenv) hint_ast with_uid @@ -764,7 +766,9 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> user_err Pp.(str "Bound head variable.") + with BoundPattern -> + user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \ + an if, case, or let expression, an application, or a projection.") let with_uid c = { obj = c; uid = fresh_key () } @@ -1388,39 +1392,34 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt (c, _, _) = pr_econstr c +let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c -let pr_hint h = match h.obj with - | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c) - | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c) - | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) +let pr_hint env sigma h = match h.obj with + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> - (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") + | Unfold_nth c -> + str"unfold " ++ pr_evaluable_reference c | Extern tac -> - let env = - try - let (_, env) = Pfedit.get_current_goal_context () in - env - with e when CErrors.noncritical e -> Global.env () - in - (str "(*external*) " ++ Pputils.pr_glb_generic env tac) + str "(*external*) " ++ Pputils.pr_glb_generic env tac -let pr_id_hint (id, v) = - let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in - (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat +let pr_id_hint env sigma (id, v) = + let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in + (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat ++ str", id " ++ int id ++ str ")" ++ spc ()) -let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) +let pr_hint_list env sigma hintlist = + (str " " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ()) -let pr_hints_db (name,db,hintlist) = +let pr_hints_db env sigma (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ if List.is_empty hintlist then (str " nothing" ++ fnl ()) - else (fnl () ++ pr_hint_list hintlist)) + else (fnl () ++ pr_hint_list env sigma hintlist)) (* Print all hints associated to head c in any database *) -let pr_hint_list_for_head c = +let pr_hint_list_for_head env sigma c = let dbs = current_db () in let validate (name, db) = let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in @@ -1432,13 +1431,13 @@ let pr_hint_list_for_head c = else hov 0 (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let pr_hint_term sigma cl = +let pr_hint_term env sigma cl = try let dbs = current_db () in let valid_dbs = @@ -1456,18 +1455,19 @@ let pr_hint_term sigma cl = (str "No hint applicable for current goal") else (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = + let env = Global.env () in let pts = Proof_global.give_me_the_proof () in - let glss = Proof.V82.subgoals pts in - match glss.Evd.it with + let glss,_,_,_,sigma = Proof.proof pts in + match glss with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> - pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) + pr_hint_term env sigma (Goal.V82.concl sigma g) let pp_hint_mode = function | ModeInput -> str"+" @@ -1475,9 +1475,9 @@ let pp_hint_mode = function | ModeOutput -> str"-" (* displays the whole hint database db *) -let pr_hint_db db = +let pr_hint_db_env env sigma db = let pr_mode = prvect_with_sep spc pp_hint_mode in - let pr_modes l = + let pr_modes l = if List.is_empty l then mt () else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")" in @@ -1487,7 +1487,7 @@ let pr_hint_db db = | None -> str "For any goal" | Some head -> str "For " ++ pr_global head ++ pr_modes modes in - let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in + let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in accu ++ hint_descr in @@ -1502,17 +1502,22 @@ let pr_hint_db db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content -let pr_hint_db_by_name dbname = +(* Deprecated in the mli *) +let pr_hint_db db = + let sigma, env = Pfedit.get_current_context () in + pr_hint_db_env env sigma db + +let pr_hint_db_by_name env sigma dbname = try - let db = searchtable_map dbname in pr_hint_db db + let db = searchtable_map dbname in pr_hint_db_env env sigma db with Not_found -> error_no_such_hint_database dbname (* displays all the hints of all databases *) -let pr_searchtable () = +let pr_searchtable env sigma = let fold name db accu = accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++ - pr_hint_db db ++ fnl () + pr_hint_db_env env sigma db ++ fnl () in Hintdbmap.fold fold !searchtable (mt ()) @@ -1530,10 +1535,13 @@ let warn_non_imported_hint = strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) let warn h x = - let hint = pr_hint h in - let (mp, _, _) = KerName.repr h.uid in - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT x + let open Proofview in + tclBIND tclENV (fun env -> + tclBIND tclEVARMAP (fun sigma -> + let hint = pr_hint env sigma h in + let (mp, _, _) = KerName.repr h.uid in + warn_non_imported_hint (hint,mp); + Proofview.tclUNIT x)) let run_hint tac k = match !warn_hint with | `LAX -> k tac.obj diff --git a/tactics/hints.mli b/tactics/hints.mli index 44e5370e93..cbf204981e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -42,7 +42,7 @@ type 'a hint_ast = | Extern of Genarg.glob_generic_argument (* Hint Extern *) type hint -type raw_hint = constr * types * Univ.universe_context_set +type raw_hint = constr * types * Univ.ContextSet.t type 'a hints_path_atom_gen = | PathHints of 'a list @@ -146,7 +146,7 @@ type hint_info = (patvar list * constr_pattern) hint_info_gen type hint_term = | IsGlobRef of global_reference - | IsConstr of constr * Univ.universe_context_set + | IsConstr of constr * Univ.ContextSet.t type hints_entry = | HintsResolveEntry of @@ -193,7 +193,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> *) val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. [eapply] is true if this hint will be used only with EApply; @@ -211,7 +211,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint val make_apply_entry : env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product @@ -260,14 +260,15 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> Pp.t +val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : global_reference -> Pp.t -val pr_hint_db_by_name : hint_db_name -> Pp.t +val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t +val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t -val pr_hint : hint -> Pp.t +[@@ocaml.deprecated "please used pr_hint_db_env"] +val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) - val add_hints_init : (unit -> unit) -> unit diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b057cf72bc..2bb9be66ba 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -39,7 +39,6 @@ type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let meta3 = mkmeta 3 let op2bool = function Some _ -> true | None -> false @@ -49,7 +48,7 @@ let match_with_non_recursive_type sigma t = let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then + if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then Some (hdapp,args) else None @@ -89,6 +88,12 @@ let is_lax_conjunction = function let prod_assum sigma t = fst (decompose_prod_assum sigma t) +(* whd_beta normalize the types of arguments in a product *) +let rec whd_beta_prod sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c) + | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) + | _ -> c + let match_with_one_constructor sigma style onlybinary allow_rec t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with @@ -112,7 +117,9 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = Some (hdapp,args) else None else - let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in + let ctyp = whd_beta_prod sigma + (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) + (EConstr.of_constr mip.mind_nf_lc.(0)) args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -160,7 +167,7 @@ let test_strict_disjunction n lc = let open Term in Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with - | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) + | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) | _ -> false) 0 lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = @@ -252,16 +259,16 @@ open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) -let mkGApp f args = CAst.make @@ GApp (f, args) -let mkGHole = CAst.make @@ +let mkGApp f args = DAst.make @@ GApp (f, args) +let mkGHole = DAst.make @@ GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) -let mkGProd id c1 c2 = CAst.make @@ +let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) -let mkGArrow c1 c2 = CAst.make @@ +let mkGArrow c1 c2 = DAst.make @@ GProd (Anonymous, Explicit, c1, c2) -let mkGVar id = CAst.make @@ GVar (Id.of_string id) -let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id)) -let mkGRef r = CAst.make @@ GRef (Lazy.force r, None) +let mkGVar id = DAst.make @@ GVar (Id.of_string id) +let mkGPatVar id = DAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id)) +let mkGRef r = DAst.make @@ GRef (Lazy.force r, None) let mkGAppRef r args = mkGApp (mkGRef r) args (** forall x : _, _ x x *) @@ -365,36 +372,39 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) let match_with_nodep_ind sigma t = let (hdapp,args) = decompose_app sigma t in - match EConstr.kind sigma hdapp with - | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in - if Array.length (mib.mind_packets)>1 then None else - let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in - if Array.for_all nodep_constr mip.mind_nf_lc then - let params= - if Int.equal mip.mind_nrealargs 0 then args else - fst (List.chop mib.mind_nparams args) in - Some (hdapp,params,mip.mind_nrealargs) - else - None - | _ -> None + match EConstr.kind sigma hdapp with + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in + if Array.length (mib.mind_packets)>1 then None else + let nodep_constr c = + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in + if Array.for_all nodep_constr mip.mind_nf_lc then + let params= + if Int.equal mip.mind_nrealargs 0 then args else + fst (List.chop mib.mind_nparams args) in + Some (hdapp,params,mip.mind_nrealargs) + else + None + | _ -> None let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) let match_with_sigma_type sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in - if Int.equal (Array.length (mib.mind_packets)) 1 && - (Int.equal mip.mind_nrealargs 0) && - (Int.equal (Array.length mip.mind_consnames)1) && - has_nodep_prod_after (mib.mind_nparams+1) sigma (EConstr.of_constr mip.mind_nf_lc.(0)) then - (*allowing only 1 existential*) - Some (hdapp,args) - else - None - | _ -> None + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in + if Int.equal (Array.length (mib.mind_packets)) 1 + && (Int.equal mip.mind_nrealargs 0) + && (Int.equal (Array.length mip.mind_consnames)1) + && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma + (EConstr.of_constr mip.mind_nf_lc.(0)) + then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t) @@ -460,22 +470,6 @@ let find_this_eq_data_decompose gl eqn = user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) -let match_eq_nf gls eqn (ref, hetero) = - let n = if hetero then 4 else 3 in - let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in - let pat = mkPattern (mkGAppRef ref args) in - match Id.Map.bindings (pf_matches gls pat eqn) with - | [(m1,t);(m2,x);(m3,y)] -> - assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - user_err Pp.(str "Not an equality.") - (*** Sigma-types *) let match_sigma env sigma ex = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c6..01d916053c 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -120,11 +120,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 : 'a Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 7f087ea01a..bc2fea2bd5 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -17,7 +17,7 @@ open Mod_subst open Libobject open Nameops open Declarations -open Term +open Constr open CErrors open Util open Declare @@ -29,7 +29,7 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants @@ -57,7 +57,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let inScheme : string * (inductive * constant) array -> obj = +let inScheme : string * (inductive * Constant.t) array -> obj = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); @@ -121,12 +121,10 @@ let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = Evd.normalize_evar_universe_context univs in - let c = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let univs = Evd.evar_context_universe_context ctx in + let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in let univs = - if p then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if p then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) in let entry = { const_entry_body = diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index f825c4f4a3..d73595a2f8 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names +open Constr open Declare (** This module provides support for registering inductive scheme builders, @@ -20,7 +20,7 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Safe_typing.private_constants + Id.t option -> inductive -> Constant.t * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants + (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 9495ca9c55..5435b63ce1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Nameops open Term open Termops open EConstr @@ -78,7 +77,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Dep dflt_concl -> if not (occur_var env !evd id concl) then user_err ~hdr:"make_inv_predicate" - (str "Current goal does not depend on " ++ pr_id id ++ str"."); + (str "Current goal does not depend on " ++ Id.print id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) @@ -283,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id = let error_too_many_names pats = let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") let get_names (allow_conj,issimple) (loc, pat as x) = match pat with @@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) @@ -343,8 +353,8 @@ let projectAndApply as_mode thin avoid id eqname names depids = Proofview.Goal.enter begin fun gl -> let sigma = project gl in (** 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 + let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 @@ -371,7 +381,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) (fun id -> - dEqThen false (deq_trailer id) + dEqThen ~keep_proofs:None false (deq_trailer id) (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) id @@ -387,7 +397,7 @@ let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.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 NamedDecl.get_id nodepids else [] in + let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> tclTHENLIST @@ -442,7 +452,7 @@ let raw_inversion inv_kind id status names = let (ind, t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> - let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in + let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg in let IndType (indf,realargs) = find_rectype env sigma t in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index aeb80ae57c..197b3030d9 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -142,7 +142,7 @@ let rec add_prods_sign env sigma t = let compute_first_inversion_scheme env sigma ind sort dep_option = let indf,realargs = dest_ind_type ind in - let allvars = ids_of_context env in + let allvars = vars_of_env env in let p = next_ident_away (Id.of_string "P") allvars in let pty,goal = if dep_option then @@ -214,15 +214,15 @@ let inversion_scheme env sigma t sort dep_option inv_op = else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in - let avoid = ref [] in - let { sigma=sigma } = Proof.V82.subgoals pf in + let avoid = ref Id.Set.empty in + let _,_,_,_,sigma = Proof.proof pf in let sigma = Evd.nf_constraints sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in - avoid := h::!avoid; + avoid := Id.Set.add h !avoid; ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign; applist (mkVar h, inst) | _ -> EConstr.map sigma fill_holes c @@ -232,25 +232,27 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context sigma + p, sigma -let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs:(snd ctx) invProof in +let add_inversion_lemma ~poly name env sigma t sort dep inv_op = + let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in + let univs = + Evd.const_univ_entry ~poly sigma + in + let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) -let add_inversion_lemma_exn na com comsort bool tac = +let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in - let evd = ref (Evd.from_env env) in - let c = Constrintern.interp_type_evars env evd com in - let sigma, sort = Pretyping.interp_sort !evd comsort in + let sigma = Evd.from_env env in + let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env sigma c sort bool tac + add_inversion_lemma ~poly na env sigma c sort bool tac with | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) user_err ~hdr:"Inv needs Nodep Prop Set" s diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 41b0e09b42..f221b1fd9a 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -14,6 +14,6 @@ open Misctypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val add_inversion_lemma_exn : - Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) -> +val add_inversion_lemma_exn : poly:bool -> + Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bce0dda10c..e7da17cff1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -10,7 +10,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open EConstr open Termops open Declarations @@ -224,9 +224,8 @@ let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures isrec ((_,k as ity),u) = - let open Term in let rec analrec c recargs = - match kind_of_term c, recargs with + match Constr.kind c, recargs with | Prod (_,_,c), recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with @@ -242,7 +241,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in let lc = - Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in + Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs @@ -472,7 +471,7 @@ module New = struct let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) - | Evd.Evar_defined c -> match Term.kind_of_term c with + | Evd.Evar_defined c -> match Constr.kind c with | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an @@ -541,7 +540,6 @@ module New = struct let nthHypId m gl = (** We only use [id] *) - let gl = Proofview.Goal.assume gl in nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -573,7 +571,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in tac rem end @@ -622,8 +620,8 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> string_of_con kn - | Var id -> string_of_id id + | Const (kn, _) -> Constant.to_string kn + | Var id -> Id.to_string id | _ -> "\b" in user_err ~hdr:"Tacticals.general_elim_then_using" @@ -659,12 +657,12 @@ module New = struct let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) - let c = Proofview.Goal.concl (Goal.assume gl) in + let c = Proofview.Goal.concl gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_hyp id gl = (** Retyping will expand evars anyway. *) - let c = pf_get_hyp_typ id (Goal.assume gl) in + let c = pf_get_hyp_typ id gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_clause id gl = match id with diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2a04c413be..c5d5c8c123 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -7,9 +7,9 @@ (************************************************************************) open Names -open Term +open Constr open EConstr -open Tacmach +open Evd open Proof_type open Locus open Misctypes @@ -23,6 +23,7 @@ val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENSEQ : tactic list -> tactic +[@@ocaml.deprecated "alias of Tacticals.tclTHENLIST"] val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENFIRST : tactic -> tactic -> tactic @@ -127,9 +128,9 @@ val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list arr val compute_induction_names : bool list array -> or_and_intro_pattern option -> intro_patterns array -val elimination_sort_of_goal : goal sigma -> sorts_family -val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family -val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family +val elimination_sort_of_goal : goal sigma -> Sorts.family +val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family +val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic @@ -224,28 +225,28 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : 'a Proofview.Goal.t -> int -> named_context + val nLastDecls : Proofview.Goal.t -> int -> named_context - val ifOnHyp : (identifier * types -> bool) -> - (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> - identifier -> unit Proofview.tactic + val ifOnHyp : (Id.t * types -> bool) -> + (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> + Id.t -> unit Proofview.tactic - val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic - val onLastHypId : (identifier -> unit tactic) -> unit tactic + val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic + val onLastHypId : (Id.t -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `LZ ] Proofview.Goal.t -> named_context) -> + val onHyps : (Proofview.Goal.t -> named_context) -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic - val tryAllHyps : (identifier -> unit tactic) -> unit tactic - val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic - val onClause : (identifier option -> unit tactic) -> clause -> unit tactic + val tryAllHyps : (Id.t -> unit tactic) -> unit tactic + val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic + val onClause : (Id.t 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 : Proofview.Goal.t -> Sorts.family + val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family + val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family val elimination_then : (branch_args -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bc55d3fe..7e281e2fe0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -14,6 +14,7 @@ open Util open Names open Nameops open Term +open Constr open Termops open Environ open EConstr @@ -58,28 +59,6 @@ let typ_of env sigma c = open Goptions -(* Option for 8.2 compatibility *) -let dependent_propositions_elimination = ref true - -let use_dependent_propositions_elimination () = - !dependent_propositions_elimination - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "dependent-propositions-elimination tactic"; - optkey = ["Dependent";"Propositions";"Elimination"]; - optread = (fun () -> !dependent_propositions_elimination) ; - optwrite = (fun b -> dependent_propositions_elimination := b) } - -let _ = - declare_bool_option - { optdepr = false; - optname = "trigger bugged context matching compatibility"; - optkey = ["Tactic";"Compat";"Context"]; - optread = (fun () -> !Flags.tactic_context_compat) ; - optwrite = (fun b -> Flags.tactic_context_compat := b) } - let apply_solve_class_goals = ref false let _ = @@ -172,7 +151,6 @@ let unsafe_intro env store decl b = let introduction ?(check=true) id = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in @@ -180,13 +158,13 @@ let introduction ?(check=true) id = let env = Proofview.Goal.env gl in let () = if check && mem_named_context_val id hyps then user_err ~hdr:"Tactics.introduction" - (str "Variable " ++ pr_id id ++ str " is already declared.") + (str "Variable " ++ Id.print id ++ str " is already declared.") in let open Context.Named.Declaration in match EConstr.kind sigma concl with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b - | _ -> raise (RefinerError IntroNeedsProduct) + | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end let refine = Tacmach.refine @@ -243,11 +221,11 @@ let convert_leq x y = convert_gen Reduction.CUMUL x y let clear_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> - pr_id id ++ str " is used in conclusion." + Id.print id ++ str " is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str"." + Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> - str "Cannot remove " ++ pr_id id ++ + str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." @@ -256,12 +234,12 @@ let error_clear_dependency env sigma id err = let replacing_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> - str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion." + str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - str "Cannot change " ++ pr_id id ++ - strbrk ", it is used in hypothesis " ++ pr_id id' ++ str"." + str "Cannot change " ++ Id.print id ++ + strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> - str "Cannot change " ++ pr_id id ++ + str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." @@ -279,7 +257,6 @@ let clear_gen fail = function Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in (** clear_hyps_in_evi does not require nf terms *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -318,7 +295,7 @@ let move_hyp id dest = let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in - let sign' = move_hyp_in_named_context sigma id dest sign in + let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty @@ -343,23 +320,24 @@ let rename_hyp repl = | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> Proofview.Goal.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 let store = Proofview.Goal.extra gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in (** Check that we do not mess variables *) let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then let hyp = Id.Set.choose (Id.Set.diff src vars) in - raise (RefinerError (NoSuchHyp hyp)) + raise (RefinerError (env, sigma, NoSuchHyp hyp)) in let mods = Id.Set.diff vars src in let () = try let elt = Id.Set.choose (Id.Set.inter dst mods) in - CErrors.user_err (pr_id elt ++ str " is already used") + CErrors.user_err (Id.print elt ++ str " is already used") with Not_found -> () in (** All is well *) @@ -384,7 +362,9 @@ let rename_hyp repl = (**************************************************************) let fresh_id_in_env avoid id env = - next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env)) + let avoid' = ids_of_named_context_val (named_context_val env) in + let avoid = if Id.Set.is_empty avoid then avoid' else Id.Set.union avoid' avoid in + next_ident_away_in_goal id avoid let fresh_id avoid id gl = fresh_id_in_env avoid id (pf_env gl) @@ -412,12 +392,12 @@ let default_id env sigma decl = possibly a move to do after the introduction *) type name_flag = - | NamingAvoid of Id.t list - | NamingBasedOn of Id.t * Id.t list + | NamingAvoid of Id.Set.t + | NamingBasedOn of Id.t * Id.Set.t | NamingMustBe of Id.t Loc.located let naming_of_name = function - | Anonymous -> NamingAvoid [] + | Anonymous -> NamingAvoid Id.Set.empty | Name id -> NamingMustBe (Loc.tag id) let find_name mayrepl decl naming gl = match naming with @@ -429,19 +409,19 @@ let find_name mayrepl decl naming gl = match naming with | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in let id' = next_ident_away id ids_of_hyps in if not mayrepl && not (Id.equal id' id) then - user_err ?loc (pr_id id ++ str" is already used."); + user_err ?loc (Id.print id ++ str" is already used."); id (**************************************************************) (* Computing position of hypotheses for replacing *) (**************************************************************) -let get_next_hyp_position id = +let get_next_hyp_position env sigma id = let rec aux = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> if Id.equal (NamedDecl.get_id decl) id then match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst @@ -450,9 +430,9 @@ let get_next_hyp_position id = in aux -let get_previous_hyp_position id = +let get_previous_hyp_position env sigma id = let rec aux dest = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right @@ -480,15 +460,15 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign = named_context_val env in let sign',t,concl,sigma = if replace then - let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else (if check && mem_named_context_val id sign then - user_err (str "Variable " ++ pr_id id ++ str " is already declared."); + user_err (str "Variable " ++ Id.print id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in - let nf_t = nf_betaiota sigma t in + let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> @@ -578,11 +558,11 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> | (f, n, ar) :: oth -> let open Context.Named.Declaration in let (sp', u') = check_mutind env sigma n ar in - if not (eq_mind sp sp') then + if not (MutInd.equal sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" - (str "Name " ++ pr_id f ++ str " already used in the environment"); + (str "Name " ++ Id.print f ++ str " already used in the environment"); mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in @@ -603,7 +583,7 @@ let fix ido n = match ido with | None -> Proofview.Goal.enter begin fun gl -> let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id [] name gl in + let id = new_fresh_id Id.Set.empty name gl in mutual_fix id n [] 0 end | Some id -> @@ -654,7 +634,7 @@ let cofix ido = match ido with | None -> Proofview.Goal.enter begin fun gl -> let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id [] name gl in + let id = new_fresh_id Id.Set.empty name gl in mutual_cofix id [] 0 end | Some id -> @@ -672,7 +652,7 @@ let pf_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); LocalAssum (id,redfun' ty) | LocalDef (id,b,ty) -> let b' = if where != InHypTypeOnly then redfun' b else b in @@ -773,7 +753,7 @@ let pf_e_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); let (sigma, ty') = redfun sigma ty in (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> @@ -816,7 +796,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); let (sigma, ty') = redfun false env sigma ty in (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> @@ -831,13 +811,13 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm let e_change_in_hyp redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let hyp = Tacmach.New.pf_get_hyp id gl in let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp c) end -type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr +type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) @@ -942,10 +922,14 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = - let trace () = + let trace env sigma = let open Printer in - let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in - Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) + let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in + Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp)) + in + let trace () = + let sigma, env = Pfedit.get_current_context () in + trace env sigma in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> @@ -975,13 +959,13 @@ let unfold_constr = function the type to build hyp names, we maintain an environment to be able to type dependent hyps. *) let find_intro_names ctxt gl = - let _, res = List.fold_right + let _, res, _ = List.fold_right (fun decl acc -> - let env,idl = acc in - let name = fresh_id idl (default_id env gl.sigma decl) gl in + let env,idl,avoid = acc in + let name = fresh_id avoid (default_id env gl.sigma decl) gl in let newenv = push_rel decl env in - (newenv,(name::idl))) - ctxt (pf_env gl , []) in + (newenv, name :: idl, Id.Set.add name avoid)) + ctxt (pf_env gl, [], Id.Set.empty) in List.rev res let build_intro_tac id dest tac = match dest with @@ -993,7 +977,8 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let env = Tacmach.New.pf_env gl in + let concl = Proofview.Goal.concl gl in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in @@ -1002,7 +987,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> - begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) + begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) (* this since at least V6.3 (a pity *) (* that intro do betaiotazeta only when reduction is needed; and *) @@ -1013,7 +998,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end @@ -1021,18 +1006,18 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = 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 (Loc.tag id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false +let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false -let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false -let intro = intro_gen (NamingAvoid []) MoveLast false false -let introf = intro_gen (NamingAvoid []) MoveLast true false +let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false +let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false +let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto true false | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false -let intro_move idopt hto = intro_move_avoid idopt [] hto +let intro_move idopt hto = intro_move_avoid idopt Id.Set.empty hto (**** Multiple introduction tactics ****) @@ -1052,7 +1037,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = (fun id -> aux (n+1) (id::ids)) end begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> tac ids | e -> Proofview.tclZERO ~info e end @@ -1063,8 +1048,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let next_hyp = get_next_hyp_position id hyps in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let hyps = Proofview.Goal.hyps gl in + let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1083,8 +1069,9 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let hyps = Proofview.Goal.hyps gl in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1097,8 +1084,9 @@ let intros_possibly_replacing ids = (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let hyps = Proofview.Goal.hyps gl in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -1130,7 +1118,7 @@ let is_quantified_hypothesis id gl = let msg_quantified_hypothesis = function | NamedHyp id -> - str "quantified hypothesis named " ++ pr_id id + str "quantified hypothesis named " ++ Id.print id | AnonHyp n -> pr_nth n ++ str " non dependent hypothesis" @@ -1159,7 +1147,7 @@ let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = Proofview.Goal.enter begin fun gl -> - let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let _ = Tacmach.New.pf_get_hyp id gl in Proofview.tclUNIT () end @@ -1202,7 +1190,7 @@ let onOpenInductionArg env sigma tac = function let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(c,NoBindings)) end)) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -1218,7 +1206,7 @@ let onInductionArg tac = function Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -1264,7 +1252,7 @@ let cut c = with e when Pretype_errors.precatchable_exception e -> false in if is_sort then - let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in + let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in Refine.refine ~typecheck:false begin fun h -> @@ -1281,14 +1269,14 @@ let error_uninstantiated_metas t clenv = let t = EConstr.Unsafe.to_constr t in let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") - in user_err (str "Cannot find an instance for " ++ pr_id id ++ str".") + in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".") let check_unresolved_evars_of_metas sigma clenv = (* This checks that Metas turned into Evars by *) (* Refiner.pose_all_metas_as_evars are resolved *) List.iter (fun (mv,b) -> match b with | Clval (_,(c,_),_) -> - (match kind_of_term c.rebus with + (match Constr.kind c.rebus with | Evar (evk,_) when Evd.is_undefined clenv.evd evk && not (Evd.mem sigma evk) -> error_uninstantiated_metas (mkMeta mv) clenv @@ -1374,7 +1362,7 @@ let enforce_prop_bound_names rename tac = (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> string_of_id id + | Some id when not very_standard -> Id.to_string id | _ -> "" in Name (add_suffix Namegen.default_prop_ident s) else @@ -1473,7 +1461,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let sort = Tacticals.New.elimination_sort_of_goal gl in let mind = on_snd (fun u -> EInstance.kind sigma u) mind in let (sigma, elim) = - if occur_term sigma c concl then + if dependent sigma c concl then build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in @@ -1501,7 +1489,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings) exception IsNonrec -let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite +let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = let gr = lookup_eliminator ind s in @@ -1577,11 +1565,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in let hypmv = - try match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> failwith "" - with Failure _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") in + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = Retyping.get_type_of env sigma hyp in @@ -1590,7 +1578,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let new_hyp_typ = clenv_type elimclause'' in if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" - (str "Nothing to rewrite in " ++ pr_id id ++ str"."); + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) end @@ -1605,7 +1593,7 @@ let general_elim_clause with_evars flags id c e = (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = - | DefinedRecord of constant option list + | DefinedRecord of Constant.t option list | NotADefinedRecordUseScheme of constr let make_projection env sigma params cstr sign elim i n c u = @@ -1737,11 +1725,11 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in + let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma thm_ty - nprod in - if n<0 then error "Applied theorem has not enough premisses."; + if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags with exn when catchable_exception exn -> @@ -1763,7 +1751,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in let tac = if with_destruct then - descend_in_conjunctions [] + descend_in_conjunctions Id.Set.empty (fun b id -> Tacticals.New.tclTHEN (try_main_apply b (mkVar id)) @@ -1873,7 +1861,7 @@ let explain_unable_to_apply_lemma ?loc env sigma thm innerclause = str ".")) let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = - let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in + let thm = nf_betaiota env sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> @@ -1912,7 +1900,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming ]) with e when with_destruct && CErrors.noncritical e -> let (e, info) = CErrors.push e in - (descend_in_conjunctions [targetid] + (descend_in_conjunctions (Id.Set.singleton targetid) (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) end @@ -1969,11 +1957,11 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = Profile.declare_profile "convert_leq";; *) -(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *) +(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) +(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) -(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) -(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) +(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) +(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) @@ -1982,7 +1970,7 @@ let exact_check c = Proofview.Goal.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 concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma, ct = Typing.type_of env sigma c in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -1991,7 +1979,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in exact_no_check (mkCast (c, cast, concl)) end @@ -2043,8 +2031,8 @@ let assumption = let on_the_bodies = function | [] -> assert false -| [id] -> str " depends on the body of " ++ pr_id id -| l -> str " depends on the bodies of " ++ pr_sequence pr_id l +| [id] -> str " depends on the body of " ++ Id.print id +| l -> str " depends on the bodies of " ++ pr_sequence Id.print l exception DependsOnBody of Id.t option @@ -2075,13 +2063,13 @@ let clear_body ids = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function | LocalAssum (id,t) as decl -> let () = if List.mem_f Id.equal id ids then - user_err (str "Hypothesis " ++ pr_id id ++ str " is not a local definition") + user_err (str "Hypothesis " ++ Id.print id ++ str " is not a local definition") in decl | LocalDef (id,_,t) as decl -> @@ -2113,7 +2101,7 @@ let clear_body ids = with DependsOnBody where -> let msg = match where with | None -> str "Conclusion" ++ on_the_bodies ids - | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids + | Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids in Tacticals.New.tclZEROMSG msg in @@ -2166,12 +2154,12 @@ let keep hyps = and [a1..an:A1..An(a1..an-1)] such that the goal is [G(a1..an)], this generalizes [hyps |- goal] into [hyps |- T] *) -let apply_type newcl args = +let apply_type ~typecheck newcl args = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine ~typecheck:false begin fun sigma -> - let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in + Refine.refine ~typecheck begin fun sigma -> + let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in (sigma, applist (ev, args)) @@ -2200,7 +2188,6 @@ let bring_hyps hyps = let revert hyps = Proofview.Goal.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) <*> (clear hyps) end @@ -2219,27 +2206,27 @@ let check_number_of_constructors expctdnumopt i nconstr = end; if i > nconstr then error "Not enough constructors." -let constructor_tac with_evars expctdnumopt i lbind = +let constructor_core with_evars cstr lbind = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let (sigma, (cons, u)) = Evd.fresh_constructor_instance env sigma cstr in + let cons = mkConstructU (cons, EInstance.make u) in + let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) apply_tac + end + +let constructor_tac with_evars expctdnumopt i lbind = + Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - in - let (mind,redcl) = reduce_to_quantified_ind cl in - let nconstr = - Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in - check_number_of_constructors expctdnumopt i nconstr; - - let (sigma, (cons, u)) = Evd.fresh_constructor_instance - (Proofview.Goal.env gl) sigma (fst mind, i) in - let cons = mkConstructU (cons, EInstance.make u) in - - let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in - Tacticals.New.tclTHENLIST - [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check redcl DEFAULTcast; - intros; apply_tac] + let ((ind,_),redcl) = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in + let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in + check_number_of_constructors expctdnumopt i nconstr; + Tacticals.New.tclTHENLIST [ + convert_concl_no_check redcl DEFAULTcast; + intros; + constructor_core with_evars (ind, i) lbind + ] end let one_constructor i lbind = constructor_tac false None i lbind @@ -2249,24 +2236,26 @@ let one_constructor i lbind = constructor_tac false None i lbind Should be generalize in Constructor (Fun c : I -> tactic) *) -let rec tclANY tac = function -| [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.") -| arg :: l -> - Tacticals.New.tclORD (tac arg) (fun () -> tclANY tac l) - 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 + let one_constr = + let tac cstr = constructor_core with_evars cstr NoBindings in + match tacopt with + | None -> tac + | Some t -> fun cstr -> Tacticals.New.tclTHEN (tac cstr) t in + let rec any_constr ind n i () = + if Int.equal i n then one_constr (ind,i) + else Tacticals.New.tclORD (one_constr (ind,i)) (any_constr ind n (i + 1)) in Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - in - let mind = fst (reduce_to_quantified_ind cl) in + let (ind,_),redcl = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in + Array.length (snd (Global.lookup_inductive ind)).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; - tclANY tac (List.interval 1 nconstr) + Tacticals.New.tclTHENLIST [ + convert_concl_no_check redcl DEFAULTcast; + intros; + any_constr ind nconstr 1 () + ] end let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 @@ -2390,15 +2379,16 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let prepare_naming ?loc = function | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id) - | IntroAnonymous -> NamingAvoid [] - | IntroFresh id -> NamingBasedOn (id,[]) + | IntroAnonymous -> NamingAvoid Id.Set.empty + | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) let rec explicit_intro_names = function | (_, IntroForthcoming _) :: l -> explicit_intro_names l -| (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l +| (_, IntroNaming (IntroIdentifier id)) :: l -> Id.Set.add id (explicit_intro_names l) | (_, IntroAction (IntroOrAndPattern l)) :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll) + let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in + List.fold_left fold Id.Set.empty ll | (_, IntroAction (IntroInjection l)) :: l' -> explicit_intro_names (l@l') | (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> @@ -2406,17 +2396,17 @@ let rec explicit_intro_names = function | (_, (IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> explicit_intro_names l -| [] -> [] +| [] -> Id.Set.empty let rec check_name_unicity env ok seen = function | (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l | (loc, IntroNaming (IntroIdentifier id)) :: l -> (try ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env); - user_err ?loc (pr_id id ++ str" is already used.") + user_err ?loc (Id.print id ++ str" is already used.") with Not_found -> if List.mem_f Id.equal id seen then - user_err ?loc (pr_id id ++ str" is used twice.") + user_err ?loc (Id.print id ++ str" is used twice.") else check_name_unicity env ok (id::seen) l) | (_, IntroAction (IntroOrAndPattern l)) :: l' -> @@ -2453,8 +2443,8 @@ let make_tmp_naming avoid l = function IntroAnonymous, but at the cost of a "renaming"; Note that in the case of IntroFresh, we should use check_thin_clash_then anyway to prevent the case of an IntroFresh precisely using the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l) - | pat -> NamingAvoid(avoid@explicit_intro_names ((Loc.tag @@ IntroAction pat)::l)) + | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) + | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))) let fit_bound n = function | None -> true @@ -2466,7 +2456,7 @@ let exceed_bound n = function (* We delay thinning until the completion of the whole intros tactic to ensure that dependent hypotheses are cleared in the right - dependency order (see bug #1000); we use fresh names, not used in + dependency order (see BZ#1000); we use fresh names, not used in the tactic, for the hyps to clear *) (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]: [b]: compatibility flag, if false at toplevel, do not complete incomplete @@ -2495,7 +2485,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l)) + intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) destopt onlydeps n bound (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound (n+List.length ids) tac l) @@ -2518,12 +2508,12 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac intro_then_gen (NamingMustBe (loc,id)) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> - intro_then_gen (NamingAvoid (avoid@explicit_intro_names l)) + intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) | IntroFresh id -> (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l)) + intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) @@ -2557,7 +2547,7 @@ and prepare_intros ?loc with_evars dft destopt = function | IntroAction ipat -> prepare_naming ?loc dft, (let tac thin bound = - intro_patterns_core with_evars true [] [] thin destopt bound 0 + intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in fun id -> intro_pattern_action ?loc with_evars true true ipat [] destopt tac id) @@ -2568,7 +2558,7 @@ let intro_patterns_head_core with_evars b destopt bound pat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in check_name_unicity env [] [] pat; - intro_patterns_core with_evars b [] [] [] destopt + intro_patterns_core with_evars b Id.Set.empty [] [] destopt bound 0 (fun _ l -> clear_wildcards l) pat end @@ -2623,8 +2613,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else - get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in + else ( + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + get_previous_hyp_position env sigma id (Proofview.Goal.hyps gl) + ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -2680,8 +2672,8 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let (sigma, (newcl, eq_tac)) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with - | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl - | IntroFresh heq_base -> new_fresh_id [id] heq_base gl + | IntroAnonymous -> new_fresh_id (Id.Set.singleton id) (add_prefix "Heq" id) gl + | IntroFresh heq_base -> new_fresh_id (Id.Set.singleton id) heq_base gl | 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 @@ -2733,11 +2725,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with - | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env - | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env + | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env + | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env | IntroIdentifier id -> if List.mem id (ids_of_named_context (named_context env)) then - user_err ?loc (pr_id id ++ str" is already used."); + user_err ?loc (Id.print id ++ str" is already used."); id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in @@ -2820,7 +2812,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t let generalized_name env sigma c t ids cl = function | Name id as na -> if Id.List.mem id ids then - user_err (pr_id id ++ str " is already used."); + user_err (Id.print id ++ str " is already used."); na | Anonymous -> match EConstr.kind sigma c with @@ -2897,7 +2889,7 @@ let generalize_dep ?(with_let=false) c = let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST [ Proofview.Unsafe.tclEVARS evd; - apply_type cl'' (if Option.is_empty body then c::args else args); + apply_type ~typecheck:false cl'' (if Option.is_empty body then c::args else args); clear (List.rev tothin')] end @@ -2911,13 +2903,12 @@ let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter map lconstr)) + (apply_type ~typecheck:false newcl (List.map_filter map lconstr)) end let new_generalize_gen_let lconstr = Proofview.Goal.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 env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in @@ -3067,10 +3058,10 @@ let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) - let env = Proofview.Goal.env (Proofview.Goal.assume gl) in + let env = Proofview.Goal.env gl in let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") + (Id.print x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval in let xval = EConstr.of_constr xval in @@ -3122,11 +3113,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" - (fun names -> - strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") - ++ str": " ++ prlist_with_sep spc - (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) + (fun names -> + strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ + str": " ++ prlist_with_sep spc + (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names) let check_unused_names env sigma names = if not (List.is_empty names) then @@ -3141,13 +3132,13 @@ let rec consume_pattern avoid na isdep gl = function | (loc,IntroForthcoming true)::names when not isdep -> consume_pattern avoid na isdep gl names | (loc,IntroForthcoming _)::names as fullpat -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,intropattern_of_name gl avoid na), fullpat) | (loc,IntroNaming IntroAnonymous)::names -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,intropattern_of_name gl avoid na), names) | (loc,IntroNaming (IntroFresh id'))::names -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names) | pat::names -> (pat,names) @@ -3205,7 +3196,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = avoid @ avoid' in + let avoid = Id.Set.union avoid avoid' in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3278,7 +3269,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in + let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in let typ0 = reduce_to_quantified_ref indref tmptyp0 in let prods, indtyp = decompose_prod_assum sigma typ0 in @@ -3301,7 +3292,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (* Based on the knowledge given by the user, all constraints on the variable are generalizable in the current environment so that it is clearable after destruction *) - atomize_one (i-1) (c::args) (c::args') (id::avoid) + atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid) | _ -> let c' = expand_projections env' sigma c in let dependent t = dependent sigma c t in @@ -3326,9 +3317,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid)) + (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid)) in - atomize_one (List.length argl) [] [] [] + atomize_one (List.length argl) [] [] Id.Set.empty end (* [cook_sign] builds the lists [beforetoclear] (preceding the @@ -3400,7 +3391,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = (* First phase from L to R: get [toclear], [decldep] and [statuslist] for the hypotheses before (= more ancient than) hyp0 (see above) *) let toclear = ref [] in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let decldeps = ref [] in let ldeps = ref [] in let rstatus = ref [] in @@ -3417,7 +3408,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = is one of indvars too *) toclear := hyp::!toclear; MoveFirst (* fake value *) - end else if Id.List.mem hyp indvars then begin + end else if Id.Set.mem hyp indvars then begin (* The variables in indvars are such that they don't occur any more after generalization, so declare them to clear. *) toclear := hyp::!toclear; @@ -3427,14 +3418,14 @@ let cook_sign hyp0_opt inhyps indvars env sigma = (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt) in let depother = List.is_empty inhyps && - (List.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || + (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother then begin decldeps := decl::!decldeps; - avoid := hyp::!avoid; + avoid := Id.Set.add hyp !avoid; maindep := dephyp0 || !maindep; if !before then begin toclear := hyp::!toclear; @@ -3558,15 +3549,15 @@ let make_up_names n ind_opt cname = else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = - if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then [] + if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then Id.Set.empty else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) (* in order to get names such as f1, f2, ... *) let avoid = - (make_ident (Id.to_string hyprecname) None) :: - (make_ident (Id.to_string hyprecname) (Some 0)) :: [] in + Id.Set.add (make_ident (Id.to_string hyprecname) None) + (Id.Set.singleton (make_ident (Id.to_string hyprecname) (Some 0))) in if not (String.equal (atompart_of_id cname) "H") then - (make_ident base (Some 0)) :: (make_ident base None) :: avoid + Id.Set.add (make_ident base (Some 0)) (Id.Set.add (make_ident base None) avoid) else avoid in Id.of_string base, hyprecname, avoid @@ -3725,10 +3716,10 @@ let abstract_args gl generalize_vars dep id defined f args = let env = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let dep = dep || local_occur_var !sigma id concl in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let get_id name = let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in - avoid := id :: !avoid; id + avoid := Id.Set.add id !avoid; id in (* Build application generalized w.r.t. the argument plus the necessary eqs. From env |- c : forall G, T and args : G we build @@ -3907,7 +3898,7 @@ let specialize_eqs id = (internal_cut true id ty') (exact_no_check ((* refresh_universes_strict *) acc')) else - Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) + Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id) end let specialize_eqs id = Proofview.Goal.enter begin fun gl -> @@ -4131,8 +4122,7 @@ let guess_elim isrec dep s hyp0 gl = let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in - if use_dependent_propositions_elimination () && dep - then + if dep then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in (sigma, ind) @@ -4152,7 +4142,7 @@ let given_elim hyp0 (elimc,lbind as e) gl = Tacmach.New.project gl, (e, elimt), ind_type_guess type scheme_signature = - (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array + (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array type eliminator_source = | ElimUsing of (eliminator * EConstr.types) * scheme_signature @@ -4164,11 +4154,10 @@ let find_induction_type isrec elim hyp0 gl = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = - guess_elim isrec (* dummy: *) true sort hyp0 gl in - let scheme = compute_elim_sig sigma ~elimc elimt in - (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let scheme = compute_elim_sig sigma ~elimc elimt in + (* We drop the scheme waiting to know if it is dependent *) + scheme, ElimOver (isrec,hyp0) | Some e -> let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in @@ -4278,7 +4267,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let deps_cstr = List.fold_left (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in - let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in + let (sigma, isrec, elim, indsign) = get_eliminator elim dep s gl in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in @@ -4288,7 +4277,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ (* Generalize dependent hyps (but not args) *) - if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr; + if deps = [] then Proofview.tclUNIT () else apply_type ~typecheck:false tmpcl deps_cstr; (* side-conditions in elim (resp case) schemes come last (resp first) *) induct_tac elim; Tacticals.New.tclMAP expand_hyp toclear; @@ -4303,7 +4292,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in + let elim_info = find_induction_type isrec elim hyp0 gl in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> induction_tac with_evars [] [hyp0] elim)) @@ -4343,7 +4332,7 @@ let induction_without_atomization isrec with_evars elim names lid = gt_wf_rec was taken as a functional scheme with no parameters, but by chance, because of the addition of at least hyp0 for cook_sign, it behaved as if there was a real induction arg. *) - if indvars = [] then [List.hd lid_params] else indvars in + if List.is_empty indvars then Id.Set.singleton (List.hd lid_params) else Id.Set.of_list indvars in let induct_tac elim = Tacticals.New.tclTHENLIST [ (* pattern to make the predicate appear. *) reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; @@ -4363,7 +4352,7 @@ let clear_unselected_context id inhyps cls = if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then user_err - (str "Conclusion must be mentioned: it depends on " ++ pr_id id + (str "Conclusion must be mentioned: it depends on " ++ Id.print id ++ str "."); match cls.onhyps with | Some hyps -> @@ -4438,8 +4427,11 @@ let check_enough_applied env sigma elim = check_expected_type env sigma elimc elimt let guard_no_unifiable = Proofview.guard_no_unifiable >>= function -| None -> Proofview.tclUNIT () -| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l)) + | None -> Proofview.tclUNIT () + | Some l -> + Proofview.tclENV >>= function env -> + Proofview.tclEVARMAP >>= function sigma -> + Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l)) 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 = @@ -4539,7 +4531,7 @@ let induction_gen clear_flag isrec with_evars elim let id = (* Type not the right one if partially applied but anyway for internal use*) let x = id_of_name_using_hdchar env evd t Anonymous in - new_fresh_id [] x gl in + new_fresh_id Id.Set.empty x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then isrec with_evars info_arg elim id arg t inhyps cls @@ -4578,7 +4570,7 @@ let induction_gen_l isrec with_evars elim names lc = let x = id_of_name_using_hdchar env sigma (type_of c) Anonymous in - let id = new_fresh_id [] x gl in + let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let _ = newlc:=id::!newlc in Tacticals.New.tclTHEN @@ -4638,7 +4630,7 @@ let induction_destruct isrec with_evars (lc,elim) = (Tacticals.New.tclMAP (fun (a,b,cl) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project 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) @@ -4663,7 +4655,7 @@ let induction_destruct isrec with_evars (lc,elim) = end let induction ev clr c l e = - induction_gen clr true ev e + induction_gen clr true ev e ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = @@ -4953,7 +4945,7 @@ let interpretable_as_section_decl evd d1 d2 = let rec decompose len c t accu = let open Context.Rel.Declaration in if len = 0 then (c, t, accu) - else match kind_of_term c, kind_of_term t with + else match Constr.kind c, Constr.kind t with | Lambda (na, u, c), Prod (_, _, t) -> decompose (pred len) c t (LocalAssum (na, u) :: accu) | LetIn (na, b, u, c), LetIn (_, _, _, t) -> @@ -4961,7 +4953,7 @@ let rec decompose len c t accu = | _ -> assert false let rec shrink ctx sign c t accu = - let open Term in + let open Constr in let open CVars in match ctx, sign with | [], [] -> (c, t, accu) @@ -4971,8 +4963,8 @@ let rec shrink ctx sign c t accu = 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 c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in let accu = if RelDecl.is_local_assum p then mkVar (NamedDecl.get_id decl) :: accu else accu @@ -5015,7 +5007,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in - let id = next_global_ident_away id (pf_ids_of_hyps gl) in + let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in let concl = match goal_type with | None -> Proofview.Goal.concl gl | Some ty -> ty in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index bca0c4c50d..74415f8d03 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -8,7 +8,7 @@ open Loc open Names -open Term +open Constr open EConstr open Environ open Proof_type @@ -21,6 +21,7 @@ open Unification open Misctypes open Tactypes open Locus +open Ltac_pretype (** Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the @@ -29,7 +30,7 @@ open Locus (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -49,18 +50,18 @@ val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) -val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t -val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t +val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t +val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic -val intro_move_avoid : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) -val intro_avoiding : Id.t list -> unit Proofview.tactic +val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic @@ -75,7 +76,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int + bool -> quantified_hypothesis -> Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic @@ -184,7 +185,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> unit Proofview.tactic +val apply_type : typecheck:bool -> constr -> constr list -> unit Proofview.tactic val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic @@ -270,7 +271,7 @@ type eliminator = { val general_elim : evars_flag -> clear_flag -> constr with_bindings -> eliminator -> unit Proofview.tactic -val general_elim_clause : evars_flag -> unify_flags -> identifier option -> +val general_elim_clause : evars_flag -> unify_flags -> Id.t option -> clausenv -> eliminator -> unit Proofview.tactic val default_elim : evars_flag -> clear_flag -> constr with_bindings -> @@ -354,7 +355,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic val assert_after : Name.t -> types -> unit Proofview.tactic val assert_as : (* true = before *) bool -> - (* optionally tell if a specialization of some hyp: *) identifier option -> + (* optionally tell if a specialization of some hyp: *) Id.t option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactics assert, enough and pose proof; note that "by" @@ -427,7 +428,7 @@ module Simple : sig val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic val case : constr -> unit Proofview.tactic - val apply_in : identifier -> constr -> unit Proofview.tactic + val apply_in : Id.t -> constr -> unit Proofview.tactic end diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 64ba38a51b..7567cfa304 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -8,7 +8,7 @@ (*i*) open Util -open Term +open Constr open Names open Globnames open Mod_subst @@ -95,13 +95,20 @@ struct let compare cmp t1 t2 = match t1, t2 with | DRel, DRel -> 0 + | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 + | DSort, _ -> -1 | _, DSort -> 1 | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 + | DRef _, _ -> -1 | _, DRef _ -> 1 + | DCtx (tl1, tr1), DCtx (tl2, tr2) | DLambda (tl1, tr1), DLambda (tl2, tr2) | DApp (tl1, tr1), DApp (tl2, tr2) -> let c = cmp tl1 tl2 in if c = 0 then cmp tr1 tr2 else c + | DCtx _, _ -> -1 | _, DCtx _ -> 1 + | DLambda _, _ -> -1 | _, DLambda _ -> 1 + | DApp _, _ -> -1 | _, DApp _ -> 1 | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) -> let c = cmp c1 c2 in @@ -113,6 +120,7 @@ struct else c else c else c + | DCase _, _ -> -1 | _, DCase _ -> 1 | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) -> let c = Int.compare j1 j2 in @@ -124,6 +132,8 @@ struct else c else c else c + | DFix _, _ -> -1 | _, DFix _ -> 1 + | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) -> let c = Int.compare i1 i2 in if c = 0 then @@ -131,7 +141,18 @@ struct if c = 0 then Array.compare cmp pl1 pl2 else c else c - | _ -> Pervasives.compare t1 t2 (** OK **) + | DCoFix _, _ -> -1 | _, DCoFix _ -> 1 + + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> + let c = cmp t1 t2 in + if Int.equal c 0 then + let c = Option.compare cmp ot1 ot2 in + if Int.equal c 0 then cmp u1 u2 + else c + else c + | DCons _, _ -> -1 | _, DCons _ -> 1 + + | DNil, DNil -> 0 let fold f acc = function | (DRel | DNil | DSort | DRef _) -> acc @@ -174,7 +195,8 @@ struct Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 - | _ -> assert false + | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ + | DFix _ | DCoFix _ | DCons _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in @@ -194,11 +216,13 @@ struct DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) - | _ -> assert false + | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ + | DFix _ | DCoFix _ | DCons _), _ -> assert false let terminal = function | (DRel | DSort | DNil | DRef _) -> true - | _ -> false + | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> + false let compare t1 t2 = compare dummy_cmp t1 t2 @@ -257,7 +281,7 @@ struct let pat_of_constr c : term_pattern = (** To each evar we associate a unique identifier. *) let metas = ref Evar.Map.empty in - let rec pat_of_constr c = match kind_of_term c with + let rec pat_of_constr c = match Constr.kind c with | Rel _ -> Term DRel | Sort _ -> Term DSort | Var i -> Term (DRef (VarRef i)) @@ -290,7 +314,7 @@ struct | Proj (p,c) -> Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) - and ctx_of_constr ctx c = match kind_of_term c with + and ctx_of_constr ctx c = match Constr.kind c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c | _ -> ctx,pat_of_constr c diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index 16122fa5e0..db7da18ba9 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Mod_subst (** Dnets on constr terms. |