From 62fa31d219dcf2129c55b3c46b8cc25be60edcab Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 10:18:10 +0200 Subject: Program: remove debug tracing --- toplevel/obligations.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index a18552c5e..6f7a5f684 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -24,10 +24,6 @@ open Util let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) -let trace s = - if !Flags.debug then msg_debug s - else () - let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -871,8 +867,6 @@ let rec solve_obligation prg num tac = let auto n tac oblset = auto_solve_obligations n ~oblset tac in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in - let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in let _ = Pfedit.by (snd (get_default_tactic ())) in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac -- cgit v1.2.3 From 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 10:55:15 +0200 Subject: Univs/Program/Function: Fix bug #4725 - In Program, a check_evars_are_solved was introduced too early. Program does it's checking of evars by itself. - In Function, the universe environments were not threaded correctly. --- plugins/funind/recdef.ml | 10 +++++----- test-suite/bugs/closed/4725.v | 38 ++++++++++++++++++++++++++++++++++++++ toplevel/command.ml | 1 - 3 files changed, 43 insertions(+), 6 deletions(-) create mode 100644 test-suite/bugs/closed/4725.v diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 065d0fe53..bc8e721ed 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1510,13 +1510,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + (* Refresh the global universes, now including those of _F *) + let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in - let relation = - fst (*FIXME*)(interp_constr - env_with_pre_rec_args - (Evd.from_env env_with_pre_rec_args) - r) + let relation, evuctx = + interp_constr env_with_pre_rec_args evm r in + let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 000000000..fd5e0fb60 --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. diff --git a/toplevel/command.ml b/toplevel/command.ml index 8f7c38997..8eb2232ed 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -923,7 +923,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = -- cgit v1.2.3 From 1e389def84cc3eafc8aa5d1a1505f078a58234bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 May 2016 19:47:38 +0200 Subject: Univs/(e)auto: fix bug #4450 polymorphic exact hints The exact and e_exact tactics were not registering the universes and constraints of the hint correctly. Now using the same connect_hint_clenv as unify_resolve, they do. Also correct the implementation of prepare_hint to normalize the universes of the hint before abstracting its undefined universes. They are going to be refreshed at each application. This means that eauto using term can use multiple different instantiations of the universes of term if term introduces new universes. If we want just one instantiation then the term should be abbreviated in the goal first. --- tactics/auto.ml | 21 ++++++---------- tactics/auto.mli | 4 +-- tactics/eauto.ml4 | 18 ++++++++------ tactics/hints.ml | 6 +++-- test-suite/bugs/closed/4450.v | 58 +++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 81 insertions(+), 26 deletions(-) create mode 100644 test-suite/bugs/closed/4450.v diff --git a/tactics/auto.ml b/tactics/auto.ml index 647ff9714..45da04cf0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -97,7 +97,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c - + let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.nf_enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in @@ -112,19 +112,12 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - let (c, _, _) = c in - let ctx, c' = - if poly then - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let ctx = Evd.evar_universe_context evd' in - ctx, subst_univs_level_constr subst c - else - let ctx = Evd.evar_universe_context clenv.evd in - ctx, c - in - Proofview.Goal.enter begin fun gl -> - let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c') + Proofview.Goal.enter begin + fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (exact_check c) end (* Util *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 2e5647f87..0276e8258 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,8 +26,8 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - [ `NF ] Proofview.Goal.t -> clausenv * constr - + 'a Proofview.Goal.t -> clausenv * constr + (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 568b1d17c..cb206a7dd 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -117,7 +117,7 @@ open Unification (***************************************************************************) let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) - + let unify_e_resolve poly flags (c,clenv) = Proofview.Goal.nf_enter begin fun gl -> @@ -138,12 +138,14 @@ let hintmap_of hdc concl = (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact poly flags (c,clenv) = - let (c, _, _) = c in - let clenv', subst = - if poly then Clenv.refresh_undefined_univs clenv - else clenv, Univ.empty_level_subst - in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) - + Proofview.Goal.enter begin + fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (Proofview.V82.tactic (e_give_exact c)) + end + let rec e_trivial_fail_db db_list local_db goal = let tacl = registered_e_assumption :: @@ -174,7 +176,7 @@ and e_my_find_search db_list local_db hdc concl = let tac = function | Res_pf (term,cl) -> unify_resolve poly st (term,cl) | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl)) + | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl))) (e_trivial_fail_db db_list local_db)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 1da464e6f..a1beacd5e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1097,10 +1097,12 @@ exception Found of constr * types let prepare_hint check (poly,local) env init (sigma,c) = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in - (* We re-abstract over uninstantiated evars. + (* We re-abstract over uninstantiated evars and universes. It is actually a bit stupid to generalize over evars since the first thing make_resolves will do is to re-instantiate the products *) - let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in + let sigma, subst = Evd.nf_univ_variables sigma in + let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in + let c = drop_extra_implicit_args c in let vars = ref (collect_vars c) in let subst = ref [] in let rec find_next_evar c = match kind_of_term c with diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v new file mode 100644 index 000000000..ecebaba81 --- /dev/null +++ b/test-suite/bugs/closed/4450.v @@ -0,0 +1,58 @@ +Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop. + +Polymorphic Axiom unit@{u} : Type@{u}. +Polymorphic Axiom tt@{u} : inhabited unit@{u}. + +Polymorphic Hint Resolve tt : the_lemmas. +Set Printing All. +Set Printing Universes. +Goal inhabited unit. +Proof. + eauto with the_lemmas. +Qed. + +Universe u. +Axiom f : Type@{u} -> Prop. +Lemma fapp (X : Type) : f X -> False. +Admitted. +Polymorphic Axiom funi@{i} : f unit@{i}. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto using (fapp unit funi). (* The two fapp's have different universes *) +Qed. + +Hint Resolve (fapp unit funi) : mylems. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto with mylems. (* Forces the two fapps at the same level *) +Qed. + +Goal (forall U, f U) -> (f unit -> False) -> False /\ False. + eauto. (* Forces the two fapps at the same level *) +Qed. + +Polymorphic Definition MyType@{i} := Type@{i}. +Universes l m n. +Constraint l < m. +Polymorphic Axiom maketype@{i} : MyType@{i}. + +Goal MyType@{l}. +Proof. + Fail solve [ eauto using maketype@{m} ]. + eauto using maketype. + Undo. + eauto using maketype@{n}. +Qed. + +Axiom foo : forall (A : Type), list A. +Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A. + +Universe x y. +Goal list Type@{x}. +Proof. + eauto using (foo Type). (* Refreshes the term *) + Undo. + eauto using foo. Show Universes. + Undo. + eauto using foop. Show Proof. Show Universes. +Qed. \ No newline at end of file -- cgit v1.2.3 From 784d82dc1a709c4c262665a4cd4eb0b1bd1487a0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 18:36:58 +0200 Subject: Univs: fix for part #2 of bug #4816. Check that the polymorphic status of everything that is parameterized in nested sections is coherent. --- library/lib.ml | 2 +- test-suite/bugs/closed/4816.v | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4816.v diff --git a/library/lib.ml b/library/lib.ml index e4617cafb..f6b4a2458 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -417,7 +417,7 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - check_same_poly poly vars; + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 000000000..ef79b9869 --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,18 @@ +Section foo. +Polymorphic Universes A B. +Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +or even, a refinement of #4503: +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +Section foo. + Polymorphic Universes A. + Section bar. + Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + End bar. +End foo. \ No newline at end of file -- cgit v1.2.3 From 3bb0753d1589489b0e33f6a116a84c4fa72ed49f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 22:28:14 +0200 Subject: Fix test-suite file, only part 2 is fixed in 8.5 --- test-suite/bugs/closed/4816.v | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index ef79b9869..5ba0787ee 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -1,10 +1,3 @@ -Section foo. -Polymorphic Universes A B. -Constraint A <= B. -End foo. -(* gives an anomaly Universe undefined *) - -or even, a refinement of #4503: Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := @@ -13,6 +6,6 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := Section foo. Polymorphic Universes A. Section bar. - Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End foo. \ No newline at end of file -- cgit v1.2.3 From 2b19f0923a314a6df0a9cfed0f56cf2405e6591c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 14 Jun 2016 11:40:24 +0200 Subject: Admitted: fix #4818 return initial stmt and univs --- stm/lemmas.ml | 7 +++++-- test-suite/bugs/closed/4818.v | 24 ++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4818.v diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5b205e79e..1ab695a5f 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -476,9 +476,11 @@ let save_proof ?proof = function let ctx = Evd.evar_context_universe_context (fst universes) in Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> + let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) - let pproofs, universes = + let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = match Pfedit.get_used_variables(), pproofs with @@ -490,7 +492,8 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in let names = Pfedit.get_universe_binders () in - let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + let evd = Evd.from_ctx universes in + let binders, ctx = Evd.universe_context ?names evd in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v new file mode 100644 index 000000000..904abb228 --- /dev/null +++ b/test-suite/bugs/closed/4818.v @@ -0,0 +1,24 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) +(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 + coqtop version 8.5pl1 (June 2016) *) +Set Universe Polymorphism. + +Inductive GCov (I : Type) : Type := | Foo : I -> GCov I. + +Section Product. + +Variables S IS : Type. +Variable locS : IS -> True. + +Goal GCov (IS * S) -> GCov IS. +intros X0. induction X0; intros. +destruct i. +specialize (locS i). +clear -locS. +destruct locS. Show Universes. +Admitted. + +(* +Anomaly: Universe Product.5189 undefined. Please report. +*) -- cgit v1.2.3 From 5401deb474ca596ffbb23a12f4b70e6def1d0d65 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jun 2016 10:48:17 +0200 Subject: remote counter: avoid thread race on sockets (fix #4823) With par: the scenario is this one: coqide --- master ---- proof worker 1 (has no par: steps) ---- proof worker 2 (has a par: step) ---- tac worker 2.1 ---- tac worker 2.2 ---- tac worker 2.3 Actor 2 installs a remote counter for universe levels, that are requested to master. Multiple threads dealing with actors 2.x may need to get values from that counter at the same time. Long story short, in this complex scenario a mutex was missing and the control threads for 2.x were accessing the counter (hence reading/writing to the single socket connecting 2 with master at the same time, "corrupting" the data flow). A better solution would be to have a way to generate unique fresh universe levels locally to a worker. --- lib/remoteCounter.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 3f1982594..6cc48c874 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -20,7 +20,7 @@ let new_counter ~name a ~incr ~build = let data = ref (ref a) in counters := (name, Obj.repr data) :: !counters; let m = Mutex.create () in - let mk_thsafe_getter f () = + let mk_thsafe_local_getter f () = (* - slaves must use a remote counter getter, not this one! *) (* - in the main process there is a race condition between slave managers (that are threads) and the main thread, hence the mutex *) @@ -28,11 +28,13 @@ let new_counter ~name a ~incr ~build = Errors.anomaly(Pp.str"Slave processes must install remote counters"); Mutex.lock m; let x = f () in Mutex.unlock m; build x in - let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in + let mk_thsafe_remote_getter f () = + Mutex.lock m; let x = f () in Mutex.unlock m; x in + let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in let installer f = if not (Flags.async_proofs_is_worker ()) then Errors.anomaly(Pp.str"Only slave processes can install a remote counter"); - getter := f in + getter := mk_thsafe_remote_getter f in (fun () -> !getter ()), installer let backup () = !counters -- cgit v1.2.3 From c064fb933a16dc25b8172a1a2e758f538ee7285e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 18 Jun 2016 11:18:01 +0200 Subject: A hack to fix another regression with Ltac trace report in 8.5. E.g. Goal 0=0 -> true=true. intro H; rewrite H1. was highlighting H1 but Goal 0=0 -> true=true. intro H; rewrite H. was only highlighting the whole "intro H; rewrite H". --- toplevel/himsg.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 244174f65..13a6489b9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1307,12 +1307,17 @@ let extract_ltac_trace trace eloc = else (* We entered a primitive tactic, we don't display trace but report on the finest location *) + let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in let best_loc = - if not (Loc.is_ghost eloc) then eloc else - (* trace is with innermost call coming first *) - let rec aux = function - | (loc,_)::tail when not (Loc.is_ghost loc) -> loc - | _::tail -> aux tail - | [] -> Loc.ghost in - aux trace in + (* trace is with innermost call coming first *) + let rec aux best_loc = function + | (loc,_)::tail -> + if Loc.is_ghost best_loc || + not (Loc.is_ghost loc) && finer_loc loc best_loc + then + aux loc tail + else + aux best_loc tail + | [] -> best_loc in + aux eloc trace in None, best_loc -- cgit v1.2.3 From 0fa8b96c243e0915477866b094735ecaaaac6ef6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 20 Jun 2016 15:08:11 +0200 Subject: Reference Manual / Extraction: the original example command no longer works with recent Coq --- doc/refman/Extraction.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index a963662f6..ee156b652 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -448,7 +448,7 @@ let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) happens when there is a quantification over types inside the type of a constructor; for example: \begin{verbatim} -Inductive anything : Set := dummy : forall A:Set, A -> anything. +Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. -- cgit v1.2.3 From 7ae226092719b26f71b675d6ceb211801349bc00 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Jun 2016 10:25:15 +0200 Subject: Remove extraction-specific code from the checker. It seems like this code was copy-pasted from kernel/inductive.ml. It was already dubious enough in the kernel. It feels completely wrong in the checker. --- checker/inductive.ml | 48 ++---------------------------------------------- 1 file changed, 2 insertions(+), 46 deletions(-) diff --git a/checker/inductive.ml b/checker/inductive.ml index 79dba4fac..909ecccae 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -59,16 +59,6 @@ let inductive_instance mib = UContext.instance mib.mind_universes else Instance.empty -let inductive_context mib = - if mib.mind_polymorphic then - instantiate_univ_context mib.mind_universes - else UContext.empty - -let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - subst_instance_constraints u (UContext.constraints mib.mind_universes) - else Constraint.empty - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) @@ -190,8 +180,6 @@ let rec make_subst env = in make Univ.LMap.empty -exception SingletonInductiveBecomesProp of Id.t - let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let subst = make_subst env (ctx,ar.template_param_levels,args) in @@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let is_prop_sort = function - | Prop Null -> true - | _ -> false - -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> if not mib.mind_polymorphic then a.mind_user_arity @@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) - -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] - -let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty = type_of_inductive_gen env pind [||] in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) + mkArity (List.rev ctx,s) let type_of_inductive_knowing_parameters env mip args = type_of_inductive_gen env mip args @@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = let type_of_constructor cstru mspec = type_of_constructor_gen cstru mspec -let type_of_constructor_in_ctx cstr (mib,mip as mspec) = - let u = Univ.UContext.instance mib.mind_universes in - let c = type_of_constructor_gen (cstr, u) mspec in - (c, mib.mind_universes) - -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn u mib) specif -- cgit v1.2.3 From 4b4397e185cee54052819ad63bef3ecd56ba4512 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Jun 2016 10:30:04 +0200 Subject: Fix typo. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0ac8e3c4c..114c5149f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -36,7 +36,7 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty (* NB: In OCaml, [type_of] and [get_of] might raise - [SingletonInductiveBecomeProp]. this exception will be catched + [SingletonInductiveBecomeProp]. This exception will be caught in late wrappers around the exported functions of this file, in order to display the location of the issue. *) -- cgit v1.2.3 From 47098e8619f269ddaaf621936ae90b9dfa128871 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Jun 2016 00:16:33 +0200 Subject: Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies. Instead of relaunching the coqtop process and then open the warning window, we rather fire the warning and wait for the user to press the OK button before doing anything. --- ide/coq.ml | 7 ++++--- ide/coq.mli | 2 +- ide/coqOps.ml | 6 ++---- ide/coqOps.mli | 2 +- 4 files changed, 8 insertions(+), 9 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 7edae47ca..1dd60ef02 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -232,7 +232,7 @@ type coqtop = { (* non quoted command-line arguments of coqtop *) mutable sup_args : string list; (* called whenever coqtop dies *) - mutable reset_handler : reset_kind -> unit task; + mutable reset_handler : unit task; (* called whenever coqtop sends a feedback message *) mutable feedback_handler : Feedback.feedback -> unit; (* actual coqtop process and its status *) @@ -424,6 +424,7 @@ let mkready coqtop = fun () -> coqtop.status <- Ready; Void let rec respawn_coqtop ?(why=Unexpected) coqtop = + if why = Unexpected then warning "Coqtop died badly. Resetting."; clear_handle coqtop.handle; ignore_error (fun () -> coqtop.handle <- @@ -435,7 +436,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop = If not, there isn't much we can do ... *) assert (coqtop.handle.alive = true); coqtop.status <- New; - ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) + ignore (coqtop.reset_handler coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = bind_self_as (fun this -> { @@ -443,7 +444,7 @@ let spawn_coqtop sup_args = (fun () -> respawn_coqtop (this ())) (fun msg -> (this ()).feedback_handler msg); sup_args = sup_args; - reset_handler = (fun _ _ k -> k ()); + reset_handler = (fun _ k -> k ()); feedback_handler = (fun _ -> ()); status = New; }) diff --git a/ide/coq.mli b/ide/coq.mli index 7cef6a4d0..8a1fa3ed1 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -60,7 +60,7 @@ val is_computing : coqtop -> bool val spawn_coqtop : string list -> coqtop (** Create a coqtop process with some command-line arguments. *) -val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit +val set_reset_handler : coqtop -> unit task -> unit (** Register a handler called when a coqtop dies (badly or on purpose) *) val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit diff --git a/ide/coqOps.ml b/ide/coqOps.ml index f3ae317a3..80ce99a69 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -144,7 +144,7 @@ object method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task - method handle_reset_initial : Coq.reset_kind -> unit task + method handle_reset_initial : unit task method raw_coq_query : string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task @@ -842,10 +842,8 @@ object(self) in loop l - method handle_reset_initial why = + method handle_reset_initial = let action () = - if why = Coq.Unexpected then warning "Coqtop died badly. Resetting." - else (* clear the stack *) if Doc.focused document then Doc.unfocus document; while not (Doc.is_empty document) do diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 4a37a1fa5..332c18f2f 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -15,7 +15,7 @@ object method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task - method handle_reset_initial : Coq.reset_kind -> unit task + method handle_reset_initial : unit task method raw_coq_query : string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task -- cgit v1.2.3 From a7ea32fbf3829d1ce39ce9cc24b71791727090c5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 26 Jun 2016 23:29:55 +0200 Subject: More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause). When typing a "with clause fails, type classes are used to possibly help to insert coercions. If this heuristic fails, do not consider it anymore to be the best failure since it has made type classes choices which may be inconsistent with other constraints and on which no backtracking is possible anymore (see new example in test suite file 4782.v). This does not mean that using type classes at this point is good. It may find an instance which help to find a coercion, but which might still be a choice of instance and coercion which is incompatible with other constraints. I tend to think that a convenient way to go to deal with the absence of backtracking in inserting coercions would be to have special For the record, here is a some comments of what happens regarding f9695eb4b and 827663982. In the presence of an instance (x:=t) given in a "with" clause, with t:T, and x expected of type T', the situation is the following: Before f9695eb4b: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is postponed to w_merge, even though there is no way to get more information since T ant T' are closed. As a result, t may be ill-typed and the unification may try to unify ill-formed terms, leading to #4872. - If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it fails, e.g. because a wrong type class instance is found, it was postponed to w_merge as above, and the test for coercion is retried now interleaved with type classes. After f9695eb4b and 827663982e: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is an immediate failure. This fixes #4872. - However, If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it gives closed terms and fails, this is immediate failure without backtracking on type classes, resulting in the problem added here to file 4872.v. The current fix does not consider the result of the use of type classes while trying to insert a coercion to be the last word on it. So, it fails with an error which is not the error for conversion of closed terms (ConversionFailed), therefore in a way expected by f9695eb4b and 827663982e, and the "with" typing problem is then postponed again. --- pretyping/coercion.ml | 2 +- test-suite/bugs/closed/4782.v | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d00445958..71c55ae05 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -510,7 +510,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = error_actual_type_loc loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercionNoUnifier (_evd,_error) -> error_actual_type_loc loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index ed4443786..dbd71035d 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +(* A simplification of an example from coquelicot, which was failing + at some time after a fix #4782 was committed. *) + +Record T := { dom : Type }. +Definition pairT A B := {| dom := (dom A * dom B)%type |}. +Class C (A:Type). +Parameter B:T. +Instance c (A:T) : C (dom A). +Instance cn : C (dom B). +Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. +Set Typeclasses Debug. +Goal forall (A:T) (x:dom A), pairT A A = pairT A A. +intros. +apply (F _ _) with (x,x). + -- cgit v1.2.3