diff options
author | 2008-08-16 15:58:25 -0400 | |
---|---|---|
committer | 2008-08-16 15:58:25 -0400 | |
commit | 402112549b47a76033fa575dc9f5e620ea214cc1 (patch) | |
tree | 839b907116d5ce5a563835d03ba54eafb9f506fb | |
parent | 62c0731399525d736de1c4e303c1abd1677a8d0c (diff) |
Looking up in a type class from a module
-rw-r--r-- | lib/basis.lig | 2 | ||||
-rw-r--r-- | src/elab_env.sml | 103 | ||||
-rw-r--r-- | src/elaborate.sml | 27 |
3 files changed, 109 insertions, 23 deletions
diff --git a/lib/basis.lig b/lib/basis.lig index 6fe847b9..01b3fab8 100644 --- a/lib/basis.lig +++ b/lib/basis.lig @@ -26,7 +26,7 @@ val sql_query : tables :: {({Type} * {Type})} -> 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 diff --git a/src/elab_env.sml b/src/elab_env.sml index b9ab587e..1b25749f 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -31,7 +31,6 @@ open Elab structure U = ElabUtil -structure IS = IntBinarySet structure IM = IntBinaryMap structure SM = BinaryMapFn(struct type ord_key = string @@ -96,6 +95,11 @@ datatype class_name = 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 @@ datatype class_key = | 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 @@ val empty_class = { 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 lookupStrNamed (env : env) n = 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 @@ fun sgnSeek f sgis = 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 @@ fun sgnS_con (str, (sgns, strs, cons)) c = 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 @@ fun enrichClasses env classes (m1, ms) sgn = 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 @@ fun projectCon env {sgn, str, field} = 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)) diff --git a/src/elaborate.sml b/src/elaborate.sml index 49498570..2046432b 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1373,6 +1373,21 @@ fun exhaustive (env, denv, t, ps) = 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 @@ fun elabExp (env, denv) (eAll as (e, loc)) = 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 |