diff options
| -rw-r--r-- | plugins/extraction/common.ml | 7 | ||||
| -rw-r--r-- | plugins/extraction/common.mli | 1 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 18 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 22 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 14 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12763.v | 6 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_3.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_3.v | 4 | ||||
| -rw-r--r-- | test-suite/output/Error_msg_diffs.out | 2 | ||||
| -rw-r--r-- | test-suite/output/RecordMissingField.out | 20 | ||||
| -rw-r--r-- | test-suite/output/RecordMissingField.v | 8 | ||||
| -rw-r--r-- | test-suite/output/ssr_error_multiple_intro_after_case.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ssr_error_multiple_intro_after_case.v | 3 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 417 | ||||
| -rw-r--r-- | vernac/declare.ml | 22 | ||||
| -rw-r--r-- | vernac/declare.mli | 3 |
19 files changed, 308 insertions, 251 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 4a41f4c890..d215a7673d 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -604,6 +604,13 @@ let pp_global k r = | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) +(* Main name printing function for declaring a reference *) + +let pp_global_name k r = + let ls = ref_renaming (k,r) in + assert (List.length ls > 1); + List.hd ls + (* The next function is used only in Ocaml extraction...*) let pp_module mp = diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0bd9efd255..a482cfc03d 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -55,6 +55,7 @@ val opened_libraries : unit -> ModPath.t list type kind = Term | Type | Cons | Mod val pp_global : kind -> GlobRef.t -> string +val pp_global_name : kind -> GlobRef.t -> string val pp_module : ModPath.t -> string val top_visible_mp : unit -> ModPath.t diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 088405da5d..6425c3111e 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -99,6 +99,8 @@ let str_global k r = let pp_global k r = str (str_global k r) +let pp_global_name k r = str (Common.pp_global k r) + let pp_modname mp = str (Common.pp_module mp) (* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *) @@ -451,7 +453,7 @@ let pp_val e typ = let pp_Dfix (rv,c,t) = let names = Array.map - (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + (fun r -> if is_inline_custom r then mt () else pp_global_name Term r) rv in let rec pp init i = if i >= Array.length rv then mt () @@ -504,7 +506,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (GlobRef.IndRef (kn,0)) in + let name = pp_global_name Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -513,7 +515,7 @@ let pp_singleton kn packet = let pp_record kn fields ip_equiv packet = let ind = GlobRef.IndRef (kn,0) in - let name = pp_global Type ind in + let name = pp_global_name Type ind in let fieldnames = pp_fields ind fields in let l = List.combine fieldnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in @@ -535,7 +537,7 @@ let pp_ind co kn ind = let nextkwd = fnl () ++ str "and " in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (GlobRef.IndRef (kn,i))) + pp_global_name Type (GlobRef.IndRef (kn,i))) ind.ind_packets in let cnames = @@ -575,7 +577,7 @@ let pp_decl = function | Dterm (r,_,_) when is_inline_custom r -> mt () | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> - let name = pp_global Type r in + let name = pp_global_name Type r in let l = rename_tvars keywords l in let ids, def = try @@ -592,7 +594,7 @@ let pp_decl = function if is_custom r then str (" = " ^ find_custom r) else pp_function (empty_env ()) a in - let name = pp_global Term r in + let name = pp_global_name Term r in pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ()) | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) @@ -603,10 +605,10 @@ let pp_spec = function | Sind (kn,i) -> pp_mind kn i | Sval (r,t) -> let def = pp_type false [] t in - let name = pp_global Term r in + let name = pp_global_name Term r in hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) | Stype (r,vl,ot) -> - let name = pp_global Type r in + let name = pp_global_name Type r in let l = rename_tvars keywords vl in let ids, def = try diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 3228c6afd4..2ca9a0e69d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -182,7 +182,7 @@ let catch_error_with_trace_loc loc use_finer call_trace f x = catching_error call_trace Exninfo.iraise e let catch_error_loc loc use_finer tac = - Proofview.tclOR tac (fun exn -> + Proofview.tclORELSE tac (fun exn -> let (e, info) = update_loc loc use_finer exn in Proofview.tclZERO ~info e) @@ -1084,7 +1084,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) -and eval_tactic ist tac : unit Proofview.tactic = match tac with +and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacAtom {loc;v=t} -> let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in @@ -1163,7 +1163,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) - | TacArg a -> interp_tactic ist (TacArg a) + | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v)) | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> @@ -1243,7 +1243,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false - (val_interp ~appl ist (Tacenv.interp_ltac r)) + (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r))) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1359,7 +1359,7 @@ and tactic_of_value ist vle = lfun = lfun; poly; extra = TacStore.set ist.extra f_trace []; } in - let tac = name_if_glob appl (eval_tactic ist t) in + let tac = name_if_glob appl (eval_tactic_ist ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) | VFun (appl,_,vmap,vars,_) -> let tactic_nm = @@ -1446,7 +1446,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = ; poly ; extra = TacStore.set ist.extra f_trace trace } in - let tac = eval_tactic ist t in + let tac = eval_tactic_ist ist t in let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) | _ -> Ftactic.return v @@ -1927,11 +1927,11 @@ let default_ist () = let eval_tactic t = Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *) Proofview.tclLIFT db_initialize <*> - interp_tactic (default_ist ()) t + eval_tactic_ist (default_ist ()) t let eval_tactic_ist ist t = Proofview.tclLIFT db_initialize <*> - interp_tactic ist t + eval_tactic_ist ist t (** FFI *) @@ -1977,7 +1977,7 @@ let interp_tac_gen lfun avoid_ids debug t = let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun; poly; extra } in let ltacvars = Id.Map.domain lfun in - interp_tactic ist + eval_tactic_ist ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end @@ -2094,7 +2094,7 @@ let () = register_interp0 wit_tactic interp let () = - let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in + let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in register_interp0 wit_ltac interp let () = @@ -2121,7 +2121,7 @@ let _ = let eval lfun poly env sigma ty tac = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in - let tac = interp_tactic ist tac in + let tac = eval_tactic_ist ist tac in (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d7996a722a..d859fe51ab 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc = let uct = Evd.evar_universe_context (fst oc) in let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*> - Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) + Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) (fun _ -> Proofview.tclZERO dependent_apply_error) end diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index da623703a2..38b26d06b9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr = Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0 in let cvtac' = - Proofview.tclOR cvtac begin function + Proofview.tclORELSE cvtac begin function | (PRtype_error e, _) -> let error = Option.cata (fun (env, sigma, te) -> Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb2e607012..70cea89ccb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1044,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = end end -let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) +let drop_intro_name (_ : Id.t) = Proofview.tclUNIT () + +let intro_gen n m f d = intro_then_gen n m f d drop_intro_name 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_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using id = intro_using_then id drop_intro_name 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 intro = intro_then drop_intro_name let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false @@ -1065,6 +1068,11 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_using_then_helper tac acc = function + | [] -> tac (List.rev acc) + | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) +let intros_using_then l tac = intros_using_then_helper tac [] l + let intros = Tacticals.New.tclREPEAT intro let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b397b15d0..00739306a7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,9 +65,11 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v new file mode 100644 index 0000000000..6cbcc0d3b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12763.v @@ -0,0 +1,6 @@ +Inductive bool_list := S (y : bool) (l : bool_list) | O. +Scheme Equality for bool_list. + +Set Mangle Names. +Scheme Equality for nat. +Scheme Equality for list. diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out new file mode 100644 index 0000000000..dbd3dbd1e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v new file mode 100644 index 0000000000..c624402a81 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.v @@ -0,0 +1,4 @@ +Ltac f := auto; intro. +Goal False. +f. +Abort. diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out index 3e337e892d..2645524a70 100644 --- a/test-suite/output/Error_msg_diffs.out +++ b/test-suite/output/Error_msg_diffs.out @@ -1,4 +1,4 @@ -File "stdin", line 32, characters 0-12: +File "stdin", line 32, characters 0-11: [37;41;1mError:[0m In environment T : [33;1mType[0m diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out index 7c80a6065f..28beee90b2 100644 --- a/test-suite/output/RecordMissingField.out +++ b/test-suite/output/RecordMissingField.out @@ -1,4 +1,16 @@ -File "stdin", line 8, characters 5-22: -Error: Cannot infer field y2p of record point2d in environment: -p : point2d - +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |}) +More precisely: +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |}) +More precisely: +- ?n: Cannot infer this placeholder of type "nat" in + environment: + p : point2d + n : nat +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v index 84f1748fa0..8ca721564b 100644 --- a/test-suite/output/RecordMissingField.v +++ b/test-suite/output/RecordMissingField.v @@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **) Record point2d := mkPoint { x2p: nat; y2p: nat }. - -Definition increment_x (p: point2d) : point2d := +Fail Definition increment_x (p: point2d) : point2d := {| x2p := x2p p + 1; |}. + +(* Here there is also an unresolved implicit, which should give an + understadable error as well *) +Fail Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + (fun n => _) 1; |}. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out new file mode 100644 index 0000000000..51fb208ae9 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-11: +Error: x already used + diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v new file mode 100644 index 0000000000..1f87966693 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -0,0 +1,3 @@ +Require Import ssreflect. +Goal forall p : nat * nat , True. +case => x x. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f47cdd8bf0..7a7e7d6e35 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -556,11 +556,17 @@ let list_id l = List.fold_left ( fun a decl -> let s' = Id.of_string (s'^"_lb")) ::a ) [] l + +let avoid_of_list_id list_id = + List.fold_left (fun avoid (s,seq,sbl,slb) -> + List.fold_left (fun avoid id -> Id.Set.add id avoid) + avoid [s;seq;sbl;slb]) + Id.Set.empty list_id + (* build the right eq_I A B.. N eq_A .. eq_N *) -let eqI ind l = - let list_id = list_id l in +let eqI ind list_id = let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) and e = match lookup_scheme beq_scheme_kind ind with @@ -568,7 +574,7 @@ let eqI ind l = | None -> user_err ~hdr:"AutoIndDecl.eqI" (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); - in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)) + in mkApp(e,eA) (**********************************************************************) (* Boolean->Leibniz *) @@ -576,12 +582,12 @@ let eqI ind l = open Namegen let compute_bl_goal ind lnamesparrec nparrec = - let eqI = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in + let eqI = eqI ind list_id in + let avoid = avoid_of_list_id list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let bl_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -607,88 +613,74 @@ let compute_bl_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in let u = Univ.Instance.empty in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( mkArrow - (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|])) + (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar x;mkVar y|]);tt ()|])) Sorts.Relevant - (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) + (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar x;mkVar y|])) ))) let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let avoid = ref [] in - let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ - ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh - in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshz = fresh_id (Id.of_string "Z") gl in - (* try with *) - Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; - intro_using freshn ; - induct_on (EConstr.mkVar freshn); - intro_using freshm; - destruct_on (EConstr.mkVar freshm); - intro_using freshz; - intros; - Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity my_discr_tac - ); - simpl_in_hyp (freshz,Locus.InHyp); -(* + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) + @ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) + in + intros_using_then first_intros begin fun fresh_first_intros -> + Tacticals.New.tclTHENLIST [ + intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn)); + intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm)); + intro_using_then (Id.of_string "Z") begin fun freshz -> + Tacticals.New.tclTHENLIST [ + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity my_discr_tac + ); + simpl_in_hyp (freshz,Locus.InHyp); + (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). -*) - Tacticals.New.tclREPEAT ( - Tacticals.New.tclTHENLIST [ - Simple.apply_in freshz (EConstr.of_constr (andb_prop())); - Proofview.Goal.enter begin fun gl -> - let fresht = fresh_id (Id.of_string "Z") gl in - destruct_on_as (EConstr.mkVar freshz) - (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht); - CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) - end - ]); -(* + *) + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [ + Simple.apply_in freshz (EConstr.of_constr (andb_prop())); + destruct_on_as (EConstr.mkVar freshz) + (IntroOrPattern [[CAst.make @@ IntroNaming (IntroFresh (Id.of_string "Z")); + CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) + ]); + (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto -*) - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let sigma = Tacmach.New.project gl in - match EConstr.kind sigma concl with - | App (c,ca) -> ( - match EConstr.kind sigma c with - | Ind (indeq, u) -> - if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") - then - Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind - (!avoid) - nparrec (ca.(2)) - (ca.(1))) - Auto.default_auto - else - Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") - ) - | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end + *) + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in + match EConstr.kind sigma concl with + | App (c,ca) -> ( + match EConstr.kind sigma c with + | Ind (indeq, u) -> + if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") + then + Tacticals.New.tclTHEN + (do_replace_bl bl_scheme_key ind + (List.rev fresh_first_intros) + nparrec (ca.(2)) + (ca.(1))) + Auto.default_auto + else + Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") + ) + | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + end - ] - end + ] + end + ] + end let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -729,11 +721,11 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = eq () and tt = tt () and bb = bb () in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in - let eqI = eqI ind lnamesparrec in + let avoid = avoid_of_list_id list_id in + let eqI = eqI ind list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -760,73 +752,62 @@ let compute_lb_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in let u = Univ.Instance.empty in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( mkArrow - (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|])) + (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar x;mkVar y|])) Sorts.Relevant - (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar x;mkVar y|]);tt|])) ))) let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let avoid = ref [] in - let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh - in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshz = fresh_id (Id.of_string "Z") gl in - (* try with *) - Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; - intro_using freshn ; - induct_on (EConstr.mkVar freshn); - intro_using freshm; - destruct_on (EConstr.mkVar freshm); - intro_using freshz; - intros; - Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity my_discr_tac - ); - my_inj_tac freshz; - intros; simpl_in_concl; - Auto.default_auto; - Tacticals.New.tclREPEAT ( - Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); - simplest_split ;Auto.default_auto ] - ); - Proofview.Goal.enter begin fun gls -> - let concl = Proofview.Goal.concl gls in - let sigma = Tacmach.New.project gl in - (* assume the goal to be eq (eq_type ...) = true *) - match EConstr.kind sigma concl with - | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with - | App(c',ca') -> - let n = Array.length ca' in - do_replace_lb mode lb_scheme_key - (!avoid) - nparrec - ca'.(n-2) ca'.(n-1) - | _ -> - Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - ) - | _ -> - Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end - ] - end + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) + @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + intros_using_then first_intros begin fun fresh_first_intros -> + Tacticals.New.tclTHENLIST [ + intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn)); + intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm)); + intro_using_then (Id.of_string "Z") begin fun freshz -> + Tacticals.New.tclTHENLIST [ + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity my_discr_tac + ); + my_inj_tac freshz; + intros; simpl_in_concl; + Auto.default_auto; + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); + simplest_split ;Auto.default_auto ] + ); + Proofview.Goal.enter begin fun gls -> + let concl = Proofview.Goal.concl gls in + let sigma = Tacmach.New.project gls in + (* assume the goal to be eq (eq_type ...) = true *) + match EConstr.kind sigma concl with + | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with + | App(c',ca') -> + let n = Array.length ca' in + do_replace_lb mode lb_scheme_key + (List.rev fresh_first_intros) + nparrec + ca'.(n-2) ca'.(n-1) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + ) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + end + ] + end + ] + end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -868,10 +849,10 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = eq () and tt = tt () and bb = bb () in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in + let avoid = avoid_of_list_id list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -912,12 +893,10 @@ let compute_dec_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in - let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in + let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar x;mkVar y|]) in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd ind (2*nparrec)) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) ( mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) @@ -925,83 +904,89 @@ let compute_dec_goal ind lnamesparrec nparrec = let compute_dec_tact ind lnamesparrec nparrec = let eq = eq () and tt = tt () - and ff = ff () and bb = bb () in + and ff = ff () and bb = bb () in let list_id = list_id lnamesparrec in find_scheme beq_scheme_kind ind >>= fun _ -> - let eqI = eqI ind lnamesparrec in - let avoid = ref [] in + let _non_fresh_eqI = eqI ind list_id in let eqtrue x = mkApp(eq,[|bb;x;tt|]) in let eqfalse x = mkApp(eq,[|bb;x;ff|]) in let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ - ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) + @ ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) + @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshH = fresh_id (Id.of_string "H") gl in - let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in - let arfresh = Array.of_list fresh_first_intros in - let xargs = Array.sub arfresh 0 (2*nparrec) in - find_scheme bl_scheme_kind ind >>= fun c -> - let blI = mkConst c in - find_scheme lb_scheme_kind ind >>= fun c -> - let lbI = mkConst c in - Tacticals.New.tclTHENLIST [ - intros_using fresh_first_intros; - intros_using [freshn;freshm]; - (*we do this so we don't have to prove the same goal twice *) - assert_by (Name freshH) (EConstr.of_constr ( - mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) - )) - (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); - + let fresh_id s gl = fresh_id_in_env (Id.Set.empty) s (Proofview.Goal.env gl) in + intros_using_then first_intros begin fun fresh_first_intros -> + let eqI = + let a = Array.of_list fresh_first_intros in + let n = List.length list_id in + assert (Int.equal (Array.length a) (4 * n)); + let fresh_list_id = + List.init n (fun i -> (Array.get a i, Array.get a (i+n), + Array.get a (i+2*n), Array.get a (i+3*n))) in + eqI ind fresh_list_id + in + intro_using_then (Id.of_string "x") begin fun freshn -> + intro_using_then (Id.of_string "y") begin fun freshm -> Proofview.Goal.enter begin fun gl -> - let freshH2 = fresh_id (Id.of_string "H") gl in - Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ - (* left *) - Tacticals.New.tclTHENLIST [ - simplest_left; - apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); - Auto.default_auto - ] - ; - - (*right *) - Proofview.Goal.enter begin fun gl -> - let freshH3 = fresh_id (Id.of_string "H") gl in - Tacticals.New.tclTHENLIST [ - simplest_right ; - unfold_constr (Coqlib.lib_ref "core.not.type"); - intro; - Equality.subst_all (); - assert_by (Name freshH3) - (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) - (Tacticals.New.tclTHENLIST [ - apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); - Auto.default_auto - ]); - Equality.general_rewrite_bindings_in true - Locus.AllOccurrences true false - (List.hd !avoid) - ((EConstr.mkVar (List.hd (List.tl !avoid))), - NoBindings - ) - true; - my_discr_tac + let freshH = fresh_id (Id.of_string "H") gl in + let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in + let arfresh = Array.of_list fresh_first_intros in + let xargs = Array.sub arfresh 0 (2*nparrec) in + find_scheme bl_scheme_kind ind >>= fun c -> + let blI = mkConst c in + find_scheme lb_scheme_kind ind >>= fun c -> + let lbI = mkConst c in + Tacticals.New.tclTHENLIST [ + (*we do this so we don't have to prove the same goal twice *) + assert_by (Name freshH) (EConstr.of_constr ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + )) + (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); + + Proofview.Goal.enter begin fun gl -> + let freshH2 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ + (* left *) + Tacticals.New.tclTHENLIST [ + simplest_left; + apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); + Auto.default_auto + ] + ; + + (*right *) + Proofview.Goal.enter begin fun gl -> + let freshH3 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENLIST [ + simplest_right ; + unfold_constr (Coqlib.lib_ref "core.not.type"); + intro; + Equality.subst_all (); + assert_by (Name freshH3) + (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) + (Tacticals.New.tclTHENLIST [ + apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); + Auto.default_auto + ]); + Equality.general_rewrite_bindings_in true + Locus.AllOccurrences true false + freshH3 + ((EConstr.mkVar freshH2), + NoBindings + ) + true; + my_discr_tac + ] + end + ] + end ] - end - ] + end end - ] - end + end + end let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in diff --git a/vernac/declare.ml b/vernac/declare.ml index eedbee852b..66537c2978 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -642,14 +642,32 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = dref (* Preparing proof entries *) +let error_unresolved_evars env sigma t evars = + let pr_unresolved_evar e = + hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++ str ": " ++ + Himsg.explain_pretype_error env sigma + (Pretype_errors.UnsolvableImplicit (e,None))) + in + CErrors.user_err (hov 0 begin + str "The following term contains unresolved implicit arguments:"++ fnl () ++ + str " " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ + str "More precisely: " ++ fnl () ++ + v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars)) + end) + +let check_evars_are_solved env sigma t = + let t = EConstr.of_constr t in + let evars = Evarutil.undefined_evars_of_term sigma t in + if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars let prepare_definition ~info ~opaque ~body ~typ sigma = let { Info.poly; udecl; inline; _ } = info in let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false sigma (fun nf -> nf body, Option.map nf typ) in + Option.iter (check_evars_are_solved env sigma) types; + check_evars_are_solved env sigma body; let univs = Evd.check_univ_decl ~poly sigma udecl in let entry = definition_entry ~opaque ~inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in diff --git a/vernac/declare.mli b/vernac/declare.mli index c5a8afbad5..3001d0d206 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -117,8 +117,7 @@ end normalized w.r.t. the passed [evar_map] [sigma]. Universes should be handled properly, including minimization and restriction. Note that [sigma] is checked for unresolved evars, thus you should be - careful not to submit open terms or evar maps with stale, - unresolved existentials *) + careful not to submit open terms *) val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t |