Mercurial > urweb
changeset 753:d484df4e841a
Preparing to allow views in SELECT FROM clauses
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 28 Apr 2009 14:02:23 -0400 |
| parents | bc5cfd6cb30f |
| children | 8688e01ae469 |
| files | lib/ur/basis.urs src/elab_env.sig src/elab_env.sml src/elaborate.sml src/monoize.sml |
| diffstat | 5 files changed, 185 insertions(+), 130 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Apr 28 11:18:27 2009 -0400 +++ b/lib/ur/basis.urs Tue Apr 28 14:02:23 2009 -0400 @@ -124,6 +124,13 @@ (** 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 @@ 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
--- a/src/elab_env.sig Tue Apr 28 11:18:27 2009 -0400 +++ b/src/elab_env.sig Tue Apr 28 14:02:23 2009 -0400 @@ -71,7 +71,8 @@ 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 @@ val patBinds : env -> Elab.pat -> env + exception Bad of Elab.con * Elab.con + end
--- a/src/elab_env.sml Tue Apr 28 11:18:27 2009 -0400 +++ b/src/elab_env.sml Tue Apr 28 14:02:23 2009 -0400 @@ -589,56 +589,9 @@ | (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) +exception Bad of con * con - | (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) - - | _ => 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 @@ 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 @@ 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
--- a/src/elaborate.sml Tue Apr 28 11:18:27 2009 -0400 +++ b/src/elaborate.sml Tue Apr 28 14:02:23 2009 -0400 @@ -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 @@ 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,7 +3707,94 @@ end val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file + + 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 + let + fun solver gs = + let + 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) (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) + 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) => @@ -3697,63 +3807,6 @@ 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 default () = expError env (Unresolvable (loc, c)) - - 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 () - | _ => default ()) - | _ => default ()) - | _ => default () - end) gs; - - if ErrorMsg.anyErrors () then - () - else app (fn f => f ()) (!checks); (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
--- a/src/monoize.sml Tue Apr 28 11:18:27 2009 -0400 +++ b/src/monoize.sml Tue Apr 28 14:02:23 2009 -0400 @@ -184,6 +184,8 @@ (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 @@ | 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