# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1216928970 14400
# Node ID adc4e42e3adc13fdd7ea90a710b27325a006c666
# Parent  34ccd7d2bea869d695f805adf834d1c7d93ea121
Basic datatype importing works

diff -r 34ccd7d2bea8 -r adc4e42e3adc src/elab_env.sig
--- 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
diff -r 34ccd7d2bea8 -r adc4e42e3adc src/elab_env.sml
--- 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
diff -r 34ccd7d2bea8 -r adc4e42e3adc src/elaborate.sml
--- 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
diff -r 34ccd7d2bea8 -r adc4e42e3adc src/lacweb.grm
--- 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))
diff -r 34ccd7d2bea8 -r adc4e42e3adc tests/datatypeMod.lac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/datatypeMod.lac	Thu Jul 24 15:49:30 2008 -0400
@@ -0,0 +1,8 @@
+structure M : sig datatype t = A | B end = struct
+        datatype t = A | B
+end
+
+datatype u = datatype M.t
+
+val a : M.t = A
+val a2 : u = a