diff options
| -rw-r--r-- | kernel/term_typing.ml | 13 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 4 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 5 | ||||
| -rw-r--r-- | stm/stm.ml | 19 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3743.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4456.v | 647 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 4 | ||||
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 2 |
8 files changed, 683 insertions, 13 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a566028d4..aa60432a7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -424,11 +424,16 @@ 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 - ~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 diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 996428033..657a91c0c 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 diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 863bab7cc..e0315dec5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -123,8 +123,9 @@ module Make(T : Task) = struct "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> 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 diff --git a/stm/stm.ml b/stm/stm.ml index 96f127aa2..e08f69a0e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1470,6 +1470,18 @@ 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 @@ -1478,9 +1490,10 @@ end = struct (* {{{ *) 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 diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index 4dfb3380a..c799d4393 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/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v new file mode 100644 index 000000000..a32acf789 --- /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. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 15cb02d37..6248babd0 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 88fbd8c11..954d3df20 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<x. |