Library compcert.cparser.validator.Interpreter
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).
| 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.
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.
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.
The top state of a stack
Definition state_of_stack (stack:stack): state :=
match stack with
| [] => init
| existT s _::_ => s
end.
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.
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.
| 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.
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.
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.
| 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.