diff options
| -rw-r--r-- | demo/listShop.ur | 8 | ||||
| -rw-r--r-- | demo/prose | 4 | ||||
| -rw-r--r-- | lib/basis.urs | 2 | ||||
| -rw-r--r-- | lib/top.ur | 2 | ||||
| -rw-r--r-- | src/compiler.sml | 4 | ||||
| -rw-r--r-- | src/elab_env.sig | 1 | ||||
| -rw-r--r-- | src/elab_env.sml | 65 | ||||
| -rw-r--r-- | src/elaborate.sml | 2068 | ||||
| -rw-r--r-- | src/monoize.sml | 2 | ||||
| -rw-r--r-- | src/source.sml | 7 | ||||
| -rw-r--r-- | src/source_print.sml | 2 | ||||
| -rw-r--r-- | src/urweb.grm | 155 | ||||
| -rw-r--r-- | src/urweb.lex | 1 | ||||
| -rw-r--r-- | tests/crud.ur | 24 |
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) @@ -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] @@ -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> |