aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/term_typing.ml13
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--stm/asyncTaskQueue.ml5
-rw-r--r--stm/stm.ml19
-rw-r--r--test-suite/bugs/closed/3743.v2
-rw-r--r--test-suite/bugs/closed/4456.v647
-rw-r--r--theories/Classes/RelationClasses.v4
-rw-r--r--theories/Structures/OrdersFacts.v2
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.