Ur/Web: src/elaborate.sml comparison

comparison src/elaborate.sml @ 228:19e5791923d0

Resolving lingering type class constraints

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 21 Aug 2008 14:45:31 -0400
parents	bbe5899a9585
children	c466678af854

comparison

equal deleted inserted replaced

-:524e10c91478
+:19e5791923d0
 (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
 val u = cunif (loc, k)
 val (e, t, gs') = unravel (subConInCon (0, u) t',
 (L'.ECApp (e, u), loc))
 in
-(e, t, gs @ gs')
+(e, t, enD gs @ gs')
 end
-| _ => (e, t, gs)
+| _ => (e, t, enD gs)
 end
 in
 unravel (t, e)
 end
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val (t', _, gs2) = elabCon (env, denv) t
 val gs3 = checkCon (env, denv) e' et t'
 in
-(e', t', gs1 @ gs2 @ gs3)
+(e', t', gs1 @ enD gs2 @ enD gs3)
 end
 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
 | L.EVar ([], s) =>
 (case E.lookupE env s of
 (L'.TFun (dom, ran), _) =>
 let
 val (dom, gs4) = normClassConstraint (env, denv) dom
 in
 case E.resolveClass env dom of
-NONE => (expError env (Unresolvable (loc, dom));
+NONE =>
-(eerror, cerror, []))
+let
-| SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3 @ gs4)
+val r = ref NONE
+in
+((L'.EUnif r, loc), ran, [TypeClass (env, dom, r, loc)])
+end
+| SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ enD gs3 @ enD gs4)
 end
 | _ => (expError env (OutOfContext (loc, SOME (e1', t1)));
 (eerror, cerror, []))
 end
 | L.EWild => (expError env (OutOfContext (loc, NONE));
 val t = (L'.TFun (dom, ran), dummy)
 val gs4 = checkCon (env, denv) e1' t1 t
 val gs5 = checkCon (env, denv) e2' t2 dom
-val gs = gs1 @ gs2 @ gs3 @ gs4 @ gs5
+val gs = gs1 @ gs2 @ gs3 @ enD gs4 @ enD gs5
 in
 ((L'.EApp (e1', e2'), loc), ran, gs)
 end
 | L.EAbs (x, to, e) =>
 let
 end
 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
 in
 ((L'.EAbs (x, t', et, e'), loc),
 (L'.TFun (t', et), loc),
-gs1 @ gs2)
+enD gs1 @ gs2)
 end
 | L.ECApp (e, c) =>
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val (e', et, gs2) = elabHead (env, denv) e' et
 val () = checkKind env c' ck k
 val eb' = subConInCon (0, c') eb
 handle SynUnif => (expError env (Unif ("substitution", eb));
 cerror)
 in
-((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
+((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
 end
 | L'.CUnif _ =>
 (expError env (Unif ("application", et));
 (eerror, cerror, []))
 val (e', t, gs4) = elabExp (env, denv') e
 in
 checkKind env c1' k1 (L'.KRecord ku1, loc);
 checkKind env c2' k2 (L'.KRecord ku2, loc);
-(e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
+(e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
 end
 | L.ERecord xes =>
 let
 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
 let
 val (x', xk, gs1) = elabCon (env, denv) x
 val (e', et, gs2) = elabExp (env, denv) e
 in
 checkKind env x' xk kname;
-((x', e', et), gs1 @ gs2 @ gs)
+((x', e', et), enD gs1 @ gs2 @ gs)
 end)
 [] xes
 val k = (L'.KType, loc)
 end)
 gs rest
 in
 prove (rest, gs)
 end
+val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
+val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
 in
 ((L'.ERecord xes', loc),
 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
-prove (xes', gs))
+enD (prove (xes', gsD)) @ gsO)
 end
 | L.EField (e, c) =>
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val gs3 =
 checkCon (env, denv) e' et
 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
 val gs4 = D.prove env denv (first, rest, loc)
 in
-((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
+((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4)
 end
 | L.ECut (e, c) =>
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val gs3 =
 checkCon (env, denv) e' et
 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
 val gs4 = D.prove env denv (first, rest, loc)
 in
-((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
+((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
+gs1 @ enD gs2 @ enD gs3 @ enD gs4)
 end
 | L.EFold =>
 let
 val dom = kunif loc
 val gs1 = checkPatCon (env, denv) p' pt et
 val (e', et, gs2) = elabExp (env, denv) e
 val gs3 = checkCon (env, denv) e' et result
 in
-((p', e'), gs1 @ gs2 @ gs3 @ gs)
+((p', e'), enD gs1 @ gs2 @ enD gs3 @ gs)
 end)
 gs1 pes
 val (total, gs') = exhaustive (env, denv, et, map #1 pes')
 in
 if total then
 ()
 else
 expError env (Inexhaustive loc);
-((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
+((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
 end
 end
 datatype decl_error =
 end
 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
-fun elabDecl ((d, loc), (env, denv, gs)) =
+fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
 case d of
 L.DCon (x, ko, c) =>
 let
 val k' = case ko of
 NONE => kunif loc
 val (c', ck, gs') = elabCon (env, denv) c
 val (env', n) = E.pushCNamed env x k' (SOME c')
 in
 checkKind env c' ck k';
-([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
+([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
 end
 | L.DDatatype (x, xs, xcs) =>
 let
 val k = (L'.KType, loc)
 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
 | SOME t' =>
 let
 val (t', tk, gs') = elabCon (env', denv') t'
 in
 checkKind env' t' tk k;
-(SOME t', (L'.TFun (t', t), loc), gs' @ gs)
+(SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
 end
 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
 val (env, n') = E.pushENamed env x t
 in
 (strerror, sgnerror))
 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
 ((L'.StrVar n, loc), sgn) ms
 in
 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
-((L'.CModProj (n, ms, s), _), gs) =>
+((L'.CModProj (n, ms, s), _), gs') =>
 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
 NONE => (conError env (UnboundDatatype (loc, s));
 ([], (env, denv, gs)))
 | SOME (xs, xncs) =>
 let
 t xs
 in
 E.pushENamedAs env x n t
 end) env xncs
 in
-([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
+([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
 end)
 | _ => (strError env (NotDatatype loc);
 ([], (env, denv, [])))
 end)
 val (c', gs4) = normClassConstraint (env, denv) c'
 val (env', n) = E.pushENamed env x c'
 in
 (*prefaces "DVal" [("x", Print.PD.string x),
 ("c'", p_con env c')];*)
-([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
+([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
 end
 | L.DValRec vis =>
 let
 val (vis, gs) = ListUtil.foldlMap
 (fn ((x, co, e), gs) =>
 let
 val (c', _, gs1) = case co of
 NONE => (cunif (loc, ktype), ktype, [])
 | SOME c => elabCon (env, denv) c
 in
-((x, c', e), gs1 @ gs)
+((x, c', e), enD gs1 @ gs)
 end) [] vis
 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
 let
 val (env, n) = E.pushENamed env x c'
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val gs2 = checkCon (env, denv) e' et c'
 in
-((x, n, c', e'), gs1 @ gs2 @ gs)
+((x, n, c', e'), gs1 @ enD gs2 @ gs)
 end) gs vis
 in
 ([(L'.DValRec vis, loc)], (env, denv, gs))
 end
 | L.DSgn (x, sgn) =>
 let
 val (sgn', gs') = elabSgn (env, denv) sgn
 val (env', n) = E.pushSgnNamed env x sgn'
 in
-([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
 end
 | L.DStr (x, sgno, str) =>
 let
 val () = if x = "Basis" then
 | _ => str
 val (str', actual, gs2) = elabStr (env, denv) str
 in
 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
-(str', formal, gs1 @ gs2)
+(str', formal, enD gs1 @ gs2)
 end
 val (env', n) = E.pushStrNamed env x sgn'
 in
 case #1 (hnormSgn env sgn') of
 let
 val (sgn', gs') = elabSgn (env, denv) sgn
 val (env', n) = E.pushStrNamed env x sgn'
 in
-([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
+([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
 end
 | L.DOpen (m, ms) =>
 (case E.lookupStr env m of
 NONE => (strError env (UnboundStr (loc, m));
 val (denv', gs4) = D.assert env denv (c1', c2')
 in
 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
-([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4 @ gs))
+([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
 end
 | L.DOpenConstraints (m, ms) =>
 let
 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
 let
 val (c', k, gs') = elabCon (env, denv) c
 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
 in
 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
-([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs))
+([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
 end
 | L.DClass (x, c) =>
 let
 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
 (ran', gs)
 end
 in
 ((L'.StrFun (m, n, dom', formal, str'), loc),
 (L'.SgnFun (m, n, dom', formal), loc),
-gs1 @ gs2 @ gs3)
+enD gs1 @ gs2 @ enD gs3)
 end
 | L.StrApp (str1, str2) =>
 let
 val (str1', sgn1, gs1) = elabStr (env, denv) str1
 val (str2', sgn2, gs2) = elabStr (env, denv) str2
 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
 in
 if ErrorMsg.anyErrors () then
 ()
 else
-app (fn (loc, env, denv, c1, c2) =>
+app (fn Disjoint (loc, env, denv, c1, c2) =>
-case D.prove env denv (c1, c2, loc) of
+(case D.prove env denv (c1, c2, loc) of
 [] => ()
 | _ =>
 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
 eprefaces' [("Con 1", p_con env c1),
 ("Con 2", p_con env c2),
 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
-("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
+("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
+| TypeClass (env, c, r, loc) =>
+case E.resolveClass env c of
+SOME e => r := SOME e
+| NONE => expError env (Unresolvable (loc, c))) gs;
 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
 end
 end

Mercurial > urweb

comparison src/elaborate.sml @ 228:19e5791923d0