packages feed

atom (empty) → 0.0.1

raw patch · 12 files changed

+2019/−0 lines, 12 filesdep +basedep +mtldep +processsetup-changed

Dependencies added: base, mtl, process

Files

+ LICENSE view
@@ -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.
+ Language/Atom.hs view
@@ -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
+ Language/Atom/Code.hs view
@@ -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)))+
+ Language/Atom/Common.hs view
@@ -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+-}++
+ Language/Atom/Compile.hs view
@@ -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+
+ Language/Atom/Elaboration.hs view
@@ -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+
+ Language/Atom/Expressions.hs view
@@ -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)
+ Language/Atom/Language.hs view
@@ -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"+
+ Language/Atom/Scheduling.hs view
@@ -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)+++
+ Language/Atom/Verify.hs view
@@ -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]+-}
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ atom.cabal view
@@ -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:   +