Source file determinacy_checker.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
open Elpi_util.Util
open Elpi_parser.Ast
open Compiler_data
module C = Constants
module UF = Symbol.UF
module S = Elpi_runtime.Data.Global_symbols
module Format = struct
include Format
let eprintf = fun e -> Format.ifprintf Format.err_formatter e
end
let error ~loc msg = error ~loc ("DetCheck: " ^ msg)
type dtype =
| Det (** -> for deterministic preds *)
| Rel (** -> for relational preds *)
| Exp of dtype list (** -> for kinds like list, int, string *)
| BVar of F.t (** -> in predicates like: std.exists or in parametric type abbreviations. *)
| Arrow of Mode.t * Structured.variadic * dtype * dtype (** -> abstractions *)
| Any
[@@deriving show, ord]
module Good_call : sig
type offending_term = { exp : dtype; found : dtype; term : ScopedTerm.t }
type t [@@deriving show]
val init : unit -> t
val make : exp:dtype -> found:dtype -> ScopedTerm.t -> t
val is_good : t -> bool
val is_wrong : t -> bool
val get : t -> offending_term list
val set : t -> t -> unit
val set_wrong : t -> exp:dtype -> found:dtype -> ScopedTerm.t -> unit
val set_good : t -> unit
val prepend : t -> exp:dtype -> found:dtype -> ScopedTerm.t -> t
end = struct
type offending_term = { exp : dtype; found : dtype; term : ScopedTerm.t }
type t = offending_term list ref
let init () : t = ref []
let make ~exp ~found term : t = ref @@ [{ exp; found; term }]
let is_good (x : t) = !x = []
let is_wrong (x : t) = !x <> []
let get (x : t) = !x
let set (t1 : t) (t2 : t) = t1 := !t2
let set_wrong (t1 : t) ~exp ~found term = t1 := [{ exp; found; term }]
let prepend (t1:t) ~exp ~found term =
match !t1 with
| x :: _ when x.term == term -> t1
| _ -> t1 := { exp; found; term } :: !t1; t1
let set_good t = t := []
let show (x : t) = match !x with [] -> "true" | e::_ -> Format.asprintf "false (%a)" Loc.pp e.term.loc
let pp fmt x = Format.fprintf fmt "%s" (show x)
end
exception DetError of (Scope.t ScopedTerm.const option * Good_call.t)
exception FatalDetError of (Scope.t ScopedTerm.const option * Good_call.t)
exception RelationalBody of (Scope.t ScopedTerm.const option * Good_call.t)
exception CastError of (Scope.t ScopedTerm.const option * Good_call.t)
exception KError of (Scope.t ScopedTerm.const option * Good_call.t)
exception LoadFlexClause of ScopedTerm.t
let rec pp_dtype fmt = function
| Det -> Format.fprintf fmt "Det"
| Rel -> Format.fprintf fmt "Rel"
| BVar b -> Format.fprintf fmt "BVar %a" F.pp b
| Any -> Format.fprintf fmt "Any"
| Arrow (m, Variadic, l, r) -> Format.fprintf fmt "(Variadic %a %a-> %a)" pp_dtype l Mode.pretty m pp_dtype r
| Arrow (m, _, l, r) -> Format.fprintf fmt "(%a %a-> %a)" pp_dtype l Mode.pretty m pp_dtype r
| Exp l -> Format.fprintf fmt "Exp [%a]" (pplist pp_dtype ", ") l
type t = (TypeAssignment.skema * Loc.t) F.Map.t [@@deriving show, ord]
let arr m ~v a b = Arrow (m, v, a, b)
let is_exp = function Exp _ -> true | _ -> false
let choose_variadic v full right = if v = Structured.Variadic then full else right
module Compilation = struct
let type_ass_2func ~loc (env : t) t : dtype =
let rec type2func_app ~loc c args =
match F.Map.find_opt c env with
| None -> Exp (List.map (type_ass_2func ~loc) args)
| Some (f, _) ->
let ta_app = TypeAssignment.apply f args in
type_ass_2func ~loc ta_app
and type_ass_2func ~loc = function
| TypeAssignment.Prop Function -> Det
| Prop Relation -> Rel
| Any -> Any
| Cons n -> type2func_app ~loc n []
| App (n, x, xs) -> type2func_app ~loc n (x :: xs)
| Arr (TypeAssignment.MVal m, v, l, r) -> arr m ~v (type_ass_2func ~loc l) (type_ass_2func ~loc r)
| Arr (MRef m, v, l, r) when MutableOnce.is_set m ->
type_ass_2func ~loc (Arr (MutableOnce.get m, v, l, r))
| Arr (MRef _, v, l, r) -> arr ~v Output (type_ass_2func ~loc l) (type_ass_2func ~loc r)
| UVar a -> if MutableOnce.is_set a then (type_ass_2func ~loc (TypeAssignment.deref a)) else BVar (MutableOnce.get_name a)
in
type_ass_2func ~loc t
let type_ass_2func_mut ~loc (env : t) t = type_ass_2func ~loc env (TypeAssignment.deref t)
end
module Aux = struct
let check_variadic f1 f2 mode d1 v1 l1 r1 d2 v2 l2 r2 =
match (v1, v2) with
| Structured.(Variadic, Variadic) -> Arrow (mode, v1, f1 l1 l2, f2 r1 r2)
| NotVariadic, NotVariadic -> Arrow (mode, v1, f1 l1 l2, f2 r1 r2)
| Variadic, NotVariadic -> Arrow (mode, v1, f1 l1 l2, f2 d1 r2)
| NotVariadic, Variadic -> Arrow (mode, v1, f1 l1 l2, f2 r1 d2)
let (<=) m1 m2 ~positive ~d1 ~d2 =
let open Mode in
match m1, m2 with
| Input, Input -> Input, not positive, (d2, d1)
| Output, Input -> (if positive then Output else Input), not positive, (if positive then d2,d1 else d1,d2)
| Output, Output -> Output, positive, (d1, d2)
| Input, Output -> (if not positive then Output else Input), positive, (if positive then d1,d2 else d2,d1)
let rec min_max ~positive ~loc ~d1 ~d2 f1 f2 =
if f1 = d1 || f2 = d1 then d1
else
match (f1, f2) with
| Det, Det -> Det
| Rel, Rel -> Rel
| a, (Any | BVar _) | (Any | BVar _), a -> a
| Exp [ ((Det | Rel | Exp _) as x) ], (Det | Rel) -> min_max ~positive ~loc ~d1 ~d2 x f2
| (Det | Rel), Exp [ ((Det | Rel | Exp _) as x) ] -> min_max ~positive ~loc ~d1 ~d2 f1 x
| Exp l1, Exp l2 -> (
try Exp (List.map2 (min_max ~positive ~loc ~d1 ~d2) l1 l2)
with Invalid_argument _ -> error ~loc (Format.asprintf "min_max invalid exp_length: %a != %a" pp_dtype f1 pp_dtype f2))
| Arrow (m1, v1, l1, r1), Arrow (m2, v2, l2, r2) ->
let m, negative, (d1', d2') = (m1 <= m2) ~positive ~d1 ~d2 in
check_variadic (min_max ~positive:negative ~loc ~d1:d1' ~d2:d2') (min_max ~positive ~loc ~d1 ~d2) m f1 v1 l1 r1 f2 v2 l2 r2
| Arrow (_, Variadic, _, r), f2 -> min_max ~positive ~loc ~d1 ~d2 r f2
| f2, Arrow (_, Variadic, _, r) -> min_max ~positive ~loc ~d1 ~d2 r f2
| _ -> Format.asprintf "min between %a and %a" pp_dtype f1 pp_dtype f2 |> error ~loc
let min = min_max ~positive:true ~d1:Det ~d2:Rel
let max = min_max ~positive:true ~d1:Rel ~d2:Det
let rec minimize_maximize ~loc ~d1 ~d2 d =
match d with
| Det | Rel -> d1
| Exp l -> Exp (List.map (minimize_maximize ~loc ~d1 ~d2) l)
| Arrow (Input, v, l, r) ->
Arrow (Input, v, minimize_maximize ~loc ~d1:d2 ~d2:d1 l, minimize_maximize ~loc ~d1 ~d2 r)
| Arrow (Output, v, l, r) -> Arrow (Output, v, minimize_maximize ~loc ~d1 ~d2 l, minimize_maximize ~loc ~d1 ~d2 r)
| Any -> Any
| BVar b -> BVar b
let maximize = minimize_maximize ~d1:Rel ~d2:Det
let is_maximized ~loc d = d = maximize ~loc d
let wrong_type ~loc a b =
error ~loc @@ Format.asprintf "Typing invariant broken: %a <<= %a\n%!" pp_dtype a pp_dtype b
let wrong_bvars ~loc v1 v2 =
error ~loc @@ Format.asprintf "<<=: TC did not unify two unif vars (%a and %a)" F.pp v1 F.pp v2
let ( <<= ) ~loc a b =
let rec choose_dir ~loc t1 t2 = function Mode.Input -> aux ~loc t2 t1 | Mode.Output -> aux ~loc t1 t2
and aux ~loc a b =
match (a, b) with
| _, Any -> true
| Any, _ -> b = maximize ~loc b
| BVar v1, BVar v2 -> F.equal v1 v2 || wrong_bvars ~loc v1 v2
| BVar _, _ | _, BVar _ -> wrong_type ~loc a b
| Exp l1, Exp l2 -> ( try List.for_all2 (aux ~loc) l1 l2 with Invalid_argument _ -> wrong_type ~loc a b)
| Exp [ ((Det | Rel | Exp _) as x) ], (Det | Rel) -> aux ~loc x b
| (Det | Rel), Exp [ ((Det | Rel | Exp _) as x) ] -> aux ~loc a x
| Arrow (m1, NotVariadic, l1, r1), Arrow (_, NotVariadic, l2, r2) -> choose_dir ~loc l1 l2 m1 && aux r1 r2 ~loc
| Arrow (m1, NotVariadic, l1, r1), Arrow (_, Variadic, l2, _) -> choose_dir ~loc l1 l2 m1 && aux r1 b ~loc
| Arrow (m1, Variadic, l1, _), Arrow (_, NotVariadic, l2, r2) -> choose_dir ~loc l1 l2 m1 && aux a r2 ~loc
| Arrow (m1, Variadic, l1, r1), Arrow (_, Variadic, l2, r2) -> choose_dir ~loc l1 l2 m1 && aux r1 r2 ~loc
| Arrow (_, Variadic, _, r), d -> aux r d ~loc
| d, Arrow (_, Variadic, _, r) -> aux d r ~loc
| Arrow _, _ | _, Arrow _ | Exp _, _ -> wrong_type ~loc a b
| _, Rel -> true
| Rel, _ -> false
| Det, _ -> true
in
let res = aux a b ~loc in
res
end
let ( <<= ) = Aux.( <<= )
module EnvMaker (M : Map.S) : sig
type t [@@deriving show]
val add : new_:bool -> loc:Loc.t -> v:dtype -> t -> M.key -> t
val get : t -> M.key -> dtype option
val clone : t -> t
val empty : t
val iter : (M.key -> dtype -> unit) -> t -> unit
end = struct
type t = dtype ref M.t [@@deriving show]
let add ~new_ ~loc ~(v : dtype) (env : t) (n : M.key) : t =
if new_ then M.add n (ref v) env
else match M.find_opt n env with
| None -> M.add n (ref v) env
| Some v' ->
v' := Aux.min ~loc v !v';
env
let get (env : t) (k : M.key) = Option.map ( ! ) (M.find_opt k env)
let empty = M.empty
let clone : t -> t = M.map (fun v -> ref !v)
let iter f (t:t) = M.iter (fun k v -> f k !v) t
end
module Uvar = EnvMaker (F.Map)
module BVar = struct
include EnvMaker (Scope.Map)
let add_oname ~new_ ~loc oname f ctx =
Format.eprintf "add_oname: %a@." (Format.pp_print_option (fun fmt { ScopedTerm.scope = s; name = n; ty = tya } ->
Format.fprintf fmt "@[<hov 2>%a@ with tya:@ %a@ and compiled@ %a@ -- [old: %a])]" F.pp n (TypeAssignment.pretty_mut_once) (TypeAssignment.deref tya)
pp_dtype (f tya)
(Format.pp_print_option pp_dtype) (get ctx (n,s))
)) oname;
match oname with None -> ctx | Some { ScopedTerm.scope; name; ty = tya } -> add ~new_ ~loc ctx (name, scope) ~v:(f tya)
end
let get_dtype ~env ~ctx ~var ~loc ~is_var { ScopedTerm.scope = t; name; ty = tya } =
let get_ctx = function
| None -> error ~loc (Format.asprintf "DetCheck: Bound var %a should be in the local map" F.pp name)
| Some e -> e
in
let get_var = function None -> Aux.maximize ~loc (Compilation.type_ass_2func_mut ~loc env tya) | Some e -> e in
let get_con _x = Compilation.type_ass_2func_mut ~loc env tya in
let det_head =
if is_var then get_var @@ Uvar.get var name
else match t with Scope.Bound b -> get_ctx @@ BVar.get ctx (name, b) | Global g -> get_con g.resolved_to
in
Format.eprintf "Type of %a is %a@." F.pp name pp_dtype det_head;
det_head
let spill_err ~loc = anomaly ~loc "Everything should have already been spilled"
let check_clause ~type_abbrevs:ta ~types ~unknown (t : ScopedTerm.t) : unit =
let same_symb symb symb' =
match symb' with
| Scope.Global { resolved_to = x } ->
begin match SymbolResolver.resolved_to types x with
| Some symb' -> TypingEnv.same_symbol types symb symb'
| _ -> false
end
| _ -> false
in
let get_user_type ~loc s = match s.ScopedTerm.scope with
| Scope.Global {resolved_to = x } ->
let open TypeAssignment in
let rec mk_args = function Ty t -> [] | Lam (_, b) -> Any :: mk_args b in
let apply ty = TypeAssignment.apply ty (mk_args ty) in
let compile TypingEnv.{ty} = Compilation.type_ass_2func ~loc ta (apply ty) in
let to_dtype x = Option.map compile @@ TypingEnv.resolve_symbol_opt x types in
Option.bind (SymbolResolver.resolved_to types x) to_dtype
| Bound _ -> None
in
let has_undeclared_signature { ScopedTerm.scope = b; name = f } =
match F.Map.find_opt f unknown with Some (_, symb) -> same_symb symb b | _ -> false
in
let is_global { ScopedTerm.scope = b } name = same_symb name b in
let is_quantifier x = is_global x S.pi || is_global x S.sigma in
let undecl_disclaimer = function
| Some ({ ScopedTerm.name; ty } as pred_name) when has_undeclared_signature pred_name ->
Format.asprintf
"@[<hov 2>Predicate %a has no declared signature,@ providing one could fix the following error@ (inferred \
signature: %a)@]@\n\
DetCheck: " F.pp name TypeAssignment.pretty_mut_once
(TypeAssignment.deref @@ ty)
| _ -> ""
in
let cnt = ref 0 in
let emit () =
incr cnt;
F.from_string ("*dummy" ^ string_of_int !cnt)
in
let rec get_tl = function Arrow (_, _, _, r) -> get_tl r | e -> e in
let is_cut ScopedTerm.{ it } = match it with App(b,[]) -> is_global b S.cut | _ -> false in
let rec infer ~ctx ~var ~exp t : dtype * Good_call.t =
let rec infer_fold ~was_input ~was_data ~loc ~user_dtype ctx d hd tl =
Format.eprintf "Starting infer fold at %a with dtype:@[%a@] and user_dtype:@[%a@]@." Loc.pp loc pp_dtype d (Format.pp_print_option pp_dtype) user_dtype;
let b = Good_call.init () in
let split_user_dtype = function
| None -> Any, None
| Some Any -> Any, None
| Some (Arrow (m,_,l,r)) -> l, Some r
| Some d -> error ~loc @@ Format.asprintf "DetCheck: found dtype:%a" pp_dtype d
in
let rec aux ~user_dtype d tl : (dtype * Good_call.t) =
Format.eprintf "@[<hov 2>In recursive call for infer.aux with head-term@ @[%a@], good_call is %a -- and dtype@ @[%a@] and user_dytpe is @[%a@]@]@." (Format.pp_print_option ScopedTerm.pretty) (List.nth_opt tl 0)
Good_call.pp b pp_dtype d (Format.pp_print_option pp_dtype) user_dtype;
match (d, tl) with
| Arrow (_, Variadic, _, t), [] -> (t, b)
| t, [] -> ((if Good_call.is_wrong b then Aux.maximize ~loc t else t), b)
| Arrow (_,v,_,r), _ :: tl when Good_call.is_wrong b ->
aux ~user_dtype:(choose_variadic v user_dtype None) (choose_variadic v d r) tl
| Arrow (Input, v, l, r), h :: tl ->
let l_user, r_user = split_user_dtype user_dtype in
let loc = h.loc in
let dy, b' = infer ~was_input:true ~exp:l ctx h in
Format.eprintf "infer.aux in Input branch with dtype:%a and t:%a@." pp_dtype l ScopedTerm.pretty h;
Format.eprintf "end infer.aux for term %a with b':%a and not ((dy <<= l) ~loc):%b and was_data:%b@." ScopedTerm.pretty h Good_call.pp b' (not ((dy <<= l) ~loc)) was_data;
if Good_call.is_wrong b' then begin
let max_exp = Aux.maximize ~loc dy in
if not ((max_exp <<= l_user) ~loc) then raise (KError (Some hd, b'))
else if not ((max_exp <<= l) ~loc) then Good_call.set b b'
end
else if not ((dy <<= l_user) ~loc) then(
raise (KError (Some hd, (Good_call.set_wrong b ~exp:l_user ~found:dy h; b))))
else if not ((dy <<= l) ~loc) then (
Good_call.set_wrong b ~exp:l ~found:dy h;
Format.eprintf "Invalid determinacy set b to wrong (%a)@." Good_call.pp b);
aux ~user_dtype:(choose_variadic v user_dtype r_user) (choose_variadic v d r) tl
| Arrow (Output, v, l, r), hd :: tl ->
if was_data then
aux ~user_dtype (Arrow (Input, v, l, r)) (hd :: tl)
else
let l_user, r_user = split_user_dtype user_dtype in
aux ~user_dtype:(choose_variadic v user_dtype r_user) (choose_variadic v d r) tl
| (BVar _ | Any), _ -> (d, Good_call.init ())
| (Det | Rel | Exp _), _ :: _ ->
Format.asprintf "deduce: Type error, found dtype %a and arguments %a" pp_dtype d
(pplist ScopedTerm.pretty ",") tl
|> anomaly ~loc
in
aux ~user_dtype d tl
and infer_app ~exp ~was_input ctx ~loc is_var t ty s tl =
let was_data = is_exp (Compilation.type_ass_2func_mut ~loc ta ty) in
let user_dtype = if was_data then get_user_type ~loc s else None in
Format.eprintf "Is_exp: %b@." was_data;
let dtype = get_dtype ~env:ta ~ctx ~var ~loc ~is_var s in
let (dt, gc as r) = infer_fold ~was_input ~was_data ~user_dtype ~loc ctx dtype s tl in
if Good_call.is_wrong gc then Good_call.prepend gc ~exp ~found:dt t |> ignore;
r
and infer_and ~was_input ctx ~loc args (_, r as dr) =
match args with
| [] -> dr
| x :: xs when is_cut x ->
Good_call.set_good r;
infer_and ~was_input ctx ~loc xs (Det, r)
| x :: xs ->
let (d,gc) = infer ~exp:Det ~was_input ctx x in
if d = Rel then (
Good_call.set_wrong gc ~exp:Det ~found:Rel x;
infer_and ~was_input ctx ~loc xs (d,gc))
else if Good_call.is_wrong gc then infer_and ~was_input ctx ~loc xs (d,gc)
else infer_and ~was_input ctx ~loc xs dr
and infer ~was_input ~exp ctx ScopedTerm.({ it; ty; loc } as t) : dtype * Good_call.t =
match it with
| Var (b, xs) -> infer_app ~exp ~was_input ~loc ctx true t ty b xs
| App (q, [{ it = Lam (b, _, bo) }]) when is_quantifier q ->
infer ~exp ~was_input (BVar.add_oname ~new_:false ~loc b (fun x -> Compilation.type_ass_2func_mut ~loc ta x) ctx) bo
| App (g, x :: xs) when is_global g S.and_ ->
Format.eprintf "Calling deduce on a comma separated list of subgoals@.";
infer_and ~was_input ctx ~loc (x :: xs) (Det, Good_call.init ())
| App (b, xs) -> infer_app ~exp ~was_input ~loc ctx false t ty b xs
| Impl (L2R,_, c, b) ->
check_clause ~ctx ~var c |> ignore;
infer ~exp ~was_input ctx b
| Impl (L2RBang,_, c, b) ->
check_clause ~ctx ~var ~has_tail_cut:true c |> ignore;
infer ~exp ~was_input ctx b
| Impl (R2L,_, _, _) ->
Format.eprintf "Recursive call to check clause@.";
(check_clause ~ctx ~var t, Good_call.init ())
| Lam _ -> (
try
let _ = check_lam ~ctx ~var t in
(Compilation.type_ass_2func_mut ~loc ta ty, Good_call.init ())
with FatalDetError (_,b1) | DetError (_, b1) | RelationalBody (_, b1) -> (Compilation.type_ass_2func_mut ~loc ta ty, b1))
| Discard ->
Format.eprintf "Calling type_ass_2func_mut in Discard@.";
(Compilation.type_ass_2func_mut ~loc ta ty, Good_call.init ())
| CData _ -> (Exp [], Good_call.init ())
| Cast (t, _) ->
let d, good = infer ~exp ~was_input ctx t in
if Good_call.is_wrong good then raise (FatalDetError (None, good));
(d, good)
| Spill (_, _) -> spill_err ~loc
in
let ((det, gc) as r) = infer ~exp ~was_input:false ctx t in
Format.eprintf "Result of infer for %a is (%a,%a)@." ScopedTerm.pretty t pp_dtype det Good_call.pp gc;
r
and infer_output ~pred_name ~ctx ~var ScopedTerm.{ it; loc } =
Format.eprintf "Calling deduce output on %a@." ScopedTerm.pretty_ it;
let rec aux d args =
match (d, args) with
| Arrow (Input, v, _, r), _ :: tl -> aux (choose_variadic v d r) tl
| Arrow (Output, v, l, r), hd :: tl ->
let det, gc = infer ~exp:l ~ctx ~var hd in
Format.eprintf "Inference of %a gives (%a,%a)@." ScopedTerm.pretty hd pp_dtype det Good_call.pp gc;
if Good_call.is_wrong gc && Aux.is_maximized ~loc l then aux (choose_variadic v d r) tl
else if Good_call.is_good gc && (det <<= l) ~loc then aux (choose_variadic v d r) tl
else if Good_call.is_good gc then raise (DetError (Some pred_name, Good_call.make ~exp:l ~found:det hd))
else raise (DetError (Some pred_name, gc))
| _ -> ()
in
match it with
| App (b, xs) -> aux (get_dtype ~env:ta ~ctx ~var ~loc ~is_var:false b) xs
| Var (b, xs) -> aux (get_dtype ~env:ta ~ctx ~var ~loc ~is_var:true b) xs
| _ -> anomaly ~loc @@ Format.asprintf "Invalid term in deduce output %a." ScopedTerm.pretty_ it
and assume ?(was_input=false) ~ctx ~var d t =
Format.eprintf "Calling assume on %a with det : %a@." ScopedTerm.pretty t pp_dtype d;
let var = ref var in
let add ~loc ~v vname =
Format.eprintf "Permanently adding %a : %a@." F.pp vname pp_dtype v;
let m = Uvar.add ~new_:false ~loc !var vname ~v in
var := m
in
let rec assume_fold ~was_input ~was_data ~loc ctx d (tl : ScopedTerm.t list) : unit =
match (d, tl) with
| _, [] -> ()
| Arrow (Input, v, l, r), h :: tl ->
assume ~was_input:true ctx l h;
assume_fold ~was_input ~was_data ~loc ctx (choose_variadic v d r) tl
| Arrow (Output, v, l, r), h :: tl ->
if was_input && was_data then assume ~was_input ctx l h;
assume_fold ~was_input ~was_data ~loc ctx (choose_variadic v d r) tl
| (BVar _ | Any), _ -> ()
| (Det | Rel | Exp _), _ :: _ ->
Format.asprintf "assume: Type error, found dtype %a and arguments %a@." pp_dtype d
(pplist ScopedTerm.pretty ",") tl
|> anomaly ~loc
and assume_app ~was_input ctx ~loc d ({ ScopedTerm.scope = t; name } as s) tl =
Format.eprintf "Calling assume_app on: %a with dtype %a with args [%a] and@." F.pp name pp_dtype d
(pplist ~boxed:true ScopedTerm.pretty " ; ")
tl;
match t with
| Scope.Bound b -> assume_var ~is_var:(Some b) ~ctx ~loc d s tl
| _ ->
let det_head = get_dtype ~env:ta ~ctx ~var:!var ~loc ~is_var:false s in
assume_fold ~was_input ~was_data:(is_exp d) ~loc ctx det_head tl;
Format.eprintf "The map after call to assume_app is %a@." Uvar.pp !var
and assume_var ~is_var ~ctx ~loc d ({ ScopedTerm.name } as s) tl =
let rec replace_signature_tgt ~with_ d' = function
| [] -> with_
| _::xs -> match d' with
| Arrow (_, Variadic, _, _) -> replace_signature_tgt ~with_ d' xs
| Arrow (m, NotVariadic, l, r) -> Arrow (m, NotVariadic, l, replace_signature_tgt ~with_ r xs)
| _ -> error ~loc @@ Format.asprintf "replace_signature_tgt: Type error: found %a " pp_dtype d' in
let dtype = get_dtype ~env:ta ~ctx ~var:!var ~loc ~is_var:(is_var = None) s in
Format.eprintf "Dtype of %a is %a@." F.pp name pp_dtype dtype;
let d' = replace_signature_tgt dtype tl ~with_:d in
Format.eprintf "d' is %a@." pp_dtype d';
match is_var with
| None -> add ~loc ~v:d' name
| Some b -> BVar.add ~new_:false ctx ~v:d' ~loc (name, b) |> ignore
and assume ~was_input ctx d ScopedTerm.({ loc; it }) : unit =
Format.eprintf "Assume of %a with dtype %a (was_input:%b)@." ScopedTerm.pretty_ it pp_dtype d was_input;
match it with
| App (q, [{ it = Lam (b, _, bo) }]) when is_quantifier q ->
assume ~was_input (BVar.add_oname ~new_:false ~loc b (fun x -> Compilation.type_ass_2func_mut ~loc ta x) ctx) d bo
| Var (b, tl) -> assume_var ~loc ~ctx ~is_var:None d b tl
| App (b, xs) -> assume_app ~was_input ctx ~loc d b xs
| Discard -> ()
| Impl (L2R,_, h, b) ->
check_clause ~ctx ~var:!var h |> ignore;
assume ~was_input ctx d b
| Impl (L2RBang,_, h, b) ->
check_clause ~ctx ~var:!var ~has_tail_cut:true h |> ignore;
assume ~was_input ctx d b
| Impl (R2L,_, {it = App (b, xs)}, bo) ->
let dtype, var' = assume_hd ~is_var:false ~loc ~ctx ~var:!var b t xs in
Uvar.iter (fun k v -> add ~loc ~v k) var';
assume ~was_input:false ctx (get_tl dtype) bo
| Impl (R2L, _,_, _B) -> ()
| Lam (oname, _, c) -> (
match d with
| Arrow (Input, NotVariadic, l, r) ->
let ctx = BVar.add_oname ~new_:true ~loc oname (fun _ -> l) ctx in
assume ~was_input ctx r c
| Arrow (Output, NotVariadic, l, r) ->
let ctx = BVar.add_oname ~new_:true ~loc oname (fun _ -> l) ctx in
assume ~was_input ctx r c
| Any -> ()
| _ -> anomaly ~loc (Format.asprintf "Found lambda term with dtype %a" pp_dtype d))
| CData _ -> ()
| Spill _ -> spill_err ~loc
| Cast (t, _) -> assume ~was_input ctx d t
in
assume ~was_input ctx d t;
!var
and assume_output ~ctx ~var d tl : Uvar.t =
let rec assume_output d args var =
match (d, args) with
| Arrow (Input, v, _, r), _ :: tl -> assume_output (choose_variadic v d r) tl var
| Arrow (Output, v, l, r), hd :: tl ->
Format.eprintf "Call assume of %a with dtype:%a@." ScopedTerm.pretty hd pp_dtype l;
let var = assume ~was_input:true ~ctx ~var l hd in
assume_output (choose_variadic v d r) tl var
| _ -> var
in
assume_output d tl var
and assume_input ~ctx ~var d tl : Uvar.t =
let rec assume_input d args var =
match (d, args) with
| Arrow (Input, v, l, r), hd :: tl ->
Format.eprintf "Call assume of %a with dtype:%a@." ScopedTerm.pretty hd pp_dtype l;
let var = assume ~was_input:true ~ctx ~var l hd in
assume_input (choose_variadic v d r) tl var
| Arrow (Output, v, _, r), _ :: tl ->assume_input (choose_variadic v d r) tl var
| _ -> var
in
assume_input d tl var
and check ~ctx ~var (d : dtype) t : Uvar.t * (dtype * _) * bool =
let has_top_level_cut = ref false in
let var = ref var in
let rec check_app ctx ~loc (d : dtype) ~is_var b tl tm =
Format.eprintf "@[<hov 2>-- Entering check_app with term@ @[%a@]@]@." ScopedTerm.pretty tm;
let d', gc = infer ~exp:d ~ctx ~var:!var tm in
Format.eprintf "-- Checked term dtype is %a and gc is %a@." pp_dtype d' Good_call.pp gc;
if Good_call.is_good gc then (
let det = get_dtype ~env:ta ~ctx ~var:!var ~is_var b ~loc in
Format.eprintf "Assuming output of %a with dtype : %a@." ScopedTerm.pretty tm pp_dtype det;
var := assume_output ~ctx ~var:!var det tl);
Format.eprintf "In check_app before result, comparing %a with %a (expected %a)@."
ScopedTerm.pretty tm pp_dtype d' pp_dtype d;
if Good_call.is_good gc then
if (d' <<= d) ~loc then (Aux.max ~loc (get_tl d) (get_tl d'), gc)
else (Rel, (Good_call.set_wrong ~exp:d ~found:d' gc tm; gc))
else (Rel, gc)
and check_comma ctx ~loc (d, bad_atom) args =
match args with
| [] -> (d, bad_atom)
| x :: xs when is_cut x ->
Good_call.set_good bad_atom;
check_comma ctx ~loc (Det, bad_atom) xs
| x :: xs ->
Format.eprintf "Checking comma with first term %a@." ScopedTerm.pretty x;
let d1, bad_atom1 = check ~ctx d x in
if Good_call.is_good bad_atom then
if Good_call.is_wrong bad_atom1 then Good_call.set bad_atom bad_atom1
else if d1 = Rel then Good_call.set_wrong bad_atom ~exp:Det ~found:Rel x;
check_comma ctx ~loc (d1, bad_atom) xs
and check ~ctx (d : dtype) ScopedTerm.({ it; loc } as t) : dtype * Good_call.t =
match it with
| Impl (L2R, _,h, b) ->
check_clause ~ctx ~var:!var h |> ignore;
check ~ctx d b
| Impl (L2RBang,_, h, b) ->
check_clause ~ctx ~var:!var ~has_tail_cut:true h |> ignore;
check ~ctx d b
| App(b,[]) when is_global b S.cut -> (Det, Good_call.init ())
| App (q, [{ it = Lam (b, _, bo) }]) when is_quantifier q ->
check ~ctx:(BVar.add_oname ~new_:true ~loc b (Compilation.type_ass_2func_mut ~loc ta) ctx) d bo
| App (b, [x; xs ]) when is_global b S.cons -> check ~ctx (check ~ctx d x |> fst) xs
| App(b,[]) when is_global b S.nil -> (d, Good_call.init ())
| App (b, x :: xs) when is_global b S.and_ -> check_comma ctx ~loc (d, Good_call.init ()) (x :: xs)
| App (b, [l; r ]) when is_global b S.eq ->
let d1, gc = infer ~exp:Any ~ctx ~var:!var l in
(if Good_call.is_good gc then
let d2, gc = infer ~exp:Any ~ctx ~var:!var r in
if Good_call.is_good gc then (
Format.eprintf "In equality calling min between the two terms %a and %a@." ScopedTerm.pretty l
ScopedTerm.pretty r;
let m = Aux.min ~loc d1 d2 in
Format.eprintf "The minimum between %a and %a is %a@." pp_dtype d1 pp_dtype d2 pp_dtype m;
var := assume ~ctx ~var:!var m l;
var := assume ~ctx ~var:!var m r));
(d, Good_call.init ())
| Var (b, xs) -> check_app ctx ~loc d ~is_var:true b xs t
| App (b, xs) -> check_app ctx ~loc d ~is_var:false b xs t
| Cast (b, _) -> (
try
let d, _ = check ~ctx d b in
let d' = Compilation.type_ass_2func_mut ~loc ta b.ty in
if not ((d <<= d') ~loc) then raise (CastError (None, Good_call.make ~exp:d' ~found:d b));
(d, Good_call.init ())
with DetError x -> raise (FatalDetError x))
| Spill _ -> spill_err ~loc
| CData _ -> anomaly ~loc "Found CData in prop position"
| Lam _ -> anomaly ~loc "Lambda-abstractions are not props"
| Discard -> anomaly ~loc "Discard found in prop position"
| Impl (R2L, _,_, _) -> anomaly ~loc "Found clause in prop position"
in
(!var, check ~ctx d t, !has_top_level_cut)
and check_lam ~ctx ~var t : dtype =
Format.eprintf "check_lam: t = %a@." ScopedTerm.pretty t;
let get_ta n args =
let ta_sk, _ = F.Map.find n ta in
let ty = TypeAssignment.apply ta_sk args in
TypeAssignment.create ty
in
let otype2term ~loc ty b =
let ty = TypeAssignment.create ty in
let it = match b with None -> ScopedTerm.Discard | Some { ScopedTerm.scope = a; name = b; ty = c; loc } -> App({ ScopedTerm.scope = Bound a; name = b; ty = c; loc },[]) in
ScopedTerm.{ it; ty; loc }
in
let build_clause args ~ctx ~loc ~ty body =
let new_pred = emit () in
let args = List.rev args in
let b = { ScopedTerm.scope = Scope.Global {resolved_to=SymbolResolver.make ();escape_ns=false}; name = new_pred; ty = t.ty; loc = t.loc } in
let pred_hd = ScopedTerm.(App (b, args)) in
let clause = ScopedTerm.{ ty; it = Impl (R2L, loc, { it = pred_hd; ty; loc }, body); loc } in
Format.eprintf "Clause is %a@." ScopedTerm.pretty clause;
(clause, ctx)
in
let add_partial_app (ScopedTerm.{ it; loc } as t) args ty =
let args = List.rev args in
match args with
| [] -> t
| hd :: tl -> (
match it with
| App (b, xs) -> { it = App (b, xs @ args); ty; loc }
| Var (b, xs) -> { it = Var (b, xs @ args); ty; loc }
| _ -> assert false)
in
let rec aux ~ctx ~args ~parial_app (ScopedTerm.{ it; loc; ty } as t) : dtype =
match (TypeAssignment.deref ty, it) with
| Prop _, Impl (R2L, _, _, bo) ->
assert (parial_app = []);
let clause, ctx = build_clause args ~ctx ~loc ~ty bo in
check_clause ~ctx ~var clause
| Prop _, _ ->
let t = add_partial_app t parial_app ty in
let clause, ctx = build_clause args ~ctx ~loc ~ty t in
Format.eprintf "check_lam: built clause is = %a@." ScopedTerm.pretty clause;
check_clause ~ctx ~var clause
| Cons b, _ when F.Map.mem b ta -> aux ~parial_app ~ctx ~args { t with ty = get_ta b [] }
| App (b, x, xs), _ when F.Map.mem b ta -> aux ~parial_app ~ctx ~args { t with ty = get_ta b (x :: xs) }
| Cons _, _ -> Exp []
| App (_, x, xs), _ -> Exp (List.map (Compilation.type_ass_2func ta ~loc) (x :: xs))
| ((UVar _ | Any) as t), _ -> Compilation.type_ass_2func ta ~loc t
| Arr (_, _, l, _), Lam (b, _, bo) ->
aux ~parial_app ~ctx:(BVar.add_oname ~new_:true ~loc b (fun t -> Aux.maximize ~loc (Compilation.type_ass_2func_mut ~loc ta t)) ctx) ~args:(otype2term ~loc l b :: args) bo
| Arr (_, Structured.Variadic, _, r), _ ->
let b = Some { ScopedTerm.scope = elpi_language; name = emit (); ty = TypeAssignment.create r; loc } in
aux ~parial_app ~ctx:(BVar.add_oname ~new_:true ~loc b (fun t -> Aux.maximize ~loc (Compilation.type_ass_2func_mut ~loc ta t)) ctx) ~args { t with ty = TypeAssignment.create r }
| Arr (_, _, l, r), _ ->
let b = Some { ScopedTerm.scope = elpi_language; name = emit (); ty = TypeAssignment.create l; loc } in
let nt = otype2term ~loc l b in
aux ~parial_app:(nt :: parial_app)
~ctx:(BVar.add_oname ~new_:true ~loc b (fun t -> Aux.maximize ~loc (Compilation.type_ass_2func_mut ~loc ta t)) ctx)
~args:(nt :: args)
{ t with ty = TypeAssignment.create r }
in
aux ~ctx ~args:[] ~parial_app:[] t
and assume_hd b ~is_var ~ctx ~var ~loc (tm : ScopedTerm.t) tl =
let det_hd = get_dtype ~env:ta ~ctx ~var ~loc ~is_var b in
Format.eprintf "assume_input for term %a with det %a@." ScopedTerm.pretty tm pp_dtype det_hd;
(det_hd, assume_input ~ctx ~var det_hd tl)
and check_clause ?(_is_toplevel = false) ~ctx ~var ?(has_tail_cut=false) ScopedTerm.({ loc } as t) : dtype =
let ctx = ref (BVar.clone ctx) in
let var = Uvar.clone var in
let rec aux ScopedTerm.{ it; loc } =
match it with
| Impl (R2L, _, ({ it = App (b, xs) } as hd), bo) -> (b, assume_hd ~loc ~ctx:!ctx ~var:var b ~is_var:false hd xs, hd, Some bo)
| Impl (R2L, _, ({ it = Var(b,xs) } as hd), bo) -> (b, assume_hd ~loc ~ctx:!ctx ~var:var b ~is_var:true hd xs, hd, Some bo)
| App (n, [{ it = Lam (oname, _, body) }]) when is_quantifier n ->
ctx := BVar.add_oname ~new_:true ~loc oname (Compilation.type_ass_2func_mut ~loc ta) !ctx;
aux body
| App (b, xs) -> (b, assume_hd ~loc ~ctx:!ctx ~var:var b ~is_var:false t xs, t, None)
| Var _ -> raise (LoadFlexClause t)
| _ -> anomaly ~loc @@ Format.asprintf "Found term %a in prop position" ScopedTerm.pretty_ it
in
try
let pred_name, (det_hd, var), hd, body = aux t in
Format.eprintf "Var is %a@." Uvar.pp var;
let var, (det_body, err_atom), _has_top_level_cut =
Option.(
map (check ~ctx:!ctx ~var Det) body
|> value ~default:(var, (Det, Good_call.init ()), false))
in
let det_body = if has_tail_cut then Det else det_body in
Format.eprintf "** END CHECKING THE CLAUSE @.";
Format.eprintf "The var map is %a and det_body is %a@." Uvar.pp var pp_dtype det_body;
let det_pred = get_tl det_hd in
if not @@ (det_body <<= det_pred) ~loc then
raise (RelationalBody (Some pred_name, Good_call.prepend ~exp:det_pred ~found:det_body err_atom (Option.get body)));
Format.eprintf "** Start checking outputs@.";
infer_output ~pred_name ~ctx:!ctx ~var hd;
det_pred
with LoadFlexClause t ->
if not has_tail_cut then
warn ~loc:t.loc ~id:FlexClause (Format.asprintf "ignoring flexible clause: %a" ScopedTerm.pretty t);
Det
in
let err gc f =
let last l = List.hd (List.rev l) in
let pp_bt Good_call.{ exp; found; term } =
Format.asprintf "From (@[%a@]) \n - Inferred: %a \n - Expected: %a" ScopedTerm.pretty term pp_dtype found pp_dtype exp
in
let l = Good_call.get gc in
assert (l <> []);
error ~loc:(last l).term.loc @@ String.concat "\n" (f (List.hd l) :: List.map pp_bt l) in
try check_clause ~_is_toplevel:true ~ctx:BVar.empty ~var:Uvar.empty t |> ignore with
| FatalDetError (pred_name, gc) | DetError (pred_name, gc) ->
let f Good_call.{ exp; found; term } =
Format.asprintf "%sInvalid determinacy of output term %a.\n Expected: %a\n Found: %a"
(undecl_disclaimer pred_name) ScopedTerm.pretty term pp_dtype exp pp_dtype found
in
err gc f
| KError (pred_name, gc) ->
let f Good_call.{ exp; found; term } =
Format.asprintf "%sInvalid determinacy of constructor argument %a.\n Expected: %a\n Found: %a"
(undecl_disclaimer pred_name) ScopedTerm.pretty term pp_dtype exp pp_dtype found
in
err gc f
| CastError (_,gc) ->
let f Good_call.{ exp; found; term } =
Format.asprintf "Cast error on term %a.\n Expected: %a\n Found: %a"
ScopedTerm.pretty term pp_dtype exp pp_dtype found
in
err gc f
| RelationalBody (pred_name, gc) ->
let f Good_call.{ term } =
Format.asprintf "%s@[<hov 2>Found relational atom@ @[<hov 2>(%a)@]@ in the body of function@ %a@]"
(undecl_disclaimer pred_name) ScopedTerm.pretty term F.pp (let { ScopedTerm.name = n } = Option.get pred_name in n)
in
err gc f