diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-12-19 10:03:31 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-12-19 10:03:31 -0500 |
| commit | ba83ee9a9b3d2539b820c9fcb1cb7cd42226da6c (patch) | |
| tree | 147dbc155a38e55b93e8c303304bdc6c9f5e8258 /src/elab_env.sml | |
| parent | 8d98194908d9001ce5da0bceda10c22e71e940ba (diff) | |
Initial conversion to arbitrary-kind classes
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index d1084d0c..53c934dd 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -604,8 +604,8 @@ fun sgiSeek (sgi, (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) - | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) - | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) + | 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 @@ -788,8 +788,8 @@ fun enrichClasses env classes (m1, ms) sgn = fmap, pushSgnNamedAs env x n sgn) - | SgiClassAbs xn => found xn - | SgiClass (x, n, _) => found (x, n) + | SgiClassAbs (x, n, _) => found (x, n) + | SgiClass (x, n, _, _) => found (x, n) | SgiVal (x, n, (CApp (f, a), _)) => let fun unravel c = @@ -946,8 +946,8 @@ fun sgiBinds env (sgi, loc) = | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env - | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE - | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) + | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE + | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c) fun sgnSubCon x = ElabUtil.Con.map {kind = id, @@ -998,14 +998,14 @@ fun projectCon env {sgn, str, field} = end 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 + | SgiClassAbs (x, _, k) => if x = field then + SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE) + else + NONE + | SgiClass (x, _, k, c) => if x = field then + SOME ((KArrow (k, (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)) @@ -1101,8 +1101,8 @@ fun sgnSeekConstraints (str, sgis) = | SgiVal _ => seek (sgis, sgns, strs, cons, acc) | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) - | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) - | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) in seek (sgis, IM.empty, IM.empty, IM.empty, []) end @@ -1189,9 +1189,9 @@ fun declBinds env (d, loc) = in pushENamedAs env x n t end - | DClass (x, n, c) => + | DClass (x, n, k, c) => let - val k = (KArrow ((KType, loc), (KType, loc)), loc) + val k = (KArrow (k, (KType, loc)), loc) val env = pushCNamedAs env x n k (SOME c) in pushClass env n |