diff src/corify.sml @ 46:44a1bc863f0f

Corifying functors
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 17:55:36 -0400
parents 3c1ce1b4eb3d
children 0a5c312de09a
line wrap: on
line diff
--- a/src/corify.sml	Thu Jun 19 17:11:24 2008 -0400
+++ b/src/corify.sml	Thu Jun 19 17:55:36 2008 -0400
@@ -68,16 +68,22 @@
     val bindStr : t -> string -> int -> t -> t
     val lookupStrById : t -> int -> t
     val lookupStrByName : string * t -> t
+
+    val bindFunctor : t -> string -> int -> int -> L.str -> t
+    val lookupFunctorById : t -> int -> int * L.str
+    val lookupFunctorByName : string * t -> int * L.str
 end = struct
 
 datatype flattening = F of {
          core : int SM.map,
-         strs : flattening SM.map
+         strs : flattening SM.map,
+         funs : (int * L.str) SM.map
 }
                            
 type t = {
      core : int IM.map,
      strs : flattening IM.map,
+     funs : (int * L.str) IM.map,
      current : flattening,
      nested : flattening list
 }
@@ -85,24 +91,27 @@
 val empty = {
     core = IM.empty,
     strs = IM.empty,
-    current = F { core = SM.empty, strs = SM.empty },
+    funs = IM.empty,
+    current = F { core = SM.empty, strs = SM.empty, funs = SM.empty },
     nested = []
 }
 
-fun bindCore {core, strs, current, nested} s n =
+fun bindCore {core, strs, funs, current, nested} s n =
     let
         val n' = alloc ()
 
         val current =
             let
-                val F {core, strs} = current
+                val F {core, strs, funs} = current
             in
                 F {core = SM.insert (core, s, n'),
-                   strs = strs}
+                   strs = strs,
+                   funs = funs}
             end
     in
         ({core = IM.insert (core, n, n'),
           strs = strs,
+          funs = funs,
           current = current,
           nested = nested},
          n')
@@ -115,36 +124,43 @@
         NONE => raise Fail "Corify.St.lookupCoreByName"
       | SOME n => n
 
-fun enter {core, strs, current, nested} =
+fun enter {core, strs, funs, current, nested} =
     {core = core,
      strs = strs,
+     funs = funs,
      current = F {core = SM.empty,
-                  strs = SM.empty},
+                  strs = SM.empty,
+                  funs = SM.empty},
      nested = current :: nested}
 
 fun dummy f = {core = IM.empty,
                strs = IM.empty,
+               funs = IM.empty,
                current = f,
                nested = []}
 
-fun leave {core, strs, current, nested = m1 :: rest} =
+fun leave {core, strs, funs, current, nested = m1 :: rest} =
         {outer = {core = core,
                   strs = strs,
+                  funs = funs,
                   current = m1,
                   nested = rest},
          inner = dummy current}
   | leave _ = raise Fail "Corify.St.leave"
 
-fun bindStr ({core, strs, current = F {core = mcore, strs = mstrs}, nested} : t) x n ({current = f, ...} : t) =
+fun bindStr ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t)
+            x n ({current = f, ...} : t) =
     {core = core,
      strs = IM.insert (strs, n, f),
+     funs = funs,
      current = F {core = mcore,
-                  strs = SM.insert (mstrs, x, f)},
+                  strs = SM.insert (mstrs, x, f),
+                  funs = mfuns},
      nested = nested}
 
 fun lookupStrById ({strs, ...} : t) n =
     case IM.find (strs, n) of
-        NONE => raise Fail "Corify.St.lookupStr"
+        NONE => raise Fail "Corify.St.lookupStrById"
       | SOME f => dummy f
 
 fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) =
@@ -152,6 +168,26 @@
         NONE => raise Fail "Corify.St.lookupStrByName"
       | SOME f => dummy f
 
+fun bindFunctor ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t)
+                x n na str =
+    {core = core,
+     strs = strs,
+     funs = IM.insert (funs, n, (na, str)),
+     current = F {core = mcore,
+                  strs = mstrs,
+                  funs = SM.insert (mfuns, x, (na, str))},
+     nested = nested}
+
+fun lookupFunctorById ({funs, ...} : t) n =
+    case IM.find (funs, n) of
+        NONE => raise Fail "Corify.St.lookupFunctorById"
+      | SOME v => v
+
+fun lookupFunctorByName (m, {current = F {funs, ...}, ...} : t) =
+    case SM.find (funs, m) of
+        NONE => raise Fail "Corify.St.lookupFunctorByName"
+      | SOME v => v
+
 end
 
 
@@ -233,6 +269,9 @@
                                                                         
       | L.DSgn _ => ([], st)
 
+      | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) =>
+        ([], St.bindFunctor st x n na str)
+
       | L.DStr (x, n, _, str) =>
         let
             val (ds, {inner, outer}) = corifyStr (str, st)
@@ -257,8 +296,28 @@
         in
             (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
         end
-      | L.StrFun _ => raise Fail "Corify functor"
-      | L.StrApp _ => raise Fail "Corify functor app"
+      | L.StrFun _ => raise Fail "Corify of nested functor definition"
+      | L.StrApp (str1, str2) =>
+        let
+            fun unwind' (str, _) =
+                case str of
+                    L.StrVar n => St.lookupStrById st n
+                  | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str)
+                  | _ => raise Fail "Corify of fancy functor application [1]"
+
+            fun unwind (str, _) =
+                case str of
+                    L.StrVar n => St.lookupFunctorById st n
+                  | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
+                  | _ => raise Fail "Corify of fancy functor application [2]"
+
+            val (na, body) = unwind str1
+
+            val (ds1, {inner, outer}) = corifyStr (str2, st)
+            val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner)
+        in
+            (ds1 @ ds2, sts)
+        end
 
 fun maxName ds = foldl (fn ((d, _), n) =>
                            case d of