From a1d6232019dd903419b0ac10819dfde6759c45d1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Dec 2015 19:32:31 +0100 Subject: Fix bug #4456, anomaly in handle-side effects The side-effects can contain universe declarations needed to typecheck later proofs, which weren't added to the env used to typecheck them. --- kernel/term_typing.ml | 5 +- test-suite/bugs/closed/4456.v | 647 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 651 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4456.v diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a566028d40..74c2e7da37 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -424,7 +424,10 @@ let export_side_effects mb env ce = let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> - Environ.add_constant kn cb env + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + Environ.push_context ~strict:true cb.const_universes env + else env | kn, cb, `Opaque(_, ctx), _ -> let env = Environ.add_constant kn cb env in Environ.push_context_set diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v new file mode 100644 index 0000000000..a32acf789c --- /dev/null +++ b/test-suite/bugs/closed/4456.v @@ -0,0 +1,647 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) +(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 + coqtop version 8.5beta3 (November 2015) *) +(* Variable P : forall n m : nat, n = m -> Prop. *) +(* Axiom Prefl : forall n : nat, P n n eq_refl. *) +Axiom proof_admitted : False. + +Tactic Notation "admit" := case proof_admitted. + +Require Coq.Program.Program. +Require Coq.Strings.String. +Require Coq.omega.Omega. +Module Export Fiat_DOT_Common. +Module Export Fiat. +Module Common. +Import Coq.Lists.List. +Export Coq.Program.Program. + +Global Set Implicit Arguments. + +Global Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false. + +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +End Common. + +End Fiat. + +End Fiat_DOT_Common. +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Relations.Relation_Definitions. +Import Coq.Classes.Morphisms. + +Local Coercion is_true : bool >-> Sortclass. + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + get : nat -> String -> option Char; + unsafe_get : nat -> String -> Char; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ]; + get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch; + get_S : forall n s, get (S n) s = get n (drop 1 s); + unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str); + bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str' + }. +Global Arguments StringLikeProperties _ {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Core. +Import Coq.Strings.String. +Import Coq.Lists.List. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End Core. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_BaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export BaseTypes. +Import Coq.Arith.Wf_nat. + +Local Coercion is_true : bool >-> Sortclass. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + nonterminal_carrierT : Type; + of_nonterminal : String.string -> nonterminal_carrierT; + to_nonterminal : nonterminal_carrierT -> String.string; + initial_nonterminals_data : nonterminals_listT; + nonterminals_length : nonterminals_listT -> nat; + is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool; + remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop + := ltof _ nonterminals_length; + nonterminals_length_zero : forall ls, + nonterminals_length ls = 0 + -> forall nt, is_valid_nonterminal ls nt = false; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + remove_nonterminal_noninc : forall ls nonterminal, + ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal); + initial_nonterminals_correct : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G); + initial_nonterminals_correct' : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G); + to_of_nonterminal : forall nonterminal, + List.In nonterminal (Valid_nonterminals G) + -> to_nonterminal (of_nonterminal nonterminal) = nonterminal; + of_to_nonterminal : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal + -> of_nonterminal (to_nonterminal nonterminal) = nonterminal; + ntl_wf : well_founded nonterminals_listT_R + := well_founded_ltof _ _; + remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. + + Class split_dataT := + { split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_data :> split_dataT }. +End recursive_descent_parser. + +End BaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_BaseTypes. + +Module Export Fiat_DOT_Common_DOT_List_DOT_Operations. +Module Export Fiat. +Module Export Common. +Module Export List. +Module Export Operations. + +Import Coq.Lists.List. + +Module Export List. + Section InT. + Context {A : Type} (a : A). + + Fixpoint InT (ls : list A) : Set + := match ls return Set with + | nil => False + | b :: m => (b = a) + InT m + end%type. + End InT. + + End List. + +End Operations. + +End List. + +End Common. + +End Fiat. + +End Fiat_DOT_Common_DOT_List_DOT_Operations. + +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Properties. + +Section String. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}. + + Lemma take_length {str n} + : length (take n str) = min n (length str). +admit. +Defined. + + End String. + +End Properties. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Properties. + +Local Open Scope list_scope. +Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char) + := { nt : _ + & { prefix : _ + & List.In nt (Valid_nonterminals G) + * List.InT + (prefix ++ p) + (Lookup G nt) } }%type. + +End Properties. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_MinimalParse. +Module Export Fiat. +Module Export Parsers. +Module Export MinimalParse. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. + +Local Coercion is_true : bool >-> Sortclass. +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' _ G predata}. + + Inductive minimal_parse_of + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall len0 valid str pat pats, + @minimal_parse_of_production len0 valid str pat + -> @minimal_parse_of len0 valid str (pat::pats) + | MinParseTail : forall len0 valid str pat pats, + @minimal_parse_of len0 valid str pats + -> @minimal_parse_of len0 valid str (pat::pats) + with minimal_parse_of_production + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall len0 valid str, + length str = 0 + -> @minimal_parse_of_production len0 valid str nil + | MinParseProductionCons : forall len0 valid str n pat pats, + length str <= len0 + -> @minimal_parse_of_item len0 valid (take n str) pat + -> @minimal_parse_of_production len0 valid (drop n str) pats + -> @minimal_parse_of_production len0 valid str (pat::pats) + with minimal_parse_of_item + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall len0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item len0 valid str (Terminal ch) + | MinParseNonTerminal + : forall len0 valid str (nt : String.string), + @minimal_parse_of_nonterminal len0 valid str nt + -> @minimal_parse_of_item len0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall len0 valid (nt : String.string) str, + length str < len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal len0 valid str nt + | MinParseNonTerminalStrEq + : forall len0 str valid nonterminal, + length str = len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) + -> is_valid_nonterminal valid (of_nonterminal nonterminal) + -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal len0 valid str nonterminal. + +End cfg. + +End MinimalParse. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_MinimalParse. + +Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export CorrectnessBaseTypes. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. +Import Fiat_DOT_Common.Fiat.Common. +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Definition split_list_completeT_for {data : @parser_computational_predataT} + {len0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : length str <= len0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In (min (length str) n) (map (min (length str)) split_list)) + * (minimal_parse_of_item (G := G) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type). + + Definition split_list_completeT {data : @parser_computational_predataT} + (splits : item Char -> production Char -> String -> list nat) + := forall len0 valid str (pf : length str <= len0) nt, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT_for data len0 valid it its str pf (splits it its str) + end)) + (Lookup G nt). + + Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} := + { split_string_for_production_complete + : split_list_completeT split_string_for_production }. +End general. + +End CorrectnessBaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. + +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Valid. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Definition item_valid (it : item Char) + := match it with + | Terminal _ => True + | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt')) + end. + + Definition production_valid pat + := List.Forall item_valid pat. + + Definition productions_valid pats + := List.Forall production_valid pats. + + Definition grammar_valid + := forall nt, + List.In nt (Valid_nonterminals G) + -> productions_valid (Lookup G nt). +End cfg. + +End Valid. + +Section app. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Lemma hd_production_valid + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : item_valid it. +admit. +Defined. + + Lemma production_valid_cons + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : production_valid its. +admit. +Defined. + + End app. + +Import Coq.Lists.List. +Import Coq.omega.Omega. +Import Fiat_DOT_Common.Fiat.Common. +Import Fiat.Parsers.ContextFreeGrammar.Valid. +Local Open Scope string_like_scope. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' _ G _} + {gvalid : grammar_valid G}. + + Local Notation dec T := (T + (T -> False))%type (only parsing). + + Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing). + + Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B). +admit. +Defined. + + Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls + : dec { a : _ & (In a ls * P a) }. +admit. +Defined. + + Section item. + Context {len0 valid} + (str : String) + (str_matches_nonterminal' + : nonterminal_carrierT -> bool) + (str_matches_nonterminal + : forall nt : nonterminal_carrierT, + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Section valid. + Context (Hmatches + : forall nt, + is_valid_nonterminal initial_nonterminals_data nt + -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool) + (it : item Char) + (Hvalid : item_valid it). + + Definition parse_item' + : dec (minimal_parse_of_item (G := G) len0 valid str it). + Proof. + clear Hvalid. + refine (match it return dec (minimal_parse_of_item len0 valid str it) with + | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ]) + then inl (MinParseTerminal _ _ _ _ _) + else inr (fun _ => !) + | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt) + then inl (MinParseNonTerminal _) + else inr (fun _ => !) + end); + clear str_matches_nonterminal Hmatches; + admit. + Defined. + End valid. + + End item. + Context {len0 valid} + (parse_nonterminal + : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT), + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Lemma dec_in_helper {ls it its str} + : iffT {n0 : nat & + (In (min (length str) n0) (map (min (length str)) ls) * + minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + {n0 : nat & + (In n0 ls * + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}. +admit. +Defined. + + Lemma parse_production'_helper {str it its} (pf : length str <= len0) + : dec {n0 : nat & + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)). +admit. +Defined. + Local Ltac t_parse_production_for := repeat + match goal with + | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H + | _ => progress subst + | _ => solve [ constructor; assumption ] + | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H) + | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H) + | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' + | _ => progress simpl in * + | _ => discriminate + | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) + | _ => solve [ eauto with nocore ] + | _ => solve [ apply Min.min_case_strong; omega ] + | _ => omega + | [ H : production_valid (_::_) |- _ ] + => let H' := fresh in + pose proof H as H'; + apply production_valid_cons in H; + apply hd_production_valid in H' + end. + + Definition parse_production'_for + (splits : item Char -> production Char -> String -> list nat) + (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str)) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0) + (prod : production Char) + (Hreachable : production_is_reachableT G prod) + : dec (minimal_parse_of_production (G := G) len0 valid str prod). + Proof. + revert prod Hreachable str len Hlen pf. + refine + ((fun pf_helper => + list_rect + (fun prod => + forall (Hreachable : production_is_reachableT G prod) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0), + dec (minimal_parse_of_production (G := G) len0 valid str prod)) + ( + fun Hreachable str len Hlen pf + => match Utils.dec (beq_nat len 0) with + | left H => inl _ + | right H => inr (fun p => _) + end) + (fun it its parse_production' Hreachable str len Hlen pf + => parse_production'_helper + _ + (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in + let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in + let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in + match dec_In + (fun n => dec_prod (parse_item n) (parse_production n)) + (splits it its str) + with + | inl p => inl (existT _ (projT1 p) (snd (projT2 p))) + | inr p + => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in + let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in + inr (fun p' => p (fst dec_in_helper (H p'))) + end) + )) _); + [ clear parse_nonterminal Hsplits splits rdata cdata + | clear parse_nonterminal Hsplits splits rdata cdata + | .. + | admit ]. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + Defined. -- cgit v1.2.3 From 37cc37090fcbabb9546a79558c9420e532701be4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Dec 2015 20:07:06 +0100 Subject: Put implicits back as in 8.4. --- test-suite/bugs/closed/3743.v | 2 +- theories/Classes/RelationClasses.v | 4 ++++ theories/Structures/OrdersFacts.v | 2 +- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index 4dfb3380a8..c799d4393f 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -3,7 +3,7 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) Require Export Coq.Setoids.Setoid. -Fail Add Parametric Relation A +Add Parametric Relation A : A (@eq A) transitivity proved by transitivity as refine_rel. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 15cb02d37f..6248babd0e 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -208,6 +208,10 @@ Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. Arguments irreflexivity {A R Irreflexive} [x] _. +Arguments symmetry {A} {R} {_} [x] [y] _. +Arguments asymmetry {A} {R} {_} [x] [y] _ _. +Arguments transitivity {A} {R} {_} [x] [y] [z] _ _. +Arguments Antisymmetric A eqA {_} _. Hint Resolve irreflexivity : ord. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 88fbd8c11c..954d3df203 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). Instance le_order : PartialOrder eq le. Proof. compute; iorder. Qed. - Instance le_antisym : Antisymmetric eq le. + Instance le_antisym : Antisymmetric _ eq le. Proof. apply partial_order_antisym; auto with *. Qed. Lemma le_not_gt_iff : forall x y, x<=y <-> ~y set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - |"-load-vernac-source" |"-compile-verbose" + | ("-async-proofs" |"-toploop" |"-vi2vo" + |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" + |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> set_slave_opt tl | x::tl -> x :: set_slave_opt tl in -- cgit v1.2.3 From d2b468a87cc50b1558feffc6cd3e1b866205c684 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 16:00:11 +0100 Subject: par: check if the goal is not ground and fail (fix #4465) --- stm/stm.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 14142aa0c5..3d007004e2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1471,17 +1471,29 @@ end = struct (* {{{ *) try Reach.known_state ~cache:`No id; let t, uc = Future.purify (fun () -> + let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + let g = Evd.find sigma0 r_goal in + if not ( + Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && + List.for_all (fun (_,bo,ty) -> + Evarutil.is_ground_term sigma0 ty && + Option.cata (Evarutil.is_ground_term sigma0) true bo) + Evd.(evar_context g)) + then + Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ + "goals only")) + else begin vernac_interp r_state_fb r_ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") | Evd.Evar_defined t -> - let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then t, Evd.evar_universe_context sigma - else Errors.errorlabstrm "Stm" (str"The solution is not ground")) - () in - RespBuiltSubProof (t,uc) + else Errors.errorlabstrm "Stm" (str"The solution is not ground") + end) () + in + RespBuiltSubProof (t,uc) with e when Errors.noncritical e -> RespError (Errors.print e) let name_of_task { t_name } = t_name -- cgit v1.2.3 From bb9acba7cfe83ba3a5116b0e7aa78ac7f1219f60 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 4 Jan 2016 16:55:44 +0100 Subject: Fix handling of side-effects in case of `Opaque side-effects as well. --- kernel/term_typing.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 74c2e7da37..aa60432a7e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -429,9 +429,11 @@ let export_side_effects mb env ce = Environ.push_context ~strict:true cb.const_universes env else env | kn, cb, `Opaque(_, ctx), _ -> - let env = Environ.add_constant kn cb env in - Environ.push_context_set - ~strict:(not cb.const_polymorphic) ctx env in + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + let env = Environ.push_context ~strict:true cb.const_universes env in + Environ.push_context_set ~strict:true ctx env + else env in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce -- cgit v1.2.3 From 456e2be8af1d4a0cf2461d62dc5e1b4b24b2a552 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 4 Jan 2016 18:04:18 +0100 Subject: Extraction: msg_notice instead of msg_info. --- plugins/extraction/extract_env.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 9964280336..657a91c0c1 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -542,7 +542,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_info (str (Buffer.contents buf)); + Pp.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -636,7 +636,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_info ans + Pp.msg_notice ans | _ -> assert false -- cgit v1.2.3 From 08fdf3c7361c75037e12c5cd0e9f965165fed498 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 21:19:50 +0100 Subject: fixup d2b468a, evar normalization is needed --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/stm/stm.ml b/stm/stm.ml index 3d007004e2..168d8bf084 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1488,6 +1488,7 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") | Evd.Evar_defined t -> + let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then t, Evd.evar_universe_context sigma else Errors.errorlabstrm "Stm" (str"The solution is not ground") -- cgit v1.2.3 From e4a682e2f2c91fac47f55cd8619af2321b2e4c30 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 8 Dec 2015 12:49:01 +0100 Subject: COMMENTS: Predicate In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). --- lib/predicate.ml | 9 +++--- lib/predicate.mli | 85 +++++++++++++++++++++++++++++++++---------------------- 2 files changed, 56 insertions(+), 38 deletions(-) diff --git a/lib/predicate.ml b/lib/predicate.ml index a60b3dadd4..1aa7db6af1 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,8 +10,6 @@ (* *) (************************************************************************) -(* Sets over ordered types *) - module type OrderedType = sig type t @@ -43,9 +41,10 @@ module Make(Ord: OrderedType) = struct module EltSet = Set.Make(Ord) - (* when bool is false, the denoted set is the complement of - the given set *) type elt = Ord.t + + (* (false, s) represents a set which is equal to the set s + (true, s) represents a set which is equal to the complement of set s *) type t = bool * EltSet.t let elements (b,s) = (b, EltSet.elements s) @@ -84,6 +83,7 @@ module Make(Ord: OrderedType) = let diff s1 s2 = inter s1 (complement s2) + (* assumes the set is infinite *) let subset s1 s2 = match (s1,s2) with ((false,p1),(false,p2)) -> EltSet.subset p1 p2 @@ -91,6 +91,7 @@ module Make(Ord: OrderedType) = | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2) | ((true,_),(false,_)) -> false + (* assumes the set is infinite *) let equal (b1,s1) (b2,s2) = b1=b2 && EltSet.equal s1 s2 diff --git a/lib/predicate.mli b/lib/predicate.mli index bcc89e7275..cee3b0bd39 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,67 +1,84 @@ +(** Infinite sets over a chosen [OrderedType]. -(** Module [Pred]: sets over infinite ordered types with complement. *) - -(** This module implements the set data structure, given a total ordering - function over the set elements. All operations over sets - are purely applicative (no side-effects). - The implementation uses the Set library. *) + All operations over sets are purely applicative (no side-effects). + *) +(** Input signature of the functor [Make]. *) module type OrderedType = sig type t - val compare: t -> t -> int + (** The type of the elements in the set. + + The chosen [t] {b must be infinite}. *) + + val compare : t -> t -> int + (** A total ordering function over the set elements. + This is a two-argument function [f] such that: + - [f e1 e2] is zero if the elements [e1] and [e2] are equal, + - [f e1 e2] is strictly negative if [e1] is smaller than [e2], + - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + *) end - (** The input signature of the functor [Pred.Make]. - [t] is the type of the set elements. - [compare] is a total ordering function over the set elements. - This is a two-argument function [f] such that - [f e1 e2] is zero if the elements [e1] and [e2] are equal, - [f e1 e2] is strictly negative if [e1] is smaller than [e2], - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. - Example: a suitable ordering function is - the generic structural comparison function [compare]. *) module type S = sig type elt - (** The type of the set elements. *) + (** The type of the elements in the set. *) + type t - (** The type of sets. *) + (** The type of sets. *) + val empty: t - (** The empty set. *) + (** The empty set. *) + val full: t - (** The whole type. *) + (** The set of all elements (of type [elm]). *) + val is_empty: t -> bool - (** Test whether a set is empty or not. *) + (** Test whether a set is empty or not. *) + val is_full: t -> bool - (** Test whether a set contains the whole type or not. *) + (** Test whether a set contains the whole type or not. *) + val mem: elt -> t -> bool - (** [mem x s] tests whether [x] belongs to the set [s]. *) + (** [mem x s] tests whether [x] belongs to the set [s]. *) + val singleton: elt -> t - (** [singleton x] returns the one-element set containing only [x]. *) + (** [singleton x] returns the one-element set containing only [x]. *) + val add: elt -> t -> t - (** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) + (** [add x s] returns a set containing all elements of [s], + plus [x]. If [x] was already in [s], then [s] is returned unchanged. *) + val remove: elt -> t -> t (** [remove x s] returns a set containing all elements of [s], - except [x]. If [x] was not in [s], [s] is returned unchanged. *) + except [x]. If [x] was not in [s], then [s] is returned unchanged. *) + val union: t -> t -> t + (** Set union. *) + val inter: t -> t -> t + (** Set intersection. *) + val diff: t -> t -> t + (** Set difference. *) + val complement: t -> t - (** Union, intersection, difference and set complement. *) + (** Set complement. *) + val equal: t -> t -> bool - (** [equal s1 s2] tests whether the sets [s1] and [s2] are - equal, that is, contain equal elements. *) + (** [equal s1 s2] tests whether the sets [s1] and [s2] are + equal, that is, contain equal elements. *) + val subset: t -> t -> bool (** [subset s1 s2] tests whether the set [s1] is a subset of - the set [s2]. *) + the set [s2]. *) + val elements: t -> bool * elt list (** Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given *) end -module Make(Ord: OrderedType): (S with type elt = Ord.t) - (** Functor building an implementation of the set structure - given a totally ordered type. *) +(** The [Make] functor constructs an implementation for any [OrderedType]. *) +module Make (Ord : OrderedType) : (S with type elt = Ord.t) -- cgit v1.2.3