diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 15:49:30 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 15:49:30 -0400 |
commit | a579d98b69649309caaf6315910813aba36fe905 (patch) | |
tree | 115627f9af3bafbad40cf823df9f1db5c8e270e2 /src | |
parent | 92af3391b64df0a2082006c39ed1335dd1bf7256 (diff) |
Basic datatype importing works
Diffstat (limited to 'src')
-rw-r--r-- | src/elab_env.sig | 8 | ||||
-rw-r--r-- | src/elab_env.sml | 118 | ||||
-rw-r--r-- | src/elaborate.sml | 76 | ||||
-rw-r--r-- | src/lacweb.grm | 6 |
4 files changed, 184 insertions, 24 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig index 83490b69..4bc480cc 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -51,6 +51,12 @@ signature ELAB_ENV = sig val lookupC : env -> string -> Elab.kind var + val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env + type datatyp + val lookupDatatype : env -> int -> datatyp + val lookupConstructor : datatyp -> int -> string * Elab.con option + val constructors : datatyp -> (string * int * Elab.con option) list + val pushERel : env -> string -> Elab.con -> env val lookupERel : env -> int -> string * Elab.con @@ -78,6 +84,8 @@ signature ELAB_ENV = sig val hnormSgn : env -> Elab.sgn -> Elab.sgn val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option + val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } + -> (string * int * Elab.con option) list option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option diff --git a/src/elab_env.sml b/src/elab_env.sml index 9f4916e3..fc6560e7 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -73,11 +73,15 @@ datatype 'a var = | Rel of int * 'a | Named of int * 'a +type datatyp = (string * con option) IM.map + type env = { renameC : kind var' SM.map, relC : (string * kind) list, namedC : (string * kind * con option) IM.map, + datatypes : datatyp IM.map, + renameE : con var' SM.map, relE : (string * con) list, namedE : (string * con) IM.map, @@ -104,6 +108,8 @@ val empty = { relC = [], namedC = IM.empty, + datatypes = IM.empty, + renameE = SM.empty, relE = [], namedE = IM.empty, @@ -124,6 +130,8 @@ fun pushCRel (env : env) x k = relC = (x, k) :: #relC env, namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), + datatypes = #datatypes 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), @@ -145,6 +153,8 @@ fun pushCNamedAs (env : env) x n k co = relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), + datatypes = #datatypes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -174,6 +184,37 @@ fun lookupC (env : env) x = | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x +fun pushDatatype (env : env) n xncs = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + datatypes = IM.insert (#datatypes env, n, + foldl (fn ((x, n, to), cons) => + IM.insert (cons, n, (x, to))) IM.empty xncs), + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} + +fun lookupDatatype (env : env) n = + case IM.find (#datatypes env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun lookupConstructor dt n = + case IM.find (dt, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt + fun pushERel (env : env) x t = let val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) @@ -183,6 +224,8 @@ fun pushERel (env : env) x t = relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = SM.insert (renameE, x, Rel' (0, t)), relE = (x, t) :: #relE env, namedE = #namedE env, @@ -203,6 +246,8 @@ fun pushENamedAs (env : env) x n t = relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = SM.insert (#renameE env, x, Named' (n, t)), relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t)), @@ -237,6 +282,8 @@ fun pushSgnNamedAs (env : env) x n sgis = relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -267,6 +314,8 @@ fun pushStrNamedAs (env : env) x n sgis = relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -292,26 +341,6 @@ fun lookupStrNamed (env : env) n = fun lookupStr (env : env) x = SM.find (#renameStr env, x) -fun declBinds env (d, loc) = - case d of - DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) - | DDatatype (x, n, xncs) => - let - val env = pushCNamedAs env x n (KType, loc) NONE - in - foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) - | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) - env xncs - end - | DDatatypeImp (x, n, m, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m, ms, x'), loc)) - | DVal (x, n, t, _) => pushENamedAs env x n t - | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis - | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn - | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn - | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn - | DConstraint _ => env - | DExport _ => env - fun sgiBinds env (sgi, loc) = case sgi of SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE @@ -479,12 +508,22 @@ fun projectCon env {sgn, str, field} = SgnConst sgis => (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE + | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE | _ => NONE) sgis of NONE => NONE | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) | _ => NONE +fun projectDatatype env {sgn, str, field} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => + (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE + | _ => NONE) sgis of + NONE => NONE + | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) + | _ => NONE + fun projectVal env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => @@ -524,4 +563,43 @@ fun projectConstraints env {sgn, str} = | SgnError => SOME [] | _ => NONE +fun declBinds env (d, loc) = + case d of + DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) + | DDatatype (x, n, xncs) => + let + val env = pushCNamedAs env x n (KType, loc) NONE + in + foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) + | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) + env xncs + end + | DDatatypeImp (x, n, m, ms, x') => + let + val t = (CModProj (m, ms, x'), loc) + val env = pushCNamedAs env x n (KType, loc) (SOME t) + val (_, sgn) = lookupStrNamed env m + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case projectStr env {sgn = sgn, str = str, field = m} of + NONE => raise Fail "ElabEnv.declBinds: Couldn't projectStr" + | SOME sgn => ((StrProj (str, m), loc), sgn)) + ((StrVar m, loc), sgn) ms + val xncs = case projectDatatype env {sgn = sgn, str = str, field = x'} of + NONE => raise Fail "ElabEnv.declBinds: Couldn't projectDatatype" + | SOME xncs => xncs + + val t = (CNamed n, loc) + in + foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t + | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc)) + env xncs + end + | DVal (x, n, t, _) => pushENamedAs env x n t + | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis + | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn + | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn + | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | DConstraint _ => env + | DExport _ => env + end diff --git a/src/elaborate.sml b/src/elaborate.sml index c6b4ed1c..f5efdd96 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -116,6 +116,7 @@ fun unifyKinds k1 k2 = datatype con_error = UnboundCon of ErrorMsg.span * string + | UnboundDatatype of ErrorMsg.span * string | UnboundStrInCon of ErrorMsg.span * string | WrongKind of L'.con * L'.kind * L'.kind * kunify_error | DuplicateField of ErrorMsg.span * string @@ -124,6 +125,8 @@ fun conError env err = case err of UnboundCon (loc, s) => ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) + | UnboundDatatype (loc, s) => + ErrorMsg.errorAt loc ("Unbound datatype " ^ s) | UnboundStrInCon (loc, s) => ErrorMsg.errorAt loc ("Unbound structure " ^ s) | WrongKind (c, k1, k2, kerr) => @@ -1283,7 +1286,38 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) end - | L.SgiDatatype _ => raise Fail "Elaborate SgiDatatype" + | L.SgiDatatype (x, xcs) => + let + val k = (L'.KType, loc) + val (env, n) = E.pushCNamed env x k NONE + val t = (L'.CNamed n, loc) + + val (xcs, (used, env, gs)) = + ListUtil.foldlMap + (fn ((x, to), (used, env, gs)) => + let + val (to, t, gs') = case to of + NONE => (NONE, t, gs) + | SOME t' => + let + val (t', tk, gs') = elabCon (env, denv) t' + in + checkKind env t' tk k; + (SOME t', (L'.TFun (t', t), loc), gs' @ gs) + end + + val (env, n') = E.pushENamed env x t + in + if SS.member (used, x) then + strError env (DuplicateConstructor (x, loc)) + else + (); + ((x, n', to), (SS.add (used, x), env, gs')) + end) + (SS.empty, env, []) xcs + in + ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs)) + end | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp" @@ -1855,7 +1889,45 @@ fun elabDecl ((d, loc), (env, denv, gs)) = ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs)) end - | L.DDatatypeImp _ => raise Fail "Elaborate DDatatypeImp" + | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" + + | L.DDatatypeImp (x, m1 :: ms, s) => + (case E.lookupStr env m1 of + NONE => (expError env (UnboundStrInExp (loc, m1)); + ([], (env, denv, gs))) + | SOME (n, sgn) => + let + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {sgn = sgn, str = str, field = m} of + NONE => (conError env (UnboundStrInCon (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms + in + case E.projectDatatype env {sgn = sgn, str = str, field = s} of + NONE => (conError env (UnboundDatatype (loc, s)); + ([], (env, denv, gs))) + | SOME xncs => + let + val k = (L'.KType, loc) + val t = (L'.CModProj (n, ms, s), loc) + val (env, n') = E.pushCNamed env x k (SOME t) + val env = E.pushDatatype env n' xncs + + val t = (L'.CNamed n', loc) + val env = foldl (fn ((x, n, to), env) => + let + val t = case to of + NONE => t + | SOME t' => (L'.TFun (t', t), loc) + in + E.pushENamedAs env x n t + end) env xncs + in + ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, [])) + end + end) + | L.DVal (x, co, e) => let val (c', _, gs1) = case co of diff --git a/src/lacweb.grm b/src/lacweb.grm index 08e36356..a1a0663f 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -136,7 +136,8 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft, | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), s (LTYPEleft, cexpright)) | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) - | DATATYPE SYMBOL EQ DATATYPE path(DDatatypeImp (SYMBOL, #1 path, #2 path), s (DATATYPEleft, pathright)) + | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path + (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) | VAL vali (DVal vali, s (VALleft, valiright)) | VAL REC valis (DValRec valis, s (VALleft, valisright)) @@ -200,7 +201,8 @@ sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, k | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), s (LTYPEleft, cexpright)) | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) - | DATATYPE SYMBOL EQ DATATYPE path(SgiDatatypeImp (SYMBOL, #1 path, #2 path), s (DATATYPEleft, pathright)) + | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path + (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) |