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
open Domain
open Lang
open Error
module Source = Util.Source
open Source
let with_lexbuf name lexbuf start =
let open Lexing in
lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = name };
try start Lexer.token lexbuf
with Parser.Error ->
error (Lexer.region lexbuf) "syntax error: unexpected token"
let parse_mixop str =
let rec mixop_of_nottyp (nottyp : El.nottyp) =
match nottyp.it with
| AtomT atom -> Mixfix.Atom atom
| SeqT typs ->
let mixops = List.map mixop_of_typ typs in
Mixfix.Seq mixops
| InfixT (typ_l, atom, typ_r) ->
let mixop_l = mixop_of_typ typ_l in
let mixop_r = mixop_of_typ typ_r in
Mixfix.Infix (mixop_l, atom, mixop_r)
| BrackT (atom_l, typ, atom_r) ->
let mixop = mixop_of_typ typ in
Mixfix.Brack (atom_l, mixop, atom_r)
and mixop_of_typ (typ : El.typ) =
match typ with
| PlainT _ -> Mixfix.Arg ()
| NotationT nottyp -> mixop_of_nottyp nottyp
in
let lexbuf = Lexing.from_string str in
let typ =
try Parser.check_typ Lexer.token lexbuf
with Parser.Error ->
error (Lexer.region lexbuf)
(Format.asprintf "syntax error in mixop string: %s" str)
in
mixop_of_typ typ
let parse_file file =
let ic = open_in file in
try
Fun.protect
(fun () -> with_lexbuf file (Lexing.from_channel ic) Parser.spec)
~finally:(fun () -> close_in ic)
with Sys_error msg ->
error (Source.region_of_file file) ("i/o error: " ^ msg)
let parse_string str =
let lexbuf = Lexing.from_string str in
try Parser.spec Lexer.token lexbuf
with Parser.Error ->
error (Lexer.region lexbuf)
(Format.asprintf "syntax error in spec string: %s" str)