1 files changed, 79 insertions, 0 deletions
diff --git a/MenhirLib/Main.v b/MenhirLib/Main.v
new file mode 100644
index 00000000..f6158074
--- /dev/null
+++ b/MenhirLib/Main.v
@@ -0,0 +1,79 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+Require Grammar Automaton Interpreter_correct Interpreter_complete.
+From Coq Require Import Syntax Arith.
+
+Module Make(Export Aut:Automaton.T).
+Export Aut.Gram.
+Export Aut.GramDefs.
+
+Module Import Inter := Interpreter.Make Aut.
+Module Correct := Interpreter_correct.Make Aut Inter.
+Module Complete := Interpreter_complete.Make Aut Inter.
+
+Definition complete_validator:unit->bool := Complete.Valid.is_complete.
+Definition safe_validator:unit->bool := ValidSafe.is_safe.
+Definition parse (safe:safe_validator ()=true) init log_n_steps buffer :
+  parse_result (symbol_semantic_type (NT (start_nt init))):=
+  parse (ValidSafe.safe_is_validator safe) init buffer log_n_steps.
+
+(** Correction theorem. **)
+Theorem parse_correct
+  (safe:safe_validator ()= true) init log_n_steps buffer:
+  match parse safe init log_n_steps buffer with
+    | Parsed_pr sem buffer_new =>
+      exists word (pt : parse_tree (NT (start_nt init)) word),
+        buffer = (word ++ buffer_new)%buf /\
+        pt_sem pt = sem
+    | _ => True
+  end.
+Proof. apply Correct.parse_correct. Qed.
+
+(** Completeness theorem. **)
+Theorem parse_complete
+  (safe:safe_validator () = true) init log_n_steps word buffer_end:
+  complete_validator () = true ->
+  forall tree:parse_tree (NT (start_nt init)) word,
+  match parse safe init log_n_steps (word ++ buffer_end) with
+  | Fail_pr => False
+  | Parsed_pr sem_res buffer_end_res =>
+    sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\
+    pt_size tree <= 2^log_n_steps
+  | Timeout_pr => 2^log_n_steps < pt_size tree
+  end.
+Proof.
+  intros. now apply Complete.parse_complete, Complete.Valid.complete_is_validator.
+Qed.
+
+(** Unambiguity theorem. **)
+Theorem unambiguity:
+  safe_validator () = true -> complete_validator () = true -> inhabited token ->
+  forall init word,
+  forall (tree1 tree2:parse_tree (NT (start_nt init)) word),
+    pt_sem tree1 = pt_sem tree2.
+Proof.
+  intros Hsafe Hcomp [tok] init word tree1 tree2.
+  pose (buf_end := cofix buf_end := (tok :: buf_end)%buf).
+  assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree1).
+  assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree2).
+  destruct parse.
+  - destruct Hcomp1.
+  - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1].
+    eapply Nat.pow_gt_lin_r. constructor.
+  - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
+Qed.
+
+End Make.