forked from LPCIC/elpi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbuiltin.ml
1541 lines (1303 loc) · 49.6 KB
/
builtin.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
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* elpi: embedded lambda prolog interpreter *)
(* license: GNU Lesser General Public License Version 2.1 or later *)
(* ------------------------------------------------------------------------- *)
open Elpi_util
open API
open RawData
open Utils
open BuiltInPredicate
open Notation
module Str = Re.Str
let in_stream_decl = {
OpaqueData.name = "in_stream";
pp = (fun fmt (_,d) -> Format.fprintf fmt "<in_stream:%s>" d);
compare = (fun (_,s1) (_,s2) -> String.compare s1 s2);
hash = (fun (x,_) -> Hashtbl.hash x);
hconsed = false;
constants = ["std_in",(stdin,"stdin")];
doc = "";
}
let in_stream = OpaqueData.declare in_stream_decl
let out_stream_decl = {
OpaqueData.name = "out_stream";
pp = (fun fmt (_,d) -> Format.fprintf fmt "<out_stream:%s>" d);
compare = (fun (_,s1) (_,s2) -> String.compare s1 s2);
hash = (fun (x,_) -> Hashtbl.hash x);
hconsed = false;
doc = "";
constants = ["std_out",(stdout,"stdout");"std_err",(stderr,"stderr")];
}
let out_stream = OpaqueData.declare out_stream_decl
type process = {
stdin : out_channel * string;
stdout : in_channel * string;
stderr : in_channel * string;
}
let process = AlgebraicData.declare {
AlgebraicData.ty = TyName "unix.process";
doc = "gathers the standard file descriptors or a process";
pp = (fun fmt { stdin; stdout; stderr } ->
Format.fprintf fmt "{ stdin = %a; stdout = %a; stderr = %a }"
out_stream_decl.OpaqueData.pp stdin
in_stream_decl.OpaqueData.pp stdout
in_stream_decl.OpaqueData.pp stderr
);
constructors = [
K("unix.process","",A(out_stream,A(in_stream,A(in_stream,N))),
B (fun stdin stdout stderr -> { stdin; stdout; stderr }),
M (fun ~ok ~ko:_ { stdin; stdout; stderr } -> ok stdin stdout stderr ))
]
}|> ContextualConversion.(!<)
let really_input ic s ofs len =
let rec unsafe_really_input read ic s ofs len =
if len <= 0 then read else begin
let r = input ic s ofs len in
if r = 0
then read
else unsafe_really_input (read+r) ic s (ofs + r) (len - r)
end
in
if ofs < 0 || len < 0 || ofs > Bytes.length s - len
then invalid_arg "really_input"
else unsafe_really_input 0 ic s ofs len
(* constant x occurs in term t with level d? *)
let occurs x d t =
let rec aux d t = match look ~depth:d t with
| Const c -> c = x
| Lam t -> aux (d+1) t
| App (c, v, vs) -> c = x || aux d v || auxs d vs
| UnifVar (_, l) -> auxs d l
| Builtin (_, vs) -> auxs d vs
| Cons (v1, v2) -> aux d v1 || aux d v2
| Nil
| CData _ -> false
and auxs d = function
| [] -> false
| t :: ts -> aux d t || auxs d ts
in
x < d && aux d t
type polyop = {
p : 'a. 'a -> 'a -> bool;
psym : string;
pname : string;
}
let bool = AlgebraicData.declare {
AlgebraicData.ty = TyName "bool";
doc = "Boolean values: tt and ff since true and false are predicates";
pp = (fun fmt b -> Format.fprintf fmt "%b" b);
constructors = [
K("tt","",N,
B true,
M (fun ~ok ~ko -> function true -> ok | _ -> ko ()));
K("ff","",N,
B false,
M (fun ~ok ~ko -> function false -> ok | _ -> ko ()));
]
}|> ContextualConversion.(!<)
let pair a b = let open AlgebraicData in declare {
ty = TyApp ("pair",a.Conversion.ty,[b.Conversion.ty]);
doc = "Pair: the constructor is pr, since ',' is for conjunction";
pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_pair a.Conversion.pp b.Conversion.pp) o);
constructors = [
K("pr","",A(a,A(b,N)),
B (fun a b -> (a,b)),
M (fun ~ok ~ko:_ -> function (a,b) -> ok a b));
]
} |> ContextualConversion.(!<)
let option a = let open AlgebraicData in declare {
ty = TyApp("option",a.Conversion.ty,[]);
doc = "The option type (aka Maybe)";
pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_option a.Conversion.pp) o);
constructors = [
K("none","",N,
B None,
M (fun ~ok ~ko -> function None -> ok | _ -> ko ()));
K("some","",A(a,N),
B (fun x -> Some x),
M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ()));
]
} |> ContextualConversion.(!<)
type diagnostic = OK | ERROR of string ioarg
let mkOK = OK
let mkERROR s = ERROR (mkData s)
let diagnostic = let open API.AlgebraicData in declare {
ty = TyName "diagnostic";
doc = "Used in builtin variants that return Coq's error rather than failing";
pp = (fun fmt -> function
| OK -> Format.fprintf fmt "OK"
| ERROR NoData -> Format.fprintf fmt "ERROR _"
| ERROR (Data s) -> Format.fprintf fmt "ERROR %S" s);
constructors = [
K("ok","Success",N,
B mkOK,
M (fun ~ok ~ko -> function OK -> ok | _ -> ko ()));
K("error","Failure",A(BuiltInPredicate.ioarg BuiltInData.string,N),
B (fun s -> ERROR s),
M (fun ~ok ~ko -> function ERROR s -> ok s | _ -> ko ()));
K("uvar","",A(FlexibleData.uvar,N),
B (fun _ -> assert false),
M (fun ~ok ~ko _ -> ko ()))
]
} |> ContextualConversion.(!<)
let unix_error_to_diagnostic e f a =
mkERROR (Printf.sprintf "%s: %s" (if a <> "" then f ^ " " ^ a else f) (Unix.error_message e))
let cmp = let open AlgebraicData in declare {
ty = TyName "cmp";
doc = "Result of a comparison";
pp = (fun fmt i -> Format.fprintf fmt "%d" i);
constructors = [
K("eq", "", N, B 0, M(fun ~ok ~ko i -> if i == 0 then ok else ko ()));
K("lt", "", N, B ~-1, M(fun ~ok ~ko i -> if i < 0 then ok else ko ()));
K("gt", "", N, B 1, M(fun ~ok ~ko i -> if i > 0 then ok else ko ()))
]
} |> ContextualConversion.(!<)
let error_cmp_flex ~depth t1 t2 = error "cmp_term on non-ground terms"
let rec cmp_term ~depth t1 t2 =
match look ~depth t1, look ~depth t2 with
| Nil, Nil -> 0
| Nil, (Cons _ | Const _ | App _ | Lam _ | Builtin _ | CData _ | UnifVar _) -> -1
| Cons(x,xs), Cons(y,ys) ->
let cmp_x = cmp_term ~depth x y in
if cmp_x == 0 then cmp_term ~depth xs ys
else cmp_x
| Cons _, (Const _ | App _ | Lam _ | Builtin _ | CData _ | UnifVar _) -> -1
| Cons _, Nil -> 1
| Const c1, Const c2 -> c1 - c2
| Const _, (App _ | Lam _ | Builtin _ | CData _ | UnifVar _) -> -1
| Const _, (Cons _ | Nil) -> 1
| Lam t1, Lam t2 -> cmp_term ~depth:(depth+1) t1 t2
| Lam _, (App _ | Builtin _ | CData _ | UnifVar _) -> -1
| Lam _, (Const _ | Cons _ | Nil) -> 1
| App(c1,x,xs), App(c2,y,ys) ->
let cmp_c1 = c1 - c2 in
if cmp_c1 == 0 then
let cmp_x = cmp_term ~depth x y in
if cmp_x == 0 then cmp_terms ~depth xs ys else cmp_x
else cmp_c1
| App _, (Builtin _ | CData _ | UnifVar _) -> -1
| App _, (Lam _ | Const _ | Cons _ | Nil) -> 1
| Builtin(c1,xs), Builtin(c2,ys) ->
let cmp_c1 = cmp_builtin c1 c2 in
if cmp_c1 == 0 then cmp_terms ~depth xs ys else cmp_c1
| Builtin _, (CData _ | UnifVar _) -> -1
| Builtin _, (App _ | Lam _ | Const _ | Cons _ | Nil) -> 1
| CData d1, CData d2 -> RawOpaqueData.compare d1 d2
| CData _, UnifVar _ -> -1
| CData _, (Builtin _ | App _ | Lam _ | Const _ | Cons _ | Nil) -> 1
| UnifVar(b1,xs), UnifVar(b2,ys) ->
if FlexibleData.Elpi.equal b1 b2 then
if cmp_terms ~depth xs ys == 0 then 0
else error_cmp_flex ~depth t1 t2
else error_cmp_flex ~depth t1 t2
| UnifVar _, (CData _ | Builtin _ | App _ | Lam _ | Const _ | Cons _ | Nil) -> 1
and cmp_terms ~depth l1 l2 =
match l1, l2 with
| [], [] -> 0
| [], _ :: _ -> -1
| _ :: _, [] -> 1
| x :: xs, y :: ys ->
let cmp_x = cmp_term ~depth x y in
if cmp_x == 0 then cmp_terms ~depth xs ys else cmp_x
let rec check_ground ~depth t =
match look ~depth t with
| Nil | Const _ | CData _ -> ()
| Lam t -> check_ground ~depth:(depth + 1) t
| Cons(x,xs) -> check_ground ~depth x; check_ground ~depth xs
| Builtin(_,l) -> List.iter (check_ground ~depth) l
| App(_,x,xs) -> check_ground ~depth x; List.iter (check_ground ~depth) xs
| UnifVar _ -> raise No_clause
type 'a unspec = Given of 'a | Unspec
let unspecC data = let open API.ContextualConversion in let open API.RawData in {
ty = data.ty;
pp_doc = data.pp_doc;
pp = (fun fmt -> function
| Unspec -> Format.fprintf fmt "Unspec"
| Given x -> Format.fprintf fmt "Given %a" data.pp x);
embed = (fun ~depth hyps constraints state -> function
| Given x -> data.embed ~depth hyps constraints state x
| Unspec -> state, mkDiscard, []);
readback = (fun ~depth hyps constraints state x ->
match look ~depth x with
| UnifVar _ -> state, Unspec, []
| t ->
let state, x, gls = data.readback ~depth hyps constraints state (kool t) in
state, Given x, gls)
}
let unspec d = API.ContextualConversion.(!<(unspecC (!> d)))
(** Core built-in ********************************************************* *)
let core_builtins = let open BuiltIn in let open ContextualConversion in [
LPDoc "File generated by elpi -document-builtins, do not edit";
LPDoc " == Core builtins =====================================";
LPDoc " -- Logic --";
LPCode "pred true.";
LPCode "true.";
LPCode "pred fail.";
LPCode "pred false.";
LPCode "external pred (=) o:A, o:A. % unification";
MLData BuiltInData.int;
MLData BuiltInData.string;
MLData BuiltInData.float;
LPCode "pred (;) i:prop, i:prop.";
LPCode "(A ; _) :- A.";
LPCode "(_ ; B) :- B.";
LPCode "type (:-) prop -> prop -> prop.";
LPCode "type (:-) prop -> list prop -> prop.";
LPCode "type (,) variadic prop prop.";
LPCode "type uvar A.";
LPCode "type (as) A -> A -> A.";
LPCode "type (=>) prop -> prop -> prop.";
LPCode "type (=>) list prop -> prop -> prop.";
LPDoc " -- Control --";
(* This is not implemented here, since the API had no access to the
* choice points *)
LPCode "external pred !. % The cut operator";
LPCode "pred not i:prop.";
LPCode "not X :- X, !, fail.";
LPCode "not _.";
(* These are not implemented here since the API has no access to the
* store of syntactic constraints *)
LPCode ("% [declare_constraint C Key1 Key2...] declares C blocked\n"^
"% on Key1 Key2 ... (variables, or lists thereof).\n"^
"external type declare_constraint any -> any -> variadic any prop.");
LPCode "external pred print_constraints. % prints all constraints";
MLCode(Pred("halt", VariadicIn(unit_ctx, !> BuiltInData.any, "halts the program and print the terms"),
(fun args ~depth _ _ ->
if args = [] then error "halt"
else
let b = Buffer.create 80 in
let fmt = Format.formatter_of_buffer b in
Format.fprintf fmt "%a%!" (RawPp.list (RawPp.term depth) " ") args;
error (Buffer.contents b))),
DocAbove);
LPCode "pred stop.";
LPCode "stop :- halt.";
] @ Calc.calc @ [
LPDoc " -- Arithmetic tests --";
] @ List.map (fun { p; psym; pname } ->
MLCode(Pred(pname,
In(BuiltInData.poly "A","X",
In(BuiltInData.poly "A","Y",
Read(unit_ctx,("checks if X " ^ psym ^ " Y. Works for string, int and float")))),
(fun t1 t2 ~depth _ _ state ->
let open RawOpaqueData in
let t1 = look ~depth (Calc.eval ~depth state t1) in
let t2 = look ~depth (Calc.eval ~depth state t2) in
match t1, t2 with
| CData x, CData y ->
if ty2 int x y then let out = to_int in
if p (out x) (out y) then () else raise No_clause
else if ty2 float x y then let out = to_float in
if p (out x) (out y) then () else raise No_clause
else if ty2 string x y then let out = to_string in
if p (out x) (out y) then () else raise No_clause
else
type_error ("Wrong arguments to " ^ psym ^ " (or to " ^ pname^ ")")
(* HACK: grundlagen.elpi uses the "age" of constants *)
| Const t1, Const t2 ->
let is_lt = if t1 < 0 && t2 < 0 then p t2 t1 else p t1 t2 in
if not is_lt then raise No_clause else ()
| _ -> type_error ("Wrong arguments to " ^psym^ " (or to " ^pname^ ")"))),
DocAbove))
[ { p = (<); psym = "<"; pname = "lt_" } ;
{ p = (>); psym = ">"; pname = "gt_" } ;
{ p = (<=); psym = "=<"; pname = "le_" } ;
{ p = (>=); psym = ">="; pname = "ge_" } ]
@
let build_symb (spref, ty) =
let op_l = ["gt_";"lt_"; "le_"; "ge_"] in
let sym_l = List.map (fun x -> spref ^ x) [">";"<"; "=<"; ">="] in
let buildLPCode s op = LPCode (Printf.sprintf "pred (%s) i:%s, i:%s.\nX %s Y :- %s X Y." s ty ty s op) in
List.map2 buildLPCode sym_l op_l in
let symbs = ["", "A"; "i", "int"; "r", "float"; "s", "string"] in
List.flatten (List.map build_symb symbs) @
[
LPDoc " -- Standard data types (supported in the FFI) --";
LPCode "kind list type -> type.";
LPCode "type (::) X -> list X -> list X.";
LPCode "type ([]) list X.";
MLData bool;
MLData (pair (BuiltInData.poly "A") (BuiltInData.poly "B"));
LPCode "pred fst i:pair A B, o:A.";
LPCode "fst (pr A _) A.";
LPCode "pred snd i:pair A B, o:B.";
LPCode "snd (pr _ B) B.";
MLData (option (BuiltInData.poly "A"));
MLData cmp;
MLData diagnostic;
]
;;
(** Standard lambda Prolog I/O built-in *********************************** *)
let io_builtins = let open BuiltIn in let open BuiltInData in [
LPDoc " == I/O builtins =====================================";
LPDoc " -- I/O --";
MLData (in_stream);
MLData (out_stream);
MLCode(Pred("open_in",
In(string, "FileName",
Out(in_stream, "InStream",
Easy "opens FileName for input")),
(fun s _ ~depth ->
try !:(open_in s,s)
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("open_out",
In(string, "FileName",
Out(out_stream, "OutStream",
Easy "opens FileName for output")),
(fun s _ ~depth ->
try !:(open_out s,s)
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("open_append",
In(string, "FileName",
Out(out_stream, "OutStream",
Easy "opens FileName for output in append mode")),
(fun s _ ~depth ->
let flags = [Open_wronly; Open_append; Open_creat; Open_text] in
try !:(open_out_gen flags 0o664 s,s)
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("close_in",
In(in_stream, "InStream",
Easy "closes input stream InStream"),
(fun (i,_) ~depth ->
try close_in i
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("close_out",
In(out_stream, "OutStream",
Easy "closes output stream OutStream"),
(fun (o,_) ~depth ->
try close_out o
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("output",
In(out_stream, "OutStream",
In(string, "Data",
Easy "writes Data to OutStream")),
(fun (o,_) s ~depth ->
try output_string o s
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("flush",
In(out_stream, "OutStream",
Easy "flush all output not yet finalized to OutStream"),
(fun (o,_) ~depth ->
try flush o
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("input",
In(in_stream, "InStream",
In(int, "Bytes",
Out(string, "Data",
Easy "reads Bytes from InStream"))),
(fun (i,_) n _ ~depth ->
let buf = Bytes.make n ' ' in
try
let read = really_input i buf 0 n in
let str = Bytes.sub buf 0 read in
!:(Bytes.to_string str)
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("input_line",
In(in_stream, "InStream",
Out(string, "Line",
Easy "reads a full line from InStream")),
(fun (i,_) _ ~depth ->
try !:(input_line i)
with
| End_of_file -> !:""
| Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("eof",
In(in_stream, "InStream",
Easy "checks if no more data can be read from InStream"),
(fun (i,_) ~depth ->
try
let pos = pos_in i in
let _ = input_char i in
Stdlib.seek_in i pos;
raise No_clause
with
| End_of_file -> ()
| Sys_error msg -> error msg)),
DocAbove);
LPDoc " -- System --";
MLCode(Pred("gettimeofday",
Out(float, "T",
Easy "sets T to the number of seconds elapsed since 1/1/1970"),
(fun _ ~depth -> !:(Unix.gettimeofday ()))),
DocAbove);
MLCode(Pred("getenv",
In(string, "VarName",
Out(option string, "Value",
Easy ("Like Sys.getenv"))),
(fun s _ ~depth ->
try !:(Some (Sys.getenv s))
with Not_found -> !: None)),
DocAbove);
MLCode(Pred("system",
In(string, "Command",
Out(int, "RetVal",
Easy "executes Command and sets RetVal to the exit code")),
(fun s _ ~depth -> !:(Sys.command s))),
DocAbove);
LPDoc " -- Unix --";
MLData process;
MLCode(Pred("unix.process.open",
In(unspec string, "Executable",
In(unspec @@ list string, "Arguments",
In(unspec (list string), "Environment",
Out(process, "P",
Out(diagnostic, "Diagnostic",
Easy {|OCaml's Unix.open_process_args_full.
Note that the first argument is the executable name (as in argv[0]).
If Executable is omitted it defaults to the first element of Arguments.
Environment can be left unspecified, defaults to the current process environment.
This API only works reliably since OCaml 4.12.|}))))),
(fun cmd args env _ _ ~depth ->
try
let env =
match env with
| Given l -> Array.of_list l
| Unspec -> Unix.environment () in
let cmd, args =
match cmd, args with
| Given x, Unspec -> x, [x]
| Given x, Given [] -> x, [x]
| Given x, Given args -> x, args
| Unspec, Given (x::_ as args) -> x, args
| _ -> type_error "unix.process.open: no executable and no argumnts" in
let (out,in_,err) as full = Unix.open_process_args_full cmd (Array.of_list args) env in
let pid = Unix.process_full_pid full in
let name_fd s = Printf.sprintf "%s of process %d (%s)" s pid cmd in
!: { stdin = (in_,name_fd "stdin"); stdout = (out,name_fd "stdout"); stderr = (err,name_fd "stderr") } +! mkOK
with Unix.Unix_error(e,f,a) -> ?: None +! (unix_error_to_diagnostic e f a))),
DocAbove);
MLCode(Pred("unix.process.close",
In(process, "P",
Out(diagnostic, "Diagnostic",
Easy "OCaml's Unix.close_process_full")),
(fun { stdin = (out,_); stdout = (in_,_); stderr = (err,_) } _ ~depth ->
match Unix.close_process_full (in_,out,err) with
| Unix.WEXITED 0 -> !: mkOK
| Unix.WEXITED i -> !: (mkERROR (Printf.sprintf "exited: %d" i))
| Unix.WSIGNALED i -> !: (mkERROR (Printf.sprintf "signaled: %d" i))
| Unix.WSTOPPED i -> !: (mkERROR (Printf.sprintf "stopped: %d" i))
| exception Unix.Unix_error(e,f,a) -> !: (unix_error_to_diagnostic e f a))),
DocAbove);
LPDoc " -- Debugging --";
MLCode(Pred("term_to_string",
In(any, "T",
Out(string, "S",
Easy "prints T to S")),
(fun t _ ~depth ->
let b = Buffer.create 1024 in
let fmt = Format.formatter_of_buffer b in
Format.fprintf fmt "%a" (RawPp.term depth) t ;
Format.pp_print_flush fmt ();
!:(Buffer.contents b))),
DocAbove);
]
;;
(** Standard lambda Prolog built-in ************************************** *)
let lp_builtins = let open BuiltIn in let open BuiltInData in [
LPDoc "== Lambda Prolog builtins =====================================";
LPDoc " -- Extra I/O --";
MLCode(Pred("open_string",
In(string, "DataIn",
Out(in_stream, "InStream",
Easy "opens DataIn as an input stream")),
(fun data _ ~depth ->
try
let filename, outch = Filename.open_temp_file "elpi" "tmp" in
output_string outch data;
close_out outch ;
let v = open_in filename in
Sys.remove filename ;
!:(v,"<string>")
with Sys_error msg -> error msg)),
DocAbove);
MLCode(Pred("lookahead",
In(in_stream, "InStream",
Out(string, "NextChar",
Easy "peeks one byte from InStream")),
(fun (i,_) _ ~depth ->
try
let pos = pos_in i in
let c = input_char i in
Stdlib.seek_in i pos;
!:(String.make 1 c)
with
| End_of_file -> !:""
| Sys_error msg -> error msg)),
DocAbove);
LPDoc " -- Hacks --";
MLCode(Pred("string_to_term",
In(string, "S",
Out(any, "T",
Full(ContextualConversion.unit_ctx, "parses a term T from S"))),
(fun text _ ~depth () () state ->
try
let state, t = Quotation.term_at ~depth state text in
state, !:t, []
with
| Parse.ParseError _ -> raise No_clause)),
DocAbove);
MLCode(Pred("readterm",
In(in_stream, "InStream",
Out(any, "T",
Full(ContextualConversion.unit_ctx, "reads T from InStream, ends with \\n"))),
(fun (i,source_name) _ ~depth () () state ->
try
let text = input_line i in
let state, t = Quotation.term_at ~depth state text in
state, !:t, []
with
| Sys_error msg -> error msg
| Parse.ParseError _ -> raise No_clause)),
DocAbove);
LPCode "pred printterm i:out_stream, i:A.";
LPCode "printterm S T :- term_to_string T T1, output S T1.";
LPCode "pred read o:A.";
LPCode "read S :- flush std_out, input_line std_in X, string_to_term X S.";
]
;;
(** ELPI specific built-in ************************************************ *)
let elpi_builtins = let open BuiltIn in let open BuiltInData in let open ContextualConversion in [
LPDoc "== Elpi builtins =====================================";
MLCode(Pred("dprint",
VariadicIn(unit_ctx, !> any, "prints raw terms (debugging)"),
(fun args ~depth _ _ state ->
Format.fprintf Format.std_formatter "@[<hov 1>%a@]@\n%!"
(RawPp.list (RawPp.Debug.term depth) " ") args ;
state, ())),
DocAbove);
MLCode(Pred("print",
VariadicIn(unit_ctx, !> any,"prints terms"),
(fun args ~depth _ _ state ->
Format.fprintf Format.std_formatter "@[<hov 1>%a@]@\n%!"
(RawPp.list (RawPp.term depth) " ") args ;
state, ())),
DocAbove);
LPCode {|% Deprecated, use trace.counter
pred counter i:string, o:int.
counter C N :- trace.counter C N.|};
MLCode(Pred("quote_syntax",
In(string, "FileName",
In(string, "QueryText",
Out(list (poly "A"), "QuotedProgram",
Out(poly "A", "QuotedQuery",
Full (unit_ctx, "quotes the program from FileName and the QueryText. "^
"See elpi-quoted_syntax.elpi for the syntax tree"))))),
(fun f s _ _ ~depth _ _ state ->
let elpi =
Setup.init
~builtins:[BuiltIn.declare ~file_name:"(dummy)" []]
~file_resolver:(Parse.std_resolver ~paths:[] ())
() in
try
let ap = Parse.program ~elpi ~files:[f] in
let loc = Ast.Loc.initial "(quote_syntax)" in
let aq = Parse.goal ~elpi ~loc ~text:s in
let p = Compile.(program ~flags:default_flags ~elpi [ap]) in
let q = API.Compile.query p aq in
let state, qp, qq = Quotation.quote_syntax_runtime state q in
state, !: qp +! qq, []
with Parse.ParseError (_,m) | Compile.CompileError (_,m) ->
Printf.eprintf "%s\n" m;
raise No_clause)),
DocAbove);
MLData loc;
MLCode(Pred("loc.fields",
In(loc, "Loc",
Out(string, "File",
Out(int, "StartChar",
Out(int, "StopChar",
Out(int, "Line",
Out(int, "LineStartsAtChar",
Easy "Decomposes a loc into its fields")))))),
(fun { source_name; source_start; source_stop; line; line_starts_at; } _ _ _ _ _ ~depth:_ ->
!: source_name +! source_start +! source_stop +! line +! line_starts_at )),
DocAbove);
LPDoc "== Regular Expressions =====================================";
MLCode(Pred("rex.match",
In(string, "Rex",
In(string, "Subject",
Easy ("checks if Subject matches Rex. "^
"Matching is based on OCaml's Str library"))),
(fun rex subj ~depth ->
let rex = Str.regexp rex in
if Str.string_match rex subj 0 then () else raise No_clause)),
DocAbove);
MLCode(Pred("rex.replace",
In(string, "Rex",
In(string, "Replacement",
In(string, "Subject",
Out(string, "Out",
Easy ("Out is obtained by replacing all occurrences of Rex with "^
"Replacement in Subject. See also OCaml's Str.global_replace"))))),
(fun rex repl subj _ ~depth ->
let rex = Str.regexp rex in
!:(Str.global_replace rex repl subj))),
DocAbove);
MLCode(Pred("rex.split",
In(string, "Rex",
In(string, "Subject",
Out(list string, "Out",
Easy ("Out is obtained by splitting Subject at all occurrences of Rex. "^
"See also OCaml's Str.split")))),
(fun rex subj _ ~depth ->
let rex = Str.regexp rex in
!:(Str.split rex subj))),
DocAbove);
LPCode {|% Deprecated, use rex.match
pred rex_match i:string, i:string.
rex_match Rx S :- rex.match Rx S.|};
LPCode {|% Deprecated, use rex.replace
pred rex_replace i:string, i:string, i:string, o:string.
rex_replace Rx R S O :- rex.replace Rx R S O.|};
LPCode {|% Deprecated, use rex.split
pred rex_split i:string, i:string, o:list string.
rex_split Rx S L :- rex.split Rx S L.|};
]
;;
(** ELPI specific NON-LOGICAL built-in *********************************** *)
let ctype = AlgebraicData.declare {
AlgebraicData.ty = TyName "ctyp";
doc = "Opaque ML data types";
pp = (fun fmt cty -> Format.fprintf fmt "%s" cty);
constructors = [
K("ctype","",A(BuiltInData.string,N),B (fun x -> x), M (fun ~ok ~ko x -> ok x))
]
} |> ContextualConversion.(!<)
let safe = OpaqueData.declare {
OpaqueData.name = "safe";
pp = (fun fmt (id,l) ->
Format.fprintf fmt "[safe %d: %a]" id
(RawPp.list (fun fmt (t,d) -> RawPp.term d fmt t) ";") !l);
compare = (fun (id1, _) (id2,_) -> Util.Int.compare id1 id2);
hash = (fun (id,_) -> id);
hconsed = false;
doc = "Holds data across bracktracking; can only contain closed terms";
constants = [];
}
let safeno = ref 0
let fresh_int = ref 0
(* factor the code of name and constant *)
let name_or_constant name condition = (); fun x out ~depth _ _ state ->
let len = List.length out in
if len != 0 && len != 2 then
type_error (name^" only supports 1 or 3 arguments");
state,
match x with
| NoData -> raise No_clause
| Data x ->
match look ~depth x with
| Const n when condition n ->
if out = [] then !: x +? None
else !: x +! [Some x; Some mkNil]
| App(n,y,ys) when condition n ->
if out = [] then !: x +? None
else !: x +! [Some (mkConst n); Some (list_to_lp_list (y::ys))]
| UnifVar _ ->
(* We build the application *)
begin match out with
| [] -> raise No_clause
| [Data hd; Data args] ->
begin match look ~depth hd, lp_list_to_list ~depth args with
| Const n, [] when condition n ->
!: (mkConst n) +! [Some hd; Some args]
| Const n, x :: xs when condition n ->
!: (mkApp n x xs) +! [Some hd; Some args]
| _ -> raise No_clause end
| _ -> raise No_clause
end
| _ -> raise No_clause
;;
let rec same_term ~depth t1 t2 =
match look ~depth t1, look ~depth t2 with
| UnifVar(b1,xs), UnifVar(b2,ys) -> FlexibleData.Elpi.equal b1 b2 && same_term_list ~depth xs ys
| App(c1,x,xs), App(c2,y,ys) -> c1 == c2 && same_term ~depth x y && same_term_list ~depth xs ys
| Const c1, Const c2 -> c1 == c2
| Cons(x,xs), Cons(y,ys) -> same_term ~depth x y && same_term ~depth xs ys
| Nil, Nil -> true
| Lam x, Lam y -> same_term ~depth:(depth+1) x y
| Builtin(c1,xs),Builtin(c2,ys) -> c1 == c2 && same_term_list ~depth xs ys
| CData d1, CData d2 -> RawOpaqueData.equal d1 d2
| _ -> false
and same_term_list ~depth xs ys =
match xs, ys with
| [], [] -> true
| x::xs, y::ys -> same_term ~depth x y && same_term_list ~depth xs ys
| _ -> false
let elpi_nonlogical_builtins = let open BuiltIn in let open BuiltInData in let open ContextualConversion in [
LPDoc "== Elpi nonlogical builtins =====================================";
MLData ctype;
MLCode(Pred("var",
InOut(ioarg_any, "V",
VariadicInOut(unit_ctx, !> (ioarg_any),"checks if the term V is a variable. When used with tree arguments it relates an applied variable with its head and argument list.")),
(fun x out ~depth _ _ state ->
let len = List.length out in
if len != 0 && len != 2 then
type_error ("var only supports 1 or 3 arguments");
let is_var x =
match look ~depth x with
| UnifVar(v,a) -> v,a
| _ -> raise No_clause in
state,
match x, out with
| Data x, [] -> let _ = is_var x in ?: None +? None
| Data x, [NoData; NoData] -> let _ = is_var x in ?: None +? None
| Data x, [NoData; Data args] -> let _, a = is_var x in ?: None +! [None; Some (list_to_lp_list a)]
| Data x, [Data var; NoData] -> let v, _ = is_var x in ?: None +! [Some (mkUnifVar v ~args:[] state); None]
| Data x, [Data y; Data args] ->
let vx, ax = is_var x in
let vy, ay = is_var y in
begin match look ~depth args with
| UnifVar _ ->
?: None +! [Some (mkUnifVar vx ~args:[] state); Some (list_to_lp_list ax)]
| _ ->
!: (mkUnifVar vy ~args:(ay @ lp_list_to_list ~depth args) state)
+! [Some (mkUnifVar vx ~args:[] state); Some (list_to_lp_list ax)]
end
| _ -> raise No_clause)),
DocAbove);
MLCode(Pred("prune",
Out(any, "V",
In(list any, "L",
Full (unit_ctx, "V is pruned to L (V is unified with a variable that only sees the list of names L)"))),
(fun _ l ~depth _ _ state ->
if not (List.for_all (fun t -> match look ~depth t with
| Const n -> n >= 0
| _ -> false) l) then
type_error ("prune only accepts a list of names");
let state, u = FlexibleData.Elpi.make state in
state, !: (mkUnifVar u ~args:l state), [])),
DocAbove);
MLCode(Pred("distinct_names",
In(list any, "L",
Easy "checks if L is a list of distinct names. If L is the scope of a unification variable (its arguments, as per var predicate) then distinct_names L checks that such variable is in the Miller pattern fragment (L_\\lambda)"),
(fun l ~depth ->
let _ = List.fold_left (fun seen t ->
match look ~depth t with
| Const n when n >= 0 ->
if not (Util.IntSet.mem n seen) then Util.IntSet.add n seen
else raise No_clause
| _ -> raise No_clause) Util.IntSet.empty l in
())),
DocAbove);
MLCode(Pred("same_var",
In(poly "A", "V1",
In(poly "A", "V2",
Easy "checks if the two terms V1 and V2 are the same variable, ignoring the arguments of the variables")),
(fun t1 t2 ~depth ->
match look ~depth t1, look ~depth t2 with
| UnifVar(p1,_), UnifVar (p2,_) when FlexibleData.Elpi.equal p1 p2 -> ()
| _,_ -> raise No_clause)),
DocAbove);
MLCode(Pred("same_term",
In(poly "A", "T1",
In(poly "A", "T2",
Easy {|checks if the two terms T1 and T2 are syntactically equal (no unification). It behaves differently than same_var since it recursively compares the arguments of the variables|})),
(fun t1 t2 ~depth ->
if same_term ~depth t1 t2 then () else raise No_clause)),
DocAbove);
LPCode {|
% Infix notation for same_term
pred (==) i:A, i:A.
X == Y :- same_term X Y.
|};
MLCode(Pred("cmp_term",
In(any, "A",
In(any, "B",
Out(cmp,"Cmp",
Easy "Compares A and B. Only works if A and B are ground."))),
(fun t1 t2 _ ~depth -> !: (cmp_term ~depth t1 t2))),
DocAbove);
MLCode(Pred("name",
InOut(ioarg_any, "T",
VariadicInOut(unit_ctx, !> (ioarg any),"checks if T is a eigenvariable. When used with tree arguments it relates an applied name with its head and argument list.")),
(name_or_constant "name" (fun x -> x >= 0))),
DocAbove);
MLCode(Pred("constant",
InOut(ioarg_any, "T",
VariadicInOut(unit_ctx, !> (ioarg any),"checks if T is a (global) constant. When used with tree arguments it relates an applied constant with its head and argument list.")),
(name_or_constant "constant" (fun x -> x < 0))),
DocAbove);
MLCode(Pred("names",
Out(list any, "list of eigenvariables in order of age (young first)",
Easy "generates the list of eigenvariable"),
(* XXX 4.06: (fun _ ~depth -> !:(List.init depth mkConst))), *)
(fun _ ~depth ->
let rec list_init i n f =
if i >= n then [] else
f i :: list_init (i+1) n f in
!:(list_init 0 depth mkConst))),
DocNext);
MLCode(Pred("occurs",
In(any, "an atom, that is a global constant or a bound name (aka eigenvariable)",
In(any, "a term",
Easy "checks if the atom occurs in the term")),
(fun t1 t2 ~depth ->
let occurs_in t2 t =
match look ~depth t with
| Const n -> occurs n depth t2
| _ -> error "The second argument of occurs must be an atom" in
if occurs_in t2 t1 then () else raise No_clause)),
DocNext);
MLCode(Pred("closed_term",
Out(any, "T",
Full (unit_ctx, "unify T with a variable that has no eigenvariables in scope")),
(fun _ ~depth _ _ state ->
let state, k = FlexibleData.Elpi.make state in
state, !:(mkUnifVar k ~args:[] state), [])),
DocAbove);
MLCode(Pred("ground_term",
In(any, "T",
Easy ("Checks if T contains unification variables")),