diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2751 |
1 files changed, 1412 insertions, 1339 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9d64e7c5..dfdd3237 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,28 +1,32 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +module CVars = Vars + open Pp open CErrors open Util open Names open Nameops -open Term -open Vars +open Constr open Termops +open Environ +open EConstr +open Vars open Find_subterm open Namegen open Declarations open Inductiveops open Reductionops -open Environ open Globnames open Evd -open Pfedit open Tacred open Genredexpr open Tacmach.New @@ -32,7 +36,6 @@ open Refiner open Tacticals open Hipattern open Coqlib -open Tacexpr open Decl_kinds open Evarutil open Indrec @@ -42,63 +45,28 @@ open Locus open Locusops open Misctypes open Proofview.Notations -open Sigma.Notations +open Context.Named.Declaration -let inj_with_occurrences e = (AllOccurrences,e) +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration -let dloc = Loc.ghost +let inj_with_occurrences e = (AllOccurrences,e) let typ_of env sigma c = let open Retyping in - try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c + try get_type_of ~lax:true env sigma c with RetypeError e -> - user_err_loc (Loc.ghost, "", print_retype_error e) + user_err (print_retype_error e) open Goptions -(* Option for 8.2 compatibility *) -let dependent_propositions_elimination = ref true - -let use_dependent_propositions_elimination () = - !dependent_propositions_elimination - && Flags.version_strictly_greater Flags.V8_2 - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - 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 - { optsync = true; - 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 _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = true; - Goptions.optname = - "Perform typeclass resolution on apply-generated subgoals."; - Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"]; - Goptions.optread = (fun () -> !apply_solve_class_goals); - Goptions.optwrite = (fun a -> apply_solve_class_goals:=a); -} - let clear_hyp_by_default = ref false let use_clear_hyp_by_default () = !clear_hyp_by_default let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "default clearing of hypotheses after use"; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; @@ -114,26 +82,12 @@ let accept_universal_lemma_under_conjunctions () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "trivial unification in tactics applying under conjunctions"; optkey = ["Universal";"Lemma";"Under";"Conjunction"]; optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optsync = true; - optdepr = true; - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -144,12 +98,10 @@ let bracketing_last_or_and_intro_pattern = ref true let use_bracketing_last_or_and_intro_pattern () = !bracketing_last_or_and_intro_pattern - && Flags.version_strictly_greater Flags.V8_4 let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); @@ -166,76 +118,74 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store decl b = - let open Context.Named.Declaration in - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in - let inst = List.map (mkVar % get_id) (named_context env) in + let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in let ninst = mkRel 1 :: inst in - let nb = subst1 (mkVar (get_id decl)) b in - let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) - end } + let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in + let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in + (sigma, mkNamedLambda_or_LetIn decl ev) + end let introduction ?(check=true) id = - let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> - let gl = Proofview.Goal.assume gl in + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if check && mem_named_context_val id hyps then - errorlabstrm "Tactics.introduction" - (str "Variable " ++ pr_id id ++ str " is already declared.") + user_err ~hdr:"Tactics.introduction" + (str "Variable " ++ Id.print id ++ str " is already declared.") in - match kind_of_term (whd_evar sigma concl) with + 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) - end } + | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) + end let refine = Tacmach.refine +let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - let conclty = Proofview.Goal.raw_concl gl in - Refine.refine ~unsafe:true { run = begin fun sigma -> - let Sigma ((), sigma, p) = + let conclty = Proofview.Goal.concl gl in + Refine.refine ~typecheck:false begin fun sigma -> + let sigma = if check then begin - let sigma = Sigma.to_evar_map sigma in ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; - Sigma.Unsafe.of_pair ((), sigma) - end else Sigma.here () sigma in - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in + sigma + end else sigma in + let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in - Sigma (ans, sigma, p +> q) - end } - end } + (sigma, ans) + end + end let convert_hyp ?(check=true) d = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let ty = Proofview.Goal.raw_concl gl in + let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty - end } - end } + end + end let convert_concl_no_check = convert_concl ~check:false let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> try let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in if b then Proofview.Unsafe.tclEVARS sigma @@ -243,37 +193,37 @@ let convert_gen pb x y = with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") -end } +end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y 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"." let error_clear_dependency env sigma id err = - errorlabstrm "" (clear_dependency_msg env sigma id err) + user_err (clear_dependency_msg 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"." let error_replacing_dependency env sigma id err = - errorlabstrm "" (replacing_dependency_msg env sigma id err) + user_err (replacing_dependency_msg env sigma id err) (* This tactic enables the user to remove hypotheses from the signature. * Some care is taken to prevent him from removing variables that are @@ -283,10 +233,9 @@ let error_replacing_dependency env sigma id err = let clear_gen fail = function | [] -> Proofview.tclUNIT () | ids -> - Proofview.Goal.s_enter { s_enter = begin fun gl -> + 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 @@ -296,43 +245,44 @@ let clear_gen fail = function with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err in let env = reset_with_named_context hyps env in - let tac = Refine.refine ~unsafe:true { run = fun sigma -> + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + (Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl - } in - Sigma.Unsafe.of_pair (tac, !evdref) - end } + end) + end let clear ids = clear_gen error_clear_dependency ids let clear_for_replacing ids = clear_gen error_replacing_dependency ids let apply_clear_request clear_flag dft c = + Proofview.tclEVARMAP >>= fun sigma -> let check_isvar c = - if not (isVar c) then + if not (isVar sigma c) then error "keep/clear modifiers apply only to hypothesis names." in let doclear = match clear_flag with - | None -> dft && isVar c + | None -> dft && isVar sigma c | Some true -> check_isvar c; true | Some false -> false in - if doclear then clear [destVar c] + if doclear then clear [destVar sigma c] else Tacticals.New.tclIDTAC (* Moving hypotheses *) let move_hyp id dest = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let ty = Proofview.Goal.raw_concl gl in + let sigma = Tacmach.New.project gl in + 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 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 ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty - end } - end } + end + end (* Renaming hypotheses *) let rename_hyp repl = - let open Context.Named.Declaration in let fold accu (src, dst) = match accu with | None -> None | Some (srcs, dsts) -> @@ -348,24 +298,25 @@ let rename_hyp repl = match dom with | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> - Proofview.Goal.enter { enter = begin fun gl -> - let gl = Proofview.Goal.assume gl in + Proofview.Goal.enter begin fun gl -> 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 (get_id decl) accu in + 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.errorlabstrm "" (pr_id elt ++ str " is already used") + CErrors.user_err (Id.print elt ++ str " is already used") with Not_found -> () in (** All is well *) @@ -373,24 +324,26 @@ let rename_hyp repl = let subst = List.map make_subst repl in let subst c = Vars.replace_vars subst c in let map decl = - decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) - |> map_constr subst + decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) + |> NamedDecl.map_constr subst in let nhyps = List.map map hyps in let nconcl = subst concl in - let nctx = Environ.val_of_named_context nhyps in - let instance = List.map (mkVar % get_id) hyps in - Refine.refine ~unsafe:true { run = begin fun sigma -> + let nctx = val_of_named_context nhyps in + let instance = List.map (NamedDecl.get_id %> mkVar) hyps in + Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance - end } - end } + end + end (**************************************************************) (* Fresh names *) (**************************************************************) 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) @@ -411,20 +364,20 @@ let default_id env sigma decl = | LocalAssum (name,t) -> let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in id_of_name_with_default dft name - | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name + | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name (* Non primitive introduction tactics are treated by intro_then_gen There is possibly renaming, with possibly names to avoid and possibly a move to do after the introduction *) type name_flag = - | NamingAvoid of Id.t list - | NamingBasedOn of Id.t * Id.t list - | NamingMustBe of Loc.t * Id.t + | NamingAvoid of Id.Set.t + | NamingBasedOn of Id.t * Id.Set.t + | NamingMustBe of lident let naming_of_name = function - | Anonymous -> NamingAvoid [] - | Name id -> NamingMustBe (dloc,id) + | Anonymous -> NamingAvoid Id.Set.empty + | Name id -> NamingMustBe (CAst.make id) let find_name mayrepl decl naming gl = match naming with | NamingAvoid idl -> @@ -433,69 +386,129 @@ let find_name mayrepl decl naming gl = match naming with let sigma = Tacmach.New.project gl in new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl - | NamingMustBe (loc,id) -> - (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_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 (loc,"",pr_id id ++ str" is already used."); - id + | NamingMustBe {CAst.loc;v=id} -> + (* When name is given, we allow to hide a global name *) + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in + if not mayrepl && Id.Set.mem id ids_of_hyps then + user_err ?loc (Id.print id ++ str" is already used."); + id + +(**************************************************************) +(* Computing position of hypotheses for replacing *) +(**************************************************************) + +let get_next_hyp_position env sigma id = + let rec aux = function + | [] -> 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 + else + aux right + in + aux + +let get_previous_hyp_position env sigma id = + let rec aux dest = function + | [] -> 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 + in + aux MoveLast (**************************************************************) (* Cut rule *) (**************************************************************) +let clear_hyps2 env sigma ids sign t cl = + try + let evdref = ref (Evd.clear_metas sigma) in + let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in + (hyps, t, cl, !evdref) + with Evarutil.ClearDependencyError (id,err) -> + error_replacing_dependency env sigma id err + +let internal_cut_gen ?(check=true) dir replace id t = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let store = Proofview.Goal.extra gl in + let sign = named_context_val env in + let sign',t,concl,sigma = + if replace then + 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 " ++ Id.print id ++ str " is already declared."); + push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in + let nf_t = nf_betaiota env sigma t in + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let (sigma,ev,ev') = + if dir then + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + (sigma,ev,ev') + else + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + (sigma,ev,ev') in + let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in + (sigma, term) + end) + end + +let internal_cut ?(check=true) = internal_cut_gen ~check true +let internal_cut_rev ?(check=true) = internal_cut_gen ~check false + let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENLAST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut b id t) (tac id) - end } + end let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) let assert_before na = assert_before_gen false (naming_of_name na) -let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id)) +let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make id)) let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENFIRST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut_rev b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut_rev b id t) (tac id) - end } + end let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) let assert_after na = assert_after_gen false (naming_of_name na) -let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id)) +let assert_after_replacing id = assert_after_gen true (NamingMustBe (CAst.make id)) (**************************************************************) (* Fixpoints and CoFixpoints *) (**************************************************************) -let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma = -fun env sigma p -> function -| [] -> Sigma ([], sigma, p) +let rec mk_holes env sigma = function +| [] -> (sigma, []) | arg :: rem -> - let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in - let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in - Sigma (arg :: rem, sigma, r) + let (sigma, arg) = Evarutil.new_evar env sigma arg in + let (sigma, rem) = mk_holes env sigma rem in + (sigma, arg :: rem) -let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with +let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with | Prod (na, c1, b) -> if Int.equal k 1 then try @@ -505,10 +518,13 @@ let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) w else let open Context.Rel.Declaration in check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b +| LetIn (na, c1, t, b) -> + let open Context.Rel.Declaration in + check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b | _ -> error "Not enough products." (* Refine as a fixpoint *) -let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> +let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -520,40 +536,45 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { 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 - errorlabstrm "Logic.prim_refiner" - (str "Name " ++ pr_id f ++ str " already used in the environment"); + user_err ~hdr:"Logic.prim_refiner" + (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 - Refine.refine { run = begin fun sigma -> - let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in + Refine.refine ~typecheck:false begin fun sigma -> + let (sigma, evs) = mk_holes nenv sigma (List.map pi3 all) in let ids = List.map pi1 all in let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in let funnames = Array.of_list (List.map (fun i -> Name i) ids) in let typarray = Array.of_list (List.map pi3 all) in let bodies = Array.of_list evs in - let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in - Sigma (oterm, sigma, p) - end } -end } + let oterm = mkFix ((indxs,0),(funnames,typarray,bodies)) in + (sigma, oterm) + end +end + +let warning_nameless_fix = + CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> + str "fix/cofix without a name are deprecated, please use the named version.") let fix ido n = match ido with | None -> - Proofview.Goal.enter { enter = begin fun gl -> - let name = Pfedit.get_current_proof_name () in - let id = new_fresh_id [] name gl in + warning_nameless_fix (); + Proofview.Goal.enter begin fun gl -> + let name = Proof_global.get_current_proof_name () in + let id = new_fresh_id Id.Set.empty name gl in mutual_fix id n [] 0 - end } + end | Some id -> mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in - match kind_of_term b with + match EConstr.kind sigma b with | Prod (na, c1, b) -> let open Context.Rel.Declaration in check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b @@ -564,7 +585,7 @@ let rec check_is_mutcoind env sigma cl = error "All methods must construct elements in coinductive types." (* Refine as a cofixpoint *) -let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> +let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -580,25 +601,26 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> 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 - Refine.refine { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let (ids, types) = List.split all in - let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in + let (sigma, evs) = mk_holes nenv sigma types in let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let funnames = Array.of_list (List.map (fun i -> Name i) ids) in let typarray = Array.of_list types in let bodies = Array.of_list evs in - let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in - Sigma (oterm, sigma, p) - end } -end } + let oterm = mkCoFix (0, (funnames, typarray, bodies)) in + (sigma, oterm) + end +end let cofix ido = match ido with | None -> - Proofview.Goal.enter { enter = begin fun gl -> - let name = Pfedit.get_current_proof_name () in - let id = new_fresh_id [] name gl in + warning_nameless_fix (); + Proofview.Goal.enter begin fun gl -> + let name = Proof_global.get_current_proof_name () in + let id = new_fresh_id Id.Set.empty name gl in mutual_cofix id [] 0 - end } + end | Some id -> mutual_cofix id [] 0 @@ -606,15 +628,16 @@ let cofix ido = match ido with (* Reduction and conversion tactics *) (**************************************************************) -type tactic_reduction = env -> evar_map -> constr -> constr +type tactic_reduction = Reductionops.reduction_function +type e_tactic_reduction = Reductionops.e_reduction_function let pf_reduce_decl redfun where decl gl = let open Context.Named.Declaration in - let redfun' = Tacmach.New.pf_apply redfun gl in + let redfun' c = Tacmach.New.pf_apply redfun gl c in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (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 @@ -690,14 +713,14 @@ let bind_red_expr_occurrences occs nbcl redexp = certain hypothesis *) let reduct_in_concl (redfun,sty) = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty - end } + end let reduct_in_hyp ?(check=false) redfun (id,where) = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl) - end } + end let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -711,30 +734,32 @@ let reduct_option ?(check=false) redfun = function let pf_e_reduce_decl redfun where decl gl = let open Context.Named.Declaration in let sigma = Proofview.Goal.sigma gl in - let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in + let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str " has no value."); - let Sigma (ty', sigma, p) = redfun sigma ty in - Sigma (LocalAssum (id, ty'), sigma, p) + user_err (Id.print id ++ str " has no value."); + let (sigma, ty') = redfun sigma ty in + (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> - let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in - let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in - Sigma (LocalDef (id, b', ty'), sigma, p +> q) + let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in + let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in + (sigma, LocalDef (id, b', ty')) let e_reduct_in_concl ~check (redfun, sty) = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in - Sigma (convert_concl ~check c' sty, sigma, p) - end } + let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_concl ~check c' sty) + end let e_reduct_in_hyp ?(check=false) redfun (id, where) = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in - Sigma (convert_hyp ~check decl', sigma, p) - end } + Proofview.Goal.enter begin fun gl -> + let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_hyp ~check decl') + end let e_reduct_option ?(check=false) redfun = function | Some id -> e_reduct_in_hyp ~check (fst redfun) id @@ -744,41 +769,42 @@ let e_reduct_option ?(check=false) redfun = function from conversions. *) let e_change_in_concl (redfun,sty) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in - Sigma (convert_concl_no_check c sty, sigma, p) - end } + let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_concl_no_check c sty) + end let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str " has no value."); - let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in - Sigma (LocalAssum (id, ty'), sigma, p) + 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) -> - let Sigma (b', sigma, p) = - if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma + let (sigma, b') = + if where != InHypTypeOnly then redfun true env sigma b else (sigma, b) in - let Sigma (ty', sigma, q) = - if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma + let (sigma, ty') = + if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty) in - Sigma (LocalDef (id,b',ty'), sigma, p +> q) + (sigma, LocalDef (id,b',ty')) let e_change_in_hyp redfun (id,where) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + 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 Sigma (c, sigma, p) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in - Sigma (convert_hyp c, sigma, p) - end } + 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 -> constr Sigma.run +type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr -let make_change_arg c pats = - { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } +let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -789,46 +815,43 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if - isSort (whd_all env sigma t1) && - isSort (whd_all env sigma t2) + isSort sigma (whd_all env sigma t1) && + isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else - errorlabstrm "convert-check-hyp" (str "Types are incompatible.") + user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") else sigma end else - if not (isSort (whd_all env sigma t1)) then - errorlabstrm "convert-check-hyp" (str "Not a type.") + if not (isSort sigma (whd_all env sigma t1)) then + user_err ~hdr:"convert-check-hyp" (str "Not a type.") else sigma (* Now we introduce different instances of the previous tacticals *) -let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c -> - let Sigma (t', sigma, p) = t.run sigma in - let sigma = Sigma.to_evar_map sigma in +let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = + let (sigma, t') = t sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); - Sigma.Unsafe.of_pair (t', sigma) -end } + if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); + (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) -let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c -> +let change_on_subterm cv_pb deep t where env sigma c = let mayneedglobalcheck = ref false in - let Sigma (c, sigma, p) = match where with - | None -> (change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty)).e_redfun env sigma c + let (sigma, c) = match where with + | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c | Some occl -> - (e_contextually false occl + e_contextually false occl (fun subst -> - change_and_check Reduction.CONV mayneedglobalcheck true (t subst))).e_redfun + change_and_check Reduction.CONV mayneedglobalcheck true (t subst)) env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c) + try ignore (Typing.unsafe_type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; - Sigma (c, sigma, p) -end } + (sigma, c) let change_in_concl occl t = e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast) @@ -841,7 +864,7 @@ let change_option occl t = function | None -> change_in_concl occl t let change chg c cls = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> @@ -849,7 +872,7 @@ let change chg c cls = | OnConcl occs -> change_option (bind_change_occurrences occs chg) c None) cls - end } + end let change_concl t = change_in_concl None (make_change_arg t) @@ -884,16 +907,24 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = - let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in + let trace env sigma = + let open Printer in + 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let redexps = reduction_clause redexp cl' in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps - end } + end end (* Unfolding occurrences of a constant *) @@ -901,7 +932,7 @@ let reduce redexp cl = let unfold_constr = function | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] - | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.") + | _ -> user_err ~hdr:"unfold_constr" (str "Cannot unfold a non-constant.") (*******************************************) (* Introduction tactics *) @@ -913,13 +944,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 @@ -929,18 +960,19 @@ let build_intro_tac id dest tac = match dest with let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = nf_evar (Tacmach.New.project gl) concl in - match kind_of_term concl with - | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project 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 build_intro_tac name move_flag tac - | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) -> + | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> 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 *) @@ -951,26 +983,26 @@ 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 - end } + end let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) -let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false +let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true 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 (dloc,id)) hto true false + | Some id -> intro_gen (NamingMustBe (CAst.make 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 ****) @@ -990,7 +1022,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 @@ -999,37 +1031,17 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = in aux n [] -let get_next_hyp_position id gl = - let open Context.Named.Declaration in - let rec aux = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - if Id.equal (get_id decl) id then - match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast - else - aux right - in - aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - -let get_previous_hyp_position id gl = - let open Context.Named.Declaration in - let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - let hyp = get_id decl in - if Id.equal hyp id then dest else aux (MoveAfter hyp) right - in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - let intro_replacing id = - Proofview.Goal.enter { enter = begin fun gl -> - let next_hyp = get_next_hyp_position id gl in + Proofview.Goal.enter begin fun gl -> + 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; move_hyp id next_hyp; ] - end } + end (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' @@ -1041,8 +1053,10 @@ let intro_replacing id = (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in - Proofview.Goal.enter { enter = begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + Proofview.Goal.enter begin fun gl -> + 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])) @@ -1050,30 +1064,32 @@ let intros_possibly_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) - end } + end (* This version assumes that replacement is actually possible *) let intros_replacing ids = - Proofview.Goal.enter { enter = begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + Proofview.Goal.enter begin fun gl -> + 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) - end } + end (* User-level introduction tactics *) -let lookup_hypothesis_as_renamed env ccl = function - | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n - | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id +let lookup_hypothesis_as_renamed env sigma ccl = function + | AnonHyp n -> Detyping.lookup_index_as_renamed env sigma ccl n + | NamedHyp id -> Detyping.lookup_name_as_displayed env sigma ccl id let lookup_hypothesis_as_renamed_gen red h gl = let env = Proofview.Goal.env gl in let rec aux ccl = - match lookup_hypothesis_as_renamed env ccl h with + match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with | None when red -> let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in - let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in + let (_, c) = redfun env (Proofview.Goal.sigma gl) ccl in aux c | x -> x in @@ -1087,7 +1103,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" @@ -1096,17 +1112,17 @@ let depth_of_quantified_hypothesis red h gl = match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> - errorlabstrm "lookup_quantified_hypothesis" + user_err ~hdr:"lookup_quantified_hypothesis" (str "No " ++ msg_quantified_hypothesis h ++ strbrk " in current goal" ++ (if red then strbrk " even after head-reduction" else mt ()) ++ str".") let intros_until_gen red h = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n = depth_of_quantified_hypothesis red h gl in Tacticals.New.tclDO n (if red then introf else intro) - end } + end let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) @@ -1115,10 +1131,10 @@ let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = - Proofview.Goal.enter { enter = begin fun gl -> - let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + Proofview.Goal.enter begin fun gl -> + let _ = Tacmach.New.pf_get_hyp id gl in Proofview.tclUNIT () - end } + end let try_intros_until_id_check id = Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id) @@ -1130,49 +1146,43 @@ let try_intros_until tac = function let rec intros_move = function | [] -> Proofview.tclUNIT () | (hyp,destopt) :: rest -> - Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false) + Tacticals.New.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt false false) (intros_move rest) -let run_delayed env sigma c = - Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma } - (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = Some solve_by_implicit_tactic; + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> - let (cbl, sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in + let (sigma', cbl) = f env sigma in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') - (tac clear_flag (pending,cbl)) + (tac clear_flag (sigma,cbl)) | clear_flag,ElimOnAnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(c,NoBindings)) - end })) - | clear_flag,ElimOnIdent (_,id) -> + tac clear_flag (sigma,(c,NoBindings)) + end)) + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(mkVar id,NoBindings)) - end }) + tac clear_flag (sigma,(mkVar id,NoBindings)) + end) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -1181,7 +1191,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) @@ -1193,12 +1203,10 @@ let map_destruction_arg f sigma = function | clear_flag,ElimOnIdent id as x -> (sigma,x) let finish_delayed_evar_resolution with_evars env sigma f = - let ((c, lbind), sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in - let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let (sigma', (c, lbind)) = f env sigma in let flags = tactic_infer_flags with_evars in - let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in - (Sigma.to_evar_map sigma', (c, lbind)) + let (sigma', c) = finish_evar_resolution ~flags env sigma' (sigma,c) in + (sigma', (c, lbind)) let with_no_bindings (c, lbind) = if lbind != NoBindings then error "'with' clause not supported here."; @@ -1214,45 +1222,46 @@ let force_destruction_arg with_evars env sigma c = let normalize_cut = false let cut c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let concl = Tacmach.New.pf_nf_concl gl in + let concl = Proofview.Goal.concl gl in let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) let typ = Typing.unsafe_type_of env sigma c in let typ = whd_all env sigma typ in - match kind_of_term typ with + match EConstr.kind sigma typ with | Sort _ -> true | _ -> false 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 ~unsafe:true { run = begin fun h -> - let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in - let Sigma (x, h, q) = Evarutil.new_evar env h c in + Refine.refine ~typecheck:false begin fun h -> + let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in + let (h, x) = Evarutil.new_evar env h c in let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - Sigma (f, h, p +> q) - end } + (h, f) + end else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") - end } + end 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 errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") + let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") + 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 @@ -1261,7 +1270,7 @@ let check_unresolved_evars_of_metas sigma clenv = (meta_list clenv.evd) let do_replace id = function - | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true + | NamingMustBe {CAst.v=id'} when Option.equal Id.equal id (Some id') -> true | _ -> false (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some @@ -1281,11 +1290,11 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; - if not with_evars && occur_meta new_hyp_typ then + if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in - let naming = NamingMustBe (dloc,targetid) in + let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) @@ -1300,90 +1309,50 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) (* Elimination tactics *) (********************************************) -let last_arg c = match kind_of_term c with +let last_arg sigma c = match EConstr.kind sigma c with | App (f,cl) -> Array.last cl - | _ -> anomaly (Pp.str "last_arg") + | _ -> anomaly (Pp.str "last_arg.") -let nth_arg i c = - if Int.equal i (-1) then last_arg c else - match kind_of_term c with +let nth_arg sigma i c = + if Int.equal i (-1) then last_arg sigma c else + match EConstr.kind sigma c with | App (f,cl) -> cl.(i) - | _ -> anomaly (Pp.str "nth_arg") + | _ -> anomaly (Pp.str "nth_arg.") -let index_of_ind_arg t = - let rec aux i j t = match kind_of_term t with +let index_of_ind_arg sigma t = + let rec aux i j t = match EConstr.kind sigma t with | Prod (_,t,u) -> (* heuristic *) - if isInd (fst (decompose_app t)) then aux (Some j) (j+1) u + if isInd sigma (fst (decompose_app sigma t)) then aux (Some j) (j+1) u else aux i (j+1) u | _ -> match i with | Some i -> i | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let enforce_prop_bound_names rename tac = - let open Context.Rel.Declaration in - match rename with - | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> - (* Rename dependent arguments in Prop with name "H" *) - (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) - (* elim or induction with schemes built by Indrec.build_induction_scheme *) - let rec aux env sigma i t = - if i = 0 then t else match kind_of_term t with - | Prod (Name _ as na,t,t') -> - let very_standard = true in - let na = - if Retyping.get_sort_family_of env sigma t = InProp then - (* "very_standard" says that we should have "H" names only, but - this would break compatibility even more... *) - let s = match Namegen.head_name t with - | Some id when not very_standard -> string_of_id id - | _ -> "" in - Name (add_suffix Namegen.default_prop_ident s) - else - na in - mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') - | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') - | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> print_int i; Feedback.msg_notice (print_constr t); assert false in - let rename_branch i = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let t = Proofview.Goal.concl gl in - change_concl (aux env sigma i t) - end } in - (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) - tac - (Array.map rename_branch nn) - | _ -> - tac - -let rec contract_letin_in_lam_header c = - match kind_of_term c with - | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header c) - | LetIn (x,b,t,c) -> contract_letin_in_lam_header (subst1 b c) +let rec contract_letin_in_lam_header sigma c = + match EConstr.kind sigma c with + | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c) + | LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c) | _ -> c let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header elim in + let elim = contract_letin_in_lam_header sigma elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = - (match kind_of_term (nth_arg i elimclause.templval.rebus) with + (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with | Meta mv -> mv - | _ -> errorlabstrm "elimination_clause" + | _ -> 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 - enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) - end } + Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags + end (* * Elimination tactic with bindings and using an arbitrary @@ -1396,22 +1365,22 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags type eliminator = { elimindex : int option; (* None = find it automatically *) elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) - elimbody : constr with_bindings + elimbody : EConstr.constr with_bindings } let general_elim_clause_gen elimtac indclause elim = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in let elimt = Retyping.get_type_of env sigma elimc in let i = - match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in + match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause - end } + end let general_elim with_evars clear_flag (c, lbindc) elim = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in @@ -1423,33 +1392,34 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) - end } + end (* Case analysis tactics *) let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in + let t = Retyping.get_type_of env sigma c in + let (mind,_) = reduce_to_quantified_ind env sigma t in let sort = Tacticals.New.elimination_sort_of_goal gl in - let Sigma (elim, sigma, p) = - if occur_term c concl then + let mind = on_snd (fun u -> EInstance.kind sigma u) mind in + let (sigma, elim) = + 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 - let tac = + let elim = EConstr.of_constr elim in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) - in - Sigma (tac, sigma, p) - end } + end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = - match kind_of_term c with + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma c with | Var id when lbindc == NoBindings -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (general_case_analysis_in_context with_evars clear_flag cx) @@ -1464,11 +1434,12 @@ 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 let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in + let c = EConstr.of_constr c in evd, c let find_eliminator c gl = @@ -1480,13 +1451,11 @@ let find_eliminator c gl = let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE - (Proofview.Goal.s_enter { s_enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let sigma, elim = find_eliminator c gl in - let tac = - (general_elim with_evars clear_flag cx elim) - in - Sigma.Unsafe.of_pair (tac, sigma) - end }) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (general_elim with_evars clear_flag cx elim) + end) begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default @@ -1502,7 +1471,8 @@ let elim_in_context with_evars clear_flag c = function | None -> default_elim with_evars clear_flag c let elim with_evars clear_flag (c,lbindc as cx) elim = - match kind_of_term c with + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma c with | Var id when lbindc == NoBindings -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (elim_in_context with_evars clear_flag cx elim) @@ -1533,30 +1503,30 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header elim in + let elim = contract_letin_in_lam_header sigma elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = destMeta (nth_arg i elimclause.templval.rebus) 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 _ -> errorlabstrm "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 let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in - if Term.eq_constr hyp_typ new_hyp_typ then - errorlabstrm "general_rewrite_in" - (str "Nothing to rewrite in " ++ pr_id id ++ str"."); + if EConstr.eq_constr sigma hyp_typ new_hyp_typ then + user_err ~hdr:"general_rewrite_in" + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) - end } + end let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1568,7 +1538,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 = @@ -1576,21 +1546,23 @@ let make_projection env sigma params cstr sign elim i n c u = let elim = match elim with | NotADefinedRecordUseScheme elim -> (* bugs: goes from right to left when i increases! *) - let decl = List.nth cstr.cs_args i in - let t = get_type decl in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.cs_args in + let decl = List.nth cs_args i in + let t = RelDecl.get_type decl in let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in - let branch = it_mkLambda_or_LetIn b cstr.cs_args in + let branch = it_mkLambda_or_LetIn b cs_args in if (* excludes dependent projection types *) - noccur_between 1 (n-i-1) t + noccur_between sigma 1 (n-i-1) t (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar (fst (whd_betaiota_stack sigma t))) - && (accept_universal_lemma_under_conjunctions () || not (isRel t)) + && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in - let abselim = beta_applist (elim,params@[t;branch]) in - let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in + let abselim = beta_applist sigma (elim, params@[t;branch]) in + let args = Context.Rel.to_extended_vect mkRel 0 sign in + let c = beta_applist sigma (abselim, [mkApp (c, args)]) in Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) else None @@ -1598,7 +1570,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> - let args = Context.Rel.to_extended_vect 0 sign in + let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = if Environ.is_projection proj env then mkProj (Projection.make proj false, mkApp (c, args)) @@ -1613,30 +1585,32 @@ let make_projection env sigma params cstr sign elim i n c u = in elim let descend_in_conjunctions avoid tac (err, info) c = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in - let sign,ccl = decompose_prod_assum t in - match match_with_tuple ccl with + let sign,ccl = EConstr.decompose_prod_assum sigma t in + match match_with_tuple sigma ccl with | Some (_,_,isrec) -> let n = (constructors_nrealargs ind).(0) in let sort = Tacticals.New.elimination_sort_of_goal gl in let IndType (indf,_) = find_rectype env sigma ccl in let (_,inst), params = dest_ind_family indf in + let params = List.map EConstr.of_constr params in let cstr = (get_constructors env indf).(0) in let elim = try DefinedRecord (Recordops.lookup_projections ind) with Not_found -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in + let u = EInstance.kind sigma u in + let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in + let elim = EConstr.of_constr elim in NotADefinedRecordUseScheme elim in Tacticals.New.tclORELSE0 (Tacticals.New.tclFIRST (List.init n (fun i -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match make_projection env sigma params cstr sign elim i n c u with @@ -1647,33 +1621,16 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end }))) + end))) (Proofview.tclZERO ~info err) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err - end } + end (****************************************************) (* Resolution tactics *) (****************************************************) -let solve_remaining_apply_goals = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - if !apply_solve_class_goals then - try - let env = Proofview.Goal.env gl in - let evd = Sigma.to_evar_map sigma in - let concl = Proofview.Goal.concl gl in - if Typeclasses.is_class_type evd concl then - let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in - let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in - Sigma.Unsafe.of_pair (tac, evd') - else Sigma.here (Proofview.tclUNIT ()) sigma - with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma - else Sigma.here (Proofview.tclUNIT ()) sigma - end } - let tclORELSEOPT t k = Proofview.tclORELSE t (fun e -> match k e with @@ -1682,25 +1639,27 @@ let tclORELSEOPT t k = Proofview.tclZERO ~info e | Some tac -> tac) -let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = - Proofview.Goal.nf_enter { enter = begin fun gl -> +let general_apply with_delta with_destruct with_evars clear_flag + {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod_modulo_zeta concl in + let concl_nprod = nb_prod_modulo_zeta sigma concl in let rec try_main_apply with_destruct c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> 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 thm_ty - nprod in - if n<0 then error "Applied theorem has not enough premisses."; + let n = nb_prod_modulo_zeta sigma thm_ty - nprod in + 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 -> @@ -1719,10 +1678,10 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) with Redelimination -> (* Last chance: if the head is a variable, apply may try second order unification *) - let info = Loc.add_loc info loc in + 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)) @@ -1746,14 +1705,12 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) | PretypeError _|RefinerError _|UserError _|Failure _ -> Some (try_red_apply thm_ty0 (e, info)) | _ -> None) - end } + end in - Tacticals.New.tclTHENLIST [ - try_main_apply with_destruct c; - solve_remaining_apply_goals; - apply_clear_request clear_flag (use_clear_hyp_by_default ()) c - ] - end } + Tacticals.New.tclTHEN + (try_main_apply with_destruct c) + (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) + end let rec apply_with_bindings_gen b e = function | [] -> Proofview.tclUNIT () @@ -1764,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function (apply_with_bindings_gen b e cbl) let apply_with_delayed_bindings_gen b e l = - let one k (loc, f) = - Proofview.Goal.enter { enter = begin fun gl -> + let one k {CAst.loc;v=f} = + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let (cb, sigma) = run_delayed env sigma f in + let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k (loc,cb)) sigma - end } + (general_apply b b e k CAst.(make ?loc cb)) sigma + end in let rec aux = function | [] -> Proofview.tclUNIT () @@ -1781,13 +1738,13 @@ let apply_with_delayed_bindings_gen b e l = (one k f) (aux cbl) in aux l -let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)] +let apply_with_bindings cb = apply_with_bindings_gen false false [None,(CAst.make cb)] -let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)] +let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(CAst.make cb)] -let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))] +let apply c = apply_with_bindings_gen false false [None,(CAst.make (c,NoBindings))] -let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))] +let eapply c = apply_with_bindings_gen false true [None,(CAst.make (c,NoBindings))] let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1811,31 +1768,44 @@ let find_matching_clause unifier clause = with NotExtensibleClause -> failwith "Cannot apply" in find clause +exception UnableToApply + let progress_with_clause flags innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in - if List.is_empty ordered_metas then error "Statement without assumptions."; + if List.is_empty ordered_metas then raise UnableToApply; let f mv = try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause) with Failure _ -> None in try List.find_map f ordered_metas - with Not_found -> error "Unable to unify." - -let apply_in_once_main flags innerclause env sigma (d,lbind) = - let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in + with Not_found -> raise UnableToApply + +let explain_unable_to_apply_lemma ?loc env sigma thm innerclause = + user_err ?loc (hov 0 + (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_leconstr_env env sigma thm) ++ spc() ++ + str "on hypothesis of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_leconstr_env innerclause.env innerclause.evd (clenv_type innerclause)) ++ + str ".")) + +let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = + 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 -> - let e = CErrors.push e in + let e' = CErrors.push e in try aux (clenv_push_prod clause) - with NotExtensibleClause -> iraise e + with NotExtensibleClause -> + match e with + | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause + | _ -> iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) let apply_in_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,(loc,(d,lbind))) tac = + id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let flags = @@ -1844,11 +1814,11 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in let rec aux idstoclear with_destruct c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in + let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ @@ -1858,25 +1828,25 @@ 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 } + end in aux [] with_destruct d - end } + end let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,(loc,f)) tac = - Proofview.Goal.enter { enter = begin fun gl -> + id (clear_flag,{CAst.loc;v=f}) tac = + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let (c, sigma) = run_delayed env sigma f in + let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars - naming id (clear_flag,(loc,c)) tac) + naming id (clear_flag,CAst.(make ?loc c)) tac) sigma - end } + end (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1896,70 +1866,65 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam *) let cut_and_apply c = - Proofview.Goal.nf_enter { enter = begin fun gl -> - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with - | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project gl in + match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with + | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in - Refine.refine { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in - let ans = mkApp (f, [|mkApp (c, [|x|])|]) in - Sigma (ans, sigma, p +> q) - end } + let (sigma, f) = Evarutil.new_evar env sigma typ in + let (sigma, x) = Evarutil.new_evar env sigma c1 in + (sigma, mkApp (f, [|mkApp (c, [|x|])|])) + end | _ -> error "lapply needs a non-dependent product." - end } + end (********************************************************************) (* 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 ~unsafe:true { run = fun h -> Sigma.here c h } + Refine.refine ~typecheck:false (fun h -> (h,c)) let exact_check c = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + 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 = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in - let tac = - Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)) + end let cast_no_check cast c = - Proofview.Goal.enter { enter = begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - exact_no_check (Term.mkCast (c, cast, concl)) - end } + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + exact_no_check (mkCast (c, cast, concl)) + end let vm_cast_no_check c = cast_no_check Term.VMcast c let native_cast_no_check c = cast_no_check Term.NATIVEcast c let exact_proof c = let open Tacmach.New in - Proofview.Goal.nf_enter { enter = begin fun gl -> - Refine.refine { run = begin fun sigma -> - let sigma = Sigma.to_evar_map sigma in + Proofview.Goal.enter begin fun gl -> + Refine.refine ~typecheck:false begin fun sigma -> let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in let sigma = Evd.merge_universe_context sigma ctx in - Sigma.Unsafe.of_pair (c, sigma) - end } - end } + (sigma, c) + end + end let assumption = - let open Context.Named.Declaration in let rec arec gl only_eq = function | [] -> if only_eq then @@ -1967,25 +1932,25 @@ let assumption = arec gl false hyps else Tacticals.New.tclZEROMSG (str "No such assumption.") | decl::rest -> - let t = get_type decl in + let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = - if only_eq then (sigma, Constr.equal t concl) + if only_eq then (sigma, EConstr.eq_constr sigma t concl) else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - exact_no_check (mkVar (get_id decl)) + exact_no_check (mkVar (NamedDecl.get_id decl)) else arec gl only_eq rest in - let assumption_tac = { enter = begin fun gl -> + let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in arec gl true hyps - end } in - Proofview.Goal.nf_enter assumption_tac + in + Proofview.Goal.enter assumption_tac (*****************************************************************) (* Modification of a local context *) @@ -1993,8 +1958,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 @@ -2008,7 +1973,7 @@ let check_is_type env sigma ty = let check_decl env sigma decl = let open Context.Named.Declaration in - let ty = get_type decl in + let ty = NamedDecl.get_type decl in let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in @@ -2018,20 +1983,20 @@ let check_decl env sigma decl = in !evdref with e when CErrors.noncritical e -> - let id = get_id decl in + let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) let clear_body ids = let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + 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 - errorlabstrm "" (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 -> @@ -2046,16 +2011,16 @@ let clear_body ids = (** Do no recheck hypotheses that do not depend *) let sigma = if not seen then sigma - else if List.exists (fun id -> occur_var_in_decl env id decl) ids then + else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then check_decl env sigma decl else sigma in - let seen = seen || List.mem_f Id.equal (get_id decl) ids in + let seen = seen || List.mem_f Id.equal (NamedDecl.get_id decl) ids in (push_named decl env, sigma, seen) in let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in let sigma = - if List.exists (fun id -> occur_var env id concl) ids then + if List.exists (fun id -> occur_var env sigma id concl) ids then check_is_type env sigma concl else sigma in @@ -2063,18 +2028,18 @@ 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 check <*> - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl - end } - end } + end + end let clear_wildcards ids = - Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids + Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear [id]) ids (* Takes a list of booleans, and introduces all the variables * quantified in the goal which are associated with a value @@ -2090,22 +2055,23 @@ let rec intros_clearing = function (* Keeping only a few hypotheses *) let keep hyps = - let open Context.Named.Declaration in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) decl -> - let hyp = get_id decl in + let decl = map_named_decl EConstr.of_constr decl in + let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps - || List.exists (occur_var_in_decl env hyp) keep - || occur_var env hyp ccl + || List.exists (occur_var_in_decl env sigma hyp) keep + || occur_var env sigma hyp ccl then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (Proofview.Goal.env gl) in clear cl - end } + end (*********************************) (* Basic generalization tactics *) @@ -2115,17 +2081,17 @@ 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 = - Proofview.Goal.enter { enter = begin fun gl -> +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 { run = begin fun sigma -> - let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in - let Sigma (ev, sigma, p) = + 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), sigma, p) - end } - end } + (sigma, applist (ev, args)) + end + end (* Given a context [hyps] with domain [x1..xn], possibly with let-ins, and well-typed in the current goal, [bring_hyps hyps] generalizes @@ -2134,25 +2100,24 @@ let apply_type newcl args = let bring_hyps hyps = if List.is_empty hyps then Tacticals.New.tclIDTAC else - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - let concl = Tacmach.New.pf_nf_concl gl in + let concl = Tacmach.New.pf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in - let args = Array.of_list (Context.Named.to_instance hyps) in - Refine.refine { run = begin fun sigma -> - let Sigma (ev, sigma, p) = + let args = Array.of_list (Context.Named.to_instance mkVar hyps) in + Refine.refine ~typecheck:false begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in - Sigma (mkApp (ev, args), sigma, p) - end } - end } + (sigma, mkApp (ev, args)) + end + end let revert hyps = - Proofview.Goal.enter { enter = begin fun gl -> - let gl = Proofview.Goal.assume gl in + Proofview.Goal.enter begin fun gl -> let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (clear hyps) - end } + end (************************) (* Introduction tactics *) @@ -2162,37 +2127,34 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - errorlabstrm "Tactics.check_number_of_constructors" + user_err ~hdr:"Tactics.check_number_of_constructors" (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; if i > nconstr then error "Not enough constructors." -let constructor_tac with_evars expctdnumopt i lbind = - Proofview.Goal.s_enter { s_enter = begin fun gl -> +let constructor_core with_evars cstr lbind = + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let cl = Tacmach.New.pf_nf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - 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, sigma, p) = Sigma.fresh_constructor_instance - (Proofview.Goal.env gl) sigma (fst mind, i) in - let cons = mkConstructU cons in - - let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in - let tac = - (Tacticals.New.tclTHENLIST - [ - convert_concl_no_check redcl DEFAULTcast; - intros; apply_tac]) - in - Sigma (tac, sigma, p) - end } + 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 (CAst.make (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 ((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 @@ -2201,25 +2163,27 @@ 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 - Proofview.Goal.enter { enter = begin fun gl -> - let cl = Tacmach.New.pf_nf_concl gl in - let reduce_to_quantified_ind = - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl - in - let mind = fst (reduce_to_quantified_ind cl) 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 (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) - end } + 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 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -2251,7 +2215,7 @@ let error_unexpected_extra_pattern loc bound pat = | IntroNaming (IntroIdentifier _) -> "name", (String.plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in - user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ + user_err ?loc (str "Unexpected " ++ str s1 ++ str " (" ++ (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ str (if Int.equal nb 1 then "was" else "were") ++ @@ -2269,34 +2233,34 @@ let my_find_eq_data_decompose gl t = -> None | Constr_matching.PatternMatchingFailure -> None -let intro_decomp_eq loc l thin tac id = - Proofview.Goal.nf_enter { enter = begin fun gl -> +let intro_decomp_eq ?loc l thin tac id = + Proofview.Goal.enter begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") - end } + end -let intro_or_and_pattern loc with_evars bracketed ll thin tac id = - Proofview.Goal.enter { enter = begin fun gl -> +let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = + Proofview.Goal.enter begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let branchsigns = compute_constructor_signatures false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in - let ll = get_and_check_or_and_pattern loc ll branchsigns in + let ll = get_and_check_or_and_pattern ?loc ll branchsigns in Tacticals.New.tclTHENLASTn (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv_with_let ll) - end } + end let rewrite_hyp_then assert_style with_evars thin l2r id tac = let rew_on l2r = @@ -2305,27 +2269,28 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq id' = clear [id';id] in let early_clear id' thin = - List.filter (fun (_,id) -> not (Id.equal id id')) thin in - Proofview.Goal.enter { enter = begin fun gl -> + List.filter (fun {CAst.v=id} -> not (Id.equal id id')) thin in + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in let t = whd_all (type_of (mkVar id)) in - let eqtac, thin = match match_with_equality_type t with + let eqtac, thin = match match_with_equality_type sigma t with | Some (hdcncl,[_;lhs;rhs]) -> - if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then - let id' = destVar lhs in + if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then + let id' = destVar sigma lhs in subst_on l2r id' rhs, early_clear id' thin - else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then - let id' = destVar rhs in + else if not l2r && isVar sigma rhs && not (occur_var env sigma (destVar sigma rhs) lhs) then + let id' = destVar sigma rhs in subst_on l2r id' lhs, early_clear id' thin else Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin | Some (hdcncl,[c]) -> let l2r = not l2r in (* equality of the form eq_true *) - if isVar c then - let id' = destVar c in + if isVar sigma c then + let id' = destVar sigma c in Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq id'), early_clear id' thin @@ -2337,39 +2302,63 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = thin in (* Skip the side conditions of the rewriting step *) Tacticals.New.tclTHENFIRST eqtac (tac thin) - end } + end -let prepare_naming loc = function - | IntroIdentifier id -> NamingMustBe (loc,id) - | IntroAnonymous -> NamingAvoid [] - | IntroFresh id -> NamingBasedOn (id,[]) +let prepare_naming ?loc = function + | IntroIdentifier id -> NamingMustBe (CAst.make ?loc 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 -| (_, IntroAction (IntroOrAndPattern l)) :: l' -> +let rec explicit_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> explicit_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l) +| {v=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) -| (_, IntroAction (IntroInjection l)) :: l' -> + let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in + List.fold_left fold Id.Set.empty ll +| {v=IntroAction (IntroInjection l)} :: l' -> explicit_intro_names (l@l') -| (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> +| {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> explicit_intro_names (pat::l') -| (_, (IntroNaming (IntroAnonymous | IntroFresh _) - | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> +| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> explicit_intro_names l -| [] -> [] +| [] -> Id.Set.empty + +let rec check_name_unicity env ok seen = let open CAst in function +| {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l +| {loc;v=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 (Id.print id ++ str" is already used.") + with Not_found -> + if List.mem_f Id.equal id seen then + user_err ?loc (Id.print id ++ str" is used twice.") + else + check_name_unicity env ok (id::seen) l) +| {v=IntroAction (IntroOrAndPattern l)} :: l' -> + let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in + List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll +| {v=IntroAction (IntroInjection l)} :: l' -> + check_name_unicity env ok seen (l@l') +| {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> + check_name_unicity env ok seen (pat::l') +| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> + check_name_unicity env ok seen l +| [] -> () let wild_id = Id.of_string "_tmp" let rec list_mem_assoc_right id = function | [] -> false - | (x,id')::l -> Id.equal id id' || list_mem_assoc_right id l + | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l let check_thin_clash_then id thin avoid tac = if list_mem_assoc_right id thin then let newid = next_ident_away (add_suffix id "'") avoid in let thin = - List.map (on_snd (fun id' -> if Id.equal id id' then newid else id')) thin in + List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) else tac thin @@ -2381,8 +2370,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 ((dloc,IntroAction pat)::l)) + | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) + | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) let fit_bound n = function | None -> true @@ -2394,7 +2383,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 @@ -2418,19 +2407,19 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = | [] -> (* Behave as IntroAnonymous *) intro_patterns_core with_evars b avoid ids thin destopt bound n tac - [dloc,IntroNaming IntroAnonymous] - | (loc,pat) :: l -> + [CAst.make @@ IntroNaming IntroAnonymous] + | {CAst.loc;v=pat} :: l -> 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) | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) destopt true false - (intro_pattern_action loc with_evars (b || not (List.is_empty l)) false + (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false pat thin destopt (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0 (fun ids thin -> @@ -2443,67 +2432,73 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac match pat with | IntroIdentifier id -> check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe (loc,id)) destopt true false + intro_then_gen (NamingMustBe CAst.(make ?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) -and intro_pattern_action loc with_evars b style pat thin destopt tac id = +and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = match pat with | IntroWildcard -> - tac ((loc,id)::thin) None [] + tac (CAst.(make ?loc id)::thin) None [] | IntroOrAndPattern ll -> - intro_or_and_pattern loc with_evars b ll thin tac id + intro_or_and_pattern ?loc with_evars b ll thin tac id | IntroInjection l' -> - intro_decomp_eq loc l' thin tac id + intro_decomp_eq ?loc l' thin tac id | IntroRewrite l2r -> rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) - | IntroApplyOn (f,(loc,pat)) -> + | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> let naming,tac_ipat = - prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in + prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in let doclear = - if naming = NamingMustBe (loc,id) then + if naming = NamingMustBe (CAst.make ?loc id) then Proofview.tclUNIT () (* apply_in_once do a replacement *) else clear [id] in - let f = { delayed = fun env sigma -> - let Sigma (c, sigma, p) = f.delayed env sigma in - Sigma ((c, NoBindings), sigma, p) - } in - apply_in_delayed_once false true true with_evars naming id (None,(loc,f)) + let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) + in + apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) -and prepare_intros_loc loc with_evars dft destopt = function +and prepare_intros ?loc with_evars dft destopt = function | IntroNaming ipat -> - prepare_naming loc ipat, + prepare_naming ?loc ipat, (fun id -> move_hyp id destopt) | IntroAction ipat -> - prepare_naming loc dft, + 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) - | IntroForthcoming _ -> user_err_loc - (loc,"",str "Introduction pattern for one hypothesis expected.") + intro_pattern_action ?loc with_evars true true ipat [] destopt tac id) + | IntroForthcoming _ -> user_err ?loc + (str "Introduction pattern for one hypothesis expected.") + +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 Id.Set.empty [] [] destopt + bound 0 (fun _ l -> clear_wildcards l) pat + end let intro_patterns_bound_to with_evars n destopt = - intro_patterns_core with_evars true [] [] [] destopt - (Some (true,n)) 0 (fun _ l -> clear_wildcards l) + intro_patterns_head_core with_evars true destopt + (Some (true,n)) let intro_patterns_to with_evars destopt = - intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ()) - [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) + intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ()) + destopt None let intro_pattern_to with_evars destopt pat = - intro_patterns_to with_evars destopt [dloc,pat] + intro_patterns_to with_evars destopt [CAst.make pat] let intro_patterns with_evars = intro_patterns_to with_evars MoveLast @@ -2516,20 +2511,20 @@ let intros_patterns with_evars = function (* Forward reasoning *) (**************************) -let prepare_intros with_evars dft destopt = function - | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ()) - | Some (loc,ipat) -> prepare_intros_loc loc with_evars dft destopt ipat +let prepare_intros_opt with_evars dft destopt = function + | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) + | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat let ipat_of_name = function | Anonymous -> None - | Name id -> Some (dloc, IntroNaming (IntroIdentifier id)) + | Name id -> Some (CAst.make @@ IntroNaming (IntroIdentifier id)) -let head_ident c = - let c = fst (decompose_app ((strip_lam_assum c))) in - if isVar c then Some (destVar c) else None +let head_ident sigma c = + let c = fst (decompose_app sigma (snd (decompose_lam_assum sigma c))) in + if isVar sigma c then Some (destVar sigma c) else None let assert_as first hd ipat t = - let naming,tac = prepare_intros false IntroAnonymous MoveLast ipat in + let naming,tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in let repl = do_replace hd naming in let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in if first then assert_before_then_gen repl naming t tac @@ -2542,19 +2537,22 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars let tac (naming,lemma) tac id = apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in - Proofview.Goal.enter { enter = begin fun gl -> + 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 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 with_evars (IntroIdentifier id) destopt ipat in + prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = let last,first = List.sep_last lemmas in - List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last) + List.map (fun lem -> (NamingMustBe (CAst.make id),lem)) first, (naming,last) in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id - end } + end (* if sidecond_first then @@ -2565,7 +2563,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars *) let apply_in simple with_evars id lemmas ipat = - let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in + let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = @@ -2589,61 +2587,69 @@ let decode_hyp = function *) let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let Sigma (t, sigma, p) = match ty with - | Some t -> Sigma.here t sigma + let (sigma, t) = match ty with + | Some t -> (sigma, t) | None -> let t = typ_of env sigma c in - let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in - Sigma.Unsafe.of_pair (c, sigma) + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in - let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with - | Some (lr,(loc,ido)) -> + let (sigma, (newcl, eq_tac)) = match with_eq with + | Some (lr,{CAst.loc;v=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 - let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in - let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in + let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in + let eq = EConstr.of_constr eq in + let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in + let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in - let sigma = Sigma.to_evar_map sigma in let sigma, _ = Typing.type_of env sigma term in let ans = term, - Tacticals.New.tclTHEN - (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) - (clear_body [heq;id]) + Tacticals.New.tclTHENLIST + [ + intro_gen (NamingMustBe CAst.(make ?loc heq)) (decode_hyp lastlhyp) true false; + clear_body [heq;id]] in - Sigma.Unsafe.of_pair (ans, sigma) + (sigma, ans) | None -> - Sigma.here (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) sigma + (sigma, (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in - let tac = Tacticals.New.tclTHENLIST - [ convert_concl_no_check newcl DEFAULTcast; - intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; + [ Proofview.Unsafe.tclEVARS sigma; + convert_concl_no_check newcl DEFAULTcast; + intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ] - in - Sigma (tac, sigma, p +> q) - end } + end let insert_before decls lasthyp env = - let open Context.Named.Declaration in match lasthyp with | None -> push_named_context decls env | Some id -> Environ.fold_named_context (fun _ d env -> - let env = if Id.equal id (get_id d) then push_named_context decls env else env in + let d = map_named_decl EConstr.of_constr d in + let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in push_named d env) ~init:(reset_context env) env +let mk_eq_name env id {CAst.loc;v=ido} = + match ido with + | 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 (Id.print id ++ str" is already used."); + id + (* unsafe *) let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = @@ -2653,30 +2659,25 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = else LocalAssum (id,t) in 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 - | IntroIdentifier id -> - if List.mem id (ids_of_named_context (named_context env)) then - user_err_loc (loc,"",pr_id id ++ str" is already used."); - id in + | Some (lr,heq) -> let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in - let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in + let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in + let eq = EConstr.of_constr eq in + let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in + let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in - let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in - Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) + let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) | None -> let newenv = insert_before [decl] lastlhyp env in - let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in - Sigma (mkNamedLetIn id c t x, sigma, p) + let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + (sigma, mkNamedLetIn id c t x) let letin_tac with_eq id c ty occs = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in @@ -2684,40 +2685,39 @@ let letin_tac with_eq id c ty occs = let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in (* We keep the original term to match but record the potential side-effects of unifying universes. *) - let Sigma (c, sigma, p) = match res with - | None -> Sigma.here c sigma - | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p) + let (sigma, c) = match res with + | None -> (sigma, c) + | Some (sigma, _) -> (sigma, c) in - let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in - Sigma (tac, sigma, p) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty) + end -let letin_pat_tac with_eq id c occs = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> +let letin_pat_tac with_evars with_eq id c occs = + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in - let Sigma (c, sigma, p) = match res with - | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c + let (sigma, c) = match res with + | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c | Some res -> res in - let tac = - (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) - in - Sigma (tac, sigma, p) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) + end (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *) let forward b usetac ipat c = match usetac with | None -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let t = Tacmach.New.pf_get_type_of gl c in - let hd = head_ident c in + let sigma = Tacmach.New.project gl in + let hd = head_ident sigma c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) - end } + end | Some tac -> let tac = match tac with | None -> Tacticals.New.tclIDTAC @@ -2738,22 +2738,22 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t (* Compute a name for a generalization *) -let generalized_name c t ids cl = function +let generalized_name env sigma c t ids cl = function | Name id as na -> if Id.List.mem id ids then - errorlabstrm "" (pr_id id ++ str " is already used."); + user_err (Id.print id ++ str " is already used."); na | Anonymous -> - match kind_of_term c with + match EConstr.kind sigma c with | Var id -> (* Keep the name even if not occurring: may be used by intros later *) Name id | _ -> - if noccurn 1 cl then Anonymous else + if noccurn sigma 1 cl then Anonymous else (* On ne s'etait pas casse la tete : on avait pris pour nom de variable la premiere lettre du type, meme si "c" avait ete une constante dont on aurait pu prendre directement le nom *) - named_hd (Global.env()) t Anonymous + named_hd env sigma t Anonymous (* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai] @@ -2761,11 +2761,11 @@ let generalized_name c t ids cl = function let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in - let decls,cl = decompose_prod_n_assum i cl in + let decls,cl = decompose_prod_n_assum sigma i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in + let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in - let na = generalized_name c t ids cl' na in + let na = generalized_name env sigma c t ids cl' na in let decl = match b with | None -> LocalAssum (na,t) | Some b -> LocalDef (na,b,t) @@ -2773,37 +2773,41 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = mkProd_or_LetIn decl cl', sigma' let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = - let env = Tacmach.pf_env gl in - let ids = Tacmach.pf_ids_of_hyps gl in + let open Tacmach.New in + let env = pf_env gl in + let ids = pf_ids_of_hyps gl in let sigma, t = Typing.type_of env sigma c in generalize_goal_gen env sigma ids i o t cl -let old_generalize_dep ?(with_let=false) c gl = - let open Context.Named.Declaration in +let generalize_dep ?(with_let=false) c = + let open Tacmach.New in + let open Tacticals.New in + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in - let sign = pf_hyps gl in + let sign = Proofview.Goal.hyps gl in + let sigma = project gl in let init_ids = ids_of_named_context (Global.named_context()) in - let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) = - if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant - || dependent_in_decl c d then + let seek (d:named_declaration) (toquant:named_context) = + if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant + || dependent_in_decl sigma c d then d::toquant else toquant in let to_quantify = Context.Named.fold_outside seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in - let qhyps = List.map get_id to_quantify_rev in + let qhyps = List.map NamedDecl.get_id to_quantify_rev in let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = - match kind_of_term c with + match EConstr.kind sigma c with | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids) -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in let body = if with_let then - match kind_of_term c with - | Var id -> Tacmach.pf_get_hyp gl id |> get_value + match EConstr.kind sigma c with + | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value | _ -> None else None in @@ -2811,35 +2815,30 @@ let old_generalize_dep ?(with_let=false) c gl = (cl',project gl) in (** Check that the generalization is indeed well-typed *) let (evd, _) = Typing.type_of env evd cl'' in - let args = Context.Named.to_instance to_quantify_rev in + let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST - [tclEVARS evd; - Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args)); - Proofview.V82.of_tactic (clear (List.rev tothin'))] - gl - -let generalize_dep ?(with_let = false) c = - Proofview.V82.tactic (old_generalize_dep ~with_let c) + [ Proofview.Unsafe.tclEVARS evd; + apply_type ~typecheck:false cl'' (if Option.is_empty body then c::args else args); + clear (List.rev tothin')] + end (** *) -let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> +let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let newcl, evd = - List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr + List.fold_right_i (generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in - let tac = apply_type newcl (List.map_filter map lconstr) in - Sigma.Unsafe.of_pair (tac, evd) -end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) + (apply_type ~typecheck:false newcl (List.map_filter map lconstr)) +end let new_generalize_gen_let lconstr = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + 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 sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in let newcl, sigma, args = @@ -2851,14 +2850,12 @@ let new_generalize_gen_let lconstr = (cl, sigma, args)) 0 lconstr (concl, sigma, []) in - let tac = - Refine.refine { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in - Sigma ((applist (ev, args)), sigma, p) - end } - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in + (sigma, applist (ev, args)) + end) + end let generalize_gen lconstr = generalize_gen_let (List.map (fun (occs_c,na) -> @@ -2886,38 +2883,77 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) +(* Instantiating some arguments (whatever their position) of an hypothesis + or any term, leaving other arguments quantified. If operating on an + hypothesis of the goal, the new hypothesis replaces it. + + (c,lbind) are supposed to be of the form + ((t t1 t2 ... tm) , someBindings) + + in which case we pose a proof with body + + (fun y1...yp => H t1 t2 ... tm u1 ... uq) where yi are the + remaining arguments of H that lbind could not resolve, ui are a mix + of inferred args and yi. The overall effect is to remove from H as + much quantification as possible given lbind. *) let specialize (c,lbind) ipat = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let sigma, term = if lbind == NoBindings then - let sigma = Typeclasses.resolve_typeclasses env sigma in - sigma, nf_evar sigma c + sigma, c else - let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in + let typ_of_c = Retyping.get_type_of env sigma c in + (* If the term is lambda then we put a letin to put avoid + interaction between the term and the bindings. *) + let c = match EConstr.kind sigma c with + | Lambda(_,_,_) -> + mkLetIn(Name.Anonymous, c, typ_of_c, (mkRel 1)) + | _ -> c in + let clause = make_clenv_binding env sigma (c,typ_of_c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in - let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in - let rec chk = function - | [] -> [] - | t::l -> if occur_meta t then [] else t :: chk l - in - let tstack = chk tstack in - let term = applist(thd,List.map (nf_evar clause.evd) tstack) in - if occur_meta term then - errorlabstrm "" (str "Cannot infer an instance for " ++ - - pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ - str "."); - clause.evd, term in + let sigma = clause.evd in + let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let c_hd , c_args = decompose_app sigma c in + let liftrel x = + match kind sigma x with + | Rel n -> mkRel (n+1) + | _ -> x in + (* We grab names used in product to remember them at re-abstracting phase *) + let typ_of_c_hd = pf_get_type_of gl c_hd in + let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in + (* accumulator args: arguments to apply to c_hd: all infered + args + re-abstracted rels *) + let rec rebuild_lambdas sigma lprd args hd l = + match lprd , l with + | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) + | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> + (* nme has not been resolved, let us re-abstract it. Same + name but type updated by instanciation of other args. *) + let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in + let liftedargs = List.map liftrel args in + (* lifting rels in the accumulator args *) + let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in + (* replace meta variable by the abstracted variable *) + let hd'' = subst_term sigma t hd' in + (* lambda expansion *) + sigma,mkLambda (nme,new_typ_of_t,hd'') + | Context.Rel.Declaration.LocalAssum(_,_)::lp' , t::l' -> + let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in + sigma,hd' + | _ ,_ -> assert false in + let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in + Evd.clear_metas sigma, hd + in let typ = Retyping.get_type_of env sigma term in let tac = - match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with + match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> (* Like assert (id:=id args) but with the concept of specialization *) let naming,tac = - prepare_intros false (IntroIdentifier id) MoveLast ipat in + prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) @@ -2927,17 +2963,19 @@ let specialize (c,lbind) ipat = | None -> (* Like generalize with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term) - | Some (loc,ipat) -> + (* TODO: add intro to be more homogeneous. It will break + scripts but will be easy to fix *) + (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) + | Some {CAst.loc;v=ipat} -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros_loc loc false IntroAnonymous MoveLast ipat in + let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac - end } + end (*****************************) (* Ad hoc unfold *) @@ -2947,22 +2985,23 @@ let specialize (c,lbind) ipat = (* Unfolds x by its definition everywhere *) let unfold_body x = let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + 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 _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") + | LocalAssum _ -> user_err ~hdr:"unfold_body" + (Id.print x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval in + let xval = EConstr.of_constr xval in Tacticals.New.afterHyp x begin fun aft -> - let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in + let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in let rfun _ _ c = replace_vars [x, xval] c in let reducth h = reduct_in_hyp rfun h in let reductc = reduct_in_concl (rfun, DEFAULTcast) in Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc] end - end } + end (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] @@ -3001,35 +3040,35 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) -let warn_unused_intro_pattern = +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_constr (fst (run_delayed (Global.env()) Evd.empty c)))) 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 names = - if not (List.is_empty names) && Flags.is_verbose () then - warn_unused_intro_pattern names +let check_unused_names env sigma names = + if not (List.is_empty names) then + warn_unused_intro_pattern env sigma names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous | Name id -> IntroNaming (IntroIdentifier (new_fresh_id avoid id gl)) -let rec consume_pattern avoid na isdep gl = function - | [] -> ((dloc, intropattern_of_name gl avoid na), []) - | (loc,IntroForthcoming true)::names when not isdep -> +let rec consume_pattern avoid na isdep gl = let open CAst in function + | [] -> ((CAst.make @@ intropattern_of_name gl avoid na), []) + | {loc;v=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 - ((loc,intropattern_of_name gl avoid na), fullpat) - | (loc,IntroNaming IntroAnonymous)::names -> - let avoid = 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 - ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names) + | {loc;v=IntroForthcoming _}::names as fullpat -> + let avoid = Id.Set.union avoid (explicit_intro_names names) in + (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) + | {loc;v=IntroNaming IntroAnonymous}::names -> + let avoid = Id.Set.union avoid (explicit_intro_names names) in + (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) + | {loc;v=IntroNaming (IntroFresh id')}::names -> + let avoid = Id.Set.union avoid (explicit_intro_names names) in + (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = @@ -3048,7 +3087,7 @@ let safe_dest_intro_patterns with_evars avoid thin dest pat tac = Proofview.tclORELSE (dest_intro_patterns with_evars avoid thin dest pat tac) begin function (e, info) -> match e with - | UserError ("move_hyp",_) -> + | UserError (Some "move_hyp",_) -> (* May happen e.g. with "destruct x using s" with an hypothesis which is morally an induction hypothesis to be "MoveLast" if known as such but which is considered instead as a subterm of @@ -3086,53 +3125,57 @@ 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) :: (IndArg,_,depind,hyprecname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with - | [loc,IntroNaming (IntroIdentifier id) as pat] -> + | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in - (pat, [dloc, IntroNaming (IntroIdentifier id')]) + (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin) - end }) - end } + end) + end | (IndArg,_,dep,hyprecname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) - end } + end | (RecArg,_,dep,recvarname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end } + end | (OtherArg,_,dep,_) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end } + end | [] -> - check_unused_names names; + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + check_unused_names env sigma names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) + end in peel_tac ra dests names [] @@ -3141,26 +3184,26 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = substitutions aussi sur l'argument voisin *) let expand_projections env sigma c = - let sigma = Sigma.to_evar_map sigma in let rec aux env c = - match kind_of_term c with + match EConstr.kind sigma c with | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) [] - | _ -> map_constr_with_full_binders push_rel aux env c - in aux env c + | _ -> map_constr_with_full_binders sigma push_rel aux env c + in + aux env c (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in + let sigma = Tacmach.New.project 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 typ0 in - let hd,argl = decompose_app indtyp in + let prods, indtyp = decompose_prod_assum sigma typ0 in + let hd,argl = decompose_app sigma indtyp in let env' = push_rel_context prods env in - let sigma = Proofview.Goal.sigma gl in let params = List.firstn nparams argl in let params' = List.map (expand_projections env' sigma) params in (* le gl est important pour ne pas préévaluer *) @@ -3172,17 +3215,18 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (tac avoid) else let c = List.nth argl (i-1) in - match kind_of_term c with - | Var id when not (List.exists (occur_var env id) args') && - not (List.exists (occur_var env id) params') -> + match EConstr.kind sigma c with + | Var id when not (List.exists (fun c -> occur_var env sigma id c) args') && + not (List.exists (fun c -> occur_var env sigma id c) params') -> (* 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 - if List.exists (dependent c) params' || - List.exists (dependent c) args' + let dependent t = dependent sigma c t in + if List.exists dependent params' || + List.exists dependent args' then (* This is a case where the argument is constrained in a way which would require some kind of inversion; we @@ -3194,18 +3238,18 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (* We reason blindly on the term and do as if it were generalizable, ignoring the constraints coming from its structure *) - let id = match kind_of_term c with + let id = match EConstr.kind sigma c with | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in 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) [] [] [] - end } + atomize_one (List.length argl) [] [] Id.Set.empty + end (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps @@ -3272,12 +3316,11 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = exception Shunt of Id.t move_location -let cook_sign hyp0_opt inhyps indvars env = +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 open Context.Named.Declaration in 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 @@ -3285,7 +3328,8 @@ let cook_sign hyp0_opt inhyps indvars env = let before = ref true in let maindep = ref false in let seek_deps env decl rhyp = - let hyp = get_id decl in + let decl = map_named_decl EConstr.of_constr decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then begin before:=false; @@ -3293,24 +3337,24 @@ let cook_sign hyp0_opt inhyps indvars env = 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; rhyp end else let dephyp0 = List.is_empty inhyps && - (Option.cata (fun id -> occur_var_in_decl env id decl) false hyp0_opt) + (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 id decl) indvars || - List.exists (fun decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps) + (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; @@ -3327,7 +3371,7 @@ let cook_sign hyp0_opt inhyps indvars env = let _ = fold_named_context seek_deps env ~init:MoveFirst in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp decl = - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then raise (Shunt lhyp); if Id.List.mem hyp !ldeps then begin @@ -3377,15 +3421,15 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) - predicates: Context.Rel.t; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) npredicates: int; (* Number of predicates *) - branches: Context.Rel.t; (* branchr,...,branch1 *) + branches: rel_context; (* branchr,...,branch1 *) nbranches: int; (* Number of branches *) - args: Context.Rel.t; (* (xni, Ti_ni) ... (x1, Ti_1) *) + args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (* number of arguments *) - indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni) + indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) concl: types; (* Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) @@ -3434,44 +3478,44 @@ 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 let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in - errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") + user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") -let glob = Universes.constr_of_global +let coq_eq sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq ()) +let coq_eq_refl sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ()) -let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) -let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ())) +let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq") +let coq_heq sigma = Evarutil.new_global sigma (Lazy.force coq_heq_ref) +let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") -let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq") -let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl") +let mkEq sigma t x y = + let sigma, eq = coq_eq sigma in + sigma, mkApp (eq, [| t; x; y |]) +let mkRefl sigma t x = + let sigma, refl = coq_eq_refl sigma in + sigma, mkApp (refl, [| t; x |]) -let mkEq t x y = - mkApp (Lazy.force coq_eq, [| t; x; y |]) +let mkHEq sigma t x u y = + let sigma, c = coq_heq sigma in + sigma, mkApp (c,[| t; x; u; y |]) -let mkRefl t x = - mkApp (Lazy.force coq_eq_refl, [| t; x |]) - -let mkHEq t x u y = - mkApp (Lazy.force coq_heq, - [| t; x; u; y |]) - -let mkHRefl t x = - mkApp (Lazy.force coq_heq_refl, - [| t; x |]) +let mkHRefl sigma t x = + let sigma, c = coq_heq_refl sigma in + sigma, mkApp (c, [| t; x |]) let lift_togethern n l = let l', _ = @@ -3483,24 +3527,24 @@ let lift_togethern n l = let lift_list l = List.map (lift 1) l -let ids_of_constr ?(all=false) vars c = +let ids_of_constr sigma ?(all=false) vars c = let rec aux vars c = - match kind_of_term c with + match EConstr.kind sigma c with | Var id -> Id.Set.add id vars | App (f, args) -> - (match kind_of_term f with + (match EConstr.kind sigma f with | Construct ((ind,_),_) | Ind (ind,_) -> let (mib,mip) = Global.lookup_inductive ind in Array.fold_left_from (if all then 0 else mib.Declarations.mind_nparams) aux vars args - | _ -> fold_constr aux vars c) - | _ -> fold_constr aux vars c + | _ -> EConstr.fold sigma aux vars c) + | _ -> EConstr.fold sigma aux vars c in aux vars c -let decompose_indapp f args = - match kind_of_term f with +let decompose_indapp sigma f args = + match EConstr.kind sigma f with | Construct ((ind,_),_) | Ind (ind,_) -> let (mib,mip) = Global.lookup_inductive ind in @@ -3509,23 +3553,29 @@ let decompose_indapp f args = mkApp (f, pars), args | _ -> f, args -let mk_term_eq env sigma ty t ty' t' = - let sigma = Sigma.to_evar_map sigma in - if Reductionops.is_conv env sigma ty ty' then - mkEq ty t t', mkRefl ty' t' +let mk_term_eq homogeneous env sigma ty t ty' t' = + if homogeneous then + let sigma, eq = mkEq sigma ty t t' in + let sigma, refl = mkRefl sigma ty' t' in + sigma, (eq, refl) else - mkHEq ty t ty' t', mkHRefl ty' t' + let sigma, heq = mkHEq sigma ty t ty' t' in + let sigma, hrefl = mkHRefl sigma ty' t' in + sigma, (heq, hrefl) let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let open Context.Rel.Declaration in - Refine.refine { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let eqslen = List.length eqs in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) - let abshypeq, abshypt = + let sigma, abshypeq, abshypt = if dep then - let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in - mkProd (Anonymous, eq, lift 1 concl), [| refl |] - else concl, [||] + let ty = lift 1 c in + let homogeneous = Reductionops.is_conv env sigma ty typ in + let sigma, (eq, refl) = + mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in + sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |] + else sigma, concl, [||] in (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) @@ -3539,7 +3589,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn genarg ctx in (* The goal will become this product. *) - let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in + let (sigma, genc) = Evarutil.new_evar env sigma ~principal:true genctyp in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instantiated hyp. *) @@ -3547,21 +3597,20 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) - Sigma (mkApp (appeqs, abshypt), sigma, p) - end } + (sigma, mkApp (appeqs, abshypt)) + end -let hyps_of_vars env sign nogen hyps = - let open Context.Named.Declaration in +let hyps_of_vars env sigma sign nogen hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside (fun (hs,hl) d -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) else - let xvars = global_vars_set_of_decl env d in + let xvars = global_vars_set_of_decl env sigma d in if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then (Id.Set.add x hs, x :: hl) else (hs, hl)) @@ -3571,11 +3620,11 @@ let hyps_of_vars env sign nogen hyps = exception Seen -let linear vars args = +let linear sigma vars args = let seen = ref vars in try Array.iter (fun i -> - let rels = ids_of_constr ~all:true Id.Set.empty i in + let rels = ids_of_constr sigma ~all:true Id.Set.empty i in let seen' = Id.Set.fold (fun id acc -> if Id.Set.mem id acc then raise Seen @@ -3587,19 +3636,19 @@ let linear vars args = with Seen -> false let is_defined_variable env id = - let open Context.Named.Declaration in - lookup_named id env |> is_local_def + env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = + let open Tacmach.New in let open Context.Rel.Declaration in - let sigma = ref (Tacmach.project gl) in - let env = Tacmach.pf_env gl in - let concl = Tacmach.pf_concl gl in - let dep = dep || dependent (mkVar id) concl in - let avoid = ref [] in + let sigma = ref (Tacmach.New.project gl) in + 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 Id.Set.empty in let get_id name = - let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in - avoid := id :: !avoid; id + let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in + 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 @@ -3611,15 +3660,15 @@ let abstract_args gl generalize_vars dep id defined f args = let name, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in - get_name decl, get_type decl, c + RelDecl.get_name decl, RelDecl.get_type decl, c in - let argty = Tacmach.pf_unsafe_type_of gl arg in + let argty = Tacmach.New.pf_unsafe_type_of gl arg in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in - let leq = constr_cmp Reduction.CUMUL liftargty ty in - match kind_of_term arg with + let leq = constr_cmp !sigma Reduction.CUMUL liftargty ty in + match EConstr.kind !sigma arg with | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) -> (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Id.Set.add id nongenvars, Id.Set.remove id vars, env) @@ -3632,29 +3681,33 @@ let abstract_args gl generalize_vars dep id defined f args = let liftarg = lift (List.length ctx) arg in let eq, refl = if leq then - mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg + let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in + let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in + sigma := sigma'; eq, refl else - mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg + let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in + let sigma', refl = mkHRefl sigma' argty arg in + sigma := sigma'; eq, refl in let eqs = eq :: lift_list eqs in let refls = refl :: refls in - let argvars = ids_of_constr vars arg in + let argvars = ids_of_constr !sigma vars arg in (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, nongenvars, Id.Set.union argvars vars, env) in - let f', args' = decompose_indapp f args in + let f', args' = decompose_indapp !sigma f args in let dogen, f', args' = - let parvars = ids_of_constr ~all:true Id.Set.empty f' in - if not (linear parvars args') then true, f, args + let parvars = ids_of_constr !sigma ~all:true Id.Set.empty f' in + if not (linear !sigma parvars args') then true, f, args else - match Array.findi (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with + match Array.findi (fun i x -> not (isVar !sigma x) || is_defined_variable env (destVar !sigma x)) args' with | None -> false, f', args' | Some nonvar -> let before, after = Array.chop nonvar args' in true, mkApp (f', before), after in if dogen then - let tyf' = Tacmach.pf_unsafe_type_of gl f' in + let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in @@ -3662,14 +3715,14 @@ let abstract_args gl generalize_vars dep id defined f args = let vars = if generalize_vars then let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars + hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars else [] in let body, c' = if defined then Some c', Retyping.get_type_of ctxenv !sigma c' else None, c' in - let typ = Tacmach.pf_get_hyp_typ gl id in + let typ = Tacmach.New.pf_get_hyp_typ id gl in let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in Some (tac, dep, succ (List.length ctx), vars) @@ -3677,21 +3730,22 @@ let abstract_args gl generalize_vars dep id defined f args = let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let open Context.Named.Declaration in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Coqlib.check_required_library Coqlib.jmeq_module_name; + let sigma = Tacmach.New.project gl in let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in match Tacmach.New.pf_get_hyp id gl with - | LocalAssum (_,t) -> let f, args = decompose_app t in + | LocalAssum (_,t) -> let f, args = decompose_app sigma t in (f, args, false, id, oldid) | LocalDef (_,t,_) -> - let f, args = decompose_app t in + let f, args = decompose_app sigma t in (f, args, true, id, oldid) in if List.is_empty args then Proofview.tclUNIT () else let args = Array.of_list args in - let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in + let newc = abstract_args gl generalize_vars force_dep id def f args in match newc with | None -> Proofview.tclUNIT () | Some (tac, dep, n, vars) -> @@ -3712,35 +3766,41 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = [revert vars ; Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars]) - end } + end -let rec compare_upto_variables x y = - if (isVar x || isRel x) && (isVar y || isRel y) then true - else compare_constr compare_upto_variables x y +let compare_upto_variables sigma x y = + let rec compare x y = + if (isVar sigma x || isRel sigma x) && (isVar sigma y || isRel sigma y) then true + else compare_constr sigma compare x y + in + compare x y -let specialize_eqs id gl = +let specialize_eqs id = let open Context.Rel.Declaration in - let env = Tacmach.pf_env gl in - let ty = Tacmach.pf_get_hyp_typ gl id in - let evars = ref (project gl) in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let ty = Tacmach.New.pf_get_hyp_typ id gl in + let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = - compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 + compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 in let rec aux in_eqs ctx acc ty = - match kind_of_term ty with + match EConstr.kind !evars ty with | Prod (na, t, b) -> - (match kind_of_term t with - | App (eq, [| eqty; x; y |]) when Term.eq_constr (Lazy.force coq_eq) eq -> - let c = if noccur_between 1 (List.length ctx) x then y else x in - let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in - let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in + (match EConstr.kind !evars t with + | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq -> + let c = if noccur_between !evars 1 (List.length ctx) x then y else x in + let pt = mkApp (eq, [| eqty; c; c |]) in + let ind = destInd !evars eq in + let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when Term.eq_constr heq (Lazy.force coq_heq) -> - let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in - let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in - let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in + | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> + let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in + let pt = mkApp (heq, [| eqt; c; eqt; c |]) in + let ind = destInd !evars heq in + let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty @@ -3754,7 +3814,7 @@ let specialize_eqs id gl = let acc, worked, ctx, ty = aux false [] (mkVar id) ty in let ctx' = nf_rel_context_evar !evars ctx in let ctx'' = List.map (function - | LocalDef (n,k,t) when isEvar k -> LocalAssum (n,t) + | LocalDef (n,k,t) when isEvar !evars k -> LocalAssum (n,t) | decl -> decl) ctx' in let ty' = it_mkProd_or_LetIn ty ctx'' in @@ -3763,20 +3823,22 @@ let specialize_eqs id gl = and acc' = Tacred.whd_simpl env !evars acc' in let ty' = Evarutil.nf_evar !evars ty' in if worked then - tclTHENFIRST (Tacmach.internal_cut true id ty') - (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl - else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl - + Tacticals.New.tclTHENFIRST + (internal_cut true id ty') + (exact_no_check ((* refresh_universes_strict *) acc')) + else + Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id) + end -let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl -> +let specialize_eqs id = Proofview.Goal.enter begin fun gl -> let msg = str "Specialization not allowed on dependent hypotheses" in Proofview.tclOR (clear [id]) (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> - Proofview.V82.tactic (specialize_eqs id) -end } + specialize_eqs id +end -let occur_rel n c = - let res = not (noccurn n c) in +let occur_rel sigma n c = + let res = not (noccurn sigma n c) in res (* This function splits the products of the induction scheme [elimt] into four @@ -3787,20 +3849,20 @@ let occur_rel n c = if there is no branch, we try to fill in acc3 with args/indargs. We also return the conclusion. *) -let decompose_paramspred_branch_args elimt = +let decompose_paramspred_branch_args sigma elimt = let open Context.Rel.Declaration in let rec cut_noccur elimt acc2 = - match kind_of_term elimt with + match EConstr.kind sigma elimt with | Prod(nme,tpe,elimt') -> - let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in - if not (occur_rel 1 elimt') && isRel hd_tpe + let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in + if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2) - else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl + else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt | _ -> error_ind_scheme "" in let rec cut_occur elimt acc1 = - match kind_of_term elimt with - | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c (LocalAssum (nme,tpe)::acc1) + match EConstr.kind sigma elimt with + | Prod(nme,tpe,c) when occur_rel sigma 1 c -> cut_occur c (LocalAssum (nme,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl | App(_, _) | Rel _ -> acc1,[],[],elimt | _ -> error_ind_scheme "" in @@ -3813,17 +3875,17 @@ let decompose_paramspred_branch_args elimt = args. We suppose there is only one predicate here. *) match acc2 with | [] -> - let hyps,ccl = decompose_prod_assum elimt in - let hd_ccl_pred,_ = decompose_app ccl in - begin match kind_of_term hd_ccl_pred with + let hyps,ccl = decompose_prod_assum sigma elimt in + let hd_ccl_pred,_ = decompose_app sigma ccl in + begin match EConstr.kind sigma hd_ccl_pred with | Rel i -> let acc3,acc1 = List.chop (i-1) hyps in acc1 , [] , acc3 , ccl | _ -> error_ind_scheme "" end | _ -> acc1, acc2 , acc3, ccl -let exchange_hd_app subst_hd t = - let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) +let exchange_hd_app sigma subst_hd t = + let hd,args= decompose_app sigma t in mkApp (subst_hd,Array.of_list args) (* Builds an elim_scheme from its type and calling form (const+binding). We first separate branches. We obtain branches, hyps before (params + preds), @@ -3841,14 +3903,14 @@ let exchange_hd_app subst_hd t = predicates are cited in the conclusion. - finish to fill in the elim_scheme: indarg/farg/args and finally indref. *) -let compute_elim_sig ?elimc elimt = +let compute_elim_sig sigma ?elimc elimt = let open Context.Rel.Declaration in let params_preds,branches,args_indargs,conclusion = - decompose_paramspred_branch_args elimt in + decompose_paramspred_branch_args sigma elimt in - let ccl = exchange_hd_app (mkVar (Id.of_string "__QI_DUMMY__")) conclusion in + let ccl = exchange_hd_app sigma (mkVar (Id.of_string "__QI_DUMMY__")) conclusion in let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in - let nparams = Int.Set.cardinal (free_rels concl_with_args) in + let nparams = Int.Set.cardinal (free_rels sigma concl_with_args) in let preds,params = List.chop (List.length params_preds - nparams) params_preds in (* A first approximation, further analysis will tweak it *) @@ -3857,7 +3919,7 @@ let compute_elim_sig ?elimc elimt = elimc = elimc; elimt = elimt; concl = conclusion; predicates = preds; npredicates = List.length preds; branches = branches; nbranches = List.length branches; - farg_in_concl = isApp ccl && isApp (last_arg ccl); + farg_in_concl = isApp sigma ccl && isApp sigma (last_arg sigma ccl); params = params; nparams = nparams; (* all other fields are unsure at this point. Including these:*) args = args_indargs; nargs = List.length args_indargs; } in @@ -3878,9 +3940,9 @@ let compute_elim_sig ?elimc elimt = match List.hd args_indargs with | LocalDef (hiname,_,hi) -> error_ind_scheme "" | LocalAssum (hiname,hi) -> - let hi_ind, hi_args = decompose_app hi in + let hi_ind, hi_args = decompose_app sigma hi in let hi_is_ind = (* hi est d'un type globalisable *) - match kind_of_term hi_ind with + match EConstr.kind sigma hi_ind with | Ind (mind,_) -> true | Var _ -> true | Const _ -> true @@ -3893,7 +3955,7 @@ let compute_elim_sig ?elimc elimt = else (* Last arg is the indarg *) res := {!res with indarg = Some (List.hd !res.args); - indarg_in_concl = occur_rel 1 ccl; + indarg_in_concl = occur_rel sigma 1 ccl; args = List.tl !res.args; nargs = !res.nargs - 1; }; raise Exit); @@ -3903,49 +3965,49 @@ let compute_elim_sig ?elimc elimt = | None -> !res (* No indref *) | Some (LocalDef _) -> error_ind_scheme "" | Some (LocalAssum (_,ind)) -> - let indhd,indargs = decompose_app ind in - try {!res with indref = Some (global_of_constr indhd) } + let indhd,indargs = decompose_app sigma ind in + try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } with e when CErrors.noncritical e -> error "Cannot find the inductive type of the inductive scheme." -let compute_scheme_signature scheme names_info ind_type_guess = +let compute_scheme_signature evd scheme names_info ind_type_guess = let open Context.Rel.Declaration in - let f,l = decompose_app scheme.concl in + let f,l = decompose_app evd scheme.concl in (* Vérifier que les arguments de Qi sont bien les xi. *) let cond, check_concl = match scheme.indarg with | Some (LocalDef _) -> error "Strange letin, cannot recognize an induction scheme." | None -> (* Non standard scheme *) - let cond hd = Term.eq_constr hd ind_type_guess && not scheme.farg_in_concl + let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl in (cond, fun _ _ -> ()) | Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *) - let indhd,indargs = decompose_app ind in - let cond hd = Term.eq_constr hd indhd in + let indhd,indargs = decompose_app evd ind in + let cond hd = EConstr.eq_constr evd hd indhd in let check_concl is_pred p = (* Check again conclusion *) let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in let ind_is_ok = - List.equal Term.eq_constr + List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2) (List.lastn scheme.nargs indargs) - (Context.Rel.to_extended_list 0 scheme.args) in + (Context.Rel.to_extended_list mkRel 0 scheme.args) in if not (ccl_arg_ok && ind_is_ok) then error_ind_scheme "the conclusion of" in (cond, check_concl) in let is_pred n c = - let hd = fst (decompose_app c) in - match kind_of_term hd with + let hd = fst (decompose_app evd c) in + match EConstr.kind evd hd with | Rel q when n < q && q <= n+scheme.npredicates -> IndArg | _ when cond hd -> RecArg | _ -> OtherArg in let rec check_branch p c = - match kind_of_term c with + match EConstr.kind evd c with | Prod (_,t,c) -> - (is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c + (is_pred p t, true, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c | LetIn (_,_,_,c) -> - (OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c + (OtherArg, false, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c | _ when is_pred p c == IndArg -> [] | _ -> raise Exit in @@ -3977,55 +4039,59 @@ let compute_scheme_signature scheme names_info ind_type_guess = the non standard case, naming of generated hypos is slightly different. *) let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = - let scheme = compute_elim_sig ~elimc:elimc elimt in - evd, (compute_scheme_signature scheme names_info ind_type_guess, scheme) + let scheme = compute_elim_sig evd ~elimc:elimc elimt in + evd, (compute_scheme_signature evd scheme names_info ind_type_guess, scheme) let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in + let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in let evd, elimc = - if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl + if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl else let env = Tacmach.New.pf_env gl in - let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in - if use_dependent_propositions_elimination () && dep - then - let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in - (Sigma.to_evar_map sigma, ind) + let sigma = Tacmach.New.project gl in + let u = EInstance.kind (Tacmach.New.project gl) u in + 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) else - let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in - (Sigma.to_evar_map sigma, ind) + let (sigma, ind) = build_case_analysis_scheme_default env sigma (mind, u) s in + let ind = EConstr.of_constr ind in + (sigma, ind) in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - evd, ((elimc, NoBindings), elimt), mkIndU mind + evd, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = + let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess + let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in + let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in + 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 * types) * scheme_signature + | ElimUsing of (eliminator * EConstr.types) * scheme_signature | ElimOver of bool * Id.t let find_induction_type isrec elim hyp0 gl = + let sigma = Tacmach.New.project gl in let scheme,elim = 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 ~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 ~elimc elimt in + let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature scheme hyp0 ind_guess in + let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in scheme, ElimUsing (elim,indsign) in @@ -4037,7 +4103,8 @@ let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in + let sigma = Tacmach.New.project gl in + let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -4046,27 +4113,28 @@ let is_functional_induction elimc gl = need a dependent one or not *) let get_eliminator elim dep s gl = - let open Context.Rel.Declaration in match elim with | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in + let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) + (List.rev s.branches) + in evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are arguments. Returns the clause obtained. *) let recolle_clenv i params args elimclause gl = - let _,arr = destApp elimclause.templval.rebus in + let _,arr = destApp elimclause.evd elimclause.templval.rebus in let lindmv = Array.map (fun x -> - match kind_of_term x with + match EConstr.kind elimclause.evd x with | Meta mv -> mv - | _ -> errorlabstrm "elimination_clause" + | _ -> user_err ~hdr:"elimination_clause" (str "The type of the elimination clause is not well-formed.")) arr in let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in @@ -4085,7 +4153,7 @@ let recolle_clenv i params args elimclause gl = (* from_n (Some 0) means that x should be taken "as is" without trying to unify (which would lead to trying to apply it to evars if y is a product). *) - let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in + let indclause = mk_clenv_from_n gl (Some 0) (x,y) in let elimclause' = clenv_fchain ~with_univs:false i acc indclause in elimclause') (List.rev clauses) @@ -4096,49 +4164,49 @@ let recolle_clenv i params args elimclause gl = produce new ones). Then refine with the resulting term with holes. *) let induction_tac with_evars params indvars elim = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project gl in let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in - let i = match i with None -> index_of_ind_arg elimt | Some i -> i in + let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) - let elimc = contract_letin_in_lam_header elimc in + let elimc = contract_letin_in_lam_header sigma elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in - let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in + let elimclause = Tacmach.New.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in (* elimclause' is built from elimclause by instanciating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) - let resolved = Tacmach.New.of_old (clenv_unique_resolver ~flags:(elim_flags ()) elimclause') gl in - enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) - end } + let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in + Clenvtac.clenv_refine with_evars resolved + end (* Apply induction "in place" taking into account dependent hypotheses from the context, replacing the main hypothesis on which induction applies with the induction hypotheses *) let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac = - let open Context.Named.Declaration in - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map sigma in - let concl = Tacmach.New.pf_nf_concl gl in - let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env in - let dep_in_concl = Option.cata (fun id -> occur_var env id concl) false hyp0 in + let concl = Tacmach.New.pf_concl gl in + let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in + let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in let dep = dep_in_hyps || dep_in_concl in let tmpcl = it_mkNamedProd_or_LetIn concl deps in let s = Retyping.get_sort_family_of env sigma tmpcl in let deps_cstr = List.fold_left - (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in - let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in + (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 gl in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in let names = compute_induction_names branchletsigns names in + Array.iter (check_name_unicity env toclear []) names; let tac = (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; @@ -4148,16 +4216,16 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (re_intro_dependent_hypotheses statuslists)) indsign names) in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac + end let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = - Proofview.Goal.enter { enter = begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in + Proofview.Goal.enter begin fun gl -> + 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)) - end } + end let msg_not_right_number_induction_arguments scheme = str"Not the right number of induction arguments (expected " ++ @@ -4174,7 +4242,7 @@ let msg_not_right_number_induction_arguments scheme = must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac *) let induction_without_atomization isrec with_evars elim names lid = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in let nargs_indarg_farg = scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in @@ -4193,7 +4261,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; @@ -4205,33 +4273,31 @@ let induction_without_atomization isrec with_evars elim names lid = ] in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context with_evars None [] elim indvars names induct_tac - end } + end (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let open Context.Named.Declaration in - if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && + Proofview.Goal.enter begin fun gl -> + if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences - then errorlabstrm "" - (str "Conclusion must be mentioned: it depends on " ++ pr_id id + then user_err + (str "Conclusion must be mentioned: it depends on " ++ Id.print id ++ str "."); match cls.onhyps with | Some hyps -> let to_erase d = - let id' = get_id d in + let id' = NamedDecl.get_id d in if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) - let test id = occur_var_in_decl (Tacmach.New.pf_env gl) id d in + let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in if List.exists test (id::inhyps) then Some id' else None in let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in clear ids | None -> Proofview.tclUNIT () - end } + end let use_bindings env sigma elim must_be_closed (c,lbind) typ = - let sigma = Sigma.to_evar_map sigma in let typ = if elim == None then (* w/o an scheme, the term has to be applied at least until @@ -4250,11 +4316,10 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = let rec find_clause typ = try let indclause = make_clenv_binding env sigma (c,typ) lbind in - if must_be_closed && occur_meta (clenv_value indclause) then + if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) - let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in - Sigma.Unsafe.of_pair (c, sigma) + pose_all_metas_as_evars env indclause.evd (clenv_value indclause) with e when catchable_exception e -> try find_clause (try_red_product env sigma typ) with Redelimination -> raise e in @@ -4268,20 +4333,19 @@ let check_expected_type env sigma (elimc,bl) elimt = if n == 0 then error "Scheme cannot be applied."; let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in - let (_,u,_) = destProd cl.cl_concl in + let (_,u,_) = destProd sigma cl.cl_concl in fun t -> Evarconv.e_cumul env (ref sigma) t u let check_enough_applied env sigma elim = - let sigma = Sigma.to_evar_map sigma in (* A heuristic to decide whether the induction arg is enough applied *) match elim with | None -> (* No eliminator given *) fun u -> - let t,_ = decompose_app (whd_all env sigma u) in isInd t + let t,_ = decompose_app sigma (whd_all env sigma u) in isInd sigma t | Some elimc -> let elimt = Retyping.get_type_of env sigma (fst elimc) in - let scheme = compute_elim_sig ~elimc elimt in + let scheme = compute_elim_sig sigma ~elimc elimt in match scheme.indref with | None -> (* in the absence of information, do not assume it may be @@ -4292,28 +4356,32 @@ 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 = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let ccl = Proofview.Goal.raw_concl gl in + let ccl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in - let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in + let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with | None -> (* pattern not found *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in + let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in + let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in - let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in + let (sigma, c0) = finish_evar_resolution ~flags env sigma (pending,c0) in let tac = (if isrec then (* Historically, induction has side conditions last *) @@ -4322,68 +4390,68 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* and destruct has side conditions first *) Tacticals.New.tclTHENLAST) (Tacticals.New.tclTHENLIST [ - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let b = not with_evars && with_eq != None in - let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in - Sigma (ans, sigma, p +> q) - end }; + let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in + let t = Retyping.get_type_of env sigma c in + mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) + end; if with_evars then Proofview.shelve_unifiable else guard_no_unifiable; if is_arg_pure_hyp - then Tacticals.New.tclTRY (clear [destVar c0]) + then Proofview.tclEVARMAP >>= fun sigma -> Tacticals.New.tclTRY (clear [destVar sigma c0]) else Proofview.tclUNIT (); if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) - tac + (tac inhyps) in - Sigma (tac, sigma, q) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac - | Some (Sigma (c, sigma', q)) -> + | Some (sigma', c) -> (* pattern found *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) let env = reset_with_named_context sign env in + let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in + let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in let tac = Tacticals.New.tclTHENLIST [ - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None - end }; - tac + end; + (tac inhyps) ] in - Sigma (tac, sigma', p +> q) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac + end -let has_generic_occurrences_but_goal cls id env ccl = +let has_generic_occurrences_but_goal cls id env sigma ccl = clause_with_generic_context_selection cls && (* TODO: whd_evar of goal *) - (cls.concl_occs != NoOccurrences || not (occur_var env id ccl)) + (cls.concl_occs != NoOccurrences || not (occur_var env sigma id ccl)) let induction_gen clear_flag isrec with_evars elim ((_pending,(c,lbind)),(eqname,names) as arg) cls = let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let ccl = Proofview.Goal.raw_concl gl in + let evd = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.concl gl in let cls = Option.default allHypsAndConcl cls in - let t = typ_of env sigma c in + let t = typ_of env evd c in let is_arg_pure_hyp = - isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ())) + isVar evd c && not (mem_named_context_val (destVar evd c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None - && has_generic_occurrences_but_goal cls (destVar c) env ccl in - let enough_applied = check_enough_applied env sigma elim t in + && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in + let enough_applied = check_enough_applied env evd elim t in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and with maximal abstraction over the variable. This is a situation where the induction argument is a clearable variable of the goal w/o occurrence selection and w/o equality kept: no need to generalize *) - let id = destVar c in + let id = destVar evd c in Tacticals.New.tclTHEN (clear_unselected_context id inhyps cls) (induction_with_atomization_of_ind_arg @@ -4393,14 +4461,14 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) - let x = id_of_name_using_hdchar (Global.env()) t Anonymous in - new_fresh_id [] x gl in + let x = id_of_name_using_hdchar env evd t Anonymous 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 (induction_with_atomization_of_ind_arg - isrec with_evars elim names id inhyps) - end } + isrec with_evars elim names id) + end (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4411,32 +4479,35 @@ let induction_gen_l isrec with_evars elim names lc = let newlc = ref [] in let lc = List.map (function | (c,None) -> c - | (c,Some(loc,eqname)) -> - user_err_loc (loc,"",str "Do not know what to do with " ++ + | (c,Some{CAst.loc;v=eqname}) -> + user_err ?loc (str "Do not know what to do with " ++ Miscprint.pr_intro_pattern_naming eqname)) lc in let rec atomize_list l = match l with | [] -> Proofview.tclUNIT () | c::l' -> - match kind_of_term c with + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma c with | Var id when not (mem_named_context_val id (Global.named_context_val ())) && not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' | _ -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in + let sigma = Tacmach.New.project gl in + Proofview.tclENV >>= fun env -> let x = - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in - let id = new_fresh_id [] x gl in - let newl' = List.map (replace_term c (mkVar id)) l' 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 (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') - end } in + end in Tacticals.New.tclTHENLIST [ (atomize_list lc); @@ -4453,7 +4524,7 @@ let induction_destruct isrec with_evars (lc,elim) = match lc with | [] -> assert false (* ensured by syntax, but if called inside caml? *) | [c,(eqname,names as allnames),cls] -> - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match elim with @@ -4470,9 +4541,9 @@ let induction_destruct isrec with_evars (lc,elim) = (* standard induction *) onOpenInductionArg env sigma (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c - end } + end | _ -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match elim with @@ -4488,12 +4559,12 @@ let induction_destruct isrec with_evars (lc,elim) = (onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag isrec with_evars None (a,b) cl) a) (Tacticals.New.tclMAP (fun (a,b,cl) -> - Proofview.Goal.enter { enter = begin fun gl -> + 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) + end) l) | Some elim -> (* Several induction hyps with induction scheme *) let lc = List.map (on_pi1 (fun c -> snd (force_destruction_arg false env sigma c))) lc in @@ -4512,39 +4583,15 @@ let induction_destruct isrec with_evars (lc,elim) = error "'as' clause with multiple arguments and 'using' clause can only occur last."; let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc - end } + end let induction ev clr c l e = - induction_gen clr true ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None + induction_gen clr true ev e + ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = induction_gen clr false ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None - -(* The registered tactic, which calls the default elimination - * if no elimination constant is provided. *) - -(* Induction tactics *) - -(* This was Induction before 6.3 (induction only in quantified premisses) *) -let simple_induct_id s = Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_elim) -let simple_induct_nodep n = Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_elim) - -let simple_induct = function - | NamedHyp id -> simple_induct_id id - | AnonHyp n -> simple_induct_nodep n - -(* Destruction tactics *) - -let simple_destruct_id s = - (Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_case)) -let simple_destruct_nodep n = - (Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_case)) - -let simple_destruct = function - | NamedHyp id -> simple_destruct_id id - | AnonHyp n -> simple_destruct_nodep n + ((Evd.empty,(c,NoBindings)),(None,l)) None (* * Eliminations giving the type instead of the proof. @@ -4554,34 +4601,36 @@ let simple_destruct = function *) let elim_scheme_type elim t = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in - match kind_of_term (last_arg clause.templval.rebus) with + Proofview.Goal.enter begin fun gl -> + let clause = mk_clenv_type_of gl elim in + match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> let clause' = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false - | _ -> anomaly (Pp.str "elim_scheme_type") - end } + | _ -> anomaly (Pp.str "elim_scheme_type.") + end let elim_type t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in - Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) + end let case_type t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Tacmach.New.pf_env gl in - let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in + let ((ind, u), t) = reduce_to_atomic_ind env sigma t in + let u = EInstance.kind sigma u in let s = Tacticals.New.elimination_sort_of_goal gl in - let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in - Sigma (elim_scheme_type elimc t, evd, p) - end } + let (evd, elimc) = build_case_analysis_scheme_default env sigma (ind, u) s in + let elimc = EConstr.of_constr elimc in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) + end (************************************************) @@ -4593,7 +4642,7 @@ let case_type t = let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make () let maybe_betadeltaiota_concl allowred gl = - let concl = Tacmach.New.pf_nf_concl gl in + let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in if not allowred then concl else @@ -4601,15 +4650,16 @@ let maybe_betadeltaiota_concl allowred gl = whd_all env sigma concl let reflexivity_red allowred = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match match_with_equality_type concl with + match match_with_equality_type sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings - end } + end let reflexivity = Proofview.tclORELSE @@ -4643,27 +4693,29 @@ let prove_symmetry hdcncl eq_kind = Tacticals.New.onLastHyp simplest_case; one_constructor 1 NoBindings ]) -let match_with_equation c = +let match_with_equation sigma c = + Proofview.tclENV >>= fun env -> try - let res = match_with_equation c in + let res = match_with_equation env sigma c in Proofview.tclUNIT res with NoEquationFound -> Proofview.tclZERO NoEquationFound let symmetry_red allowred = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation concl >>= fun with_eqn -> + match_with_equation sigma concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) - (Tacticals.New.pf_constr_of_global eq_data.sym apply) + (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind - end } + end let symmetry = Proofview.tclORELSE @@ -4677,17 +4729,19 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project gl in let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in - let sign,t = decompose_prod_assum ctype in + let sign,t = decompose_prod_assum sigma ctype in Proofview.tclORELSE begin - match_with_equation t >>= fun (_,hdcncl,eq) -> - let symccl = match eq with + match_with_equation sigma t >>= fun (_,hdcncl,eq) -> + let symccl = + match eq with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in - Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) + Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) [ intro_replacing id; Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] end @@ -4695,7 +4749,7 @@ let symmetry_in id = | NoEquationFound -> Hook.get forward_setoid_symmetry_in id | e -> Proofview.tclZERO ~info e end - end } + end let intros_symmetry = Tacticals.New.onClause @@ -4720,7 +4774,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4740,27 +4794,28 @@ let prove_transitivity hdcncl eq_kind t = [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; assumption ])) - end } + end let transitivity_red allowred t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation concl >>= fun with_eqn -> + match_with_equation sigma concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) (match t with - | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply - | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t])) + | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply + | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) | None,eq,eq_kind -> match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") | Some t -> prove_transitivity eq eq_kind t - end } + end let transitivity_gen t = Proofview.tclORELSE @@ -4780,18 +4835,24 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) is solved by tac *) (** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl evd d1 d2 = +let interpretable_as_section_decl env evd d1 d2 = let open Context.Named.Declaration in + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with + | None -> false + | Some cstr -> + try ignore (Evd.add_universe_constraints !sigma cstr); true + with UniversesDiffer -> false + in match d2, d1 with | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2) + | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type 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) -> @@ -4799,7 +4860,8 @@ let rec decompose len c t accu = | _ -> assert false let rec shrink ctx sign c t accu = - let open Context.Rel.Declaration in + let open Constr in + let open CVars in match ctx, sign with | [], [] -> (c, t, accu) | p :: ctx, decl :: sign -> @@ -4808,11 +4870,11 @@ 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 accu = if is_local_assum p then let open Context.Named.Declaration in - mkVar (get_id decl) :: accu - else accu + 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 in shrink ctx sign c t accu | _ -> assert false @@ -4834,28 +4896,30 @@ let shrink_entry sign const = } in (const, args) -let abstract_subproof id gk tac = +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - let open Context.Named.Declaration in - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in - let sigma = Sigma.to_evar_map sigma in let evdref = ref sigma in let sign,secsign = List.fold_right (fun d (s1,s2) -> - let id = get_id d in + let id = NamedDecl.get_id d in if mem_named_context_val id current_sign && - interpretable_as_section_decl evdref (lookup_named_val id current_sign) d + interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d 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 concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign 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 + let concl = it_mkNamedProd_or_LetIn concl sign in let concl = try flush_and_check_evars !evdref concl with Uninstantiated_evar _ -> @@ -4867,6 +4931,7 @@ let abstract_subproof id gk tac = let ctx = Evd.universe_context_set evd in evd, ctx, nf concl in + let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = @@ -4879,12 +4944,10 @@ let abstract_subproof id gk tac = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance sign)) - in - let cd = Entries.DefinitionEntry const in - let decl = (cd, IsProof Lemma) in + let const, args = shrink_entry sign const in + let args = List.map EConstr.of_constr args in + let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in let cst () = (** do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in @@ -4892,8 +4955,21 @@ let abstract_subproof id gk tac = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in let cst = Impargs.with_implicit_protection cst () in - (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in + let lem = + match const.Entries.const_entry_universes with + | Entries.Polymorphic_const_entry uctx -> + let uctx = Univ.ContextSet.of_context uctx in + (** Hack: the kernel may generate definitions whose universe variables are + not the same as requested in the entry because of constraints delayed + in the body, even in polymorphic mode. We mimick what it does for now + in hope it is fixed at some point. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in + let u = Univ.UContext.instance uctx in + mkConstU (cst, EInstance.make u) + | Entries.Monomorphic_const_entry _ -> + mkConst cst + in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in @@ -4901,31 +4977,39 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> - exact_no_check (applist (lem, args)) + tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Sigma.Unsafe.of_pair (tac, evd) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + end + +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) let anon_id = Id.of_string "anonymous" -let tclABSTRACT name_op tac = +let name_op_to_name name_op object_kind suffix = let open Proof_global in - let default_gk = (Global, false, Proof Theorem) in - let s, gk = match name_op with - | Some s -> - (try let _, gk, _ = current_proof_statement () in s, gk - with NoCurrentProof -> s, default_gk) - | None -> - let name, gk = - try let name, gk, _ = current_proof_statement () in name, gk - with NoCurrentProof -> anon_id, default_gk in - add_suffix name "_subproof", gk + let default_gk = (Global, false, object_kind) in + let name, gk = match Proof_global.V82.get_current_initial_conclusions () with + | (id, (_, gk)) -> Some id, gk + | exception NoCurrentProof -> None, default_gk in - abstract_subproof s gk tac + match name_op with + | Some s -> s, gk + | None -> + let name = Option.default anon_id name in + add_suffix name suffix, gk + +let tclABSTRACT ?(opaque=true) name_op tac = + let s, gk = if opaque + then name_op_to_name name_op (Proof Theorem) "_subproof" + else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in + abstract_subproof ~opaque s gk tac let unify ?(state=full_transparent_state) x y = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in try let core_flags = @@ -4938,12 +5022,11 @@ let unify ?(state=full_transparent_state) x y = merge_unify_flags = core_flags; subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } in - let sigma = Sigma.to_evar_map sigma in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in - Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma) + Proofview.Unsafe.tclEVARS sigma with e when CErrors.noncritical e -> - Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma - end } + Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) + end module Simple = struct (** Simplified version of some of the above tactics *) @@ -4951,40 +5034,30 @@ module Simple = struct let intro x = intro_move (Some x) MoveLast let apply c = - apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))] + apply_with_bindings_gen false false [None,(CAst.make (c,NoBindings))] let eapply c = - apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))] + apply_with_bindings_gen false true [None,(CAst.make (c,NoBindings))] let elim c = elim false None (c,NoBindings) None let case c = general_case_analysis false None (c,NoBindings) let apply_in id c = - apply_in false false id [None,(Loc.ghost, (c, NoBindings))] None + apply_in false false id [None,(CAst.make (c, NoBindings))] None end (** Tacticals defined directly in term of Proofview *) module New = struct - open Proofview.Notations - - let exact_proof c = exact_proof c - open Genredexpr open Locus let reduce_after_refine = - let onhyps = - (** We reduced everywhere in the hyps before 8.6 *) - if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0 - then None - else Some [] - in reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; rZeta=false;rDelta=false;rConst=[]}) - {onhyps; concl_occs=AllOccurrences } + {onhyps = Some []; concl_occs = AllOccurrences } - let refine ?unsafe c = - Refine.refine ?unsafe c <*> + let refine ~typecheck c = + Refine.refine ~typecheck c <*> reduce_after_refine end |