aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-02 19:10:34 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-02 19:10:34 +0200
commitbb4810e7c7fc59c950cff7554cf77b076d25a0bd (patch)
tree6b65f072459bae9f6254d0adbfa8e9f54264dd26
parent467920d19aee31e523b147bb1fb4c491850db516 (diff)
Adding a test for bug #4057.
-rw-r--r--test-suite/bugs/closed/4057.v210
1 files changed, 210 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4057.v b/test-suite/bugs/closed/4057.v
new file mode 100644
index 000000000..4f0e696c9
--- /dev/null
+++ b/test-suite/bugs/closed/4057.v
@@ -0,0 +1,210 @@
+Require Coq.Strings.String.
+
+Set Implicit Arguments.
+
+Axiom falso : False.
+Ltac admit := destruct falso.
+
+Reserved Notation "[ x ]".
+
+Record string_like (CharType : Type) :=
+ {
+ String :> Type;
+ Singleton : CharType -> String where "[ x ]" := (Singleton x);
+ Empty : String;
+ Concat : String -> String -> String where "x ++ y" := (Concat x y);
+ bool_eq : String -> String -> bool;
+ bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+ Length : String -> nat
+ }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Infix "++" := (@Concat _ _) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+ := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Module Export ContextFreeGrammar.
+ Import Coq.Strings.String.
+ Import Coq.Lists.List.
+
+ Section cfg.
+ Variable CharType : Type.
+
+ Section definitions.
+
+ Inductive item :=
+ | NonTerminal (name : string).
+
+ Definition production := list item.
+ Definition productions := list production.
+
+ Record grammar :=
+ {
+ Start_symbol :> string;
+ Lookup :> string -> productions
+ }.
+ End definitions.
+
+ Section parse.
+ Variable String : string_like CharType.
+ Variable G : grammar.
+
+ Inductive parse_of : String -> productions -> Type :=
+ | ParseHead : forall str pat pats, parse_of_production str pat
+ -> parse_of str (pat::pats)
+ | ParseTail : forall str pat pats, parse_of str pats
+ -> parse_of str (pat::pats)
+ with parse_of_production : String -> production -> Type :=
+ | ParseProductionCons : forall str pat strs pats,
+ parse_of_item str pat
+ -> parse_of_production strs pats
+ -> parse_of_production (str ++ strs) (pat::pats)
+ with parse_of_item : String -> item -> Type :=
+ | ParseNonTerminal : forall name str, parse_of str (Lookup G name)
+ -> parse_of_item str (NonTerminal
+name).
+ End parse.
+ End cfg.
+
+End ContextFreeGrammar.
+Module Export ContextFreeGrammarProperties.
+
+ Section cfg.
+ Context CharType (String : string_like CharType) (G : grammar)
+ (P : String.string -> Type).
+
+ Fixpoint Forall_parse_of {str pats} (p : parse_of String G str pats)
+ := match p with
+ | @ParseHead _ _ _ str 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 String G
+str pat)
+ := let Forall_parse_of_item {str it} (p : parse_of_item String G str
+it)
+ := match p return Type with
+ | @ParseNonTerminal _ _ _ name str p'
+ => (P name * Forall_parse_of p')%type
+ end in
+ match p return Type with
+ | @ParseProductionCons _ _ _ str pat strs pats p' p''
+ => (Forall_parse_of_item p' * Forall_parse_of_production
+p'')%type
+ end.
+
+ Definition Forall_parse_of_item {str it} (p : parse_of_item String G str it)
+ := match p return Type with
+ | @ParseNonTerminal _ _ _ name str p'
+ => (P name * Forall_parse_of p')%type
+ end.
+ End cfg.
+
+End ContextFreeGrammarProperties.
+
+Module Export DependentlyTyped.
+ Import Coq.Strings.String.
+
+ Section recursive_descent_parser.
+
+ Class parser_computational_predataT :=
+ { nonterminal_names_listT : Type;
+ initial_nonterminal_names_data : nonterminal_names_listT;
+ is_valid_nonterminal_name : nonterminal_names_listT -> string -> bool;
+ remove_nonterminal_name : nonterminal_names_listT -> string ->
+nonterminal_names_listT }.
+
+ End recursive_descent_parser.
+
+End DependentlyTyped.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+
+Section cfg.
+ Context CharType (String : string_like CharType) (G : grammar).
+ Context (names_listT : Type)
+ (initial_names_data : names_listT)
+ (is_valid_name : names_listT -> string -> bool)
+ (remove_name : names_listT -> string -> names_listT).
+
+ Inductive minimal_parse_of
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ productions -> 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 : names_listT)
+ (str : String),
+ production -> Type :=
+ | MinParseProductionNil : forall str0 valid,
+ @minimal_parse_of_production str0 valid (Empty _)
+nil
+ | MinParseProductionCons : forall str0 valid str strs pat pats,
+ str ++ strs ≤s str0
+ -> @minimal_parse_of_item str0 valid str pat
+ -> @minimal_parse_of_production str0 valid strs
+pats
+ -> @minimal_parse_of_production str0 valid (str
+++ strs) (pat::pats)
+ with minimal_parse_of_item
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ item -> Type :=
+ | MinParseNonTerminal
+ : forall str0 valid str name,
+ @minimal_parse_of_name str0 valid str name
+ -> @minimal_parse_of_item str0 valid str (NonTerminal name)
+ with minimal_parse_of_name
+ : forall (str0 : String) (valid : names_listT)
+ (str : String),
+ string -> Type :=
+ | MinParseNonTerminalStrLt
+ : forall str0 valid name str,
+ @minimal_parse_of str initial_names_data str (Lookup G name)
+ -> @minimal_parse_of_name str0 valid str name
+ | MinParseNonTerminalStrEq
+ : forall str valid name,
+ @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+ -> @minimal_parse_of_name str valid str name.
+ Definition parse_of_item_name__of__minimal_parse_of_name
+ : forall {str0 valid str name} (p : @minimal_parse_of_name str0 valid str
+name),
+ parse_of_item String G str (NonTerminal name).
+ Proof.
+ admit.
+ Defined.
+
+End cfg.
+
+Section recursive_descent_parser.
+ Context (CharType : Type)
+ (String : string_like CharType)
+ (G : grammar).
+ Context {premethods : parser_computational_predataT}.
+ Let P : string -> Prop.
+ Proof.
+ admit.
+ Defined.
+
+ Let mp_parse_nonterminal_name str0 valid str nonterminal_name
+ := { p' : minimal_parse_of_name String G initial_nonterminal_names_data
+remove_nonterminal_name str0 valid str nonterminal_name & Forall_parse_of_item
+P (parse_of_item_name__of__minimal_parse_of_name p') }.
+
+ Goal False.
+ Proof.
+ clear -mp_parse_nonterminal_name.
+ subst P.
+ simpl in *.
+ admit.
+ Qed.