Mercurial > urweb

comparison src/iflow.sml @ 1215:360f1ed0a969

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Implemented proper congruence closure, to the point where tests/policy works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Apr 2010 12:46:21 -0400
parents 648e6b087dfb
children 09caa8c780e5
comparison
equal deleted inserted replaced
1214:648e6b087dfb 1215:360f1ed0a969
30 open Mono 30 open Mono
31 31
32 structure IS = IntBinarySet 32 structure IS = IntBinarySet
33 structure IM = IntBinaryMap 33 structure IM = IntBinaryMap
34 34
35 structure SS = BinarySetFn(struct 35 structure SK = struct
36 type ord_key = string 36 type ord_key = string
37 val compare = String.compare 37 val compare = String.compare
38 end) 38 end
39
40 structure SS = BinarySetFn(SK)
41 structure SM = BinaryMapFn(SK)
39 42
40 val writers = ["htmlifyInt_w", 43 val writers = ["htmlifyInt_w",
41 "htmlifyFloat_w", 44 "htmlifyFloat_w",
42 "htmlifyString_w", 45 "htmlifyString_w",
43 "htmlifyBool_w", 46 "htmlifyBool_w",
54 57
55 val writers = SS.addList (SS.empty, writers) 58 val writers = SS.addList (SS.empty, writers)
56 59
57 type lvar = int 60 type lvar = int
58 61
62 datatype func =
63 DtCon0 of string
64 | DtCon1 of string
65 | UnCon of string
66 | Other of string
67
59 datatype exp = 68 datatype exp =
60 Const of Prim.t 69 Const of Prim.t
61 | Var of int 70 | Var of int
62 | Lvar of lvar 71 | Lvar of lvar
63 | Func of string * exp list 72 | Func of func * exp list
64 | Recd of (string * exp) list 73 | Recd of (string * exp) list
65 | Proj of exp * string 74 | Proj of exp * string
66 | Finish 75 | Finish
67 76
68 datatype reln = 77 datatype reln =
69 Known 78 Known
70 | Sql of string 79 | Sql of string
71 | DtCon of string 80 | PCon0 of string
81 | PCon1 of string
72 | Eq 82 | Eq
73 | Ne 83 | Ne
74 | Lt 84 | Lt
75 | Le 85 | Le
76 | Gt 86 | Gt
83 | And of prop * prop 93 | And of prop * prop
84 | Or of prop * prop 94 | Or of prop * prop
85 | Reln of reln * exp list 95 | Reln of reln * exp list
86 | Cond of exp * prop 96 | Cond of exp * prop
87 97
98 val unif = ref (IM.empty : exp IM.map)
99
100 fun reset () = unif := IM.empty
101 fun save () = !unif
102 fun restore x = unif := x
103
88 local 104 local
89 open Print 105 open Print
90 val string = PD.string 106 val string = PD.string
91 in 107 in
92 108
109 fun p_func f =
110 string (case f of
111 DtCon0 s => s
112 | DtCon1 s => s
113 | UnCon s => "un" ^ s
114 | Other s => s)
115
93 fun p_exp e = 116 fun p_exp e =
94 case e of 117 case e of
95 Const p => Prim.p_t p 118 Const p => Prim.p_t p
96 | Var n => string ("x" ^ Int.toString n) 119 | Var n => string ("x" ^ Int.toString n)
97 | Lvar n => string ("X" ^ Int.toString n) 120 | Lvar n =>
98 | Func (f, es) => box [string (f ^ "("), 121 (case IM.find (!unif, n) of
122 NONE => string ("X" ^ Int.toString n)
123 | SOME e => p_exp e)
124 | Func (f, es) => box [p_func f,
125 string "(",
99 p_list p_exp es, 126 p_list p_exp es,
100 string ")"] 127 string ")"]
101 | Recd xes => box [string "{", 128 | Recd xes => box [string "{",
102 p_list (fn (x, e) => box [string x, 129 p_list (fn (x, e) => box [string x,
103 space, 130 space,
127 string ")"] 154 string ")"]
128 | _ => raise Fail "Iflow.p_reln: Known") 155 | _ => raise Fail "Iflow.p_reln: Known")
129 | Sql s => box [string (s ^ "("), 156 | Sql s => box [string (s ^ "("),
130 p_list p_exp es, 157 p_list p_exp es,
131 string ")"] 158 string ")"]
132 | DtCon s => box [string (s ^ "("), 159 | PCon0 s => box [string (s ^ "("),
160 p_list p_exp es,
161 string ")"]
162 | PCon1 s => box [string (s ^ "("),
133 p_list p_exp es, 163 p_list p_exp es,
134 string ")"] 164 string ")"]
135 | Eq => p_bop "=" es 165 | Eq => p_bop "=" es
136 | Ne => p_bop "<>" es 166 | Ne => p_bop "<>" es
137 | Lt => p_bop "<" es 167 | Lt => p_bop "<" es
196 fun isFinish e = 226 fun isFinish e =
197 case e of 227 case e of
198 Finish => true 228 Finish => true
199 | _ => false 229 | _ => false
200 230
201 val unif = ref (IM.empty : exp IM.map)
202
203 fun reset () = unif := IM.empty
204 fun save () = !unif
205 fun restore x = unif := x
206
207 fun simplify e = 231 fun simplify e =
208 case e of 232 case e of
209 Const _ => e 233 Const _ => e
210 | Var _ => e 234 | Var _ => e
211 | Lvar n => 235 | Lvar n =>
212 (case IM.find (!unif, n) of 236 (case IM.find (!unif, n) of
213 NONE => e 237 NONE => e
214 | SOME e => simplify e) 238 | SOME e => simplify e)
215 | Func (f, es) => 239 | Func (f, es) => Func (f, map simplify es)
216 let 240 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
217 val es = map simplify es 241 | Proj (e, s) => Proj (simplify e, s)
218
219 fun default () = Func (f, es)
220 in
221 if List.exists isFinish es then
222 Finish
223 else if String.isPrefix "un" f then
224 case es of
225 [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then
226 e
227 else
228 default ()
229 | _ => default ()
230 else
231 default ()
232 end
233 | Recd xes =>
234 let
235 val xes = map (fn (x, e) => (x, simplify e)) xes
236 in
237 if List.exists (isFinish o #2) xes then
238 Finish
239 else
240 Recd xes
241 end
242 | Proj (e, s) =>
243 (case simplify e of
244 Recd xes =>
245 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
246 | e' =>
247 if isFinish e' then
248 Finish
249 else
250 Proj (e', s))
251 | Finish => Finish 242 | Finish => Finish
252 243
253 datatype atom = 244 datatype atom =
254 AReln of reln * exp list 245 AReln of reln * exp list
255 | ACond of exp * prop 246 | ACond of exp * prop
256 247
257 fun p_atom a = 248 fun p_atom a =
258 p_prop (case a of 249 p_prop (case a of
259 AReln x => Reln x 250 AReln x => Reln x
260 | ACond x => Cond x) 251 | ACond x => Cond x)
252
253 fun lvarIn lv =
254 let
255 fun lvi e =
256 case e of
257 Const _ => false
258 | Var _ => false
259 | Lvar lv' => lv' = lv
260 | Func (_, es) => List.exists lvi es
261 | Recd xes => List.exists (lvi o #2) xes
262 | Proj (e, _) => lvi e
263 | Finish => false
264 in
265 lvi
266 end
267
268 fun lvarInP lv =
269 let
270 fun lvi p =
271 case p of
272 True => false
273 | False => false
274 | Unknown => true
275 | And (p1, p2) => lvi p1 orelse lvi p2
276 | Or (p1, p2) => lvi p1 orelse lvi p2
277 | Reln (_, es) => List.exists (lvarIn lv) es
278 | Cond (e, p) => lvarIn lv e orelse lvi p
279 in
280 lvi
281 end
282
283 fun varIn lv =
284 let
285 fun lvi e =
286 case e of
287 Const _ => false
288 | Lvar _ => false
289 | Var lv' => lv' = lv
290 | Func (_, es) => List.exists lvi es
291 | Recd xes => List.exists (lvi o #2) xes
292 | Proj (e, _) => lvi e
293 | Finish => false
294 in
295 lvi
296 end
297
298 fun varInP lv =
299 let
300 fun lvi p =
301 case p of
302 True => false
303 | False => false
304 | Unknown => false
305 | And (p1, p2) => lvi p1 orelse lvi p2
306 | Or (p1, p2) => lvi p1 orelse lvi p2
307 | Reln (_, es) => List.exists (varIn lv) es
308 | Cond (e, p) => varIn lv e orelse lvi p
309 in
310 lvi
311 end
312
313 fun eq' (e1, e2) =
314 case (e1, e2) of
315 (Const p1, Const p2) => Prim.equal (p1, p2)
316 | (Var n1, Var n2) => n1 = n2
317
318 | (Lvar n1, _) =>
319 (case IM.find (!unif, n1) of
320 SOME e1 => eq' (e1, e2)
321 | NONE =>
322 case e2 of
323 Lvar n2 =>
324 (case IM.find (!unif, n2) of
325 SOME e2 => eq' (e1, e2)
326 | NONE => n1 = n2
327 orelse (unif := IM.insert (!unif, n2, e1);
328 true))
329 | _ =>
330 if lvarIn n1 e2 then
331 false
332 else
333 (unif := IM.insert (!unif, n1, e2);
334 true))
335
336 | (_, Lvar n2) =>
337 (case IM.find (!unif, n2) of
338 SOME e2 => eq' (e1, e2)
339 | NONE =>
340 if lvarIn n2 e1 then
341 false
342 else
343 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
344 ("e1", p_exp e1)];*)
345 unif := IM.insert (!unif, n2, e1);
346 true))
347
348 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
349 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
350 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
351 | (Finish, Finish) => true
352 | _ => false
353
354 fun eq (e1, e2) =
355 let
356 val saved = save ()
357 in
358 if eq' (simplify e1, simplify e2) then
359 true
360 else
361 (restore saved;
362 false)
363 end
364
365 val debug = ref false
366
367 fun eeq (e1, e2) =
368 case (e1, e2) of
369 (Const p1, Const p2) => Prim.equal (p1, p2)
370 | (Var n1, Var n2) => n1 = n2
371 | (Lvar n1, Lvar n2) => n1 = n2
372 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
373 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
374 List.all (fn (x2, e2) =>
375 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
376 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
377 | (Finish, Finish) => true
378 | _ => false
379
380 (* Congruence closure *)
381 structure Cc :> sig
382 type database
383 type representative
384
385 exception Contradiction
386 exception Undetermined
387
388 val database : unit -> database
389 val representative : database * exp -> representative
390
391 val assert : database * atom -> unit
392 val check : database * atom -> bool
393
394 val p_database : database Print.printer
395 end = struct
396
397 exception Contradiction
398 exception Undetermined
399
400 structure CM = BinaryMapFn(struct
401 type ord_key = Prim.t
402 val compare = Prim.compare
403 end)
404
405 datatype node = Node of {Rep : node ref option ref,
406 Cons : node ref SM.map ref,
407 Variety : variety,
408 Known : bool ref}
409
410 and variety =
411 Dt0 of string
412 | Dt1 of string * node ref
413 | Prim of Prim.t
414 | Recrd of node ref SM.map ref
415 | VFinish
416 | Nothing
417
418 type representative = node ref
419
420 val finish = ref (Node {Rep = ref NONE,
421 Cons = ref SM.empty,
422 Variety = VFinish,
423 Known = ref false})
424
425 type database = {Vars : representative IM.map ref,
426 Consts : representative CM.map ref,
427 Con0s : representative SM.map ref,
428 Records : (representative SM.map * representative) list ref,
429 Funcs : ((string * representative list) * representative) list ref }
430
431 fun database () = {Vars = ref IM.empty,
432 Consts = ref CM.empty,
433 Con0s = ref SM.empty,
434 Records = ref [],
435 Funcs = ref []}
436
437 fun unNode n =
438 case !n of
439 Node r => r
440
441 open Print
442 val string = PD.string
443 val newline = PD.newline
444
445 fun p_rep n =
446 case !(#Rep (unNode n)) of
447 SOME n => p_rep n
448 | NONE =>
449 case #Variety (unNode n) of
450 Nothing => string ("?" ^ Int.toString (Unsafe.cast n))
451 | Dt0 s => string ("Dt0(" ^ s ^ ")")
452 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
453 space,
454 p_rep n,
455 string ")"]
456 | Prim p => Prim.p_t p
457 | Recrd (ref m) => box [string "{",
458 p_list (fn (x, n) => box [string x,
459 space,
460 string "=",
461 space,
462 p_rep n]) (SM.listItemsi m),
463 string "}"]
464 | VFinish => string "FINISH"
465
466 fun p_database (db : database) =
467 box [string "Vars:",
468 newline,
469 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
470 space,
471 string "=",
472 space,
473 p_rep n]) (IM.listItemsi (!(#Vars db)))]
474
475 fun repOf (n : representative) : representative =
476 case !(#Rep (unNode n)) of
477 NONE => n
478 | SOME r =>
479 let
480 val r = repOf r
481 in
482 #Rep (unNode n) := SOME r;
483 r
484 end
485
486 fun markKnown r =
487 (#Known (unNode r) := true;
488 case #Variety (unNode r) of
489 Dt1 (_, r) => markKnown r
490 | Recrd xes => SM.app markKnown (!xes)
491 | _ => ())
492
493 fun representative (db : database, e) =
494 let
495 fun rep e =
496 case e of
497 Const p => (case CM.find (!(#Consts db), p) of
498 SOME r => repOf r
499 | NONE =>
500 let
501 val r = ref (Node {Rep = ref NONE,
502 Cons = ref SM.empty,
503 Variety = Prim p,
504 Known = ref false})
505 in
506 #Consts db := CM.insert (!(#Consts db), p, r);
507 r
508 end)
509 | Var n => (case IM.find (!(#Vars db), n) of
510 SOME r => repOf r
511 | NONE =>
512 let
513 val r = ref (Node {Rep = ref NONE,
514 Cons = ref SM.empty,
515 Variety = Nothing,
516 Known = ref false})
517 in
518 #Vars db := IM.insert (!(#Vars db), n, r);
519 r
520 end)
521 | Lvar n =>
522 (case IM.find (!unif, n) of
523 NONE => raise Undetermined
524 | SOME e => rep e)
525 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
526 SOME r => repOf r
527 | NONE =>
528 let
529 val r = ref (Node {Rep = ref NONE,
530 Cons = ref SM.empty,
531 Variety = Dt0 f,
532 Known = ref false})
533 in
534 #Con0s db := SM.insert (!(#Con0s db), f, r);
535 r
536 end)
537 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
538 | Func (DtCon1 f, [e]) =>
539 let
540 val r = rep e
541 in
542 case SM.find (!(#Cons (unNode r)), f) of
543 SOME r => repOf r
544 | NONE =>
545 let
546 val r' = ref (Node {Rep = ref NONE,
547 Cons = ref SM.empty,
548 Variety = Dt1 (f, r),
549 Known = ref false})
550 in
551 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
552 r'
553 end
554 end
555 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
556 | Func (UnCon f, [e]) =>
557 let
558 val r = rep e
559 in
560 case #Variety (unNode r) of
561 Dt1 (f', n) => if f' = f then
562 repOf n
563 else
564 raise Contradiction
565 | Nothing =>
566 let
567 val cons = ref SM.empty
568 val r' = ref (Node {Rep = ref NONE,
569 Cons = cons,
570 Variety = Nothing,
571 Known = ref false})
572
573 val r'' = ref (Node {Rep = ref NONE,
574 Cons = #Cons (unNode r),
575 Variety = Dt1 (f, r'),
576 Known = #Known (unNode r)})
577 in
578 cons := SM.insert (!cons, f, r'');
579 #Rep (unNode r) := SOME r'';
580 r'
581 end
582 | VFinish => r
583 | _ => raise Contradiction
584 end
585 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
586 | Func (Other f, es) =>
587 let
588 val rs = map rep es
589 in
590 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
591 NONE =>
592 let
593 val r = ref (Node {Rep = ref NONE,
594 Cons = ref SM.empty,
595 Variety = Nothing,
596 Known = ref false})
597 in
598 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
599 r
600 end
601 | SOME (_, r) => repOf r
602 end
603 | Recd xes =>
604 let
605 val xes = map (fn (x, e) => (x, rep e)) xes
606 val len = length xes
607 in
608 case List.find (fn (xes', _) =>
609 SM.numItems xes' = len
610 andalso List.all (fn (x, n) =>
611 case SM.find (xes', x) of
612 NONE => false
613 | SOME n' => n = repOf n') xes)
614 (!(#Records db)) of
615 SOME (_, r) => repOf r
616 | NONE =>
617 let
618 val xes = foldl SM.insert' SM.empty xes
619
620 val r' = ref (Node {Rep = ref NONE,
621 Cons = ref SM.empty,
622 Variety = Recrd (ref xes),
623 Known = ref false})
624 in
625 #Records db := (xes, r') :: (!(#Records db));
626 r'
627 end
628 end
629 | Proj (e, f) =>
630 let
631 val r = rep e
632 in
633 case #Variety (unNode r) of
634 Recrd xes =>
635 (case SM.find (!xes, f) of
636 SOME r => repOf r
637 | NONE =>let
638 val r = ref (Node {Rep = ref NONE,
639 Cons = ref SM.empty,
640 Variety = Nothing,
641 Known = ref false})
642 in
643 xes := SM.insert (!xes, f, r);
644 r
645 end)
646 | Nothing =>
647 let
648 val r' = ref (Node {Rep = ref NONE,
649 Cons = ref SM.empty,
650 Variety = Nothing,
651 Known = ref false})
652
653 val r'' = ref (Node {Rep = ref NONE,
654 Cons = #Cons (unNode r),
655 Variety = Recrd (ref (SM.insert (SM.empty, f, r'))),
656 Known = #Known (unNode r)})
657 in
658 #Rep (unNode r) := SOME r'';
659 r'
660 end
661 | VFinish => r
662 | _ => raise Contradiction
663 end
664 | Finish => finish
665 in
666 rep e
667 end
668
669 fun assert (db, a) =
670 case a of
671 ACond _ => ()
672 | AReln x =>
673 case x of
674 (Known, [e]) => markKnown (representative (db, e))
675 | (PCon0 f, [e]) =>
676 let
677 val r = representative (db, e)
678 in
679 case #Variety (unNode r) of
680 Dt0 f' => if f = f' then
681 ()
682 else
683 raise Contradiction
684 | Nothing =>
685 let
686 val r' = ref (Node {Rep = ref NONE,
687 Cons = ref SM.empty,
688 Variety = Dt0 f,
689 Known = ref false})
690 in
691 #Rep (unNode r) := SOME r'
692 end
693 | _ => raise Contradiction
694 end
695 | (PCon1 f, [e]) =>
696 let
697 val r = representative (db, e)
698 in
699 case #Variety (unNode r) of
700 Dt1 (f', e') => if f = f' then
701 ()
702 else
703 raise Contradiction
704 | Nothing =>
705 let
706 val r'' = ref (Node {Rep = ref NONE,
707 Cons = ref SM.empty,
708 Variety = Nothing,
709 Known = ref false})
710
711 val r' = ref (Node {Rep = ref NONE,
712 Cons = ref SM.empty,
713 Variety = Dt1 (f, r''),
714 Known = ref false})
715 in
716 #Rep (unNode r) := SOME r'
717 end
718 | _ => raise Contradiction
719 end
720 | (Eq, [e1, e2]) =>
721 let
722 fun markEq (r1, r2) =
723 if r1 = r2 then
724 ()
725 else case (#Variety (unNode r1), #Variety (unNode r2)) of
726 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
727 ()
728 else
729 raise Contradiction
730 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
731 ()
732 else
733 raise Contradiction
734 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
735 markEq (r1, r2)
736 else
737 raise Contradiction
738 | (Recrd xes1, Recrd xes2) =>
739 let
740 fun unif (xes1, xes2) =
741 SM.appi (fn (x, r1) =>
742 case SM.find (xes2, x) of
743 NONE => ()
744 | SOME r2 => markEq (r1, r2)) xes1
745 in
746 unif (!xes1, !xes2);
747 unif (!xes2, !xes1)
748 end
749 | (VFinish, VFinish) => ()
750 | (Nothing, _) =>
751 (#Rep (unNode r1) := SOME r2;
752 if !(#Known (unNode r1)) andalso not (!(#Known (unNode r2))) then
753 markKnown r2
754 else
755 ();
756 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
757 compactFuncs ())
758 | (_, Nothing) =>
759 (#Rep (unNode r2) := SOME r1;
760 if !(#Known (unNode r2)) andalso not (!(#Known (unNode r1))) then
761 markKnown r1
762 else
763 ();
764 #Cons (unNode r1) := SM.unionWith #1 (!(#Cons (unNode r1)), !(#Cons (unNode r2)));
765 compactFuncs ())
766 | _ => raise Contradiction
767
768 and compactFuncs () =
769 let
770 fun loop funcs =
771 case funcs of
772 [] => []
773 | (fr as ((f, rs), r)) :: rest =>
774 let
775 val rest = List.filter (fn ((f' : string, rs'), r') =>
776 if f' = f
777 andalso ListPair.allEq (fn (r1, r2) =>
778 repOf r1 = repOf r2)
779 (rs, rs') then
780 (markEq (r, r');
781 false)
782 else
783 true) rest
784 in
785 fr :: loop rest
786 end
787 in
788 #Funcs db := loop (!(#Funcs db))
789 end
790 in
791 markEq (representative (db, e1), representative (db, e2))
792 end
793 | _ => ()
794
795 fun check (db, a) =
796 case a of
797 ACond _ => false
798 | AReln x =>
799 case x of
800 (Known, [e]) => !(#Known (unNode (representative (db, e))))
801 | (PCon0 f, [e]) =>
802 (case #Variety (unNode (representative (db, e))) of
803 Dt0 f' => f' = f
804 | _ => false)
805 | (PCon1 f, [e]) =>
806 (case #Variety (unNode (representative (db, e))) of
807 Dt1 (f', _) => f' = f
808 | _ => false)
809 | (Eq, [e1, e2]) =>
810 let
811 val r1 = representative (db, e1)
812 val r2 = representative (db, e2)
813 in
814 repOf r1 = repOf r2
815 end
816 | _ => false
817
818 end
261 819
262 fun decomp fals or = 820 fun decomp fals or =
263 let 821 let
264 fun decomp p k = 822 fun decomp p k =
265 case p of 823 case p of
276 | Cond x => k [ACond x] 834 | Cond x => k [ACond x]
277 in 835 in
278 decomp 836 decomp
279 end 837 end
280 838
281 fun lvarIn lv =
282 let
283 fun lvi e =
284 case e of
285 Const _ => false
286 | Var _ => false
287 | Lvar lv' => lv' = lv
288 | Func (_, es) => List.exists lvi es
289 | Recd xes => List.exists (lvi o #2) xes
290 | Proj (e, _) => lvi e
291 | Finish => false
292 in
293 lvi
294 end
295
296 fun lvarInP lv =
297 let
298 fun lvi p =
299 case p of
300 True => false
301 | False => false
302 | Unknown => true
303 | And (p1, p2) => lvi p1 orelse lvi p2
304 | Or (p1, p2) => lvi p1 orelse lvi p2
305 | Reln (_, es) => List.exists (lvarIn lv) es
306 | Cond (e, p) => lvarIn lv e orelse lvi p
307 in
308 lvi
309 end
310
311 fun varIn lv =
312 let
313 fun lvi e =
314 case e of
315 Const _ => false
316 | Lvar _ => false
317 | Var lv' => lv' = lv
318 | Func (_, es) => List.exists lvi es
319 | Recd xes => List.exists (lvi o #2) xes
320 | Proj (e, _) => lvi e
321 | Finish => false
322 in
323 lvi
324 end
325
326 fun varInP lv =
327 let
328 fun lvi p =
329 case p of
330 True => false
331 | False => false
332 | Unknown => false
333 | And (p1, p2) => lvi p1 orelse lvi p2
334 | Or (p1, p2) => lvi p1 orelse lvi p2
335 | Reln (_, es) => List.exists (varIn lv) es
336 | Cond (e, p) => varIn lv e orelse lvi p
337 in
338 lvi
339 end
340
341 fun eq' (e1, e2) =
342 case (e1, e2) of
343 (Const p1, Const p2) => Prim.equal (p1, p2)
344 | (Var n1, Var n2) => n1 = n2
345
346 | (Lvar n1, _) =>
347 (case IM.find (!unif, n1) of
348 SOME e1 => eq' (e1, e2)
349 | NONE =>
350 case e2 of
351 Lvar n2 =>
352 (case IM.find (!unif, n2) of
353 SOME e2 => eq' (e1, e2)
354 | NONE => n1 = n2
355 orelse (unif := IM.insert (!unif, n2, e1);
356 true))
357 | _ =>
358 if lvarIn n1 e2 then
359 false
360 else
361 (unif := IM.insert (!unif, n1, e2);
362 true))
363
364 | (_, Lvar n2) =>
365 (case IM.find (!unif, n2) of
366 SOME e2 => eq' (e1, e2)
367 | NONE =>
368 if lvarIn n2 e1 then
369 false
370 else
371 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
372 ("e1", p_exp e1)];*)
373 unif := IM.insert (!unif, n2, e1);
374 true))
375
376 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
377 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
378 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
379 | (Finish, Finish) => true
380 | _ => false
381
382 fun eq (e1, e2) =
383 let
384 val saved = save ()
385 in
386 if eq' (simplify e1, simplify e2) then
387 true
388 else
389 (restore saved;
390 false)
391 end
392
393 val debug = ref false
394
395 fun eeq (e1, e2) =
396 case (e1, e2) of
397 (Const p1, Const p2) => Prim.equal (p1, p2)
398 | (Var n1, Var n2) => n1 = n2
399 | (Lvar n1, Lvar n2) => n1 = n2
400 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
401 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
402 List.all (fn (x2, e2) =>
403 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
404 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
405 | (Finish, Finish) => true
406 | _ => false
407
408 (* Congruence closure *)
409 structure Cc :> sig
410 type t
411 val empty : t
412 val assert : t * exp * exp -> t
413 val query : t * exp * exp -> bool
414 val allPeers : t * exp -> exp list
415 val p_t : t Print.printer
416 end = struct
417
418 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
419
420 type t = (exp * exp) list
421
422 val empty = []
423
424 fun lookup (t, e) =
425 case List.find (fn (e', _) => eq (e', e)) t of
426 NONE => e
427 | SOME (_, e2) => lookup (t, e2)
428
429 fun allPeers (t, e) =
430 let
431 val r = lookup (t, e)
432 in
433 r :: List.mapPartial (fn (e1, e2) =>
434 let
435 val r' = lookup (t, e2)
436 in
437 if eq (r, r') then
438 SOME e1
439 else
440 NONE
441 end) t
442 end
443
444 open Print
445
446 val p_t = p_list (fn (e1, e2) => box [p_exp (simplify e1),
447 space,
448 PD.string "->",
449 space,
450 p_exp (simplify e2)])
451
452 fun query (t, e1, e2) =
453 let
454 fun doUn e =
455 case e of
456 Func (f, [e1]) =>
457 if String.isPrefix "un" f then
458 let
459 val s = String.extract (f, 2, NONE)
460 in
461 case ListUtil.search (fn e =>
462 case e of
463 Func (f', [e']) =>
464 if f' = s then
465 SOME e'
466 else
467 NONE
468 | _ => NONE) (allPeers (t, e1)) of
469 NONE => e
470 | SOME e => doUn e
471 end
472 else
473 e
474 | _ => e
475
476 val e1' = doUn (lookup (t, doUn (simplify e1)))
477 val e2' = doUn (lookup (t, doUn (simplify e2)))
478 in
479 (*prefaces "CC query" [("e1", p_exp (simplify e1)),
480 ("e2", p_exp (simplify e2)),
481 ("e1'", p_exp (simplify e1')),
482 ("e2'", p_exp (simplify e2')),
483 ("t", p_t t)];*)
484 eq (e1', e2')
485 end
486
487 fun assert (t, e1, e2) =
488 let
489 val r1 = lookup (t, e1)
490 val r2 = lookup (t, e2)
491 in
492 if eq (r1, r2) then
493 t
494 else
495 let
496 fun doUn (t, e1, e2) =
497 case e1 of
498 Func (f, [e]) => if String.isPrefix "un" f then
499 let
500 val s = String.extract (f, 2, NONE)
501 in
502 foldl (fn (e', t) =>
503 case e' of
504 Func (f', [e']) =>
505 if f' = s then
506 assert (assert (t, e', e1), e', e2)
507 else
508 t
509 | _ => t) t (allPeers (t, e))
510 end
511 else
512 t
513 | _ => t
514
515 fun doProj (t, e1, e2) =
516 foldl (fn ((e1', e2'), t) =>
517 let
518 fun doOne (e, t) =
519 case e of
520 Proj (e', f) =>
521 if query (t, e1, e') then
522 assert (t, e, Proj (e2, f))
523 else
524 t
525 | _ => t
526 in
527 doOne (e1', doOne (e2', t))
528 end) t t
529
530 val t = (r1, r2) :: t
531 val t = doUn (t, r1, r2)
532 val t = doUn (t, r2, r1)
533 val t = doProj (t, r1, r2)
534 val t = doProj (t, r2, r1)
535 in
536 t
537 end
538 end
539
540 end
541
542 fun rimp cc ((r1, es1), (r2, es2)) =
543 case (r1, r2) of
544 (Sql r1', Sql r2') =>
545 r1' = r2' andalso
546 (case (es1, es2) of
547 ([e1], [e2]) => eq (e1, e2)
548 | _ => false)
549 | (Eq, Eq) =>
550 (case (es1, es2) of
551 ([x1, y1], [x2, y2]) =>
552 let
553 val saved = save ()
554 in
555 if eq (x1, x2) andalso eq (y1, y2) then
556 true
557 else
558 (restore saved;
559 if eq (x1, y2) andalso eq (y1, x2) then
560 true
561 else
562 (restore saved;
563 false))
564 end
565 | _ => false)
566 | (Known, Known) =>
567 (case (es1, es2) of
568 ([Var v], [e2]) =>
569 let
570 fun matches e =
571 case e of
572 Var v' => v' = v
573 | Proj (e, _) => matches e
574 | Func (f, [e]) => String.isPrefix "un" f andalso matches e
575 | _ => false
576 in
577 (*Print.prefaces "Checking peers" [("e2", p_exp e2),
578 ("peers", Print.p_list p_exp (Cc.allPeers (cc, e2))),
579 ("db", Cc.p_t cc)];*)
580 List.exists matches (Cc.allPeers (cc, e2))
581 end
582 | _ => false)
583 | _ => false
584
585 fun imply (p1, p2) = 839 fun imply (p1, p2) =
586 let 840 (reset ();
587 fun doOne doKnown = 841 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
588 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 842 (fn hyps =>
589 (fn hyps => 843 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
590 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 844 (fn goals =>
591 (fn goals => 845 let
592 let 846 fun gls goals onFail acc =
593 val cc = foldl (fn (p, cc) => 847 case goals of
594 case p of 848 [] =>
595 AReln (Eq, [e1, e2]) => Cc.assert (cc, e1, e2) 849 (let
596 | _ => cc) Cc.empty hyps 850 val cc = Cc.database ()
597 851 val () = app (fn a => Cc.assert (cc, a)) hyps
598 fun gls goals onFail = 852 in
599 case goals of 853 (List.all (fn a =>
600 [] => true 854 if Cc.check (cc, a) then
601 | ACond _ :: _ => false 855 true
602 | AReln g :: goals => 856 else
603 case (doKnown, g) of 857 ((*Print.prefaces "Can't prove"
604 (false, (Known, _)) => gls goals onFail 858 [("a", p_atom a),
605 | _ => 859 ("hyps", Print.p_list p_atom hyps),
606 let 860 ("db", Cc.p_database cc)];*)
607 fun hps hyps = 861 false)) acc
608 case hyps of 862 orelse onFail ())
609 [] => ((*Print.prefaces "Fail" [("g", p_prop (Reln g)), 863 handle Cc.Contradiction => onFail ()
610 ("db", Cc.p_t cc)];*) 864 end handle Cc.Undetermined => onFail ())
611 onFail ()) 865 | AReln (Sql gf, [ge]) :: goals =>
612 | ACond _ :: hyps => hps hyps 866 let
613 | AReln h :: hyps => 867 fun hps hyps =
614 let 868 case hyps of
615 val saved = save () 869 [] => onFail ()
616 in 870 | AReln (Sql hf, [he]) :: hyps =>
617 if rimp cc (h, g) then 871 if gf = hf then
618 let 872 let
619 val changed = IM.numItems (!unif) 873 val saved = save ()
620 <> IM.numItems saved 874 in
621 in 875 if eq (ge, he) then
622 gls goals (fn () => (restore saved; 876 let
623 changed (*andalso 877 val changed = IM.numItems (!unif)
624 (Print.preface ("Retry", 878 <> IM.numItems saved
625 p_prop 879 in
626 (Reln g) 880 gls goals (fn () => (restore saved;
627 ); true)*) 881 changed
628 andalso hps hyps)) 882 andalso hps hyps))
629 end 883 acc
630 else 884 end
631 hps hyps 885 else
632 end 886 hps hyps
633 in 887 end
634 (case g of 888 else
635 (Eq, [e1, e2]) => Cc.query (cc, e1, e2) 889 hps hyps
636 | _ => false) 890 | _ :: hyps => hps hyps
637 orelse hps hyps 891 in
638 end 892 hps hyps
639 in 893 end
640 if List.exists (fn AReln (DtCon c1, [e]) => 894 | g :: goals => gls goals onFail (g :: acc)
641 List.exists (fn AReln (DtCon c2, [e']) => 895 in
642 c1 <> c2 andalso 896 gls goals (fn () => false) []
643 Cc.query (cc, e, e') 897 end handle Cc.Contradiction => true)))
644 | _ => false) hyps
645 orelse List.exists (fn Func (c2, []) => c1 <> c2
646 | Finish => true
647 | _ => false)
648 (Cc.allPeers (cc, e))
649 | _ => false) hyps
650 orelse gls goals (fn () => false) then
651 true
652 else
653 ((*Print.prefaces "Can't prove"
654 [("hyps", Print.p_list p_atom hyps),
655 ("goals", Print.p_list p_atom goals)];*)
656 false)
657 end))
658 in
659 reset ();
660 doOne false;
661 doOne true
662 end
663 898
664 fun patCon pc = 899 fun patCon pc =
665 case pc of 900 case pc of
666 PConVar n => "C" ^ Int.toString n 901 PConVar n => "C" ^ Int.toString n
667 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 902 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
951 1186
952 val query = log "query" 1187 val query = log "query"
953 (wrap (follow (follow select from) (opt wher)) 1188 (wrap (follow (follow select from) (opt wher))
954 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) 1189 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
955 1190
956 fun removeDups ls = 1191 fun removeDups (ls : (string * string) list) =
957 case ls of 1192 case ls of
958 [] => [] 1193 [] => []
959 | x :: ls => 1194 | x :: ls =>
960 let 1195 let
961 val ls = removeDups ls 1196 val ls = removeDups ls
1027 in 1262 in
1028 inl (deinj e) 1263 inl (deinj e)
1029 end 1264 end
1030 | SqFunc (f, e) => 1265 | SqFunc (f, e) =>
1031 inl (case expIn e of 1266 inl (case expIn e of
1032 inl e => Func (f, [e]) 1267 inl e => Func (Other f, [e])
1033 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f)) 1268 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
1034 | Count => inl count 1269 | Count => inl count
1035 1270
1036 val p = case #Where r of 1271 val p = case #Where r of
1037 NONE => p 1272 NONE => p
1079 fun evalPat env e (pt, _) = 1314 fun evalPat env e (pt, _) =
1080 case pt of 1315 case pt of
1081 PWild => (env, True) 1316 PWild => (env, True)
1082 | PVar _ => (e :: env, True) 1317 | PVar _ => (e :: env, True)
1083 | PPrim _ => (env, True) 1318 | PPrim _ => (env, True)
1084 | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e])) 1319 | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
1085 | PCon (_, pc, SOME pt) => 1320 | PCon (_, pc, SOME pt) =>
1086 let 1321 let
1087 val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt 1322 val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
1088 in 1323 in
1089 (env, And (p, Reln (DtCon (patCon pc), [e]))) 1324 (env, And (p, Reln (PCon1 (patCon pc), [e])))
1090 end 1325 end
1091 | PRecord xpts => 1326 | PRecord xpts =>
1092 foldl (fn ((x, pt, _), (env, p)) => 1327 foldl (fn ((x, pt, _), (env, p)) =>
1093 let 1328 let
1094 val (env, p') = evalPat env (Proj (e, x)) pt 1329 val (env, p') = evalPat env (Proj (e, x)) pt
1095 in 1330 in
1096 (env, And (p', p)) 1331 (env, And (p', p))
1097 end) (env, True) xpts 1332 end) (env, True) xpts
1098 | PNone _ => (env, Reln (DtCon "None", [e])) 1333 | PNone _ => (env, Reln (PCon0 "None", [e]))
1099 | PSome (_, pt) => 1334 | PSome (_, pt) =>
1100 let 1335 let
1101 val (env, p) = evalPat env (Func ("unSome", [e])) pt 1336 val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
1102 in 1337 in
1103 (env, And (p, Reln (DtCon "Some", [e]))) 1338 (env, And (p, Reln (PCon1 "Some", [e])))
1104 end 1339 end
1105 1340
1106 fun peq (p1, p2) = 1341 fun peq (p1, p2) =
1107 case (p1, p2) of 1342 case (p1, p2) of
1108 (True, True) => true 1343 (True, True) => true
1143 in 1378 in
1144 case #1 e of 1379 case #1 e of
1145 EPrim p => (Const p, st) 1380 EPrim p => (Const p, st)
1146 | ERel n => (List.nth (env, n), st) 1381 | ERel n => (List.nth (env, n), st)
1147 | ENamed _ => default () 1382 | ENamed _ => default ()
1148 | ECon (_, pc, NONE) => (Func (patCon pc, []), st) 1383 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
1149 | ECon (_, pc, SOME e) => 1384 | ECon (_, pc, SOME e) =>
1150 let 1385 let
1151 val (e, st) = evalExp env (e, st) 1386 val (e, st) = evalExp env (e, st)
1152 in 1387 in
1153 (Func (patCon pc, [e]), st) 1388 (Func (DtCon1 (patCon pc), [e]), st)
1154 end 1389 end
1155 | ENone _ => (Func ("None", []), st) 1390 | ENone _ => (Func (DtCon0 "None", []), st)
1156 | ESome (_, e) => 1391 | ESome (_, e) =>
1157 let 1392 let
1158 val (e, st) = evalExp env (e, st) 1393 val (e, st) = evalExp env (e, st)
1159 in 1394 in
1160 (Func ("Some", [e]), st) 1395 (Func (DtCon1 "Some", [e]), st)
1161 end 1396 end
1162 | EFfi _ => default () 1397 | EFfi _ => default ()
1163 1398
1164 | EFfiApp (m, s, es) => 1399 | EFfiApp (m, s, es) =>
1165 if m = "Basis" andalso SS.member (writers, s) then 1400 if m = "Basis" andalso SS.member (writers, s) then
1172 default () 1407 default ()
1173 else 1408 else
1174 let 1409 let
1175 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1410 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1176 in 1411 in
1177 (Func (m ^ "." ^ s, es), st) 1412 (Func (Other (m ^ "." ^ s), es), st)
1178 end 1413 end
1179 1414
1180 | EApp (e1, e2) => 1415 | EApp (e1, e2) =>
1181 let 1416 let
1182 val (e1, st) = evalExp env (e1, st) 1417 val (e1, st) = evalExp env (e1, st)
1189 | EAbs _ => default () 1424 | EAbs _ => default ()
1190 | EUnop (s, e1) => 1425 | EUnop (s, e1) =>
1191 let 1426 let
1192 val (e1, st) = evalExp env (e1, st) 1427 val (e1, st) = evalExp env (e1, st)
1193 in 1428 in
1194 (Func (s, [e1]), st) 1429 (Func (Other s, [e1]), st)
1195 end 1430 end
1196 | EBinop (s, e1, e2) => 1431 | EBinop (s, e1, e2) =>
1197 let 1432 let
1198 val (e1, st) = evalExp env (e1, st) 1433 val (e1, st) = evalExp env (e1, st)
1199 val (e2, st) = evalExp env (e2, st) 1434 val (e2, st) = evalExp env (e2, st)
1200 in 1435 in
1201 (Func (s, [e1, e2]), st) 1436 (Func (Other s, [e1, e2]), st)
1202 end 1437 end
1203 | ERecord xets => 1438 | ERecord xets =>
1204 let 1439 let
1205 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) => 1440 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
1206 let 1441 let
1239 | EStrcat (e1, e2) => 1474 | EStrcat (e1, e2) =>
1240 let 1475 let
1241 val (e1, st) = evalExp env (e1, st) 1476 val (e1, st) = evalExp env (e1, st)
1242 val (e2, st) = evalExp env (e2, st) 1477 val (e2, st) = evalExp env (e2, st)
1243 in 1478 in
1244 (Func ("cat", [e1, e2]), st) 1479 (Func (Other "cat", [e1, e2]), st)
1245 end 1480 end
1246 | EError _ => (Finish, st) 1481 | EError _ => (Finish, st)
1247 | EReturnBlob {blob = b, mimeType = m, ...} => 1482 | EReturnBlob {blob = b, mimeType = m, ...} =>
1248 let 1483 let
1249 val (b, st) = evalExp env (b, st) 1484 val (b, st) = evalExp env (b, st)
1277 end 1512 end
1278 | EClosure (n, es) => 1513 | EClosure (n, es) =>
1279 let 1514 let
1280 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1515 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1281 in 1516 in
1282 (Func ("Cl" ^ Int.toString n, es), st) 1517 (Func (Other ("Cl" ^ Int.toString n), es), st)
1283 end 1518 end
1284 1519
1285 | EQuery {query = q, body = b, initial = i, ...} => 1520 | EQuery {query = q, body = b, initial = i, ...} =>
1286 let 1521 let
1287 val (_, st) = evalExp env (q, st) 1522 val (_, st) = evalExp env (q, st)
1407 fun doAll e = 1642 fun doAll e =
1408 case e of 1643 case e of
1409 Const _ => () 1644 Const _ => ()
1410 | Var _ => doOne e 1645 | Var _ => doOne e
1411 | Lvar _ => raise Fail "Iflow.doAll: Lvar" 1646 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
1412 | Func (f, es) => if String.isPrefix "un" f then 1647 | Func (UnCon _, [e]) => doOne e
1413 doOne e 1648 | Func (_, es) => app doAll es
1414 else
1415 app doAll es
1416 | Recd xes => app (doAll o #2) xes 1649 | Recd xes => app (doAll o #2) xes
1417 | Proj _ => doOne e 1650 | Proj _ => doOne e
1418 | Finish => () 1651 | Finish => ()
1419 in 1652 in
1420 doAll e 1653 doAll e