1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
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.
|
