diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Tom Hawkins 2007-2009
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. 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.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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/Language/Atom.hs b/Language/Atom.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom.hs
@@ -0,0 +1,9 @@
+module Language.Atom
+  ( module Language.Atom.Compile
+  , module Language.Atom.Common
+  , module Language.Atom.Language
+  ) where
+
+import Language.Atom.Compile
+import Language.Atom.Common
+import Language.Atom.Language
diff --git a/Language/Atom/Code.hs b/Language/Atom/Code.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Code.hs
@@ -0,0 +1,154 @@
+-- | Atom code generation.
+module Language.Atom.Code
+  ( writeC
+  , ruleComplexity
+  ) where
+
+import Data.Char
+import Data.List
+import Data.Maybe
+import System.IO
+
+import Language.Atom.Elaboration
+import Language.Atom.Expressions
+
+declareMemory :: UV -> String
+declareMemory (UV id name init) = cType (constType init) ++ " " ++ e id ++ " = " ++ c ++ ";  /* " ++ name ++ " */\n"
+  where
+  c = case init of
+    CBool   c -> if c then "1" else "0" 
+    CInt8   c -> show c
+    CInt16  c -> show c
+    CInt32  c -> show c
+    CInt64  c -> show c
+    CWord8  c -> show c
+    CWord16 c -> show c
+    CWord32 c -> show c
+    CWord64 c -> show c
+    CFloat  c -> show c
+    CDouble c -> show c
+
+declareUE :: String -> (UE, Int) -> String
+declareUE d (ue, i) = case ue of
+  UVRef _              -> ""
+  UConst (CBool True ) -> d ++ "const " ++ cType (ueType ue) ++ " " ++ e i ++ " = 1;\n"
+  UConst (CBool False) -> d ++ "const " ++ cType (ueType ue) ++ " " ++ e i ++ " = 0;\n"
+  UConst c             -> d ++ "const " ++ cType (ueType ue) ++ " " ++ e i ++ " = " ++ show c ++ ";\n"
+  _                    -> d ++ cType (ueType ue) ++ " " ++ e i ++ ";\n"
+
+cType :: Type -> String
+cType t = case t of
+  Bool   -> "unsigned char"
+  Int8   -> "signed char"
+  Int16  -> "signed short int"
+  Int32  -> "signed long int"
+  Int64  -> "signed long long int"
+  Word8  -> "unsigned char"
+  Word16 -> "unsigned short int"
+  Word32 -> "unsigned long int"
+  Word64 -> "unsigned long long int"
+  Float  -> "float"
+  Double -> "double"
+
+codeUE :: [(UE, Int)] -> String -> (UE, Int) -> String
+codeUE ues d (ue, i) = case ue of
+  UConst _       -> ""
+  UVRef _        -> ""
+  _              -> d ++ e i ++ " = " ++ basic operands ++ ";\n"
+  where
+  operands = map (fromJust . flip lookup ues) $ ueUpstream ue
+  basic :: [Int] -> String
+  basic operands = case ue of
+    UVRef _              -> error "Code.ueStmt: should not get here."
+    UCust _ c            -> c
+    UCast _ _            -> "(" ++ cType (ueType ue) ++ ") " ++ a
+    UConst _             -> error "Code.ueStmt: should not get here."
+    UAdd _ _             ->  a ++ " + " ++ b
+    USub _ _             ->  a ++ " - " ++ b
+    UMul _ _             ->  a ++ " * " ++ b
+    UDiv _ _             ->  a ++ " / " ++ b
+    UMod _ _             ->  a ++ " % " ++ b
+    UNot _               ->  "! " ++ a
+    UAnd _               ->  drop 4 $ concat [ " && " ++ e a | a <- operands ]
+    UBWNot _             ->  "~ " ++ a
+    UBWAnd _ _           ->  a ++ " & " ++ b
+    UBWOr  _ _           ->  a ++ " | " ++ b
+    UShift _ n           -> (if n >= 0 then a ++ " << " ++ show n else a ++ " >> " ++ show (0 - n))
+    UEq  _ _             -> a ++ " == " ++ b
+    ULt  _ _             -> a ++ " < " ++ b
+    UMux _ _ _           -> a ++ " ? " ++ b ++ " : " ++ c
+    UF2B _               -> "*((unsigned long int *) &" ++ a ++ ")"
+    UD2B _               -> "*((unsigned long long int *) &" ++ a ++ ")"
+    UB2F _               -> "*((float *) &" ++ a ++ ")"
+    UB2D _               -> "*((double *) &" ++ a ++ ")"
+    where
+    a = e $ operands !! 0
+    b = e $ operands !! 1
+    c = e $ operands !! 2
+
+writeC :: Name -> String -> String -> String -> [[[Rule]]] -> [UV] -> IO ()
+writeC name include preCode postCode periods uvs = do
+  writeFile (name ++ ".c") c
+  where
+  c = unlines
+    [ include
+    , cType Word64 ++ " globalClock = 0;"
+    , concatMap declareMemory uvs
+    , concatMap (codeRule topo') $ concat $ concat periods
+    , "void " ++ name ++ "(void) {"
+    , preCode
+    , concatMap codePeriod $ zip [1..] periods
+    , postCode
+    , "  globalClock = globalClock + 1;"
+    , "}"
+    ]
+
+  topo' = topo $ maximum (map (\ (UV i _ _) -> i) uvs) + 1
+
+codeRule :: ([UE] -> [(UE, Int)]) -> Rule -> String
+codeRule topo rule = 
+  "/* " ++ show rule ++ " */\n" ++
+  "void r" ++ show (ruleId rule) ++ "(void) {\n" ++
+  concatMap (declareUE  "  ") ues ++
+  concatMap (codeUE ues "  ") ues ++
+  concatMap codeAction (ruleActions rule) ++
+  concatMap (\ (UV i _ _, ue) -> "  " ++ e i ++ " = " ++ e (id ue) ++ ";\n") (ruleAssigns rule) ++
+  "}\n\n"
+  where
+  ues = topo $ ruleEnable rule : snd (unzip (ruleAssigns rule)) ++ concat (snd (unzip (ruleActions rule)))
+  id ue = fromJust $ lookup ue ues
+  codeAction :: (([String] -> String), [UE]) -> String
+  codeAction (f, args) = "  if (" ++ e (id (ruleEnable rule)) ++ ") " ++ f (map (e . id) args) ++ ";\n"
+
+codePeriod :: (Int, [[Rule]]) -> String
+codePeriod (period, cycles) = concatMap (codeCycle period) $ zip [0..] cycles
+
+codeCycle :: Int -> (Int, [Rule]) -> String
+codeCycle period (cycle, _) | cycle >= period = error "Code.codeCycle"
+codeCycle _ (_, rules)      | null rules = ""
+codeCycle period (cycle, rules) =
+  "  if (globalClock % " ++ show period ++ " == " ++ show cycle ++ ") {\n" ++
+  concatMap (\ r -> "    r" ++ show (ruleId r) ++ "();  /* " ++ show r ++ " */\n") rules ++
+  "  }\n"
+
+e :: Int -> String
+e i = "e" ++ show i
+
+
+-- | Topologically sorts a list of expressions and subexpressions.
+topo :: Int -> [UE] -> [(UE, Int)]
+topo start ues = reverse ues'
+  where
+  (_, ues') = foldl collect (start, []) ues
+  collect :: (Int, [(UE, Int)]) -> UE -> (Int, [(UE, Int)])
+  collect (n, ues) ue | any ((== ue) . fst) ues = (n, ues)
+  collect (n, ues) ue = case ue of
+    UVRef (UV i _ _) -> (n,      (ue, i)  : ues )
+    _              -> (n' + 1, (ue, n') : ues')
+      where
+      (n', ues') = foldl collect (n, ues) $ ueUpstream ue
+
+-- | Number of UE's computed in rule.
+ruleComplexity :: Rule -> Int
+ruleComplexity rule = length $ topo 0 $ ruleEnable rule : snd (unzip (ruleAssigns rule)) ++ concat (snd (unzip (ruleActions rule)))
+
diff --git a/Language/Atom/Common.hs b/Language/Atom/Common.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Common.hs
@@ -0,0 +1,294 @@
+-- | Common Atom functions.
+module Language.Atom.Common
+  (
+  -- * Timers
+    Timer
+  , timer
+  , startTimer
+  , timerDone
+  -- * One Shots
+  , oneShotRise
+  , oneShotFall
+  -- * Debouncing
+  , debounce
+  -- * Lookup Tables
+  , lookupTable
+  -- * Hysteresis
+  , hysteresis
+  ) where
+
+import Data.Word
+
+import Language.Atom.Language
+
+-- | A Timer.
+data Timer = Timer (V Word64)
+
+-- | Creates a new timer.
+timer :: Name -> Atom Timer
+timer name = do
+  timer <- word64 name 0
+  return $ Timer timer
+
+-- | Starts a Timer.  A Timer can be restarted at any time.
+startTimer :: Timer -> E Word64 -> Atom ()
+startTimer (Timer t) time = t <== clock + time
+
+-- | True when a timer has completed.
+timerDone :: Timer -> E Bool
+timerDone (Timer t) = value t <=. clock
+
+
+-- | One-shot on a rising transition.
+oneShotRise :: E Bool -> Atom (E Bool)
+oneShotRise a = do
+  last <- bool "last" False
+  last <== a
+  return $ a &&. not_ (value last)
+
+-- | One-shot on a falling transition.
+oneShotFall :: E Bool -> Atom (E Bool)
+oneShotFall = oneShotRise . not_
+
+
+-- | Debounces a boolean given an on and off time (ticks) and an initial state.
+debounce :: Name -> E Word64 -> E Word64 -> Bool -> E Bool -> Atom (E Bool)
+debounce name onTime offTime init a = atom name $ do
+  x     <- bool "x" init
+  offTimer <- timer "offTimer"
+  onTimer  <- timer "onTimer"
+  atom "on" $ do
+    cond a
+    startTimer offTimer offTime
+  atom "off" $ do
+    cond $ not_ a
+    startTimer onTimer onTime
+  atom "set" $ do
+    cond $ timerDone onTimer &&. a ||. timerDone offTimer &&. not_ a
+    x <== a
+  return $ value x
+
+
+-- | 1-D lookup table.  X values out of table range are clipped at end Y values.
+--   Input table must be monitonically increasing in X.
+lookupTable :: FloatingE a => [(E a, E a)] -> E a -> E a
+lookupTable table x = mux (x >=. x1) y1 $ foldl f y0 table'
+  where
+  (_,  y0) = head table
+  (x1, y1) = last table
+  table' = zip (init table) (tail table)
+  f a ((x0,y0),(x1,y1)) = mux (x >=. x0) interp a
+    where
+    slope = (y1 - y0) / (x1 - x0)
+    interp = (x - x0) * slope + y0
+
+
+-- | Hysteresis returns true when then input exceeds max and false when
+--   the input is less than min.  The state is held when the input is between min and max.
+--
+-- > hysteresis name min max input
+hysteresis :: OrdE a => E a -> E a -> E a -> Atom (E Bool)
+hysteresis a b u = do
+  s <- bool "s" False
+  s <== (mux (u >. max) true $ mux (u <. min) false $ value s)
+  return $ value s
+  where
+  min = min_ a b
+  max = max_ a b
+
+{-
+
+-- | A channel is a uni-directional communication link that ensures one read for every write.
+data Channel a = Channel a (V Bool)
+
+-- | Creates a new channel, with a given name and data.
+channel :: a -> Atom (Channel a)
+channel a = do
+  hasData <- bool False
+  return $ Channel a hasData
+
+-- | Write data to a 'Channel'.  A write will only suceed if the 'Channel' is empty.
+writeChannel :: Channel a -> Action ()
+writeChannel (Channel _ hasData) = do
+  when $ not_ $ value hasData
+  hasData <== true
+  
+-- | Read data from a 'Channel'.  A read will only suceed if the 'Channel' has data to be read.
+readChannel :: Channel a -> Action a
+readChannel (Channel a hasData) = do
+  when $ value hasData
+  hasData <== false
+  return a
+
+-- | Fades one signal to another.
+module Language.Atom.Common.Fader
+  ( Fader
+  , FaderInit (..)
+  , fader
+  , fadeToA
+  , fadeToB
+  , fadeToCenter
+  ) where
+
+import Language.Atom
+
+-- | Fader object.
+data Fader = Fader (V Int)
+
+-- | Fader initalization.
+data FaderInit = OnA | OnB | OnCenter
+
+toA = 0
+toB = 1
+toCenter = 2
+
+-- | Fader construction.  Name, fade rate, fader init, and signal A and B.
+fader :: Name -> Double -> FaderInit -> E Double -> E Double -> Atom (Fader, E Double)
+fader name rate init a b = scope name $ do
+  --assert "positiveRate" $ rate >= 0
+
+  target <- int (case init of {OnA -> toA; OnB -> toB; OnCenter -> toCenter})
+  perA <- double (case init of {OnA -> 1;   OnB -> 0;   OnCenter -> 0.5})
+
+  rule "toA" $ do
+    when $ value target ==. intC toA
+    when $ value perA <. 1
+    perA <== mux (1 - value perA <. doubleC rate) 1 (value perA + doubleC rate)
+
+  rule "toB" $ do
+    when $ value target ==. intC toB
+    when $ value perA >. 0
+    perA <== mux (value perA <. doubleC rate) 0 (value perA - doubleC rate)
+
+  rule "toCenterFrom0" $ do
+    when $ value target ==. intC toCenter
+    when $ value perA <. 0.5
+    perA <== mux (0.5 - value perA <. doubleC rate) 0.5 (value perA + doubleC rate)
+
+  rule "toCenterFrom1" $ do
+    when $ value target ==. intC toCenter
+    when $ value perA >. 0.5
+    perA <== mux (value perA - 0.5 <. doubleC rate) 0.5 (value perA - doubleC rate)
+
+  return (Fader target, (a * value perA + b * (1 - value perA)) / 2)
+
+-- | Fade to signal A.
+fadeToA :: Fader -> Action ()
+fadeToA (Fader target) = target <== intC toA
+
+-- | Fade to signal B.
+fadeToB :: Fader -> Action ()
+fadeToB (Fader target) = target <== intC toB
+
+-- | Fade to center, ie average of signal A and B.
+fadeToCenter :: Fader -> Action ()
+fadeToCenter (Fader target) = target <== intC toCenter
+
+module Language.Atom.Common.Process
+  ( Process (..)
+  , process
+  ) where
+
+import Language.Atom
+
+data Process
+  = Par [Process]
+  | Seq [Process]
+  | Alt [Process]
+  | Rep Process
+  | Act Action
+
+process :: Name -> Process -> Atom ()
+
+-- | Time integrated threshold functions typically used in condition monitoring.
+module Language.Atom.Common.Threshold
+  ( boolThreshold
+  , floatingThreshold
+  ) where
+
+import Language.Atom
+
+
+-- | Boolean thresholding over time.  Output is set when internal counter hits limit, and cleared when counter is 0.
+boolThreshold :: Name -> Int -> Bool -> E Bool -> Atom (E Bool)
+boolThreshold name num init input = scope name $ do
+  --assert "positiveNumber" $ num >= 0
+
+  state <- bool init
+  count <- int  (if init then num else 0)
+
+  rule "update" $ do
+    when $ value count >. 0 &&. value count <. num
+    count <== value count + mux input 1 (-1)
+
+  rule "low" $ do
+    when $ value count ==. 0
+    state <== false
+
+  rule "high" $ do
+    when $ value count ==. intC num
+    state <== true
+
+  return $ value state
+
+-- | Integrating threshold.  Output is set with integral reaches limit, and cleared when integral reaches 0.
+doubleThreshold :: Name -> Double -> E Double -> Atom (E Bool)
+doubleThreshold name lim input = scope name $ do
+  --assert "positiveLimit" $ lim >= 0
+
+  state <- bool False
+  sum <- double 0
+
+  (high,low) <- priority
+  
+  rule "update"
+    sum <== value sum + input
+    low
+
+  rule "clear" $ do
+    when $ value sum <=. 0
+    state <== false
+    sum <== 0
+    high
+
+  rule "set" $ do
+    when $ value sum >=. doubleC lim
+    state <== true
+    sum <== doubleC lim
+    high
+
+  return  $ value state
+
+-- | Capturing data that can either be valid or invalid.
+module Language.Atom.Common.ValidData
+  ( ValidData
+  , validData
+  , getValidData
+  , whenValid
+  , whenInvalid
+  ) where
+
+import Language.Atom
+
+-- | 'ValidData' captures the data and its validity condition.
+--   'ValidData' is abstract to prevent rules from using invalid data.
+data ValidData a = ValidData a (E Bool)
+
+-- | Create 'ValidData' given the data and validity condition.
+validData :: a -> E Bool -> ValidData a
+validData = ValidData 
+
+-- | Get a valid data.  Action is disabled if data is invalid.
+getValidData :: ValidData a -> Action a
+getValidData (ValidData a v) = cond v >> return a
+
+-- | Action enabled if 'ValidData' is valid.
+whenValid :: ValidData a -> Action ()
+whenValid (ValidData _ v) = cond v
+
+-- | Action enabled if 'ValidData' is not valid.
+whenInvalid :: ValidData a -> Action ()
+whenInvalid (ValidData _ v) = cond $ not_ v
+-}
+
+
diff --git a/Language/Atom/Compile.hs b/Language/Atom/Compile.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Compile.hs
@@ -0,0 +1,35 @@
+-- | Atom compilation.
+module Language.Atom.Compile
+  ( compile
+  ) where
+
+import Control.Monad.State hiding (join)
+import Data.Maybe
+import System.Exit
+import System.IO
+
+import Language.Atom.Code
+import Language.Atom.Scheduling
+import Language.Atom.Elaboration
+import Language.Atom.Language hiding (Atom)
+import Language.Atom.Verify
+
+-- | Compiles an atom description to C.
+compile :: Name -> String -> String -> String -> Atom () -> Int -> IO ()
+compile name include preCode postCode atom depth = do
+  r <- elaborate name atom
+  case r of
+    Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)
+    Just (rules, uvs, asserts) -> do
+      r <- schedule rules
+      case r of
+        Nothing -> putStrLn "ERROR: Rule scheduling failed." >> exitWith (ExitFailure 1)
+        Just schedule -> do
+          when (depth > 0) $ do
+            putStrLn $ "Starting bounded model checking with depth " ++ show depth ++ "..."
+            v <- mapM (verify depth schedule uvs) asserts 
+            when (not $ and v) $ putStrLn "ERROR: Verification failed." >> exitWith (ExitFailure 1)
+          putStrLn "Starting code generation..."
+          hFlush stdout
+          writeC name include preCode postCode schedule uvs
+
diff --git a/Language/Atom/Elaboration.hs b/Language/Atom/Elaboration.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Elaboration.hs
@@ -0,0 +1,152 @@
+module Language.Atom.Elaboration
+  (
+  -- * Atom monad and container.
+    Atom
+  , AtomDB     (..)
+  , Global     (..)
+  , Rule       (..)
+  , buildAtom
+  -- * Type Aliases and Utilities
+  , UID
+  , Name
+  , Path
+  , elaborate
+  , var
+  , addName
+  ) where
+
+import Control.Monad.State hiding (join)
+import Data.List
+import Data.Maybe
+import Data.Word
+import Language.Atom.Expressions
+import System.IO
+
+type UID = Int
+
+-- | A name.
+type Name = String
+
+-- | A heirarchical name.
+type Path = [Name]
+
+data Global = Global
+  { gId      :: Int
+  , gProbes  :: [(String, Type, E Word64)]
+  , gUVs     :: [UV]
+  , gPeriod  :: Int
+  , gAsserts :: [(String, UE)]
+  }
+
+data AtomDB = AtomDB
+  { atomId          :: Int
+  , atomName        :: Name
+  , atomNames       :: [Name]      -- Names used at this level.
+  , atomEnable      :: UE          -- Enabling condition.
+  , atomSubs        :: [AtomDB]    -- Sub atoms.
+  , atomPeriod      :: Int
+  , atomAssigns     :: [(UV, UE)]
+  , atomActions     :: [([String] -> String, [UE])]
+  }
+
+data Rule = Rule
+  { ruleId        :: Int
+  , ruleName      :: Name
+  , ruleEnable    :: UE
+  , ruleAssigns   :: [(UV, UE)]
+  , ruleActions   :: [([String] -> String, [UE])]
+  , rulePeriod    :: Int
+  }
+
+instance Show AtomDB where show = atomName
+instance Eq   AtomDB where a == b = atomId a == atomId b
+instance Ord  AtomDB where compare a b = compare (atomId a) (atomId b)
+instance Show Rule   where show = ruleName
+instance Eq   Rule   where a == b = ruleId a == ruleId b
+instance Ord  Rule   where compare a b = compare (ruleId a) (ruleId b)
+
+elaborateRules:: UE -> AtomDB -> [Rule]
+elaborateRules parentEnable atom = if isRule then rule : rules else rules
+  where
+  isRule = not (null $ atomAssigns atom) || not (null $ atomActions atom)
+  enable = uand parentEnable $ atomEnable atom
+  rule = Rule
+    { ruleId        = atomId   atom
+    , ruleName      = atomName atom
+    , ruleEnable    = enable
+    , ruleAssigns   = map enableAssign $ atomAssigns atom
+    , ruleActions   = atomActions atom
+    , rulePeriod    = atomPeriod atom
+    }
+  rules = concatMap (elaborateRules enable) (atomSubs atom)
+  enableAssign :: (UV, UE) -> (UV, UE)
+  enableAssign (uv, ue) = (uv, umux enable ue $ UVRef uv)
+
+buildAtom :: Global -> Name -> Atom a -> IO (a, (Global, AtomDB))
+buildAtom g name atom = do
+  runStateT atom $ (g { gId = gId g + 1 }, AtomDB
+    { atomId        = gId g
+    , atomName      = name
+    , atomNames     = []
+    , atomEnable    = ubool True
+    , atomSubs      = []
+    , atomPeriod    = gPeriod g
+    , atomAssigns   = []
+    , atomActions   = []
+    })
+
+
+-- | The 'Atom' container holds top level IO, 'Var', and 'Rule' definitions.
+type Atom = StateT (Global, AtomDB) IO
+
+-- | A Relation is used for relative performance constraints between 'Action's.
+-- data Relation = Higher UID | Lower UID deriving (Show, Eq)
+
+-- | Given a top level name and design, elabortes design and returns a design database.
+elaborate :: Name -> Atom () -> IO (Maybe ([Rule], [UV], [(String, UE)]))
+elaborate name atom = do
+  putStrLn "Starting atom elaboration..."
+  hFlush stdout
+  (_, (g, atomDB)) <- buildAtom (Global { gId = 0, gProbes = [], gUVs = [], gPeriod = 1, gAsserts = [] }) name atom
+  let rules = elaborateRules (ubool True) atomDB
+  mapM_ checkEnable rules
+  ok <- checkAssignConflicts atomDB
+  if not ok
+    then return Nothing
+    else return $ Just (rules, sort $ gUVs g, gAsserts g)
+
+checkEnable :: Rule -> IO ()
+checkEnable rule | ruleEnable rule == ubool False = putStrLn $ "WARNING: Rule will never execute: " ++ show rule
+                 | otherwise                      = return ()
+
+checkAssignConflicts :: AtomDB -> IO Bool
+checkAssignConflicts atom = do
+  if length vars /= length vars'
+    then do
+      putStrLn $ "ERROR: Atom " ++ show atom ++ " contains multiple assignments to the same variable(s)."
+      return False
+    else do
+      subs <- mapM checkAssignConflicts $ atomSubs atom
+      return $ and subs
+  where
+  vars = fst $ unzip $ atomAssigns atom
+  vars' = nub vars
+
+-- | Generic variable declaration.
+var :: Name -> Const -> Atom (V a)
+var name const = do
+  name <- addName name
+  (g, atom) <- get
+  let uv = UV (gId g) name const
+  put (g { gId = gId g  + 1, gUVs =  uv : gUVs g }, atom)
+  return $ V uv
+
+addName :: Name -> Atom Name
+addName name = do
+  (g, atom) <- get
+  if elem name (atomNames atom)
+    then error $ "ERROR: Name \"" ++ name ++ "\" not unique in " ++ show atom ++ "."
+    else do
+      put (g, atom { atomNames = name : atomNames atom })
+      return $ atomName atom ++ "." ++ name
+
diff --git a/Language/Atom/Expressions.hs b/Language/Atom/Expressions.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Expressions.hs
@@ -0,0 +1,842 @@
+module Language.Atom.Expressions
+  (
+  -- * Types
+    E     (..)
+  , V     (..)
+  , UE    (..)
+  , UV    (..)
+  , Expr  (..)
+  , Expression (..)
+  , Variable   (..)
+  , Type  (..)
+  , Const (..)
+  , Width (..)
+  , constType
+  , ue
+  , uv
+  , ueType
+  , uvType
+  , ueUpstream
+  , uvSet
+  , NumE
+  , FloatingE
+  , EqE
+  , OrdE
+  -- * Custom Es
+  , customDouble
+  -- * Constants
+  , true
+  , false
+  -- * Variable Reference and Assignment
+  , value
+  -- * Logical Operations
+  , not_
+  , (&&.)
+  , (||.)
+  , and_
+  , or_
+  , any_
+  , all_
+  -- * Equality and Comparison
+  , (==.)
+  , (/=.)
+  , (<.)
+  , (<=.)
+  , (>.)
+  , (>=.)
+  , min_
+  , minimum_
+  , max_
+  , maximum_
+  , limit
+  -- * Arithmetic Operations
+  , div_
+  , mod_
+  -- * Conditional Operator
+  , mux
+  -- * Smart constructors for untyped expressions.
+  , ubool
+  , unot
+  , uand
+  , uor
+  , ueq
+  , umux
+  ) where
+
+import Data.Bits
+import Data.Int
+import Data.List
+import Data.Ratio
+import Data.Word
+
+--infixl 7 /., %.
+--infixl 6 +., -.
+--infixr 5 ++.
+infix  4 ==., /=., <., <=., >., >=.
+infixl 3 &&. --, ^. -- , &&&, $&, $&&
+infixl 2 ||. -- , |||, $$, $:, $|
+--infixr 1 -- <==, <-- -- , |->, |=>, -->
+
+-- | The type of a 'E'.
+data Type
+  = Bool
+  | Int8
+  | Int16
+  | Int32
+  | Int64
+  | Word8
+  | Word16
+  | Word32
+  | Word64
+  | Float
+  | Double
+  deriving (Show, Read, Eq, Ord)
+
+data Const
+  = CBool   Bool
+  | CInt8   Int8
+  | CInt16  Int16
+  | CInt32  Int32
+  | CInt64  Int64
+  | CWord8  Word8
+  | CWord16 Word16
+  | CWord32 Word32
+  | CWord64 Word64
+  | CFloat  Float
+  | CDouble Double
+  deriving (Eq, Ord)
+
+instance Show Const where
+  show c = case c of
+    CBool   True  -> "1"
+    CBool   False -> "0"
+    CInt8   c -> show c
+    CInt16  c -> show c
+    CInt32  c -> show c
+    CInt64  c -> show c
+    CWord8  c -> show c
+    CWord16 c -> show c
+    CWord32 c -> show c
+    CWord64 c -> show c
+    CFloat  c -> show c
+    CDouble c -> show c
+
+constType :: Const -> Type
+constType c = case c of
+  CBool   _ -> Bool
+  CInt8   _ -> Int8
+  CInt16  _ -> Int16
+  CInt32  _ -> Int32
+  CInt64  _ -> Int64
+  CWord8  _ -> Word8
+  CWord16 _ -> Word16
+  CWord32 _ -> Word32
+  CWord64 _ -> Word64
+  CFloat  _ -> Float
+  CDouble _ -> Double
+
+data Expression
+  = EBool   (E Bool)
+  | EInt8   (E Int8)
+  | EInt16  (E Int16)
+  | EInt32  (E Int32)
+  | EInt64  (E Int64)
+  | EWord8  (E Word8)
+  | EWord16 (E Word16)
+  | EWord32 (E Word32)
+  | EWord64 (E Word64)
+  | EFloat  (E Float)
+  | EDouble (E Double)
+  
+data Variable
+  = VBool   (V Bool)
+  | VInt8   (V Int8)
+  | VInt16  (V Int16)
+  | VInt32  (V Int32)
+  | VInt64  (V Int64)
+  | VWord8  (V Word8)
+  | VWord16 (V Word16)
+  | VWord32 (V Word32)
+  | VWord64 (V Word64)
+  | VFloat  (V Float)
+  | VDouble (V Double) deriving Eq
+  
+
+-- | Variables updated by state transition rules.
+data V a = V UV deriving Eq
+
+-- | Unsigned variables.
+data UV = UV Int String Const deriving Show
+instance Eq   UV where UV a _ _  == UV b _ _ = a == b
+instance Ord  UV where compare (UV a _ _) (UV b _ _) = compare a b
+
+-- | A typed expression.
+data E a where
+  VRef    :: V a -> E a
+  Const   :: a -> E a
+  Cust    :: String -> E a
+  Cast    :: (NumE a, NumE b) => E a -> E b
+  Add     :: NumE a => E a -> E a -> E a
+  Sub     :: NumE a => E a -> E a -> E a
+  Mul     :: NumE a => E a -> E a -> E a
+  Div     :: NumE a => E a -> E a -> E a
+  Mod     :: IntegralE a => E a -> E a -> E a
+  Not     :: E Bool -> E Bool
+  And     :: E Bool -> E Bool -> E Bool
+  BWNot   :: IntegralE a => E a -> E a
+  BWAnd   :: IntegralE a => E a -> E a -> E a
+  BWOr    :: IntegralE a => E a -> E a -> E a
+  Shift   :: IntegralE a => E a -> Int -> E a
+  Eq      :: (EqE a, OrdE a) => E a -> E a -> E Bool
+  Lt      :: OrdE a => E a -> E a -> E Bool
+  Mux     :: E Bool -> E a -> E a -> E a
+  F2B     :: E Float  -> E Word32
+  D2B     :: E Double -> E Word64
+  B2F     :: E Word32 -> E Float
+  B2D     :: E Word64 -> E Double
+
+instance Show (E a) where
+  show _ = error "Show (E a) not implemented"
+
+instance Expr a => Eq (E a) where
+  a == b = ue a == ue b
+
+-- | An untyped term.
+data UE
+  = UVRef UV
+  | UConst Const
+  | UCust  Type String
+  | UCast  Type UE
+  | UAdd   UE UE
+  | USub   UE UE
+  | UMul   UE UE
+  | UDiv   UE UE
+  | UMod   UE UE
+  | UNot   UE
+  | UAnd   [UE]
+  | UBWNot UE
+  | UBWAnd UE UE
+  | UBWOr  UE UE
+  | UShift UE Int
+  | UEq    UE UE
+  | ULt    UE UE
+  | UMux   UE UE UE
+  | UF2B   UE
+  | UD2B   UE
+  | UB2F   UE
+  | UB2D   UE
+  deriving (Show, Eq, Ord)
+
+class Width a where
+  width :: a -> Int
+
+instance Width Type where
+  width t = case t of
+    Bool   -> 1
+    Int8   -> 8
+    Int16  -> 16
+    Int32  -> 32
+    Int64  -> 64
+    Word8  -> 8
+    Word16 -> 16
+    Word32 -> 32
+    Word64 -> 64
+    Float  -> 32
+    Double -> 64
+
+instance Width Const           where width = width . constType
+instance Expr a => Width (E a) where width = width . eType
+instance Expr a => Width (V a) where width = width . eType . value
+instance Width UE              where width = width . ueType
+
+class Eq a => Expr a where
+  eType      :: E a -> Type
+  constant   :: a -> Const
+  expression :: E a -> Expression
+  variable   :: V a -> Variable
+  rawBits    :: E a -> E Word64
+
+instance Expr Bool   where
+  eType _    = Bool
+  constant   = CBool
+  expression = EBool
+  variable   = VBool
+  rawBits a  = mux a 1 0
+
+instance Expr Int8   where
+  eType _    = Int8
+  constant   = CInt8
+  expression = EInt8
+  variable   = VInt8
+  rawBits    = Cast
+
+instance Expr Int16  where
+  eType _    = Int16
+  constant   = CInt16
+  expression = EInt16
+  variable   = VInt16
+  rawBits    = Cast
+
+instance Expr Int32  where
+  eType _    = Int32
+  constant   = CInt32
+  expression = EInt32
+  variable   = VInt32
+  rawBits     = Cast
+
+instance Expr Int64  where
+  eType _    = Int64
+  constant   = CInt64
+  expression = EInt64
+  variable   = VInt64
+  rawBits    = Cast
+
+instance Expr Word8  where
+  eType _    = Word8
+  constant   = CWord8
+  expression = EWord8
+  variable   = VWord8
+  rawBits    = Cast
+
+instance Expr Word16 where
+  eType _    = Word16
+  constant   = CWord16
+  expression = EWord16
+  variable   = VWord16
+  rawBits    = Cast
+
+instance Expr Word32 where
+  eType _    = Word32
+  constant   = CWord32
+  expression = EWord32
+  variable   = VWord32
+  rawBits    = Cast
+
+instance Expr Word64 where
+  eType _    = Word64
+  constant   = CWord64
+  expression = EWord64
+  variable   = VWord64
+  rawBits    = id
+
+instance Expr Float  where
+  eType _    = Float
+  constant   = CFloat
+  expression = EFloat
+  variable   = VFloat
+  rawBits    = Cast . F2B
+
+instance Expr Double where
+  eType _    = Double
+  constant   = CDouble
+  expression = EDouble
+  variable   = VDouble
+  rawBits    = D2B
+
+
+class (Num a, Expr a, EqE a, OrdE a) => NumE a
+instance NumE Int8
+instance NumE Int16
+instance NumE Int32
+instance NumE Int64
+instance NumE Word8
+instance NumE Word16
+instance NumE Word32
+instance NumE Word64
+instance NumE Float
+instance NumE Double
+
+class (NumE a, Integral a) => IntegralE a where signed :: E a -> Bool
+instance IntegralE Int8   where signed _ = True
+instance IntegralE Int16  where signed _ = True
+instance IntegralE Int32  where signed _ = True
+instance IntegralE Int64  where signed _ = True
+instance IntegralE Word8  where signed _ = False
+instance IntegralE Word16 where signed _ = False
+instance IntegralE Word32 where signed _ = False
+instance IntegralE Word64 where signed _ = False
+
+class (Eq a, Expr a) => EqE a
+instance EqE Bool
+instance EqE Int8
+instance EqE Int16
+instance EqE Int32
+instance EqE Int64
+instance EqE Word8
+instance EqE Word16
+instance EqE Word32
+instance EqE Word64
+instance EqE Float
+instance EqE Double
+
+class (Eq a, Ord a, EqE a) => OrdE a
+instance OrdE Int8
+instance OrdE Int16
+instance OrdE Int32
+instance OrdE Int64
+instance OrdE Word8
+instance OrdE Word16
+instance OrdE Word32
+instance OrdE Word64
+instance OrdE Float
+instance OrdE Double
+
+class (RealFloat a, NumE a, OrdE a) => FloatingE a
+instance FloatingE Float
+instance FloatingE Double
+
+instance (Num a, NumE a, OrdE a) => Num (E a) where
+  (Const a) + (Const b) = Const $ a + b
+  a + b = Add a b
+  (Const a) - (Const b) = Const $ a - b
+  a - b = Sub a b
+  (Const a) * (Const b) = Const $ a * b
+  a * b = Mul a b
+  negate a = 0 - a
+  abs a = mux (a <. 0) (negate a) a
+  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
+  fromInteger i = Const $ fromInteger i
+
+instance (OrdE a, NumE a, Num a, Fractional a) => Fractional (E a) where
+  (Const a) / (Const b) = Const $ a / b
+  a / b = Div a b
+  recip a = 1 / a
+  fromRational r = Const $ (fromInteger (numerator r)) / (fromInteger (denominator r))
+
+{-
+instance (Num a, Fractional a, Floating a, FloatingE a) => Floating (E a) where
+  pi       = Const pi
+  exp      (Const a) = Const $ exp a
+  exp      a         = Exp a
+  log      (Const a) = Const $ log a
+  log      a         = Log a
+  sqrt     (Const a) = Const $ sqrt a
+  sqrt     a         = Sqrt a
+  (**)     (Const a) (Const b) = Const $ a ** b
+  (**)     a b       = Pow a b
+  sin      (Const a) = Const $ sin a
+  sin      a         = Sin a
+  cos      a         = sqrt (1 - sin a ** 2)
+  sinh     a         = (exp a - exp (-a)) / 2
+  cosh     a         = (exp a + exp (-a)) / 2
+  asin     (Const a) = Const $ asin a
+  asin     a         = Asin a
+  acos     a         = pi / 2 - asin a
+  atan     a         = asin (a / (sqrt (a ** 2 + 1)))
+  asinh    a         = log (a + sqrt (a ** 2 + 1))
+  acosh    a         = log (a + sqrt (a ** 2 - 1))
+  atanh    a         = 0.5 * log ((1 + a) / (1 - a))
+-}
+
+instance (Expr a, OrdE a, EqE a, IntegralE a, Bits a) => Bits (E a) where
+  (Const a) .&. (Const b) = Const $ a .&. b
+  a .&. b = BWAnd a b
+  complement (Const a) = Const $ complement a
+  complement a = BWNot a
+  (Const a) .|. (Const b) = Const $ a .|. b
+  a .|. b = BWOr a b
+  xor a b = (a .&. complement b) .|. (complement a .&. b)
+  shift (Const a) n = Const $ shift a n
+  shift a n = Shift a n
+  rotate = error "E rotate not supported."
+  bitSize  a = width a
+  isSigned a = signed a
+
+-- | Creates a custom E Double.
+customDouble :: String -> E Double
+customDouble c = Cust c
+
+-- | True term.
+true :: E Bool
+true = Const True
+
+-- | False term.
+false :: E Bool
+false = Const False
+
+-- | Logical negation.
+not_ :: E Bool -> E Bool
+not_ = Not
+
+-- | Logical AND.
+(&&.) :: E Bool -> E Bool -> E Bool
+(&&.) = And
+
+-- | Logical OR.
+(||.) :: E Bool -> E Bool -> E Bool
+(||.) a b = not_ $ not_ a &&. not_ b
+
+-- | The conjunction of a E Bool list.
+and_ :: [E Bool] -> E Bool
+and_ = foldl (&&.) true
+
+-- | The disjunction of a E Bool list.
+or_ :: [E Bool] -> E Bool
+or_ = foldl (||.) false
+
+-- | True iff the predicate is true for all elements.
+all_ :: (a -> E Bool) -> [a] -> E Bool
+all_ f a = and_ $ map f a
+
+-- | True iff the predicate is true for any element.
+any_ :: (a -> E Bool) -> [a] -> E Bool
+any_ f a = or_ $ map f a
+
+-- | Equal.
+(==.) :: (EqE a, OrdE a) => E a -> E a -> E Bool
+(==.) = Eq
+
+-- | Not equal.
+(/=.) :: (EqE a, OrdE a) => E a -> E a -> E Bool
+a /=. b = not_ (a ==. b)
+
+-- | Less than.
+(<.) :: OrdE a => E a -> E a -> E Bool
+(<.) = Lt
+
+-- | Greater than.
+(>.) :: OrdE a => E a -> E a -> E Bool
+a >. b = b <. a
+
+-- | Less than or equal.
+(<=.) :: OrdE a => E a -> E a -> E Bool
+a <=. b =  not_ (a >. b)
+
+-- | Greater than or equal.
+(>=.) :: OrdE a => E a -> E a -> E Bool
+a >=. b = not_ (a <. b)
+
+-- | Returns the minimum of two numbers.
+min_ :: OrdE a => E a -> E a -> E a
+min_ a b = mux (a <=. b) a b
+
+-- | Returns the minimum of a list of numbers.
+minimum_ :: OrdE a => [E a] -> E a
+minimum_ = foldl1 min_
+
+-- | Returns the maximum of two numbers.
+max_ :: OrdE a => E a -> E a -> E a
+max_ a b = mux (a >=. b) a b
+
+-- | Returns the maximum of a list of numbers.
+maximum_ :: OrdE a => [E a] -> E a
+maximum_ = foldl1 max_
+
+-- | Limits between min and max.
+limit :: OrdE a => E a -> E a -> E a -> E a
+limit a b i = max_ min $ min_ max i
+  where
+  min = min_ a b
+  max = max_ a b
+
+-- | Division.
+div_ :: IntegralE a => E a -> E a -> E a
+div_ (Const a) (Const b) = Const $ a `div` b
+div_ a b = Div a b
+
+-- | Modulo.
+mod_ :: IntegralE a => E a -> E a -> E a
+mod_ (Const a) (Const b) = Const $ a `mod` b
+mod_ a b = Mod a b
+
+-- | Returns the value of a 'V'.
+value :: V a -> E a
+value a = VRef a
+
+-- | Conditional expression.
+--
+-- > mux test onTrue ofFalse
+mux :: Expr a => E Bool -> E a -> E a -> E a
+mux = Mux
+
+-- | A set of all variables referenced in a term.
+uvSet :: UE -> [UV]
+uvSet = nub . uvList
+
+uvList :: UE -> [UV]
+uvList t = case t of
+  UVRef v      -> [v]
+  UCust _ _    -> []
+  UCast _ a    -> uvList a
+  UConst _     -> []
+  UAdd a b     -> uvList a ++ uvList b
+  USub a b     -> uvList a ++ uvList b
+  UMul a b     -> uvList a ++ uvList b
+  UDiv a b     -> uvList a ++ uvList b
+  UMod a b     -> uvList a ++ uvList b
+  UNot a       -> uvList a
+  UAnd a       -> concatMap uvList a
+  UBWNot a     -> uvList a
+  UBWAnd a b   -> uvList a ++ uvList b
+  UBWOr  a b   -> uvList a ++ uvList b
+  UShift a _   -> uvList a
+  UEq  a b     -> uvList a ++ uvList b
+  ULt  a b     -> uvList a ++ uvList b
+  UMux a b c   -> uvList a ++ uvList b ++ uvList c
+  UF2B a       -> uvList a
+  UD2B a       -> uvList a
+  UB2F a       -> uvList a
+  UB2D a       -> uvList a
+
+uvType :: UV -> Type
+uvType (UV _ _ c) = constType c
+
+-- | The type of an UE.
+ueType :: UE -> Type
+ueType t = case t of
+  UVRef uvar -> uvType uvar
+  UCust t _  -> t
+  UCast t _  -> t
+  UConst c   -> constType c
+  UAdd a _   -> ueType a
+  USub a _   -> ueType a
+  UMul a _   -> ueType a
+  UDiv a _   -> ueType a
+  UMod a _   -> ueType a
+  UNot _     -> Bool
+  UAnd _     -> Bool
+  UBWNot a   -> ueType a
+  UBWAnd a _ -> ueType a
+  UBWOr  a _ -> ueType a
+  UShift a _ -> ueType a
+  UEq  _ _   -> Bool
+  ULt  _ _   -> Bool
+  UMux _ a _ -> ueType a
+  UF2B _     -> Word32
+  UD2B _     -> Word64
+  UB2F _     -> Float
+  UB2D _     -> Double
+
+-- | The list of UEs adjacent upstream of a UE.
+ueUpstream :: UE -> [UE]
+ueUpstream t = case t of
+  UVRef _   -> []
+  UCust _ _   -> []
+  UCast _ a   -> [a]
+  UConst _    -> []
+  UAdd a b    -> [a, b]
+  USub a b    -> [a, b]
+  UMul a b    -> [a, b]
+  UDiv a b    -> [a, b]
+  UMod a b    -> [a, b]
+  UNot a      -> [a]
+  UAnd a      -> a
+  UBWNot a    -> [a]
+  UBWAnd a b  -> [a, b]
+  UBWOr  a b  -> [a, b]
+  UShift a _  -> [a]
+  UEq  a b    -> [a, b]
+  ULt  a b    -> [a, b]
+  UMux a b c  -> [a, b, c]
+  UF2B a      -> [a]
+  UD2B a      -> [a]
+  UB2F a      -> [a]
+  UB2D a      -> [a]
+
+ue :: Expr a => E a -> UE
+ue t = case t of
+  VRef (V v) -> UVRef v
+  Const  a     -> UConst $ constant a
+  Cust   a     -> UCust    tt a
+  Cast   a     -> UCast    tt (ue a)
+  Add    a b   -> UAdd     (ue a) (ue b)
+  Sub    a b   -> USub     (ue a) (ue b)
+  Mul    a b   -> UMul     (ue a) (ue b)
+  Div    a b   -> UDiv     (ue a) (ue b)
+  Mod    a b   -> UMod     (ue a) (ue b)
+  Not    a     -> unot     (ue a)
+  And    a b   -> uand     (ue a) (ue b)
+  BWNot  a     -> UBWNot   (ue a)
+  BWAnd  a b   -> UBWAnd   (ue a) (ue b)
+  BWOr   a b   -> UBWOr    (ue a) (ue b)
+  Shift  a b   -> UShift   (ue a) b
+  Eq     a b   -> ueq      (ue a) (ue b)
+  Lt     a b   -> ult      (ue a) (ue b)
+  Mux    a b c -> umux     (ue a) (ue b) (ue c)
+  F2B    a     -> UF2B     (ue a)
+  D2B    a     -> UD2B     (ue a)
+  B2F    a     -> UB2F     (ue a)
+  B2D    a     -> UB2D     (ue a)
+  where
+  tt = eType t
+
+uv :: V a -> UV
+uv (V v) = v
+
+-- XXX A future smart constructor for numeric type casting.
+-- ucast :: Type -> UE -> UE
+
+ubool :: Bool -> UE
+ubool = UConst . CBool
+
+unot :: UE -> UE
+unot (UConst (CBool a)) = ubool $ not a
+unot (UNot a) = a
+unot a = UNot a
+
+uand :: UE -> UE -> UE
+uand a b | a == b                   = a
+uand a@(UConst (CBool False)) _     = a
+uand _ a@(UConst (CBool False))     = a
+uand (UConst (CBool True)) a        = a
+uand a (UConst (CBool True))        = a
+uand (UAnd a) (UAnd b)              = reduceAnd $ a ++ b
+uand (UAnd a) b                     = reduceAnd $ b : a
+uand a (UAnd b)                     = reduceAnd $ a : b
+uand a b                            = reduceAnd [a, b]
+
+reduceAnd :: [UE] -> UE
+
+-- a && not a
+reduceAnd terms | not $ null [ e | e <- terms, e' <- map unot terms, e == e' ] = ubool False
+
+-- a == x && a == y && x /= y
+reduceAnd terms | or [ f a b | a <- terms, b <- terms ]                        = ubool False
+  where
+  f :: UE -> UE -> Bool
+  f (UEq a b) (UEq x y) | a == x = yep $ ueq b y
+                        | a == y = yep $ ueq b x
+                        | b == x = yep $ ueq a y
+                        | b == y = yep $ ueq a x
+  f _ _ = False
+  yep :: UE -> Bool
+  yep (UConst (CBool False)) = True
+  yep _ = False
+
+-- a && b && not (a && b)
+reduceAnd terms | not $ null [ e | e <- terms, not $ null $ f e, all (flip elem terms) $ f e ] = ubool False
+  where
+  f :: UE -> [UE]
+  f (UNot (UAnd a)) = a
+  f _               = []
+
+-- collect, sort, and return
+reduceAnd terms = UAnd $ sort $ nub $ terms
+
+uor :: UE -> UE -> UE
+uor a b = unot (uand (unot a) (unot b))
+
+ueq :: UE -> UE -> UE
+ueq a b | a == b = ubool True
+ueq (UConst (CBool   a)) (UConst (CBool   b)) = ubool $ a == b
+ueq (UConst (CInt8   a)) (UConst (CInt8   b)) = ubool $ a == b
+ueq (UConst (CInt16  a)) (UConst (CInt16  b)) = ubool $ a == b
+ueq (UConst (CInt32  a)) (UConst (CInt32  b)) = ubool $ a == b
+ueq (UConst (CInt64  a)) (UConst (CInt64  b)) = ubool $ a == b
+ueq (UConst (CWord8  a)) (UConst (CWord8  b)) = ubool $ a == b
+ueq (UConst (CWord16 a)) (UConst (CWord16 b)) = ubool $ a == b
+ueq (UConst (CWord32 a)) (UConst (CWord32 b)) = ubool $ a == b
+ueq (UConst (CWord64 a)) (UConst (CWord64 b)) = ubool $ a == b
+ueq (UConst (CFloat  a)) (UConst (CFloat  b)) = ubool $ a == b
+ueq (UConst (CDouble a)) (UConst (CDouble b)) = ubool $ a == b
+ueq a b = UEq a b
+
+ult :: UE -> UE -> UE
+ult a b | a == b = ubool False
+ult (UConst (CBool   a)) (UConst (CBool   b)) = ubool $ a < b
+ult (UConst (CInt8   a)) (UConst (CInt8   b)) = ubool $ a < b
+ult (UConst (CInt16  a)) (UConst (CInt16  b)) = ubool $ a < b
+ult (UConst (CInt32  a)) (UConst (CInt32  b)) = ubool $ a < b
+ult (UConst (CInt64  a)) (UConst (CInt64  b)) = ubool $ a < b
+ult (UConst (CWord8  a)) (UConst (CWord8  b)) = ubool $ a < b
+ult (UConst (CWord16 a)) (UConst (CWord16 b)) = ubool $ a < b
+ult (UConst (CWord32 a)) (UConst (CWord32 b)) = ubool $ a < b
+ult (UConst (CWord64 a)) (UConst (CWord64 b)) = ubool $ a < b
+ult (UConst (CFloat  a)) (UConst (CFloat  b)) = ubool $ a < b
+ult (UConst (CDouble a)) (UConst (CDouble b)) = ubool $ a < b
+ult a b = ULt a b
+
+umux :: UE -> UE -> UE -> UE
+umux _ t f | t == f = f
+umux b t f | ueType t == Bool = uor (uand b t) (uand (unot b) f)
+umux (UConst (CBool b)) t f = if b then t else f
+umux (UNot b) t f = umux b f t
+umux b1 (UMux b2 t _) f | b1 == b2 = umux b1 t f
+umux b1 t (UMux b2 _ f) | b1 == b2 = umux b1 t f
+umux b t f = UMux b t f
+
+{-
+-- | Balances mux trees in expression.  Reduces critical path at cost of additional logic.
+balance :: UE -> UE
+balance ue = case ue of
+  UVRef _      -> ue
+  UCust _ _    -> ue
+  UCast t a    -> UCast t (balance a)
+  UConst _     -> ue
+  UAdd a b     -> UAdd   (balance a) (balance b)
+  USub a b     -> USub   (balance a) (balance b)
+  UMul a b     -> UMul   (balance a) (balance b)
+  UDiv a b     -> UDiv   (balance a) (balance b)
+  UMod a b     -> UMod   (balance a) (balance b)
+  UNot a       -> UNot   (balance a)
+  UAnd a       -> UAnd   (map balance a)
+  UBWNot a     -> UBWNot (balance a)
+  UBWAnd a b   -> UBWAnd (balance a) (balance b)
+  UBWOr  a b   -> UBWOr  (balance a) (balance b)
+  UShift a n   -> UShift (balance a) n
+  UEq  a b     -> UEq    (balance a) (balance b)
+  ULt  a b     -> ULt    (balance a) (balance b)
+  UMux a t f   -> rotate $ umux a t' f'
+    where
+    t' = balance t
+    f' = balance f
+    depth :: UE -> Int
+    depth (UMux _ t f) = 1 + max (depth t) (depth f)
+    depth _            = 0
+    rotate :: UE -> UE
+    rotate ue = case ue of
+      UMux a1 t1@(UMux a2 t2 f2) f1 | depth t1 >= depth f1 + 2 -> umux (uand a1 a2) t2 (umux a1 f2 f1)
+      UMux a1 t1 f1@(UMux a2 t2 f2) | depth f1 >= depth t1 + 2 -> umux (uor  a1 a2) (umux a1 t1 t2) f2
+      _ -> ue
+-}
+
+-- Idea analyzing a pair of comparisons with one common operand: take to other two operands and construct the appropriate
+-- expression and check never.
+-- never (a == x) && (a == y)  =>  never (x == y)
+-- never (a == x) && (a <  y)  =>  never (x >= y)
+-- never (a == x) && (a /= y)  =>  never (x == y)
+-- never (a == x) || (a == y)  =>  never (x == y)
+{-
+isExclusiveCompare :: (ConstantCompare, ConstantCompare) -> Bool
+isExclusiveCompare a = case a of
+  (Equal a, Equal     b) -> a /= b
+  (Equal a, NotEqual  b) -> a == b
+  (Equal a, Less      b) -> a >= b
+  (Equal a, LessEqual b) -> a >  b
+  (Equal a, More      b) -> a <= b
+  (Equal a, MoreEqual b) -> a <  b
+
+  (NotEqual a, Equal     b) -> a == b
+  (NotEqual _, _)           -> False
+
+  (Less  a, Equal     b) -> a <= b
+  (Less  a, More      b) -> a <= b
+  (Less  a, MoreEqual b) -> a <= b
+  (Less  _, _)           -> False
+
+  (LessEqual  a, Equal     b) -> a <  b
+  (LessEqual  a, More      b) -> a <= b
+  (LessEqual  a, MoreEqual b) -> a <  b
+  (LessEqual  _, _)           -> False
+
+  (More  a, Equal     b) -> a >= b
+  (More  a, Less      b) -> a >= b
+  (More  a, LessEqual b) -> a >= b
+  (More  _, _)           -> False
+
+  (MoreEqual  a, Equal     b) -> a >  b
+  (MoreEqual  a, Less      b) -> a >= b
+  (MoreEqual  a, LessEqual b) -> a >  b
+  (MoreEqual  _, _)           -> False
+
+data ConstantCompare
+  = Equal     TermConst
+  | NotEqual  TermConst
+  | Less      TermConst
+  | LessEqual TermConst
+  | More      TermConst
+  | MoreEqual TermConst
+  deriving (Eq, Ord)
+-}
+
+--data NetList = NetList Int (IntMap UE)
diff --git a/Language/Atom/Language.hs b/Language/Atom/Language.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Language.hs
@@ -0,0 +1,206 @@
+-- | The Atom language.
+module Language.Atom.Language
+  (
+    module Language.Atom.Expressions
+  -- * Primary Language Containers
+  , Atom
+  -- * Hierarchical Rule Declarations
+  , atom
+  , period
+  , getPeriod
+  -- * Action Directives
+  , cond
+  , Assign (..)
+  , incr
+  , decr
+  -- ** Performance Constraints
+  --, required
+  --, priority
+  -- * Variable Declarations
+  , var
+  , bool
+  , int8
+  , int16
+  , int32
+  , int64
+  , word8
+  , word16
+  , word32
+  , word64
+  , float
+  , double
+  -- * Custom Actions
+  , action
+  -- * Assertions
+  , assert
+  -- * Probing
+  , probe
+  , probes
+  -- * Utilities
+  , Name
+  , liftIO
+  , path
+  , clock
+  ) where
+
+import Control.Monad.State hiding (join)
+import Data.Int
+import Data.List
+import Data.Word
+
+import Language.Atom.Elaboration hiding (Atom)
+import qualified Language.Atom.Elaboration as E
+import Language.Atom.Expressions
+
+infixr 1 <==
+
+-- | A Atom captures declarations including inputs, outputs, variables, and assertions
+--   and actions including guard conditions and variable assignments.
+type Atom = E.Atom
+
+-- | Creates a hierarical node, where each node could be a atomic rule.
+atom :: Name -> Atom a -> Atom a
+atom name design = do
+  name <- addName name
+  (g, parent) <- get
+  (a, (g, child)) <- liftIO $ buildAtom g name design
+  put (g, parent { atomSubs = atomSubs parent ++ [child] })
+  return a
+
+-- | Defines the period of execution of sub rules as a factor of the base rate of the system.
+--   Rule period is bound by the closest period assertion.  For example:
+--
+--   > period 10 $ period 2 a   -- Rules in 'a' have a period of 2, not 10.
+period :: Int -> Atom a -> Atom a
+period n _ | n <= 0 = error "ERROR: Execution period must be greater than 0."
+period n atom = do
+  (g, a) <- get
+  put (g { gPeriod = n }, a)
+  r <- atom
+  (g', a) <- get
+  put (g' { gPeriod = gPeriod g }, a)
+  return r
+
+-- | Returns the execution period of the current scope.
+getPeriod :: Atom Int
+getPeriod = do
+  (g, _) <- get
+  return $ gPeriod g
+
+-- | Returns the current atom heirarchical path.
+path :: Atom String
+path = do
+  (_, atom) <- get
+  return $ atomName atom
+
+-- | Boolean variable declaration.
+bool :: Name -> Bool -> Atom (V Bool)
+bool name init = var name $ CBool init
+
+-- | Int8 variable declaration.
+int8 :: Name -> Int8 -> Atom (V Int8)
+int8 name init = var name $ CInt8 init
+
+-- | Int16 variable declaration.
+int16 :: Name -> Int16 -> Atom (V Int16)
+int16 name init = var name $ CInt16 init
+
+-- | Int32 variable declaration.
+int32 :: Name -> Int32 -> Atom (V Int32)
+int32 name init = var name $ CInt32 init
+
+-- | Int64 variable declaration.
+int64 :: Name -> Int64 -> Atom (V Int64)
+int64 name init = var name $ CInt64 init
+
+-- | Word8 variable declaration.
+word8 :: Name -> Word8 -> Atom (V Word8)
+word8 name init = var name $ CWord8 init
+
+-- | Word16 variable declaration.
+word16 :: Name -> Word16 -> Atom (V Word16)
+word16 name init = var name $ CWord16 init
+
+-- | Word32 variable declaration.
+word32 :: Name -> Word32 -> Atom (V Word32)
+word32 name init = var name $ CWord32 init
+
+-- | Word64 variable declaration.
+word64 :: Name -> Word64 -> Atom (V Word64)
+word64 name init = var name $ CWord64 init
+
+-- | Float variable declaration.
+float :: Name -> Float -> Atom (V Float)
+float name init = var name $ CFloat init
+
+-- | Double variable declaration.
+double :: Name -> Double -> Atom (V Double)
+double name init = var name $ CDouble init
+
+-- | Declares an action.
+action :: ([String] -> String) -> [UE] -> Atom ()
+action f ues = do
+  (g, a) <- get
+  put (g, a { atomActions = atomActions a ++ [(f, ues)] })
+
+-- | Asserts expression must always be true.
+assert :: Name -> E Bool -> Atom ()
+assert name a = do
+  name <- addName name
+  (g, atom) <- get
+  put (g { gAsserts = gAsserts g ++ [(name, ue a)] }, atom)
+
+-- | Declares a probe.
+probe :: Expr a => Name -> E a -> Atom ()
+probe name a = do
+  (g, atom) <- get
+  put (g { gProbes = (name, eType a, rawBits a) : gProbes g }, atom)
+
+
+-- | Fetches all declared probes to current design point.
+probes :: Atom [(String, Type, E Word64)]
+probes = do
+  (g, _) <- get
+  return $ gProbes g
+
+
+-- | Increments a NumE 'V'.
+incr :: (Assign a, NumE a) => V a -> Atom ()
+incr a = a <== value a + 1
+
+-- | Decrements a NumE 'V'.
+decr :: (Assign a, NumE a) => V a -> Atom ()
+decr a = a <== value a - 1
+
+
+class Expr a => Assign a where
+  -- | Assigns a 'E' to a 'V'.
+  (<==) :: V a -> E a -> Atom ()
+  v <== e = do
+    (g, atom) <- get
+    put (g, atom { atomAssigns = (uv v, ue e) : atomAssigns atom })
+
+instance Assign Bool
+instance Assign Int8
+instance Assign Int16
+instance Assign Int32
+instance Assign Int64
+instance Assign Word8
+instance Assign Word16
+instance Assign Word32
+instance Assign Word64
+instance Assign Float
+instance Assign Double
+
+-- | Adds an enabling condition to an atom subtree of rules.
+--   This condition must be true before any rules in heirarchy
+--   are allowed to execute.
+cond :: E Bool -> Atom ()
+cond c = do
+  (g, atom) <- get
+  put (g, atom { atomEnable = uand (atomEnable atom) (ue c) })
+
+-- | Reference to the 64-bit free running clock.
+clock :: E Word64
+clock = Cust "globalClock"
+
diff --git a/Language/Atom/Scheduling.hs b/Language/Atom/Scheduling.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Scheduling.hs
@@ -0,0 +1,52 @@
+-- | Atom rule scheduling.
+module Language.Atom.Scheduling
+  ( schedule
+  ) where
+
+import Control.Monad
+import Data.List
+import Data.Maybe
+import Language.Atom.Code
+import Language.Atom.Elaboration
+import System.IO
+import Text.Printf
+
+schedule :: [Rule] -> IO (Maybe [[[Rule]]])
+schedule rules = do
+  putStrLn "Starting rule scheduling..."
+  hFlush stdout
+  putStrLn "Writing scheduling report: schedule.log"
+  writeFile "schedule.log" $ reportSchedule periods
+  hFlush stdout
+  return $ Just periods
+  where
+
+  periods = map spread $ zip [1..] $ map rulesWithPeriod [1 .. maxPeriod]  -- XXX No scheduling done.
+
+  maxPeriod = maximum $ map rulePeriod rules
+
+  rulesWithPeriod :: Int -> [Rule]
+  rulesWithPeriod p = [ r | r <- rules, rulePeriod r == p ]
+
+  spread :: (Int, [Rule]) -> [[Rule]]
+  spread (0, []) = []
+  spread (0, _)  = error "Scheduling.spread"
+  spread (period, rules) = take rulesInCycle rules : spread (period - 1, drop rulesInCycle rules)
+    where
+    rulesInCycle = (length rules `div` period) + (if length rules `mod` period > 0 then 1 else 0)
+
+
+reportSchedule :: [[[Rule]]] -> String
+reportSchedule s = "Rule Scheduling Report\n\n  Period  Cycle  Exprs  Rule\n  ------  -----  -----  ----\n" ++ (concatMap reportPeriod) (zip [1..] s) ++
+                   "                 -----\n" ++
+                   printf "                 %5i\n" (sum $ map ruleComplexity (concat (concat s)))
+
+reportPeriod (period, p) = concatMap (reportCycle period) (zip [0..] p)
+
+reportCycle period (cycle, c) = concatMap (reportRule period cycle) c
+
+reportRule :: Int -> Int -> Rule -> String
+reportRule period cycle rule = printf "  %6i  %5i  %5i  %s\n" period cycle (ruleComplexity rule) (show rule)
+
+
+
diff --git a/Language/Atom/Verify.hs b/Language/Atom/Verify.hs
new file mode 100644
--- /dev/null
+++ b/Language/Atom/Verify.hs
@@ -0,0 +1,214 @@
+module Language.Atom.Verify (verify) where
+
+import Data.Char
+import Data.Int
+import Data.List
+import Data.Ratio
+import Data.Word
+import System.Process
+
+import Language.Atom.Elaboration
+import Language.Atom.Expressions
+
+verify :: Int -> [[[Rule]]] -> [UV] -> (String, UE) -> IO Bool
+verify depth rules uvs (name, assert) = do
+  putStrLn $ "Checking assertion " ++ name ++ "..."
+  verify
+      
+  where
+  verify | assert == ubool True  = return True
+         | assert == ubool False = putStrLn ("Assertion failed trivially.") >> return False
+         | otherwise = do
+             --putStrLn yices
+             --putStrLn "***********************************************"
+             out <- readProcess "yices" ["-e"] yices
+             case parseYices out of
+               S "unsat" : _ -> return True
+               S "sat"   : vars' -> do
+                 let vars = map (parseVar uvs) vars'
+                 putStrLn ("Assertion failed.  See counter example: " ++ name ++ ".vcd")
+                 writeFile (name ++ ".vcd") $ vcd uvs vars
+                 return False
+               _         -> error "Unexpected results from yices."
+      
+  assertUE :: Int -> String
+  assertUE step = "(assert (not " ++ f ++ "))\n"
+    where
+    f = case assert of
+      UVRef uv -> uvName step uv
+      _        -> error "expressions not supported assertions yet"
+
+  asserts = concatMap assertUE [0..depth]
+  yices = initialize uvs ++ concatMap (transition rules uvs) [1..depth] ++ asserts ++ "(check)"
+
+yicesType :: Type -> String
+yicesType t = case t of
+  Bool   -> "bool"
+  Int8   -> "(bitvector  8)"
+  Int16  -> "(bitvector 16)"
+  Int32  -> "(bitvector 32)"
+  Int64  -> "(bitvector 64)"
+  Word8  -> "(bitvector  8)"
+  Word16 -> "(bitvector 16)"
+  Word32 -> "(bitvector 32)"
+  Word64 -> "(bitvector 64)"
+  Float  -> "real"
+  Double -> "real"
+
+vars :: [UV] -> Int -> String
+vars uvs step = concatMap (var step) uvs
+  where
+  var :: Int -> UV -> String
+  var step uv = "(define " ++ uvName step uv ++ "::" ++ yicesType (uvType uv) ++ ")\n"
+
+uvName :: Int -> UV -> String
+uvName step (UV i _ _) = "v" ++ show i ++ "_" ++ show step
+
+initialize :: [UV] -> String
+initialize uvs = vars uvs 0 ++ concatMap initialize uvs
+  where
+  initialize :: UV -> String
+  initialize uv@(UV _ _ c) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"
+  const :: Const -> String
+  const c = case c of
+    CBool   c -> if c then "true" else "false" 
+    CInt8   c -> "0b" ++ bits  8 (fromIntegral c)
+    CInt16  c -> "0b" ++ bits 16 (fromIntegral c)
+    CInt32  c -> "0b" ++ bits 32 (fromIntegral c)
+    CInt64  c -> "0b" ++ bits 64 (fromIntegral c)
+    CWord8  c -> "0b" ++ bits  8 (fromIntegral c)
+    CWord16 c -> "0b" ++ bits 16 (fromIntegral c)
+    CWord32 c -> "0b" ++ bits 32 (fromIntegral c)
+    CWord64 c -> "0b" ++ bits 64 (fromIntegral c)
+    CFloat  c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
+    CDouble c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
+
+  bits :: Int -> Word64 -> String
+  bits 0 _ = ""
+  bits n a = bits (n - 1) (div a 2) ++ show (mod a 2)
+
+-- Time 0 to 1 is step 1.
+transition :: [[[Rule]]] -> [UV] -> Int -> String
+transition _ {-schedule-} uvs step = vars uvs step ++ transition
+  where
+  transition = "; transition " ++ show (step - 1) ++ " to " ++ show step ++ "\n"  --XXX
+
+getUV :: [UV] -> Int -> UV
+getUV [] _ = error "Verify.getUV"
+getUV (uv@(UV i _ _):_) j | i == j = uv
+getUV (_:a) i = getUV a i
+
+
+parseVar :: [UV] -> Group -> (Int, UV, String)
+parseVar uvs (G [S "=", S name, value]) = (t, getUV uvs i, parseValue value)
+  where
+  (i', t') = break (== '_') $ tail name
+  i = read i'
+  t = read $ tail t'
+parseVar _ g = error $ "Verify.parseVar: " ++ show g
+
+parseValue :: Group -> String
+parseValue (S ('0':'b':a)) = "b" ++ a ++ " "
+parseValue (S "true")      = "1"
+parseValue (S "false")     = "0"
+parseValue (S v)           = "r" ++ v ++ " "
+parseValue (G [S "/", S n, S d]) = "r" ++ show (fromRational (read n % read d)) ++ " "
+parseValue a               = error $ "Verify.parseValue: " ++ show a
+
+
+data Group = G [Group] | S String deriving Show
+
+parseYices :: String -> [Group]
+parseYices = groups . tokens
+
+groups :: [String] -> [Group]
+groups [] = []
+groups ("(":a) = G (groups x) : groups y where (x, y) = split 0 [] a
+groups (a:b) = S a : groups b
+
+split :: Int -> [String] -> [String] -> ([String], [String])
+split 0 a (")":b) = (reverse a, b)
+split n a ("(":b) = split (n + 1) ("(" : a) b
+split n a (")":b) = split (n - 1) (")" : a) b
+split n a (b:c)   = split n (b:a) c
+split _ _ []      = error "Verify.split"
+
+tokens :: String -> [String]
+tokens [] = []
+tokens (a:b) | isSpace a = tokens b
+tokens ('(':b) = "(" : tokens b
+tokens (')':b) = ")" : tokens b
+tokens a = tokens' "" a
+
+tokens' :: String -> String -> [String]
+tokens' a [] = [reverse a]
+tokens' a c@(b:_) | isSpace b || elem b "()" = reverse a : tokens c
+tokens' a (b:c) = tokens' (b:a) c
+
+data Heirarchy = Variable UV | Module String [Heirarchy]
+
+vcd :: [UV] -> [(Int, UV, String)] -> String
+vcd uvs signals' = header ++ samples ++ end
+  where
+  signals = sortBy (\ (a,_,_) (b,_,_) -> compare a b) signals' 
+
+  header = "$timescale\n  1 ms\n$end\n" ++ concatMap decl (heirarchy 0 uvs) ++ "$enddefinitions $end\n"
+  (lastTime, _, _) = last signals
+  end = "#" ++ show (lastTime + 1) ++ "\n"
+
+  decl :: Heirarchy -> String
+  decl (Module name subs) = "$scope module " ++ name ++ " $end\n" ++ concatMap decl subs ++ "$upscope $end\n"
+  decl (Variable uv)      = declVar uv
+
+  declVar :: UV -> String
+  declVar uv@(UV i n _) = case uvType uv of
+    Bool   -> "$var wire 1 "     ++ code ++ " " ++ name ++ " $end\n"
+    Int8   -> "$var integer 8 "  ++ code ++ " " ++ name ++ " $end\n"
+    Int16  -> "$var integer 16 " ++ code ++ " " ++ name ++ " $end\n"
+    Int32  -> "$var integer 32 " ++ code ++ " " ++ name ++ " $end\n"
+    Int64  -> "$var integer 64 " ++ code ++ " " ++ name ++ " $end\n"
+    Word8  -> "$var wire 8 "     ++ code ++ " " ++ name ++ " $end\n"
+    Word16 -> "$var wire 16 "    ++ code ++ " " ++ name ++ " $end\n"
+    Word32 -> "$var wire 32 "    ++ code ++ " " ++ name ++ " $end\n"
+    Word64 -> "$var wire 64 "    ++ code ++ " " ++ name ++ " $end\n"
+    Float  -> "$var real 32 "    ++ code ++ " " ++ name ++ " $end\n"
+    Double -> "$var real 64 "    ++ code ++ " " ++ name ++ " $end\n"
+    where
+    code = vcdCode i
+    name = reverse $ takeWhile (/= '.') $ reverse n
+
+  samples = concatMap sample signals
+
+  sample (t, (UV i _ _), v) = "#" ++ show t ++ "\n" ++ v ++ vcdCode i ++ "\n"
+
+heirarchy :: Int -> [UV] -> [Heirarchy]
+heirarchy _ [] = []
+heirarchy depth uvs = heirarchy' depth notvars ++ map Variable vars
+  where
+  isVar :: UV -> Bool
+  isVar uv = length (path depth uv) == 1
+  (vars, notvars) = partition isVar uvs
+
+heirarchy' :: Int -> [UV] -> [Heirarchy]
+heirarchy' _ [] = []
+heirarchy' depth uvs@(a:_) = Module n (heirarchy (depth + 1) yes) : heirarchy' depth no
+  where
+  n = head $ path depth a
+  isMod uv = n == head (path depth uv)
+  (yes, no) = partition isMod uvs
+
+path :: Int -> UV -> [String]
+path depth (UV _ n _) = drop depth $ words $ map (\ c -> if c == '.' then ' ' else c) n
+ 
+vcdCode :: Int -> String
+vcdCode i | i < 94 =              [chr (33 + mod i 94)] 
+vcdCode i = vcdCode (div i 94) ++ [chr (33 + mod i 94)] 
+
+{-
+bitString :: Int -> String
+bitString n = if null bits then "0" else bits
+  where
+  bit :: Int -> Char
+  bit i = if testBit n i then '1' else '0'
+  bits = dropWhile (== '0') $ map bit $ reverse [0..31]
+-}
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/atom.cabal b/atom.cabal
new file mode 100644
--- /dev/null
+++ b/atom.cabal
@@ -0,0 +1,32 @@
+Name:           atom
+Version:        0.0.1
+Synopsis:       A DSL for embedded hard realtime applications.
+Description:    Atom is a Haskell DSL for designing hard realtime embedded programs.
+                Based on conditional term rewriting, atom will compile
+                a collection of atomic state transition rules
+                to a C program with constant memory use and deterministic execution time.
+License:        BSD3
+License-File:   LICENSE
+Author:         Tom Hawkins
+Maintainer:     tomahawkins@gmail.com
+Category:       Language
+Build-Type:     Simple
+Cabal-Version:  >= 1.2.3
+Extra-Source-Files:
+
+Library
+  Build-Depends:   base, mtl, process
+  Exposed-Modules:
+    Language.Atom,
+    Language.Atom.Code,
+    Language.Atom.Common,
+    Language.Atom.Compile,
+    Language.Atom.Elaboration,
+    Language.Atom.Expressions,
+    Language.Atom.Language,
+    Language.Atom.Scheduling,
+    Language.Atom.Verify
+  extensions:      GADTs
+  ghc-options:     -W
+  Other-Modules:   
+