-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathSharpenedJSONDebug.v
207 lines (191 loc) · 8.09 KB
/
SharpenedJSONDebug.v
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
(** Sharpened ADT for JSON *)
Require Import Fiat.Parsers.Grammars.JSONImpoverished.
Require Import Fiat.Parsers.Refinement.Tactics.
Require Import Fiat.Parsers.Refinement.DisjointRules.
Require Import Fiat.Parsers.Refinement.DisjointRulesRev.
Require Import Fiat.Parsers.ExtrOcamlParsers. (* for simpl rules for [find_first_char_such_that] *)
Require Import Fiat.Parsers.Refinement.BinOpBrackets.BinOpRules.
Require Import Fiat.Parsers.StringLike.String.
Require Import Fiat.Parsers.Refinement.SharpenedJSON.
Require Export Fiat.Parsers.ParserFromParserADT.
Require Export Fiat.Parsers.ExtrOcamlParsers.
Export Fiat.Parsers.ExtrOcamlParsers.HideProofs.
Require Export Fiat.Parsers.StringLike.OcamlString.
Definition json_parser (str : Coq.Strings.String.string) : bool.
Proof.
(*Set Ltac Profiling.*)
Time let splitter := constr:(@ComputationalSplitter(* _ String.string_stringlike _ _*)) in
(idtac;
let str := match goal with
| [ str : String.string |- _ ] => constr:(str)
| [ str : Ocaml.Ocaml.string |- _ ] => constr:(str)
end in
let b := make_Parser splitter in
let b := constr:(ParserInterface.has_parse b str) in
let b' := (let term := b in
let term := match term with
| appcontext[ParserFromParserADT.parser _ ?splitter]
=> let splitter' := head splitter in
(eval unfold splitter' in term)
| _ => constr:(term)
end in
let term := match term with
| appcontext[@ParserInterface.has_parse _ (grammar_of_pregrammar ?G)]
=> let G' := head G in
(eval unfold G' in term)
| _ => constr:(term)
end in
let dummy := cidtac "starting parser_red0" in
let dummy := cidtac "starting parser_red0" in
let term := (eval parser_red0 in term) in
let dummy := cidtac "starting parser_red1" in
let dummy := cidtac "starting parser_red1" in
let term := (eval parser_red1 in term) in
let dummy := cidtac "starting parser_red2" in
let dummy := cidtac "starting parser_red2" in
let term := (eval parser_red2 in term) in
let dummy := cidtac "starting parser_red3" in
let dummy := cidtac "starting parser_red3" in
let term := (eval parser_red3 in term) in
let dummy := cidtac "starting parser_red4" in
let dummy := cidtac "starting parser_red4" in
let term := (eval parser_red4 in term) in
let dummy := cidtac "starting parser_red5" in
let dummy := cidtac "starting parser_red5" in
let term := (eval parser_red5 in term) in (* this runs through 64 GB of RAM *)
let dummy := cidtac "starting parser_red6" in
let dummy := cidtac "starting parser_red6" in
let term := (eval parser_red6 in term) in
let dummy := cidtac "starting parser_red7" in
let dummy := cidtac "starting parser_red7" in
let term := (eval parser_red7 in term) in
let dummy := cidtac "starting parser_red8" in
let dummy := cidtac "starting parser_red8" in
let term := (eval parser_red8 in term) in
let dummy := cidtac "starting parser_red9" in
let dummy := cidtac "starting parser_red9" in
let term := (parser_red9_manual term) in
let dummy := cidtac "starting parser_red10" in
let dummy := cidtac "starting parser_red10" in
let term := (eval parser_red10 in term) in
let dummy := cidtac "starting parser_red11" in
let dummy := cidtac "starting parser_red11" in
let term := (parser_red11_manual term) in
let dummy := cidtac "starting parser_red12" in
let dummy := cidtac "starting parser_red12" in
let term := (eval parser_red12 in term) in
let dummy := cidtac "finished parser_red12" in
let dummy := cidtac "finished parser_red12" in
(*
let term := (match do_simpl_list_map with
| true => eval simpl List.map in term
| _ => term
end) in
let term := (eval parser_red17 in term) in*)
constr:(term)) in
(* exact_no_check b' *)
pose b').
(*Time make_parser (@ComputationalSplitter(* _ String.string_stringlike _ _*)).*)
Show Ltac Profile.
Time Defined.
(*Definition json_parser_ocaml (str : Ocaml.Ocaml.string) : bool.
Proof.
Time make_parser (@ComputationalSplitter _ Ocaml.string_stringlike _ _). (* 0.82 s *)
Defined.*)
Print json_parser(*_ocaml*).
Recursive Extraction json_parser(*_ocaml*).
(*
Definition json_parser (str : Coq.Strings.String.string) : bool.
Proof.
Set Ltac Profiling.
Time let splitter := constr:(@ComputationalSplitter(* _ String.string_stringlike _ _*)) in
(idtac;
let str := match goal with
| [ str : String.string |- _ ] => constr:(str)
| [ str : Ocaml.Ocaml.string |- _ ] => constr:(str)
end in
let b := make_Parser splitter in
let b := constr:(ParserInterface.has_parse b str) in
pose b).
Locate grammar_of_pregrammar.
let term := (eval cbv [b] in b) in
lazymatch term with
| appcontext[@ParserInterface.has_parse _ (ContextFreeGrammar.PreNotations.grammar_of_pregrammar ?G)]
=> let G' := head G in
end.
let b' := (let term := b in
let term := lazymatch term with
| context[@ParserInterface.has_parse _ (grammar_of_pregrammar ?G)]
=> let G' := head G in
(eval unfold G' in term)
end in
let term := match term with
| context[ParserFromParserADT.parser _ ?splitter]
=> let splitter' := head splitter in
(eval unfold splitter' in term)
| _ => constr:(term)
end in
let dummy := cidtac "starting parser_red0" in
let dummy := cidtac "starting parser_red0" in
let term := (eval parser_red0 in term) in
let dummy := cidtac "starting parser_red1" in
let dummy := cidtac "starting parser_red1" in
let term := (eval parser_red1 in term) in
let dummy := cidtac "starting parser_red2" in
let dummy := cidtac "starting parser_red2" in
let term := (eval parser_red2 in term) in
let dummy := cidtac "starting parser_red3" in
let dummy := cidtac "starting parser_red3" in
let term := (eval parser_red3 in term) in
let dummy := cidtac "starting parser_red4" in
let dummy := cidtac "starting parser_red4" in
let term := (eval parser_red4 in term) in
let dummy := cidtac "starting parser_red5" in
let dummy := cidtac "starting parser_red5" in
let term := (eval parser_red5 in term) in
let dummy := cidtac "starting parser_red6" in
let dummy := cidtac "starting parser_red6" in
let term := (eval parser_red6 in term) in
let dummy := cidtac "starting parser_red7" in
let dummy := cidtac "starting parser_red7" in
let term := (eval parser_red7 in term) in
let dummy := cidtac "starting parser_red8" in
let dummy := cidtac "starting parser_red8" in
let term := (eval parser_red8 in term) in
let dummy := cidtac "starting parser_red9" in
let dummy := cidtac "starting parser_red9" in
let term := (parser_red9_manual term) in
let dummy := cidtac "starting parser_red10" in
let dummy := cidtac "starting parser_red10" in
let term := (eval parser_red10 in term) in
let dummy := cidtac "starting parser_red11" in
let dummy := cidtac "starting parser_red11" in
let term := (parser_red11_manual term) in
let dummy := cidtac "starting parser_red12" in
let dummy := cidtac "starting parser_red12" in
let term := (eval parser_red12 in term) in
let dummy := cidtac "finished parser_red12" in
let dummy := cidtac "finished parser_red12" in
(*
let term := (match do_simpl_list_map with
| true => eval simpl List.map in term
| _ => term
end) in
let term := (eval parser_red17 in term) in*)
constr:(term)) in
pose b').
Set Printing Depth 100000.
pose
(Def Method "length" (r : rep) : rep * nat := (r, length r) )%cMethDef.
Set Printing All.
Print getcMethDef.
Time make_parser (@ComputationalSplitter(* _ String.string_stringlike _ _*)).
Show Ltac Profile.
Time Defined.
(*Definition json_parser_ocaml (str : Ocaml.Ocaml.string) : bool.
Proof.
Time make_parser (@ComputationalSplitter _ Ocaml.string_stringlike _ _). (* 0.82 s *)
Defined.*)
Print json_parser(*_ocaml*).
Recursive Extraction json_parser(*_ocaml*).
*)