summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--demo/listShop.ur8
-rw-r--r--demo/prose4
-rw-r--r--lib/basis.urs2
-rw-r--r--lib/top.ur2
-rw-r--r--src/compiler.sml4
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml65
-rw-r--r--src/elaborate.sml2068
-rw-r--r--src/monoize.sml2
-rw-r--r--src/source.sml7
-rw-r--r--src/source_print.sml2
-rw-r--r--src/urweb.grm155
-rw-r--r--src/urweb.lex1
-rw-r--r--tests/crud.ur24
14 files changed, 1196 insertions, 1149 deletions
diff --git a/demo/listShop.ur b/demo/listShop.ur
index 0c23819f..be35d505 100644
--- a/demo/listShop.ur
+++ b/demo/listShop.ur
@@ -1,13 +1,13 @@
structure I = struct
type t = int
- val toString = show _
- val fromString = read _
+ val toString = show
+ val fromString = read
end
structure S = struct
type t = string
- val toString = show _
- val fromString = read _
+ val toString = show
+ val fromString = read
end
structure IL = ListFun.Make(I)
diff --git a/demo/prose b/demo/prose
index 388dc00c..72c9cb6f 100644
--- a/demo/prose
+++ b/demo/prose
@@ -7,3 +7,7 @@ hello.urp
link.urp
<p>This is my second favorite.</p>
+
+listShop.urp
+
+<p>This is my other favorite.</p>
diff --git a/lib/basis.urs b/lib/basis.urs
index 027e81ac..de4204b3 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -248,7 +248,7 @@ val insert : fields ::: {Type}
[] fields)
-> dml
-val update : changed :: {Type} -> unchanged ::: {Type} ->
+val update : unchanged ::: {Type} -> changed :: {Type} ->
fn [changed ~ unchanged] =>
$(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
[nm = sql_exp [T = changed ++ unchanged] [] [] t]
diff --git a/lib/top.ur b/lib/top.ur
index 4b9f54ef..bdf5f182 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -20,7 +20,7 @@ fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
(f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) =
- cdata (show sh v)
+ cdata (@show sh v)
fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
(f : nm :: Name -> t :: Type -> rest :: {Type}
diff --git a/src/compiler.sml b/src/compiler.sml
index 43e361f0..2ddcfb4d 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -535,6 +535,10 @@ fun compile job =
else
let
val dir = OS.FileSys.tmpName ()
+ val () = if OS.FileSys.access (dir, []) then
+ OS.FileSys.remove dir
+ else
+ ()
val cname = OS.Path.joinDirFile {dir = dir, file = "urweb.c"}
val oname = OS.Path.joinDirFile {dir = dir, file = "urweb.o"}
in
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 1d265991..363cbe26 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -61,6 +61,7 @@ signature ELAB_ENV = sig
val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option
val pushClass : env -> int -> env
+ val isClass : env -> Elab.con -> bool
val resolveClass : env -> Elab.con -> Elab.exp option
val pushERel : env -> string -> Elab.con -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 4ff026f1..958d369c 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -358,7 +358,7 @@ fun pushClass (env : env) n =
sgn = #sgn env,
renameStr = #renameStr env,
- str = #str env}
+ str = #str env}
fun class_name_in (c, _) =
case c of
@@ -367,6 +367,14 @@ fun class_name_in (c, _) =
| CUnif (_, _, _, ref (SOME c)) => class_name_in c
| _ => NONE
+fun isClass (env : env) c =
+ let
+ fun find NONE = false
+ | find (SOME c) = Option.isSome (CM.find (#classes env, c))
+ in
+ find (class_name_in c)
+ end
+
fun class_key_in (c, _) =
case c of
CRel n => SOME (CkRel n)
@@ -405,14 +413,16 @@ fun pushERel (env : env) x t =
val classes = case class_pair_in t of
NONE => classes
| SOME (f, x) =>
- let
- val class = Option.getOpt (CM.find (classes, f), empty_class)
- val class = {
- ground = KM.insert (#ground class, x, (ERel 0, #2 t))
- }
- in
- CM.insert (classes, f, class)
- end
+ case CM.find (classes, f) of
+ NONE => classes
+ | SOME class =>
+ let
+ val class = {
+ ground = KM.insert (#ground class, x, (ERel 0, #2 t))
+ }
+ in
+ CM.insert (classes, f, class)
+ end
in
{renameC = #renameC env,
relC = #relC env,
@@ -444,14 +454,16 @@ fun pushENamedAs (env : env) x n t =
val classes = case class_pair_in t of
NONE => classes
| SOME (f, x) =>
- let
- val class = Option.getOpt (CM.find (classes, f), empty_class)
- val class = {
- ground = KM.insert (#ground class, x, (ENamed n, #2 t))
- }
- in
- CM.insert (classes, f, class)
- end
+ case CM.find (classes, f) of
+ NONE => classes
+ | SOME class =>
+ let
+ val class = {
+ ground = KM.insert (#ground class, x, (ENamed n, #2 t))
+ }
+ in
+ CM.insert (classes, f, class)
+ end
in
{renameC = #renameC env,
relC = #relC env,
@@ -740,14 +752,21 @@ fun enrichClasses env classes (m1, ms) sgn =
| SOME ck =>
let
val cn = ClProj (m1, ms, fx)
- val class = Option.getOpt (CM.find (classes, cn), empty_class)
- val class = {
- ground = KM.insert (#ground class, ck,
- (EModProj (m1, ms, x), #2 sgn))
- }
+ val classes =
+ case CM.find (classes, cn) of
+ NONE => classes
+ | SOME class =>
+ let
+ val class = {
+ ground = KM.insert (#ground class, ck,
+ (EModProj (m1, ms, x), #2 sgn))
+ }
+ in
+ CM.insert (classes, cn, class)
+ end
in
- (CM.insert (classes, cn, class),
+ (classes,
newClasses,
fmap,
env)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 1d793923..b965f0da 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1,1041 +1,1057 @@
-(* Copyright (c) 2008, Adam Chlipala
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are met:
- *
- * - Redistributions of source code must retain the above copyright notice,
- * this list of conditions and the following disclaimer.
- * - Redistributions in binary form must reproduce the above copyright notice,
- * this list of conditions and the following disclaimer in the documentation
- * and/or other materials provided with the distribution.
- * - The names of contributors may not be used to endorse or promote products
- * derived from this software without specific prior written permission.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
- * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
- * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
- * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
- * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
- * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
- * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
- * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
- * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
- * POSSIBILITY OF SUCH DAMAGE.
- *)
-
-structure Elaborate :> ELABORATE = struct
-
-structure P = Prim
-structure L = Source
-structure L' = Elab
-structure E = ElabEnv
-structure U = ElabUtil
-structure D = Disjoint
-
-open Print
-open ElabPrint
-open ElabErr
-
-structure IM = IntBinaryMap
-
-structure SK = struct
-type ord_key = string
-val compare = String.compare
-end
-
-structure SS = BinarySetFn(SK)
-structure SM = BinaryMapFn(SK)
-
-val basis_r = ref 0
-
-fun elabExplicitness e =
- case e of
- L.Explicit => L'.Explicit
- | L.Implicit => L'.Implicit
-
-fun occursKind r =
- U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
- | _ => false)
-
-exception KUnify' of kunify_error
-
-fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
- let
- fun err f = raise KUnify' (f (k1All, k2All))
- in
- case (k1, k2) of
- (L'.KType, L'.KType) => ()
- | (L'.KUnit, L'.KUnit) => ()
-
- | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
- (unifyKinds' d1 d2;
- unifyKinds' r1 r2)
- | (L'.KName, L'.KName) => ()
- | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
- | (L'.KTuple ks1, L'.KTuple ks2) =>
- ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
- handle ListPair.UnequalLengths => err KIncompatible)
-
- | (L'.KError, _) => ()
- | (_, L'.KError) => ()
-
- | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
- | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
-
- | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
- if r1 = r2 then
- ()
- else
- r1 := SOME k2All
-
- | (L'.KUnif (_, _, r), _) =>
- if occursKind r k2All then
- err KOccursCheckFailed
- else
- r := SOME k2All
- | (_, L'.KUnif (_, _, r)) =>
- if occursKind r k1All then
- err KOccursCheckFailed
- else
- r := SOME k1All
-
- | _ => err KIncompatible
- end
-
-exception KUnify of L'.kind * L'.kind * kunify_error
-
-fun unifyKinds k1 k2 =
- unifyKinds' k1 k2
- handle KUnify' err => raise KUnify (k1, k2, err)
-
-fun checkKind env c k1 k2 =
- unifyKinds k1 k2
- handle KUnify (k1, k2, err) =>
- conError env (WrongKind (c, k1, k2, err))
-
-val dummy = ErrorMsg.dummySpan
-
-val ktype = (L'.KType, dummy)
-val kname = (L'.KName, dummy)
-val ktype_record = (L'.KRecord ktype, dummy)
-
-val cerror = (L'.CError, dummy)
-val kerror = (L'.KError, dummy)
-val eerror = (L'.EError, dummy)
-val sgnerror = (L'.SgnError, dummy)
-val strerror = (L'.StrError, dummy)
-
-val int = ref cerror
-val float = ref cerror
-val string = ref cerror
-val table = ref cerror
-
-local
- val count = ref 0
-in
-
-fun resetKunif () = count := 0
-
-fun kunif loc =
- let
- val n = !count
- val s = if n <= 26 then
- str (chr (ord #"A" + n))
- else
- "U" ^ Int.toString (n - 26)
- in
- count := n + 1;
- (L'.KUnif (loc, s, ref NONE), dummy)
- end
-
-end
-
-local
- val count = ref 0
-in
-
-fun resetCunif () = count := 0
-
-fun cunif (loc, k) =
- let
- val n = !count
- val s = if n <= 26 then
- str (chr (ord #"A" + n))
- else
- "U" ^ Int.toString (n - 26)
- in
- count := n + 1;
- (L'.CUnif (loc, k, s, ref NONE), dummy)
- end
-
-end
-
-fun elabKind (k, loc) =
- case k of
- L.KType => (L'.KType, loc)
- | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
- | L.KName => (L'.KName, loc)
- | L.KRecord k => (L'.KRecord (elabKind k), loc)
- | L.KUnit => (L'.KUnit, loc)
- | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
- | L.KWild => kunif loc
-
-fun foldKind (dom, ran, loc)=
- (L'.KArrow ((L'.KArrow ((L'.KName, loc),
- (L'.KArrow (dom,
- (L'.KArrow (ran, ran), loc)), loc)), loc),
- (L'.KArrow (ran,
- (L'.KArrow ((L'.KRecord dom, loc),
- ran), loc)), loc)), loc)
-
-fun hnormKind (kAll as (k, _)) =
- case k of
- L'.KUnif (_, _, ref (SOME k)) => hnormKind k
- | _ => kAll
-
-fun elabCon (env, denv) (c, loc) =
- case c of
- L.CAnnot (c, k) =>
- let
- val k' = elabKind k
- val (c', ck, gs) = elabCon (env, denv) c
- in
- checkKind env c' ck k';
- (c', k', gs)
- end
-
- | L.TFun (t1, t2) =>
- let
- val (t1', k1, gs1) = elabCon (env, denv) t1
- val (t2', k2, gs2) = elabCon (env, denv) t2
- in
- checkKind env t1' k1 ktype;
- checkKind env t2' k2 ktype;
- ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
- end
- | L.TCFun (e, x, k, t) =>
- let
- val e' = elabExplicitness e
- val k' = elabKind k
- val env' = E.pushCRel env x k'
- val (t', tk, gs) = elabCon (env', D.enter denv) t
- in
- checkKind env t' tk ktype;
- ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
- end
- | L.CDisjoint (c1, c2, c) =>
- let
- val (c1', k1, gs1) = elabCon (env, denv) c1
- val (c2', k2, gs2) = elabCon (env, denv) c2
-
- val ku1 = kunif loc
- val ku2 = kunif loc
-
- val (denv', gs3) = D.assert env denv (c1', c2')
- val (c', k, gs4) = elabCon (env, denv') c
- in
- checkKind env c1' k1 (L'.KRecord ku1, loc);
- checkKind env c2' k2 (L'.KRecord ku2, loc);
-
- ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
- end
- | L.TRecord c =>
- let
- val (c', ck, gs) = elabCon (env, denv) c
- val k = (L'.KRecord ktype, loc)
- in
- checkKind env c' ck k;
- ((L'.TRecord c', loc), ktype, gs)
- end
+ (* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+ structure Elaborate :> ELABORATE = struct
+
+ structure P = Prim
+ structure L = Source
+ structure L' = Elab
+ structure E = ElabEnv
+ structure U = ElabUtil
+ structure D = Disjoint
+
+ open Print
+ open ElabPrint
+ open ElabErr
+
+ structure IM = IntBinaryMap
+
+ structure SK = struct
+ type ord_key = string
+ val compare = String.compare
+ end
+
+ structure SS = BinarySetFn(SK)
+ structure SM = BinaryMapFn(SK)
+
+ val basis_r = ref 0
+
+ fun elabExplicitness e =
+ case e of
+ L.Explicit => L'.Explicit
+ | L.Implicit => L'.Implicit
+
+ fun occursKind r =
+ U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
+ | _ => false)
+
+ exception KUnify' of kunify_error
+
+ fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
+ let
+ fun err f = raise KUnify' (f (k1All, k2All))
+ in
+ case (k1, k2) of
+ (L'.KType, L'.KType) => ()
+ | (L'.KUnit, L'.KUnit) => ()
+
+ | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
+ (unifyKinds' d1 d2;
+ unifyKinds' r1 r2)
+ | (L'.KName, L'.KName) => ()
+ | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
+ | (L'.KTuple ks1, L'.KTuple ks2) =>
+ ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
+ handle ListPair.UnequalLengths => err KIncompatible)
+
+ | (L'.KError, _) => ()
+ | (_, L'.KError) => ()
+
+ | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
+ | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
+
+ | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
+ if r1 = r2 then
+ ()
+ else
+ r1 := SOME k2All
+
+ | (L'.KUnif (_, _, r), _) =>
+ if occursKind r k2All then
+ err KOccursCheckFailed
+ else
+ r := SOME k2All
+ | (_, L'.KUnif (_, _, r)) =>
+ if occursKind r k1All then
+ err KOccursCheckFailed
+ else
+ r := SOME k1All
+
+ | _ => err KIncompatible
+ end
+
+ exception KUnify of L'.kind * L'.kind * kunify_error
+
+ fun unifyKinds k1 k2 =
+ unifyKinds' k1 k2
+ handle KUnify' err => raise KUnify (k1, k2, err)
+
+ fun checkKind env c k1 k2 =
+ unifyKinds k1 k2
+ handle KUnify (k1, k2, err) =>
+ conError env (WrongKind (c, k1, k2, err))
+
+ val dummy = ErrorMsg.dummySpan
+
+ val ktype = (L'.KType, dummy)
+ val kname = (L'.KName, dummy)
+ val ktype_record = (L'.KRecord ktype, dummy)
+
+ val cerror = (L'.CError, dummy)
+ val kerror = (L'.KError, dummy)
+ val eerror = (L'.EError, dummy)
+ val sgnerror = (L'.SgnError, dummy)
+ val strerror = (L'.StrError, dummy)
+
+ val int = ref cerror
+ val float = ref cerror
+ val string = ref cerror
+ val table = ref cerror
+
+ local
+ val count = ref 0
+ in
+
+ fun resetKunif () = count := 0
+
+ fun kunif loc =
+ let
+ val n = !count
+ val s = if n <= 26 then
+ str (chr (ord #"A" + n))
+ else
+ "U" ^ Int.toString (n - 26)
+ in
+ count := n + 1;
+ (L'.KUnif (loc, s, ref NONE), dummy)
+ end
- | L.CVar ([], s) =>
- (case E.lookupC env s of
- E.NotBound =>
- (conError env (UnboundCon (loc, s));
- (cerror, kerror, []))
- | E.Rel (n, k) =>
- ((L'.CRel n, loc), k, [])
- | E.Named (n, k) =>
- ((L'.CNamed n, loc), k, []))
- | L.CVar (m1 :: ms, s) =>
- (case E.lookupStr env m1 of
- NONE => (conError env (UnboundStrInCon (loc, m1));
- (cerror, kerror, []))
- | SOME (n, sgn) =>
- let
- val (str, sgn) = foldl (fn (m, (str, sgn)) =>
- case E.projectStr env {sgn = sgn, str = str, field = m} of
- NONE => (conError env (UnboundStrInCon (loc, m));
- (strerror, sgnerror))
- | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
- ((L'.StrVar n, loc), sgn) ms
+ end
- val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
- NONE => (conError env (UnboundCon (loc, s));
- kerror)
- | SOME (k, _) => k
- in
- ((L'.CModProj (n, ms, s), loc), k, [])
- end)
-
- | L.CApp (c1, c2) =>
- let
- val (c1', k1, gs1) = elabCon (env, denv) c1
- val (c2', k2, gs2) = elabCon (env, denv) c2
- val dom = kunif loc
- val ran = kunif loc
- in
- checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
- checkKind env c2' k2 dom;
- ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
- end
- | L.CAbs (x, ko, t) =>
- let
- val k' = case ko of
- NONE => kunif loc
- | SOME k => elabKind k
- val env' = E.pushCRel env x k'
- val (t', tk, gs) = elabCon (env', D.enter denv) t
- in
- ((L'.CAbs (x, k', t'), loc),
- (L'.KArrow (k', tk), loc),
- gs)
- end
+ local
+ val count = ref 0
+ in
- | L.CName s =>
- ((L'.CName s, loc), kname, [])
+ fun resetCunif () = count := 0
- | L.CRecord xcs =>
- let
- val k = kunif loc
-
- val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
- let
- val (x', xk, gs1) = elabCon (env, denv) x
- val (c', ck, gs2) = elabCon (env, denv) c
- in
- checkKind env x' xk kname;
- checkKind env c' ck k;
- ((x', c'), gs1 @ gs2 @ gs)
- end) [] xcs
-
- val rc = (L'.CRecord (k, xcs'), loc)
- (* Add duplicate field checking later. *)
-
- fun prove (xcs, ds) =
- case xcs of
- [] => ds
- | xc :: rest =>
- let
- val r1 = (L'.CRecord (k, [xc]), loc)
- val ds = foldl (fn (xc', ds) =>
+ fun cunif (loc, k) =
+ let
+ val n = !count
+ val s = if n <= 26 then
+ str (chr (ord #"A" + n))
+ else
+ "U" ^ Int.toString (n - 26)
+ in
+ count := n + 1;
+ (L'.CUnif (loc, k, s, ref NONE), dummy)
+ end
+
+ end
+
+ fun elabKind (k, loc) =
+ case k of
+ L.KType => (L'.KType, loc)
+ | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
+ | L.KName => (L'.KName, loc)
+ | L.KRecord k => (L'.KRecord (elabKind k), loc)
+ | L.KUnit => (L'.KUnit, loc)
+ | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
+ | L.KWild => kunif loc
+
+ fun foldKind (dom, ran, loc)=
+ (L'.KArrow ((L'.KArrow ((L'.KName, loc),
+ (L'.KArrow (dom,
+ (L'.KArrow (ran, ran), loc)), loc)), loc),
+ (L'.KArrow (ran,
+ (L'.KArrow ((L'.KRecord dom, loc),
+ ran), loc)), loc)), loc)
+
+ fun hnormKind (kAll as (k, _)) =
+ case k of
+ L'.KUnif (_, _, ref (SOME k)) => hnormKind k
+ | _ => kAll
+
+ fun elabCon (env, denv) (c, loc) =
+ case c of
+ L.CAnnot (c, k) =>
+ let
+ val k' = elabKind k
+ val (c', ck, gs) = elabCon (env, denv) c
+ in
+ checkKind env c' ck k';
+ (c', k', gs)
+ end
+
+ | L.TFun (t1, t2) =>
+ let
+ val (t1', k1, gs1) = elabCon (env, denv) t1
+ val (t2', k2, gs2) = elabCon (env, denv) t2
+ in
+ checkKind env t1' k1 ktype;
+ checkKind env t2' k2 ktype;
+ ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
+ end
+ | L.TCFun (e, x, k, t) =>
+ let
+ val e' = elabExplicitness e
+ val k' = elabKind k
+ val env' = E.pushCRel env x k'
+ val (t', tk, gs) = elabCon (env', D.enter denv) t
+ in
+ checkKind env t' tk ktype;
+ ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
+ end
+ | L.CDisjoint (c1, c2, c) =>
+ let
+ val (c1', k1, gs1) = elabCon (env, denv) c1
+ val (c2', k2, gs2) = elabCon (env, denv) c2
+
+ val ku1 = kunif loc
+ val ku2 = kunif loc
+
+ val (denv', gs3) = D.assert env denv (c1', c2')
+ val (c', k, gs4) = elabCon (env, denv') c
+ in
+ checkKind env c1' k1 (L'.KRecord ku1, loc);
+ checkKind env c2' k2 (L'.KRecord ku2, loc);
+
+ ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
+ end
+ | L.TRecord c =>
+ let
+ val (c', ck, gs) = elabCon (env, denv) c
+ val k = (L'.KRecord ktype, loc)
+ in
+ checkKind env c' ck k;
+ ((L'.TRecord c', loc), ktype, gs)
+ end
+
+ | L.CVar ([], s) =>
+ (case E.lookupC env s of
+ E.NotBound =>
+ (conError env (UnboundCon (loc, s));
+ (cerror, kerror, []))
+ | E.Rel (n, k) =>
+ ((L'.CRel n, loc), k, [])
+ | E.Named (n, k) =>
+ ((L'.CNamed n, loc), k, []))
+ | L.CVar (m1 :: ms, s) =>
+ (case E.lookupStr env m1 of
+ NONE => (conError env (UnboundStrInCon (loc, m1));
+ (cerror, kerror, []))
+ | SOME (n, sgn) =>
+ let
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => (conError env (UnboundStrInCon (loc, m));
+ (strerror, sgnerror))
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+
+ val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
+ NONE => (conError env (UnboundCon (loc, s));
+ kerror)
+ | SOME (k, _) => k
+ in
+ ((L'.CModProj (n, ms, s), loc), k, [])
+ end)
+
+ | L.CApp (c1, c2) =>
+ let
+ val (c1', k1, gs1) = elabCon (env, denv) c1
+ val (c2', k2, gs2) = elabCon (env, denv) c2
+ val dom = kunif loc
+ val ran = kunif loc
+ in
+ checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
+ checkKind env c2' k2 dom;
+ ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
+ end
+ | L.CAbs (x, ko, t) =>
+ let
+ val k' = case ko of
+ NONE => kunif loc
+ | SOME k => elabKind k
+ val env' = E.pushCRel env x k'
+ val (t', tk, gs) = elabCon (env', D.enter denv) t
+ in
+ ((L'.CAbs (x, k', t'), loc),
+ (L'.KArrow (k', tk), loc),
+ gs)
+ end
+
+ | L.CName s =>
+ ((L'.CName s, loc), kname, [])
+
+ | L.CRecord xcs =>
+ let
+ val k = kunif loc
+
+ val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
+ let
+ val (x', xk, gs1) = elabCon (env, denv) x
+ val (c', ck, gs2) = elabCon (env, denv) c
+ in
+ checkKind env x' xk kname;
+ checkKind env c' ck k;
+ ((x', c'), gs1 @ gs2 @ gs)
+ end) [] xcs
+
+ val rc = (L'.CRecord (k, xcs'), loc)
+ (* Add duplicate field checking later. *)
+
+ fun prove (xcs, ds) =
+ case xcs of
+ [] => ds
+ | xc :: rest =>
+ let
+ val r1 = (L'.CRecord (k, [xc]), loc)
+ val ds = foldl (fn (xc', ds) =>
+ let
+ val r2 = (L'.CRecord (k, [xc']), loc)
+ in
+ D.prove env denv (r1, r2, loc) @ ds
+ end)
+ ds rest
+ in
+ prove (rest, ds)
+ end
+ in
+ (rc, (L'.KRecord k, loc), prove (xcs', gs))
+ end
+ | L.CConcat (c1, c2) =>
+ let
+ val (c1', k1, gs1) = elabCon (env, denv) c1
+ val (c2', k2, gs2) = elabCon (env, denv) c2
+ val ku = kunif loc
+ val k = (L'.KRecord ku, loc)
+ in
+ checkKind env c1' k1 k;
+ checkKind env c2' k2 k;
+ ((L'.CConcat (c1', c2'), loc), k,
+ D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
+ end
+ | L.CFold =>
+ let
+ val dom = kunif loc
+ val ran = kunif loc
+ in
+ ((L'.CFold (dom, ran), loc),
+ foldKind (dom, ran, loc),
+ [])
+ end
+
+ | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
+
+ | L.CTuple cs =>
+ let
+ val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
let
- val r2 = (L'.CRecord (k, [xc']), loc)
+ val (c', k, gs') = elabCon (env, denv) c
in
- D.prove env denv (r1, r2, loc) @ ds
- end)
- ds rest
- in
- prove (rest, ds)
- end
- in
- (rc, (L'.KRecord k, loc), prove (xcs', gs))
- end
- | L.CConcat (c1, c2) =>
- let
- val (c1', k1, gs1) = elabCon (env, denv) c1
- val (c2', k2, gs2) = elabCon (env, denv) c2
- val ku = kunif loc
- val k = (L'.KRecord ku, loc)
- in
- checkKind env c1' k1 k;
- checkKind env c2' k2 k;
- ((L'.CConcat (c1', c2'), loc), k,
- D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
- end
- | L.CFold =>
- let
- val dom = kunif loc
- val ran = kunif loc
- in
- ((L'.CFold (dom, ran), loc),
- foldKind (dom, ran, loc),
- [])
- end
-
- | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
-
- | L.CTuple cs =>
- let
- val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
- let
- val (c', k, gs') = elabCon (env, denv) c
- in
- (c' :: cs', k :: ks, gs' @ gs)
- end) ([], [], []) cs
- in
- ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
- end
- | L.CProj (c, n) =>
- let
- val (c', k, gs) = elabCon (env, denv) c
- in
- case hnormKind k of
- (L'.KTuple ks, _) =>
- if n <= 0 orelse n > length ks then
- (conError env (ProjBounds (c', n));
- (cerror, kerror, []))
- else
- ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
- | k => (conError env (ProjMismatch (c', k));
+ (c' :: cs', k :: ks, gs' @ gs)
+ end) ([], [], []) cs
+ in
+ ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
+ end
+ | L.CProj (c, n) =>
+ let
+ val (c', k, gs) = elabCon (env, denv) c
+ in
+ case hnormKind k of
+ (L'.KTuple ks, _) =>
+ if n <= 0 orelse n > length ks then
+ (conError env (ProjBounds (c', n));
(cerror, kerror, []))
- end
-
- | L.CWild k =>
- let
- val k' = elabKind k
- in
- (cunif (loc, k'), k', [])
- end
-
-fun kunifsRemain k =
- case k of
- L'.KUnif (_, _, ref NONE) => true
- | _ => false
-fun cunifsRemain c =
- case c of
- L'.CUnif (loc, _, _, ref NONE) => SOME loc
- | _ => NONE
-
-val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
- con = fn _ => false,
- exp = fn _ => false,
- sgn_item = fn _ => false,
- sgn = fn _ => false,
- str = fn _ => false,
- decl = fn _ => false}
-
-val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
- con = cunifsRemain,
- exp = fn _ => NONE,
- sgn_item = fn _ => NONE,
- sgn = fn _ => NONE,
- str = fn _ => NONE,
- decl = fn _ => NONE}
-
-fun occursCon r =
- U.Con.exists {kind = fn _ => false,
- con = fn L'.CUnif (_, _, _, r') => r = r'
- | _ => false}
-
-exception CUnify' of cunify_error
-
-exception SynUnif = E.SynUnif
-
-open ElabOps
-
-type record_summary = {
- fields : (L'.con * L'.con) list,
- unifs : (L'.con * L'.con option ref) list,
- others : L'.con list
-}
-
-fun summaryToCon {fields, unifs, others} =
- let
- val c = (L'.CRecord (ktype, []), dummy)
- val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
- val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
- in
- (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
- end
-
-fun p_summary env s = p_con env (summaryToCon s)
-
-exception CUnify of L'.con * L'.con * cunify_error
-
-fun kindof env (c, loc) =
- case c of
- L'.TFun _ => ktype
- | L'.TCFun _ => ktype
- | L'.TRecord _ => ktype
-
- | L'.CRel xn => #2 (E.lookupCRel env xn)
- | L'.CNamed xn => #2 (E.lookupCNamed env xn)
- | L'.CModProj (n, ms, x) =>
- let
- val (_, sgn) = E.lookupStrNamed env n
- val (str, sgn) = foldl (fn (m, (str, sgn)) =>
- case E.projectStr env {sgn = sgn, str = str, field = m} of
- NONE => raise Fail "kindof: Unknown substructure"
- | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
- ((L'.StrVar n, loc), sgn) ms
- in
- case E.projectCon env {sgn = sgn, str = str, field = x} of
- NONE => raise Fail "kindof: Unknown con in structure"
- | SOME (k, _) => k
- end
-
- | L'.CApp (c, _) =>
- (case hnormKind (kindof env c) of
- (L'.KArrow (_, k), _) => k
- | (L'.KError, _) => kerror
- | k => raise CUnify' (CKindof (k, c)))
- | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
- | L'.CDisjoint (_, _, _, c) => kindof env c
-
- | L'.CName _ => kname
-
- | L'.CRecord (k, _) => (L'.KRecord k, loc)
- | L'.CConcat (c, _) => kindof env c
- | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
-
- | L'.CUnit => (L'.KUnit, loc)
-
- | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
- | L'.CProj (c, n) =>
- (case hnormKind (kindof env c) of
- (L'.KTuple ks, _) => List.nth (ks, n - 1)
- | k => raise CUnify' (CKindof (k, c)))
-
- | L'.CError => kerror
- | L'.CUnif (_, k, _, _) => k
-
-val hnormCon = D.hnormCon
-
-datatype con_summary =
- Nil
- | Cons
- | Unknown
-
-fun compatible cs =
- case cs of
- (Unknown, _) => false
- | (_, Unknown) => false
- | (s1, s2) => s1 = s2
-
-fun summarizeCon (env, denv) c =
- let
- val (c, gs) = hnormCon (env, denv) c
- in
- case #1 c of
- L'.CRecord (_, []) => (Nil, gs)
- | L'.CRecord (_, _ :: _) => (Cons, gs)
- | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
- | L'.CDisjoint (_, _, _, c) =>
- let
- val (s, gs') = summarizeCon (env, denv) c
- in
- (s, gs @ gs')
- end
- | _ => (Unknown, gs)
- end
-
-fun p_con_summary s =
- Print.PD.string (case s of
- Nil => "Nil"
- | Cons => "Cons"
- | Unknown => "Unknown")
-
-exception SummaryFailure
-
-fun unifyRecordCons (env, denv) (c1, c2) =
- let
- fun rkindof c =
- case hnormKind (kindof env c) of
- (L'.KRecord k, _) => k
- | (L'.KError, _) => kerror
- | k => raise CUnify' (CKindof (k, c))
-
- val k1 = rkindof c1
- val k2 = rkindof c2
-
- val (r1, gs1) = recordSummary (env, denv) c1
- val (r2, gs2) = recordSummary (env, denv) c2
- in
- unifyKinds k1 k2;
- unifySummaries (env, denv) (k1, r1, r2);
- gs1 @ gs2
- end
-
-and recordSummary (env, denv) c =
- let
- val (c, gs) = hnormCon (env, denv) c
-
- val (sum, gs') =
- case c of
- (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
- | (L'.CConcat (c1, c2), _) =>
- let
- val (s1, gs1) = recordSummary (env, denv) c1
- val (s2, gs2) = recordSummary (env, denv) c2
- in
- ({fields = #fields s1 @ #fields s2,
- unifs = #unifs s1 @ #unifs s2,
- others = #others s1 @ #others s2},
- gs1 @ gs2)
- end
- | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
- | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
- | c' => ({fields = [], unifs = [], others = [c']}, [])
- in
- (sum, gs @ gs')
- end
-
-and consEq (env, denv) (c1, c2) =
- let
- val gs = unifyCons (env, denv) c1 c2
- in
- List.all (fn (loc, env, denv, c1, c2) =>
- case D.prove env denv (c1, c2, loc) of
- [] => true
- | _ => false) gs
- end
- handle CUnify _ => false
-
-and consNeq env (c1, c2) =
- case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
- (L'.CName x1, L'.CName x2) => x1 <> x2
- | _ => false
-
-and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
- let
- val loc = #2 k
- (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
- ("#2", p_summary env s2)]*)
-
- fun eatMatching p (ls1, ls2) =
- let
- fun em (ls1, ls2, passed1) =
- case ls1 of
- [] => (rev passed1, ls2)
- | h1 :: t1 =>
- let
- fun search (ls2', passed2) =
- case ls2' of
- [] => em (t1, ls2, h1 :: passed1)
- | h2 :: t2 =>
- if p (h1, h2) then
- em (t1, List.revAppend (passed2, t2), passed1)
- else
- search (t2, h2 :: passed2)
- in
- search (ls2, [])
- end
- in
- em (ls1, ls2, [])
- end
-
- val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
- not (consNeq env (x1, x2))
- andalso consEq (env, denv) (c1, c2)
- andalso consEq (env, denv) (x1, x2))
- (#fields s1, #fields s2)
- (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
- ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
- val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
- val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
- (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
- ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
-
- fun unifFields (fs, others, unifs) =
- case (fs, others, unifs) of
- ([], [], _) => ([], [], unifs)
- | (_, _, []) => (fs, others, [])
- | (_, _, (_, r) :: rest) =>
- let
- val r' = ref NONE
- val kr = (L'.KRecord k, dummy)
- val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
-
- val prefix = case (fs, others) of
- ([], other :: others) =>
- List.foldl (fn (other, c) =>
- (L'.CConcat (c, other), dummy))
- other others
- | (fs, []) =>
- (L'.CRecord (k, fs), dummy)
- | (fs, others) =>
- List.foldl (fn (other, c) =>
- (L'.CConcat (c, other), dummy))
- (L'.CRecord (k, fs), dummy) others
- in
- r := SOME (L'.CConcat (prefix, cr'), dummy);
- ([], [], (cr', r') :: rest)
- end
-
- val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
- val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
-
- (*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) =
- let
- val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
- in
- List.all (fn (loc, env, denv, c1, c2) =>
- case D.prove env denv (c1, c2, loc) of
- [] => true
- | _ => false) gs
- end
- handle SummaryFailure => false
-
- val (fs1, fs2, others1, others2) =
- case (fs1, fs2, others1, others2) of
- ([], _, [other1], []) =>
- if isGuessable (other1, fs2) then
- ([], [], [], [])
- else
- (fs1, fs2, others1, others2)
- | (_, [], [], [other2]) =>
- if isGuessable (other2, fs1) then
- ([], [], [], [])
- else
- (fs1, fs2, others1, others2)
- | _ => (fs1, fs2, others1, others2)
-
- (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
- ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
-
- val clear = case (fs1, others1, fs2, others2) of
- ([], [], [], []) => true
- | _ => false
- val empty = (L'.CRecord (k, []), dummy)
-
- fun unsummarize {fields, unifs, others} =
- let
- val c = (L'.CRecord (k, fields), loc)
-
- val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
- c unifs
- in
- foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
- c others
- end
-
- fun pairOffUnifs (unifs1, unifs2) =
- case (unifs1, unifs2) of
- ([], _) =>
- if clear then
- List.app (fn (_, r) => r := SOME empty) unifs2
- else
- raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
- | (_, []) =>
- if clear then
- List.app (fn (_, r) => r := SOME empty) unifs1
- else
- raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
- | ((c1, _) :: rest1, (_, r2) :: rest2) =>
- (r2 := SOME c1;
- pairOffUnifs (rest1, rest2))
- in
- pairOffUnifs (unifs1, unifs2)
- (*before eprefaces "Summaries'" [("#1", p_summary env s1),
- ("#2", p_summary env s2)]*)
- end
-
-and guessFold (env, denv) (c1, c2, gs, ex) =
- let
- val loc = #2 c1
+ else
+ ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
+ | k => (conError env (ProjMismatch (c', k));
+ (cerror, kerror, []))
+ end
+
+ | L.CWild k =>
+ let
+ val k' = elabKind k
+ in
+ (cunif (loc, k'), k', [])
+ end
+
+ fun kunifsRemain k =
+ case k of
+ L'.KUnif (_, _, ref NONE) => true
+ | _ => false
+ fun cunifsRemain c =
+ case c of
+ L'.CUnif (loc, _, _, ref NONE) => SOME loc
+ | _ => NONE
+
+ val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
+ con = fn _ => false,
+ exp = fn _ => false,
+ sgn_item = fn _ => false,
+ sgn = fn _ => false,
+ str = fn _ => false,
+ decl = fn _ => false}
+
+ val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
+ con = cunifsRemain,
+ exp = fn _ => NONE,
+ sgn_item = fn _ => NONE,
+ sgn = fn _ => NONE,
+ str = fn _ => NONE,
+ decl = fn _ => NONE}
+
+ fun occursCon r =
+ U.Con.exists {kind = fn _ => false,
+ con = fn L'.CUnif (_, _, _, r') => r = r'
+ | _ => false}
+
+ exception CUnify' of cunify_error
+
+ exception SynUnif = E.SynUnif
+
+ open ElabOps
+
+ type record_summary = {
+ fields : (L'.con * L'.con) list,
+ unifs : (L'.con * L'.con option ref) list,
+ others : L'.con list
+ }
+
+ fun summaryToCon {fields, unifs, others} =
+ let
+ val c = (L'.CRecord (ktype, []), dummy)
+ val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
+ val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
+ in
+ (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
+ end
+
+ fun p_summary env s = p_con env (summaryToCon s)
+
+ exception CUnify of L'.con * L'.con * cunify_error
+
+ fun kindof env (c, loc) =
+ case c of
+ L'.TFun _ => ktype
+ | L'.TCFun _ => ktype
+ | L'.TRecord _ => ktype
+
+ | L'.CRel xn => #2 (E.lookupCRel env xn)
+ | L'.CNamed xn => #2 (E.lookupCNamed env xn)
+ | L'.CModProj (n, ms, x) =>
+ let
+ val (_, sgn) = E.lookupStrNamed env n
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "kindof: Unknown substructure"
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case E.projectCon env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail "kindof: Unknown con in structure"
+ | SOME (k, _) => k
+ end
+
+ | L'.CApp (c, _) =>
+ (case hnormKind (kindof env c) of
+ (L'.KArrow (_, k), _) => k
+ | (L'.KError, _) => kerror
+ | k => raise CUnify' (CKindof (k, c)))
+ | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
+ | L'.CDisjoint (_, _, _, c) => kindof env c
+
+ | L'.CName _ => kname
+
+ | L'.CRecord (k, _) => (L'.KRecord k, loc)
+ | L'.CConcat (c, _) => kindof env c
+ | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
+
+ | L'.CUnit => (L'.KUnit, loc)
+
+ | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
+ | L'.CProj (c, n) =>
+ (case hnormKind (kindof env c) of
+ (L'.KTuple ks, _) => List.nth (ks, n - 1)
+ | k => raise CUnify' (CKindof (k, c)))
+
+ | L'.CError => kerror
+ | L'.CUnif (_, k, _, _) => k
+
+ val hnormCon = D.hnormCon
+
+ datatype con_summary =
+ Nil
+ | Cons
+ | Unknown
+
+ fun compatible cs =
+ case cs of
+ (Unknown, _) => false
+ | (_, Unknown) => false
+ | (s1, s2) => s1 = s2
+
+ fun summarizeCon (env, denv) c =
+ let
+ val (c, gs) = hnormCon (env, denv) c
+ in
+ case #1 c of
+ L'.CRecord (_, []) => (Nil, gs)
+ | L'.CRecord (_, _ :: _) => (Cons, gs)
+ | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
+ | L'.CDisjoint (_, _, _, c) =>
+ let
+ val (s, gs') = summarizeCon (env, denv) c
+ in
+ (s, gs @ gs')
+ end
+ | _ => (Unknown, gs)
+ end
+
+ fun p_con_summary s =
+ Print.PD.string (case s of
+ Nil => "Nil"
+ | Cons => "Cons"
+ | Unknown => "Unknown")
+
+ exception SummaryFailure
+
+ fun unifyRecordCons (env, denv) (c1, c2) =
+ let
+ fun rkindof c =
+ case hnormKind (kindof env c) of
+ (L'.KRecord k, _) => k
+ | (L'.KError, _) => kerror
+ | k => raise CUnify' (CKindof (k, c))
+
+ val k1 = rkindof c1
+ val k2 = rkindof c2
+
+ val (r1, gs1) = recordSummary (env, denv) c1
+ val (r2, gs2) = recordSummary (env, denv) c2
+ in
+ unifyKinds k1 k2;
+ unifySummaries (env, denv) (k1, r1, r2);
+ gs1 @ gs2
+ end
+
+ and recordSummary (env, denv) c =
+ let
+ val (c, gs) = hnormCon (env, denv) c
+
+ val (sum, gs') =
+ case c of
+ (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
+ | (L'.CConcat (c1, c2), _) =>
+ let
+ val (s1, gs1) = recordSummary (env, denv) c1
+ val (s2, gs2) = recordSummary (env, denv) c2
+ in
+ ({fields = #fields s1 @ #fields s2,
+ unifs = #unifs s1 @ #unifs s2,
+ others = #others s1 @ #others s2},
+ gs1 @ gs2)
+ end
+ | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
+ | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
+ | c' => ({fields = [], unifs = [], others = [c']}, [])
+ in
+ (sum, gs @ gs')
+ end
+
+ and consEq (env, denv) (c1, c2) =
+ let
+ val gs = unifyCons (env, denv) c1 c2
+ in
+ List.all (fn (loc, env, denv, c1, c2) =>
+ case D.prove env denv (c1, c2, loc) of
+ [] => true
+ | _ => false) gs
+ end
+ handle CUnify _ => false
+
+ and consNeq env (c1, c2) =
+ case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
+ (L'.CName x1, L'.CName x2) => x1 <> x2
+ | _ => false
+
+ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
+ let
+ val loc = #2 k
+ (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
+ ("#2", p_summary env s2)]*)
+
+ fun eatMatching p (ls1, ls2) =
+ let
+ fun em (ls1, ls2, passed1) =
+ case ls1 of
+ [] => (rev passed1, ls2)
+ | h1 :: t1 =>
+ let
+ fun search (ls2', passed2) =
+ case ls2' of
+ [] => em (t1, ls2, h1 :: passed1)
+ | h2 :: t2 =>
+ if p (h1, h2) then
+ em (t1, List.revAppend (passed2, t2), passed1)
+ else
+ search (t2, h2 :: passed2)
+ in
+ search (ls2, [])
+ end
+ in
+ em (ls1, ls2, [])
+ end
- fun unfold (dom, ran, f, i, r, c) =
- let
- val nm = cunif (loc, (L'.KName, loc))
- val v = cunif (loc, dom)
- val rest = cunif (loc, (L'.KRecord dom, loc))
- val acc = (L'.CFold (dom, ran), loc)
- val acc = (L'.CApp (acc, f), loc)
- val acc = (L'.CApp (acc, i), loc)
- val acc = (L'.CApp (acc, rest), loc)
-
- val (iS, gs3) = summarizeCon (env, denv) i
-
- val app = (L'.CApp (f, nm), loc)
- val app = (L'.CApp (app, v), loc)
- val app = (L'.CApp (app, acc), loc)
- val (appS, gs4) = summarizeCon (env, denv) app
-
- val (cS, gs5) = summarizeCon (env, denv) c
- in
- (*prefaces "Summaries" [("iS", p_con_summary iS),
- ("appS", p_con_summary appS),
- ("cS", p_con_summary cS)];*)
+ val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
+ not (consNeq env (x1, x2))
+ andalso consEq (env, denv) (c1, c2)
+ andalso consEq (env, denv) (x1, x2))
+ (#fields s1, #fields s2)
+ (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
+ ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
+ val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
+ val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
+ (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
+ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
+
+ fun unifFields (fs, others, unifs) =
+ case (fs, others, unifs) of
+ ([], [], _) => ([], [], unifs)
+ | (_, _, []) => (fs, others, [])
+ | (_, _, (_, r) :: rest) =>
+ let
+ val r' = ref NONE
+ val kr = (L'.KRecord k, dummy)
+ val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
+
+ val prefix = case (fs, others) of
+ ([], other :: others) =>
+ List.foldl (fn (other, c) =>
+ (L'.CConcat (c, other), dummy))
+ other others
+ | (fs, []) =>
+ (L'.CRecord (k, fs), dummy)
+ | (fs, others) =>
+ List.foldl (fn (other, c) =>
+ (L'.CConcat (c, other), dummy))
+ (L'.CRecord (k, fs), dummy) others
+ in
+ r := SOME (L'.CConcat (prefix, cr'), dummy);
+ ([], [], (cr', r') :: rest)
+ end
- if compatible (iS, appS) then
- raise ex
- else if compatible (cS, iS) then
- let
- (*val () = prefaces "Same?" [("i", p_con env i),
- ("c", p_con env c)]*)
- val gs6 = unifyCons (env, denv) i c
- (*val () = TextIO.print "Yes!\n"*)
+ val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
+ val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
- val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
- in
- gs @ gs3 @ gs5 @ gs6 @ gs7
- end
- else if compatible (cS, appS) then
- let
- (*val () = prefaces "Same?" [("app", p_con env app),
- ("c", p_con env c),
- ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
- val gs6 = unifyCons (env, denv) app c
- (*val () = TextIO.print "Yes!\n"*)
-
- val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
- val concat = (L'.CConcat (singleton, rest), loc)
- (*val () = prefaces "Pre-crew" [("r", p_con env r),
- ("concat", p_con env concat)]*)
- val gs7 = unifyCons (env, denv) r concat
- in
- (*prefaces "The crew" [("nm", p_con env nm),
- ("v", p_con env v),
- ("rest", p_con env rest)];*)
+ (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
+ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
- gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
- end
- else
- raise ex
- end
- handle _ => raise ex
- in
- case (#1 c1, #1 c2) of
- (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
- unfold (dom, ran, f, i, r, c2)
- | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
- unfold (dom, ran, f, i, r, c1)
- | _ => raise ex
- end
+ fun isGuessable (other, fs) =
+ let
+ val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
+ in
+ List.all (fn (loc, env, denv, c1, c2) =>
+ case D.prove env denv (c1, c2, loc) of
+ [] => true
+ | _ => false) gs
+ end
+ handle SummaryFailure => false
-and unifyCons' (env, denv) c1 c2 =
- case (#1 c1, #1 c2) of
- (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
- let
- val gs1 = unifyCons' (env, denv) x1 x2
- val gs2 = unifyCons' (env, denv) y1 y2
- val (denv', gs3) = D.assert env denv (x1, y1)
- val gs4 = unifyCons' (env, denv') t1 t2
- in
- gs1 @ gs2 @ gs3 @ gs4
- end
- | _ =>
- let
- val (c1, gs1) = hnormCon (env, denv) c1
- val (c2, gs2) = hnormCon (env, denv) c2
- in
- let
- val gs3 = unifyCons'' (env, denv) c1 c2
- in
- gs1 @ gs2 @ gs3
- end
- handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
- end
-
-and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
- let
- fun err f = raise CUnify' (f (c1All, c2All))
+ val (fs1, fs2, others1, others2) =
+ case (fs1, fs2, others1, others2) of
+ ([], _, [other1], []) =>
+ if isGuessable (other1, fs2) then
+ ([], [], [], [])
+ else
+ (fs1, fs2, others1, others2)
+ | (_, [], [], [other2]) =>
+ if isGuessable (other2, fs1) then
+ ([], [], [], [])
+ else
+ (fs1, fs2, others1, others2)
+ | _ => (fs1, fs2, others1, others2)
- fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
- in
- (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
- ("c2All", p_con env c2All)];*)
-
- case (c1, c2) of
- (L'.CUnit, L'.CUnit) => []
-
- | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
- unifyCons' (env, denv) d1 d2
- @ unifyCons' (env, denv) r1 r2
- | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
- if expl1 <> expl2 then
- err CExplicitness
- else
- (unifyKinds d1 d2;
- unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
- | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
+ (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
+ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
- | (L'.CRel n1, L'.CRel n2) =>
- if n1 = n2 then
- []
- else
- err CIncompatible
- | (L'.CNamed n1, L'.CNamed n2) =>
- if n1 = n2 then
- []
- else
- err CIncompatible
-
- | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
- (unifyCons' (env, denv) d1 d2;
- unifyCons' (env, denv) r1 r2)
- | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
- (unifyKinds k1 k2;
- unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
-
- | (L'.CName n1, L'.CName n2) =>
- if n1 = n2 then
- []
- else
- err CIncompatible
+ val clear = case (fs1, others1, fs2, others2) of
+ ([], [], [], []) => true
+ | _ => false
+ val empty = (L'.CRecord (k, []), dummy)
- | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
- if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
- []
- else
- err CIncompatible
-
- | (L'.CTuple cs1, L'.CTuple cs2) =>
- ((ListPair.foldlEq (fn (c1, c2, gs) =>
- let
- val gs' = unifyCons' (env, denv) c1 c2
- in
- gs' @ gs
- end) [] (cs1, cs2))
- handle ListPair.UnequalLengths => err CIncompatible)
-
- | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
- unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All
- | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
- unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc)
- | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
- let
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' (env, denv) (List.nth (us, n - 1)) c2All
- end
- | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
- let
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' (env, denv) c1All (List.nth (us, n - 1))
- end
- | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
- if n1 = n2 then
- unifyCons' (env, denv) c1 c2
- else
- err CIncompatible
+ fun unsummarize {fields, unifs, others} =
+ let
+ val c = (L'.CRecord (k, fields), loc)
- | (L'.CError, _) => []
- | (_, L'.CError) => []
+ val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
+ c unifs
+ in
+ foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
+ c others
+ end
- | (L'.CRecord _, _) => isRecord ()
- | (_, L'.CRecord _) => isRecord ()
- | (L'.CConcat _, _) => isRecord ()
- | (_, L'.CConcat _) => isRecord ()
+ fun pairOffUnifs (unifs1, unifs2) =
+ case (unifs1, unifs2) of
+ ([], _) =>
+ if clear then
+ List.app (fn (_, r) => r := SOME empty) unifs2
+ else
+ raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
+ | (_, []) =>
+ if clear then
+ List.app (fn (_, r) => r := SOME empty) unifs1
+ else
+ raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
+ | ((c1, _) :: rest1, (_, r2) :: rest2) =>
+ (r2 := SOME c1;
+ pairOffUnifs (rest1, rest2))
+ in
+ pairOffUnifs (unifs1, unifs2)
+ (*before eprefaces "Summaries'" [("#1", p_summary env s1),
+ ("#2", p_summary env s2)]*)
+ end
+
+ and guessFold (env, denv) (c1, c2, gs, ex) =
+ let
+ val loc = #2 c1
+
+ fun unfold (dom, ran, f, i, r, c) =
+ let
+ val nm = cunif (loc, (L'.KName, loc))
+ val v = cunif (loc, dom)
+ val rest = cunif (loc, (L'.KRecord dom, loc))
+ val acc = (L'.CFold (dom, ran), loc)
+ val acc = (L'.CApp (acc, f), loc)
+ val acc = (L'.CApp (acc, i), loc)
+ val acc = (L'.CApp (acc, rest), loc)
+
+ val (iS, gs3) = summarizeCon (env, denv) i
+
+ val app = (L'.CApp (f, nm), loc)
+ val app = (L'.CApp (app, v), loc)
+ val app = (L'.CApp (app, acc), loc)
+ val (appS, gs4) = summarizeCon (env, denv) app
+
+ val (cS, gs5) = summarizeCon (env, denv) c
+ in
+ (*prefaces "Summaries" [("iS", p_con_summary iS),
+ ("appS", p_con_summary appS),
+ ("cS", p_con_summary cS)];*)
- | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
- if r1 = r2 then
- []
- else
- (unifyKinds k1 k2;
- r1 := SOME c2All;
- [])
+ if compatible (iS, appS) then
+ raise ex
+ else if compatible (cS, iS) then
+ let
+ (*val () = prefaces "Same?" [("i", p_con env i),
+ ("c", p_con env c)]*)
+ val gs6 = unifyCons (env, denv) i c
+ (*val () = TextIO.print "Yes!\n"*)
- | (L'.CUnif (_, _, _, r), _) =>
- if occursCon r c2All then
- err COccursCheckFailed
- else
- (r := SOME c2All;
- [])
- | (_, L'.CUnif (_, _, _, r)) =>
- if occursCon r c1All then
- err COccursCheckFailed
- else
- (r := SOME c1All;
- [])
+ val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+ in
+ gs @ gs3 @ gs5 @ gs6 @ gs7
+ end
+ else if compatible (cS, appS) then
+ let
+ (*val () = prefaces "Same?" [("app", p_con env app),
+ ("c", p_con env c),
+ ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
+ val gs6 = unifyCons (env, denv) app c
+ (*val () = TextIO.print "Yes!\n"*)
+
+ val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
+ val concat = (L'.CConcat (singleton, rest), loc)
+ (*val () = prefaces "Pre-crew" [("r", p_con env r),
+ ("concat", p_con env concat)]*)
+ val gs7 = unifyCons (env, denv) r concat
+ in
+ (*prefaces "The crew" [("nm", p_con env nm),
+ ("v", p_con env v),
+ ("rest", p_con env rest)];*)
- | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
- (unifyKinds dom1 dom2;
- unifyKinds ran1 ran2;
+ gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+ end
+ else
+ raise ex
+ end
+ handle _ => raise ex
+ in
+ case (#1 c1, #1 c2) of
+ (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
+ unfold (dom, ran, f, i, r, c2)
+ | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
+ unfold (dom, ran, f, i, r, c1)
+ | _ => raise ex
+ end
+
+ and unifyCons' (env, denv) c1 c2 =
+ case (#1 c1, #1 c2) of
+ (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
+ let
+ val gs1 = unifyCons' (env, denv) x1 x2
+ val gs2 = unifyCons' (env, denv) y1 y2
+ val (denv', gs3) = D.assert env denv (x1, y1)
+ val gs4 = unifyCons' (env, denv') t1 t2
+ in
+ gs1 @ gs2 @ gs3 @ gs4
+ end
+ | _ =>
+ let
+ val (c1, gs1) = hnormCon (env, denv) c1
+ val (c2, gs2) = hnormCon (env, denv) c2
+ in
+ let
+ val gs3 = unifyCons'' (env, denv) c1 c2
+ in
+ gs1 @ gs2 @ gs3
+ end
+ handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
+ end
+
+ and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
+ let
+ fun err f = raise CUnify' (f (c1All, c2All))
+
+ fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
+ in
+ (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
+ ("c2All", p_con env c2All)];*)
+
+ case (c1, c2) of
+ (L'.CUnit, L'.CUnit) => []
+
+ | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
+ unifyCons' (env, denv) d1 d2
+ @ unifyCons' (env, denv) r1 r2
+ | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
+ if expl1 <> expl2 then
+ err CExplicitness
+ else
+ (unifyKinds d1 d2;
+ unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
+ | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
+
+ | (L'.CRel n1, L'.CRel n2) =>
+ if n1 = n2 then
+ []
+ else
+ err CIncompatible
+ | (L'.CNamed n1, L'.CNamed n2) =>
+ if n1 = n2 then
+ []
+ else
+ err CIncompatible
+
+ | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
+ (unifyCons' (env, denv) d1 d2;
+ unifyCons' (env, denv) r1 r2)
+ | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
+ (unifyKinds k1 k2;
+ unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
+
+ | (L'.CName n1, L'.CName n2) =>
+ if n1 = n2 then
+ []
+ else
+ err CIncompatible
+
+ | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
+ if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
+ []
+ else
+ err CIncompatible
+
+ | (L'.CTuple cs1, L'.CTuple cs2) =>
+ ((ListPair.foldlEq (fn (c1, c2, gs) =>
+ let
+ val gs' = unifyCons' (env, denv) c1 c2
+ in
+ gs' @ gs
+ end) [] (cs1, cs2))
+ handle ListPair.UnequalLengths => err CIncompatible)
+
+ | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
+ unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All
+ | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
+ unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc)
+ | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
+ let
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' (env, denv) (List.nth (us, n - 1)) c2All
+ end
+ | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
+ let
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' (env, denv) c1All (List.nth (us, n - 1))
+ end
+ | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
+ if n1 = n2 then
+ unifyCons' (env, denv) c1 c2
+ else
+ err CIncompatible
+
+ | (L'.CError, _) => []
+ | (_, L'.CError) => []
+
+ | (L'.CRecord _, _) => isRecord ()
+ | (_, L'.CRecord _) => isRecord ()
+ | (L'.CConcat _, _) => isRecord ()
+ | (_, L'.CConcat _) => isRecord ()
+
+ | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
+ if r1 = r2 then
+ []
+ else
+ (unifyKinds k1 k2;
+ r1 := SOME c2All;
+ [])
+
+ | (L'.CUnif (_, _, _, r), _) =>
+ if occursCon r c2All then
+ err COccursCheckFailed
+ else
+ (r := SOME c2All;
+ [])
+ | (_, L'.CUnif (_, _, _, r)) =>
+ if occursCon r c1All then
+ err COccursCheckFailed
+ else
+ (r := SOME c1All;
+ [])
+
+ | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
+ (unifyKinds dom1 dom2;
+ unifyKinds ran1 ran2;
+ [])
+
+ | _ => err CIncompatible
+ end
+
+ and unifyCons (env, denv) c1 c2 =
+ unifyCons' (env, denv) c1 c2
+ handle CUnify' err => raise CUnify (c1, c2, err)
+ | KUnify args => raise CUnify (c1, c2, CKind args)
+
+ fun checkCon (env, denv) e c1 c2 =
+ unifyCons (env, denv) c1 c2
+ handle CUnify (c1, c2, err) =>
+ (expError env (Unify (e, c1, c2, err));
[])
- | _ => err CIncompatible
- end
+ fun checkPatCon (env, denv) p c1 c2 =
+ unifyCons (env, denv) c1 c2
+ handle CUnify (c1, c2, err) =>
+ (expError env (PatUnify (p, c1, c2, err));
+ [])
-and unifyCons (env, denv) c1 c2 =
- unifyCons' (env, denv) c1 c2
- handle CUnify' err => raise CUnify (c1, c2, err)
- | KUnify args => raise CUnify (c1, c2, CKind args)
-
-fun checkCon (env, denv) e c1 c2 =
- unifyCons (env, denv) c1 c2
- handle CUnify (c1, c2, err) =>
- (expError env (Unify (e, c1, c2, err));
- [])
-
-fun checkPatCon (env, denv) p c1 c2 =
- unifyCons (env, denv) c1 c2
- handle CUnify (c1, c2, err) =>
- (expError env (PatUnify (p, c1, c2, err));
- [])
-
-fun primType env p =
- case p of
- P.Int _ => !int
- | P.Float _ => !float
- | P.String _ => !string
-
-fun recCons (k, nm, v, rest, loc) =
- (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
- rest), loc)
-
-fun foldType (dom, loc) =
- (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
- (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
- (L'.TCFun (L'.Explicit, "v", dom,
- (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
- (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
- (L'.CDisjoint (L'.Instantiate,
- (L'.CRecord
- ((L'.KUnit, loc),
- [((L'.CRel 2, loc),
- (L'.CUnit, loc))]), loc),
- (L'.CRel 0, loc),
- (L'.CApp ((L'.CRel 3, loc),
- recCons (dom,
- (L'.CRel 2, loc),
- (L'.CRel 1, loc),
- (L'.CRel 0, loc),
- loc)), loc)),
- loc)), loc)),
- loc)), loc)), loc),
- (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
- (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
- (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
- loc)), loc)), loc)
-
-datatype constraint =
- Disjoint of D.goal
- | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
-
-val enD = map Disjoint
-
-fun elabHead (env, denv) (e as (_, loc)) t =
- let
- fun unravel (t, e) =
- let
- val (t, gs) = hnormCon (env, denv) t
- in
- case t of
- (L'.TCFun (L'.Implicit, x, k, t'), _) =>
- let
- val u = cunif (loc, k)
+ fun primType env p =
+ case p of
+ P.Int _ => !int
+ | P.Float _ => !float
+ | P.String _ => !string
+
+ fun recCons (k, nm, v, rest, loc) =
+ (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
+ rest), loc)
+
+ fun foldType (dom, loc) =
+ (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
+ (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
+ (L'.TCFun (L'.Explicit, "v", dom,
+ (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
+ (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
+ (L'.CDisjoint (L'.Instantiate,
+ (L'.CRecord
+ ((L'.KUnit, loc),
+ [((L'.CRel 2, loc),
+ (L'.CUnit, loc))]), loc),
+ (L'.CRel 0, loc),
+ (L'.CApp ((L'.CRel 3, loc),
+ recCons (dom,
+ (L'.CRel 2, loc),
+ (L'.CRel 1, loc),
+ (L'.CRel 0, loc),
+ loc)), loc)),
+ loc)), loc)),
+ loc)), loc)), loc),
+ (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
+ (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
+ (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
+ loc)), loc)), loc)
+
+ datatype constraint =
+ Disjoint of D.goal
+ | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
+
+ val enD = map Disjoint
+
+ fun elabHead (env, denv) infer (e as (_, loc)) t =
+ let
+ fun unravel (t, e) =
+ let
+ val (t, gs) = hnormCon (env, denv) t
+ in
+ case t of
+ (L'.TCFun (L'.Implicit, x, k, t'), _) =>
+ let
+ val u = cunif (loc, k)
- val t'' = subConInCon (0, u) t'
- val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
- in
- (*prefaces "Unravel" [("t'", p_con env t'),
- ("t''", p_con env t'')];*)
- (e, t, enD gs @ gs')
- end
+ val t'' = subConInCon (0, u) t'
+ val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
+ in
+ (*prefaces "Unravel" [("t'", p_con env t'),
+ ("t''", p_con env t'')];*)
+ (e, t, enD gs @ gs')
+ end
+ | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) =>
+ let
+ val cl = #1 (hnormCon (env, denv) cl)
+ in
+ if infer <> L.TypesOnly andalso E.isClass env cl then
+ let
+ val r = ref NONE
+ val (e, t, gs') = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
+ in
+ (e, t, TypeClass (env, dom, r, loc) :: enD gs @ gs')
+ end
+ else
+ (e, t, enD gs)
+ end
| _ => (e, t, enD gs)
end
in
- unravel (t, e)
+ case infer of
+ L.DontInfer => (e, t, [])
+ | _ => unravel (t, e)
end
fun elabPat (pAll as (p, loc), (env, denv, bound)) =
@@ -1393,18 +1409,14 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
end
| L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
- | L.EVar ([], s) =>
+ | L.EVar ([], s, infer) =>
(case E.lookupE env s of
E.NotBound =>
(expError env (UnboundExp (loc, s));
(eerror, cerror, []))
- | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
- | E.Named (n, t) =>
- if Char.isUpper (String.sub (s, 0)) then
- elabHead (env, denv) (L'.ENamed n, loc) t
- else
- ((L'.ENamed n, loc), t, []))
- | L.EVar (m1 :: ms, s) =>
+ | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
+ | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t)
+ | L.EVar (m1 :: ms, s, infer) =>
(case E.lookupStr env m1 of
NONE => (expError env (UnboundStrInExp (loc, m1));
(eerror, cerror, []))
@@ -1422,7 +1434,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
cerror)
| SOME t => t
in
- ((L'.EModProj (n, ms, s), loc), t, [])
+ elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t
end)
| L.EWild =>
@@ -1436,17 +1448,16 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.EApp (e1, e2) =>
let
val (e1', t1, gs1) = elabExp (env, denv) e1
- val (e1', t1, gs2) = elabHead (env, denv) e1' t1
- val (e2', t2, gs3) = elabExp (env, denv) e2
+ val (e2', t2, gs2) = elabExp (env, denv) e2
val dom = cunif (loc, ktype)
val ran = cunif (loc, ktype)
val t = (L'.TFun (dom, ran), dummy)
- val gs4 = checkCon (env, denv) e1' t1 t
- val gs5 = checkCon (env, denv) e2' t2 dom
+ val gs3 = checkCon (env, denv) e1' t1 t
+ val gs4 = checkCon (env, denv) e2' t2 dom
- val gs = gs1 @ gs2 @ gs3 @ enD gs4 @ enD gs5
+ val gs = gs1 @ gs2 @ enD gs3 @ enD gs4
in
((L'.EApp (e1', e2'), loc), ran, gs)
end
@@ -1472,9 +1483,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
let
val (e', et, gs1) = elabExp (env, denv) e
val oldEt = et
- val (e', et, gs2) = elabHead (env, denv) e' et
- val (c', ck, gs3) = elabCon (env, denv) c
- val ((et', _), gs4) = hnormCon (env, denv) et
+ val (c', ck, gs2) = elabCon (env, denv) c
+ val ((et', _), gs3) = hnormCon (env, denv) et
in
case et' of
L'.CError => (eerror, cerror, [])
@@ -1491,7 +1501,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
("eb", p_con (E.pushCRel env x k) eb),
("c", p_con env c'),
("eb'", p_con env eb')];*)
- ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
+ ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2 @ enD gs3)
end
| _ =>
diff --git a/src/monoize.sml b/src/monoize.sml
index 06156544..36ae4a08 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -916,7 +916,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
end
| _ => poly ())
- | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), changed), _), _) =>
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), _), _), changed) =>
(case monoType env (L.TRecord changed, loc) of
(L'.TRecord changed, _) =>
let
diff --git a/src/source.sml b/src/source.sml
index d99907ae..23d2089f 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -105,11 +105,16 @@ datatype pat' =
withtype pat = pat' located
+datatype inference =
+ Infer
+ | DontInfer
+ | TypesOnly
+
datatype exp' =
EAnnot of exp * con
| EPrim of Prim.t
- | EVar of string list * string
+ | EVar of string list * string * inference
| EApp of exp * exp
| EAbs of string * con option * exp
| ECApp of exp * con
diff --git a/src/source_print.sml b/src/source_print.sml
index 324b50d5..f9fc8a53 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -199,7 +199,7 @@ fun p_exp' par (e, _) =
string ")"]
| EPrim p => Prim.p_t p
- | EVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
+ | EVar (ss, s, _) => p_list_sep (string ".") string (ss @ [s])
| EApp (e1, e2) => parenIf par (box [p_exp e1,
space,
p_exp' true e2])
diff --git a/src/urweb.grm b/src/urweb.grm
index f47e26bb..9a9081a3 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -116,17 +116,13 @@ fun amend_group loc (gi, tabs) =
tabs
end
-fun sql_inject (v, t, loc) =
- let
- val e = (EApp ((EVar (["Basis"], "sql_inject"), loc), (t, loc)), loc)
- in
- (EApp (e, (v, loc)), loc)
- end
+fun sql_inject (v, loc) =
+ (EApp ((EVar (["Basis"], "sql_inject", Infer), loc), (v, loc)), loc)
fun sql_compare (oper, sqlexp1, sqlexp2, loc) =
let
- val e = (EVar (["Basis"], "sql_comparison"), loc)
- val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper), loc)), loc)
+ val e = (EVar (["Basis"], "sql_comparison", Infer), loc)
+ val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper, Infer), loc)), loc)
val e = (EApp (e, sqlexp1), loc)
in
(EApp (e, sqlexp2), loc)
@@ -134,8 +130,8 @@ fun sql_compare (oper, sqlexp1, sqlexp2, loc) =
fun sql_binary (oper, sqlexp1, sqlexp2, loc) =
let
- val e = (EVar (["Basis"], "sql_binary"), loc)
- val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper), loc)), loc)
+ val e = (EVar (["Basis"], "sql_binary", Infer), loc)
+ val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper, Infer), loc)), loc)
val e = (EApp (e, sqlexp1), loc)
in
(EApp (e, sqlexp2), loc)
@@ -143,16 +139,16 @@ fun sql_binary (oper, sqlexp1, sqlexp2, loc) =
fun sql_unary (oper, sqlexp, loc) =
let
- val e = (EVar (["Basis"], "sql_unary"), loc)
- val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper), loc)), loc)
+ val e = (EVar (["Basis"], "sql_unary", Infer), loc)
+ val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper, Infer), loc)), loc)
in
(EApp (e, sqlexp), loc)
end
fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
let
- val e = (EVar (["Basis"], "sql_relop"), loc)
- val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper), loc)), loc)
+ val e = (EVar (["Basis"], "sql_relop", Infer), loc)
+ val e = (EApp (e, (EVar (["Basis"], "sql_" ^ oper, Infer), loc)), loc)
val e = (EApp (e, sqlexp1), loc)
in
(EApp (e, sqlexp2), loc)
@@ -160,16 +156,14 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) =
fun native_unop (oper, e1, loc) =
let
- val e = (EVar (["Basis"], oper), loc)
- val e = (EApp (e, (EWild, loc)), loc)
+ val e = (EVar (["Basis"], oper, Infer), loc)
in
(EApp (e, e1), loc)
end
fun native_op (oper, e1, e2, loc) =
let
- val e = (EVar (["Basis"], oper), loc)
- val e = (EApp (e, (EWild, loc)), loc)
+ val e = (EVar (["Basis"], oper, Infer), loc)
val e = (EApp (e, e1), loc)
in
(EApp (e, e2), loc)
@@ -191,7 +185,7 @@ fun tagIn bt =
| SYMBOL of string | CSYMBOL of string
| LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
| EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
- | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD
+ | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
| CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
| DATATYPE | OF
| TYPE | NAME
@@ -676,14 +670,14 @@ eexp : eapps (eapps)
end)
| SYMBOL LARROW eexp SEMI eexp (let
val loc = s (SYMBOLleft, eexp2right)
- val e = (EVar (["Basis"], "bind"), loc)
+ val e = (EVar (["Basis"], "bind", Infer), loc)
val e = (EApp (e, eexp1), loc)
in
(EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc)
end)
| UNIT LARROW eexp SEMI eexp (let
val loc = s (UNITleft, eexp2right)
- val e = (EVar (["Basis"], "bind"), loc)
+ val e = (EVar (["Basis"], "bind", Infer), loc)
val e = (EApp (e, eexp1), loc)
val t = (TRecord (CRecord [], loc), loc)
in
@@ -804,8 +798,12 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
e)) etuple), loc)
end)
- | path (EVar path, s (pathleft, pathright))
- | cpath (EVar cpath, s (cpathleft, cpathright))
+ | path (EVar (#1 path, #2 path, Infer), s (pathleft, pathright))
+ | cpath (EVar (#1 cpath, #2 cpath, Infer), s (cpathleft, cpathright))
+ | AT path (EVar (#1 path, #2 path, TypesOnly), s (ATleft, pathright))
+ | AT AT path (EVar (#1 path, #2 path, DontInfer), s (AT1left, pathright))
+ | AT cpath (EVar (#1 cpath, #2 cpath, TypesOnly), s (ATleft, cpathright))
+ | AT AT cpath (EVar (#1 cpath, #2 cpath, DontInfer), s (AT1left, cpathright))
| LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright))
| UNIT (ERecord [], s (UNITleft, UNITright))
@@ -818,7 +816,21 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
in
foldl (fn (ident, e) =>
(EField (e, ident), loc))
- (EVar path, s (pathleft, pathright)) idents
+ (EVar (#1 path, #2 path, Infer), s (pathleft, pathright)) idents
+ end)
+ | AT path DOT idents (let
+ val loc = s (ATleft, identsright)
+ in
+ foldl (fn (ident, e) =>
+ (EField (e, ident), loc))
+ (EVar (#1 path, #2 path, TypesOnly), s (pathleft, pathright)) idents
+ end)
+ | AT AT path DOT idents (let
+ val loc = s (AT1left, identsright)
+ in
+ foldl (fn (ident, e) =>
+ (EField (e, ident), loc))
+ (EVar (#1 path, #2 path, DontInfer), s (pathleft, pathright)) idents
end)
| FOLD (EFold, s (FOLDleft, FOLDright))
@@ -838,7 +850,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
()
else
ErrorMsg.errorAt loc "Initial XML tag pair aren't both tagged \"xml\".";
- (EApp ((EVar (["Basis"], "cdata"), loc),
+ (EApp ((EVar (["Basis"], "cdata", Infer), loc),
(EPrim (Prim.String ""), loc)),
loc)
end)
@@ -849,7 +861,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
()
else
ErrorMsg.errorAt loc "Initial XML tag pair aren't both tagged \"xml\".";
- (EApp ((EVar (["Basis"], "cdata"), loc),
+ (EApp ((EVar (["Basis"], "cdata", Infer), loc),
(EPrim (Prim.String ""), loc)),
loc)
end)
@@ -862,7 +874,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
(let
val loc = s (LPAREN1left, RPAREN3right)
- val e = (EVar (["Basis"], "insert"), loc)
+ val e = (EVar (["Basis"], "insert", Infer), loc)
val e = (EApp (e, texp), loc)
in
if length fields <> length sqlexps then
@@ -875,7 +887,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
(let
val loc = s (LPARENleft, RPARENright)
- val e = (EVar (["Basis"], "update"), loc)
+ val e = (EVar (["Basis"], "update", Infer), loc)
val e = (ECApp (e, (CWild (KRecord (KType, loc), loc), loc)), loc)
val e = (EApp (e, (ERecord fsets, loc)), loc)
val e = (EApp (e, texp), loc)
@@ -886,7 +898,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
(let
val loc = s (LPARENleft, RPARENright)
- val e = (EVar (["Basis"], "delete"), loc)
+ val e = (EVar (["Basis"], "delete", Infer), loc)
val e = (EApp (e, texp), loc)
in
(EApp (e, sqlexp), loc)
@@ -897,7 +909,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
enterDml : (inDml := true)
leaveDml : (inDml := false)
-texp : SYMBOL (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))
+texp : SYMBOL (EVar ([], SYMBOL, Infer), s (SYMBOLleft, SYMBOLright))
| LBRACE LBRACE eexp RBRACE RBRACE (eexp)
fields : fident ([fident])
@@ -953,20 +965,20 @@ xml : xmlOne xml (let
val pos = s (xmlOneleft, xmlright)
in
(EApp ((EApp (
- (EVar (["Basis"], "join"), pos),
+ (EVar (["Basis"], "join", Infer), pos),
xmlOne), pos),
xml), pos)
end)
| xmlOne (xmlOne)
-xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata"), s (NOTAGSleft, NOTAGSright)),
+xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer), s (NOTAGSleft, NOTAGSright)),
(EPrim (Prim.String NOTAGS), s (NOTAGSleft, NOTAGSright))),
s (NOTAGSleft, NOTAGSright))
| tag DIVIDE GT (let
val pos = s (tagleft, GTright)
in
(EApp (#2 tag,
- (EApp ((EVar (["Basis"], "cdata"), pos),
+ (EApp ((EVar (["Basis"], "cdata", Infer), pos),
(EPrim (Prim.String ""), pos)),
pos)), pos)
end)
@@ -977,7 +989,7 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata"), s (NO
in
if #1 tag = et then
if et = "form" then
- (EApp ((EVar (["Basis"], "form"), pos),
+ (EApp ((EVar (["Basis"], "form", Infer), pos),
xml), pos)
else
(EApp (#2 tag, xml), pos)
@@ -991,8 +1003,7 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata"), s (NO
| LBRACE eexp RBRACE (eexp)
| LBRACE LBRACK eexp RBRACK RBRACE (let
val loc = s (LBRACEleft, RBRACEright)
- val e = (EVar (["Top"], "txt"), loc)
- val e = (EApp (e, (EWild, loc)), loc)
+ val e = (EVar (["Top"], "txt", Infer), loc)
in
(EApp (e, eexp), loc)
end)
@@ -1001,7 +1012,7 @@ tag : tagHead attrs (let
val pos = s (tagHeadleft, attrsright)
in
(#1 tagHead,
- (EApp ((EApp ((EVar (["Basis"], "tag"), pos),
+ (EApp ((EApp ((EVar (["Basis"], "tag", Infer), pos),
(ERecord attrs, pos)), pos),
(EApp (#2 tagHead,
(ERecord [], pos)), pos)),
@@ -1013,7 +1024,7 @@ tagHead: BEGIN_TAG (let
val pos = s (BEGIN_TAGleft, BEGIN_TAGright)
in
(bt,
- (EVar ([], bt), pos))
+ (EVar ([], bt, Infer), pos))
end)
| tagHead LBRACE cexp RBRACE (#1 tagHead, (ECApp (#2 tagHead, cexp), s (tagHeadleft, RBRACEright)))
@@ -1039,7 +1050,7 @@ query : query1 obopt lopt ofopt (let
((CName "Offset", loc),
ofopt)], loc)
in
- (EApp ((EVar (["Basis"], "sql_query"), loc), re), loc)
+ (EApp ((EVar (["Basis"], "sql_query", Infer), loc), re), loc)
end)
query1 : SELECT select FROM tables wopt gopt hopt
@@ -1069,7 +1080,8 @@ query1 : SELECT select FROM tables wopt gopt hopt
val sel = (CRecord sel, loc)
val grp = case gopt of
- NONE => (ECApp ((EVar (["Basis"], "sql_subset_all"), loc),
+ NONE => (ECApp ((EVar (["Basis"], "sql_subset_all",
+ Infer), loc),
(CWild (KRecord (KRecord (KType, loc), loc),
loc), loc)), loc)
| SOME gis =>
@@ -1085,11 +1097,11 @@ query1 : SELECT select FROM tables wopt gopt hopt
loc),
loc)], loc))) tabs
in
- (ECApp ((EVar (["Basis"], "sql_subset"), loc),
+ (ECApp ((EVar (["Basis"], "sql_subset", Infer), loc),
(CRecord tabs, loc)), loc)
end
- val e = (EVar (["Basis"], "sql_query1"), loc)
+ val e = (EVar (["Basis"], "sql_query1", Infer), loc)
val re = (ERecord [((CName "From", loc),
(ERecord tables, loc)),
((CName "Where", loc),
@@ -1099,7 +1111,7 @@ query1 : SELECT select FROM tables wopt gopt hopt
((CName "Having", loc),
hopt),
((CName "SelectFields", loc),
- (ECApp ((EVar (["Basis"], "sql_subset"), loc),
+ (ECApp ((EVar (["Basis"], "sql_subset", Infer), loc),
sel), loc)),
((CName "SelectExps", loc),
(ERecord exps, loc))], loc)
@@ -1119,8 +1131,8 @@ tname : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLr
| LBRACE cexp RBRACE (cexp)
table : SYMBOL ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)),
- (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
- | SYMBOL AS tname (tname, (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)))
+ (EVar ([], SYMBOL, Infer), s (SYMBOLleft, SYMBOLright)))
+ | SYMBOL AS tname (tname, (EVar ([], SYMBOL, Infer), s (SYMBOLleft, SYMBOLright)))
| LBRACE LBRACE eexp RBRACE RBRACE AS tname (tname, eexp)
tident : SYMBOL (CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright))
@@ -1140,26 +1152,21 @@ selis : seli ([seli])
select : STAR (Star)
| selis (Items selis)
-sqlexp : TRUE (sql_inject (EVar (["Basis"], "True"),
- EVar (["Basis"], "sql_bool"),
+sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", Infer),
s (TRUEleft, TRUEright)))
- | FALSE (sql_inject (EVar (["Basis"], "False"),
- EVar (["Basis"], "sql_bool"),
+ | FALSE (sql_inject (EVar (["Basis"], "False", Infer),
s (FALSEleft, FALSEright)))
| INT (sql_inject (EPrim (Prim.Int INT),
- EVar (["Basis"], "sql_int"),
s (INTleft, INTright)))
| FLOAT (sql_inject (EPrim (Prim.Float FLOAT),
- EVar (["Basis"], "sql_float"),
s (FLOATleft, FLOATright)))
| STRING (sql_inject (EPrim (Prim.String STRING),
- EVar (["Basis"], "sql_string"),
s (STRINGleft, STRINGright)))
| tident DOT fident (let
val loc = s (tidentleft, fidentright)
- val e = (EVar (["Basis"], "sql_field"), loc)
+ val e = (EVar (["Basis"], "sql_field", Infer), loc)
val e = (ECApp (e, tident), loc)
in
(ECApp (e, fident), loc)
@@ -1169,14 +1176,14 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True"),
in
if !inDml then
let
- val e = (EVar (["Basis"], "sql_field"), loc)
+ val e = (EVar (["Basis"], "sql_field", Infer), loc)
val e = (ECApp (e, (CName "T", loc)), loc)
in
(ECApp (e, (CName CSYMBOL, loc)), loc)
end
else
let
- val e = (EVar (["Basis"], "sql_exp"), loc)
+ val e = (EVar (["Basis"], "sql_exp", Infer), loc)
in
(ECApp (e, (CName CSYMBOL, loc)), loc)
end
@@ -1194,29 +1201,26 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True"),
| NOT sqlexp (sql_unary ("not", sqlexp, s (NOTleft, sqlexpright)))
| LBRACE eexp RBRACE (sql_inject (#1 eexp,
- EWild,
s (LBRACEleft, RBRACEright)))
| LPAREN sqlexp RPAREN (sqlexp)
| COUNT LPAREN STAR RPAREN (let
val loc = s (COUNTleft, RPARENright)
in
- (EApp ((EVar (["Basis"], "sql_count"), loc),
+ (EApp ((EVar (["Basis"], "sql_count", Infer), loc),
(ERecord [], loc)), loc)
end)
| sqlagg LPAREN sqlexp RPAREN (let
val loc = s (sqlaggleft, RPARENright)
- val e = (EApp ((EVar (["Basis"], "sql_" ^ sqlagg), loc),
- (EWild, loc)), loc)
- val e = (EApp ((EVar (["Basis"], "sql_aggregate"), loc),
+ val e = (EVar (["Basis"], "sql_" ^ sqlagg, Infer), loc)
+ val e = (EApp ((EVar (["Basis"], "sql_aggregate", Infer), loc),
e), loc)
in
(EApp (e, sqlexp), loc)
end)
-wopt : (sql_inject (EVar (["Basis"], "True"),
- EVar (["Basis"], "sql_bool"),
+wopt : (sql_inject (EVar (["Basis"], "True", Infer),
dummy))
| CWHERE sqlexp (sqlexp)
@@ -1228,12 +1232,11 @@ groupis: groupi ([groupi])
gopt : (NONE)
| GROUP BY groupis (SOME groupis)
-hopt : (sql_inject (EVar (["Basis"], "True"),
- EVar (["Basis"], "sql_bool"),
+hopt : (sql_inject (EVar (["Basis"], "True", Infer),
dummy))
| HAVING sqlexp (sqlexp)
-obopt : (ECApp ((EVar (["Basis"], "sql_order_by_Nil"), dummy),
+obopt : (ECApp ((EVar (["Basis"], "sql_order_by_Nil", Infer), dummy),
(CWild (KRecord (KType, dummy), dummy), dummy)),
dummy)
| ORDER BY obexps (obexps)
@@ -1243,10 +1246,10 @@ obitem : sqlexp diropt (sqlexp, diropt)
obexps : obitem (let
val loc = s (obitemleft, obitemright)
- val e' = (ECApp ((EVar (["Basis"], "sql_order_by_Nil"), loc),
+ val e' = (ECApp ((EVar (["Basis"], "sql_order_by_Nil", Infer), loc),
(CWild (KRecord (KType, loc), loc), loc)),
loc)
- val e = (EApp ((EVar (["Basis"], "sql_order_by_Cons"), loc),
+ val e = (EApp ((EVar (["Basis"], "sql_order_by_Cons", Infer), loc),
#1 obitem), loc)
val e = (EApp (e, #2 obitem), loc)
in
@@ -1255,30 +1258,30 @@ obexps : obitem (let
| obitem COMMA obexps (let
val loc = s (obitemleft, obexpsright)
- val e = (EApp ((EVar (["Basis"], "sql_order_by_Cons"), loc),
+ val e = (EApp ((EVar (["Basis"], "sql_order_by_Cons", Infer), loc),
#1 obitem), loc)
val e = (EApp (e, #2 obitem), loc)
in
(EApp (e, obexps), loc)
end)
-diropt : (EVar (["Basis"], "sql_asc"), dummy)
- | ASC (EVar (["Basis"], "sql_asc"), s (ASCleft, ASCright))
- | DESC (EVar (["Basis"], "sql_desc"), s (DESCleft, DESCright))
+diropt : (EVar (["Basis"], "sql_asc", Infer), dummy)
+ | ASC (EVar (["Basis"], "sql_asc", Infer), s (ASCleft, ASCright))
+ | DESC (EVar (["Basis"], "sql_desc", Infer), s (DESCleft, DESCright))
-lopt : (EVar (["Basis"], "sql_no_limit"), dummy)
- | LIMIT ALL (EVar (["Basis"], "sql_no_limit"), dummy)
+lopt : (EVar (["Basis"], "sql_no_limit", Infer), dummy)
+ | LIMIT ALL (EVar (["Basis"], "sql_no_limit", Infer), dummy)
| LIMIT sqlint (let
val loc = s (LIMITleft, sqlintright)
in
- (EApp ((EVar (["Basis"], "sql_limit"), loc), sqlint), loc)
+ (EApp ((EVar (["Basis"], "sql_limit", Infer), loc), sqlint), loc)
end)
-ofopt : (EVar (["Basis"], "sql_no_offset"), dummy)
+ofopt : (EVar (["Basis"], "sql_no_offset", Infer), dummy)
| OFFSET sqlint (let
val loc = s (OFFSETleft, sqlintright)
in
- (EApp ((EVar (["Basis"], "sql_offset"), loc), sqlint), loc)
+ (EApp ((EVar (["Basis"], "sql_offset", Infer), loc), sqlint), loc)
end)
sqlint : INT (EPrim (Prim.Int INT), s (INTleft, INTright))
diff --git a/src/urweb.lex b/src/urweb.lex
index a3c34a16..fd8a8077 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -278,6 +278,7 @@ notags = [^<{\n]+;
<INITIAL> "-" => (Tokens.MINUS (pos yypos, pos yypos + size yytext));
<INITIAL> "/" => (Tokens.DIVIDE (yypos, yypos + size yytext));
<INITIAL> "%" => (Tokens.MOD (pos yypos, pos yypos + size yytext));
+<INITIAL> "@" => (Tokens.AT (pos yypos, pos yypos + size yytext));
<INITIAL> "con" => (Tokens.CON (pos yypos, pos yypos + size yytext));
<INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
diff --git a/tests/crud.ur b/tests/crud.ur
index 5427100c..8aff038d 100644
--- a/tests/crud.ur
+++ b/tests/crud.ur
@@ -11,19 +11,19 @@ con colsMeta = fn cols :: {(Type * Type)} => $(Top.mapT2T colMeta cols)
fun default (t ::: Type) (sh : show t) (rd : read t) (inj : sql_injectable t)
name : colMeta (t, string) =
{Nam = name,
- Show = txt _,
+ Show = txt,
Widget = fn nm :: Name => <xml><textbox{nm}/></xml>,
WidgetPopulated = fn (nm :: Name) n =>
- <xml><textbox{nm} value={show _ n}/></xml>,
- Parse = readError _,
+ <xml><textbox{nm} value={show n}/></xml>,
+ Parse = readError,
Inject = _}
-val int = default _ _ _
-val float = default _ _ _
-val string = default _ _ _
+val int = default
+val float = default
+val string = default
fun bool name = {Nam = name,
- Show = txt _,
+ Show = txt,
Widget = fn nm :: Name => <xml><checkbox{nm}/></xml>,
WidgetPopulated = fn (nm :: Name) b =>
<xml><checkbox{nm} checked={b}/></xml>,
@@ -53,11 +53,11 @@ functor Make(M : sig
sql_exp [] [] [] t.1) cols)]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
[[nm] ~ rest] =>
- fn input col acc => acc with nm = sql_inject col.Inject (col.Parse input))
+ fn input col acc => acc with nm = @sql_inject col.Inject (col.Parse input))
{} [M.cols] inputs M.cols
with #Id = (SQL {id})));
return <xml><body>
- Inserted with ID {txt _ id}.
+ Inserted with ID {[id]}.
</body></xml>
fun save (id : int) (inputs : $(mapT2T sndTT M.cols)) =
@@ -70,7 +70,7 @@ functor Make(M : sig
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
[[nm] ~ rest] =>
fn input col acc => acc with nm =
- sql_inject col.Inject (col.Parse input))
+ @sql_inject col.Inject (col.Parse input))
{} [M.cols] inputs M.cols)
tab (WHERE T.Id = {id}));
return <xml><body>
@@ -103,7 +103,7 @@ functor Make(M : sig
</body></xml>
fun confirm (id : int) = return <xml><body>
- <p>Are you sure you want to delete ID #{txt _ id}?</p>
+ <p>Are you sure you want to delete ID #{[id]}?</p>
<p><a link={delete id}>I was born sure!</a></p>
</body></xml>
@@ -112,7 +112,7 @@ functor Make(M : sig
rows <- queryX (SELECT * FROM tab AS T)
(fn (fs : {T : $([Id = int] ++ mapT2T fstTT M.cols)}) => <xml>
<tr>
- <td>{txt _ fs.T.Id}</td>
+ <td>{[fs.T.Id]}</td>
{foldT2RX2 [fstTT] [colMeta] [tr]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
[[nm] ~ rest] v col => <xml>