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
open Elpi_util
open Elpi_lexer_config
exception ParseError = Parser_config.ParseError
module type Parser = sig
val program : file:string -> Ast.Program.decl list
val goal : loc:Util.Loc.t -> text:string -> Ast.Goal.t
val goal_from : loc:Util.Loc.t -> Lexing.lexbuf -> Ast.Goal.t
val program_from : loc:Util.Loc.t -> Lexing.lexbuf -> Ast.Program.t
end
module type Parser_w_Internals = sig
include Parser
module Internal : sig
val infix_SYMB : (Lexing.lexbuf -> Tokens.token) -> Lexing.lexbuf -> Ast.Func.t
val prefix_SYMB : (Lexing.lexbuf -> Tokens.token) -> Lexing.lexbuf -> Ast.Func.t
val postfix_SYMB : (Lexing.lexbuf -> Tokens.token) -> Lexing.lexbuf -> Ast.Func.t
end
end
module type Config = sig
val resolver : ?cwd:string -> unit:string -> unit -> string
end
module Make(C : Config) = struct
let parse_ref : (?cwd:string -> string -> (Digest.t * Ast.Program.decl list) list) ref =
ref (fun ?cwd:_ _ -> assert false)
module Grammar = Grammar.Make(struct
let parse_file ?cwd file = !parse_ref ?cwd file
end)
let message_of_state s = try Error_messages.message s with Not_found -> "syntax error"
let chunk s (p1,p2) =
String.sub s p1.Lexing.pos_cnum (p2.Lexing.pos_cnum - p1.Lexing.pos_cnum)
let parse grammar digest lexbuf =
let buffer, lexer = MenhirLib.ErrorReports.wrap Lexer.token in
try
let p = grammar lexer lexbuf in
digest, p
with
| Ast.Term.NotInProlog(loc,message) ->
raise (Parser_config.ParseError(loc,message^"\n"))
| Grammar.Error stateid ->
let message = message_of_state stateid in
let loc = lexbuf.Lexing.lex_curr_p in
let loc = {
Util.Loc.source_name = loc.Lexing.pos_fname;
line = loc.Lexing.pos_lnum;
line_starts_at = loc.Lexing.pos_bol;
source_start = loc.Lexing.pos_cnum;
source_stop = loc.Lexing.pos_cnum;
} in
raise (Parser_config.ParseError(loc,message))
let already_parsed = Hashtbl.create 11
let () =
parse_ref := (fun ?cwd filename ->
let filename = C.resolver ?cwd ~unit:filename () in
let digest = Digest.file filename in
let to_parse =
if Filename.extension filename = ".mod" then
let sigf = Filename.chop_extension filename ^ ".sig" in
if Sys.file_exists sigf then [sigf,Digest.file sigf;filename,digest]
else [filename,digest]
else [filename,digest] in
to_parse |> List.map (fun (filename,digest) ->
if Hashtbl.mem already_parsed digest then
digest, []
else
let ic = open_in filename in
let lexbuf = Lexing.from_channel ic in
lexbuf.Lexing.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
Hashtbl.add already_parsed digest true;
let ast = parse Grammar.program digest lexbuf in
close_in ic;
ast))
let to_lexing_loc { Util.Loc.source_name; line; line_starts_at; source_start; _ } =
{ Lexing.pos_fname = source_name;
pos_lnum = line;
pos_bol = line_starts_at;
pos_cnum = source_start; }
let goal_from ~loc lexbuf =
let lexbuf = { lexbuf with Lexing.lex_start_p = to_lexing_loc loc } in
let lexbuf = { lexbuf with Lexing.lex_curr_p = to_lexing_loc loc } in
snd @@ parse Grammar.goal "" lexbuf
let goal ~loc ~text =
let lexbuf = Lexing.from_string text in
goal_from ~loc lexbuf
let program_from ~loc lexbuf =
Hashtbl.clear already_parsed;
let lexbuf = { lexbuf with Lexing.lex_start_p = to_lexing_loc loc } in
let lexbuf = { lexbuf with Lexing.lex_curr_p = to_lexing_loc loc } in
snd @@ parse Grammar.program "" lexbuf
let program ~file =
Hashtbl.clear already_parsed;
List.(concat (map snd @@ !parse_ref file))
module Internal = struct
let infix_SYMB = Grammar.infix_SYMB
let prefix_SYMB = Grammar.prefix_SYMB
let postfix_SYMB = Grammar.postfix_SYMB
end
end