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
211
212
213
214
215
216
217
218
219
220
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
Require Import Streams.
Require Import List.
Require Import Syntax.
Require Automaton.
Require Import Alphabet.
Module Make(Import A:Automaton.T).
(** The error monad **)
Inductive result (A:Type) :=
| Err: result A
| OK: A -> result A.
Implicit Arguments Err [A].
Implicit Arguments OK [A].
Definition bind {A B: Type} (f: result A) (g: A -> result B): result B :=
match f with
| OK x => g x
| Err => Err
end.
Definition bind2 {A B C: Type} (f: result (A * B)) (g: A -> B -> result C):
result C :=
match f with
| OK (x, y) => g x y
| Err => Err
end.
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
(at level 200, X ident, Y ident, A at level 100, B at level 200).
(** Some operations on streams **)
(** Concatenation of a list and a stream **)
Fixpoint app_str {A:Type} (l:list A) (s:Stream A) :=
match l with
| nil => s
| cons t q => Cons t (app_str q s)
end.
Infix "++" := app_str (right associativity, at level 60).
Lemma app_str_app_assoc {A:Type} (l1 l2:list A) (s:Stream A) :
l1 ++ (l2 ++ s) = (l1 ++ l2) ++ s.
Proof.
induction l1.
reflexivity.
simpl.
rewrite IHl1.
reflexivity.
Qed.
(** The type of a non initial state: the type of semantic values associated
with the last symbol of this state. *)
Definition noninitstate_type state :=
symbol_semantic_type (last_symb_of_non_init_state state).
(** The stack of the automaton : it can be either nil or contains a non
initial state, a semantic value for the symbol associted with this state,
and a nested stack. **)
Definition stack := list (sigT noninitstate_type). (* eg. list {state & state_type state} *)
Section Init.
Variable init : initstate.
(** The top state of a stack **)
Definition state_of_stack (stack:stack): state :=
match stack with
| [] => init
| existT s _::_ => s
end.
(** [pop] pops some symbols from the stack. It returns the popped semantic
values using [sem_popped] as an accumulator and discards the popped
states.**)
Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack):
forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
result (stack * A) :=
match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with
| [] => fun A action => OK (stack_cur, action)
| t::q => fun A action =>
match stack_cur with
| existT state_cur sem::stack_rec =>
match compare_eqdec (last_symb_of_non_init_state state_cur) t with
| left e =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
pop q stack_rec (action sem_conv)
| right _ => Err
end
| [] => Err
end
end.
(** [step_result] represents the result of one step of the automaton : it can
fail, accept or progress. [Fail_sr] means that the input is incorrect.
[Accept_sr] means that this is the last step of the automaton, and it
returns the semantic value of the input word. [Progress_sr] means that
some progress has been made, but new steps are needed in order to accept
a word.
For [Accept_sr] and [Progress_sr], the result contains the new input buffer.
[Fail_sr] means that the input word is rejected by the automaton. It is
different to [Err] (from the error monad), which mean that the automaton is
bogus and has perfomed a forbidden action. **)
Inductive step_result :=
| Fail_sr: step_result
| Accept_sr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> step_result
| Progress_sr: stack -> Stream token -> step_result.
Program Definition prod_action':
forall p,
arrows_right (symbol_semantic_type (NT (prod_lhs p)))
(map symbol_semantic_type (prod_rhs_rev p)):=
fun p =>
eq_rect _ (fun x => x) (prod_action p) _ _.
Next Obligation.
unfold arrows_left, arrows_right; simpl.
rewrite <- fold_left_rev_right, <- map_rev, rev_involutive.
reflexivity.
Qed.
(** [reduce_step] does a reduce action :
- pops some elements from the stack
- execute the action of the production
- follows the goto for the produced non terminal symbol **)
Definition reduce_step stack_cur production buffer: result step_result :=
do (stack_new, sem) <-
pop (prod_rhs_rev production) stack_cur (prod_action' production);
match goto_table (state_of_stack stack_new) (prod_lhs production) return _ with
| Some (exist state_new e) =>
let sem := eq_rect _ _ sem _ e in
OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer)
| None =>
match stack_new return _ with
| [] =>
match compare_eqdec (prod_lhs production) (start_nt init) return _ with
| left e =>
let sem := eq_rect _ (fun nt => _ (_ nt)) sem _ e in
OK (Accept_sr sem buffer)
| right _ => Err
end
| _::_ => Err
end
end.
(** One step of parsing. **)
Definition step stack_cur buffer: result step_result :=
match action_table (state_of_stack stack_cur) with
| Default_reduce_act production =>
reduce_step stack_cur production buffer
| Lookahead_act awt =>
match Streams.hd buffer with
| existT term sem =>
match awt term with
| Shift_act state_new e =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
OK (Progress_sr (existT noninitstate_type state_new sem_conv::stack_cur)
(Streams.tl buffer))
| Reduce_act production =>
reduce_step stack_cur production buffer
| Fail_action =>
OK Fail_sr
end
end
end.
(** The parsing use a [nat] parameter [n_steps], so that we do not have to prove
terminaison, which is difficult. So the result of a parsing is either
a failure (the automaton has rejected the input word), either a timeout
(the automaton has spent all the given [n_steps]), either a parsed semantic
value with a rest of the input buffer.
**)
Inductive parse_result :=
| Fail_pr: parse_result
| Timeout_pr: parse_result
| Parsed_pr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> parse_result.
Fixpoint parse_fix stack_cur buffer n_steps: result parse_result:=
match n_steps with
| O => OK Timeout_pr
| S it =>
do r <- step stack_cur buffer;
match r with
| Fail_sr => OK Fail_pr
| Accept_sr t buffer_new => OK (Parsed_pr t buffer_new)
| Progress_sr s buffer_new => parse_fix s buffer_new it
end
end.
Definition parse buffer n_steps: result parse_result :=
parse_fix [] buffer n_steps.
End Init.
End Make.
Module Type T(A:Automaton.T).
Include (Make A).
End T.
|
