aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/compat.ml4
blob: 4a36af2d8056b22bb33c34d4635de4d259f647ea (plain)
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** Compatibility file depending on ocaml/camlp4 version *)

(** Locations *)

let file_loc_of_file = function
| None -> ""
| Some f -> f

IFDEF CAMLP5 THEN

module CompatLoc = struct
  include Ploc
  let ghost = dummy
  let merge = encl
end

exception Exc_located = Ploc.Exc

let to_coqloc loc =
  { Loc.fname = Ploc.file_name loc;
    Loc.line_nb = Ploc.line_nb loc;
    Loc.bol_pos = Ploc.bol_pos loc;
    Loc.bp = Ploc.first_pos loc;
    Loc.ep = Ploc.last_pos loc;
    Loc.line_nb_last = Ploc.line_nb_last loc;
    Loc.bol_pos_last = Ploc.bol_pos_last loc; }

let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""

(* Update a loc without allocating an intermediate pair *)
let set_loc_pos loc bp ep =
  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)

(* Increase line number by 1 and update position of beginning of line *)
let bump_loc_line loc bol_pos =
  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)

(* Same as [bump_loc_line], but for the last line in location *)
(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
   so we have to resort to a hack merging two locations. *)
(* Warning: [bump_loc_line_last] changes the end position. You may need to call
   [set_loc_pos] to fix it. *)
let bump_loc_line_last loc bol_pos =
  let loc' =
    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
  in
  Ploc.encl loc loc'

let set_loc_file loc fname =
  Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc)
		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)

(* For some reason, the [Ploc.after] function of Camlp5 does not update line
   numbers, so we define our own function that does it. *)
let after loc =
  let line_nb = Ploc.line_nb_last loc in
  let bol_pos = Ploc.bol_pos_last loc in
  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)

ELSE

module CompatLoc = Camlp4.PreCast.Loc

exception Exc_located = CompatLoc.Exc_located

let to_coqloc loc =
  { Loc.fname = CompatLoc.file_name loc;
    Loc.line_nb = CompatLoc.start_line loc;
    Loc.bol_pos = CompatLoc.start_bol loc;
    Loc.bp = CompatLoc.start_off loc;
    Loc.ep = CompatLoc.stop_off loc;
    Loc.line_nb_last = CompatLoc.stop_line loc;
    Loc.bol_pos_last = CompatLoc.stop_bol loc; }

let make_loc fname line_nb bol_pos start stop =
  CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)

open CompatLoc

let set_loc_pos loc bp ep =
  of_tuple (file_name loc, start_line loc, start_bol loc, bp,
	    stop_line loc, stop_bol loc, ep, is_ghost loc)

let bump_loc_line loc bol_pos =
  of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc,
	    start_line loc + 1, bol_pos, stop_off loc, is_ghost loc)

let bump_loc_line_last loc bol_pos =
  of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc,
	    stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)

let set_loc_file loc fname =
  of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)

let after loc =
  of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc,
	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)

END

let (!@) = to_coqloc

(** Misc module emulation *)

IFDEF CAMLP5 THEN

module PcamlSig = struct end
module Token = Token
module CompatGramext = struct include Gramext type assoc = g_assoc end

ELSE

module PcamlSig = Camlp4.Sig
module Ast = Camlp4.PreCast.Ast
module Pcaml = Camlp4.PreCast.Syntax
module MLast = Ast
module Token = struct exception Error of string end
module CompatGramext = Camlp4.Sig.Grammar

END

(** Signature of CLexer *)

IFDEF CAMLP5 THEN

module type LexerSig = sig
  include Grammar.GLexerType with type te = Tok.t
  module Error : sig
    type t
    exception E of t
    val to_string : t -> string
  end
  type lexer_state
  val init_lexer_state : string option -> lexer_state
  val set_lexer_state : lexer_state -> unit
  val release_lexer_state : unit -> lexer_state
  val drop_lexer_state : unit -> unit
end

ELSE

module type LexerSig = sig
  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
  type lexer_state
  val init_lexer_state : string option -> lexer_state
  val set_lexer_state : lexer_state -> unit
  val release_lexer_state : unit -> lexer_state
  val drop_lexer_state : unit -> unit
end

END

(** Signature and implementation of grammars *)

IFDEF CAMLP5 THEN

module type GrammarSig = sig
  include Grammar.S with type te = Tok.t
  type 'a entry = 'a Entry.e
  type internal_entry = Tok.t Gramext.g_entry
  type symbol = Tok.t Gramext.g_symbol
  type action = Gramext.g_action
  type production_rule = symbol list * action
  type single_extend_statment =
      string option * Gramext.g_assoc option * production_rule list
  type extend_statment =
      Gramext.position option * single_extend_statment list
  type coq_parsable
  val parsable : ?file:string -> char Stream.t -> coq_parsable
  val action : 'a -> action
  val entry_create : string -> 'a entry
  val entry_parse : 'a entry -> coq_parsable -> 'a
  val entry_print : Format.formatter -> 'a entry -> unit
  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
  val srules' : production_rule list -> symbol
  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
end

module GrammarMake (L:LexerSig) : GrammarSig = struct
  include Grammar.GMake (L)
  type 'a entry = 'a Entry.e
  type internal_entry = Tok.t Gramext.g_entry
  type symbol = Tok.t Gramext.g_symbol
  type action = Gramext.g_action
  type production_rule = symbol list * action
  type single_extend_statment =
      string option * Gramext.g_assoc option * production_rule list
  type extend_statment =
      Gramext.position option * single_extend_statment list
  type coq_parsable = parsable * L.lexer_state ref
  let parsable ?file c =
    let state = ref (L.init_lexer_state file) in
    L.set_lexer_state !state;
    let a = parsable c in
    state := L.release_lexer_state ();
    (a,state)
  let action = Gramext.action
  let entry_create = Entry.create
  let entry_parse e (p,state) =
    L.set_lexer_state !state;
    try
      let c = Entry.parse e p in
      state := L.release_lexer_state ();
      c
    with Exc_located (loc,e) ->
      L.drop_lexer_state ();
      let loc' = Loc.get_loc (Exninfo.info e) in
      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
      Loc.raise ~loc e
  let with_parsable (p,state) f x =
    L.set_lexer_state !state;
    try
      let a = f x in
      state := L.release_lexer_state ();
      a
    with e ->
      L.drop_lexer_state ();
      raise e

  let entry_print ft x = Entry.print ft x
  let srules' = Gramext.srules
  let parse_tokens_after_filter = Entry.parse_token
end

ELSE

module type GrammarSig = sig
  include Camlp4.Sig.Grammar.Static
    with module Loc = CompatLoc and type Token.t = Tok.t
  type 'a entry = 'a Entry.t
  type action = Action.t
  type coq_parsable
  val parsable : ?file:string -> char Stream.t -> coq_parsable
  val action : 'a -> action
  val entry_create : string -> 'a entry
  val entry_parse : 'a entry -> coq_parsable -> 'a
  val entry_print : Format.formatter -> 'a entry -> unit
  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
  val srules' : production_rule list -> symbol
end

module GrammarMake (L:LexerSig) : GrammarSig = struct
  (* We need to refer to Coq's module Loc before it is hidden by include *)
  let raise_coq_loc loc e = Loc.raise ~loc:(to_coqloc loc) e
  include Camlp4.Struct.Grammar.Static.Make (L)
  type 'a entry = 'a Entry.t
  type action = Action.t
  type coq_parsable = char Stream.t * L.lexer_state ref
  let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
  let action = Action.mk
  let entry_create = Entry.mk
  let entry_parse e (s,state) =
    L.set_lexer_state !state;
    try
      let c = parse e (*FIXME*)CompatLoc.ghost s in
      state := L.release_lexer_state ();
      c
    with Exc_located (loc,e) ->
      L.drop_lexer_state ();
      raise_coq_loc loc e;;
  let with_parsable (p,state) f x =
    L.set_lexer_state !state;
    try
      let a = f x in
      state := L.release_lexer_state ();
      a
    with e ->
      L.drop_lexer_state ();
      Pervasives.raise e;;
  let entry_print ft x = Entry.print ft x
  let srules' = srules (entry_create "dummy")
end

END

(** Some definitions are grammar-specific in Camlp4, so we use a functor to
    depend on it while taking a dummy argument in Camlp5. *)

module GramextMake (G : GrammarSig) :
sig
  val stoken : Tok.t -> G.symbol
  val sself : G.symbol
  val snext : G.symbol
  val slist0 : G.symbol -> G.symbol
  val slist0sep : G.symbol * G.symbol -> G.symbol
  val slist1 : G.symbol -> G.symbol
  val slist1sep : G.symbol * G.symbol -> G.symbol
  val sopt : G.symbol -> G.symbol
  val snterml : G.internal_entry * string -> G.symbol
  val snterm : G.internal_entry -> G.symbol
  val snterml_level : G.symbol -> string
end =
struct

IFDEF CAMLP5 THEN
  let stoken tok =
    let pattern = match tok with
    | Tok.KEYWORD s -> "", s
    | Tok.IDENT s -> "IDENT", s
    | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
    | Tok.FIELD s -> "FIELD", s
    | Tok.INT s -> "INT", s
    | Tok.STRING s -> "STRING", s
    | Tok.LEFTQMARK -> "LEFTQMARK", ""
    | Tok.BULLET s -> "BULLET", s
    | Tok.EOI -> "EOI", ""
    in
    Gramext.Stoken pattern
ELSE
  module Gramext = G
  let stoken tok = match tok with
  | Tok.KEYWORD s -> Gramext.Skeyword s
  | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok)
END

  IFDEF CAMLP5 THEN
     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
  ELSE
    let slist0sep (x, y) = Gramext.Slist0sep (x, y)
    let slist1sep (x, y) = Gramext.Slist1sep (x, y)
  END

  let snterml (x, y) = Gramext.Snterml (x, y)
  let snterm x = Gramext.Snterm x
  let sself = Gramext.Sself
  let snext = Gramext.Snext
  let slist0 x = Gramext.Slist0 x
  let slist1 x = Gramext.Slist1 x
  let sopt x = Gramext.Sopt x

  let snterml_level = function
  | Gramext.Snterml (_, l) -> l
  | _ -> failwith "snterml_level"

end


(** Misc functional adjustments *)

(** - The lexer produces streams made of pairs in camlp4 *)

let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END

(** - Gram.extend is more currified in camlp5 than in camlp4 *)

IFDEF CAMLP5 THEN
let maybe_curry f x y = f (x,y)
let maybe_uncurry f (x,y) = f x y
ELSE
let maybe_curry f = f
let maybe_uncurry f = f
END

(** Compatibility with camlp5 strict mode *)
IFDEF CAMLP5 THEN
  IFDEF STRICT THEN
    let vala x = Ploc.VaVal x
  ELSE
    let vala x = x
  END
ELSE
  let vala x = x
END

(** Fix a quotation difference in [str_item] *)

let declare_str_items loc l =
IFDEF CAMLP5 THEN
  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
ELSE
  Ast.stSem_of_list l
END

(** Quotation difference for match clauses *)

let default_patt loc =
  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)

IFDEF CAMLP5 THEN

let make_fun loc cl =
  let l = cl @ [default_patt loc] in
  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)

ELSE

let make_fun loc cl =
  let mk_when = function
    | Some w -> w
    | None -> Ast.ExNil loc
  in
  let mk_clause (patt,optwhen,expr) =
    (* correspond to <:match_case< ... when ... -> ... >> *)
    Ast.McArr (loc, patt, mk_when optwhen, expr) in
  let init = mk_clause (default_patt loc) in
  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
  let l = List.fold_right add_clause cl init in
  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)

END

IFDEF CAMLP5 THEN
let warning_verbose = Gramext.warning_verbose
ELSE
(* TODO: this is a workaround, since there isn't such
   [warning_verbose] in new camlp4. *)
let warning_verbose = ref true
END