summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 15:58:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 15:58:25 -0400
commit402112549b47a76033fa575dc9f5e620ea214cc1 (patch)
tree839b907116d5ce5a563835d03ba54eafb9f506fb /src
parent62c0731399525d736de1c4e303c1abd1677a8d0c (diff)
Looking up in a type class from a module
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sml103
-rw-r--r--src/elaborate.sml27
2 files changed, 108 insertions, 22 deletions
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