Imported Upstream version 8.6upstream/8.6

1 files changed, 709 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v
new file mode 100644
index 00000000..b13ca36a
--- /dev/null
+++ b/test-suite/bugs/closed/4187.v
@@ -0,0 +1,709 @@
+(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *)
+(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *)
+(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0
+   coqtop version 8.4pl5 (December 2014) *)
+Set Asymmetric Patterns.
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Import Coq.Lists.List.
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Global Set Implicit Arguments.
+Global Generalizable All Variables.
+Coercion is_true : bool >-> Sortclass.
+Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x 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.
+
+Module Export ADTSynthesis_DOT_Common_DOT_Wf.
+Module Export ADTSynthesis.
+Module Export Common.
+Module Export Wf.
+
+Section wf.
+  Section wf_prod.
+    Context A B (RA : relation A) (RB : relation B).
+Definition prod_relation : relation (A * B).
+exact (fun ab a'b' =>
+           RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))).
+Defined.
+
+    Fixpoint well_founded_prod_relation_helper
+             a b
+             (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A}
+    : Acc prod_relation (a, b)
+      := match wf_A with
+           | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b')
+                              := Acc_intro
+                                   _
+                                   (fun ab =>
+                                      match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with
+                                        | (a'', b'') =>
+                                          fun pf =>
+                                            match pf with
+                                              | or_introl pf'
+                                                => @well_founded_prod_relation_helper
+                                                     _ _
+                                                     (fa _ pf')
+                                                     wf_B
+                                              | or_intror (conj pfa pfb)
+                                                => match wf_B' with
+                                                     | Acc_intro fb
+                                                       => eq_rect
+                                                            _
+                                                            (fun a'' => Acc prod_relation (a'', b''))
+                                                            (wf_B_rec _ (fb _ pfb))
+                                                            _
+                                                            pfa
+                                                   end
+                                            end
+                                      end)
+                             ) b (wf_B b)
+         end.
+
+    Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation.
+    Proof.
+      intros wf_A wf_B [a b]; hnf in *.
+      apply well_founded_prod_relation_helper; auto.
+    Defined.
+  End wf_prod.
+
+  Section wf_projT1.
+    Context A (B : A -> Type) (R : relation A).
+Definition projT1_relation : relation (sigT B).
+exact (fun ab a'b' =>
+           R (projT1 ab) (projT1 a'b')).
+Defined.
+
+    Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation.
+    Proof.
+      intros wf [a b]; hnf in *.
+      induction (wf a) as [a H IH].
+      constructor.
+      intros y r.
+      specialize (IH _ r (projT2 y)).
+      destruct y.
+      exact IH.
+    Defined.
+  End wf_projT1.
+End wf.
+
+Section Fix3.
+  Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type)
+          (R : A -> A -> Prop) (Rwf : well_founded R)
+          (P : forall a b c, D a b c -> Type)
+          (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d).
+Definition Fix3 a b c d : @P a b c d.
+exact (@Fix { a : A & { b : B a & { c : C b & D c } } }
+            (fun x y => R (projT1 x) (projT1 y))
+            (well_founded_projT1_relation Rwf)
+            (fun abcd => P (projT2 (projT2 (projT2 abcd))))
+            (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _)
+            (existT _ a (existT _ b (existT _ c d)))).
+Defined.
+End Fix3.
+
+End Wf.
+
+End Common.
+
+End ADTSynthesis.
+
+End ADTSynthesis_DOT_Common_DOT_Wf.
+
+Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core.
+Module Export ADTSynthesis.
+Module Export Parsers.
+Module Export StringLike.
+Module Export Core.
+Import Coq.Setoids.Setoid.
+Import Coq.Classes.Morphisms.
+
+
+
+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;
+      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.
+
+  Definition str_le `{StringLike Char} (s1 s2 : String)
+    := length s1 < length s2 \/ s1 =s s2.
+  Infix "≤s" := str_le (at level 70, right associativity).
+
+  Class StringLikeProperties (Char : Type) `{StringLike Char} :=
+    {
+      singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = 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)
+    }.
+
+  Arguments StringLikeProperties Char {_}.
+End StringLike.
+
+End Core.
+
+End StringLike.
+
+End Parsers.
+
+End ADTSynthesis.
+
+End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core.
+
+Module Export ADTSynthesis.
+Module Export Parsers.
+Module Export ContextFreeGrammar.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Export ADTSynthesis.Parsers.StringLike.Core.
+Import ADTSynthesis.Common.
+
+Local Open Scope string_like_scope.
+
+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.
+
+  Section parse.
+    Context {HSL : StringLike Char}.
+    Variable G : grammar.
+
+    Inductive parse_of (str : String) : productions -> Type :=
+    | ParseHead : forall pat pats, parse_of_production str pat
+                                   -> parse_of str (pat::pats)
+    | ParseTail : forall pat pats, parse_of str pats
+                                   -> parse_of str (pat::pats)
+    with parse_of_production (str : String) : production -> Type :=
+    | ParseProductionNil : length str = 0 -> parse_of_production str nil
+    | ParseProductionCons : forall n pat pats,
+                              parse_of_item (take n str) pat
+                              -> parse_of_production (drop n str) pats
+                              -> parse_of_production str (pat::pats)
+    with parse_of_item (str : String) : item -> Type :=
+    | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch)
+    | ParseNonTerminal : forall nt, parse_of str (Lookup G nt)
+                                    -> parse_of_item str (NonTerminal nt).
+  End parse.
+End cfg.
+
+Arguments item _ : clear implicits.
+Arguments production _ : clear implicits.
+Arguments productions _ : clear implicits.
+Arguments grammar _ : clear implicits.
+
+End ContextFreeGrammar.
+
+Module Export BaseTypes.
+
+Section recursive_descent_parser.
+
+  Class parser_computational_predataT :=
+    { nonterminals_listT : Type;
+      initial_nonterminals_data : nonterminals_listT;
+      is_valid_nonterminal : nonterminals_listT -> String.string -> bool;
+      remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT;
+      nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop;
+      remove_nonterminal_dec : forall ls nonterminal,
+                                 is_valid_nonterminal ls nonterminal
+                                 -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls;
+      ntl_wf : well_founded nonterminals_listT_R }.
+
+  Class parser_removal_dataT' `{predata : parser_computational_predataT} :=
+    { 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' }.
+End recursive_descent_parser.
+
+End BaseTypes.
+Import Coq.Lists.List.
+Import ADTSynthesis.Parsers.ContextFreeGrammar.
+
+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' predata}.
+
+  Inductive minimal_parse_of
+  : forall (str0 : String) (valid : nonterminals_listT)
+           (str : String),
+      productions Char -> Type :=
+  | MinParseHead : forall str0 valid str pat pats,
+                     @minimal_parse_of_production str0 valid str pat
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  | MinParseTail : forall str0 valid str pat pats,
+                     @minimal_parse_of str0 valid str pats
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  with minimal_parse_of_production
+  : forall (str0 : String) (valid : nonterminals_listT)
+           (str : String),
+      production Char -> Type :=
+  | MinParseProductionNil : forall str0 valid str,
+                              length str = 0
+                              -> @minimal_parse_of_production str0 valid str nil
+  | MinParseProductionCons : forall str0 valid str n pat pats,
+                               str ≤s str0
+                               -> @minimal_parse_of_item str0 valid (take n str) pat
+                               -> @minimal_parse_of_production str0 valid (drop n str) pats
+                               -> @minimal_parse_of_production str0 valid str (pat::pats)
+  with minimal_parse_of_item
+  : forall (str0 : String) (valid : nonterminals_listT)
+           (str : String),
+      item Char -> Type :=
+  | MinParseTerminal : forall str0 valid str ch,
+                         str ~= [ ch ]
+                         -> @minimal_parse_of_item str0 valid str (Terminal ch)
+  | MinParseNonTerminal
+    : forall str0 valid str (nt : String.string),
+        @minimal_parse_of_nonterminal str0 valid str nt
+        -> @minimal_parse_of_item str0 valid str (NonTerminal nt)
+  with minimal_parse_of_nonterminal
+  : forall (str0 : String) (valid : nonterminals_listT)
+           (str : String),
+      String.string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall str0 valid (nt : String.string) str,
+        length str < length str0
+        -> is_valid_nonterminal initial_nonterminals_data nt
+        -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt)
+        -> @minimal_parse_of_nonterminal str0 valid str nt
+  | MinParseNonTerminalStrEq
+    : forall str0 str valid nonterminal,
+        str =s str0
+        -> is_valid_nonterminal initial_nonterminals_data nonterminal
+        -> is_valid_nonterminal valid nonterminal
+        -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal)
+        -> @minimal_parse_of_nonterminal str0 valid str nonterminal.
+End cfg.
+Import ADTSynthesis.Common.
+
+Section general.
+  Context {Char} {HSL : StringLike Char} {G : grammar Char}.
+
+  Class boolean_parser_dataT :=
+    { predata :> parser_computational_predataT;
+      split_string_for_production
+      : item Char -> production Char -> String -> list nat }.
+
+  Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT.
+
+  Definition split_list_completeT `{data : @parser_computational_predataT}
+             {str0 valid}
+             (it : item Char) (its : production Char)
+             (str : String)
+             (pf : str ≤s str0)
+             (split_list : list nat)
+
+    := ({ n : nat
+              & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it)
+                * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type)
+       -> ({ n : nat
+                 & (In n split_list)
+                   * (minimal_parse_of_item (G := G) str0 valid (take n str) it)
+                   * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type).
+
+  Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} :=
+    { split_string_for_production_complete
+      : forall str0 valid str (pf : str ≤s str0) nt,
+          is_valid_nonterminal initial_nonterminals_data nt
+          -> ForallT
+               (Forall_tails
+                  (fun prod
+                   => match prod return Type with
+                        | nil => True
+                        | it::its
+                          => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str)
+                      end))
+               (Lookup G nt) }.
+End general.
+
+Module Export BooleanRecognizer.
+Import Coq.Numbers.Natural.Peano.NPeano.
+Import Coq.Arith.Compare_dec.
+Import Coq.Arith.Wf_nat.
+
+Section recursive_descent_parser.
+  Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}.
+  Context {data : @boolean_parser_dataT Char _}.
+
+  Section bool.
+    Section parts.
+Definition parse_item
+                 (str_matches_nonterminal : String.string -> bool)
+                 (str : String)
+                 (it : item Char)
+      : bool.
+Admitted.
+
+      Section production.
+        Context {str0}
+                (parse_nonterminal
+                 : forall (str : String),
+                     str ≤s str0
+                     -> String.string
+                     -> bool).
+
+        Fixpoint parse_production
+                 (str : String)
+                 (pf : str ≤s str0)
+                 (prod : production Char)
+        : bool.
+        Proof.
+          refine
+            match prod with
+              | nil =>
+
+                Nat.eq_dec (length str) 0
+              | it::its
+                => let parse_production' := fun str pf => parse_production str pf its in
+                   fold_right
+                     orb
+                     false
+                     (map (fun n =>
+                             (parse_item
+                                (parse_nonterminal (str := take n str) _)
+                                (take n str)
+                                it)
+                               && parse_production' (drop n str) _)%bool
+                          (split_string_for_production it its str))
+            end;
+          revert pf; clear -HSLP; intros; admit.
+        Defined.
+      End production.
+
+      Section productions.
+        Context {str0}
+                (parse_nonterminal
+                 : forall (str : String)
+                          (pf : str ≤s str0),
+                     String.string -> bool).
+Definition parse_productions
+                   (str : String)
+                   (pf : str ≤s str0)
+                   (prods : productions Char)
+        : bool.
+exact (fold_right orb
+                        false
+                        (map (parse_production parse_nonterminal pf)
+                             prods)).
+Defined.
+      End productions.
+
+      Section nonterminals.
+        Section step.
+          Context {str0 valid}
+                  (parse_nonterminal
+                   : forall (p : String * nonterminals_listT),
+                       prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid)
+                       -> forall str : String,
+                            str ≤s fst p -> String.string -> bool).
+
+          Definition parse_nonterminal_step
+                     (str : String)
+                     (pf : str ≤s str0)
+                     (nt : String.string)
+          : bool.
+          Proof.
+            refine
+              (if lt_dec (length str) (length str0)
+               then
+                 parse_productions
+                   (@parse_nonterminal
+                      (str : String, initial_nonterminals_data)
+                      (or_introl _))
+                   (or_intror (reflexivity _))
+                   (Lookup G nt)
+               else
+                 if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt)
+                 then
+                   parse_productions
+                     (@parse_nonterminal
+                        (str0 : String, remove_nonterminal valid nt)
+                        (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _))))
+                     (str := str)
+                     _
+                     (Lookup G nt)
+                 else
+                   false);
+            assumption.
+          Defined.
+        End step.
+
+        Section wf.
+Definition parse_nonterminal_or_abort
+          : forall (p : String * nonterminals_listT)
+                   (str : String),
+              str ≤s fst p
+              -> String.string
+              -> bool.
+exact (Fix3
+                 _ _ _
+                 (well_founded_prod_relation
+                    (well_founded_ltof _ length)
+                    ntl_wf)
+                 _
+                 (fun sl => @parse_nonterminal_step (fst sl) (snd sl))).
+Defined.
+Definition parse_nonterminal
+                     (str : String)
+                     (nt : String.string)
+          : bool.
+exact (@parse_nonterminal_or_abort
+                 (str : String, initial_nonterminals_data) str
+                 (or_intror (reflexivity _)) nt).
+Defined.
+        End wf.
+      End nonterminals.
+    End parts.
+  End bool.
+End recursive_descent_parser.
+
+Section cfg.
+  Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char).
+
+  Section definitions.
+    Context (P : String -> String.string -> Type).
+
+    Definition Forall_parse_of_item'
+               (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type)
+               {str it} (p : parse_of_item G str it)
+      := match p return Type with
+           | ParseTerminal ch pf => unit
+           | ParseNonTerminal nt p'
+             => (P str nt * Forall_parse_of p')%type
+         end.
+
+    Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats)
+      := match p with
+           | ParseHead pat pats p'
+             => Forall_parse_of_production p'
+           | ParseTail _ _ p'
+             => Forall_parse_of p'
+         end
+    with Forall_parse_of_production {str pat} (p : parse_of_production G str pat)
+         := match p return Type with
+              | ParseProductionNil pf => unit
+              | ParseProductionCons pat strs pats p' p''
+                => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type
+            end.
+
+    Definition Forall_parse_of_item {str it} (p : parse_of_item G str it)
+      := @Forall_parse_of_item' (@Forall_parse_of) str it p.
+  End definitions.
+
+  End cfg.
+
+Section recursive_descent_parser_list.
+  Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}.
+Definition rdp_list_nonterminals_listT : Type.
+exact (list String.string).
+Defined.
+Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool.
+admit.
+Defined.
+Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT.
+admit.
+Defined.
+Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop.
+exact (ltof _ (@List.length _)).
+Defined.
+  Lemma rdp_list_remove_nonterminal_dec : forall ls prods,
+                                            @rdp_list_is_valid_nonterminal ls prods = true
+                                            -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls.
+admit.
+Defined.
+  Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R.
+  Proof.
+    unfold rdp_list_nonterminals_listT_R.
+    intro.
+    apply well_founded_ltof.
+  Defined.
+
+  Global Instance rdp_list_predata : parser_computational_predataT
+    := { nonterminals_listT := rdp_list_nonterminals_listT;
+         initial_nonterminals_data := Valid_nonterminals G;
+         is_valid_nonterminal := rdp_list_is_valid_nonterminal;
+         remove_nonterminal := rdp_list_remove_nonterminal;
+         nonterminals_listT_R := rdp_list_nonterminals_listT_R;
+         remove_nonterminal_dec := rdp_list_remove_nonterminal_dec;
+         ntl_wf := rdp_list_ntl_wf }.
+End recursive_descent_parser_list.
+
+Section sound.
+  Section general.
+    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' predata}.
+
+    Section parts.
+
+      Section nonterminals.
+        Section wf.
+
+          Lemma parse_nonterminal_sound
+                (str : String) (nonterminal : String.string)
+          : parse_nonterminal (G := G) str nonterminal
+            = true
+            -> parse_of_item G str (NonTerminal nonterminal).
+admit.
+Defined.
+        End wf.
+      End nonterminals.
+    End parts.
+  End general.
+End sound.
+
+Import Coq.Strings.String.
+Import ADTSynthesis.Parsers.ContextFreeGrammar.
+
+Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T
+  := match ls with
+       | nil => fun _ => default
+       | (str, t)::ls' => fun s => if string_dec str s
+                                   then t
+                                   else list_to_productions default ls' s
+     end.
+
+Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T
+  := {| Start_symbol := hd ""%string (map (@fst _ _) ls);
+        Lookup := list_to_productions default ls;
+        Valid_nonterminals := map (@fst _ _) ls |}.
+
+Section interface.
+  Context {Char} (G : grammar Char).
+Definition production_is_reachable (p : production Char) : Prop.
+admit.
+Defined.
+Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char)
+             (splits : list nat)
+  : Prop.
+exact (forall n,
+         n <= length str
+         -> parse_of_item G (take n str) it
+         -> parse_of_production G (drop n str) its
+         -> production_is_reachable (it::its)
+         -> List.In n splits).
+Defined.
+
+  Record Splitter :=
+    {
+      string_type :> StringLike Char;
+      splits_for : String -> item Char -> production Char -> list nat;
+
+      string_type_properties :> StringLikeProperties Char;
+      splits_for_complete : forall str it its,
+                              split_list_is_complete str it its (splits_for str it its)
+
+    }.
+  Global Existing Instance string_type_properties.
+
+  Record Parser (HSL : StringLike Char) :=
+    {
+      has_parse : @String Char HSL -> bool;
+
+      has_parse_sound : forall str,
+                          has_parse str = true
+                          -> parse_of_item G str (NonTerminal (Start_symbol G));
+
+      has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))),
+                             Forall_parse_of_item
+                               (fun _ nt => List.In nt (Valid_nonterminals G))
+                               p
+                             -> has_parse str = true
+    }.
+End interface.
+
+Module Export ParserImplementation.
+
+Section implementation.
+  Context {Char} {G : grammar Char}.
+  Context (splitter : Splitter G).
+
+  Local Instance parser_data : @boolean_parser_dataT Char _ :=
+    { predata := rdp_list_predata (G := G);
+      split_string_for_production it its str
+      := splits_for splitter str it its }.
+
+  Program Definition parser : Parser G splitter
+    := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G);
+          has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse;
+          has_parse_complete str p Hp := _ |}.
+  Next Obligation.
+admit.
+Defined.
+End implementation.
+
+End ParserImplementation.
+
+Section implementation.
+  Context {Char} {ls : list (String.string * productions Char)}.
+  Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing).
+  Context (splitter : Splitter G).
+
+  Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter.
+
+  Goal forall str : @String Char splitter,
+         let G' :=
+             @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in
+         G'.
+    intros str G'.
+    Timeout 1 assert (pf' : G' -> Prop) by abstract admit.