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
|
let doc =
"Definition a := Type.
Definition b := Prop.
Definition c :=
b.
Definition d :=
c.
(* this is a comment *)
Definition m :=
forall (x : Type), x.
"
let parse pa n =
let entry = Pvernac.Vernac_.main_entry in
let rec loop res n =
if n = 0 then res else
match Pcoq.Entry.parse entry pa with
| None -> res
| Some r -> loop (r :: res) (n-1)
in
loop [] n |> List.rev
let raw_pr_loc fmt (l : Loc.t) =
let { Loc.fname=_; line_nb; bol_pos; line_nb_last; bol_pos_last; bp; ep } = l in
Format.fprintf fmt "| line_nb: %d | bol_pos: %d | line_nb_last: %d | bol_pos_last: %d | bp: %d | ep: %d |"
line_nb bol_pos line_nb_last bol_pos_last bp ep
let print_locs fmt { CAst.loc; _ } =
Option.iter (Format.fprintf fmt "@[%a@]" raw_pr_loc) loc
let parse_whole () =
let text = doc in
let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string text) in
parse pa 10
(* Use junk *)
let parse_n n =
let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string doc) in
let res1 = parse pa n in
let loc = Pcoq.Parsable.loc pa |> CLexer.after in
let str = Gramlib.Stream.of_string doc in
Gramlib.Stream.njunk () loc.bp str;
let pa = Pcoq.Parsable.make ~loc str in
let res2 = parse pa 10 in
res1 @ res2
(* Use offset to set count and avoid the junk *)
let parse_n_offset n =
let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string doc) in
let res1 = parse pa n in
let loc = Pcoq.Parsable.loc pa |> CLexer.after in
let doc = String.sub doc loc.bp (String.length doc - loc.bp) in
let str = Gramlib.Stream.of_string ~offset:loc.bp doc in
let pa = Pcoq.Parsable.make ~loc str in
let res2 = parse pa 10 in
res1 @ res2
let log_file = __FILE__ ^ ".log"
let main () =
let reference = parse_whole () in
let test1 = [parse_n 1; parse_n 2; parse_n 3; parse_n 4; parse_n 5] in
let test2 = [parse_n_offset 1; parse_n_offset 2; parse_n_offset 3; parse_n_offset 4; parse_n_offset 5] in
let tests = test1 @ test2 in
let res = List.for_all (fun t -> t = reference) tests in
let oc = Stdlib.open_out log_file in
let outf = Format.formatter_of_out_channel oc in
Format.fprintf outf "split parsing test passed: %b@\n%!" res;
List.iter (Format.fprintf outf "locs@\n@[<v>%a@]@\n@\n" (Format.pp_print_list print_locs)) tests;
Format.pp_print_flush outf ();
Stdlib.close_out oc;
if res then exit 0 else exit 1
let () = main ()
|
