Source file acg_lexicon.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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
open UtilsLib
open Containers
open Logic
open Abstract_syntax
open Lambda
open Signature
module Log = Xlog.Make (struct
let name = "Acg_lexicon"
end)
module MagicLog = Xlog.Make (struct
let name = "Acg_lexicon/Magic"
end)
module ParsingLog = Xlog.Make (struct
let name = "Acg_lexicon/Parsing_check"
end)
module Data_Lexicon = struct
exception Duplicate_type_interpretation
exception Duplicate_constant_interpretation
exception Not_almost_linear
module Pair = struct
type kind = Type | Cst
type t = string * kind
let compare (s, k) (s', k') =
match (k, k') with
| Type, Cst -> -1
| Cst, Type -> 1
| _, _ -> String.compare s s'
end
module Dico = Map.Make (Pair)
type resumptions = int SharedForest.SharedForest.Resumptions.resumptions * int SharedForest.SharedForest.forest * (Data_Signature.term * Data_Signature.stype)
type interpretation =
| Type of (Abstract_syntax.location * Lambda.stype)
| Constant of (Abstract_syntax.location * Lambda.term)
let pp_interpretation fun_type_from_id i sg fmt abstract_type_or_cst_id =
let pp_term = Data_Signature.pp_term sg in
let pp_type = Data_Signature.pp_type sg in
match i with
| Type (_, t) -> pp_type fmt t
| Constant (_, c) ->
let eta_long =
Data_Signature.eta_long_form c
(fun_type_from_id abstract_type_or_cst_id)
sg
in
Format.fprintf fmt "%a [eta-long form: %a {%s}]" pp_term c pp_term
eta_long
(Lambda.raw_to_string eta_long)
module Datalog = DatalogLib.Datalog.Datalog
module DatalogRule = Datalog.Rule
module DatalogPredMap = Datalog.Predicate.PredMap
module DatalogAbstractSyntax = DatalogLib.Datalog_AbstractSyntax.AbstractSyntax
module ASPred = DatalogAbstractSyntax.Predicate
module ASProg = DatalogAbstractSyntax.Program
module ASRule = DatalogAbstractSyntax.Rule
module RuleToCstMap = Utils.IntMap
type datalog_correspondance = {
prog : Datalog.Program.program;
magic_programs :
(Datalog.Program.program * MagicRewriting.Rewriting.magic_context)
MagicRewriting.Rewriting.QueryMap.t
option;
rule_to_cst : Lambda.term RuleToCstMap.t;
cst_to_rule : int Utils.IntMap.t;
generated_symbols : string Utils.IntMap.t * Utils.StringSet.t;
}
type 'a build =
| Interpret of (string * string)
| Compose of ('a list)
[@@@warning "-69"]
type t = {
name : string * Abstract_syntax.location;
dico : interpretation Dico.t;
syntax_dico : Abstract_syntax.lex_entry Dico.t option;
non_linear_interpretation : bool;
abstract_sig : Data_Signature.t;
object_sig : Data_Signature.t;
datalog_prog : datalog_correspondance option;
build : string build;
timestamp : float;
is_almost_linear : bool;
}
type dumped_t = {
dumped_name : string * Abstract_syntax.location;
dumped_dico : interpretation Dico.t;
dumped_syntax_dico : Abstract_syntax.lex_entry Dico.t option;
dumped_non_linear_interpretation : bool;
dumped_abstract_sig : (string * Data_Signature.id) * string;
dumped_object_sig : (string * Data_Signature.id) * string;
dumped_datalog_prog : datalog_correspondance option;
dumped_build : string build;
dumped_timestamp : float;
dumped_is_almost_linear : bool;
}
let name_of_dumped l = fst (l.dumped_name)
let prepare_dump (l:t) =
{
dumped_name = l.name;
dumped_dico = l.dico;
dumped_syntax_dico = l.syntax_dico;
dumped_non_linear_interpretation = l.non_linear_interpretation;
dumped_abstract_sig = Data_Signature.full_name l.abstract_sig;
dumped_object_sig = Data_Signature.full_name l.object_sig;
dumped_datalog_prog= l.datalog_prog;
dumped_build = l.build;
dumped_timestamp = l.timestamp;
dumped_is_almost_linear = l.is_almost_linear;
}
let recover_from_dump ~filename ~get_sig l =
let check_and_get_sig ((sg_name, sg_id), _) =
let sg = (get_sig sg_name) in
let sg_name_id, sg_filename = (Data_Signature.full_name sg) in
if sg_name_id = (sg_name, sg_id) then
sg
else
Errors.(LexiconErrors.emit (Lexicon_l.NotCompatibleSignature (fst l.dumped_name, filename, sg_name, sg_filename))) in
{
name = l.dumped_name;
dico = l.dumped_dico;
syntax_dico = l.dumped_syntax_dico;
non_linear_interpretation = l.dumped_non_linear_interpretation;
abstract_sig = check_and_get_sig l.dumped_abstract_sig;
object_sig = check_and_get_sig l.dumped_object_sig;
datalog_prog= l.dumped_datalog_prog;
build = l.dumped_build;
timestamp = l.dumped_timestamp;
is_almost_linear = l.dumped_is_almost_linear;
}
[@@@warning "+69"]
type dependency =
| Signatures of (string * string)
| Lexicons of string list
type parsing = Unavailable | Available_with_magic | Available_wo_magic
let get_dependencies lex =
match lex.build with
| Interpret s -> Signatures s
| Compose l -> Lexicons l
let pp_lex fmt lex =
let name, _ = lex.name in
Utils.lex_pp fmt name
let short_pp fmt
({ abstract_sig = abs_sg; object_sig = obj_sg; _ } as lex) =
Format.fprintf fmt "lexicon@ %a(%a):@ %a" pp_lex lex
Utils.sig_pp (fst (Data_Signature.name abs_sg))
Utils.sig_pp (fst (Data_Signature.name obj_sg))
let name { name = n; _ } = n
let get_sig { abstract_sig = abs; object_sig = obj; _ } = (abs, obj)
let empty ?(non_linear = false) ~abs ~obj name =
let prog =
if Data_Signature.is_2nd_order abs then
Some
{
prog = Datalog.Program.empty;
magic_programs = None;
rule_to_cst = RuleToCstMap.empty;
cst_to_rule = Utils.IntMap.empty;
generated_symbols = (Utils.IntMap.empty, Utils.StringSet.empty);
}
else None
in
{
name;
dico = Dico.empty;
syntax_dico = Some Dico.empty;
abstract_sig = abs;
object_sig = obj;
datalog_prog = prog;
non_linear_interpretation = non_linear;
build = Data_Signature.(Interpret (fst (name abs), fst (name obj)));
timestamp = Unix.time ();
is_almost_linear = true;
}
let is_linear { non_linear_interpretation; _ } = not non_linear_interpretation
let emit_missing_inter lex lst =
let lex_name, loc = name lex in
let abs_name, _ = Data_Signature.name lex.abstract_sig in
Errors.(LexiconErrors.emit (Lexicon_l.MissingInterpretations (lex_name, abs_name, lst)) ~loc)
let rec interpret_type abs_ty ({ abstract_sig = abs_sg; dico; _ } as lex) =
match abs_ty with
| Lambda.Atom i -> (
let () =
assert (
snd (Data_Signature.id_to_string abs_sg i)
= Format.asprintf "%a" (Data_Signature.pp_type abs_sg) abs_ty)
in
let abs_ty_as_str = snd (Data_Signature.id_to_string abs_sg i) in
match Dico.find (abs_ty_as_str, Pair.Type) dico with
| Type (_, obj_ty) -> Data_Signature.expand_type obj_ty lex.object_sig
| Constant _ -> failwith "Bug"
| exception Not_found -> emit_missing_inter lex [ abs_ty_as_str ])
| Lambda.DAtom i ->
interpret_type (Data_Signature.unfold_type_definition i abs_sg) lex
| Lambda.LFun (ty1, ty2) ->
if lex.non_linear_interpretation then
Lambda.Fun (interpret_type ty1 lex, interpret_type ty2 lex)
else Lambda.LFun (interpret_type ty1 lex, interpret_type ty2 lex)
| Lambda.Fun (ty1, ty2) ->
Lambda.Fun (interpret_type ty1 lex, interpret_type ty2 lex)
| _ -> failwith "Not yet implemented"
let rec interpret_term abs_t ({ abstract_sig = abs_sg; dico; _ } as lex) =
match abs_t with
| Lambda.Var _ -> abs_t
| Lambda.LVar i ->
if lex.non_linear_interpretation then Lambda.Var i else abs_t
| Lambda.Const _ -> (
let abs_term_as_str =
Format.asprintf "%a" (Data_Signature.pp_term abs_sg) abs_t
in
match Dico.find (abs_term_as_str, Pair.Cst) dico with
| Constant (_, obj_t) -> obj_t
| Type _ -> failwith "Bug"
| exception Not_found -> emit_missing_inter lex [ abs_term_as_str ])
| Lambda.DConst i ->
interpret_term (Data_Signature.unfold_term_definition i abs_sg) lex
| Lambda.Abs (x, t) -> Lambda.Abs (x, interpret_term t lex)
| Lambda.LAbs (x, t) ->
if lex.non_linear_interpretation then
Lambda.Abs (x, interpret_term t lex)
else Lambda.LAbs (x, interpret_term t lex)
| Lambda.App (t, u) ->
Lambda.App (interpret_term t lex, interpret_term u lex)
| _ -> failwith "Not yet implemented"
let interpret t ty lex =
let t_interpretation = interpret_term t lex in
let t_interpretation =
Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i lex.object_sig)
t_interpretation
in
let ty_interpretation = interpret_type ty lex in
(t_interpretation, ty_interpretation)
let pp fmt
({ dico = d; abstract_sig = abs_sg; object_sig = obj_sg; _ }
as lex) =
let pp_dico fmt dico =
Dico.iter
(fun (id, _) i ->
Format.fprintf fmt "@[<hv 2>%s :=@ %a;@]@;" id
(pp_interpretation
(fun id ->
interpret_type (Data_Signature.type_of_constant id abs_sg) lex)
i obj_sg)
id)
dico
in
let () = Format.fprintf fmt "@[<hv 2>@[" in
let () = short_pp fmt lex in
let () =
Format.fprintf fmt " =@]@,@[<v>%a@]@," pp_dico d
in
let () = Format.fprintf fmt "-----------------------------------@," in
match lex.datalog_prog with
| None ->
Format.fprintf fmt
"@[This@ lexicon@ was@ not@ recognized@ as@ having@ a@ 2nd-order@ \
abstract@ signature@]@]"
| Some { prog = p; _ } ->
Format.fprintf fmt
"@[This@ lexicon@ is@ recognized@ as@ having@ a@ 2nd-order@ abstract@ \
signature.@ The@ associated@ datalog@ program@ is:@,\
@[<v> @[%a@]@]" (DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true)
(Datalog.Program.to_abstract p)
module Reduction = Reduction.Make (Data_Signature)
let generate_unambiguous_obj_sym lex cst (map, syms) =
let rec disambiguate id l_s =
let () = Log.debug (fun m -> m "Testing \"%s\"" l_s) in
if
Data_Signature.is_type ~atomic:true l_s lex.abstract_sig
|| Utils.StringSet.mem l_s syms
||
match Data_Signature.is_constant l_s lex.object_sig with
| true, Some (_, false, _) -> true
| _, _ -> false
then disambiguate id (Printf.sprintf "%s__" l_s)
else
let () = Log.debug (fun m -> m "Succeeded!") in
(l_s, (Utils.IntMap.add id l_s map, Utils.StringSet.add l_s syms))
in
let cst_name =
Format.asprintf "%a" (Data_Signature.pp_term lex.object_sig) cst
in
if Data_Signature.is_type ~atomic:true cst_name lex.abstract_sig then
let () =
Log.debug (fun m ->
m "Needs to define a new symbol instead of \"%s\"" cst_name)
in
let new_sym =
Printf.sprintf "%s__%s__" cst_name
(fst (Data_Signature.name lex.object_sig))
in
let cst_id =
match cst with
| Lambda.Const i -> i
| _ ->
failwith
"Bug: Predicates should be build only for declared constants"
in
disambiguate cst_id new_sym
else
(cst_name, (map, syms))
let add_rule_for_cst_in_prog name duplicated abs_type interpreted_term lex
{ prog; magic_programs; rule_to_cst; cst_to_rule; generated_symbols } =
let interpreted_type = interpret_type abs_type lex in
let eta_long_term =
Data_Signature.eta_long_form interpreted_term interpreted_type
lex.object_sig
in
let pp_obj_term = Data_Signature.pp_term lex.object_sig in
let pp_obj_type = Data_Signature.pp_type lex.object_sig in
Log.info (fun m ->
m "term: %a: %a" pp_obj_term interpreted_term pp_obj_type
interpreted_type);
Log.info (fun m -> m "eta-long form: %a" pp_obj_term eta_long_term);
Log.info (fun m ->
m "eta-long form (as caml term): %s" (Lambda.raw_to_caml eta_long_term));
Log.info (fun m ->
m "Datalog rule addition: lexicon \"%s\", constant \"%s: %a\""
(fst lex.name) name
(Data_Signature.pp_type lex.abstract_sig)
abs_type);
Log.info (fun m ->
m "mapped to \"%a: %a\"" pp_obj_term eta_long_term pp_obj_type
interpreted_type);
let obj_princ_type, obj_typing_env =
TypeInference.Type.inference eta_long_term
in
Log.info (fun m ->
m "Interpreting \"%s\" as \"%a=%s\" with principle type: \"%s\"" name
(Data_Signature.pp_term lex.object_sig)
eta_long_term
(Lambda.raw_to_caml eta_long_term)
(Lambda.raw_type_to_string obj_princ_type));
Log.info (fun m ->
let pp_typing_env fmt env =
Utils.IntMap.iter
(fun k (t, ty) ->
Format.fprintf fmt "@[%d --> %s : %s@]" k (Lambda.raw_to_string t)
(Lambda.raw_type_to_string ty))
env
in
m "In the context of:@,@[<v> @[%a@]@]" pp_typing_env obj_typing_env);
let rule, new_prog, new_generated_symbols =
Reduction.generate_and_add_rule ~abs_cst:(name, abs_type) ~obj_princ_type
~obj_typing_env ~abs_sig:lex.abstract_sig ~obj_sig:lex.object_sig
~update_fct:(generate_unambiguous_obj_sym lex)
~syms:generated_symbols prog
in
let cst_id, _ = Data_Signature.find_term name lex.abstract_sig in
let cst_id_as_int =
match cst_id with
| Lambda.Const i -> i
| _ ->
failwith
"Bug: Trying to add a rule that does not correspond to a constant"
in
let new_prog' =
if duplicated then
Datalog.Program.remove_rule
(Utils.IntMap.find cst_id_as_int cst_to_rule)
rule.DatalogAbstractSyntax.Rule.lhs
.DatalogAbstractSyntax.Predicate.p_id new_prog
else new_prog
in
{
prog = new_prog';
magic_programs;
rule_to_cst =
RuleToCstMap.add rule.DatalogAbstractSyntax.Rule.id cst_id rule_to_cst;
cst_to_rule =
Utils.IntMap.add cst_id_as_int rule.DatalogAbstractSyntax.Rule.id
cst_to_rule;
generated_symbols = new_generated_symbols;
}
let insert e ({ dico = d; _ } as lex) =
match e with
| Abstract_syntax.Type (id, loc, ty) ->
let interpreted_type = Data_Signature.convert_type ty lex.object_sig in
{
lex with
dico = Dico.add (id, Pair.Type) (Type (loc, interpreted_type)) d;
}
| Abstract_syntax.Constant (id, loc, t) ->
let abs_type =
Data_Signature.expand_type
(Data_Signature.type_of_constant id lex.abstract_sig)
lex.abstract_sig
in
let interpreted_type = interpret_type abs_type lex in
let unfold i = Data_Signature.unfold_term_definition i lex.object_sig in
let interpretation, is_almost_linear =
Data_Signature.typecheck t interpreted_type lex.object_sig
in
let () =
if not is_almost_linear then
Logs.warn (fun m ->
m
"Because@ of@ \"%s :=@ %a :@ %a\",@ the@ lexicon@ \"%a\"@ \
is@ not@ almost@ linear."
id
(Data_Signature.pp_term lex.object_sig)
interpretation
(Data_Signature.pp_type lex.object_sig)
interpreted_type
Utils.lex_pp
(let name, _ = lex.name in
name))
in
let interpreted_term =
Lambda.normalize ~id_to_term:unfold interpretation
in
let prog =
match (lex.datalog_prog, is_almost_linear) with
| None, _ -> None
| _, false -> None
| Some p, true ->
let duplicated_entry = Dico.mem (id, Pair.Cst) d in
let new_prog =
add_rule_for_cst_in_prog id duplicated_entry abs_type
(Data_Signature.expand_term interpreted_term lex.object_sig)
lex p
in
Some { new_prog with magic_programs = None }
in
{
lex with
dico = Dico.add (id, Pair.Cst) (Constant (loc, interpreted_term)) d;
datalog_prog = prog;
is_almost_linear = lex.is_almost_linear && is_almost_linear;
}
let rebuild_prog lex =
match lex.datalog_prog with
| None -> lex
| Some _ -> (
try
let new_prog =
Dico.fold
(fun (id, _) inter acc ->
match inter with
| Type (_, _) -> acc
| Constant (_, t) ->
add_rule_for_cst_in_prog id false
(Data_Signature.expand_type
(Data_Signature.type_of_constant id lex.abstract_sig)
lex.abstract_sig)
t lex acc)
lex.dico
{
prog = Datalog.Program.empty;
magic_programs = None;
rule_to_cst = RuleToCstMap.empty;
cst_to_rule = Utils.IntMap.empty;
generated_symbols = Utils.IntMap.empty, Utils.StringSet.empty;
}
in
{ lex with datalog_prog = Some new_prog }
with Not_almost_linear -> { lex with is_almost_linear = false })
let parse ~alt_max ?(magic = true) (term, term_type) dist_type lex =
let dist_type = Data_Signature.expand_type dist_type lex.abstract_sig in
let term_type = Data_Signature.expand_type term_type lex.object_sig in
let term =
Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i lex.object_sig)
(Data_Signature.expand_term term lex.object_sig)
in
match
(lex.datalog_prog, dist_type)
with
| None, _ ->
let () =
Logs.warn (fun m ->
m "Parsing@ is@ not@ implemented@ for@ non@ 2nd-order@ ACG.")
in
SharedForest.SharedForest.Resumptions.empty ~alt_max, [], ( term, dist_type)
| ( Some { prog; magic_programs = Some q_to_prog_map; generated_symbols; _ },
(Lambda.Atom _ as dist_type) )
when magic = true ->
Log.info (fun m -> m "Before parsing. Program is currently:@,@[<v> @[%a@]@]" (DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true) (Datalog.Program.to_abstract prog));
let dist_type_image = interpret_type dist_type lex in
if dist_type_image <> term_type then
let obj_term_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) term_type in
let abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.abstract_sig) dist_type in
let interpreted_abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) dist_type_image in
let lex_name = Format.dprintf "%a" pp_lex lex in
Errors.(CmdErrors.emit (Cmd_l.TypeMismatch (obj_term_type_s, abs_dist_type_s, interpreted_abs_dist_type_s, lex_name)))
else
let () = Log.info (fun m ->
m "Term for the query: %a"
(Data_Signature.pp_term lex.object_sig)
term) in
let obj_term =
Data_Signature.eta_long_form term dist_type_image lex.object_sig
in
let obj_princ_type, obj_typing_env =
TypeInference.Type.inference obj_term
in
Log.debug (fun m ->
m "Going to set a query for the distinguised type \"%a(%s)\""
(Data_Signature.pp_type lex.abstract_sig)
dist_type
(Lambda.raw_type_to_string dist_type));
Log.debug (fun m ->
m "whose image is \"%a(%s)\""
(Data_Signature.pp_type lex.object_sig)
dist_type_image
(Lambda.raw_type_to_string dist_type_image));
Log.debug (fun m ->
m "resulting int the principle type \"%s\""
(Lambda.raw_type_to_string obj_princ_type));
let original_query, original_queried_program =
Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
~obj_sig:lex.object_sig ~syms:generated_symbols
in
let () = Log.debug (fun m -> m "Done (query)") in
let bfs, _ =
MagicRewriting.Adornment.adornment ~bound_variables:ASPred.TermSet.empty original_query in
let () = Log.debug (fun m -> m "Done (adornment of the query)") in
let magic_program, magic_context =
match
MagicRewriting.Rewriting.QueryMap.find_opt
(original_query.ASPred.p_id, bfs)
q_to_prog_map
with
| None -> failwith "Bug: no magic rewritten program"
| Some (p, c) ->
let abstract_program = Datalog.Program.to_abstract p in
let () =
Log.debug (fun m ->
m "Found the following magic program for the query '%s':@,@[<v> @[%a@]@]"
(MagicRewriting.Adornment.adorned_predicate_to_string ~pred_table:prog.Datalog.Program.pred_table (original_query, bfs))
(ASProg.pp ~with_position:false ~with_id:true)
abstract_program)
in
let () =
Log.debug (fun m ->
m "It was built from the following unique binding program:@,@[<v> @[%a@]@]"
(ASProg.pp ~with_position:false ~with_id:true)
c.MagicRewriting.Rewriting.unique_binding_program)
in
( Datalog.Program.
{ p with const_table = original_queried_program.const_table },
c )
in
let query, temp_magic_prog =
Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
~obj_typing_env ~dist_type ~adornment:bfs magic_program
~abs_sig:lex.abstract_sig ~obj_sig:lex.object_sig ~syms:generated_symbols
in
let temp_magic_prog' =
MagicRewriting.Magic.query_to_seed_concrete query temp_magic_prog
in
let () =
Log.info (fun m ->
m "Going to solve the query: \"%a\" with the program:@,@[<v> @[%a@]@]"
(DatalogAbstractSyntax.Predicate.pp
temp_magic_prog'.Datalog.Program.pred_table
temp_magic_prog'.Datalog.Program.const_table) query
(DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true)
(Datalog.Program.to_abstract temp_magic_prog'))
in
let parse_time_start = Timer.top () in
let _derived_facts, magic_derivations =
Datalog.Program.seminaive temp_magic_prog'
in
let parse_time_end = Timer.top () in
let () =
Log.debug (fun m ->
m "I could derive the following facts:@,@[ @[<v>%a@]@]"
(Datalog.Predicate.pp_facts
temp_magic_prog'.Datalog.Program.pred_table
temp_magic_prog'.Datalog.Program.const_table) _derived_facts)
in
let () =
Log.debug (fun m ->
m "With the following derivations:@,@[<v> @[%a@]@]"
(Datalog.Predicate.pp_facts_from_premises ~with_id:true
temp_magic_prog'.Datalog.Program.pred_table
temp_magic_prog'.Datalog.Program.const_table)
magic_derivations)
in
let () =
Log.debug (fun m ->
m "Mapping of unique binding predicates to original program predicates:@[ @[<v>%a@]@]@]"
(fun fmt unadorned_predicats ->
ASPred.PredIdMap.iter
(fun p_id_ub p_id_orig ->
Format.fprintf
fmt
"@[%a ---> %a@]@,"
(ASPred.pp
~with_id:true
magic_context.MagicRewriting.Rewriting.unique_binding_program.ASProg.pred_table
DatalogLib.Datalog_AbstractSyntax.ConstGen.Table.empty)
ASPred.{ p_id = p_id_ub; arity = 0; arguments = [] }
(ASPred.pp
~with_id:true
original_queried_program.Datalog.Program.pred_table
DatalogLib.Datalog_AbstractSyntax.ConstGen.Table.empty)
ASPred.{ p_id = p_id_orig; arity = 0; arguments = [] })
unadorned_predicats)
magic_context.MagicRewriting.Rewriting.adorn_to_unadorm_pred_ids_map)
in
let derivations, prog_for_building_forest =
let rewritten_derivations =
MagicRewriting.Rewriting.rewrite_derivations magic_derivations
magic_context
in
let () =
Log.debug (fun m ->
m "Rewritten derivations:@,@[<v>@[%a@]@]"
(Datalog.Predicate.pp_facts_from_premises ~with_id:true
original_queried_program.Datalog.Program.pred_table
original_queried_program.Datalog.Program.const_table)
rewritten_derivations)
in
(rewritten_derivations, original_queried_program)
in
let () =
Log.debug (fun m ->
m "Original query (original program): %a"
(ASPred.pp ~with_id:true
original_queried_program.Datalog.Program.pred_table
original_queried_program.Datalog.Program.const_table) original_query)
in
let () =
Log.debug (fun m ->
m "Magic query: %a"
(ASPred.pp ~with_id:true
temp_magic_prog'.Datalog.Program.pred_table
temp_magic_prog'.Datalog.Program.const_table) query)
in
let build_forest_start = Timer.top () in
let parse_forest =
Datalog.Program.build_forest ~query:original_query derivations
prog_for_building_forest
in
let build_forest_end = Timer.top () in
let () =
Logs.app
(fun m -> m "Parsing time: %a"
Timer.diff
(parse_time_end, parse_time_start)) in
let () =
Logs.app
(fun m -> m "Parse forest building time: %a"
Timer.diff
(build_forest_end, build_forest_start)) in
let resumptions =
match parse_forest with
| [] ->
let () = Log.debug (fun m -> m "The shared forest is empty") in
SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)
| [ f ] ->
let () =
Log.debug (fun m -> m "The shared forest is not empty") in
let forest = f in
let () =
Log.debug (fun m ->
m
"The shared forest is: @[%a@]"
(SharedForest.SharedForest.pp_forest Format.pp_print_int)
forest)
in
SharedForest.SharedForest.init ~alt_max (Format.pp_print_int) f, f, (term, dist_type)
| _ -> failwith "Bug: not fully specified query"
in
resumptions
| Some { prog; magic_programs = None; generated_symbols; _ }, (Lambda.Atom _ as dist_type)
| Some { prog; magic_programs = _; generated_symbols; _ }, (Lambda.Atom _ as dist_type) ->
let dist_type_image = interpret_type dist_type lex in
if dist_type_image <> term_type then
let obj_term_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) term_type in
let abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.abstract_sig) dist_type in
let interpreted_abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) dist_type_image in
let lex_name = Format.dprintf "%a" pp_lex lex in
Errors.(CmdErrors.emit (Cmd_l.TypeMismatch (obj_term_type_s, abs_dist_type_s, interpreted_abs_dist_type_s, lex_name)))
else
let term =
Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i lex.object_sig)
(Data_Signature.expand_term term lex.object_sig)
in
Log.info (fun m ->
m "Term for the query: %a"
(Data_Signature.pp_term lex.object_sig) term);
let obj_term =
Data_Signature.eta_long_form term dist_type_image lex.object_sig
in
let obj_princ_type, obj_typing_env =
TypeInference.Type.inference obj_term
in
Log.debug (fun m ->
m "Going to set a query for the distinguised type \"%a(%s)\""
(Data_Signature.pp_type lex.abstract_sig) dist_type
(Lambda.raw_type_to_string dist_type));
Log.debug (fun m ->
m "whose image is \"%a(%s)\""
(Data_Signature.pp_type lex.object_sig) dist_type_image
(Lambda.raw_type_to_string dist_type_image));
Log.debug (fun m ->
m "resulting in the principle type \"%s\""
(Lambda.raw_type_to_string obj_princ_type));
let query, temp_prog =
Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
~obj_sig:lex.object_sig ~syms:generated_symbols
in
let parse_time_start = Timer.top () in
let _, derivations = Datalog.Program.seminaive temp_prog in
let parse_time_end = Timer.top () in
let () =
Log.debug (fun m ->
m "Derivations:@,@[<v>@[%a@]@]"
(Datalog.Predicate.pp_facts_from_premises ~with_id:true
temp_prog.Datalog.Program.pred_table
temp_prog.Datalog.Program.const_table)
derivations)
in
let build_forest_start = Timer.top () in
let parse_forest =
Datalog.Program.build_forest ~query derivations temp_prog
in
let build_forest_end = Timer.top () in
let () =
Logs.app
(fun m -> m "Parsing time: %a"
Timer.diff
(parse_time_end, parse_time_start)) in
let () =
Logs.app
(fun m -> m "Parse forest building time: %a"
Timer.diff
(build_forest_end, build_forest_start)) in
let resumptions =
match parse_forest with
| [] ->
let () = Log.debug (fun m -> m "The shared forest is empty") in
SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)
| [ f ] ->
let () =
Log.debug (fun m -> m "The shared forest is not empty") in
let forest = f in
let () =
Log.debug (fun m ->
m
"The shared forest is:@[%a@]"
(SharedForest.SharedForest.pp_forest Format.pp_print_int)
forest)
in
SharedForest.SharedForest.init ~alt_max (Format.pp_print_int) f, f, (term, dist_type)
| _ -> failwith "Bug: not fully specified query"
in
resumptions
| Some _, _ ->
let () =
Logs.warn (fun m ->
m
"Parsing@ is@ not@ yet@ implemented@ for@ non-atomic@ \
distinguished@ type.")
in
SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)
let get_analysis (resumptions, initial_forest, object_term) lex =
Log.debug (fun m -> m "Trying to get some analysis");
match lex.datalog_prog with
| None ->
let () =
Logs.warn (fun m ->
m
"Parsing@ is@ not@ yet@ implemented@ for@ non-atomic@ \
distinguished@ type.")
in
(None, (resumptions, initial_forest, object_term))
| Some { rule_to_cst = rule_id_to_cst; _ } -> (
match SharedForest.SharedForest.resume resumptions with
| None, resumptions -> (None, (resumptions, initial_forest, object_term))
| Some (t, weight), resumptions ->
let res = Containers.TreeContext.Tree.fold_depth_first
( (fun rule_id -> RuleToCstMap.find rule_id rule_id_to_cst),
fun x y -> Lambda.App (x, y) )
t in
let () =
ParsingLog.info
(fun m ->
let test =
let obj_term, dist_type = object_term in
let interpreted_type = Data_Signature.expand_type (interpret_type dist_type lex) lex.object_sig in
Lambda.equal
~id_to_term:(fun i -> Data_Signature.unfold_term_definition i lex.object_sig)
~type_of_const:(fun i -> Data_Signature.(expand_type (type_of_constant (snd (id_to_string lex.object_sig i)) lex.object_sig) lex.object_sig))
(obj_term, interpreted_type)
(interpret res (Data_Signature.expand_type dist_type lex.abstract_sig) lex) in
let () = m "Checking@ that@ the@ interpretation@ of@ the@ parsing@ result@ and@ the@ term@ to@ parse@ are@ the@ same: %B" test in
assert test) in
( Some(res, weight ),
(resumptions, initial_forest, object_term) ))
let is_empty (resumptions, _, _) = SharedForest.SharedForest.Resumptions.is_empty resumptions
let get_program lex =
match lex.datalog_prog with None -> None | Some { prog = p; _ } -> Some p
let check_intentional_predicates lex =
if Data_Signature.is_2nd_order lex.abstract_sig then
match lex.datalog_prog with
| None -> ()
| Some ({ prog; magic_programs = _; rule_to_cst = _; cst_to_rule = _ ; generated_symbols = _} as _correspondance) ->
let _new_ids_to_rules_map =
List.fold_left
(fun ids_to_rules p_id ->
match DatalogPredMap.find_opt p_id ids_to_rules with
| Some rules when not (DatalogRule.Rules.is_empty rules) -> ids_to_rules
| _ ->
let () =
Logs.warn (fun m ->
m
"The@ ACG@ defined@ by@ lexicon@ \"%a\"@ is@ \
second-order,@ but@ the@ abstract@ type@ \"%s\"@ is@ \
never@ the@ resulting@ type@ of@ an@ abstract@ \
constant,@ although@ it@ is@ used@ as@ argument@ \
type@ for@ some@ constant."
Utils.lex_pp
(let name, _ = lex.name in
name)
(ASPred.PredIdTable.find_sym_from_id p_id
prog.Datalog.Program.pred_table)) in
DatalogPredMap.add p_id DatalogRule.Rules.empty ids_to_rules)
prog.Datalog.Program.rules
prog.Datalog.Program.idb in
()
else ()
let check ({ dico = d; abstract_sig = abs; _ } as lex) =
let missing_interpretations =
Data_Signature.fold
(fun e acc ->
match Data_Signature.is_declared e abs with
| Some s -> (
match Data_Signature.entry_to_data e with
| Data_Signature.Type _ ->
if Dico.mem (s, Pair.Type) d then acc else s :: acc
| Data_Signature.Term _ ->
if Dico.mem (s, Pair.Cst) d then acc else s :: acc)
| None -> acc)
[] abs
in
match missing_interpretations with
| [] -> check_intentional_predicates lex
| lst -> emit_missing_inter lex lst
let rebuild_interpetation lex =
match lex.syntax_dico with
| None ->
failwith
"bug: a rebuild of a lexicon defined as composition was triggered"
| Some syntax_dico ->
let prog =
if Data_Signature.is_2nd_order lex.abstract_sig then
Some
{
prog = Datalog.Program.empty;
magic_programs = None;
rule_to_cst = RuleToCstMap.empty;
cst_to_rule = Utils.IntMap.empty;
generated_symbols = (Utils.IntMap.empty, Utils.StringSet.empty);
}
else None
in
let new_lex =
Dico.fold
(fun _ abs_syntax_tree lex -> insert abs_syntax_tree lex)
syntax_dico
{ lex with dico = Dico.empty; datalog_prog = prog }
in
{ new_lex with timestamp = Unix.time () }
[@@warning "-32"]
let compose lex1 lex2 n =
let temp_lex =
{
name = n;
dico =
Dico.fold
(fun key inter acc ->
match inter with
| Type (l, stype) ->
Dico.add key (Type (l, interpret_type stype lex1)) acc
| Constant (l, t) ->
Dico.add key
(Constant
( l,
Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i
lex1.object_sig)
(interpret_term t lex1) ))
acc)
lex2.dico Dico.empty;
syntax_dico = None;
abstract_sig = lex2.abstract_sig;
object_sig = lex1.object_sig;
datalog_prog = lex2.datalog_prog;
non_linear_interpretation =
lex1.non_linear_interpretation || lex2.non_linear_interpretation;
build = Compose [fst (name lex1); fst(name lex2)];
timestamp = Unix.time ();
is_almost_linear = true;
}
in
rebuild_prog temp_lex
let rec interpret_by_lexicons ~interpretation term_or_type lexicons =
match lexicons with
| [] -> term_or_type
| (l,_) :: tl ->
interpret_by_lexicons ~interpretation (interpretation term_or_type l) tl
let term_interpretation_and_normalization t l =
let interpreted_term = interpret_term t l in
Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i
l.object_sig)
interpreted_term
let compose_lexicons lexicons n =
match lexicons with
| [] -> failwith "Bug: composing an empty sequence of lexicons"
| (lex,pos) :: tl ->
let (last_lex, _), non_linear_interpretation =
List.fold_left
(fun ((previous_lex,pos1), non_linear_interpretation) (l_lex,pos2) ->
match Data_Signature.name previous_lex.object_sig, Data_Signature.name l_lex.abstract_sig with
| (l1_name,_), (l2_name, _) when l1_name <> l2_name ->
let new_loc = fst pos2, snd pos1 in
Errors.(LexiconErrors.emit (Lexicon_l.NotComposable (fst n, fst previous_lex.name, fst l_lex.name)) ~loc:new_loc)
| _ ->
(l_lex, pos2),
non_linear_interpretation || l_lex.non_linear_interpretation)
((lex,pos), lex.non_linear_interpretation)
tl in
let temp_lex =
{
name = n;
dico =
Dico.fold
(fun key inter acc ->
match inter with
| Type (l, stype) ->
Dico.add key (Type (l, interpret_by_lexicons
~interpretation:(fun stype l_lex ->
interpret_type stype l_lex)
stype
tl)) acc
| Constant (l, t) ->
Dico.add key
(Constant
( l,
(interpret_by_lexicons ~interpretation:term_interpretation_and_normalization t tl) ))
acc)
lex.dico Dico.empty;
syntax_dico = None;
abstract_sig = lex.abstract_sig;
object_sig = last_lex.object_sig;
datalog_prog = lex.datalog_prog;
non_linear_interpretation = non_linear_interpretation;
build = Compose ((fst (name lex) :: (List.map (fun (l, _) -> fst (name l)) tl))) ;
timestamp = Unix.time ();
is_almost_linear = true;
}
in
rebuild_prog temp_lex
let pp_query lex fmt (term, dist_type) =
match
(lex.datalog_prog, Data_Signature.expand_type dist_type lex.abstract_sig)
with
| None, _ ->
Logs.warn (fun m ->
m "Parsing is not implemented for non 2nd order ACG")
| Some { prog; generated_symbols; _ }, (Lambda.Atom _ as dist_type) ->
let dist_type_image = interpret_type dist_type lex in
let obj_term =
Data_Signature.eta_long_form
(Lambda.normalize
~id_to_term:(fun i ->
Data_Signature.unfold_term_definition i lex.object_sig)
(Data_Signature.expand_term term lex.object_sig))
dist_type_image lex.object_sig
in
let obj_princ_type, obj_typing_env =
TypeInference.Type.inference obj_term
in
let query, temp_prog =
Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
~obj_sig:lex.object_sig ~syms:generated_symbols
in
Format.fprintf fmt
"@[Facts:@,@[<v> @[<v>%a@]@]@]@,@[Query:@,@[<v> @[%a?@]@]@]"
Datalog.Program.pp_edb temp_prog
(DatalogAbstractSyntax.Predicate.pp
temp_prog.Datalog.Program.pred_table
temp_prog.Datalog.Program.const_table)
query
| Some _, _ ->
Logs.warn (fun m -> m
"Parsing is not yet implemented for non atomic distinguished type")
let magic lex =
match lex.datalog_prog with
| None -> lex
| Some prog
when prog.magic_programs = None
&& Data_Signature.is_2nd_order lex.abstract_sig ->
let rules = prog.prog.Datalog.Program.abstract_rules in
let t = Timer.top () in
let abs_prog =
ASProg.
{
rules;
pred_table = prog.prog.Datalog.Program.pred_table;
const_table = prog.prog.Datalog.Program.const_table;
i_preds = ASPred.PredIds.of_list prog.prog.Datalog.Program.idb;
rule_id_gen = prog.prog.Datalog.Program.rule_id_gen;
head_to_rules =
ASRule.Rules.fold
(fun r acc ->
match
ASPred.PredIdMap.find_opt r.ASRule.lhs.ASPred.p_id acc
with
| None ->
ASPred.PredIdMap.add r.ASRule.lhs.ASPred.p_id
(ASRule.Rules.singleton r) acc
| Some ruls ->
ASPred.PredIdMap.add r.ASRule.lhs.ASPred.p_id
(ASRule.Rules.add r ruls) acc)
rules ASPred.PredIdMap.empty;
e_pred_to_rules = ASPred.PredIdMap.empty;
}
in
let () = Timer.debug (fun m ->
m "@[Converting@ Datalog@ program@ for@ %a@ to@ abstract@ \
progam@ before@ magic@ rewritting@ took: %a@]"
pp_lex lex UtilsLib.Timer.elapsed t) in
let starting_magic_computation = Timer.top () in
let progs =
MagicRewriting.Rewriting.rewrite_programs
~msg:(Printf.sprintf "Lexicon '%s'" (fst lex.name))
abs_prog
in
let ending_magic_computation = Timer.top () in
let magic_programs =
MagicRewriting.Rewriting.QueryMap.mapi
(fun (p_id, bfs) (as_prog, ctx) ->
let () =
MagicLog.info (fun m ->
m "Making magic program for lexicon %s and query %s_%s \
(%d rules)@?"
(fst lex.name)
(ASPred.PredIdTable.find_sym_from_id p_id
prog.prog.Datalog.Program.pred_table)
(MagicRewriting.Adornment.to_string bfs)
(ASRule.Rules.cardinal as_prog.ASProg.rules)) in
let () =
MagicLog.debug (fun m ->
m "Abstract program (%s) for %s_%s is:@,@[<v>@[%a@]@]" (fst lex.name)
(ASPred.PredIdTable.find_sym_from_id p_id
prog.prog.Datalog.Program.pred_table)
(MagicRewriting.Adornment.to_string bfs)
(ASProg.pp ~with_position:false ~with_id:true)
as_prog)
in
(Datalog.Program.make_program as_prog, ctx))
progs
in
let ending_compile_all_programs = Timer.top () in
let () =
Timer.debug (fun m ->
m "@[<v2>Magic programs for lexicon %a:@,@[<hv>Build time: %a@]@,@[Compile time: %a@]@]"
pp_lex
lex
Timer.diff
(ending_magic_computation, starting_magic_computation)
Timer.diff
(ending_compile_all_programs, ending_magic_computation)) in
let prog' = { prog with magic_programs = Some magic_programs } in
{ lex with datalog_prog = Some prog' }
| Some _prog -> lex
let has_magic lex =
match lex.datalog_prog with
| None -> Unavailable
| Some prog when prog.magic_programs = None -> Available_wo_magic
| Some _ -> Available_with_magic
end