blob: f6158074c2e131384675239f48b4584297d7a231 (
plain)
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
|
(****************************************************************************)
(* *)
(* 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.
|
