Mercurial > urweb
changeset 211:e86411f647c6
Initial type class support
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 Aug 2008 14:32:18 -0400 |
| parents | f4033abd6ab1 |
| children | ba4d7c33a45f |
| files | src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/type_class.lac |
| diffstat | 13 files changed, 588 insertions(+), 163 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab.sml Sat Aug 16 14:32:18 2008 -0400 @@ -124,6 +124,8 @@ | SgiSgn of string * int * sgn | SgiConstraint of con * con | SgiTable of int * string * int * con + | SgiClassAbs of string * int + | SgiClass of string * int * con and sgn' = SgnConst of sgn_item list
--- a/src/elab_env.sig Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab_env.sig Sat Aug 16 14:32:18 2008 -0400 @@ -60,6 +60,9 @@ val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option + val pushClass : env -> int -> env + val resolveClass : env -> Elab.con -> Elab.exp option + val pushERel : env -> string -> Elab.con -> env val lookupERel : env -> int -> string * Elab.con
--- a/src/elab_env.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab_env.sml Sat Aug 16 14:32:18 2008 -0400 @@ -31,6 +31,7 @@ structure U = ElabUtil +structure IS = IntBinarySet structure IM = IntBinaryMap structure SM = BinaryMapFn(struct type ord_key = string @@ -61,6 +62,22 @@ val lift = liftConInCon 0 +val liftExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + 1) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + + +val liftExp = liftExpInExp 0 (* Back to environments *) @@ -75,6 +92,61 @@ type datatyp = string list * (string * con option) IM.map +datatype class_name = + ClNamed of int + | ClProj of int * string list * string + +structure CK = struct +type ord_key = class_name +open Order +fun compare x = + case x of + (ClNamed n1, ClNamed n2) => Int.compare (n1, n2) + | (ClNamed _, _) => LESS + | (_, ClNamed _) => GREATER + + | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) => + join (Int.compare (m1, m2), + fn () => join (joinL String.compare (ms1, ms2), + fn () => String.compare (x1, x2))) +end + +structure CM = BinaryMapFn(CK) + +datatype class_key = + CkNamed of int + | CkRel of int + | CkProj of int * string list * string + +structure KK = struct +type ord_key = class_key +open Order +fun compare x = + case x of + (CkNamed n1, CkNamed n2) => Int.compare (n1, n2) + | (CkNamed _, _) => LESS + | (_, CkNamed _) => GREATER + + | (CkRel n1, CkRel n2) => Int.compare (n1, n2) + | (CkRel _, _) => LESS + | (_, CkRel _) => GREATER + + | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) => + join (Int.compare (m1, m2), + fn () => join (joinL String.compare (ms1, ms2), + fn () => String.compare (x1, x2))) +end + +structure KM = BinaryMapFn(KK) + +type class = { + ground : exp KM.map +} + +val empty_class = { + ground = KM.empty +} + type env = { renameC : kind var' SM.map, relC : (string * kind) list, @@ -83,6 +155,8 @@ datatypes : datatyp IM.map, constructors : (datatype_kind * int * string list * con option * int) SM.map, + classes : class CM.map, + renameE : con var' SM.map, relE : (string * con) list, namedE : (string * con) IM.map, @@ -112,6 +186,8 @@ datatypes = IM.empty, constructors = SM.empty, + classes = CM.empty, + renameE = SM.empty, relE = [], namedE = IM.empty, @@ -123,6 +199,12 @@ str = IM.empty } +fun liftClassKey ck = + case ck of + CkNamed _ => ck + | CkRel n => CkRel (n + 1) + | CkProj _ => ck + fun pushCRel (env : env) x k = let val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) @@ -135,6 +217,13 @@ datatypes = #datatypes env, constructors = #constructors env, + classes = CM.map (fn class => { + ground = KM.foldli (fn (ck, e, km) => + KM.insert (km, liftClassKey ck, e)) + KM.empty (#ground class) + }) + (#classes env), + renameE = #renameE env, relE = map (fn (x, c) => (x, lift c)) (#relE env), namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), @@ -159,6 +248,8 @@ datatypes = #datatypes env, constructors = #constructors env, + classes = #classes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -203,6 +294,8 @@ SM.insert (cmap, x, (dk, n', xs, to, n))) (#constructors env) xncs, + classes = #classes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -229,10 +322,77 @@ fun datatypeArgs (xs, _) = xs fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt +fun pushClass (env : env) n = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + datatypes = #datatypes env, + constructors = #constructors env, + + classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}), + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} + +fun class_name_in (c, _) = + case c of + CNamed n => SOME (ClNamed n) + | CModProj x => SOME (ClProj x) + | _ => NONE + +fun class_key_in (c, _) = + case c of + CRel n => SOME (CkRel n) + | CNamed n => SOME (CkNamed n) + | CModProj x => SOME (CkProj x) + | _ => NONE + +fun class_pair_in (c, _) = + case c of + CApp (f, x) => + (case (class_name_in f, class_key_in x) of + (SOME f, SOME x) => SOME (f, x) + | _ => NONE) + | _ => NONE + +fun resolveClass (env : env) c = + case class_pair_in c of + SOME (f, x) => + (case CM.find (#classes env, f) of + NONE => NONE + | SOME class => + case KM.find (#ground class, x) of + NONE => NONE + | SOME e => SOME e) + | _ => NONE + fun pushERel (env : env) x t = let val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) | x => x) (#renameE env) + + val classes = CM.map (fn class => { + ground = KM.map liftExp (#ground class) + }) (#classes env) + val classes = case class_pair_in t of + NONE => classes + | SOME (f, x) => + let + val class = Option.getOpt (CM.find (classes, f), empty_class) + val class = { + ground = KM.insert (#ground class, x, (ERel 0, #2 t)) + } + in + CM.insert (classes, f, class) + end in {renameC = #renameC env, relC = #relC env, @@ -241,6 +401,8 @@ datatypes = #datatypes env, constructors = #constructors env, + classes = classes, + renameE = SM.insert (renameE, x, Rel' (0, t)), relE = (x, t) :: #relE env, namedE = #namedE env, @@ -257,22 +419,39 @@ handle Subscript => raise UnboundRel n fun pushENamedAs (env : env) x n t = - {renameC = #renameC env, - relC = #relC env, - namedC = #namedC env, + let + val classes = #classes env + val classes = case class_pair_in t of + NONE => classes + | SOME (f, x) => + let + val class = Option.getOpt (CM.find (classes, f), empty_class) + val class = { + ground = KM.insert (#ground class, x, (ENamed n, #2 t)) + } + in + CM.insert (classes, f, class) + end + in + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, - datatypes = #datatypes env, - constructors = #constructors env, + datatypes = #datatypes env, + constructors = #constructors env, - renameE = SM.insert (#renameE env, x, Named' (n, t)), - relE = #relE env, - namedE = IM.insert (#namedE env, n, (x, t)), + classes = classes, - renameSgn = #renameSgn env, - sgn = #sgn env, - - renameStr = #renameStr env, - str = #str env} + renameE = SM.insert (#renameE env, x, Named' (n, t)), + relE = #relE env, + namedE = IM.insert (#namedE env, n, (x, t)), + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} + end fun pushENamed env x t = let @@ -301,6 +480,8 @@ datatypes = #datatypes env, constructors = #constructors env, + classes = #classes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -326,32 +507,6 @@ fun lookupSgn (env : env) x = SM.find (#renameSgn env, x) -fun pushStrNamedAs (env : env) x n sgis = - {renameC = #renameC env, - relC = #relC env, - namedC = #namedC env, - - datatypes = #datatypes env, - constructors = #constructors env, - - renameE = #renameE env, - relE = #relE env, - namedE = #namedE env, - - renameSgn = #renameSgn env, - sgn = #sgn env, - - renameStr = SM.insert (#renameStr env, x, (n, sgis)), - str = IM.insert (#str env, n, (x, sgis))} - -fun pushStrNamed env x sgis = - let - val n = !namedCounter - in - namedCounter := n + 1; - (pushStrNamedAs env x n sgis, n) - end - fun lookupStrNamed (env : env) n = case IM.find (#str env, n) of NONE => raise UnboundNamed n @@ -359,57 +514,6 @@ fun lookupStr (env : env) x = SM.find (#renameStr env, x) -fun sgiBinds env (sgi, loc) = - case sgi of - SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE - | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) - | SgiDatatype (x, n, xs, xncs) => - let - val env = pushCNamedAs env x n (KType, loc) NONE - in - foldl (fn ((x', n', to), env) => - let - val t = - case to of - NONE => (CNamed n, loc) - | SOME t => (TFun (t, (CNamed n, loc)), loc) - - val k = (KType, loc) - val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs - in - pushENamedAs env x' n' t - end) - env xncs - end - | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => - let - val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) - in - foldl (fn ((x', n', to), env) => - let - val t = - case to of - NONE => (CNamed n, loc) - | SOME t => (TFun (t, (CNamed n, loc)), loc) - - val k = (KType, loc) - val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs - in - pushENamedAs env x' n' t - end) - env xncs - end - | SgiVal (x, n, t) => pushENamedAs env x n t - | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn - | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn - | SgiConstraint _ => env - - | SgiTable (tn, x, n, c) => - let - val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) - in - pushENamedAs env x n t - end fun sgnSeek f sgis = let @@ -439,6 +543,8 @@ | 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)) in seek (sgis, IM.empty, IM.empty, IM.empty) end @@ -500,17 +606,24 @@ end) | _ => sgn -fun sgnSubCon x = - ElabUtil.Con.map {kind = id, - con = sgnS_con x} - fun sgnSubSgn x = ElabUtil.Sgn.map {kind = id, con = sgnS_con x, sgn_item = id, sgn = sgnS_sgn x} -fun hnormSgn env (all as (sgn, loc)) = + + +and projectSgn env {sgn, str, field} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => + (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of + NONE => NONE + | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) + | SgnError => SOME (SgnError, ErrorMsg.dummySpan) + | _ => NONE + +and hnormSgn env (all as (sgn, loc)) = case sgn of SgnError => all | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) @@ -547,14 +660,117 @@ end | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" -and projectSgn env {sgn, str, field} = +fun enrichClasses env classes (m1, ms) sgn = case #1 (hnormSgn env sgn) of SgnConst sgis => - (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of - NONE => NONE - | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) - | SgnError => SOME (SgnError, ErrorMsg.dummySpan) - | _ => NONE + let + val (classes, _) = + foldl (fn (sgi, (classes, newClasses)) => + let + fun found (x, n) = + (CM.insert (classes, + ClProj (m1, ms, x), + empty_class), + IS.add (newClasses, n)) + in + case #1 sgi of + SgiClassAbs xn => found xn + | SgiClass (x, n, _) => found (x, n) + | _ => (classes, newClasses) + end) + (classes, IS.empty) sgis + in + classes + end + | _ => classes + +fun pushStrNamedAs (env : env) x n sgn = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + datatypes = #datatypes env, + constructors = #constructors env, + + classes = enrichClasses env (#classes env) (n, []) sgn, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = SM.insert (#renameStr env, x, (n, sgn)), + str = IM.insert (#str env, n, (x, sgn))} + +fun pushStrNamed env x sgn = + let + val n = !namedCounter + in + namedCounter := n + 1; + (pushStrNamedAs env x n sgn, n) + end + +fun sgiBinds env (sgi, loc) = + case sgi of + SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE + | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) + | SgiDatatype (x, n, xs, xncs) => + let + val env = pushCNamedAs env x n (KType, loc) NONE + in + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) + env xncs + end + | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => + let + val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) + in + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) + env xncs + end + | SgiVal (x, n, t) => pushENamedAs env x n t + | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn + | SgiConstraint _ => env + + | SgiTable (tn, x, n, c) => + let + val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end + + | 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) + + +fun sgnSubCon x = + ElabUtil.Con.map {kind = id, + con = sgnS_con x} fun projectStr env {sgn, str, field} = case #1 (hnormSgn env sgn) of @@ -675,6 +891,8 @@ | 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) | SgiTable _ => seek (sgis, sgns, strs, 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) in seek (sgis, IM.empty, IM.empty, IM.empty, []) end
--- a/src/elab_print.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab_print.sml Sat Aug 16 14:32:18 2008 -0400 @@ -464,6 +464,16 @@ string ":", space, p_con env c] + | SgiClassAbs (x, n) => box [string "class", + space, + p_named x n] + | SgiClass (x, n, c) => box [string "class", + space, + p_named x n, + space, + string "=", + space, + p_con env c] and p_sgn env (sgn, _) = case sgn of
--- a/src/elab_util.sig Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab_util.sig Sat Aug 16 14:32:18 2008 -0400 @@ -75,6 +75,11 @@ con : (Elab.con', 'state, 'abort) Search.mapfolder, exp : (Elab.exp', 'state, 'abort) Search.mapfolder} -> (Elab.exp, 'state, 'abort) Search.mapfolder + val mapB : {kind : Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + exp : 'context -> Elab.exp' -> Elab.exp', + bind : 'context * binder -> 'context} + -> 'context -> (Elab.exp -> Elab.exp) val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool, exp : Elab.exp' -> bool} -> Elab.exp -> bool
--- a/src/elab_util.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elab_util.sml Sat Aug 16 14:32:18 2008 -0400 @@ -376,6 +376,14 @@ S.Return _ => true | S.Continue _ => false +fun mapB {kind, con, exp, bind} ctx e = + case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), + exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), + bind = bind} ctx e () of + S.Continue (e, ()) => e + | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" + end structure Sgn = struct @@ -455,6 +463,11 @@ S.map2 (con ctx c, fn c' => (SgiTable (tn, x, n, c'), loc)) + | SgiClassAbs _ => S.return2 siAll + | SgiClass (x, n, c) => + S.map2 (con ctx c, + fn c' => + (SgiClass (x, n, c'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -478,7 +491,11 @@ | SgiSgn (x, _, sgn) => bind (ctx, Sgn (x, sgn)) | SgiConstraint _ => ctx - | SgiTable _ => ctx, + | SgiTable _ => ctx + | SgiClassAbs (x, _) => + bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) + | SgiClass (x, _, _) => + bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))), sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc))
--- a/src/elaborate.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/elaborate.sml Sat Aug 16 14:32:18 2008 -0400 @@ -985,7 +985,8 @@ | PatHasNoArg of ErrorMsg.span | Inexhaustive of ErrorMsg.span | DuplicatePatField of ErrorMsg.span * string - | SqlInfer of ErrorMsg.span * L'.con + | Unresolvable of ErrorMsg.span * L'.con + | OutOfContext of ErrorMsg.span fun expError env err = case err of @@ -1028,9 +1029,11 @@ ErrorMsg.errorAt loc "Inexhaustive 'case'" | DuplicatePatField (loc, s) => ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern") - | SqlInfer (loc, c) => - (ErrorMsg.errorAt loc "Can't infer SQL-ness of type"; - eprefaces' [("Type", p_con env c)]) + | OutOfContext loc => + ErrorMsg.errorAt loc "Type class wildcard occurs out of context" + | Unresolvable (loc, c) => + (ErrorMsg.errorAt loc "Can't resolve type class instance"; + eprefaces' [("Class constraint", p_con env c)]) fun checkCon (env, denv) e c1 c2 = unifyCons (env, denv) c1 c2 @@ -1419,50 +1422,23 @@ ((L'.EModProj (n, ms, s), loc), t, []) end) - | L.EApp (e1, (L.ESqlInfer, _)) => + | L.EApp (e1, (L.EWild, _)) => let val (e1', t1, gs1) = elabExp (env, denv) e1 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 val (t1, gs3) = hnormCon (env, denv) t1 in case t1 of - (L'.TFun ((L'.CApp ((L'.CModProj (basis, [], "sql_type"), _), - t), _), ran), _) => - if basis <> !basis_r then - raise Fail "Bad use of ESqlInfer [1]" - else - let - val (t, gs4) = hnormCon (env, denv) t - - fun error () = expError env (SqlInfer (loc, t)) - in - case t of - (L'.CModProj (basis, [], x), _) => - (if basis <> !basis_r then - error () - else - case x of - "bool" => () - | "int" => () - | "float" => () - | "string" => () - | _ => error (); - ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_" ^ x), loc)), loc), - ran, gs1 @ gs2 @ gs3 @ gs4)) - | (L'.CUnif (_, (L'.KType, _), _, r), _) => - let - val t = (L'.CModProj (basis, [], "int"), loc) - in - r := SOME t; - ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_int"), loc)), loc), - ran, gs1 @ gs2 @ gs3 @ gs4) - end - | _ => (error (); - (eerror, cerror, [])) - end - | _ => raise Fail "Bad use of ESqlInfer [2]" + (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)) + | _ => (expError env (OutOfContext loc); + (eerror, cerror, [])) end - | L.ESqlInfer => raise Fail "Bad use of ESqlInfer [3]" + | L.EWild => (expError env (OutOfContext loc); + (eerror, cerror, [])) | L.EApp (e1, e2) => let @@ -1961,6 +1937,26 @@ ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs)) end + | L.SgiClassAbs x => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val (env, n) = E.pushCNamed env x k NONE + val env = E.pushClass env n + in + ([(L'.SgiClassAbs (x, n), loc)], (env, denv, [])) + end + + | L.SgiClass (x, c) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val (c', ck, gs) = elabCon (env, denv) c + val (env, n) = E.pushCNamed env x k (SOME c') + val env = E.pushClass env n + in + checkKind env c' ck k; + ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) + end + and elabSgn (env, denv) (sgn, loc) = case sgn of L.SgnConst sgis => @@ -2027,7 +2023,19 @@ sgnError env (DuplicateVal (loc, x)) else (); - (cons, SS.add (vals, x), sgns, strs))) + (cons, SS.add (vals, x), sgns, strs)) + | L'.SgiClassAbs (x, _) => + (if SS.member (cons, x) then + sgnError env (DuplicateCon (loc, x)) + else + (); + (SS.add (cons, x), vals, sgns, strs)) + | L'.SgiClass (x, _, _) => + (if SS.member (cons, x) then + sgnError env (DuplicateCon (loc, x)) + else + (); + (SS.add (cons, x), vals, sgns, strs))) (SS.empty, SS.empty, SS.empty, SS.empty) sgis' in ((L'.SgnConst sgis', loc), gs) @@ -2160,6 +2168,20 @@ | L'.SgiTable (_, x, n, c) => (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc), (L'.EModProj (str, strs, x), loc)), loc) + | L'.SgiClassAbs (x, n) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val c = (L'.CModProj (str, strs, x), loc) + in + (L'.DCon (x, n, k, c), loc) + end + | L'.SgiClass (x, n, _) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val c = (L'.CModProj (str, strs, x), loc) + in + (L'.DCon (x, n, k, c), loc) + end in (d, (E.declBinds env' d, denv')) end) @@ -2283,27 +2305,41 @@ in found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) end + | L'.SgiClassAbs (x', n1) => found (x', n1, + (L'.KArrow ((L'.KType, loc), + (L'.KType, loc)), loc), + NONE) + | L'.SgiClass (x', n1, c) => found (x', n1, + (L'.KArrow ((L'.KType, loc), + (L'.KType, loc)), loc), + SOME c) | _ => NONE end) | L'.SgiCon (x, n2, k2, c2) => seek (fn sgi1All as (sgi1, _) => - case sgi1 of - L'.SgiCon (x', n1, k1, c1) => - if x = x' then - let - fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv) - in - (case unifyCons (env, denv) c1 c2 of - [] => good () - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - good ()) - end - else - NONE - | _ => NONE) + let + fun found (x', n1, k1, c1) = + if x = x' then + let + fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv) + in + (case unifyCons (env, denv) c1 c2 of + [] => good () + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + good ()) + end + else + NONE + in + case sgi1 of + L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) + | L'.SgiClass (x', n1, c1) => + found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1) + | _ => NONE + end) | L'.SgiDatatype (x, n2, xs2, xncs2) => seek (fn sgi1All as (sgi1, _) => @@ -2491,6 +2527,54 @@ else NONE | _ => NONE) + + | L'.SgiClassAbs (x, n2) => + seek (fn sgi1All as (sgi1, _) => + let + fun found (x', n1, co) = + if x = x' then + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val env = E.pushCNamedAs env x n1 k co + in + SOME (if n1 = n2 then + env + else + E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)), + denv) + end + else + NONE + in + case sgi1 of + L'.SgiClassAbs (x', n1) => found (x', n1, NONE) + | L'.SgiClass (x', n1, c) => found (x', n1, SOME c) + | _ => NONE + end) + | L'.SgiClass (x, n2, c2) => + seek (fn sgi1All as (sgi1, _) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + + fun found (x', n1, c1) = + if x = x' then + let + fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv) + in + (case unifyCons (env, denv) c1 c2 of + [] => good () + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + good ()) + end + else + NONE + in + case sgi1 of + L'.SgiClass (x', n1, c1) => found (x', n1, c1) + | _ => NONE + end) end in ignore (foldl folder (env, denv) sgis2) @@ -2849,6 +2933,17 @@ ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs)) end + | L.DClass (x, c) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + val (c', ck, gs) = elabCon (env, denv) c + val (env, n) = E.pushCNamed env x k (SOME c') + val env = E.pushClass env n + in + checkKind env c' ck k; + ([(L'.DCon (x, n, k, c'), loc)], (env, denv, [])) + end + and elabStr (env, denv) (str, loc) = case str of L.StrConst ds => @@ -2949,6 +3044,30 @@ (SS.add (vals, x), x) in ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiClassAbs (x, n) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + + val (cons, x) = + if SS.member (cons, x) then + (cons, "?" ^ x) + else + (SS.add (cons, x), x) + in + ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiClass (x, n, c) => + let + val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) + + val (cons, x) = + if SS.member (cons, x) then + (cons, "?" ^ x) + else + (SS.add (cons, x), x) + in + ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) end) ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
--- a/src/explify.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/explify.sml Sat Aug 16 14:32:18 2008 -0400 @@ -128,6 +128,9 @@ | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) | L.SgiConstraint _ => NONE | L.SgiTable _ => raise Fail "Explify SgiTable" + | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc) + | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), + explifyCon c), loc) and explifySgn (sgn, loc) = case sgn of
--- a/src/lacweb.grm Sat Aug 16 12:35:46 2008 -0400 +++ b/src/lacweb.grm Sat Aug 16 14:32:18 2008 -0400 @@ -89,7 +89,7 @@ | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR | DIVIDE | GT | DOTDOTDOT - | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT + | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT | CLASS | DATATYPE | OF | TYPE | NAME | ARROW | LARROW | DARROW | STAR @@ -241,6 +241,14 @@ | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) | EXPORT spath (DExport spath, s (EXPORTleft, spathright)) | TABLE SYMBOL COLON cexp (DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright)) + | CLASS SYMBOL EQ cexp (DClass (SYMBOL, cexp), s (CLASSleft, cexpright)) + | CLASS SYMBOL SYMBOL EQ cexp (let + val loc = s (CLASSleft, cexpright) + val k = (KType, loc) + val c = (CAbs (SYMBOL2, SOME k, cexp), loc) + in + (DClass (SYMBOL1, c), s (CLASSleft, cexpright)) + end) dargs : ([]) | SYMBOL dargs (SYMBOL :: dargs) @@ -299,6 +307,15 @@ | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) | TABLE SYMBOL COLON cexp (SgiTable (SYMBOL, entable cexp), s (TABLEleft, cexpright)) + | CLASS SYMBOL (SgiClassAbs SYMBOL, s (CLASSleft, SYMBOLright)) + | CLASS SYMBOL EQ cexp (SgiClass (SYMBOL, cexp), s (CLASSleft, cexpright)) + | CLASS SYMBOL SYMBOL EQ cexp (let + val loc = s (CLASSleft, cexpright) + val k = (KType, loc) + val c = (CAbs (SYMBOL2, SOME k, cexp), loc) + in + (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright)) + end) sgis : ([]) | sgi sgis (sgi :: sgis) @@ -459,6 +476,7 @@ (EPrim (Prim.String ""), s (XML_BEGINleft, XML_ENDright))), s (XML_BEGINleft, XML_ENDright)) | LPAREN query RPAREN (query) + | UNDER (EWild, s (UNDERleft, UNDERright)) idents : ident ([ident]) | ident DOT idents (ident :: idents) @@ -633,7 +651,7 @@ s (FALSEleft, FALSEright))) | LBRACE eexp RBRACE (sql_inject (#1 eexp, - ESqlInfer, + EWild, s (LBRACEleft, RBRACEright))) wopt : (sql_inject (EVar (["Basis"], "True"),
--- a/src/lacweb.lex Sat Aug 16 12:35:46 2008 -0400 +++ b/src/lacweb.lex Sat Aug 16 14:32:18 2008 -0400 @@ -280,6 +280,7 @@ <INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext)); <INITIAL> "export" => (Tokens.EXPORT (pos yypos, pos yypos + size yytext)); <INITIAL> "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); +<INITIAL> "class" => (Tokens.CLASS (pos yypos, pos yypos + size yytext)); <INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); <INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
--- a/src/source.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/source.sml Sat Aug 16 14:32:18 2008 -0400 @@ -83,6 +83,8 @@ | SgiInclude of sgn | SgiConstraint of con * con | SgiTable of string * con + | SgiClassAbs of string + | SgiClass of string * con and sgn' = SgnConst of sgn_item list @@ -119,7 +121,7 @@ | ECut of exp * con | EFold - | ESqlInfer + | EWild | ECase of exp * (pat * exp) list @@ -139,6 +141,7 @@ | DOpenConstraints of string * string list | DExport of str | DTable of string * con + | DClass of string * con and str' = StrConst of decl list
--- a/src/source_print.sml Sat Aug 16 12:35:46 2008 -0400 +++ b/src/source_print.sml Sat Aug 16 14:32:18 2008 -0400 @@ -379,6 +379,16 @@ string ":", space, p_con c] + | SgiClassAbs x => box [string "class", + space, + string x] + | SgiClass (x, c) => box [string "class", + space, + string x, + space, + string "=", + space, + p_con c] and p_sgn (sgn, _) = case sgn of @@ -531,6 +541,13 @@ string ":", space, p_con c] + | DClass (x, c) => box [string "class", + space, + string x, + space, + string "=", + space, + p_con c] and p_str (str, _) = case str of
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/type_class.lac Sat Aug 16 14:32:18 2008 -0400 @@ -0,0 +1,9 @@ +class default t = t + +val string_default : default string = "" +val int_default : default int = 0 + +val default : t :: Type -> default t -> t = + fn t :: Type => fn d : default t => d +val empty = default [string] _ +val zero = default [int] _