summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/basis.urs13
-rw-r--r--src/elab_env.sig5
-rw-r--r--src/elab_env.sml85
-rw-r--r--src/elaborate.sml197
-rw-r--r--src/monoize.sml11
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 06:55:19 +0000