Mercurial > urweb
changeset 216:38b299373676
Looking up in a type class from a module
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 Aug 2008 15:58:25 -0400 |
| parents | 2f574c07df2e |
| children | 56db662ebcfd |
| files | lib/basis.lig src/elab_env.sml src/elaborate.sml |
| diffstat | 3 files changed, 109 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.lig Sat Aug 16 15:09:53 2008 -0400 +++ b/lib/basis.lig Sat Aug 16 15:58:25 2008 -0400 @@ -26,7 +26,7 @@ -> sql_query (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => [nm] ~ acc => [nm = selected_unselected.1] ++ acc) [] tables) -con sql_type :: Type -> Type +class sql_type val sql_bool : sql_type bool val sql_int : sql_type int val sql_float : sql_type float
--- a/src/elab_env.sml Sat Aug 16 15:09:53 2008 -0400 +++ b/src/elab_env.sml Sat Aug 16 15:58:25 2008 -0400 @@ -31,7 +31,6 @@ structure U = ElabUtil -structure IS = IntBinarySet structure IM = IntBinaryMap structure SM = BinaryMapFn(struct type ord_key = string @@ -96,6 +95,11 @@ ClNamed of int | ClProj of int * string list * string +fun cn2s cn = + case cn of + ClNamed n => "Named(" ^ Int.toString n ^ ")" + | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" + structure CK = struct type ord_key = class_name open Order @@ -118,6 +122,14 @@ | CkRel of int | CkProj of int * string list * string +fun ck2s ck = + case ck of + CkNamed n => "Named(" ^ Int.toString n ^ ")" + | CkRel n => "Rel(" ^ Int.toString n ^ ")" + | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" + +fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" + structure KK = struct type ord_key = class_key open Order @@ -147,6 +159,11 @@ ground = KM.empty } +fun printClasses cs = CM.appi (fn (cn, {ground = km}) => + (print (cn2s cn ^ ":"); + KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km; + print "\n")) cs + type env = { renameC : kind var' SM.map, relC : (string * kind) list, @@ -515,6 +532,20 @@ fun lookupStr (env : env) x = SM.find (#renameStr env, x) +fun sgiSeek (sgi, (sgns, strs, cons)) = + case sgi of + SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) + | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) + | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) + | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) + | SgiVal _ => (sgns, strs, cons) + | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) + | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) + | SgiConstraint _ => (sgns, strs, cons) + | SgiTable _ => (sgns, strs, cons) + | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) + | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) + fun sgnSeek f sgis = let fun seek (sgis, sgns, strs, cons) = @@ -533,18 +564,11 @@ SOME (v, (sgns, strs, cons)) end | NONE => - case sgi of - SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiVal _ => seek (sgis, sgns, strs, cons) - | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) - | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) - | SgiConstraint _ => seek (sgis, sgns, strs, cons) - | SgiTable _ => seek (sgis, sgns, strs, cons) - | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + let + val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons)) + in + seek (sgis, sgns, strs, cons) + end in seek (sgis, IM.empty, IM.empty, IM.empty) end @@ -584,6 +608,18 @@ end) | _ => c +fun sgnS_con' (m1, ms', (sgns, strs, cons)) c = + case c of + CModProj (m1, ms, x) => + (case IM.find (strs, m1) of + NONE => c + | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) + | CNamed n => + (case IM.find (cons, n) of + NONE => c + | SOME nx => CModProj (m1, ms', nx)) + | _ => c + fun sgnS_sgn (str, (sgns, strs, cons)) sgn = case sgn of SgnProj (m1, ms, x) => @@ -664,21 +700,44 @@ case #1 (hnormSgn env sgn) of SgnConst sgis => let - val (classes, _) = - foldl (fn (sgi, (classes, newClasses)) => + val (classes, _, _) = + foldl (fn (sgi, (classes, newClasses, fmap)) => let fun found (x, n) = (CM.insert (classes, ClProj (m1, ms, x), empty_class), - IS.add (newClasses, n)) + IM.insert (newClasses, n, x), + sgiSeek (#1 sgi, fmap)) + + fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap)) in case #1 sgi of SgiClassAbs xn => found xn | SgiClass (x, n, _) => found (x, n) - | _ => (classes, newClasses) + | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) => + (case IM.find (newClasses, f) of + NONE => default () + | SOME fx => + case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of + NONE => default () + | 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)) + } + + in + (CM.insert (classes, cn, class), + newClasses, + fmap) + end) + | _ => default () end) - (classes, IS.empty) sgis + (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis in classes end @@ -803,6 +862,14 @@ SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) else NONE + | SgiClassAbs (x, _) => if x = field then + SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE) + else + NONE + | SgiClass (x, _, c) => if x = field then + SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c) + else + NONE | _ => NONE) sgis of NONE => NONE | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
--- a/src/elaborate.sml Sat Aug 16 15:09:53 2008 -0400 +++ b/src/elaborate.sml Sat Aug 16 15:58:25 2008 -0400 @@ -1373,6 +1373,21 @@ isTotal (combinedCoverage ps, t) end +fun normClassConstraint envs c = + let + val ((c, loc), gs1) = hnormCon envs c + in + case c of + L'.CApp (f, x) => + let + val (f, gs2) = hnormCon envs f + val (x, gs3) = hnormCon envs x + in + ((L'.CApp (f, x), loc), gs1 @ gs2 @ gs3) + end + | _ => ((c, loc), gs1) + end + fun elabExp (env, denv) (eAll as (e, loc)) = let @@ -1430,10 +1445,14 @@ in case t1 of (L'.TFun (dom, ran), _) => - (case E.resolveClass env dom of - NONE => (expError env (Unresolvable (loc, dom)); - (eerror, cerror, [])) - | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3)) + let + val (dom, gs4) = normClassConstraint (env, denv) dom + in + case E.resolveClass env dom of + NONE => (expError env (Unresolvable (loc, dom)); + (eerror, cerror, [])) + | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3 @ gs4) + end | _ => (expError env (OutOfContext loc); (eerror, cerror, [])) end