summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-28 15:04:37 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-28 15:04:37 -0400
commit51f2a80dac5c3cd25a27fb5abfdfa50d813ab0b2 (patch)
treee4e2246dc15a7cbbf067401a21197b6fd17ea95b /src/elab_env.sml
parentcaf010bca085bea65037d194c3eb21ca8b83c23b (diff)
A view query works
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml82
1 files changed, 54 insertions, 28 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 0184d0b1..efc2b74e 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -591,6 +591,22 @@ fun unifySubst (rs : con list) =
exception Bad of con * con
+val hasUnif = U.Con.exists {kind = fn _ => false,
+ con = fn CUnif (_, _, _, ref NONE) => true
+ | _ => false}
+
+fun startsWithUnif c =
+ let
+ fun firstArg (c, acc) =
+ case #1 c of
+ CApp (f, x) => firstArg (f, SOME x)
+ | _ => acc
+ in
+ case firstArg (c, NONE) of
+ NONE => false
+ | SOME x => hasUnif x
+ end
+
fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
let
fun resolve c =
@@ -671,34 +687,37 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
tryGrounds (#ground class)
end
in
- case #1 c of
- TRecord c =>
- (case #1 (hnorm c) of
- CRecord (_, xts) =>
- let
- fun resolver (xts, acc) =
- case xts of
- [] => SOME (ERecord acc, #2 c)
- | (x, t) :: xts =>
- let
- val t = hnorm t
-
- val t = case t of
- (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
- | _ => t
- in
- case resolve t of
- NONE => NONE
- | SOME e => resolver (xts, (x, e, t) :: acc)
- end
- in
- resolver (xts, [])
- end
- | _ => NONE)
- | _ =>
- case class_head_in c of
- SOME f => doHead f
- | _ => NONE
+ if startsWithUnif c then
+ NONE
+ else
+ case #1 c of
+ TRecord c =>
+ (case #1 (hnorm c) of
+ CRecord (_, xts) =>
+ let
+ fun resolver (xts, acc) =
+ case xts of
+ [] => SOME (ERecord acc, #2 c)
+ | (x, t) :: xts =>
+ let
+ val t = hnorm t
+
+ val t = case t of
+ (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
+ | _ => t
+ in
+ case resolve t of
+ NONE => NONE
+ | SOME e => resolver (xts, (x, e, t) :: acc)
+ end
+ in
+ resolver (xts, [])
+ end
+ | _ => NONE)
+ | _ =>
+ case class_head_in c of
+ SOME f => doHead f
+ | _ => NONE
end
in
resolve
@@ -1482,6 +1501,13 @@ fun declBinds env (d, loc) =
in
pushENamedAs env x n t
end
+ | DView (tn, x, n, _, c) =>
+ let
+ val ct = (CModProj (tn, [], "sql_view"), loc)
+ val ct = (CApp (ct, c), loc)
+ in
+ pushENamedAs env x n ct
+ end
| DClass (x, n, k, c) =>
let
val k = (KArrow (k, (KType, loc)), loc)