Preparing to allow views in SELECT FROM clauses

5 files changed, 183 insertions, 128 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index c80dde7c..ec31e57f 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -124,6 +124,13 @@ val self : transaction client
 (** SQL *)
 
 con sql_table :: {Type} -> {{Unit}} -> Type
+con sql_view :: {Type} -> Type
+
+class fieldsOf :: Type -> {Type} -> Type
+val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
+                     -> fieldsOf (sql_table fs keys) fs
+val fieldsOf_view : fs ::: {Type}
+                    -> fieldsOf (sql_view fs) fs
 
 (*** Constraints *)
 
@@ -222,9 +229,9 @@ val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
 
 con sql_from_items :: {{Type}} -> Type
 
-val sql_from_table : cols ::: {Type} -> keys ::: {{Unit}}
-                     -> name :: Name -> sql_table cols keys
-                     -> sql_from_items [name = cols]
+val sql_from_table : t ::: Type -> fs ::: {Type}
+                     -> fieldsOf t fs -> name :: Name
+                     -> t -> sql_from_items [name = fs]
 val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
                      -> [tabs1 ~ tabs2]
     => sql_from_items tabs1 -> sql_from_items tabs2
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 1621722f..a5b8751a 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -71,7 +71,8 @@ signature ELAB_ENV = sig
 
     val pushClass : env -> int -> env
     val isClass : env -> Elab.con -> bool
-    val resolveClass : (Elab.con -> Elab.con) -> env -> Elab.con -> Elab.exp option
+    val resolveClass : (Elab.con -> Elab.con) -> (Elab.con * Elab.con -> bool)
+                       -> env -> Elab.con -> Elab.exp option
     val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list
 
     val pushERel : env -> string -> Elab.con -> env
@@ -118,4 +119,6 @@ signature ELAB_ENV = sig
 
     val patBinds : env -> Elab.pat -> env
 
+    exception Bad of Elab.con * Elab.con
+
 end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 7b20a700..0184d0b1 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -589,56 +589,9 @@ fun unifySubst (rs : con list) =
                         | (d, _) => d}
                0
 
-fun postUnify x =
-    let
-        fun unify (c1, c2) =
-            case (#1 c1, #1 c2) of
-                (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2)
-              | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2)
-
-              | (CUnif (_, _, _, r), _) => r := SOME c2
-
-              | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2))
-              | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2))
-              | (TRecord c1, TRecord c2) => unify (c1, c2)
-              | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
-                (unify (a1, a2); unify (b1, b2); unify (c1, c2))
-
-              | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
-              | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
-              | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
-                if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
-              | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2))
-              | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2))
-
-              | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2)
-              | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2))
-              | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2)
-
-              | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
-
-              | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
-                (unifyKinds (k1, k2);
-                 ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2)
-                 handle ListPair.UnequalLengths => raise Unify)
-              | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2))
-              | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
-
-              | (CUnit, CUnit) => ()
-
-              | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2)
-                                             handle ListPair.UnequalLengths => raise Unify)
-              | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2);
-                                                     if n1 = n2 then () else raise Unify)
+exception Bad of con * con
 
-              | _ => raise Unify
-    in
-        unify x
-    end
-
-fun postUnifies x = (postUnify x; true) handle Unify => false
-
-fun resolveClass (hnorm : con -> con) (env : env) =
+fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
     let
         fun resolve c =
             let
@@ -649,6 +602,37 @@ fun resolveClass (hnorm : con -> con) (env : env) =
                         let
                             val loc = #2 c
 
+                            fun generalize (c as (_, loc)) =
+                                case #1 c of
+                                    CApp (f, x) =>
+                                    let
+                                        val (f, equate) = generalize f
+
+                                        fun isRecord () =
+                                            let
+                                                val rk = ref NONE
+                                                val k = (KUnif (loc, "k", rk), loc)
+                                                val r = ref NONE
+                                                val rc = (CUnif (loc, k, "x", r), loc)
+                                            in
+                                                ((CApp (f, rc), loc),
+                                              fn () => (if consEq (rc, x) then
+                                                            true
+                                                        else
+                                                            (raise Bad (rc, x);
+                                                             false))
+                                                       andalso equate ())
+                                            end
+                                    in
+                                        case #1 x of
+                                            CConcat _ => isRecord ()
+                                          | CRecord _ => isRecord ()
+                                          | _ => ((CApp (f, x), loc), equate)
+                                    end
+                                  | _ => (c, fn () => true)
+
+                            val (c, equate) = generalize c
+
                             fun tryRules rules =
                                 case rules of
                                     [] => NONE
@@ -660,7 +644,8 @@ fun resolveClass (hnorm : con -> con) (env : env) =
                                             val eos = map (resolve o unifySubst rs) cs
                                         in
                                             if List.exists (not o Option.isSome) eos
-                                               orelse not (postUnifies (c, unifySubst rs c')) then
+                                               orelse not (equate ())
+                                               orelse not (consEq (c, unifySubst rs c')) then
                                                 tryRules rules'
                                             else
                                                 let
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 709871da..81fcbda1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -647,6 +647,13 @@
              case hnormKind (kindof env c) of
                  (L'.KRecord k, _) => k
                | (L'.KError, _) => kerror
+               | (L'.KUnif (_, _, r), _) =>
+                 let
+                     val k = kunif (#2 c)
+                 in
+                     r := SOME (L'.KRecord k, #2 c);
+                     k
+                 end
                | k => raise CUnify' (CKindof (k, c, "record"))
 
          val k1 = rkindof c1
@@ -786,20 +793,25 @@
          (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
                                             ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
 
-         fun isGuessable (other, fs) =
-             (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure);
-              true)
-             handle GuessFailure => false
+         fun isGuessable (other, fs, unifs) =
+             let
+                 val c = (L'.CRecord (k, fs), loc)
+                 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs
+             in
+                 (guessMap env (other, c, GuessFailure);
+                  true)
+                 handle GuessFailure => false
+             end
 
          val (fs1, fs2, others1, others2) =
-             case (fs1, fs2, others1, others2) of
-                 ([], _, [other1], []) =>
-                 if isGuessable (other1, fs2) then
+             case (fs1, fs2, others1, others2, unifs1, unifs2) of
+                 ([], _, [other1], [], [], _) =>
+                 if isGuessable (other1, fs2, unifs2) then
                      ([], [], [], [])
                  else
                      (fs1, fs2, others1, others2)
-               | (_, [], [], [other2]) =>
-                 if isGuessable (other2, fs1) then
+               | (_, [], [], [other2], _, []) =>
+                 if isGuessable (other2, fs1, unifs1) then
                      ([], [], [], [])
                  else
                      (fs1, fs2, others1, others2)
@@ -866,6 +878,13 @@
                              unfold (r2, c2');
                              unifyCons env r (L'.CConcat (r1, r2), loc)
                          end
+                       | L'.CUnif (_, _, _, ref (SOME c)) => unfold (r, c)
+                       | L'.CUnif (_, _, _, ur as ref NONE) =>
+                         let
+                             val ur' = cunif (loc, (L'.KRecord dom, loc))
+                         in
+                             ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc)
+                         end
                        | _ => raise ex
              in
                  unfold (r, c)
@@ -1144,17 +1163,21 @@
                              default ()
 
                      fun hasInstance c =
-                         case #1 (hnormCon env c) of
-                             L'.CApp (cl, x) =>
+                         case hnormCon env c of
+                             (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false,
+                                                                con = fn c =>
+                                                                         E.isClass env (hnormCon env (c, loc))} c
+                           | c =>
                              let
-                                 val cl = hnormCon env cl
+                                 fun findHead c =
+                                     case #1 c of
+                                         L'.CApp (f, _) => findHead f
+                                       | _ => c
+                                 
+                                 val cl = hnormCon env (findHead c)
                              in
                                  isClassOrFolder env cl
                              end
-                           | L'.TRecord c => U.Con.exists {kind = fn _ => false,
-                                                           con = fn c =>
-                                                                    E.isClass env (hnormCon env (c, loc))} c
-                           | _ => false
                  in
                      if hasInstance dom then
                          isInstance ()
@@ -3647,7 +3670,7 @@ fun elabFile basis topStr topSgn env file =
                                   let
                                       val c = normClassKey env c
                                   in
-                                      case E.resolveClass (hnormCon env) env c of
+                                      case E.resolveClass (hnormCon env) (consEq env) env c of
                                           SOME e => r := SOME e
                                         | NONE => expError env (Unresolvable (loc, c))
                                   end) gs
@@ -3684,72 +3707,102 @@ fun elabFile basis topStr topSgn env file =
             end
 
         val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
-    in
-        mayDelay := false;
 
-        app (fn (env, k, s1, s2) =>
-                unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
-                handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification";
-                                       cunifyError env err))
-            (!delayedUnifs);
+        val delayed = !delayedUnifs
+    in
         delayedUnifs := [];
+        app (fn (env, k, s1, s2) =>
+                unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
+            delayed;
 
         if ErrorMsg.anyErrors () then
             ()
         else
-            app (fn Disjoint (loc, env, denv, c1, c2) =>
-                    (case D.prove env denv (c1, c2, loc) of
-                         [] => ()
-                       | _ =>
-                         (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
-                          eprefaces' [("Con 1", p_con env c1),
-                                      ("Con 2", p_con env c2),
-                                      ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
-                                      ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
-                  | TypeClass (env, c, r, loc) =>
+            let
+                fun solver gs =
                     let
-                        fun default () = expError env (Unresolvable (loc, c))
+                        val (gs, solved) =
+                            ListUtil.foldlMapPartial
+                            (fn (g, solved) =>
+                                case g of
+                                    Disjoint (loc, env, denv, c1, c2) =>
+                                    (case D.prove env denv (c1, c2, loc) of
+                                         [] => (NONE, true)
+                                       | _ => (SOME g, solved))
+                                  | TypeClass (env, c, r, loc) =>
+                                    let
+                                        fun default () = (SOME g, solved)
 
-                        val c = normClassKey env c
-                    in
-                        case E.resolveClass (hnormCon env) env c of
-                            SOME e => r := SOME e
-                          | NONE =>
-                            case #1 (hnormCon env c) of
-                                L'.CApp (f, x) =>
-                                (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
-                                     (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
-                                     (case #1 (hnormCon env f) of
-                                          L'.CModProj (top_n', [], "folder") =>
-                                          if top_n' = top_n then
-                                              let
-                                                  val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
-                                                  val e = (L'.EKApp (e, k), loc)
-
-                                                  val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
-                                                                              let
-                                                                                  val e = (L'.EModProj (top_n, ["Folder"],
-                                                                                                        "cons"), loc)
-                                                                                  val e = (L'.EKApp (e, k), loc)
-                                                                                  val e = (L'.ECApp (e,
-                                                                                                     (L'.CRecord (k, xcs),
-                                                                                                      loc)), loc)
-                                                                                  val e = (L'.ECApp (e, x), loc)
-                                                                                  val e = (L'.ECApp (e, c), loc)
-                                                                                  val e = (L'.EApp (e, folder), loc)
-                                                                              in
-                                                                                  (e, (x, c) :: xcs)
-                                                                              end)
-                                                                          (e, []) xcs
-                                              in
-                                                  r := SOME folder
-                                              end
-                                          else
-                                              default ()
+                                        val c = normClassKey env c
+                                    in
+                                        case E.resolveClass (hnormCon env) (consEq env) env c of
+                                            SOME e => (r := SOME e;
+                                                       (NONE, true))
+                                          | NONE =>
+                                            case #1 (hnormCon env c) of
+                                                L'.CApp (f, x) =>
+                                                (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
+                                                     (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
+                                                     (case #1 (hnormCon env f) of
+                                                          L'.CModProj (top_n', [], "folder") =>
+                                                          if top_n' = top_n then
+                                                              let
+                                                                  val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
+                                                                  val e = (L'.EKApp (e, k), loc)
+                                                                          
+                                                                  val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
+                                                                                              let
+                                                                                                  val e = (L'.EModProj (top_n, ["Folder"],
+                                                                                                                        "cons"), loc)
+                                                                                                  val e = (L'.EKApp (e, k), loc)
+                                                                                                  val e = (L'.ECApp (e,
+                                                                                                                     (L'.CRecord (k, xcs),
+                                                                                                                      loc)), loc)
+                                                                                                  val e = (L'.ECApp (e, x), loc)
+                                                                                                  val e = (L'.ECApp (e, c), loc)
+                                                                                                  val e = (L'.EApp (e, folder), loc)
+                                                                                              in
+                                                                                                  (e, (x, c) :: xcs)
+                                                                                              end)
+                                                                                          (e, []) xcs
+                                                              in
+                                                                  (r := SOME folder;
+                                                                   (NONE, true))
+                                                              end
+                                                          else
+                                                              default ()
                                         | _ => default ())
                                    | _ => default ())
                               | _ => default ()
-                    end) gs;
+                                    end)
+                            false gs
+                    in
+                        case (gs, solved) of
+                            ([], _) => ()
+                          | (_, true) => solver gs
+                          | _ =>
+                            app (fn Disjoint (loc, env, denv, c1, c2) =>
+                                    ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
+                                      eprefaces' [("Con 1", p_con env c1),
+                                                  ("Con 2", p_con env c2),
+                                                  ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
+                                                  ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
+                                  | TypeClass (env, c, r, loc) =>
+                                    expError env (Unresolvable (loc, c)))
+                                gs
+                    end
+            in
+                solver gs
+            end;
+
+        mayDelay := false;
+
+        app (fn (env, k, s1, s2) =>
+                unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
+                handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification";
+                                       cunifyError env err))
+            (!delayedUnifs);
+        delayedUnifs := [];
 
         if ErrorMsg.anyErrors () then
             ()
diff --git a/src/monoize.sml b/src/monoize.sml
index 16839cf9..ccc5a851 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -184,6 +184,8 @@ fun monoType env =
                     (L'.TFfi ("Basis", "string"), loc)
                   | L.CFfi ("Basis", "sql_offset") =>
                     (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CApp ((L.CFfi ("Basis", "fieldsOf"), _), _), _), _) =>
+                    (L'.TRecord [], loc)
 
                   | L.CApp ((L.CFfi ("Basis", "sql_injectable_prim"), _), t) =>
                     (L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc)
@@ -1725,8 +1727,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
           | L.ECApp ((L.EFfi ("Basis", "sql_subset_all"), _), _) =>
             ((L'.ERecord [], loc), fm)
 
-          | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_from_table"), _), _), _), _), _),
-                              (L.CName name, _)) =>
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "fieldsOf_table"), _), _), _), _) =>
+            ((L'.ERecord [], loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "fieldsOf_view"), _), _) =>
+            ((L'.ERecord [], loc), fm)
+
+          | L.ECApp ((L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_from_table"), _), _), _), _), _), _), _),
+                     (L.CName name, _)) =>
             let
                 val s = (L'.TFfi ("Basis", "string"), loc)
             in