Main.v 3.34 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
(****************************************************************************)
(*                                                                          *)
(*                                   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.            *)
(*                                                                          *)
(****************************************************************************)
13

14
Require Grammar Automaton Interpreter_correct Interpreter_complete.
15
From Coq Require Import Syntax Arith.
16 17 18 19 20 21 22 23 24 25

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.
26
Definition safe_validator:unit->bool := ValidSafe.is_safe.
27
Definition parse (safe:safe_validator ()=true) init log_n_steps buffer :
28
  parse_result (symbol_semantic_type (NT (start_nt init))):=
29
  parse (ValidSafe.is_safe_correct safe) init buffer log_n_steps.
30 31 32

(** Correction theorem. **)
Theorem parse_correct
33 34
  (safe:safe_validator ()= true) init log_n_steps buffer:
  match parse safe init log_n_steps buffer with
35
    | Parsed_pr sem buffer_new =>
36
      exists word (pt : parse_tree (NT (start_nt init)) word),
37
        buffer = (word ++ buffer_new)%buf /\
38
        pt_sem pt = sem
39 40
    | _ => True
  end.
41
Proof. apply Correct.parse_correct. Qed.
42 43 44

(** Completeness theorem. **)
Theorem parse_complete
45
  (safe:safe_validator () = true) init log_n_steps word buffer_end:
46
  complete_validator () = true ->
47
  forall tree:parse_tree (NT (start_nt init)) word,
48
  match parse safe init log_n_steps (word ++ buffer_end) with
49 50
  | Fail_pr => False
  | Parsed_pr sem_res buffer_end_res =>
51 52 53
    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
54 55
  end.
Proof.
56
  intros. now apply Complete.parse_complete, Complete.Valid.is_complete_correct.
57 58 59 60 61 62
Qed.

(** Unambiguity theorem. **)
Theorem unambiguity:
  safe_validator () = true -> complete_validator () = true -> inhabited token ->
  forall init word,
63 64
  forall (tree1 tree2:parse_tree (NT (start_nt init)) word),
    pt_sem tree1 = pt_sem tree2.
65
Proof.
66
  intros Hsafe Hcomp [tok] init word tree1 tree2.
67 68 69 70 71
  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).
72 73
  destruct parse.
  - destruct Hcomp1.
74 75
  - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1].
    eapply Nat.pow_gt_lin_r. constructor.
76
  - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
77 78 79
Qed.

End Make.