Start of elaboration

10 files changed, 617 insertions, 0 deletions

diff --git a/src/elab.sml b/src/elab.sml
new file mode 100644
index 00000000..3c339190
--- /dev/null
+++ b/src/elab.sml
@@ -0,0 +1,74 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Elab = struct
+
+type 'a located = 'a ErrorMsg.located
+
+datatype kind' =
+         KType
+       | KArrow of kind * kind
+       | KName
+       | KRecord of kind
+
+       | KError
+       | KUnif of string * kind option ref
+
+withtype kind = kind' located
+
+datatype explicitness =
+         Explicit
+       | Implicit
+
+datatype con' =
+         TFun of con * con
+       | TCFun of explicitness * string * kind * con
+       | TRecord of con
+
+       | CRel of int
+       | CNamed of int
+       | CApp of con * con
+       | CAbs of explicitness * string * kind * con
+
+       | CName of string
+
+       | CRecord of kind * (con * con) list
+       | CConcat of con * con
+
+       | CError
+       | CUnif of string * con option ref
+
+withtype con = con' located
+
+datatype decl' =
+         DCon of string * kind * con
+
+withtype decl = decl' located
+
+type file = decl list
+
+end
diff --git a/src/elab_env.sig b/src/elab_env.sig
new file mode 100644
index 00000000..8300c2a9
--- /dev/null
+++ b/src/elab_env.sig
@@ -0,0 +1,49 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature ELAB_ENV = sig
+
+    type env
+
+    val empty : env
+
+    exception UnboundRel of int
+    exception UnboundNamed of int
+
+    val pushCRel : env -> string -> Elab.kind -> env
+    val lookupCRel : env -> int -> string * Elab.kind
+
+    val pushCNamed : env -> string -> Elab.kind -> env * int
+    val lookupCNamed : env -> int -> string * Elab.kind
+                                                 
+    datatype var =
+             CNotBound
+           | CRel of int * Elab.kind
+           | CNamed of int * Elab.kind
+    val lookupC : env -> string -> var
+
+end
diff --git a/src/elab_env.sml b/src/elab_env.sml
new file mode 100644
index 00000000..7b932aad
--- /dev/null
+++ b/src/elab_env.sml
@@ -0,0 +1,100 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ElabEnv :> ELAB_ENV = struct
+
+open Elab
+
+structure IM = IntBinaryMap
+structure SM = BinaryMapFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
+
+exception UnboundRel of int
+exception UnboundNamed of int
+
+datatype var' =
+         CRel' of int * kind
+       | CNamed' of int * kind
+
+datatype var =
+         CNotBound
+       | CRel of int * kind
+       | CNamed of int * kind
+
+type env = {
+     renameC : var' SM.map,
+     relC : (string * kind) list,
+     namedC : (string * kind) IM.map
+}
+
+val namedCounter = ref 0
+
+val empty = {
+    renameC = SM.empty,
+    relC = [],
+    namedC = IM.empty
+}
+
+fun pushCRel (env : env) x k =
+    let
+        val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k)
+                               | x => x) (#renameC env)
+    in
+        {renameC = SM.insert (renameC, x, CRel' (0, k)),
+         relC = (x, k) :: #relC env,
+         namedC = #namedC env}
+    end
+
+fun lookupCRel (env : env) n =
+    (List.nth (#relC env, n))
+    handle Subscript => raise UnboundRel n
+
+fun pushCNamed (env : env) x k =
+    let
+        val n = !namedCounter
+    in
+        namedCounter := n + 1;
+        ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
+          relC = #relC env,
+          namedC = IM.insert (#namedC env, n, (x, k))},
+         n)
+    end
+
+fun lookupCNamed (env : env) n =
+    case IM.find (#namedC env, n) of
+        NONE => raise UnboundNamed n
+      | SOME x => x
+
+fun lookupC (env : env) x =
+    case SM.find (#renameC env, x) of
+        NONE => CNotBound
+      | SOME (CRel' x) => CRel x
+      | SOME (CNamed' x) => CNamed x
+
+end
diff --git a/src/elab_util.sig b/src/elab_util.sig
new file mode 100644
index 00000000..0190b576
--- /dev/null
+++ b/src/elab_util.sig
@@ -0,0 +1,36 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature ELAB_UTIL = sig
+
+structure Kind : sig
+    val mapfold : (Elab.kind', 'state, 'abort) Search.mapfold_arg
+                  -> (Elab.kind, 'state, 'abort) Search.mapfolder
+    val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
+end
+
+end
diff --git a/src/elab_util.sml b/src/elab_util.sml
new file mode 100644
index 00000000..8a0463cf
--- /dev/null
+++ b/src/elab_util.sml
@@ -0,0 +1,78 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ElabUtil :> ELAB_UTIL = struct
+
+open Elab
+
+structure S = Search
+
+structure Kind = struct
+
+fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'state, 'abort) S.mapfolder =
+    let
+        fun mfk k acc =
+            S.bindP (mfk' k acc, f)
+
+        and mfk' (kAll as (k, loc)) =
+            case k of
+                KType => S.return2 kAll
+
+              | KArrow (k1, k2) =>
+                S.bind2 (mfk k1,
+                      fn k1' =>
+                         S.map2 (mfk k2,
+                              fn k2' =>
+                                 (KArrow (k1', k2'), loc)))
+
+              | KName => S.return2 kAll
+
+              | KRecord k =>
+                S.map2 (mfk k,
+                        fn k' =>
+                           (KRecord k', loc))
+
+              | KError => S.return2 kAll
+
+              | KUnif (_, ref (SOME k)) => mfk' k
+              | KUnif _ => S.return2 kAll
+    in
+        mfk
+    end
+
+fun exists f k =
+    case mapfold (fn (k, ()) =>
+                     if f k then
+                         S.Return ()
+                     else
+                         S.Continue (k, ())) k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+end
diff --git a/src/elaborate.sig b/src/elaborate.sig
new file mode 100644
index 00000000..99fc9ebf
--- /dev/null
+++ b/src/elaborate.sig
@@ -0,0 +1,32 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature ELABORATE = sig
+
+    val elabFile : Laconic.file -> Elab.file
+
+end
diff --git a/src/elaborate.sml b/src/elaborate.sml
new file mode 100644
index 00000000..ca950de2
--- /dev/null
+++ b/src/elaborate.sml
@@ -0,0 +1,102 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Elaborate :> ELABORATE = struct
+
+structure L = Laconic
+structure L' = Elab
+structure E = ElabEnv
+structure U = ElabUtil
+
+fun elabKind (k, loc) =
+    case k of
+        L.KType => (L'.KType, loc)
+      | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
+      | L.KName => (L'.KName, loc)
+      | L.KRecord k => (L'.KRecord (elabKind k), loc)
+
+fun elabExplicitness e =
+    case e of
+        L.Explicit => L'.Explicit
+      | L.Implicit => L'.Implicit
+
+fun occursKind r =
+    U.Kind.exists (fn L'.KUnif (_, r') => r = r'
+                    | _ => false)
+
+datatype unify_error =
+         KOccursCheckFailed of L'.kind * L'.kind
+       | KIncompatible of L'.kind * L'.kind
+
+fun unifyError err =
+    case err of
+        KOccursCheckFailed (k1, k2) =>
+        ErrorMsg.errorAt (#2 k1) "Kind occurs check failed"
+      | KIncompatible (k1, k2) =>
+        ErrorMsg.errorAt (#2 k1) "Incompatible kinds"
+
+fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) =
+    let
+        fun err f = unifyError (f (k1All, k2All))
+    in
+        case (k1, k2) of
+            (L'.KType, L'.KType) => ()
+          | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
+            (unifyKinds d1 d2;
+             unifyKinds r1 r2)
+          | (L'.KName, L'.KName) => ()
+          | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2
+
+          | (L'.KError, _) => ()
+          | (_, L'.KError) => ()
+
+          | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All
+          | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All
+
+          | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
+            if r1 = r2 then
+                ()
+            else
+                r1 := SOME k2All
+
+          | (L'.KUnif (_, r), _) =>
+            if occursKind r k2All then
+                err KOccursCheckFailed
+            else
+                r := SOME k2All
+          | (_, L'.KUnif (_, r)) =>
+            if occursKind r k1All then
+                err KOccursCheckFailed
+            else
+                r := SOME k1All
+
+          | _ => err KIncompatible
+    end
+
+fun elabFile _ = raise Fail ""
+
+end
diff --git a/src/search.sig b/src/search.sig
new file mode 100644
index 00000000..65fc6aa6
--- /dev/null
+++ b/src/search.sig
@@ -0,0 +1,62 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature SEARCH = sig
+
+    datatype ('state, 'abort) result =
+             Return of 'abort
+           | Continue of 'state
+
+    type ('data, 'state, 'abort) mapfold_arg =
+         'data * 'state -> ('data * 'state, 'abort) result
+
+    type ('data, 'state, 'abort) mapfolder =
+         'data -> 'state -> ('data * 'state, 'abort) result
+
+    val return2 : 'state1 -> 'state2 -> ('state1 * 'state2, 'abort) result
+
+    val map : ('state1, 'abort) result
+              * ('state1 -> 'state2)
+              -> ('state2, 'abort) result
+
+    val map2 : ('state2 -> ('state1 * 'state2, 'abort) result)
+               * ('state1 -> 'state1')
+               -> ('state2 -> ('state1' * 'state2, 'abort) result)
+                         
+    val bind : ('state1, 'abort) result
+               * ('state1 -> ('state2, 'abort) result)
+               -> ('state2, 'abort) result
+
+    val bind2 : ('state2 -> ('state1 * 'state2, 'abort) result)
+               * ('state1 -> 'state2 -> ('state1 * 'state2, 'abort) result)
+               -> ('state2 -> ('state1 * 'state2, 'abort) result)
+
+    val bindP : (('state11 * 'state12) * 'state2, 'abort) result
+                * ('state11 * 'state2 -> ('state11 * 'state2, 'abort) result)
+                -> (('state11 * 'state12) * 'state2, 'abort) result
+
+end
diff --git a/src/search.sml b/src/search.sml
new file mode 100644
index 00000000..50904bba
--- /dev/null
+++ b/src/search.sml
@@ -0,0 +1,70 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Search :> SEARCH = struct
+
+datatype ('state, 'abort) result =
+         Return of 'abort
+       | Continue of 'state
+
+type ('data, 'state, 'abort) mapfold_arg =
+     'data * 'state -> ('data * 'state, 'abort) result
+
+type ('data, 'state, 'abort) mapfolder =
+     'data -> 'state -> ('data * 'state, 'abort) result
+
+fun return2 v acc = Continue (v, acc)
+
+fun map (r, f) =
+    case r of
+        Continue acc => Continue (f acc)
+      | Return x => Return x
+
+fun map2 (r, f) acc =
+    case r acc of
+        Continue (x, acc) => Continue (f x, acc)
+      | Return x => Return x
+
+fun bind (r, f) =
+    case r of
+        Continue acc => f acc
+      | Return x => Return x
+
+fun bind2 (r, f) acc =
+    case r acc of
+        Continue (x, acc) => f x acc
+      | Return x => Return x
+
+fun bindP (r, f) =
+    case r of
+        Continue ((x, pos), acc) =>
+        map (f (x, acc),
+          fn (x', acc') =>
+             ((x', pos), acc'))
+      | Return x => Return x
+
+end
diff --git a/src/sources b/src/sources
index 0329092a..6270b1ea 100644
--- a/src/sources
+++ b/src/sources
@@ -12,5 +12,19 @@ print.sml
 laconic_print.sig
 laconic_print.sml
 
+elab.sml
+
+search.sig
+search.sml
+
+elab_util.sig
+elab_util.sml
+
+elab_env.sig
+elab_env.sml
+
+elaborate.sig
+elaborate.sml
+
 compiler.sig
 compiler.sml