summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 12:45:15 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 12:45:15 -0400
commitefb882576e0fe75fa25829b417ea909b572634a5 (patch)
tree263fbd3e49bfad578b96fcbf7aad2ba07aba1c61
parentaccb8e1bf49e1c1e8300bda9be3cf72ce592ab44 (diff)
Express all query outputs using record literals
-rw-r--r--src/iflow.sml41
1 files changed, 27 insertions, 14 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index f275d013..2b67b9ea 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1426,21 +1426,34 @@ fun queryProp env rvN rv oe e =
end
| AllCols oe =>
let
- val (p', rvN) =
- foldl (fn (si, (p, rvN)) =>
- let
- val (p', rvN) =
- case si of
- SqField (v, f) => (Reln (Eq, [Proj (Proj (oe, v), f),
- Proj (rvOf v, f)]), rvN)
- | SqExp (e, f) =>
+ val (ts, es, rvN) =
+ foldl (fn (si, (ts, es, rvN)) =>
+ case si of
+ SqField (v, f) =>
+ let
+ val fs = getOpt (SM.find (ts, v), SM.empty)
+ in
+ (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN)
+ end
+ | SqExp (e, f) =>
+ let
+ val (e, rvN) =
case expIn (e, rvN) of
- (inr p, rvN) => (Cond (Proj (oe, f), p), rvN)
- | (inl e, rvN) => (Reln (Eq, [Proj (oe, f), e]), rvN)
- in
- (And (p, p'), rvN)
- end)
- (True, rvN) (#Select r)
+ (inr _, rvN) =>
+ let
+ val (rvN, e) = rv rvN
+ in
+ (e, rvN)
+ end
+ | (inl e, rvN) => (e, rvN)
+ in
+ (ts, SM.insert (es, f, e), rvN)
+ end)
+ (SM.empty, SM.empty, rvN) (#Select r)
+
+ val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
+ (SM.listItemsi ts)
+ @ SM.listItemsi es)])
in
(rvN, And (p, p'), True, [])
end