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
|
(* The idea of this test is to have the lexer crash at a new line,
with the ∀ symbol in line 2; then we test that we can recover correctly. *)
let doc =
"Definition map_union_weak `{β A, Insert K A (M A),
∀ A, Empty (M A),
∀ A, Lookup K A (M A),
∀ A, FinMapToList K A (M A)} {A} (m1 m2 : M A) :=
map_imap (λ l v, Some (default v (m1 !! l))) m2."
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 setup_pa () =
let text = doc in
Pcoq.Parsable.make (Gramlib.Stream.of_string text)
let parse_whole pa =
parse pa 10
(* Use junk *)
let log_file = __FILE__ ^ ".log"
let main () =
let pa = setup_pa () in
let res, loc =
try
let _ = parse_whole pa in
false, Pcoq.Parsable.loc pa
with
(* should be `E Undefined_token` but type is private *)
| CLexer.Error.E _ ->
(* We now consume a single token and check that the location is
correct for "A" *)
let () = Pcoq.Parsable.consume pa 1 in
let loc = Pcoq.Parsable.loc pa in
let res = (loc.line_nb = 2) && (loc.bol_pos = 52) && (loc.bp = 58) && (loc.ep = 59) in
res, loc
| _ -> false, Pcoq.Parsable.loc pa
in
let oc = Stdlib.open_out log_file in
let outf = Format.formatter_of_out_channel oc in
Format.fprintf outf "fail lexer test passed: %a@\n%!" raw_pr_loc loc;
Format.pp_print_flush outf ();
Stdlib.close_out oc;
if res then exit 0 else exit 1
let () = main ()
|
