summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-08 12:46:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-08 12:46:21 -0400
commit6768acc57c8aea2a48a51d38f69596fd3e5cb1e0 (patch)
tree3a35eb51d05a2144c4c47d148f16352a803fae78
parented25721e17d6798aad7b7a0cea8e5393bb840a91 (diff)
Implemented proper congruence closure, to the point where tests/policy works
-rw-r--r--src/iflow.sml871
1 files changed, 552 insertions, 319 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index e49700cf..d1f36a96 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -32,10 +32,13 @@ open Mono
structure IS = IntBinarySet
structure IM = IntBinaryMap
-structure SS = BinarySetFn(struct
- type ord_key = string
- val compare = String.compare
- end)
+structure SK = struct
+type ord_key = string
+val compare = String.compare
+end
+
+structure SS = BinarySetFn(SK)
+structure SM = BinaryMapFn(SK)
val writers = ["htmlifyInt_w",
"htmlifyFloat_w",
@@ -56,11 +59,17 @@ val writers = SS.addList (SS.empty, writers)
type lvar = int
+datatype func =
+ DtCon0 of string
+ | DtCon1 of string
+ | UnCon of string
+ | Other of string
+
datatype exp =
Const of Prim.t
| Var of int
| Lvar of lvar
- | Func of string * exp list
+ | Func of func * exp list
| Recd of (string * exp) list
| Proj of exp * string
| Finish
@@ -68,7 +77,8 @@ datatype exp =
datatype reln =
Known
| Sql of string
- | DtCon of string
+ | PCon0 of string
+ | PCon1 of string
| Eq
| Ne
| Lt
@@ -85,17 +95,34 @@ datatype prop =
| Reln of reln * exp list
| Cond of exp * prop
+val unif = ref (IM.empty : exp IM.map)
+
+fun reset () = unif := IM.empty
+fun save () = !unif
+fun restore x = unif := x
+
local
open Print
val string = PD.string
in
+fun p_func f =
+ string (case f of
+ DtCon0 s => s
+ | DtCon1 s => s
+ | UnCon s => "un" ^ s
+ | Other s => s)
+
fun p_exp e =
case e of
Const p => Prim.p_t p
| Var n => string ("x" ^ Int.toString n)
- | Lvar n => string ("X" ^ Int.toString n)
- | Func (f, es) => box [string (f ^ "("),
+ | Lvar n =>
+ (case IM.find (!unif, n) of
+ NONE => string ("X" ^ Int.toString n)
+ | SOME e => p_exp e)
+ | Func (f, es) => box [p_func f,
+ string "(",
p_list p_exp es,
string ")"]
| Recd xes => box [string "{",
@@ -129,7 +156,10 @@ fun p_reln r es =
| Sql s => box [string (s ^ "("),
p_list p_exp es,
string ")"]
- | DtCon s => box [string (s ^ "("),
+ | PCon0 s => box [string (s ^ "("),
+ p_list p_exp es,
+ string ")"]
+ | PCon1 s => box [string (s ^ "("),
p_list p_exp es,
string ")"]
| Eq => p_bop "=" es
@@ -198,12 +228,6 @@ fun isFinish e =
Finish => true
| _ => false
-val unif = ref (IM.empty : exp IM.map)
-
-fun reset () = unif := IM.empty
-fun save () = !unif
-fun restore x = unif := x
-
fun simplify e =
case e of
Const _ => e
@@ -212,42 +236,9 @@ fun simplify e =
(case IM.find (!unif, n) of
NONE => e
| SOME e => simplify e)
- | Func (f, es) =>
- let
- val es = map simplify es
-
- fun default () = Func (f, es)
- in
- if List.exists isFinish es then
- Finish
- else if String.isPrefix "un" f then
- case es of
- [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then
- e
- else
- default ()
- | _ => default ()
- else
- default ()
- end
- | Recd xes =>
- let
- val xes = map (fn (x, e) => (x, simplify e)) xes
- in
- if List.exists (isFinish o #2) xes then
- Finish
- else
- Recd xes
- end
- | Proj (e, s) =>
- (case simplify e of
- Recd xes =>
- getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
- | e' =>
- if isFinish e' then
- Finish
- else
- Proj (e', s))
+ | Func (f, es) => Func (f, map simplify es)
+ | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
+ | Proj (e, s) => Proj (simplify e, s)
| Finish => Finish
datatype atom =
@@ -259,25 +250,6 @@ fun p_atom a =
AReln x => Reln x
| ACond x => Cond x)
-fun decomp fals or =
- let
- fun decomp p k =
- case p of
- True => k []
- | False => fals
- | Unknown => k []
- | And (p1, p2) =>
- decomp p1 (fn ps1 =>
- decomp p2 (fn ps2 =>
- k (ps1 @ ps2)))
- | Or (p1, p2) =>
- or (decomp p1 k, fn () => decomp p2 k)
- | Reln x => k [AReln x]
- | Cond x => k [ACond x]
- in
- decomp
- end
-
fun lvarIn lv =
let
fun lvi e =
@@ -407,260 +379,523 @@ fun eeq (e1, e2) =
(* Congruence closure *)
structure Cc :> sig
- type t
- val empty : t
- val assert : t * exp * exp -> t
- val query : t * exp * exp -> bool
- val allPeers : t * exp -> exp list
- val p_t : t Print.printer
-end = struct
+ type database
+ type representative
-fun eq (e1, e2) = eeq (simplify e1, simplify e2)
+ exception Contradiction
+ exception Undetermined
-type t = (exp * exp) list
+ val database : unit -> database
+ val representative : database * exp -> representative
-val empty = []
+ val assert : database * atom -> unit
+ val check : database * atom -> bool
-fun lookup (t, e) =
- case List.find (fn (e', _) => eq (e', e)) t of
- NONE => e
- | SOME (_, e2) => lookup (t, e2)
+ val p_database : database Print.printer
+end = struct
-fun allPeers (t, e) =
- let
- val r = lookup (t, e)
- in
- r :: List.mapPartial (fn (e1, e2) =>
- let
- val r' = lookup (t, e2)
- in
- if eq (r, r') then
- SOME e1
- else
- NONE
- end) t
- end
+exception Contradiction
+exception Undetermined
+
+structure CM = BinaryMapFn(struct
+ type ord_key = Prim.t
+ val compare = Prim.compare
+ end)
+
+datatype node = Node of {Rep : node ref option ref,
+ Cons : node ref SM.map ref,
+ Variety : variety,
+ Known : bool ref}
+
+ and variety =
+ Dt0 of string
+ | Dt1 of string * node ref
+ | Prim of Prim.t
+ | Recrd of node ref SM.map ref
+ | VFinish
+ | Nothing
+
+type representative = node ref
+
+val finish = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = VFinish,
+ Known = ref false})
+
+type database = {Vars : representative IM.map ref,
+ Consts : representative CM.map ref,
+ Con0s : representative SM.map ref,
+ Records : (representative SM.map * representative) list ref,
+ Funcs : ((string * representative list) * representative) list ref }
+
+fun database () = {Vars = ref IM.empty,
+ Consts = ref CM.empty,
+ Con0s = ref SM.empty,
+ Records = ref [],
+ Funcs = ref []}
+
+fun unNode n =
+ case !n of
+ Node r => r
open Print
+val string = PD.string
+val newline = PD.newline
+
+fun p_rep n =
+ case !(#Rep (unNode n)) of
+ SOME n => p_rep n
+ | NONE =>
+ case #Variety (unNode n) of
+ Nothing => string ("?" ^ Int.toString (Unsafe.cast n))
+ | Dt0 s => string ("Dt0(" ^ s ^ ")")
+ | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
+ space,
+ p_rep n,
+ string ")"]
+ | Prim p => Prim.p_t p
+ | Recrd (ref m) => box [string "{",
+ p_list (fn (x, n) => box [string x,
+ space,
+ string "=",
+ space,
+ p_rep n]) (SM.listItemsi m),
+ string "}"]
+ | VFinish => string "FINISH"
+
+fun p_database (db : database) =
+ box [string "Vars:",
+ newline,
+ p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
+ space,
+ string "=",
+ space,
+ p_rep n]) (IM.listItemsi (!(#Vars db)))]
+
+fun repOf (n : representative) : representative =
+ case !(#Rep (unNode n)) of
+ NONE => n
+ | SOME r =>
+ let
+ val r = repOf r
+ in
+ #Rep (unNode n) := SOME r;
+ r
+ end
-val p_t = p_list (fn (e1, e2) => box [p_exp (simplify e1),
- space,
- PD.string "->",
- space,
- p_exp (simplify e2)])
+fun markKnown r =
+ (#Known (unNode r) := true;
+ case #Variety (unNode r) of
+ Dt1 (_, r) => markKnown r
+ | Recrd xes => SM.app markKnown (!xes)
+ | _ => ())
-fun query (t, e1, e2) =
+fun representative (db : database, e) =
let
- fun doUn e =
+ fun rep e =
case e of
- Func (f, [e1]) =>
- if String.isPrefix "un" f then
- let
- val s = String.extract (f, 2, NONE)
- in
- case ListUtil.search (fn e =>
- case e of
- Func (f', [e']) =>
- if f' = s then
- SOME e'
- else
- NONE
- | _ => NONE) (allPeers (t, e1)) of
- NONE => e
- | SOME e => doUn e
- end
- else
- e
- | _ => e
+ Const p => (case CM.find (!(#Consts db), p) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Prim p,
+ Known = ref false})
+ in
+ #Consts db := CM.insert (!(#Consts db), p, r);
+ r
+ end)
+ | Var n => (case IM.find (!(#Vars db), n) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false})
+ in
+ #Vars db := IM.insert (!(#Vars db), n, r);
+ r
+ end)
+ | Lvar n =>
+ (case IM.find (!unif, n) of
+ NONE => raise Undetermined
+ | SOME e => rep e)
+ | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt0 f,
+ Known = ref false})
+ in
+ #Con0s db := SM.insert (!(#Con0s db), f, r);
+ r
+ end)
+ | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
+ | Func (DtCon1 f, [e]) =>
+ let
+ val r = rep e
+ in
+ case SM.find (!(#Cons (unNode r)), f) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt1 (f, r),
+ Known = ref false})
+ in
+ #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
+ r'
+ end
+ end
+ | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
+ | Func (UnCon f, [e]) =>
+ let
+ val r = rep e
+ in
+ case #Variety (unNode r) of
+ Dt1 (f', n) => if f' = f then
+ repOf n
+ else
+ raise Contradiction
+ | Nothing =>
+ let
+ val cons = ref SM.empty
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = cons,
+ Variety = Nothing,
+ Known = ref false})
+
+ val r'' = ref (Node {Rep = ref NONE,
+ Cons = #Cons (unNode r),
+ Variety = Dt1 (f, r'),
+ Known = #Known (unNode r)})
+ in
+ cons := SM.insert (!cons, f, r'');
+ #Rep (unNode r) := SOME r'';
+ r'
+ end
+ | VFinish => r
+ | _ => raise Contradiction
+ end
+ | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
+ | Func (Other f, es) =>
+ let
+ val rs = map rep es
+ in
+ case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
+ NONE =>
+ let
+ val r = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false})
+ in
+ #Funcs db := ((f, rs), r) :: (!(#Funcs db));
+ r
+ end
+ | SOME (_, r) => repOf r
+ end
+ | Recd xes =>
+ let
+ val xes = map (fn (x, e) => (x, rep e)) xes
+ val len = length xes
+ in
+ case List.find (fn (xes', _) =>
+ SM.numItems xes' = len
+ andalso List.all (fn (x, n) =>
+ case SM.find (xes', x) of
+ NONE => false
+ | SOME n' => n = repOf n') xes)
+ (!(#Records db)) of
+ SOME (_, r) => repOf r
+ | NONE =>
+ let
+ val xes = foldl SM.insert' SM.empty xes
- val e1' = doUn (lookup (t, doUn (simplify e1)))
- val e2' = doUn (lookup (t, doUn (simplify e2)))
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Recrd (ref xes),
+ Known = ref false})
+ in
+ #Records db := (xes, r') :: (!(#Records db));
+ r'
+ end
+ end
+ | Proj (e, f) =>
+ let
+ val r = rep e
+ in
+ case #Variety (unNode r) of
+ Recrd xes =>
+ (case SM.find (!xes, f) of
+ SOME r => repOf r
+ | NONE =>let
+ val r = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false})
+ in
+ xes := SM.insert (!xes, f, r);
+ r
+ end)
+ | Nothing =>
+ let
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false})
+
+ val r'' = ref (Node {Rep = ref NONE,
+ Cons = #Cons (unNode r),
+ Variety = Recrd (ref (SM.insert (SM.empty, f, r'))),
+ Known = #Known (unNode r)})
+ in
+ #Rep (unNode r) := SOME r'';
+ r'
+ end
+ | VFinish => r
+ | _ => raise Contradiction
+ end
+ | Finish => finish
in
- (*prefaces "CC query" [("e1", p_exp (simplify e1)),
- ("e2", p_exp (simplify e2)),
- ("e1'", p_exp (simplify e1')),
- ("e2'", p_exp (simplify e2')),
- ("t", p_t t)];*)
- eq (e1', e2')
+ rep e
end
-fun assert (t, e1, e2) =
- let
- val r1 = lookup (t, e1)
- val r2 = lookup (t, e2)
- in
- if eq (r1, r2) then
- t
- else
+fun assert (db, a) =
+ case a of
+ ACond _ => ()
+ | AReln x =>
+ case x of
+ (Known, [e]) => markKnown (representative (db, e))
+ | (PCon0 f, [e]) =>
let
- fun doUn (t, e1, e2) =
- case e1 of
- Func (f, [e]) => if String.isPrefix "un" f then
- let
- val s = String.extract (f, 2, NONE)
- in
- foldl (fn (e', t) =>
- case e' of
- Func (f', [e']) =>
- if f' = s then
- assert (assert (t, e', e1), e', e2)
+ val r = representative (db, e)
+ in
+ case #Variety (unNode r) of
+ Dt0 f' => if f = f' then
+ ()
+ else
+ raise Contradiction
+ | Nothing =>
+ let
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt0 f,
+ Known = ref false})
+ in
+ #Rep (unNode r) := SOME r'
+ end
+ | _ => raise Contradiction
+ end
+ | (PCon1 f, [e]) =>
+ let
+ val r = representative (db, e)
+ in
+ case #Variety (unNode r) of
+ Dt1 (f', e') => if f = f' then
+ ()
+ else
+ raise Contradiction
+ | Nothing =>
+ let
+ val r'' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false})
+
+ val r' = ref (Node {Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt1 (f, r''),
+ Known = ref false})
+ in
+ #Rep (unNode r) := SOME r'
+ end
+ | _ => raise Contradiction
+ end
+ | (Eq, [e1, e2]) =>
+ let
+ fun markEq (r1, r2) =
+ if r1 = r2 then
+ ()
+ else case (#Variety (unNode r1), #Variety (unNode r2)) of
+ (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
+ ()
+ else
+ raise Contradiction
+ | (Dt0 f1, Dt0 f2) => if f1 = f2 then
+ ()
+ else
+ raise Contradiction
+ | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
+ markEq (r1, r2)
+ else
+ raise Contradiction
+ | (Recrd xes1, Recrd xes2) =>
+ let
+ fun unif (xes1, xes2) =
+ SM.appi (fn (x, r1) =>
+ case SM.find (xes2, x) of
+ NONE => ()
+ | SOME r2 => markEq (r1, r2)) xes1
+ in
+ unif (!xes1, !xes2);
+ unif (!xes2, !xes1)
+ end
+ | (VFinish, VFinish) => ()
+ | (Nothing, _) =>
+ (#Rep (unNode r1) := SOME r2;
+ if !(#Known (unNode r1)) andalso not (!(#Known (unNode r2))) then
+ markKnown r2
+ else
+ ();
+ #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
+ compactFuncs ())
+ | (_, Nothing) =>
+ (#Rep (unNode r2) := SOME r1;
+ if !(#Known (unNode r2)) andalso not (!(#Known (unNode r1))) then
+ markKnown r1
+ else
+ ();
+ #Cons (unNode r1) := SM.unionWith #1 (!(#Cons (unNode r1)), !(#Cons (unNode r2)));
+ compactFuncs ())
+ | _ => raise Contradiction
+
+ and compactFuncs () =
+ let
+ fun loop funcs =
+ case funcs of
+ [] => []
+ | (fr as ((f, rs), r)) :: rest =>
+ let
+ val rest = List.filter (fn ((f' : string, rs'), r') =>
+ if f' = f
+ andalso ListPair.allEq (fn (r1, r2) =>
+ repOf r1 = repOf r2)
+ (rs, rs') then
+ (markEq (r, r');
+ false)
else
- t
- | _ => t) t (allPeers (t, e))
- end
- else
- t
- | _ => t
-
- fun doProj (t, e1, e2) =
- foldl (fn ((e1', e2'), t) =>
- let
- fun doOne (e, t) =
- case e of
- Proj (e', f) =>
- if query (t, e1, e') then
- assert (t, e, Proj (e2, f))
- else
- t
- | _ => t
- in
- doOne (e1', doOne (e2', t))
- end) t t
-
- val t = (r1, r2) :: t
- val t = doUn (t, r1, r2)
- val t = doUn (t, r2, r1)
- val t = doProj (t, r1, r2)
- val t = doProj (t, r2, r1)
+ true) rest
+ in
+ fr :: loop rest
+ end
+ in
+ #Funcs db := loop (!(#Funcs db))
+ end
in
- t
+ markEq (representative (db, e1), representative (db, e2))
end
- end
+ | _ => ()
+
+fun check (db, a) =
+ case a of
+ ACond _ => false
+ | AReln x =>
+ case x of
+ (Known, [e]) => !(#Known (unNode (representative (db, e))))
+ | (PCon0 f, [e]) =>
+ (case #Variety (unNode (representative (db, e))) of
+ Dt0 f' => f' = f
+ | _ => false)
+ | (PCon1 f, [e]) =>
+ (case #Variety (unNode (representative (db, e))) of
+ Dt1 (f', _) => f' = f
+ | _ => false)
+ | (Eq, [e1, e2]) =>
+ let
+ val r1 = representative (db, e1)
+ val r2 = representative (db, e2)
+ in
+ repOf r1 = repOf r2
+ end
+ | _ => false
end
-fun rimp cc ((r1, es1), (r2, es2)) =
- case (r1, r2) of
- (Sql r1', Sql r2') =>
- r1' = r2' andalso
- (case (es1, es2) of
- ([e1], [e2]) => eq (e1, e2)
- | _ => false)
- | (Eq, Eq) =>
- (case (es1, es2) of
- ([x1, y1], [x2, y2]) =>
- let
- val saved = save ()
- in
- if eq (x1, x2) andalso eq (y1, y2) then
- true
- else
- (restore saved;
- if eq (x1, y2) andalso eq (y1, x2) then
- true
- else
- (restore saved;
- false))
- end
- | _ => false)
- | (Known, Known) =>
- (case (es1, es2) of
- ([Var v], [e2]) =>
- let
- fun matches e =
- case e of
- Var v' => v' = v
- | Proj (e, _) => matches e
- | Func (f, [e]) => String.isPrefix "un" f andalso matches e
- | _ => false
- in
- (*Print.prefaces "Checking peers" [("e2", p_exp e2),
- ("peers", Print.p_list p_exp (Cc.allPeers (cc, e2))),
- ("db", Cc.p_t cc)];*)
- List.exists matches (Cc.allPeers (cc, e2))
- end
- | _ => false)
- | _ => false
-
-fun imply (p1, p2) =
+fun decomp fals or =
let
- fun doOne doKnown =
- decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
- (fn hyps =>
- decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
- (fn goals =>
- let
- val cc = foldl (fn (p, cc) =>
- case p of
- AReln (Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
- | _ => cc) Cc.empty hyps
-
- fun gls goals onFail =
- case goals of
- [] => true
- | ACond _ :: _ => false
- | AReln g :: goals =>
- case (doKnown, g) of
- (false, (Known, _)) => gls goals onFail
- | _ =>
- let
- fun hps hyps =
- case hyps of
- [] => ((*Print.prefaces "Fail" [("g", p_prop (Reln g)),
- ("db", Cc.p_t cc)];*)
- onFail ())
- | ACond _ :: hyps => hps hyps
- | AReln h :: hyps =>
- let
- val saved = save ()
- in
- if rimp cc (h, g) then
- let
- val changed = IM.numItems (!unif)
- <> IM.numItems saved
- in
- gls goals (fn () => (restore saved;
- changed (*andalso
- (Print.preface ("Retry",
- p_prop
- (Reln g)
- ); true)*)
- andalso hps hyps))
- end
- else
- hps hyps
- end
- in
- (case g of
- (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
- | _ => false)
- orelse hps hyps
- end
- in
- if List.exists (fn AReln (DtCon c1, [e]) =>
- List.exists (fn AReln (DtCon c2, [e']) =>
- c1 <> c2 andalso
- Cc.query (cc, e, e')
- | _ => false) hyps
- orelse List.exists (fn Func (c2, []) => c1 <> c2
- | Finish => true
- | _ => false)
- (Cc.allPeers (cc, e))
- | _ => false) hyps
- orelse gls goals (fn () => false) then
- true
- else
- ((*Print.prefaces "Can't prove"
- [("hyps", Print.p_list p_atom hyps),
- ("goals", Print.p_list p_atom goals)];*)
- false)
- end))
+ fun decomp p k =
+ case p of
+ True => k []
+ | False => fals
+ | Unknown => k []
+ | And (p1, p2) =>
+ decomp p1 (fn ps1 =>
+ decomp p2 (fn ps2 =>
+ k (ps1 @ ps2)))
+ | Or (p1, p2) =>
+ or (decomp p1 k, fn () => decomp p2 k)
+ | Reln x => k [AReln x]
+ | Cond x => k [ACond x]
in
- reset ();
- doOne false;
- doOne true
+ decomp
end
+fun imply (p1, p2) =
+ (reset ();
+ decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
+ (fn hyps =>
+ decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
+ (fn goals =>
+ let
+ fun gls goals onFail acc =
+ case goals of
+ [] =>
+ (let
+ val cc = Cc.database ()
+ val () = app (fn a => Cc.assert (cc, a)) hyps
+ in
+ (List.all (fn a =>
+ if Cc.check (cc, a) then
+ true
+ else
+ ((*Print.prefaces "Can't prove"
+ [("a", p_atom a),
+ ("hyps", Print.p_list p_atom hyps),
+ ("db", Cc.p_database cc)];*)
+ false)) acc
+ orelse onFail ())
+ handle Cc.Contradiction => onFail ()
+ end handle Cc.Undetermined => onFail ())
+ | AReln (Sql gf, [ge]) :: goals =>
+ let
+ fun hps hyps =
+ case hyps of
+ [] => onFail ()
+ | AReln (Sql hf, [he]) :: hyps =>
+ if gf = hf then
+ let
+ val saved = save ()
+ in
+ if eq (ge, he) then
+ let
+ val changed = IM.numItems (!unif)
+ <> IM.numItems saved
+ in
+ gls goals (fn () => (restore saved;
+ changed
+ andalso hps hyps))
+ acc
+ end
+ else
+ hps hyps
+ end
+ else
+ hps hyps
+ | _ :: hyps => hps hyps
+ in
+ hps hyps
+ end
+ | g :: goals => gls goals onFail (g :: acc)
+ in
+ gls goals (fn () => false) []
+ end handle Cc.Contradiction => true)))
+
fun patCon pc =
case pc of
PConVar n => "C" ^ Int.toString n
@@ -953,7 +1188,7 @@ val query = log "query"
(wrap (follow (follow select from) (opt wher))
(fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
-fun removeDups ls =
+fun removeDups (ls : (string * string) list) =
case ls of
[] => []
| x :: ls =>
@@ -1029,7 +1264,7 @@ fun queryProp env rvN rv oe e =
end
| SqFunc (f, e) =>
inl (case expIn e of
- inl e => Func (f, [e])
+ inl e => Func (Other f, [e])
| _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
| Count => inl count
@@ -1081,12 +1316,12 @@ fun evalPat env e (pt, _) =
PWild => (env, True)
| PVar _ => (e :: env, True)
| PPrim _ => (env, True)
- | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e]))
+ | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
| PCon (_, pc, SOME pt) =>
let
- val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt
+ val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
in
- (env, And (p, Reln (DtCon (patCon pc), [e])))
+ (env, And (p, Reln (PCon1 (patCon pc), [e])))
end
| PRecord xpts =>
foldl (fn ((x, pt, _), (env, p)) =>
@@ -1095,12 +1330,12 @@ fun evalPat env e (pt, _) =
in
(env, And (p', p))
end) (env, True) xpts
- | PNone _ => (env, Reln (DtCon "None", [e]))
+ | PNone _ => (env, Reln (PCon0 "None", [e]))
| PSome (_, pt) =>
let
- val (env, p) = evalPat env (Func ("unSome", [e])) pt
+ val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
in
- (env, And (p, Reln (DtCon "Some", [e])))
+ (env, And (p, Reln (PCon1 "Some", [e])))
end
fun peq (p1, p2) =
@@ -1145,19 +1380,19 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
EPrim p => (Const p, st)
| ERel n => (List.nth (env, n), st)
| ENamed _ => default ()
- | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
+ | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
| ECon (_, pc, SOME e) =>
let
val (e, st) = evalExp env (e, st)
in
- (Func (patCon pc, [e]), st)
+ (Func (DtCon1 (patCon pc), [e]), st)
end
- | ENone _ => (Func ("None", []), st)
+ | ENone _ => (Func (DtCon0 "None", []), st)
| ESome (_, e) =>
let
val (e, st) = evalExp env (e, st)
in
- (Func ("Some", [e]), st)
+ (Func (DtCon1 "Some", [e]), st)
end
| EFfi _ => default ()
@@ -1174,7 +1409,7 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
let
val (es, st) = ListUtil.foldlMap (evalExp env) st es
in
- (Func (m ^ "." ^ s, es), st)
+ (Func (Other (m ^ "." ^ s), es), st)
end
| EApp (e1, e2) =>
@@ -1191,14 +1426,14 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
let
val (e1, st) = evalExp env (e1, st)
in
- (Func (s, [e1]), st)
+ (Func (Other s, [e1]), st)
end
| EBinop (s, e1, e2) =>
let
val (e1, st) = evalExp env (e1, st)
val (e2, st) = evalExp env (e2, st)
in
- (Func (s, [e1, e2]), st)
+ (Func (Other s, [e1, e2]), st)
end
| ERecord xets =>
let
@@ -1241,7 +1476,7 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
val (e1, st) = evalExp env (e1, st)
val (e2, st) = evalExp env (e2, st)
in
- (Func ("cat", [e1, e2]), st)
+ (Func (Other "cat", [e1, e2]), st)
end
| EError _ => (Finish, st)
| EReturnBlob {blob = b, mimeType = m, ...} =>
@@ -1279,7 +1514,7 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
let
val (es, st) = ListUtil.foldlMap (evalExp env) st es
in
- (Func ("Cl" ^ Int.toString n, es), st)
+ (Func (Other ("Cl" ^ Int.toString n), es), st)
end
| EQuery {query = q, body = b, initial = i, ...} =>
@@ -1409,10 +1644,8 @@ fun check file =
Const _ => ()
| Var _ => doOne e
| Lvar _ => raise Fail "Iflow.doAll: Lvar"
- | Func (f, es) => if String.isPrefix "un" f then
- doOne e
- else
- app doAll es
+ | Func (UnCon _, [e]) => doOne e
+ | Func (_, es) => app doAll es
| Recd xes => app (doAll o #2) xes
| Proj _ => doOne e
| Finish => ()