diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+2009
+BSD3 License terms
+
+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.
+
+Neither the name of the developers nor the names of its contributors
+may 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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,59 @@
+Overview
+========
+[copilot-core](http://hackage.haskell.org/package/copilot-core) The core
+language, which efficiently represents Copilot expressions.  The core is only of
+interest to implementers wishing to add a new back-end to Copilot.
+
+Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
+Haskell that compiles into embedded C.  Copilot is similar in spirit to
+languages like Lustre.  Copilot contains an interpreter, multiple back-end
+compilers, and other verification tools.
+
+Installation
+============
+The Copilot library is cabalized. Assuming you have cabal and the GHC compiler
+installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the
+easiest way to obtain these), it should merely be a matter of running 
+     
+         cabal install copilot-core
+
+However, we strongly recommend you install Copilot, which installs copilot-c99
+and other packages automatically.  Execute
+
+         cabal install copilot
+
+Resources
+=========
+To understand our use of Dynamic typing, please consult the following,
+particularly the last document:
+
++ Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,
+  "*Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages*",
+  Journal of Functional Programming vol. 19, p. 509-543, 2009.
+
++ Guillemette, Louis-Julien and Monnier, Stefan,
+  "*Type-Safe Code Transformations in Haskell*",
+  Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007.
+
++ Baars, Arthur I. and Swierstra, S. Doaitse,
+  "*Typing dynamic typing*",
+  ACM SIGPLAN Notices vol. 37, p. 157-166, 2002
+
+Resources
+=========
+[copilot-core](http://hackage.haskell.org/package/copilot-core) is available on
+Hackage.
+
+**Sources** for each package are available on Github as well.  Just go to
+[Github](github.com) and search for the package of interest.  Feel free to fork!
+
+Copyright, License
+==================
+Copilot is distributed with the BSD3 license. The license file contains the
+[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
+
+Thanks
+======
+We are grateful for NASA Contract NNL08AD13T to [Galois,
+Inc](http://corp.galois.com/) and the [National Institute of
+Aerospace](http://www.nianet.org/), which partially supported this work.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/copilot-core.cabal b/copilot-core.cabal
new file mode 100644
--- /dev/null
+++ b/copilot-core.cabal
@@ -0,0 +1,68 @@
+cabal-version:       >=1.10
+name:                copilot-core
+version:             0.2
+synopsis:            An intermediate representation for Copilot.
+description:         Intermediate representation for Copilot.
+                     Strictly follows Haskell 2010 except for universal
+                     and existential quantification.
+author:              Lee Pike, Robin Morisset, Alwyn Goodloe,
+                     Sebastian Niller, Nis Nordby Wegmann
+license:             BSD3
+license-file:        LICENSE
+maintainer:          leepike@gmail.com
+stability:           Experimental
+category:            Language, Embedded
+build-type:          Simple
+extra-source-files:  README.md
+
+source-repository head
+    type:       git
+    location:   git://github.com/niswegmann/copilot-core.git
+
+library
+
+  default-language:  Haskell2010
+
+  hs-source-dirs:    src
+
+  ghc-options:
+    -Wall
+    -fwarn-tabs
+    -auto-all
+    -caf-all
+    -fno-warn-orphans
+    --enable-library-profiling
+
+  build-depends:
+    containers >= 0.4 && < 1,
+    base >= 4.0 && < 5,
+    pretty >= 1.0,
+    random > 1.0,
+    pretty-ncols >= 0.1,
+    mtl >= 2.0,
+    dlist
+
+  exposed-modules:
+
+    Copilot.Compile.Header.C99
+    Copilot.Core
+    Copilot.Core.Error
+    Copilot.Core.Expr
+    Copilot.Core.External
+    Copilot.Core.Interpret
+    Copilot.Core.Interpret.Eval
+    Copilot.Core.Interpret.Render
+    Copilot.Core.MakeTags
+    Copilot.Core.Operators
+    Copilot.Core.Spec
+    Copilot.Core.Spec.Locals
+    Copilot.Core.Random
+    Copilot.Core.Random.Gen
+    Copilot.Core.Random.Weights
+    Copilot.Core.Type
+    Copilot.Core.Type.Dynamic
+    Copilot.Core.Type.Equality
+    Copilot.Core.Type.Show
+    Copilot.Core.Type.Uninitialized
+    Copilot.Core.PrettyPrint
+    Copilot.Core.Version
diff --git a/src/Copilot/Compile/Header/C99.hs b/src/Copilot/Compile/Header/C99.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Header/C99.hs
@@ -0,0 +1,198 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Generates a C99 header from a copilot-specification. The functionality
+-- provided by the header must be implemented by back-ends targetting C99.
+
+{-# LANGUAGE GADTs #-}
+
+module Copilot.Compile.Header.C99
+  ( genC99Header
+  , c99HeaderName
+  ) where
+
+import Copilot.Core
+import Copilot.Core.Version
+import Data.List (intersperse, nubBy)
+import Text.PrettyPrint.HughesPJ
+import Prelude hiding (unlines)
+
+--------------------------------------------------------------------------------
+
+genC99Header :: Maybe String -> FilePath -> Spec -> IO ()
+genC99Header mprefix path spec =
+  let
+    filePath = path ++ "/" ++ prefix ++ "copilot.h"
+    prefix   = case mprefix of
+                 Just cs -> cs ++ "_"
+                 _       -> ""
+  in
+    writeFile filePath (c99Header prefix spec)
+
+c99HeaderName :: Maybe String -> String
+c99HeaderName (Just cs) = cs ++ "_" ++ "copilot.h"
+c99HeaderName _         = "copilot.h"
+
+c99Header :: String -> Spec -> String
+c99Header prefix spec = render $ vcat $
+  [ text "/* Generated by Copilot Core v." <+> text version <+> text "*/"
+  , text ""
+  , ppHeaders
+  , text ""
+  , text "/* Observers (defined by Copilot): */"
+  , text ""
+  , ppObservers prefix (specObservers spec)
+  , text ""
+  , text "/* Triggers (must be defined by user): */"
+  , text ""
+  , ppTriggerPrototypes prefix (specTriggers spec)
+  , text ""
+  , text "/* External variables (must be defined by user): */"
+  , text ""
+  , ppExternalVariables (externVars spec)
+  , text ""
+  , text "/* External arrays (must be defined by user): */"
+  , text ""
+  , ppExternalArrays (externArrays spec)
+  , text ""
+  , text "/* External functions (must be defined by user): */"
+  , text ""
+  , ppExternalFunctions (externFuns spec)
+  , text ""
+  , text "/* Step function: */"
+  , text ""
+  , ppStep prefix
+  ]
+
+--------------------------------------------------------------------------------
+
+ppHeaders :: Doc
+ppHeaders = unlines
+  [ "#include <stdint.h>"
+  , "#include <stdbool.h>"
+  ]
+
+--------------------------------------------------------------------------------
+
+ppObservers :: String -> [Observer] -> Doc
+ppObservers prefix = vcat . map ppObserver
+
+  where
+
+  ppObserver :: Observer -> Doc
+  ppObserver
+    Observer
+      { observerName     = name
+      , observerExprType = t } =
+          text "extern" <+> text (typeSpec (UType t)) <+>
+          text (prefix ++ name) <> text ";"
+
+--------------------------------------------------------------------------------
+
+ppTriggerPrototypes :: String -> [Trigger] -> Doc
+ppTriggerPrototypes prefix = vcat . map ppTriggerPrototype
+
+  where
+
+  ppTriggerPrototype :: Trigger -> Doc
+  ppTriggerPrototype
+    Trigger
+      { triggerName = name
+      , triggerArgs = args } =
+          text "void" <+> text (prefix ++ name) <>
+          text "(" <> ppArgs args <> text ");"
+
+    where
+
+    ppArgs :: [UExpr] -> Doc
+    ppArgs = vcat . intersperse (text ",") . map ppArg
+
+    ppArg :: UExpr -> Doc
+    ppArg UExpr { uExprType = t } = text (typeSpec (UType t))
+
+--------------------------------------------------------------------------------
+
+ppExternalVariables :: [ExtVar] -> Doc
+ppExternalVariables = vcat . map ppExternalVariable
+
+ppExternalVariable :: ExtVar -> Doc
+ppExternalVariable
+  ExtVar
+    { externVarName = name
+    , externVarType = t } =
+        text "extern" <+> text (typeSpec t) <+> text name <> text ";"
+
+--------------------------------------------------------------------------------
+
+ppExternalArrays :: [ExtArray] -> Doc
+ppExternalArrays = vcat . map ppExternalArray . nubBy eq
+
+  where
+
+  eq ExtArray { externArrayName = name1 } ExtArray { externArrayName = name2 } =
+    name1 == name2
+
+ppExternalArray :: ExtArray -> Doc
+ppExternalArray
+  ExtArray
+    { externArrayName = name
+    , externArrayElemType = t } =
+        text "extern" <+> text (typeSpec (UType t)) <+> text "*" <+>
+        text name <> text ";"
+
+--------------------------------------------------------------------------------
+
+ppExternalFunctions :: [ExtFun] -> Doc
+ppExternalFunctions = vcat . map ppExternalFunction . nubBy eq
+
+  where
+
+  eq ExtFun { externFunName = name1 } ExtFun { externFunName = name2 } =
+    name1 == name2
+
+ppExternalFunction :: ExtFun -> Doc
+ppExternalFunction
+  ExtFun
+    { externFunName = name
+    , externFunType = t
+    , externFunArgs = args } =
+        text (typeSpec (UType t)) <+> text name <>
+        text "(" <> ppArgs args <> text ");"
+
+  where
+
+  ppArgs :: [UExpr] -> Doc
+  ppArgs = hcat . intersperse (text ",") . map ppArg
+
+  ppArg :: UExpr -> Doc
+  ppArg UExpr { uExprType = t1 } = text (typeSpec (UType t1))
+
+--------------------------------------------------------------------------------
+
+typeSpec :: UType -> String
+typeSpec UType { uTypeType = t } = typeSpec' t
+
+  where
+
+  typeSpec' Bool = "bool"
+  typeSpec' Int8   = "int8_t"
+  typeSpec' Int16  = "int16_t"
+  typeSpec' Int32  = "int32_t"
+  typeSpec' Int64  = "int64_t"
+  typeSpec' Word8  = "uint8_t"
+  typeSpec' Word16 = "uint16_t"
+  typeSpec' Word32 = "uint32_t"
+  typeSpec' Word64 = "uint64_t"
+  typeSpec' Float  = "float"
+  typeSpec' Double = "double"
+
+--------------------------------------------------------------------------------
+
+ppStep :: String -> Doc
+ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "();"
+
+--------------------------------------------------------------------------------
+
+unlines :: [String] -> Doc
+unlines = vcat . map text
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core.hs
@@ -0,0 +1,47 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Intermediate representation for Copilot specifications.
+-- The form of the representation is based on this paper:
+--
+-- * Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,
+-- \"/Finally tagless, partially evaluated: Tagless staged/
+-- /interpreters for simpler typed languages/\",
+-- Journal of Functional Programming vol. 19, p. 509-543, 2009.
+--
+-- The following article might also be useful:
+--
+-- * Guillemette, Louis-Julien and Monnier, Stefan,
+-- \"/Type-Safe Code Transformations in Haskell/\",
+-- Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007.
+--
+-- For examples of how to traverse a Copilot specification see
+-- the source code of the interpreter
+-- ("Copilot.Core.Interpret")
+-- and the pretty-printer
+-- ("Copilot.Core.PrettyPrint").
+
+module Copilot.Core
+  ( module Copilot.Core.Error
+  , module Copilot.Core.Expr
+  , module Copilot.Core.External
+  , module Copilot.Core.MakeTags
+  , module Copilot.Core.Operators
+  , module Copilot.Core.Spec
+  , module Copilot.Core.Type
+  , module Copilot.Core.Type.Uninitialized
+  , module Data.Int
+  , module Data.Word
+  ) where
+
+import Copilot.Core.Error
+import Copilot.Core.Expr
+import Copilot.Core.External
+import Copilot.Core.MakeTags
+import Copilot.Core.Operators
+import Copilot.Core.Spec
+import Copilot.Core.Type
+import Copilot.Core.Type.Uninitialized
+import Data.Int
+import Data.Word
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Error.hs
@@ -0,0 +1,16 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+module Copilot.Core.Error 
+  ( impossible
+  , badUsage ) where
+
+impossible :: String -> String -> a
+impossible function package = 
+  error $ "Impossible error in function " ++ function ++ ", in package " ++ 
+    package ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " ++
+    "(remove spaces) or file a bug report on github.com."
+
+badUsage :: String -> a
+badUsage msg = error $ "Copilot error: " ++ msg ++ "."
diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Expr.hs
@@ -0,0 +1,102 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module Copilot.Core.Expr
+  ( Id
+  , Name
+  , Expr (..)
+  , UExpr (..)
+  , DropIdx
+  , Tag
+  ) where
+
+import Copilot.Core.Operators (Op1, Op2, Op3)
+import Copilot.Core.Type (Type)
+import Data.Word (Word16)
+
+--------------------------------------------------------------------------------
+
+-- | A stream identifier.
+type Id = Int
+
+--------------------------------------------------------------------------------
+
+-- | A name of a trigger, an external variable, or an external function.
+type Name = String
+
+--------------------------------------------------------------------------------
+
+-- | An index for the drop operator.
+type DropIdx = Word16
+
+--------------------------------------------------------------------------------
+
+-- | A unique tag for external arrays/function calls.
+type Tag = Int
+
+--------------------------------------------------------------------------------
+
+data Expr a where
+  Const
+    :: Type a
+    -> a
+    -> Expr a
+  Drop
+    :: Type a
+    -> DropIdx
+    -> Id
+    -> Expr a
+  Local
+    :: Type a
+    -> Type b
+    -> Name
+    -> Expr a
+    -> Expr b
+    -> Expr b
+  Var
+    :: Type a
+    -> Name
+    -> Expr a
+  ExternVar
+    :: Type a
+    -> Name
+    -> Expr a
+  ExternFun
+    :: Type a
+    -> Name
+    -> [UExpr]
+    -> Maybe Tag
+    -> Expr a
+  ExternArray
+    :: Integral a
+    => Type a
+    -> Type b
+    -> Name
+    -> Expr a
+    -> Maybe Tag
+    -> Expr b
+  Op1
+    :: Op1 a b
+    -> Expr a
+    -> Expr b
+  Op2
+    :: Op2 a b c
+    -> Expr a
+    -> Expr b
+    -> Expr c
+  Op3
+    :: Op3 a b c d
+    -> Expr a
+    -> Expr b
+    -> Expr c
+    -> Expr d
+
+--------------------------------------------------------------------------------
+
+-- | A untyped expression (no phantom type).
+data UExpr = forall a . UExpr
+  { uExprType :: Type a
+  , uExprExpr :: Expr a }
diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/External.hs
@@ -0,0 +1,133 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE Rank2Types #-}
+
+module Copilot.Core.External
+  ( ExtVar (..), ExtArray (..), ExtFun (..)
+  , externVars, externArrays, externFuns
+  ) where
+
+import Copilot.Core.Expr
+import Copilot.Core.Type
+import Copilot.Core.Spec
+import Data.DList (DList, empty, singleton, append, concat, toList)
+import Data.List (nubBy)
+import Prelude hiding (all, concat, foldr)
+
+--------------------------------------------------------------------------------
+
+data ExtVar = ExtVar
+  { externVarName :: Name
+  , externVarType :: UType }
+
+data ExtArray = forall a b . Integral a => ExtArray
+  { externArrayName     :: Name
+  , externArrayElemType :: Type b
+  , externArrayIdx      :: Expr a
+  , externArrayIdxType  :: Type a
+  , externArrayTag      :: Maybe Tag }
+
+data ExtFun = forall a . ExtFun
+  { externFunName      :: Name
+  , externFunType      :: Type a
+  , externFunArgs      :: [UExpr]
+  , externFunTag       :: Maybe Tag }
+
+--------------------------------------------------------------------------------
+
+externVars :: Spec -> [ExtVar]
+externVars = nubBy eqExt . toList . all externVarsExpr
+
+  where
+
+  eqExt :: ExtVar -> ExtVar -> Bool
+  eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } =
+    name1 == name2
+
+externVarsExpr :: Expr a -> DList ExtVar
+externVarsExpr e0 = case e0 of
+  Const  _ _            -> empty
+  Drop   _ _ _          -> empty
+  Local _ _ _ e1 e2     -> externVarsExpr e1 `append` externVarsExpr e2
+  Var _ _               -> empty
+  ExternVar t name      -> singleton (ExtVar name (UType t))
+  ExternArray _ _ _ e _ -> externVarsExpr e
+  ExternFun _ _ ues _   -> concat (map externVarsUExpr ues)
+  Op1 _ e               -> externVarsExpr e
+  Op2 _ e1 e2           -> externVarsExpr e1 `append` externVarsExpr e2
+  Op3 _ e1 e2 e3        -> externVarsExpr e1 `append`
+                           externVarsExpr e2 `append`
+                           externVarsExpr e3
+
+externVarsUExpr :: UExpr -> DList ExtVar
+externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e
+
+--------------------------------------------------------------------------------
+
+externArrays :: Spec -> [ExtArray]
+externArrays = toList . all externArraysExpr
+
+externArraysExpr :: Expr a -> DList ExtArray
+externArraysExpr e0 = case e0 of
+  Const  _ _                      -> empty
+  Drop   _ _ _                    -> empty
+  Local _ _ _ e1 e2               -> externArraysExpr e1 `append` externArraysExpr e2
+  Var _ _                         -> empty
+  ExternVar _ _                   -> empty
+  ExternArray t1 t2  name idx tag -> singleton (ExtArray name t2 idx t1 tag)
+  ExternFun _ _ ues _             -> concat (map externArraysUExpr ues)
+  Op1 _ e                         -> externArraysExpr e
+  Op2 _ e1 e2                     -> externArraysExpr e1 `append` externArraysExpr e2
+  Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`
+                                     externArraysExpr e2 `append`
+                                     externArraysExpr e3
+
+externArraysUExpr :: UExpr -> DList ExtArray
+externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e
+
+--------------------------------------------------------------------------------
+
+externFuns :: Spec -> [ExtFun]
+externFuns = toList . all externFunsExpr
+
+externFunsExpr :: Expr a -> DList ExtFun
+externFunsExpr e0 = case e0 of
+  Const  _ _                  -> empty
+  Drop   _ _ _                -> empty
+  Local _ _ _ e1 e2           -> externFunsExpr e1 `append` externFunsExpr e2
+  Var _ _                     -> empty
+  ExternVar _ _               -> empty
+  ExternArray _ _ _ idx _     -> externFunsExpr idx
+  ExternFun t name ues tag    -> singleton (ExtFun name t ues tag)
+  Op1 _ e                     -> externFunsExpr e
+  Op2 _ e1 e2                 -> externFunsExpr e1 `append` externFunsExpr e2
+  Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`
+                                 externFunsExpr e2 `append`
+                                 externFunsExpr e3
+
+--------------------------------------------------------------------------------
+
+all :: (forall a . Expr a -> DList b) -> Spec -> DList b
+all f spec =
+  concat (fmap (allStream) (specStreams   spec)) `append`
+  concat (fmap allTrigger  (specTriggers  spec)) `append`
+  concat (fmap allObserver (specObservers spec))
+
+  where
+  
+  allStream
+    Stream { streamExpr = e } = f e
+
+  allTrigger
+    Trigger
+      { triggerGuard = e
+      , triggerArgs = args } = f e `append` concat (fmap allUExpr args)
+
+  allUExpr
+    (UExpr _ e1) = f e1
+
+  allObserver
+    Observer { observerExpr = e } = f e
diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Interpret.hs
@@ -0,0 +1,27 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | An interpreter for Copilot specifications.
+
+module Copilot.Core.Interpret
+  ( ExtEnv (..)
+  , Format (..)
+  , interpret
+  ) where
+
+import Copilot.Core
+import Copilot.Core.Interpret.Eval
+import Copilot.Core.Interpret.Render
+import Copilot.Core.Type.Show (ShowType(..))
+
+data Format = Table | CSV
+
+-- | Interprets a Copilot specification.
+interpret :: Format -> Int -> ExtEnv -> Spec -> String
+interpret format k exts spec =
+  case format of
+    Table -> renderAsTable e
+    CSV   -> renderAsCSV e
+
+  where e = eval Haskell k exts spec
diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Interpret/Eval.hs
@@ -0,0 +1,310 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | A tagless interpreter for Copilot specifications.
+
+{-# LANGUAGE GADTs, BangPatterns #-}
+
+module Copilot.Core.Interpret.Eval
+  ( ExtEnv (..)
+  , Output
+  , ExecTrace (..)
+  , eval
+  ) where
+
+import Copilot.Core
+import Copilot.Core.Type.Dynamic
+import Copilot.Core.Type.Show (showWithType, ShowType)
+
+import Data.List (transpose)
+import qualified Data.Map as M
+import Data.Map (Map)
+import Data.Maybe (fromJust, catMaybes)
+import Data.Bits
+
+import Prelude hiding (id)
+import qualified Prelude as P
+
+--------------------------------------------------------------------------------
+
+type Env nm = [(nm, DynamicF [] Type)]
+
+-- | External arrays environment.
+type ArrEnv = [(Name, [DynamicF [] Type])] 
+
+-- | Environment for simulation.
+data ExtEnv = ExtEnv { varEnv  :: Env Name
+                     , arrEnv  :: ArrEnv 
+                     , funcEnv :: [(Name, Spec)] 
+                     }
+
+--------------------------------------------------------------------------------
+
+type Output = String
+
+data ExecTrace = ExecTrace
+    -- map from trigger names to their maybe output, which is a list of strings
+    -- representing their valus.  (Nothing output if the guard for the trigger
+    -- is false).
+  { interpTriggers  :: Map String [Maybe [Output]]
+    -- map from observer names to their outputs.  We also show observer outputs.
+  , interpObservers :: Map String [Output] }
+  deriving Show
+
+--------------------------------------------------------------------------------
+
+{-
+eval :: Int -> Env Name -> Spec -> ExecTrace
+eval k exts spec =
+  let
+    strms = fmap (evalStream     exts strms) (specStreams   spec)
+    trigs = fmap (evalTrigger  k exts strms) (specTriggers  spec)
+    obsvs = fmap (evalObserver k exts strms) (specObservers spec)
+  in
+    ExecTrace
+      { interpTriggers  = M.fromList $
+          zip (fmap triggerName  (specTriggers  spec)) trigs
+      , interpObservers = M.fromList $
+          zip (fmap observerName (specObservers spec)) obsvs
+      }
+-}
+
+-- We could write this in a beautiful lazy style like above, but that creates a
+-- space leak in the interpreter that is hard to fix while maintaining laziness.
+-- We take a more brute-force appraoch below.
+eval :: ShowType -> Int -> ExtEnv -> Spec -> ExecTrace
+eval showType k exts spec =
+--  let exts  = take k $ reverse exts'                          in
+
+  let initStrms = map initStrm (specStreams spec)             in
+
+  let strms = evalStreams k exts (specStreams spec) initStrms in
+
+  let trigs = map (evalTrigger showType k exts strms) 
+                  (specTriggers spec)                         in
+
+  let obsvs = map (evalObserver showType k exts strms) 
+                  (specObservers spec)                        in 
+
+  strms `seq` ExecTrace
+                { interpTriggers  = M.fromList $
+                    zip (map triggerName  (specTriggers  spec)) trigs
+                , interpObservers = M.fromList $
+                    zip (map observerName (specObservers spec)) obsvs
+                }
+
+--------------------------------------------------------------------------------
+
+type LocalEnv = [(Name, Dynamic Type)]
+
+evalExpr_ :: Int -> Expr a -> ExtEnv -> LocalEnv -> Env Id -> a
+evalExpr_ k e0 exts locs strms = case e0 of
+  Const _ x              -> x 
+  Drop t i id            -> 
+    let Just xs = lookup id strms >>= fromDynF t in
+    reverse xs !! (fromIntegral i + k)
+  Local t1 _ name e1 e2 -> 
+    let x     = evalExpr_ k e1 exts locs strms in
+    let locs' = (name, toDyn t1 x) : locs  in
+    x `seq` locs' `seq` evalExpr_ k e2 exts locs' strms
+  Var t name                 -> fromJust $ lookup name locs >>= fromDyn t
+  ExternVar t name           -> evalExtern k t name (varEnv exts)
+  ExternFun t name _ _       -> evalFunc k t name exts
+  ExternArray _ t name idx _ -> evalArray k t name evalIdx (arrEnv exts)
+    where evalIdx = evalExpr_ k idx exts locs strms
+  Op1 op e1              -> 
+    let ev1 = evalExpr_ k e1 exts locs strms in 
+    let op1 = evalOp1 op                     in
+    ev1 `seq` op1 `seq` op1 ev1               
+  Op2 op e1 e2           -> 
+    let ev1 = evalExpr_ k e1 exts locs strms in 
+    let ev2 = evalExpr_ k e2 exts locs strms in 
+    let op2 = evalOp2 op                     in
+    ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2
+  Op3 op e1 e2 e3        -> 
+    let ev1 = evalExpr_ k e1 exts locs strms in 
+    let ev2 = evalExpr_ k e2 exts locs strms in 
+    let ev3 = evalExpr_ k e3 exts locs strms in 
+    let op3 = evalOp3 op                     in
+    ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3
+
+--------------------------------------------------------------------------------
+
+evalExtern :: Int -> Type a -> Name -> Env Name -> a
+evalExtern k t name exts = 
+  case lookup name exts of
+    Nothing -> badUsage $ "you need to supply a list of values for interpreting variable " ++ name
+    Just dyn ->
+      case fromDynF t dyn of
+        Nothing -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
+        Just xs -> xs !! k
+
+--------------------------------------------------------------------------------
+
+evalFunc :: Int -> Type a -> Name -> ExtEnv -> a
+evalFunc k t name exts  = 
+  case lookup name (funcEnv exts) of
+    Nothing -> 
+      badUsage $ "to simulate a spec containing the external function "
+                   ++ name ++ ", you need to include a stream to simulate it"
+
+    -- We created this spec in Interpreter.hs, copilot-language, so it should
+    -- contain no triggers and exactly one observer.
+    Just Spec { specStreams   = specStrms
+              , specObservers = obsLs }  -> 
+     let initStrms = map initStrm specStrms             in
+     let strms = evalStreams k exts specStrms initStrms in
+     case obsLs of
+       [Observer { observerExpr     = expr_
+                 , observerExprType = t1 }] -> 
+         let dyn = toDynF t1 expr_ in
+           case fromDynF t dyn of
+             Nothing    -> impossible "evalFunc" "copilot-core"
+             Just expr  -> evalExpr_ k expr exts [] strms
+       _ -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
+
+--------------------------------------------------------------------------------
+
+evalArray :: Integral b => Int -> Type a -> Name -> b -> ArrEnv -> a
+evalArray k t name idx exts =
+  case lookup name exts of
+    Nothing -> badUsage $ "you need to supply a list of finite lists " ++ 
+                 "for interpreting array " ++ name
+    Just dyn ->
+      case catMaybes $ map (fromDynF t) dyn of
+        [] -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."
+        xs -> let arr = (xs !! k) in
+              if length arr > fromIntegral idx
+                then arr !! fromIntegral idx
+                else badUsage $ "in the environment for array " ++ name ++ 
+                          ", you tried to index out of bounds"
+  
+--------------------------------------------------------------------------------
+
+evalOp1 :: Op1 a b -> (a -> b)
+evalOp1 op = case op of
+  Not        -> P.not
+  Abs _      -> P.abs
+  Sign _     -> P.signum
+  Recip _    -> P.recip
+  Exp _      -> P.exp
+  Sqrt _     -> P.sqrt
+  Log _      -> P.log
+  Sin _      -> P.sin
+  Tan _      -> P.tan
+  Cos _      -> P.cos
+  Asin _     -> P.asin
+  Atan _     -> P.atan
+  Acos _     -> P.acos
+  Sinh _     -> P.sinh
+  Tanh _     -> P.tanh
+  Cosh _     -> P.cosh
+  Asinh _    -> P.asinh
+  Atanh _    -> P.atanh
+  Acosh _    -> P.acosh
+  BwNot _    -> complement
+  Cast _ _   -> P.fromIntegral 
+
+--------------------------------------------------------------------------------
+
+evalOp2 :: Op2 a b c -> (a -> b -> c)
+evalOp2 op = case op of
+  And          -> (&&)
+  Or           -> (||)
+  Add _        -> (+)
+  Sub _        -> (-)
+  Mul _        -> (*)
+  Mod _        -> (catchZero P.mod)
+  Div _        -> (catchZero P.div)
+  Fdiv _       -> (P./)
+  Pow _        -> (P.**)
+  Logb _       -> P.logBase
+  Eq _         -> (==)
+  Ne _         -> (/=)
+  Le _         -> (<=)
+  Ge _         -> (>=)
+  Lt _         -> (<)
+  Gt _         -> (>)
+  BwAnd _      -> (.&.)
+  BwOr  _      -> (.|.)
+  BwXor _      -> (xor)
+  BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )
+  BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
+
+catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)
+catchZero _ _ 0 = badUsage "divide by zero"
+catchZero f x y = f x y
+
+--------------------------------------------------------------------------------
+
+evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
+evalOp3 (Mux _) = \ !v !x !y -> if v then x else y
+
+--------------------------------------------------------------------------------
+
+initStrm :: Stream -> (Id, DynamicF [] Type)
+initStrm Stream { streamId       = id
+                , streamBuffer   = buffer
+                , streamExprType = t } =
+  (id, toDynF t (reverse buffer))
+
+-- XXX actually only need to compute until shortest stream is of length k
+-- XXX this should just be a foldl' over [0,1..k]
+evalStreams :: Int -> ExtEnv -> [Stream] -> Env Id -> Env Id
+evalStreams top exts specStrms initStrms = 
+  evalStreams_ 0 initStrms 
+  where 
+  evalStreams_ :: Int -> Env Id -> Env Id
+  evalStreams_ k strms | k == top  = strms
+  evalStreams_ k strms | otherwise = 
+    evalStreams_ (k+1) $! strms_ 
+    where 
+    strms_ = map evalStream specStrms
+    evalStream Stream { streamId       = id
+                      , streamExpr     = e
+                      , streamExprType = t } =
+      let xs = fromJust $ lookup id strms >>= fromDynF t       in
+      let x  = evalExpr_ k e exts [] strms                     in
+      let ls = x `seq` (x:xs)                                  in
+      (id, toDynF t ls)
+
+--------------------------------------------------------------------------------
+
+evalTrigger :: 
+  ShowType -> Int -> ExtEnv -> Env Id -> Trigger -> [Maybe [Output]]
+evalTrigger showType k exts strms
+  Trigger
+    { triggerGuard = e
+    , triggerArgs  = args
+    } = take k $ map tag (zip bs vs) ++ repeat Nothing -- there might be 0 args!
+
+  where
+  tag :: (Bool, a) -> Maybe a
+  tag (True,  x) = Just x
+  tag (False, _) = Nothing
+
+  bs :: [Bool]
+  bs = evalExprs_ k e exts strms
+
+  vs :: [[Output]]
+  vs = transpose $ map evalUExpr args 
+
+  evalUExpr :: UExpr -> [Output]
+  evalUExpr (UExpr t e1) =
+    map (showWithType showType t) (evalExprs_ k e1 exts strms)
+
+--------------------------------------------------------------------------------
+evalObserver :: ShowType -> Int -> ExtEnv -> Env Id -> Observer -> [Output]
+evalObserver showType k exts strms
+  Observer
+    { observerExpr     = e
+    , observerExprType = t }
+  = map (showWithType showType t) (evalExprs_ k e exts strms)
+
+--------------------------------------------------------------------------------
+
+evalExprs_ :: Int -> Expr a -> ExtEnv -> Env Id -> [a]
+evalExprs_ k e exts strms = 
+  map (\i -> evalExpr_ i e exts [] strms) [0..(k-1)]
+                                       
diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Interpret/Render.hs
@@ -0,0 +1,95 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | An tagless interpreter for Copilot specifications.
+
+module Copilot.Core.Interpret.Render
+  ( renderAsTable
+  , renderAsCSV
+  ) where
+
+import Data.List (intersperse, transpose, foldl')
+import Data.Maybe (catMaybes)
+import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
+import qualified Data.Map as M
+import Text.PrettyPrint.NCol (asColumns)
+import Text.PrettyPrint (Doc, ($$), (<>), text, render, empty)
+
+--------------------------------------------------------------------------------
+
+renderAsTable :: ExecTrace -> String
+renderAsTable
+  ExecTrace
+    { interpTriggers  = trigs
+    , interpObservers = obsvs } =
+  ( render
+  . asColumns
+  . transpose
+  . (:) (ppTriggerNames ++ ppObserverNames)
+  . transpose
+  ) (ppTriggerOutputs ++ ppObserverOutputs)
+
+  where
+
+  ppTriggerNames :: [Doc]
+  ppTriggerNames  = map (text . (++ ":")) (M.keys trigs)
+
+  ppObserverNames :: [Doc]
+  ppObserverNames = map (text . (++ ":")) (M.keys obsvs)
+
+  ppTriggerOutputs :: [[Doc]]
+  ppTriggerOutputs = map (map ppTriggerOutput) (M.elems trigs)
+
+  ppTriggerOutput :: Maybe [Output] -> Doc
+  ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
+  ppTriggerOutput Nothing   = text "--"
+
+  ppObserverOutputs :: [[Doc]]
+  ppObserverOutputs = map (map text) (M.elems obsvs)
+
+--------------------------------------------------------------------------------
+
+renderAsCSV :: ExecTrace -> String
+renderAsCSV = render . unfold
+
+unfold :: ExecTrace -> Doc
+unfold r =
+  case step r of
+    (cs, Nothing) -> cs
+    (cs, Just r') -> cs $$ unfold r'
+
+step :: ExecTrace -> (Doc, Maybe ExecTrace)
+step ExecTrace
+       { interpTriggers  = trigs
+       } = 
+  if M.null trigs then (empty, Nothing)
+    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
+
+  where
+
+  ppTriggerOutputs :: [Doc]
+  ppTriggerOutputs =
+      catMaybes 
+    . fmap ppTriggerOutput 
+    . M.assocs 
+    . fmap head 
+    $ trigs
+
+  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
+  ppTriggerOutput (_,  Nothing) = Nothing
+  ppTriggerOutput (cs, Just xs) = Just $
+    text cs <> text "," <>
+      (foldr (<>) empty . map text . intersperse ",") xs
+
+  tails :: Maybe ExecTrace
+  tails =
+    if any null (M.elems (fmap tail trigs))
+      then Nothing
+      else Just
+        ExecTrace
+          { interpTriggers  = fmap tail trigs
+          , interpObservers = M.empty
+          }
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/MakeTags.hs
@@ -0,0 +1,112 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Sets a unique tags for each external array/function call.
+
+module Copilot.Core.MakeTags (makeTags) where
+
+import Copilot.Core.Expr
+import Copilot.Core.Spec
+import Control.Monad.State
+import Prelude hiding (id)
+
+next :: State Int Int
+next =
+  do
+    k <- get
+    put (succ k)
+    return k
+
+makeTags :: Spec -> Spec
+makeTags spec = evalState (mkTagsSpec spec) 0
+
+mkTagsSpec :: Spec -> State Int Spec
+mkTagsSpec
+  Spec
+    { specStreams   = strms
+    , specObservers = obsvs
+    , specTriggers  = trigs
+    } =
+  liftM3 Spec
+    (mkTagsStrms strms)
+    (mkTagsObsvs obsvs)
+    (mkTagsTrigs trigs)
+
+mkTagsStrms :: [Stream] -> State Int [Stream]
+mkTagsStrms = mapM mkTagsStrm
+
+  where
+
+    mkTagsStrm Stream
+      { streamId         = id
+      , streamBuffer     = xs
+      , streamGuard      = g
+      , streamExpr       = e
+      , streamExprType   = t } =
+        do
+          e' <- mkTagsExpr e
+          return $ Stream
+            { streamId         = id
+            , streamBuffer     = xs
+            , streamGuard      = g
+            , streamExpr       = e'
+            , streamExprType   = t }
+
+mkTagsObsvs :: [Observer] -> State Int [Observer]
+mkTagsObsvs = mapM mkTagsObsv
+
+  where
+
+    mkTagsObsv Observer
+      { observerName     = name
+      , observerExpr     = e
+      , observerExprType = t } =
+        do
+          e' <- mkTagsExpr e
+          return $ Observer
+            { observerName     = name
+            , observerExpr     = e'
+            , observerExprType = t }
+
+mkTagsTrigs :: [Trigger] -> State Int [Trigger]
+mkTagsTrigs = mapM mkTagsTrig
+
+ where
+
+   mkTagsTrig Trigger
+     { triggerName      = name
+     , triggerGuard     = g
+     , triggerArgs      = args } =
+       do
+         g' <- mkTagsExpr g
+         args' <- mapM mkTagsUExpr args
+         return $ Trigger
+           { triggerName      = name
+           , triggerGuard     = g'
+           , triggerArgs      = args' }
+
+mkTagsUExpr :: UExpr -> State Int UExpr
+mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } =
+  do
+    e' <- mkTagsExpr e
+    return $ UExpr { uExprExpr = e', uExprType = t }
+
+mkTagsExpr :: Expr a -> State Int (Expr a)
+mkTagsExpr e0 = case e0 of
+  Const t x                     -> return $ Const t x
+  Drop t k id                   -> return $ Drop t k id
+  Local t1 t2 name e1 e2        -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)
+  Var t name                    -> return $ Var t name
+  ExternVar t name              -> return $ ExternVar t name
+  ExternFun t name args _       -> do
+                                     args' <- mapM mkTagsUExpr args
+                                     k <- next
+                                     return $ ExternFun t name args' (Just k)
+  ExternArray t1 t2 name idx _  -> do
+                                     idx' <- mkTagsExpr idx
+                                     k <- next
+                                     return $ ExternArray t1 t2 name idx' (Just k)
+  Op1 op e                      -> liftM  (Op1 op) (mkTagsExpr e)
+  Op2 op e1 e2                  -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2)
+  Op3 op e1 e2 e3               -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3)
diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Operators.hs
@@ -0,0 +1,83 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs, Rank2Types #-}
+
+module Copilot.Core.Operators
+  ( Op1 (..)
+  , Op2 (..)
+  , Op3 (..)
+  ) where
+
+import Copilot.Core.Type (Type)
+import Data.Bits
+
+--------------------------------------------------------------------------------
+
+-- Unary operators.
+data Op1 a b where
+  -- Boolean operators.
+  Not      :: Op1 Bool Bool
+  -- Numeric operators.
+  Abs      :: Num a => Type a -> Op1 a a
+  Sign     :: Num a => Type a -> Op1 a a
+  -- Fractional operators.
+  Recip    :: Fractional a => Type a -> Op1 a a
+  -- Floating operators.
+  Exp      :: Floating a => Type a -> Op1 a a
+  Sqrt     :: Floating a => Type a -> Op1 a a
+  Log      :: Floating a => Type a -> Op1 a a
+  Sin      :: Floating a => Type a -> Op1 a a
+  Tan      :: Floating a => Type a -> Op1 a a
+  Cos      :: Floating a => Type a -> Op1 a a
+  Asin     :: Floating a => Type a -> Op1 a a
+  Atan     :: Floating a => Type a -> Op1 a a
+  Acos     :: Floating a => Type a -> Op1 a a
+  Sinh     :: Floating a => Type a -> Op1 a a
+  Tanh     :: Floating a => Type a -> Op1 a a
+  Cosh     :: Floating a => Type a -> Op1 a a
+  Asinh    :: Floating a => Type a -> Op1 a a
+  Atanh    :: Floating a => Type a -> Op1 a a
+  Acosh    :: Floating a => Type a -> Op1 a a
+  -- Bitwise operators.
+  BwNot    :: Bits     a => Type a -> Op1 a a
+  -- Casting operaators.
+  Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b
+
+-- | Binary operators.
+data Op2 a b c where
+  -- Boolean operators.
+  And      :: Op2 Bool Bool Bool
+  Or       :: Op2 Bool Bool Bool
+  -- Numeric operators.
+  Add      :: Num a => Type a -> Op2 a a a
+  Sub      :: Num a => Type a -> Op2 a a a
+  Mul      :: Num a => Type a -> Op2 a a a
+  -- Integral operators.
+  Mod      :: Integral a => Type a -> Op2 a a a
+  Div      :: Integral a => Type a -> Op2 a a a
+  -- Fractional operators.
+  Fdiv     :: Fractional a => Type a -> Op2 a a a
+  -- Floating operators.
+  Pow      :: Floating a => Type a -> Op2 a a a
+  Logb     :: Floating a => Type a -> Op2 a a a
+  -- Equality operators.
+  Eq       :: Eq a => Type a -> Op2 a a Bool
+  Ne       :: Eq a => Type a -> Op2 a a Bool
+  -- Relational operators.
+  Le       :: Ord a => Type a -> Op2 a a Bool
+  Ge       :: Ord a => Type a -> Op2 a a Bool
+  Lt       :: Ord a => Type a -> Op2 a a Bool
+  Gt       :: Ord a => Type a -> Op2 a a Bool
+  -- Bitwise operators.
+  BwAnd    :: Bits a => Type a -> Op2 a a a
+  BwOr     :: Bits a => Type a -> Op2 a a a
+  BwXor    :: Bits a => Type a -> Op2 a a a
+  BwShiftL :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a
+  BwShiftR :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a
+
+-- | Ternary operators.
+data Op3 a b c d where
+  -- Conditional operator:
+  Mux   :: Type a -> Op3 Bool a a a
diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/PrettyPrint.hs
@@ -0,0 +1,174 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | A pretty printer for Copilot specifications.
+
+{-# LANGUAGE GADTs #-}
+
+module Copilot.Core.PrettyPrint
+  ( prettyPrint
+  ) where
+
+import Copilot.Core
+import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
+import Prelude hiding (id)
+import Text.PrettyPrint.HughesPJ
+import Data.List (intersperse)
+
+--------------------------------------------------------------------------------
+
+strmName :: Int -> Doc
+strmName id = text "s" <> int id
+
+--------------------------------------------------------------------------------
+
+ppExpr :: Expr a -> Doc
+ppExpr e0 = case e0 of
+  Const t x                  -> text (showWithType Haskell t x)
+  Drop _ 0 id                -> strmName id
+  Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id
+  ExternVar _ name           -> text "extern" <+> doubleQuotes (text name)
+  ExternFun _ name args _    -> 
+    text "extern" <+> doubleQuotes 
+      (text name <> lparen <> 
+         hcat (punctuate (comma <> space) (map ppUExpr args))
+       <> rparen)
+  ExternArray _ _ name idx _ -> text "extern" <+> doubleQuotes (text name <> lbrack 
+                                  <> ppExpr idx <> rbrack)
+  Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals
+                                          <+> ppExpr e1 $$ text "in" <+> ppExpr e2
+  Var _ name                 -> text "var" <+> doubleQuotes (text name)
+  Op1 op e                   -> ppOp1 op (ppExpr e)
+  Op2 op e1 e2               -> ppOp2 op (ppExpr e1) (ppExpr e2)
+  Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)
+
+ppUExpr :: UExpr -> Doc
+ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0
+
+ppOp1 :: Op1 a b -> Doc -> Doc
+ppOp1 op = case op of
+  Not      -> ppPrefix "not"
+  Abs _    -> ppPrefix "abs"
+  Sign _   -> ppPrefix "signum"
+  Recip _  -> ppPrefix "recip"
+  Exp _    -> ppPrefix "exp"
+  Sqrt _   -> ppPrefix "sqrt"
+  Log _    -> ppPrefix "log"
+  Sin _    -> ppPrefix "sin"
+  Tan _    -> ppPrefix "tan"
+  Cos _    -> ppPrefix "cos"
+  Asin _   -> ppPrefix "asin"
+  Atan _   -> ppPrefix "atan"
+  Acos _   -> ppPrefix "acos"
+  Sinh _   -> ppPrefix "sinh"
+  Tanh _   -> ppPrefix "tanh"
+  Cosh _   -> ppPrefix "cosh"
+  Asinh _  -> ppPrefix "asinh"
+  Atanh _  -> ppPrefix "atanh"
+  Acosh _  -> ppPrefix "acosh"
+  BwNot _  -> ppPrefix "~"
+  Cast _ _ -> ppPrefix "(cast)"
+
+ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc
+ppOp2 op = case op of
+  And          -> ppInfix "&&"
+  Or           -> ppInfix "||"
+  Add      _   -> ppInfix "+"
+  Sub      _   -> ppInfix "-"
+  Mul      _   -> ppInfix "*"
+  Div      _   -> ppInfix "div"
+  Mod      _   -> ppInfix "mod"
+  Fdiv     _   -> ppInfix "/"
+  Pow      _   -> ppInfix "**"
+  Logb     _   -> ppInfix "logBase"
+  Eq       _   -> ppInfix "=="
+  Ne       _   -> ppInfix "/="
+  Le       _   -> ppInfix "<="
+  Ge       _   -> ppInfix ">="
+  Lt       _   -> ppInfix "<"
+  Gt       _   -> ppInfix ">"
+  BwAnd    _   -> ppInfix "&"
+  BwOr     _   -> ppInfix "|"
+  BwXor    _   -> ppInfix "^"
+  BwShiftL _ _ -> ppInfix "<<"
+  BwShiftR _ _ -> ppInfix ">>"
+
+ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc
+ppOp3 op = case op of
+  Mux _    -> \ doc1 doc2 doc3 ->
+    text "(if"   <+> doc1 <+>
+    text "then" <+> doc2 <+>
+    text "else" <+> doc3 <> text ")"
+
+--------------------------------------------------------------------------------
+  
+ppInfix :: String -> Doc -> Doc -> Doc
+ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2
+
+ppPrefix :: String -> Doc -> Doc
+ppPrefix cs = (text cs <+>)
+
+--------------------------------------------------------------------------------
+
+ppStream :: Stream -> Doc
+ppStream
+  Stream
+    { streamId       = id
+    , streamBuffer   = buffer
+    , streamExpr     = e
+    , streamExprType = t
+    }
+      = (parens . text . showType) t
+          <+> strmName id 
+    <+> text "="
+    <+> text ("["
+              ++ ( concat $ intersperse "," 
+                              $ map (showWithType Haskell t) buffer )
+              ++ "]")
+    <+> text "++"
+    <+> ppExpr e
+
+--------------------------------------------------------------------------------
+
+ppTrigger :: Trigger -> Doc
+ppTrigger
+  Trigger
+    { triggerName  = name
+    , triggerGuard = e
+    , triggerArgs  = args }
+  =   text "trigger" <+> text "\"" <> text name <> text "\""
+  <+> text "="
+  <+> ppExpr e
+  <+> lbrack
+  $$  (nest 2 $ vcat (punctuate comma $ 
+                          map (\a -> text "arg" <+> ppUExpr a) args))
+  $$  nest 2 rbrack
+
+--------------------------------------------------------------------------------
+
+ppObserver :: Observer -> Doc
+ppObserver
+  Observer
+    { observerName     = name
+    , observerExpr     = e }
+  =   text "observer \"" <> text name <> text "\""
+  <+> text "="
+  <+> ppExpr e
+
+--------------------------------------------------------------------------------
+
+ppSpec :: Spec -> Doc
+ppSpec spec = cs $$ ds $$ es
+  where
+    cs = foldr (($$) . ppStream)   empty (specStreams   spec)
+    ds = foldr (($$) . ppTrigger)  empty (specTriggers  spec)
+    es = foldr (($$) . ppObserver) empty (specObservers spec)
+
+--------------------------------------------------------------------------------
+
+-- | Pretty-prints a Copilot specification.
+prettyPrint :: Spec -> String
+prettyPrint = render . ppSpec
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Random.hs b/src/Copilot/Core/Random.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Random.hs
@@ -0,0 +1,311 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module Copilot.Core.Random
+  ( randomSpec
+  ) where
+
+import Control.Monad
+import Copilot.Core (UExpr (..))
+import qualified Copilot.Core as E
+import Copilot.Core.Spec
+import Copilot.Core.Random.Gen
+import Copilot.Core.Random.Weights
+import Copilot.Core.Type
+import Copilot.Core.Type.Equality
+import Data.Int
+import Data.Word
+import Prelude hiding (id)
+import System.Random (StdGen)
+
+--------------------------------------------------------------------------------
+
+randomSpec :: Weights -> StdGen -> Spec
+randomSpec = runGen genSpec 0
+
+--------------------------------------------------------------------------------
+
+genSpec :: Gen Spec
+genSpec =
+  do
+    ws <- weights
+    numTriggers <- choose (1, maxTriggers ws)
+    ss <- genStreamInfo's
+    streams  <- mapM (genStream ss) ss
+    triggers <- mapM (genTrigger ss) (map mkTriggerName [0..numTriggers-1])
+    return
+      Spec
+        { specStreams   = streams
+        , specObservers = []
+        , specTriggers  = triggers }
+
+  where
+
+  mkTriggerName :: Int -> E.Name
+  mkTriggerName k = "f" ++ show k
+
+--------------------------------------------------------------------------------
+
+data StreamInfo = forall a . (Eq a, Ord a) => StreamInfo
+  { streamInfoId         :: E.Id
+  , streamInfoType       :: Type a
+  , streamInfoBufferSize :: Int }
+
+--------------------------------------------------------------------------------
+
+data WrapType = forall a . (Eq a, Ord a) => WrapType (Type a)
+
+genType :: Weights -> Gen WrapType
+genType ws = freq
+  [ (boolFreq   ws, return $ WrapType (typeOf :: Type Bool  ))
+  , (int8Freq   ws, return $ WrapType (typeOf :: Type Int8  ))
+  , (int16Freq  ws, return $ WrapType (typeOf :: Type Int16 ))
+  , (int32Freq  ws, return $ WrapType (typeOf :: Type Int32 ))
+  , (int64Freq  ws, return $ WrapType (typeOf :: Type Int64 ))
+  , (word8Freq  ws, return $ WrapType (typeOf :: Type Word8 ))
+  , (word16Freq ws, return $ WrapType (typeOf :: Type Word16))
+  , (word32Freq ws, return $ WrapType (typeOf :: Type Word32))
+  , (word64Freq ws, return $ WrapType (typeOf :: Type Word64))
+  , (floatFreq  ws, return $ WrapType (typeOf :: Type Float ))
+  , (floatFreq  ws, return $ WrapType (typeOf :: Type Double)) ]
+
+genTypeFromStreamInfo's :: [StreamInfo] -> Gen WrapType
+genTypeFromStreamInfo's = elements . map (\ (StreamInfo _ t _) -> WrapType t)
+
+--------------------------------------------------------------------------------
+
+genStreamInfo's :: Gen [StreamInfo]
+genStreamInfo's =
+  do
+    let
+      s0 = StreamInfo 0 (typeOf :: Type Bool) 1
+    ws <- weights
+    ss <- mapM genStreamInfo [1 .. numStreams ws - 1]
+    return (s0 : ss)
+
+  where
+  genStreamInfo :: Int -> Gen StreamInfo
+  genStreamInfo id =
+    do
+      ws <- weights
+      k  <- choose (1, maxBuffSize ws)
+      WrapType t <- genType ws
+      return
+        StreamInfo
+          { streamInfoId         = id
+          , streamInfoType       = t
+          , streamInfoBufferSize = k }
+
+--------------------------------------------------------------------------------
+
+genStream :: [StreamInfo] -> StreamInfo -> Gen Stream
+genStream ss
+  StreamInfo
+    { streamInfoId         = id
+    , streamInfoType       = t
+    , streamInfoBufferSize = k } =
+  do
+    xs <- replicateM k (randomFromType t)
+    w  <- genExpr ss t
+    return
+      Stream
+        { streamId       = id
+        , streamBuffer   = xs
+        , streamGuard    = E.Const (typeOf :: Type Bool) True
+        , streamExpr     = w
+        , streamExprType = t }
+
+--------------------------------------------------------------------------------
+
+genTrigger :: [StreamInfo] -> E.Name -> Gen Trigger
+genTrigger ss name =
+  do
+    w  <- genExpr ss (typeOf :: Type Bool)
+    ws <- weights
+    i  <- choose (1, maxTrigArgs ws)
+    args <- replicateM i genArg
+    return
+      Trigger
+        { triggerName  = name
+        , triggerGuard = w
+        , triggerArgs  = args }
+
+  where
+
+  genArg :: Gen UExpr
+  genArg =
+    do
+      WrapType t <- genTypeFromStreamInfo's ss
+      w <- genExpr ss t
+      return
+        UExpr
+          { uExprExpr = w
+          , uExprType = t }
+
+--------------------------------------------------------------------------------
+
+genExpr :: [StreamInfo] -> Type a -> Gen (E.Expr a)
+genExpr ss t =
+  do
+    dp <- depth
+    ws <- weights
+    if dp >= maxExprDepth ws
+      then freq
+        [ (constFreq ws, genConst)
+        , (dropFreq  ws, genDrop) ]
+      else freq
+        [ (constFreq ws, genConst)
+        , (dropFreq  ws, genDrop)
+        , (op1Freq   ws, genOp1)
+        , (op2Freq   ws, genOp2)
+        , (op3Freq   ws, genOp3) ]
+
+  where
+  genConst =
+    do
+      x <- randomFromType t
+      return $ E.Const t x
+  genDrop =
+    do
+      s <- findStreamInfoWithMatchingType
+      k <- choose (0, streamInfoBufferSize s - 1)
+      return $ E.Drop t (fromIntegral k) (streamInfoId s)
+
+    where
+    findStreamInfoWithMatchingType =
+      let
+        p (StreamInfo _ t1 _) =
+          case t =~= t1 of
+            Just _ -> True
+            _      -> False
+      in
+        elements (filter p ss)
+
+  genOp1 = incDepth $ case t of
+    Bool   -> genOp1Bool ss
+    Int8   -> genOp1Num  ss t
+    Int16  -> genOp1Num  ss t
+    Int32  -> genOp1Num  ss t
+    Int64  -> genOp1Num  ss t
+    Word8  -> genOp1Num  ss t
+    Word16 -> genOp1Num  ss t
+    Word32 -> genOp1Num  ss t
+    Word64 -> genOp1Num  ss t
+    Float  -> genOp1Num  ss t
+    Double -> genOp1Num  ss t
+
+  genOp2 = incDepth $ case t of
+-- XXX 
+--    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss, genOp2Ord ss]
+    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss]
+    Int8    -> intOrWord NumWit IntegralWit
+    Int16   -> intOrWord NumWit IntegralWit
+    Int32   -> intOrWord NumWit IntegralWit
+    Int64   -> intOrWord NumWit IntegralWit
+    Word8   -> intOrWord NumWit IntegralWit
+    Word16  -> intOrWord NumWit IntegralWit
+    Word32  -> intOrWord NumWit IntegralWit
+    Word64  -> intOrWord NumWit IntegralWit
+    Float   -> floatOrDouble NumWit
+    Double  -> floatOrDouble NumWit
+
+    where
+
+      intOrWord numWit integralWit = do 
+        ws <- weights 
+        if divModFreq ws 
+          then oneOf $ num ++ [genOp2Integral ss t integralWit ]
+          else oneOf num
+        where num = [ genOp2Num ss t numWit ]
+
+      floatOrDouble numWit = oneOf
+        [ genOp2Num ss t numWit ]
+
+  genOp3 = incDepth (genOp3Mux ss t)
+
+--------------------------------------------------------------------------------
+
+genOp1Bool :: [StreamInfo] -> Gen (E.Expr Bool)
+genOp1Bool ss =
+  do
+    ew <- genExpr ss (typeOf :: Type Bool)
+    return $ E.Op1 E.Not ew
+
+genOp1Num :: Num a => [StreamInfo] -> Type a -> Gen (E.Expr a)
+genOp1Num ss t =
+  do
+    ew  <- genExpr ss t
+    opw <- elements [E.Abs t, E.Sign t]
+    return $ E.Op1 opw ew
+
+genOp2Bool :: [StreamInfo] -> Gen (E.Expr Bool)
+genOp2Bool ss =
+  do
+    ew1 <- genExpr ss (typeOf :: Type Bool)
+    ew2 <- genExpr ss (typeOf :: Type Bool)
+    opw <- elements [E.And, E.Or]
+    return $ E.Op2 opw ew1 ew2
+
+genOp2Eq :: [StreamInfo] -> Gen (E.Expr Bool)
+genOp2Eq ss =
+  do
+    WrapType t <- genTypeFromStreamInfo's ss
+    ew1 <- genExpr ss t
+    ew2 <- genExpr ss t
+    opw <- elements [E.Eq t, E.Ne t]
+    return $ E.Op2 opw ew1 ew2
+
+-- XXX
+-- Figure out how to ensure t comes from a Numeric Class
+-- genOp2Ord :: [StreamInfo] -> Gen (E.Expr Bool)
+-- genOp2Ord ss =
+--   do
+--     WrapType t <- genTypeFromStreamInfo's ss
+--     ew1 <- genExpr ss t
+--     ew2 <- genExpr ss t
+--     opw <- elements
+--       [ (E.Lt t)
+--       , (E.Gt t)
+--       , (E.Le t)
+--       , (E.Ge t) ]
+--     return $ E.Op2 opw ew1 ew2
+
+genOp2Num :: [StreamInfo] -> Type a -> NumWit a -> Gen (E.Expr a)
+genOp2Num ss t NumWit =
+  do
+    ew1 <- genExpr ss t
+    ew2 <- genExpr ss t
+    opw <-
+      elements
+        [ (E.Add t)
+        , (E.Sub t)
+        , (E.Mul t) ]
+    return
+      $ E.Op2 opw ew1 ew2
+
+genOp2Integral :: [StreamInfo] -> Type a -> IntegralWit a -> Gen (E.Expr a)
+genOp2Integral ss t IntegralWit =
+  do
+    ew1 <- genExpr ss t
+    ew2 <- genExpr ss t
+    opw <-
+      elements
+        [ (E.Div t)
+        , (E.Mod t) ]
+    return
+      $ E.Op2 opw ew1 ew2
+
+genOp3Mux :: [StreamInfo] -> Type a -> Gen (E.Expr a)
+genOp3Mux ss t =
+  do
+    ew1 <- genExpr ss (typeOf :: Type Bool)
+    ew2 <- genExpr ss t
+    ew3 <- genExpr ss t
+    return $ E.Op3 (E.Mux t) ew1 ew2 ew3
+
+data NumWit a = Num a => NumWit
+
+data IntegralWit a = Integral a => IntegralWit
diff --git a/src/Copilot/Core/Random/Gen.hs b/src/Copilot/Core/Random/Gen.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Random/Gen.hs
@@ -0,0 +1,127 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module Copilot.Core.Random.Gen
+  ( Gen
+  , runGen
+  , randomFromType
+  , oneOf
+  , freq
+  , choose
+  , elements
+  , depth
+  , weights
+  , incDepth
+  ) where
+
+import Copilot.Core.Random.Weights
+import Copilot.Core.Error
+import Copilot.Core.Type
+import System.Random (StdGen, Random, random, randomR, split)
+
+--------------------------------------------------------------------------------
+
+-- | @runGen@ takes a @Gen a@, a max depth of the expression, the weights, and
+-- the standard random generator.
+newtype Gen a = MkGen { runGen :: Depth -> Weights -> StdGen -> a }
+
+--------------------------------------------------------------------------------
+
+instance Functor Gen where
+  fmap f (MkGen h) = MkGen (\ d ws r -> f (h d ws r))
+
+instance Monad Gen where
+  return x = MkGen (\ _ _ _ -> x)
+
+  MkGen m >>= k = MkGen $ \ d ws r ->
+    let (r1, r2) = split r       in
+    let MkGen m' = k (m d ws r1) in
+    m' d ws r2
+
+--------------------------------------------------------------------------------
+
+stdGen :: Gen StdGen
+stdGen = MkGen $ \ _ _ g -> g
+
+depth :: Gen Depth
+depth = MkGen $ \ d _ _ -> d
+
+weights :: Gen Weights
+weights = MkGen $ \ _ ws _ -> ws
+
+incDepth :: Gen a -> Gen a
+incDepth gen = MkGen $ \ d ws g -> runGen gen (succ d) ws g
+
+--------------------------------------------------------------------------------
+
+randomFromType :: Type a -> Gen a
+randomFromType t =
+  case t of
+    Bool   -> genBool
+    Int8   -> genBoundedIntegral
+    Int16  -> genBoundedIntegral
+    Int32  -> genBoundedIntegral
+    Int64  -> genBoundedIntegral
+    Word8  -> genBoundedIntegral
+    Word16 -> genBoundedIntegral
+    Word32 -> genBoundedIntegral
+    Word64 -> genBoundedIntegral
+    Float  -> genFractional
+    Double -> genFractional
+
+  where
+
+  genBool :: Gen Bool
+  genBool =
+    do
+      g <- stdGen
+      return $ fst (random g)
+
+  genBoundedIntegral :: (Bounded a, Integral a) => Gen a
+  genBoundedIntegral =
+    do let mn = minBound
+           mx = maxBound `asTypeOf` mn
+       n <- choose (toInteger mn, toInteger mx)
+       return (fromInteger n `asTypeOf` mn)
+
+  genFractional :: (Random a, Fractional a) => Gen a
+  genFractional =
+    do
+      g <- stdGen
+      return $ fst (random g)
+
+--------------------------------------------------------------------------------
+
+choose :: Random a => (a, a) -> Gen a
+choose rng =
+  do
+    g <- stdGen
+    return $ fst (randomR rng g)
+
+oneOf :: [Gen a] -> Gen a
+oneOf [] = impossible "oneof" "copilot-core" 
+oneOf gs = choose (0,length gs - 1) >>= (gs !!)
+
+-- | Takes a list of pairs (weight, Gen), and choose the Gen based on the
+-- weights.  To get the frequency of choosing a Gen, sum up all the weights, and
+-- choose c between 1 and the total.  Now recurse down the list, choosing an
+-- item only when c <= weight.  If not, subtract the current weight from c.
+freq :: [(Int, Gen a)] -> Gen a
+freq [] = impossible "feq" "copilot-core" 
+freq xs0 = choose (1, tot) >>= (`pick` xs0)
+
+ where
+  tot = sum (map fst xs0)
+  pick n ((k,x):xs)
+    | n <= k    = x
+    | otherwise = pick (n-k) xs
+  pick _ _  = impossible "pick" "copilot-core" 
+
+elements :: [a] -> Gen a
+elements [] = impossible "elements" "copilot-core" 
+elements xs = (xs !!) `fmap` choose (0, length xs - 1)
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Random/Weights.hs b/src/Copilot/Core/Random/Weights.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Random/Weights.hs
@@ -0,0 +1,69 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+module Copilot.Core.Random.Weights
+  ( Depth
+  , Weights (..)
+  , simpleWeights ) where
+
+type Depth = Int
+
+data Weights = Weights
+  { maxExprDepth :: Int
+  , maxBuffSize  :: Int
+  , maxTriggers  :: Int
+  , maxTrigArgs  :: Int
+  , maxObservers :: Int
+  , numStreams   :: Int
+  -- Expression frequencies:
+  , constFreq    :: Int
+  , drop0Freq    :: Int
+  , dropFreq     :: Int
+  , externFreq   :: Int
+  , op1Freq      :: Int
+  , op2Freq      :: Int
+  , op3Freq      :: Int
+  -- Type frequencies:
+  , boolFreq     :: Int
+  , int8Freq     :: Int
+  , int16Freq    :: Int
+  , int32Freq    :: Int
+  , int64Freq    :: Int
+  , word8Freq    :: Int
+  , word16Freq   :: Int
+  , word32Freq   :: Int
+  , word64Freq   :: Int
+  , floatFreq    :: Int
+  , doubleFreq   :: Int 
+  , divModFreq   :: Bool }
+
+simpleWeights :: Weights
+simpleWeights = Weights 
+  { maxExprDepth = 10
+  , maxBuffSize  = 8
+  , maxTriggers  = 5
+  , maxTrigArgs  = 5
+  , maxObservers = 8
+  , numStreams   = 10
+  -- Expression frequencies:
+  , constFreq    = 1
+  , drop0Freq    = 1
+  , dropFreq     = 1
+  , externFreq   = 1
+  , op1Freq      = 1
+  , op2Freq      = 1
+  , op3Freq      = 1
+  -- Type frequencies:
+  , boolFreq     = 1
+  , int8Freq     = 1
+  , int16Freq    = 1
+  , int32Freq    = 1
+  , int64Freq    = 1
+  , word8Freq    = 1
+  , word16Freq   = 1
+  , word32Freq   = 1
+  , word64Freq   = 1
+  , floatFreq    = 1
+  , doubleFreq   = 1 
+  , divModFreq   = True }
diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Spec.hs
@@ -0,0 +1,53 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification, GADTs #-}
+
+module Copilot.Core.Spec
+  ( Stream (..)
+  , Observer (..)
+  , Trigger (..)
+  , Spec (..)
+  ) where
+
+import Copilot.Core.Expr (Name, Id, Expr, UExpr)
+import Copilot.Core.Type (Type)
+
+--------------------------------------------------------------------------------
+
+-- | A stream.
+data Stream = forall a  . Stream
+  { streamId         :: Id
+  , streamBuffer     :: [a]
+  , streamGuard      :: Expr Bool
+  , streamExpr       :: Expr a
+  , streamExprType   :: Type a }
+
+--------------------------------------------------------------------------------
+
+-- | An observer.
+data Observer = forall a . Observer
+  { observerName     :: Name
+  , observerExpr     :: Expr a
+  , observerExprType :: Type a }
+
+--------------------------------------------------------------------------------
+
+-- | A trigger.
+data Trigger = Trigger
+  { triggerName      :: Name
+  , triggerGuard     :: Expr Bool
+  , triggerArgs      :: [UExpr] }
+
+--------------------------------------------------------------------------------
+
+-- | A Copilot specification consists of a list of variables bound to anonymous
+-- streams, a lost of anomymous streams, a list of observers, and a list of
+-- triggers.
+data Spec = Spec
+  { specStreams      :: [Stream]
+  , specObservers    :: [Observer]
+  , specTriggers     :: [Trigger] }
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Spec/Locals.hs b/src/Copilot/Core/Spec/Locals.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Spec/Locals.hs
@@ -0,0 +1,86 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification #-}
+
+-- |
+
+module Copilot.Core.Spec.Locals
+  ( Loc (..)
+  , locals
+  ) where
+
+import Copilot.Core
+import Data.DList (DList, empty, singleton, append, concat, toList)
+import Data.List (nubBy)
+import Prelude hiding (concat, foldr)
+
+--------------------------------------------------------------------------------
+
+data Loc = forall a . Loc
+  { localName :: Name
+  , localType :: Type a }
+
+instance Show Loc where
+  show Loc { localName = name } = name
+
+--------------------------------------------------------------------------------
+
+locals :: Spec -> [Loc]
+locals
+  Spec
+    { specStreams   = streams
+    , specTriggers  = triggers
+    , specObservers = observers
+    } = nubBy eqLoc . toList $
+          concat (fmap locsStream   streams)  `append`
+          concat (fmap locsTrigger  triggers) `append`
+          concat (fmap locsObserver observers)
+
+  where
+
+  eqLoc :: Loc -> Loc -> Bool
+  eqLoc Loc { localName = name1 } Loc { localName = name2 } =
+    name1 == name2
+
+--------------------------------------------------------------------------------
+
+locsStream :: Stream -> DList Loc
+locsStream Stream { streamExpr = e } = locsExpr e
+
+--------------------------------------------------------------------------------
+
+locsTrigger :: Trigger -> DList Loc
+locsTrigger Trigger { triggerGuard = e, triggerArgs = args } =
+  locsExpr e `append` concat (fmap locsUExpr args)
+
+  where
+
+  locsUExpr :: UExpr -> DList Loc
+  locsUExpr (UExpr _ e1) = locsExpr e1
+
+--------------------------------------------------------------------------------
+
+locsObserver :: Observer -> DList Loc
+locsObserver Observer { observerExpr = e } = locsExpr e
+
+--------------------------------------------------------------------------------
+
+locsExpr :: Expr a -> DList Loc
+locsExpr e0 = case e0 of
+  Const  _ _             -> empty
+  Drop   _ _ _           -> empty
+  Local t _ name e1 e2   -> singleton (Loc name t)
+                                        `append` locsExpr e1
+                                        `append` locsExpr e2
+  Var _ _                -> empty
+  ExternVar _ _          -> empty
+  ExternFun _ _ _ _      -> empty
+  ExternArray _ _ _ _ _  -> empty
+  Op1 _ e                -> locsExpr e
+  Op2 _ e1 e2            -> locsExpr e1 `append` locsExpr e2
+  Op3 _ e1 e2 e3         -> locsExpr e1 `append` locsExpr e2
+                                        `append` locsExpr e3
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type.hs
@@ -0,0 +1,64 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | 
+
+{-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-}
+
+module Copilot.Core.Type
+  ( Type (..)
+  , Typed (..)
+  , UType (..)
+  ) where
+
+import Data.Int
+import Data.Word
+import Copilot.Core.Type.Equality
+
+data Type :: * -> * where
+  Bool    :: Type Bool
+  Int8    :: Type Int8
+  Int16   :: Type Int16
+  Int32   :: Type Int32
+  Int64   :: Type Int64
+  Word8   :: Type Word8
+  Word16  :: Type Word16
+  Word32  :: Type Word32
+  Word64  :: Type Word64
+  Float   :: Type Float
+  Double  :: Type Double
+
+instance EqualType Type where
+  (=~=) Bool   Bool   = Just Refl
+  (=~=) Int8   Int8   = Just Refl
+  (=~=) Int16  Int16  = Just Refl
+  (=~=) Int32  Int32  = Just Refl
+  (=~=) Int64  Int64  = Just Refl
+  (=~=) Word8  Word8  = Just Refl
+  (=~=) Word16 Word16 = Just Refl
+  (=~=) Word32 Word32 = Just Refl
+  (=~=) Word64 Word64 = Just Refl
+  (=~=) Float  Float  = Just Refl
+  (=~=) Double Double = Just Refl
+  (=~=) _ _ = Nothing
+
+class Typed a where
+  typeOf :: Type a
+
+instance Typed Bool   where typeOf = Bool
+instance Typed Int8   where typeOf = Int8
+instance Typed Int16  where typeOf = Int16
+instance Typed Int32  where typeOf = Int32
+instance Typed Int64  where typeOf = Int64
+instance Typed Word8  where typeOf = Word8
+instance Typed Word16 where typeOf = Word16
+instance Typed Word32 where typeOf = Word32
+instance Typed Word64 where typeOf = Word64
+instance Typed Float  where typeOf = Float
+instance Typed Double where typeOf = Double
+
+--------------------------------------------------------------------------------
+
+-- | A untyped type (no phantom type).
+data UType = forall a . UType { uTypeType :: Type a }
diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Dynamic.hs
@@ -0,0 +1,52 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE Rank2Types #-}
+
+-- | An implementation of dynamic types using "Copilot.Core.Type.Equality".
+-- The theory behind this technique is described the following paper:
+--
+-- * Baars, Arthur I. and Swierstra, S. Doaitse,
+-- \"/Typing dynamic typing/\",
+-- ACM SIGPLAN Notices vol. 37, p. 157-166, 2002
+
+{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-}
+
+module Copilot.Core.Type.Dynamic
+  ( Dynamic
+  , DynamicF
+  , toDyn
+  , fromDyn
+  , toDynF
+  , fromDynF
+  ) where
+
+import Copilot.Core.Type.Equality
+
+--------------------------------------------------------------------------------
+
+data Dynamic :: (* -> *) -> * where
+  Dynamic :: a -> t a -> Dynamic t
+
+data DynamicF :: (* -> *) -> (* -> *) -> * where
+  DynamicF :: f a -> t a -> DynamicF f t
+
+toDyn :: EqualType t => t a -> a -> Dynamic t
+toDyn t x = Dynamic x t
+
+fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a
+fromDyn t1 (Dynamic x t2) =
+  case t1 =~= t2 of
+    Just Refl -> return x
+    Nothing   -> Nothing
+
+toDynF :: EqualType t => t a -> f a -> DynamicF f t
+toDynF t fx = DynamicF fx t
+
+fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)
+fromDynF t1 (DynamicF fx t2) =
+  case t1 =~= t2 of
+    Just Refl -> return fx
+    Nothing   -> Nothing
diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Equality.hs
@@ -0,0 +1,36 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs, KindSignatures #-}
+
+module Copilot.Core.Type.Equality
+  ( Equal (..)
+  , EqualType (..)
+  , coerce
+  , refl
+  , trans
+  , symm
+  , cong
+  ) where
+
+data Equal :: * -> * -> * where
+  Refl :: Equal a a
+
+class EqualType t where
+  (=~=) :: t a -> t b -> Maybe (Equal a b)
+
+coerce :: Equal a b -> a -> b
+coerce Refl x = x
+
+refl :: Equal a a
+refl = Refl
+
+symm :: Equal a b -> Equal b a
+symm Refl = Refl
+
+trans :: Equal a b -> Equal b c -> Equal a c
+trans Refl Refl = Refl
+
+cong :: Equal a b -> Equal (f a) (f b)
+cong Refl = Refl
diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Show.hs
@@ -0,0 +1,76 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE ExistentialQuantification, GADTs #-}
+
+module Copilot.Core.Type.Show
+  ( ShowWit (..)
+  , showWit
+  , showWithType
+  , ShowType(..)
+  , showType
+  ) where
+
+import Copilot.Core.Type
+
+--------------------------------------------------------------------------------
+
+data ShowWit a = Show a => ShowWit
+
+--------------------------------------------------------------------------------
+
+showWit :: Type a -> ShowWit a
+showWit t =
+  case t of
+    Bool   -> ShowWit
+    Int8   -> ShowWit
+    Int16  -> ShowWit
+    Int32  -> ShowWit
+    Int64  -> ShowWit
+    Word8  -> ShowWit
+    Word16 -> ShowWit
+    Word32 -> ShowWit
+    Word64 -> ShowWit
+    Float  -> ShowWit
+    Double -> ShowWit
+
+--------------------------------------------------------------------------------
+
+showType :: Type a -> String
+showType t =
+  case t of
+    Bool   -> "Bool"
+    Int8   -> "Int8"
+    Int16  -> "Int16"
+    Int32  -> "Int32"
+    Int64  -> "Int64"
+    Word8  -> "Word8"
+    Word16 -> "Word16"
+    Word32 -> "Word32"
+    Word64 -> "Word64"
+    Float  -> "Float"
+    Double -> "Double"
+
+--------------------------------------------------------------------------------
+
+-- Are we proving equivalence with a C backend, in which case we want to show
+-- Booleans as '0' and '1'.
+data ShowType = C | Haskell
+
+--------------------------------------------------------------------------------
+
+showWithType :: ShowType -> Type a -> a -> String
+showWithType showT t x =
+  case showT of
+    C         -> case t of
+                   Bool -> if x then "1" else "0"
+                   _    -> sw
+    Haskell   -> case t of
+                   Bool -> if x then "true" else "false"
+                   _    -> sw                   
+  where
+  sw = case showWit t of
+         ShowWit -> show x
+
+--------------------------------------------------------------------------------
diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Type/Uninitialized.hs
@@ -0,0 +1,30 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | 
+
+{-# LANGUAGE GADTs #-}
+
+module Copilot.Core.Type.Uninitialized
+  ( uninitialized
+  ) where
+
+import Copilot.Core.Type
+
+--------------------------------------------------------------------------------
+
+uninitialized :: Type a -> a
+uninitialized t =
+  case t of
+    Bool   -> False
+    Int8   -> 0
+    Int16  -> 0
+    Int32  -> 0
+    Int64  -> 0
+    Word8  -> 0
+    Word16 -> 0
+    Word32 -> 0
+    Word64 -> 0
+    Float  -> 0
+    Double -> 0
diff --git a/src/Copilot/Core/Version.hs b/src/Copilot/Core/Version.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Version.hs
@@ -0,0 +1,9 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+module Copilot.Core.Version (version) where
+
+-- | The current version of Copilot Core.
+version :: String
+version = "0.1"