Mercurial > urweb
changeset 157:adc4e42e3adc
Basic datatype importing works
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 24 Jul 2008 15:49:30 -0400 |
parents | 34ccd7d2bea8 |
children | b4b70de488e9 |
files | src/elab_env.sig src/elab_env.sml src/elaborate.sml src/lacweb.grm tests/datatypeMod.lac |
diffstat | 5 files changed, 192 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sig Thu Jul 24 15:02:03 2008 -0400 +++ b/src/elab_env.sig Thu Jul 24 15:49:30 2008 -0400 @@ -51,6 +51,12 @@ 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 @@ 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
--- a/src/elab_env.sml Thu Jul 24 15:02:03 2008 -0400 +++ b/src/elab_env.sml Thu Jul 24 15:49:30 2008 -0400 @@ -73,11 +73,15 @@ | 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 @@ relC = [], namedC = IM.empty, + datatypes = IM.empty, + renameE = SM.empty, relE = [], namedE = IM.empty, @@ -124,6 +130,8 @@ 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 @@ 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 @@ | 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 @@ 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 @@ 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 @@ relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -267,6 +314,8 @@ relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + renameE = #renameE env, relE = #relE env, namedE = #namedE env, @@ -292,26 +341,6 @@ 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 @@ 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 @@ | 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
--- a/src/elaborate.sml Thu Jul 24 15:02:03 2008 -0400 +++ b/src/elaborate.sml Thu Jul 24 15:49:30 2008 -0400 @@ -116,6 +116,7 @@ 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 @@ 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 @@ ([(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 @@ ([(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
--- a/src/lacweb.grm Thu Jul 24 15:02:03 2008 -0400 +++ b/src/lacweb.grm Thu Jul 24 15:49:30 2008 -0400 @@ -136,7 +136,8 @@ | 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 @@ | 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))