Commit 8e7ec381 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Coq backend: the fuel parameter is now given as the logarithm of the maximal number of steps.

parent 76292c83
Pipeline #69754 passed with stages
in 33 seconds
...@@ -26,6 +26,11 @@ ...@@ -26,6 +26,11 @@
MenhirLib matches. This check can be disabled with MenhirLib matches. This check can be disabled with
--coq-no-version-check. --coq-no-version-check.
* Coq backend: The fuel parameter is now given as the *logarithm* of
the maximum number of steps to perform. Therefore, using e.g., 50
makes sure we will not run out of fuel in any reasonnable
computation time.
## 2018/11/13 ## 2018/11/13
* In `.mly` files, a new syntax for rules has been introduced, which is * In `.mly` files, a new syntax for rules has been introduced, which is
......
...@@ -283,7 +283,7 @@ Inductive step_result := ...@@ -283,7 +283,7 @@ Inductive step_result :=
- follows the goto for the produced non terminal symbol **) - follows the goto for the produced non terminal symbol **)
Definition reduce_step stk prod (buffer : buffer) Definition reduce_step stk prod (buffer : buffer)
(Hval : thunkP (valid_for_reduce (state_of_stack stk) prod)) (Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
(Hi : stack_invariant stk) (Hi : thunkP (stack_invariant stk))
: step_result. : step_result.
refine refine
((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod) ((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod)
...@@ -302,7 +302,7 @@ refine ...@@ -302,7 +302,7 @@ refine
(fun _ => pop_state_valid _ _ _ _ _ _ _)). (fun _ => pop_state_valid _ _ _ _ _ _ _)).
Proof. Proof.
- clear -Hi Hval. - clear -Hi Hval.
abstract (intros _; destruct Hi; eapply prefix_ass; [by apply Hval|eassumption]). abstract (intros _; destruct Hi=>//; eapply prefix_ass; [by apply Hval|eassumption]).
- clear -Hval. - clear -Hval.
abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//). abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//).
- clear -Hi. abstract by destruct Hi. - clear -Hi. abstract by destruct Hi.
...@@ -315,7 +315,7 @@ Proof. ...@@ -315,7 +315,7 @@ Proof.
unfold reduce_step. unfold reduce_step.
match goal with match goal with
| |- context [pop ?symbols_to_pop stk ?Hp ?action] => | |- context [pop ?symbols_to_pop stk ?Hp ?action] =>
assert (Hi':=pop_preserves_invariant symbols_to_pop stk Hp _ action Hi); assert (Hi':=pop_preserves_invariant symbols_to_pop stk Hp _ action (Hi I));
generalize (pop_state_valid symbols_to_pop stk Hp _ action) generalize (pop_state_valid symbols_to_pop stk Hp _ action)
end. end.
destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'. destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'.
...@@ -332,7 +332,7 @@ Proof. ...@@ -332,7 +332,7 @@ Proof.
Qed. Qed.
(** One step of parsing. **) (** One step of parsing. **)
Definition step stk buffer (Hi : stack_invariant stk): step_result := Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result :=
match action_table (state_of_stack stk) as a return match action_table (state_of_stack stk) as a return
thunkP thunkP
match a return Prop with match a return Prop with
...@@ -383,43 +383,52 @@ Proof. ...@@ -383,43 +383,52 @@ Proof.
* unfold state_stack_of_stack; simpl; constructor. * unfold state_stack_of_stack; simpl; constructor.
-- intros ?. by destruct singleton_state_pred. -- intros ?. by destruct singleton_state_pred.
-- eapply prefix_pred_ass. apply Hshift2. by destruct Hi. -- eapply prefix_pred_ass. apply Hshift2. by destruct Hi.
* by constructor. * constructor; by apply Hi.
+ eauto using reduce_step_stack_invariant_preserved. + eauto using reduce_step_stack_invariant_preserved.
Qed. Qed.
(** The parsing use a [nat] parameter [n_steps], so that we do not have to prove (** The parsing use a [nat] fuel parameter [log_n_steps], so that we
terminaison, which is difficult. So the result of a parsing is either do not have to prove terminaison, which is difficult.
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 Note that [log_n_steps] is *not* the fuel in the conventionnal
value with a rest of the input buffer. sense: this parameter contains the logarithm (in base 2) of the
number of steps to perform. Hence, a value of, e.g., 50 will
usually be enough to ensure termination. *)
Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant stk)):
{ sr : step_result |
forall stk' buffer', sr = Progress_sr stk' buffer' -> stack_invariant stk' } :=
match log_n_steps with
| O => exist _ (step stk buffer Hi)
(step_stack_invariant_preserved _ _ Hi)
| S log_n_steps =>
match parse_fix stk buffer log_n_steps Hi with
| exist _ (Progress_sr stk buffer) Hi' =>
parse_fix stk buffer log_n_steps (fun _ => Hi' _ buffer eq_refl)
| sr => sr
end
end.
(** The final 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 [2^log_n_steps]), either a parsed semantic value
with a rest of the input buffer.
Note that we do not make parse_result depend on start_nt for the result Note that we do not make parse_result depend on start_nt for the
type, so that this inductive is extracted without the use of Obj.t in OCaml. result type, so that this inductive is extracted without the use
**) of Obj.t in OCaml. **)
Inductive parse_result {A : Type} := Inductive parse_result {A : Type} :=
| Fail_pr: parse_result | Fail_pr: parse_result
| Timeout_pr: parse_result | Timeout_pr: parse_result
| Parsed_pr: A -> buffer -> parse_result. | Parsed_pr: A -> buffer -> parse_result.
Global Arguments parse_result _ : clear implicits. Global Arguments parse_result _ : clear implicits.
Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk): Definition parse (buffer : buffer) (log_n_steps : nat):
parse_result (symbol_semantic_type (NT (start_nt init))) :=
match n_steps return _ with
| O => Timeout_pr
| S it =>
match step stk buffer Hi as r
return (forall stk' buffer', r = _ -> _) -> _
with
| Fail_sr => fun _ => Fail_pr
| Accept_sr t buffer_new => fun _ => Parsed_pr t buffer_new
| Progress_sr s buffer_new => fun Hi =>
parse_fix s buffer_new it (Hi s _ eq_refl)
end (step_stack_invariant_preserved _ _ _)
end.
Definition parse (buffer : buffer) (n_steps : nat):
parse_result (symbol_semantic_type (NT (start_nt init))). parse_result (symbol_semantic_type (NT (start_nt init))).
refine (parse_fix [] buffer n_steps _). refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with
| Fail_sr => Fail_pr
| Accept_sr sem buffer' => Parsed_pr sem buffer'
| Progress_sr _ _ => Timeout_pr
end).
Proof. Proof.
abstract (repeat constructor; intros; by destruct singleton_state_pred). abstract (repeat constructor; intros; by destruct singleton_state_pred).
Defined. Defined.
......
...@@ -426,6 +426,16 @@ Definition next_ptd (ptd:pt_dot) : option pt_dot := ...@@ -426,6 +426,16 @@ Definition next_ptd (ptd:pt_dot) : option pt_dot :=
end (Non_terminal_pt _ ptl) end (Non_terminal_pt _ ptl)
end. end.
Fixpoint next_ptd_iter (ptd:pt_dot) (log_n_steps:nat) : option pt_dot :=
match log_n_steps with
| O => next_ptd ptd
| S log_n_steps =>
match next_ptd_iter ptd log_n_steps with
| None => None
| Some ptd => next_ptd_iter ptd log_n_steps
end
end.
(** We prove that these functions behave well w.r.t. semantic values. *) (** We prove that these functions behave well w.r.t. semantic values. *)
Lemma sem_build_from_pt {symb word} Lemma sem_build_from_pt {symb word}
(pt : parse_tree symb word) (ptz : pt_zipper symb word) : (pt : parse_tree symb word) (ptz : pt_zipper symb word) :
...@@ -472,6 +482,18 @@ Proof. ...@@ -472,6 +482,18 @@ Proof.
- by rewrite -sem_build_from_ptl. - by rewrite -sem_build_from_ptl.
Qed. Qed.
Lemma sem_next_ptd_iter (ptd : pt_dot) (log_n_steps : nat) :
match next_ptd_iter ptd log_n_steps with
| None => True
| Some ptd' => ptd_sem ptd = ptd_sem ptd'
end.
Proof.
revert ptd.
induction log_n_steps as [|log_n_steps IH]; [by apply sem_next_ptd|]=>/= ptd.
assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|]=>//.
specialize (IH ptd'). destruct next_ptd_iter=>//. congruence.
Qed.
(** We prove that these functions behave well w.r.t. xxx_buffer. *) (** We prove that these functions behave well w.r.t. xxx_buffer. *)
Lemma ptd_buffer_build_from_pt {symb word} Lemma ptd_buffer_build_from_pt {symb word}
(pt : parse_tree symb word) (ptz : pt_zipper symb word) : (pt : parse_tree symb word) (ptz : pt_zipper symb word) :
...@@ -657,6 +679,30 @@ Proof. ...@@ -657,6 +679,30 @@ Proof.
+ apply (ptd_stack_compat_build_from_ptl _ _ _ stk0); simpl; eauto. + apply (ptd_stack_compat_build_from_ptl _ _ _ stk0); simpl; eauto.
Qed. Qed.
(** We prove the completeness of the parser main loop. *)
Lemma parse_fix_next_ptd_iter (ptd : pt_dot) (stk : stack) (log_n_steps : nat) Hi :
ptd_stack_compat ptd stk ->
match next_ptd_iter ptd log_n_steps with
| None =>
proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) =
Accept_sr (ptd_sem ptd) buffer_end
| Some ptd' =>
exists stk',
proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) =
Progress_sr stk' (ptd_buffer ptd') /\
ptd_stack_compat ptd' stk'
end.
Proof.
revert ptd stk Hi.
induction log_n_steps as [|log_n_steps IH]; [by apply step_next_ptd|].
move => /= ptd stk Hi Hstk. assert (IH1 := IH ptd stk Hi Hstk).
assert (EQsem := sem_next_ptd_iter ptd log_n_steps).
destruct parse_fix as [sr Hi']. simpl in IH1.
destruct next_ptd_iter as [ptd'|].
- rewrite EQsem. destruct IH1 as (stk' & -> & Hstk'). by apply IH.
- by subst.
Qed.
(** The parser is defined by recursion over a fuel parameter. In the (** The parser is defined by recursion over a fuel parameter. In the
completeness proof, we need to predict how much fuel is going to be completeness proof, we need to predict how much fuel is going to be
needed in order to prove that enough fuel gives rise to a successful needed in order to prove that enough fuel gives rise to a successful
...@@ -725,30 +771,19 @@ Proof. ...@@ -725,30 +771,19 @@ Proof.
- by rewrite -ptd_cost_build_from_ptl. - by rewrite -ptd_cost_build_from_ptl.
Qed. Qed.
(** We prove the completeness of the parser main loop. *) Lemma next_ptd_iter_cost ptd log_n_steps :
Lemma parse_fix_complete: match next_ptd_iter ptd log_n_steps with
forall (ptd : pt_dot) (stk : stack) (n_steps : nat) Hi, | None => ptd_cost ptd < 2^log_n_steps
ptd_stack_compat ptd stk -> | Some ptd' => ptd_cost ptd = 2^log_n_steps + ptd_cost ptd'
match parse_fix safe init stk (ptd_buffer ptd) n_steps Hi with end.
| Timeout_pr => n_steps < S (ptd_cost ptd)
| Parsed_pr sem buff =>
sem = ptd_sem ptd /\ buff = buffer_end /\ S (ptd_cost ptd) <= n_steps
| Fail_pr => False
end.
Proof. Proof.
intros ptd stk n_steps. revert ptd stk. revert ptd. induction log_n_steps as [|log_n_steps IH]=>ptd /=.
induction n_steps as [|n_steps IH]=>/= ptd stk Hi Hstk. - assert (Hptd := next_ptd_cost ptd). destruct next_ptd=>//. by rewrite Hptd.
- apply Nat.lt_0_succ. - rewrite Nat.add_0_r. assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|].
- generalize (step_stack_invariant_preserved safe init stk (ptd_buffer ptd) Hi). + specialize (IH ptd'). destruct next_ptd_iter as [ptd''|].
assert (Hstep := step_next_ptd ptd stk Hi Hstk). * by rewrite IH1 IH -!plus_assoc.
assert (Hcost := next_ptd_cost ptd). * rewrite IH1. by apply plus_lt_compat_l.
assert (Hsem := sem_next_ptd ptd). + by apply lt_plus_trans.
destruct next_ptd as [ptd'|].
+ destruct Hstep as (stk' & -> & Hptd')=>/(_ _ _ eq_refl) Hi'.
specialize (IH ptd' stk' Hi' Hptd'). destruct parse_fix=>//.
* apply lt_n_S. by rewrite Hcost.
* by rewrite -Nat.succ_le_mono Hcost Hsem.
+ rewrite Hstep Hcost=>_. auto with arith.
Qed. Qed.
(** We now prove the top-level parsing function. The only thing that (** We now prove the top-level parsing function. The only thing that
...@@ -757,22 +792,26 @@ Qed. ...@@ -757,22 +792,26 @@ Qed.
Variable full_pt : parse_tree (NT (start_nt init)) full_word. Variable full_pt : parse_tree (NT (start_nt init)) full_word.
Theorem parse_complete n_steps: Theorem parse_complete log_n_steps:
match parse safe init (full_word ++ buffer_end) n_steps with match parse safe init (full_word ++ buffer_end) log_n_steps with
| Parsed_pr sem buff => | Parsed_pr sem buff =>
sem = pt_sem full_pt /\ buff = buffer_end /\ pt_size full_pt <= n_steps sem = pt_sem full_pt /\ buff = buffer_end /\ pt_size full_pt <= 2^log_n_steps
| Timeout_pr => n_steps < pt_size full_pt | Timeout_pr => 2^log_n_steps < pt_size full_pt
| Fail_pr => False | Fail_pr => False
end. end.
Proof. Proof.
assert (Hstk : ptd_stack_compat (build_pt_dot_from_pt full_pt Top_ptz) []) by assert (Hstk : ptd_stack_compat (build_pt_dot_from_pt full_pt Top_ptz) []) by
by apply ptd_stack_compat_build_from_pt. by apply ptd_stack_compat_build_from_pt.
unfold parse. unfold parse.
assert (Hparse := parse_fix_complete _ _ n_steps (parse_subproof init) Hstk). assert (Hparse := parse_fix_next_ptd_iter _ _ log_n_steps (parse_subproof init) Hstk).
rewrite -ptd_buffer_build_from_pt -ptd_cost_build_from_pt in Hparse. rewrite -ptd_buffer_build_from_pt -sem_build_from_pt /= in Hparse.
destruct parse_fix=>//. assert (Hcost := next_ptd_iter_cost (build_pt_dot_from_pt full_pt Top_ptz) log_n_steps).
- by rewrite -plus_n_O in Hparse. destruct next_ptd_iter.
- by rewrite -plus_n_O -sem_build_from_pt in Hparse. - destruct Hparse as (? & -> & ?). apply (f_equal S) in Hcost.
rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. rewrite Hcost.
apply le_lt_n_Sm, le_plus_l.
- rewrite Hparse. split; [|split]=>//. apply lt_le_S in Hcost.
by rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost.
Qed. Qed.
End Completeness_Proof. End Completeness_Proof.
......
...@@ -130,11 +130,34 @@ Proof. ...@@ -130,11 +130,34 @@ Proof.
* destruct Hword_stk as [<- ?]; eauto. * destruct Hword_stk as [<- ?]; eauto.
Qed. Qed.
(** [step] preserves the invariant **)
Lemma parse_fix_invariant stk word buffer safe log_n_steps Hi :
word_has_stack_semantics word stk ->
match proj1_sig (parse_fix safe init stk buffer log_n_steps Hi) with
| Accept_sr sem buffer_new =>
exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
(word ++ buffer = word_new ++ buffer_new)%buf /\
pt_sem pt = sem
| Progress_sr stk_new buffer_new =>
exists word_new,
(word ++ buffer = word_new ++ buffer_new)%buf /\
word_has_stack_semantics word_new stk_new
| Fail_sr => True
end.
Proof.
revert stk word buffer Hi.
induction log_n_steps as [|log_n_steps IH]=>/= stk word buffer Hi Hstk;
[by apply step_invariant|].
assert (IH1 := IH stk word buffer Hi Hstk).
destruct parse_fix as [[] Hi']=>/=; try by apply IH1.
destruct IH1 as (word' & -> & Hstk')=>//. by apply IH.
Qed.
(** The interpreter is correct : if it returns a semantic value, then the input (** The interpreter is correct : if it returns a semantic value, then the input
word has this semantic value. word has this semantic value.
**) **)
Theorem parse_correct safe buffer n_steps: Theorem parse_correct safe buffer log_n_steps:
match parse safe init buffer n_steps with match parse safe init buffer log_n_steps with
| Parsed_pr sem buffer_new => | Parsed_pr sem buffer_new =>
exists word_new (pt:parse_tree (NT (start_nt init)) word_new), exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
buffer = (word_new ++ buffer_new)%buf /\ buffer = (word_new ++ buffer_new)%buf /\
...@@ -143,14 +166,9 @@ Theorem parse_correct safe buffer n_steps: ...@@ -143,14 +166,9 @@ Theorem parse_correct safe buffer n_steps:
end. end.
Proof. Proof.
unfold parse. unfold parse.
change buffer with ([] ++ buffer)%buf at 2. revert buffer. generalize Nil_stack_whss. assert (Hparse := parse_fix_invariant [] [] buffer safe log_n_steps
generalize (parse_subproof init). (parse_subproof init)).
generalize (@nil token). generalize (@nil (sigT noninitstate_type)). destruct proj1_sig=>//. apply Hparse. constructor.
induction n_steps as [|n_steps IH]=>//= stk word Hi Hword_stk buffer.
apply (step_invariant _ _ buffer safe Hi) in Hword_stk.
generalize (step_stack_invariant_preserved safe init stk buffer Hi).
destruct step as [| |stk' buffer']=>//. clear Hi. move=> /(_ _ _ eq_refl) Hi.
destruct Hword_stk as (word' & -> & Hword'). by eapply IH.
Qed. Qed.
End Init. End Init.
......
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
(****************************************************************************) (****************************************************************************)
Require Grammar Automaton Interpreter_correct Interpreter_complete. Require Grammar Automaton Interpreter_correct Interpreter_complete.
From Coq Require Import Syntax. From Coq Require Import Syntax Arith.
Module Make(Export Aut:Automaton.T). Module Make(Export Aut:Automaton.T).
Export Aut.Gram. Export Aut.Gram.
...@@ -24,14 +24,14 @@ Module Complete := Interpreter_complete.Make Aut Inter. ...@@ -24,14 +24,14 @@ Module Complete := Interpreter_complete.Make Aut Inter.
Definition complete_validator:unit->bool := Complete.Valid.is_complete. Definition complete_validator:unit->bool := Complete.Valid.is_complete.
Definition safe_validator:unit->bool := ValidSafe.is_safe. Definition safe_validator:unit->bool := ValidSafe.is_safe.
Definition parse (safe:safe_validator ()=true) init n_steps buffer : Definition parse (safe:safe_validator ()=true) init log_n_steps buffer :
parse_result (symbol_semantic_type (NT (start_nt init))):= parse_result (symbol_semantic_type (NT (start_nt init))):=
parse (ValidSafe.is_safe_correct safe) init buffer n_steps. parse (ValidSafe.is_safe_correct safe) init buffer log_n_steps.
(** Correction theorem. **) (** Correction theorem. **)
Theorem parse_correct Theorem parse_correct
(safe:safe_validator ()= true) init n_steps buffer: (safe:safe_validator ()= true) init log_n_steps buffer:
match parse safe init n_steps buffer with match parse safe init log_n_steps buffer with
| Parsed_pr sem buffer_new => | Parsed_pr sem buffer_new =>
exists word (pt : parse_tree (NT (start_nt init)) word), exists word (pt : parse_tree (NT (start_nt init)) word),
buffer = (word ++ buffer_new)%buf /\ buffer = (word ++ buffer_new)%buf /\
...@@ -42,14 +42,15 @@ Proof. apply Correct.parse_correct. Qed. ...@@ -42,14 +42,15 @@ Proof. apply Correct.parse_correct. Qed.
(** Completeness theorem. **) (** Completeness theorem. **)
Theorem parse_complete Theorem parse_complete
(safe:safe_validator () = true) init n_steps word buffer_end: (safe:safe_validator () = true) init log_n_steps word buffer_end:
complete_validator () = true -> complete_validator () = true ->
forall tree:parse_tree (NT (start_nt init)) word, forall tree:parse_tree (NT (start_nt init)) word,
match parse safe init n_steps (word ++ buffer_end) with match parse safe init log_n_steps (word ++ buffer_end) with
| Fail_pr => False | Fail_pr => False
| Parsed_pr sem_res buffer_end_res => | Parsed_pr sem_res buffer_end_res =>
sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\
| Timeout_pr => n_steps < pt_size tree pt_size tree <= 2^log_n_steps
| Timeout_pr => 2^log_n_steps < pt_size tree
end. end.
Proof. Proof.
intros. now apply Complete.parse_complete, Complete.Valid.is_complete_correct. intros. now apply Complete.parse_complete, Complete.Valid.is_complete_correct.
...@@ -70,7 +71,8 @@ Proof. ...@@ -70,7 +71,8 @@ Proof.
Hcomp tree2). Hcomp tree2).
destruct parse. destruct parse.
- destruct Hcomp1. - destruct Hcomp1.
- exfalso. eapply PeanoNat.Nat.lt_irrefl, Hcomp1. - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1].
eapply Nat.pow_gt_lin_r. constructor.
- destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity. - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
Qed. Qed.
......
...@@ -3881,11 +3881,12 @@ The proof of termination of an LR(1) parser in the case of invalid input seems ...@@ -3881,11 +3881,12 @@ The proof of termination of an LR(1) parser in the case of invalid input seems
far from obvious. We did not find such a proof in the literature. In an far from obvious. We did not find such a proof in the literature. In an
application such as CompCert~\cite{compcert}, this question is not considered application such as CompCert~\cite{compcert}, this question is not considered
crucial. For this reason, we did not formally establish the termination of the crucial. For this reason, we did not formally establish the termination of the
parser. Instead, we use the ``fuel'' technique. The parser takes an additional parser. Instead, in order to satisfy Coq's termination requirements, we use
parameter of type \verb+nat+ that indicates the maximum number of steps the the ``fuel'' technique: the parser takes an additional parameter
parser is allowed to perform. In practice, after extracting the code to \verb+log_fuel+ of type \verb+nat+ such that $2^{\verb+log_fuel+}$ is the
\ocaml, one can use the standard trick of passing an infinite amount of fuel, maximum number of steps the parser is allowed to perform. In practice, one
defined in \ocaml by \verb+let rec inf = S inf+. can use a value of e.g., 40 or 50 to make sure the parser will never run out
of fuel in a reasonnable time.
Parsing can have three different outcomes, represented by the type Parsing can have three different outcomes, represented by the type
\verb+parse_result+. \verb+parse_result+.
......
...@@ -480,8 +480,8 @@ module Run (T: sig end) = struct ...@@ -480,8 +480,8 @@ module Run (T: sig end) = struct
fprintf f "Definition %s : nat -> MenhirLibParser.Inter.buffer -> MenhirLibParser.Inter.parse_result %s := MenhirLibParser.parse safe Aut.%s.\n\n" fprintf f "Definition %s : nat -> MenhirLibParser.Inter.buffer -> MenhirLibParser.Inter.parse_result %s := MenhirLibParser.parse safe Aut.%s.\n\n"
funName (print_type (Nonterminal.ocamltype startnt)) (print_init node); funName (print_type (Nonterminal.ocamltype startnt)) (print_init node);
fprintf f "Theorem %s_correct (iterator : nat) (buffer : MenhirLibParser.Inter.buffer):\n" funName; fprintf f "Theorem %s_correct (log_fuel : nat) (buffer : MenhirLibParser.Inter.buffer):\n" funName;
fprintf f " match %s iterator buffer with\n" funName; fprintf f " match %s log_fuel buffer with\n" funName;
fprintf f " | MenhirLibParser.Inter.Parsed_pr sem buffer_new =>\n"; fprintf f " | MenhirLibParser.Inter.Parsed_pr sem buffer_new =>\n";
fprintf f " exists word (tree : Gram.parse_tree (%s) word),\n" fprintf f " exists word (tree : Gram.parse_tree (%s) word),\n"
(print_symbol (Symbol.N startnt)); (print_symbol (Symbol.N startnt));
...@@ -493,14 +493,14 @@ module Run (T: sig end) = struct ...@@ -493,14 +493,14 @@ module Run (T: sig end) = struct
if not Settings.coq_no_complete then if not Settings.coq_no_complete then
begin begin
fprintf f "Theorem %s_complete (iterator : nat) (word : list token) (buffer_end : MenhirLibParser.Inter.buffer) :\n" funName; fprintf f "Theorem %s_complete (log_fuel : nat) (word : list token) (buffer_end : MenhirLibParser.Inter.buffer) :\n" funName;
fprintf f " forall tree : Gram.parse_tree (%s) word,\n" (print_symbol (Symbol.N startnt)); fprintf f " forall tree : Gram.parse_tree (%s) word,\n" (print_symbol (Symbol.N startnt));
fprintf f " match %s iterator (MenhirLibParser.Inter.app_buf word buffer_end) with\n" funName; fprintf f " match %s log_fuel (MenhirLibParser.Inter.app_buf word buffer_end) with\n" funName;
fprintf f " | MenhirLibParser.Inter.Fail_pr => False\n"; fprintf f " | MenhirLibParser.Inter.Fail_pr => False\n";
fprintf f " | MenhirLibParser.Inter.Parsed_pr output_res buffer_end_res =>\n"; fprintf f " | MenhirLibParser.Inter.Parsed_pr output_res buffer_end_res =>\n";
fprintf f " output_res = Gram.pt_sem tree /\\\n"; fprintf f " output_res = Gram.pt_sem tree /\\\n";
fprintf f " buffer_end_res = buffer_end /\\ le (Gram.pt_size tree) iterator\n"; fprintf f " buffer_end_res = buffer_end /\\ (Gram.pt_size tree <= PeanoNat.Nat.pow 2 log_fuel)%%nat\n";
fprintf f " | MenhirLibParser.Inter.Timeout_pr => lt iterator (Gram.pt_size tree)\n"; fprintf f " | MenhirLibParser.Inter.Timeout_pr => (PeanoNat.Nat.pow 2 log_fuel < Gram.pt_size tree)%%nat\n";
fprintf f " end.\n"; fprintf f " end.\n";
fprintf f "Proof. apply MenhirLibParser.parse_complete with (init:=Aut.%s); exact complete. Qed.\n" (print_init node); fprintf f "Proof. apply MenhirLibParser.parse_complete with (init:=Aut.%s); exact complete. Qed.\n" (print_init node);
end end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment