From efa3add0c03b70ecda3890cc6c69e66850605e7d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Jun 2014 19:06:03 +0200 Subject: Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) Every time you use abstract a kitten dies, please stop. --- kernel/declareops.ml | 2 +- stm/lemmas.ml | 10 ++++++ test-suite/bugs/closed/3344.v | 58 +++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/HoTT_coq_111.v | 24 +++++++++++++++ test-suite/bugs/opened/3344.v | 58 ----------------------------------- test-suite/bugs/opened/HoTT_coq_111.v | 27 ---------------- 6 files changed, 93 insertions(+), 86 deletions(-) create mode 100644 test-suite/bugs/closed/3344.v create mode 100644 test-suite/bugs/closed/HoTT_coq_111.v delete mode 100644 test-suite/bugs/opened/3344.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_111.v diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 149eeba287..51b7b6f971 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -284,7 +284,7 @@ type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = CList.uniquize l +let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) let union_side_effects l1 l2 = l1 @ l2 let flatten_side_effects l = List.flatten l let side_effects_of_list l = l diff --git a/stm/lemmas.ml b/stm/lemmas.ml index e5cfeecdff..c400008113 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -65,6 +65,16 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) + let add c cb e = + let exists c e = + try ignore(Environ.lookup_constant c e); true + with Not_found -> false in + if exists c e then e else Environ.add_constant c cb e in + let env = Declareops.fold_side_effects (fun env -> function + | SEsubproof (c, cb) -> add c cb env + | SEscheme (l,_) -> + List.fold_left (fun e (_,c,cb) -> add c cb e) env l) + env (Declareops.uniquize_side_effects eff) in let indexes = search_guard Loc.ghost env possible_indexes fixdecls in diff --git a/test-suite/bugs/closed/3344.v b/test-suite/bugs/closed/3344.v new file mode 100644 index 0000000000..8255fd6cce --- /dev/null +++ b/test-suite/bugs/closed/3344.v @@ -0,0 +1,58 @@ +(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *) +Require Import Coq.Sets.Ensembles. +Require Import Coq.Strings.String. +Global Set Implicit Arguments. +Global Set Asymmetric Patterns. +Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end. + +Inductive Comp : Type -> Type := +| Return : forall A, A -> Comp A +| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B. +Inductive computes_to : forall A, Comp A -> A -> Prop := +| ReturnComputes : forall A v, @computes_to A (Return v) v +| BindComputes : forall A B comp_a f comp_a_value comp_b_value, + @computes_to A comp_a comp_a_value + -> @computes_to B (f comp_a_value) comp_b_value + -> @computes_to B (Bind comp_a f) comp_b_value. + +Inductive is_computational : forall A, Comp A -> Prop := +| Return_is_computational : forall A (x : A), is_computational (Return x) +| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B), + is_computational cA + -> (forall a, + @computes_to _ cA a -> is_computational (f a)) + -> is_computational (Bind cA f). +Theorem is_computational_inv A (c : Comp A) +: is_computational c + -> match c with + | Return _ _ => True + | Bind _ _ x f => is_computational x + /\ forall v, computes_to x v + -> is_computational (f v) + end. + admit. +Defined. +Fixpoint is_computational_unique_val A (c : Comp A) {struct c} +: is_computational c -> { a | unique (computes_to c) a }. +Proof. + refine match c as c return is_computational c -> { a | unique (computes_to c) a } with + | Return T x => fun _ => exist (unique (computes_to (Return x))) + x + _ + | Bind _ _ x f + => fun H + => let H' := is_computational_inv H in + let xv := @is_computational_unique_val _ _ (proj1 H') in + let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in + exist (unique (computes_to _)) + (proj1_sig fxv) + _ + end; + clearbodies; + clear is_computational_unique_val; + clear; + first [ abstract admit + | abstract admit ]. +(* [Fail] does not catch the anomaly *) +Defined. +(* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/closed/HoTT_coq_111.v b/test-suite/bugs/closed/HoTT_coq_111.v new file mode 100644 index 0000000000..3b43f31df1 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_111.v @@ -0,0 +1,24 @@ + +Module X. + (*Set Universe Polymorphism.*) + Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. + Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. + + Axioms A B : Type. + Axiom P : A = B. + Definition foo : A = B. + abstract (rewrite <- P; reflexivity). + Defined. +End X. + +Module Y. + (*Set Universe Polymorphism.*) + Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. + Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. + + Axioms A B : Type. + Axiom P : A = B. + Definition foo : (A = B) * (A = B). + split; abstract (rewrite <- P; reflexivity). + Defined. +End Y. diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/opened/3344.v deleted file mode 100644 index 8255fd6cce..0000000000 --- a/test-suite/bugs/opened/3344.v +++ /dev/null @@ -1,58 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *) -Require Import Coq.Sets.Ensembles. -Require Import Coq.Strings.String. -Global Set Implicit Arguments. -Global Set Asymmetric Patterns. -Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end. - -Inductive Comp : Type -> Type := -| Return : forall A, A -> Comp A -| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B. -Inductive computes_to : forall A, Comp A -> A -> Prop := -| ReturnComputes : forall A v, @computes_to A (Return v) v -| BindComputes : forall A B comp_a f comp_a_value comp_b_value, - @computes_to A comp_a comp_a_value - -> @computes_to B (f comp_a_value) comp_b_value - -> @computes_to B (Bind comp_a f) comp_b_value. - -Inductive is_computational : forall A, Comp A -> Prop := -| Return_is_computational : forall A (x : A), is_computational (Return x) -| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B), - is_computational cA - -> (forall a, - @computes_to _ cA a -> is_computational (f a)) - -> is_computational (Bind cA f). -Theorem is_computational_inv A (c : Comp A) -: is_computational c - -> match c with - | Return _ _ => True - | Bind _ _ x f => is_computational x - /\ forall v, computes_to x v - -> is_computational (f v) - end. - admit. -Defined. -Fixpoint is_computational_unique_val A (c : Comp A) {struct c} -: is_computational c -> { a | unique (computes_to c) a }. -Proof. - refine match c as c return is_computational c -> { a | unique (computes_to c) a } with - | Return T x => fun _ => exist (unique (computes_to (Return x))) - x - _ - | Bind _ _ x f - => fun H - => let H' := is_computational_inv H in - let xv := @is_computational_unique_val _ _ (proj1 H') in - let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in - exist (unique (computes_to _)) - (proj1_sig fxv) - _ - end; - clearbodies; - clear is_computational_unique_val; - clear; - first [ abstract admit - | abstract admit ]. -(* [Fail] does not catch the anomaly *) -Defined. -(* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v deleted file mode 100644 index deb8e61235..0000000000 --- a/test-suite/bugs/opened/HoTT_coq_111.v +++ /dev/null @@ -1,27 +0,0 @@ -Module X. - Set Universe Polymorphism. - Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. - Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. - - Axioms A B : Type. - Axiom P : A = B. - Definition foo : A = B. - abstract (rewrite <- P; reflexivity). - (* Error: internal_paths_rew already exists. *) - Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) - Admitted. -End X. - -Module Y. - Set Universe Polymorphism. - Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. - Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope. - - Axioms A B : Type. - Axiom P : A = B. - Definition foo : (A = B) * (A = B). - split; abstract (rewrite <- P; reflexivity). - (* Error: internal_paths_rew already exists. *) - Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) - Admitted. -End Y. -- cgit v1.2.3