summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 16:41:11 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 16:41:11 -0400
commit1a5acb4732536e4be288895eb89d139b19aebc94 (patch)
treee4856ac916556022e401a21e2ff722af1b472aa1 /src/elaborate.sml
parenta3418cf924752accf2f68fc2673da2a661276ae5 (diff)
New implicit argument handling
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml2068
1 files changed, 1039 insertions, 1029 deletions
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
| _ =>
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 16:13:19 +0000