package elpi

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file ast.ml

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
422
423
424
425
426
427
428
429
430
431
432
(* elpi: embedded lambda prolog interpreter                                  *)
(* license: GNU Lesser General Public License Version 2.1 or later           *)
(* ------------------------------------------------------------------------- *)

open Elpi_util
open Util

module Loc = Loc
module Func = struct

  module Self = struct

  type t = string
  let compare = String.compare

  (* Hash consing *)
  let from_string =
   let h = Hashtbl.create 37 in
   let rec aux = function
    | "nil" -> aux "[]"
    | "cons" -> aux "::"
    | "&" -> aux "," (* legacy parser *)
    | x ->
       try Hashtbl.find h x
       with Not_found -> Hashtbl.add h x x ; x
   in
     aux

  let pp fmt s = Format.fprintf fmt "%s" s
  let show x = x
  let equal x y = x == y || x = y (* Resilient to unmarshaling *)
  let truef = from_string "true"
  let andf = from_string ","
  let orf = from_string ";"
  let implf = from_string "=>"
  let implbangf = from_string "=!=>"
  let rimplf = from_string ":-"
  let cutf = from_string "!"
  let pif = from_string "pi"
  let sigmaf = from_string "sigma"
  let eqf = from_string "="
  let pmf = from_string "pattern_match"
  let isf = from_string "is"
  let asf = from_string "as"
  let consf = from_string "::"
  let nilf = from_string "[]"
  let arrowf = from_string "->"
  let sequentf = from_string "?-"
  let ctypef = from_string "ctype"

  let propf = from_string "prop"
  let fpropf = from_string "fprop"

  let typef = from_string "type"
  let mainf = from_string "main"

  
  let dummyname = from_string "%dummy"
  let spillf = from_string "%spill"

  end

  let is_uvar_name s =
    let c = s.[0] in
    ('A' <= c && c <= 'Z')

  include Self
  module Map = Map.Make(Self)
  module Set = Set.Make(Self)

end

module Mode : Mode with type t = Mode.t = Mode

type raw_attribute =
  | If of string
  | Name of string
  | After of string
  | Before of string
  | Replace of string
  | Remove of string
  | External of string option
  | Index of int list * string option
  | Functional
  | Untyped
[@@deriving show, ord]


module TypeExpression = struct

  type 'attribute t_ =
    | TConst of Func.t
    | TApp of Func.t * 'attribute t * 'attribute t list
    | TPred of 'attribute * (Mode.t * 'attribute t) list
    | TArr of 'attribute t * 'attribute t
  and 'a t = { tit : 'a t_; tloc : Loc.t }
  [@@ deriving show, ord]

end
  
module Term = struct
  
  type typ = raw_attribute list TypeExpression.t
  [@@ deriving show, ord]
  type t_ =
   | Const of Func.t
   | App of t * t list
   | Lam of Func.t * Loc.t * typ option * t
   | CData of CData.t
   | Quoted of quote
   | Cast of t * typ
   | Parens of t
  and t = { it : t_; loc : Loc.t }
  and quote = { qloc : Loc.t; data : string; kind : string option }
  [@@ deriving show, ord]

exception NotInProlog of Loc.t * string

let mkC loc x = { loc; it = CData x }
let mkLam loc x xloc ty t = { loc; it = Lam (Func.from_string x,xloc,ty,t) }
let mkNil loc = {loc; it = Const Func.nilf }
let mkParens loc t = { loc; it = Parens t }
let mkQuoted loc pad s =
  let strip n m loc = { loc with Loc.source_start = loc.Loc.source_start + n;
                                 Loc.source_stop = loc.Loc.source_stop - m;
             } in
  (* Printf.eprintf "mkQuoted '%s'\n" s; *)
  let find_data i pad =
    match s.[i] with
    (* | '{' -> assert false; find_data (i+1) (pad+1) *)
    | ':' ->
       let len = String.length s in
       let rec find_space i =
         if i >= len then
           raise (NotInProlog(loc,"syntax error: bad named quotation: {{"^s^"}}.\nDid you separate the name from the data with a space as in {{:name data}} ?."));
         match s.[i] with
         | ' ' -> i 
         | '\n' -> i 
         | _ -> find_space (i+1) in
       let space_after = find_space 0 in
  (* Printf.eprintf "mkQuoted space_after '%d'\n" space_after; *)
       let kind = String.sub s 1 (space_after-1) in
       let data = String.sub s (space_after+1) (String.length s - space_after-1) in
       let qloc = strip (space_after+1+pad) pad loc in
  (* Printf.eprintf "mkQuoted data '%s'\n" data;
  Printf.eprintf "mkQuoted kind '%s'\n" kind;
  Printf.eprintf "mkQuoted qloc '%s'\n" (Loc.show qloc); *)
       { qloc; data; kind = Some kind }
    | _ ->
      let qloc = strip pad pad loc in
  (* Printf.eprintf "mkQuoted qloc '%s'\n" (Loc.show qloc); *)
       { qloc; data = String.sub s i (String.length s - i - i); kind = None }
  in
    { loc; it = Quoted (find_data 0 pad) }
let mkSeq ?loc (l : t list) =
 let rec aux = function
    [] -> assert false
  | [e] -> e
  | { it = Parens it} :: tl -> aux (it :: tl)
  | hd::tl ->
      let tl = aux tl in
      { loc = Loc.merge hd.loc tl.loc; it = App({ it = Const Func.consf; loc = hd.loc },[hd;tl]) }
 in
   let l = aux l in
   match loc with None -> l | Some loc -> { l with loc }
let mkCast loc t ty = { loc; it = Cast(t,ty) }

let rec best_effort_pp = function
 | Lam (x,_,_,t) -> "x\\" ^ best_effort_pp t.it
 | CData c -> CData.show c
 | Quoted _ -> "{{ .. }}"
 | Cast _ -> "(.. : ..)"
 | _ -> ".."

let mkApp loc = function
(* FG: for convenience, we accept an empty list of arguments *)
  | [{ it = (App _ | Const _ | Quoted _) } as c] -> c
  | { it = App(c,l1) } ::l2 -> { loc; it = App(c,l1@l2) }
  | { it = (Const _ | Quoted _) } as c::l2 -> { loc; it = App(c,l2) }
  | [] -> anomaly ~loc "empty application"
  | x::_ -> raise (NotInProlog(loc,"syntax error: the head of an application must be a constant or a variable, got: " ^ best_effort_pp x.it))

let mkAppF loc (cloc, c) l =
  if l = [] then anomaly ~loc "empty application";
  if c = "," then
      { loc; it =
        App({ it = Const c; loc = cloc },
          List.concat_map (function 
            | { loc; it = Parens { it = App({it=Const ","}, l)}} -> l
            | { loc; it = App({it=Const ","}, l)} -> l
            | x -> [x]
        ) l) }
  else
    { loc; it = App({ it = Const c; loc = cloc },l) }



let last_warn_impl = ref (Loc.initial "(dummy)")
let warn_impl { it; loc } =
  match it with
  | App({ it = Const "=>" }, _ ) ->
      if !last_warn_impl <> loc then
        warn ~loc ~id:ImplicationPrecedence
{|The standard λProlog infix operator for implication => has higher precedence
than conjunction. This means that 'A => B, C' reads '(A => B), C'.
This is a common mistake since it makes A only available to B (and not to C
as many newcomers may expect).
If this is really what you want write '(A => B), C' to silence this warning.
Otherwise write 'A => (B, C)', or use the alternative implication operator ==>.
Infix ==>  has lower precedence than conjunction, hence
'A ==> B, C' reads 'A ==> (B, C)' and means the same as 'A => (B, C)'.|};
      last_warn_impl := loc
  | _ -> ()

let warn_impl_conj_precedence = function
  | App({ it = Const "," }, args ) ->
      begin match List.rev args with
      | { it = Const "!"} :: args_but_last -> ()
      | _ :: args_but_last -> List.iter warn_impl args_but_last
      | _ -> ()
      end
  | _ -> ()

let mkAppF loc (cloc,c) l =
  let t = mkAppF loc (cloc,c) l in
  warn_impl_conj_precedence t.it;
  t


let fresh_uv_names = ref (-1);;
let mkFreshUVar loc = incr fresh_uv_names; { loc; it = Const (Func.from_string ("_" ^ string_of_int !fresh_uv_names)) }
let fresh_names = ref (-1);;
let mkFreshName loc = incr fresh_names; { loc; it = Const (Func.from_string ("__" ^ string_of_int !fresh_names)) }
let mkCon loc c = { loc; it = Const (Func.from_string c) }
let mkConst loc c = { loc; it = Const c }

end

module Clause = struct
  
  type ('term,'attributes,'spill,'deterministic) t = {
    loc : Loc.t;
    attributes : 'attributes;
    body : 'term;
    needs_spilling : 'spill;
  }
  [@@deriving show, ord]

end

module Chr = struct

  type 'term sequent = { eigen : 'term; context : 'term; conclusion : 'term }
  and ('attribute,'term) t = {
    to_match : 'term sequent list;
    to_remove : 'term sequent list;
    guard : 'term option;
    new_goal : 'term sequent option;
    attributes : 'attribute;
    loc : Loc.t;
  }
  [@@ deriving show,ord]

end

module Macro = struct

  type ('name,'term) t = {
     loc : Loc.t;
     name : 'name;
     body : 'term
  }
  [@@deriving show, ord]

end

module Type = struct

  type ('attribute,'inner_attribute) t = {
    loc : Loc.t;
    attributes : 'attribute;
    name : Func.t;
    ty : 'inner_attribute TypeExpression.t;
  }
  [@@deriving show, ord]

end

module TypeAbbreviation = struct

  type 'ty closedTypeexpression = 
    | Lam of Func.t * Loc.t * 'ty closedTypeexpression 
    | Ty of 'ty
  [@@ deriving show, ord]

  type ('name,'ty) t =
    { name : 'name; value : 'ty closedTypeexpression; nparams : int; loc : Loc.t }
  [@@ deriving show, ord]

end


module Program = struct

  type decl =
    (* Blocks *)
    | Begin of Loc.t
    | Namespace of Loc.t * Func.t
    | Constraint of Loc.t * Func.t list * Func.t list
    | Shorten of Loc.t * (Func.t * Func.t) list (* prefix suffix *)
    | End of Loc.t

    | Accumulated of Loc.t * parser_output list

    (* data *)
    | Clause of (Term.t, raw_attribute list,unit, unit) Clause.t
    | Chr of (raw_attribute list,Term.t) Chr.t
    | Macro of (Func.t, Term.t) Macro.t
    | Kind of (raw_attribute list,raw_attribute list) Type.t list
    | Type of (raw_attribute list,raw_attribute list) Type.t list
    | Pred of (raw_attribute list,raw_attribute list) Type.t
    | TypeAbbreviation of (Func.t,raw_attribute list TypeExpression.t) TypeAbbreviation.t
    | Ignored of Loc.t
  and parser_output = { file_name : string; digest : Digest.t; ast : decl list }
  [@@deriving show]


type t = decl list [@@deriving show]

end

module Goal = struct

  type t = Term.t
  let pp fmt t = Term.pp fmt t
  let show x = Format.asprintf "%a" pp x

end
 
module Fmt = Format

let cfloat =
  CData.(declare {
    data_name = "float";
    data_pp = (fun f x -> Fmt.fprintf f "%f" x);
    data_compare = Float.compare;
    data_hash = Hashtbl.hash;
    data_hconsed = false;
  })
let cint =
  CData.(declare {
    data_name = "int";
    data_pp = (fun f x -> Fmt.fprintf f "%d" x);
    data_compare = Int.compare;
    data_hash = Hashtbl.hash;
    data_hconsed = false;
  })
let cstring =
  CData.(declare {
    data_name = "string";
    data_pp = (fun f x -> Fmt.fprintf f "%s" x);
    data_compare = String.compare;
    data_hash = Hashtbl.hash;
    data_hconsed = true;
  })
let cloc =
  CData.(declare {
    data_name = "loc";
    data_pp = Util.Loc.pp;
    data_compare = Stdlib.compare;
    data_hash = Hashtbl.hash;
    data_hconsed = false;
  })

module Structured = struct
type provenance =
  | Core (* baked into the elpi runtime *)
  | Builtin of { variant : int } (* builtin or host declared *)
  | File of Loc.t
[@@deriving show, ord]
  
type program = {
  macros : (Func.t, Term.t) Macro.t list;
  kinds : (unit,unit) Type.t list;
  types : (symbol_attribute,functionality) Type.t list;
  type_abbrevs : (Func.t,functionality TypeExpression.t) TypeAbbreviation.t list;
  body : block list;
}
and cattribute = {
  cid : string;
  cifexpr : string option
}
and ('func,'term) block_constraint = {
   loc: Loc.t;
   clique : 'func list;
   ctx_filter : 'func list;
   rules : (cattribute,'term) Chr.t list
}
and block =
  | Clauses of (Term.t,attribute,unit,unit) Clause.t list
  | Namespace of Func.t * program
  | Shorten of Func.t shorthand list * program
  | Constraints of (Func.t,Term.t) block_constraint * program
  | Accumulated of program
and attribute = {
  insertion : insertion option;
  id : string option;
  ifexpr : string option;
  typecheck : bool;
}
and insertion = Insert of insertion_place | Replace of string | Remove of string
and insertion_place = Before of string | After of string
and symbol_attribute = {
  availability : symbol_availability;
  index : predicate_indexing option;
}
and predicate_indexing =
  | Index of int list * tindex option
  | MaximizeForFunctional
and symbol_availability = Elpi | OCaml of provenance
and tindex = Map | HashMap | DiscriminationTree
and 'a shorthand = {
  iloc : Loc.t;
  full_name : 'a;
  short_name : 'a;
}
and functionality = Function | Relation
and variadic = Variadic | NotVariadic
[@@deriving show, ord]

end

OCaml

Innovation. Community. Security.