summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 10:40:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 10:40:55 -0400
commit3f95c104bdbf0e24e3557c66d7a4a3e165d562f0 (patch)
tree063a23a9ab9bf6acb5884e38af9645c093ae4fbe /src
parent8ee738489b23b52246046305325ba7dd0db29c63 (diff)
Fix problem with overly weak ambients for queries; fix known-related bug in assert for Dt1
Diffstat (limited to 'src')
-rw-r--r--src/iflow.sml50
1 files changed, 30 insertions, 20 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index 797f13d0..73ff07ea 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -787,12 +787,12 @@ fun assert (db, a) =
val r'' = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
Variety = Nothing,
- Known = ref false})
+ Known = ref (!(#Known (unNode r)))})
val r' = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
Variety = Dt1 (f, r''),
- Known = ref false})
+ Known = #Known (unNode r)})
in
#Rep (unNode r) := SOME r'
end
@@ -2109,8 +2109,12 @@ fun evalExp env (e as (_, loc), st) =
val st = St.addPath (st, ((loc, e, orig), Case))
- val (st, paths) =
- foldl (fn ((pt, pe), (st, paths)) =>
+ (*val () = Print.prefaces "Case" [("loc", Print.PD.string (ErrorMsg.spanToString loc)),
+ ("e", Print.p_list (MonoPrint.p_exp MonoEnv.empty o #2) pes),
+ ("orig", p_prop orig)]*)
+
+ val (st, ambients, paths) =
+ foldl (fn ((pt, pe), (st, ambients, paths)) =>
let
val (env, pp) = evalPat env e pt
val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
@@ -2118,15 +2122,16 @@ fun evalExp env (e as (_, loc), st) =
val this = And (removeRedundant orig (St.ambient st'),
Reln (Eq, [Var r, pe]))
in
- (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths),
+ (St.setPaths (st', origPaths),
+ Or (ambients, this),
St.paths st' @ paths)
- end) (St.setAmbient (st, False), []) pes
+ end) (st, False, []) pes
val st = case #1 res of
TRecord [] => St.setPaths (st, origPaths)
| _ => St.setPaths (st, paths)
in
- (Var r, St.setAmbient (st, And (orig, St.ambient st)))
+ (Var r, St.setAmbient (st, And (orig, ambients)))
end
| EStrcat (e1, e2) =>
let
@@ -2183,6 +2188,7 @@ fun evalExp env (e as (_, loc), st) =
val (st', acc) = St.nextVar st'
val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
+ val amb = removeRedundant (St.ambient st) (St.ambient st')
val (st', qp, used, _) =
queryProp env
@@ -2194,8 +2200,6 @@ fun evalExp env (e as (_, loc), st) =
end)
(AllCols (Var r)) q
- val p' = And (qp, St.ambient st')
-
val (st, res) = if varInP acc (St.ambient st') then
let
val (st, r) = St.nextVar st
@@ -2204,17 +2208,19 @@ fun evalExp env (e as (_, loc), st) =
end
else
let
- val (st, out) = St.nextVar st'
+ val (st', out) = St.nextVar st'
- val p = Or (Reln (Eq, [Var out, i]),
- And (Reln (Eq, [Var out, b]),
- p'))
+ val p = And (St.ambient st,
+ Or (Reln (Eq, [Var out, i]),
+ And (Reln (Eq, [Var out, b]),
+ And (qp, amb))))
in
- (St.setAmbient (st, p), Var out)
+ (St.setAmbient (st', p), Var out)
end
val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
+ val p' = And (qp, St.ambient st')
val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
in
(res, St.addPaths (St.setSent (st, sent), paths))
@@ -2508,13 +2514,16 @@ fun check file =
val avail = foldl (fn (AReln (Sql tab, _), avail) =>
SS.add (avail, tab)
| (_, avail) => avail) SS.empty hyps
- in
- List.filter
- (fn (g1, _) =>
- decompG g1
- (List.all (fn AReln (Sql tab, _) =>
+
+ val ls = List.filter
+ (fn (g1, _) =>
+ decompG g1
+ (List.all (fn AReln (Sql tab, _) =>
SS.member (avail, tab)
- | _ => true))) client
+ | _ => true))) client
+ in
+ (*print ("Max: " ^ Int.toString (length ls) ^ "\n");*)
+ ls
end
fun tryCombos (maxLv, pols, g, outs) =
@@ -2551,6 +2560,7 @@ fun check file =
| Control Case => " (case discriminee)"
| Data => " (returned data value)"),
Print.p_list p_atom hyps);
+ Print.preface ("DB", Cc.p_database cc);
false)
end handle Cc.Contradiction => true) then
()