atom 0.0.3 → 0.0.4

raw patch · 10 files changed

+270/−414 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/Atom/Code.hs +76/−53
• Language/Atom/Compile.hs +2/−9
• Language/Atom/Elaboration.hs +32/−20
• Language/Atom/Example.hs +4/−4
• Language/Atom/Expressions.hs +92/−82
• Language/Atom/Language.hs +18/−27
• Language/Atom/Scheduling.hs +35/−1
• Language/Atom/Verify.hs +0/−215
• RELEASE-NOTES +9/−0
• atom.cabal +2/−3

@@ -11,7 +11,9 @@ import Data.Char import Data.List import Data.Maybe+import Data.Word import System.IO+import Unsafe.Coerce  import Language.Atom.Elaboration import Language.Atom.Expressions@@ -34,30 +36,19 @@   , cPostCode = ""   } -declareMemory :: Config -> UV -> String-declareMemory config (UV id name (Local init)) = cType config (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-declareMemory _ (UV _ _ (External _)) = ""--declareUE :: Config -> String -> (UE, String) -> String-declareUE config d (ue, n) = case ue of-  UVRef _              -> ""-  UConst (CBool True ) -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = 1;\n"-  UConst (CBool False) -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = 0;\n"-  UConst c             -> d ++ "const " ++ cType config (ueType ue) ++ " " ++ n ++ " = " ++ show c ++ ";\n"-  _                    -> d ++             cType config (ueType ue) ++ " " ++ n ++ ";\n"+showConst :: Const -> String+showConst c = case c 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  -- | ANSI C type naming rules. cTypes :: Type -> String@@ -90,17 +81,15 @@   Double -> "double"  codeUE :: Config -> [(UE, String)] -> String -> (UE, String) -> String-codeUE config ues d (ue, n) = case ue of-  UConst _       -> ""-  UVRef _        -> ""-  _              -> d ++ n ++ " = " ++ basic operands ++ ";\n"+codeUE config ues d (ue, n) = d ++ cType config (typeOf ue) ++ " " ++ n ++ " = " ++ basic operands ++ ";\n"   where   operands = map (fromJust . flip lookup ues) $ ueUpstream ue   basic :: [String] -> String   basic operands = case ue of-    UVRef _              -> error "Code.ueStmt: should not get here."-    UCast _ _            -> "(" ++ cType config (ueType ue) ++ ") (" ++ a ++ ")"-    UConst _             -> error "Code.ueStmt: should not get here."+    UVRef (UV (Array ua@(UA _ n _) _)) -> arrayIndex config ua a ++ " /* " ++ n ++ " */ "+    UVRef (UV (External n _)) -> n+    UCast _ _            -> "(" ++ cType config (typeOf ue) ++ ") " ++ a+    UConst c             -> showConst c     UAdd _ _             ->  a ++ " + " ++ b     USub _ _             ->  a ++ " - " ++ b     UMul _ _             ->  a ++ " * " ++ b@@ -124,8 +113,8 @@     b = operands !! 1     c = operands !! 2 -writeC :: Name -> Config -> [[[Rule]]] -> [UV] -> IO ()-writeC name config periods uvs = do+writeC :: Name -> Config -> [[[Rule]]] -> ([Const], [Const], [Const], [Const]) -> IO ()+writeC name config periods (init8, init16, init32, init64) = do   putStrLn $ "Writing C code (" ++ name ++ ".c)..."   writeFile (name ++ ".c") c   putStrLn $ "Writing coverage data description (" ++ name' ++ "CoverageData.hs)..."@@ -134,11 +123,11 @@   name' = toUpper (head name) : tail name   c = unlines     [ cPreCode config-    , cType config Word64 ++ " __clock = 0;"-    , "const " ++ cType config Word32 ++ " __coverage_len = " ++ show covLen ++ ";"-    , cType config Word32 ++ " __coverage[" ++ show covLen ++ "] = {" ++ drop 2 (concat $ replicate covLen ", 0") ++ "};"-    , cType config Word32 ++ " __coverage_index = 0;"-    , concatMap (declareMemory config) uvs+    , "static " ++ cType config Word64 ++ " __clock = 0;"+    , "static const " ++ cType config Word32 ++ " __coverage_len = " ++ show covLen ++ ";"+    , "static " ++ cType config Word32 ++ " __coverage[" ++ show covLen ++ "] = {" ++ drop 2 (concat $ replicate covLen ", 0") ++ "};"+    , "static " ++ cType config Word32 ++ " __coverage_index = 0;"+    , memoryInit config Word8  init8 ++ memoryInit config Word16 init16 ++ memoryInit config Word32 init32 ++ memoryInit config Word64 init64     , concatMap (codeRule config topo') $ concat $ concat periods     , "void " ++ (if null (cFuncName config) then name else cFuncName config) ++ "(void) {"     , concatMap codePeriod $ zip [1..] periods@@ -157,29 +146,65 @@     , "coverageData = " ++ show [ (ruleName r, (div (ruleId r) 32, mod (ruleId r) 32)) | r <- rules ]     ] -  topo' = topo $ maximum (map (\ (UV i _ _) -> i) uvs) + 1+  topo' = topo 0   covLen = 1 + div (maximum $ map ruleId rules) 32 +memoryInit :: Config -> Type -> [Const] -> String+memoryInit _ _ [] = ""+memoryInit config t init = "static " ++ cType config t ++ " " ++ memory t ++ "[" ++ show (length init) ++ "] = {" ++ drop 2 (concat [", " ++ format a | a <- init ]) ++ "};\n"+  where+  format :: Const -> String+  format c = case c of+    CBool True  -> "1"+    CBool False -> "0"+    CInt8   a   -> show a+    CInt16  a   -> show a+    CInt32  a   -> show a+    CInt64  a   -> show a+    CWord8  a   -> show a+    CWord16 a   -> show a+    CWord32 a   -> show a+    CWord64 a   -> show a+    CFloat  a   -> show $ floatBits  a+    CDouble a   -> show $ doubleBits a++floatBits :: Float -> Word32+floatBits = unsafeCoerce++doubleBits :: Double -> Word64+doubleBits = unsafeCoerce++memory :: Width a => a -> String+memory a = "__memory" ++ show (if width a == 1 then 8 else width a)+ codeRule :: Config -> ([UE] -> [(UE, String)]) -> Rule -> String codeRule config topo rule =    "/* " ++ show rule ++ " */\n" ++-  "void __r" ++ show (ruleId rule) ++ "(void) {\n" ++-  concatMap (declareUE config     "  ") ues +++  "static void __r" ++ show (ruleId rule) ++ "(void) {\n" ++   concatMap (codeUE    config ues "  ") ues ++   "  if (" ++ id (ruleEnable rule) ++ ") {\n" ++   concatMap codeAction (ruleActions rule) ++   "    __coverage[" ++ covWord ++ "] = __coverage[" ++ covWord ++ "] | (1 << " ++ covBit ++ ");\n" ++   "  }\n" ++-  concatMap (\ (uv, ue) -> "  " ++ v uv ++ " = " ++ id ue ++ ";\n") (ruleAssigns rule) +++  concatMap codeAssign (ruleAssigns rule) ++   "}\n\n"   where-  ues = topo $ ruleEnable rule : snd (unzip (ruleAssigns rule)) ++ concat (snd (unzip (ruleActions rule)))+  ues = topo $ allUEs rule   id ue = fromJust $ lookup ue ues+   codeAction :: (([String] -> String), [UE]) -> String   codeAction (f, args) = "    " ++ f (map id args) ++ ";\n"+   covWord = show $ div (ruleId rule) 32   covBit  = show $ mod (ruleId rule) 32 +  codeAssign :: (UV, UE) -> String+  codeAssign (UV (Array ua@(UA _ n _) i), ue) = "  " ++ arrayIndex config ua (id i) ++ " = " ++ id ue ++ ";  /* " ++ n ++ " */\n"+  codeAssign (UV (External n _), ue) = "  " ++ n ++ " = " ++ id ue ++ ";\n"++arrayIndex :: Config -> UA -> String -> String+arrayIndex config (UA addr _ c) i = "((" ++ cType config (typeOf (head c)) ++ " *) (" ++ memory (head c) ++ " + " ++ show addr ++ "))[" ++ i ++ "]"+ codePeriod :: (Int, [[Rule]]) -> String codePeriod (period, cycles) = concatMap (codeCycle period) $ zip [0..] cycles @@ -194,9 +219,12 @@ e :: Int -> String e i = "__" ++ show i -v :: UV -> String-v (UV i _ (Local _)) = e i-v (UV _ n (External _)) = n+allUEs :: Rule -> [UE]+allUEs rule = ruleEnable rule : concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ] ++ concat (snd (unzip (ruleActions rule)))+  where+  index :: UV -> [UE]+  index (UV (Array _ ue)) = [ue]+  index _ = []  -- | Topologically sorts a list of expressions and subexpressions. topo :: Int -> [UE] -> [(UE, String)]@@ -205,14 +233,9 @@   (_, ues') = foldl collect (start, []) ues   collect :: (Int, [(UE, String)]) -> UE -> (Int, [(UE, String)])   collect (n, ues) ue | any ((== ue) . fst) ues = (n, ues)-  collect (n, ues) ue = case ue of-    UVRef (UV i _ (Local    _)) -> (n, (ue, e i) : ues)-    UVRef (UV _ a (External _)) -> (n, (ue, a)   : ues)-    _                -> (n' + 1, (ue, e n') : ues')-      where-      (n', ues') = foldl collect (n, ues) $ ueUpstream ue+  collect (n, ues) ue = (n' + 1, (ue, e 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)))+ruleComplexity rule = length $ topo 0 $ allUEs rule 

@@ -12,7 +12,6 @@ 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 -> Config -> Atom () -> IO ()@@ -20,18 +19,12 @@   r <- elaborate name atom   case r of     Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)-    Just (rules, uvs, _) -> do+    Just (rules, init) -> do       r <- schedule name 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 config schedule uvs+          writeC name config schedule init 

@@ -13,6 +13,7 @@   , elaborate   , var   , var'+  , array   , addName   , get   , put@@ -36,9 +37,11 @@ data Global = Global   { gId      :: Int   , gProbes  :: [(String, Type, E Word64)]-  , gUVs     :: [UV]+  , gInit8   :: [Const]+  , gInit16  :: [Const]+  , gInit32  :: [Const]+  , gInit64  :: [Const]   , gPeriod  :: Int-  , gAsserts :: [(String, UE)]   }  data AtomDB = AtomDB@@ -131,20 +134,17 @@ -- 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 () -> IO (Maybe ([Rule], ([Const], [Const], [Const], [Const]))) elaborate name atom = do   putStrLn "Starting atom elaboration..."   hFlush stdout-  (_, (g, atomDB)) <- buildAtom (Global { gId = 0, gProbes = [], gUVs = [], gPeriod = 1, gAsserts = [] }) name atom+  (_, (g, atomDB)) <- buildAtom (Global { gId = 0, gInit8 = [], gInit16 = [], gInit32 = [], gInit64 = [], gProbes = [], gPeriod = 1 }) name atom   let rules = reIdRules $ elaborateRules (ubool True) atomDB   mapM_ checkEnable rules   ok <- checkAssignConflicts atomDB   if not ok     then return Nothing-    else do-      let uvs = sort $ gUVs g-      ruleGraph name rules uvs-      return $ Just (rules, uvs, gAsserts g)+    else return $ Just (rules, (gInit8 g, gInit16 g, gInit32 g, gInit64 g))  checkEnable :: Rule -> IO () checkEnable rule | ruleEnable rule == ubool False = putStrLn $ "WARNING: Rule will never execute: " ++ show rule@@ -164,21 +164,32 @@   vars' = nub vars  -- | Generic local variable declaration.-var :: Name -> Const -> Atom (V a)-var name const = do-  name <- addName name-  (g, atom) <- get-  let uv = UV (gId g) name $ Local const-  put (g { gId = gId g  + 1, gUVs =  uv : gUVs g }, atom)-  return $ V uv+var :: Expr a => Name -> a -> Atom (V a)+var name init = do+  A a <- array name [init]+  return $ V $ UV $ Array a $ UConst $ CWord8 0  -- | Generic external variable declaration. var' :: Name -> Type -> Atom (V a)-var' name t = do+var' name t = return $ V $ UV $ External name t++-- | Generic array declaration.+array :: Expr a => Name -> [a] -> Atom (A a)+array name [] = error $ "ERROR: arrays can not be empty: " ++ name+array name init = do+  name <- addName name   (g, atom) <- get-  let uv = UV (gId g) name $ External t-  put (g { gId = gId g  + 1, gUVs =  uv : gUVs g }, atom)-  return $ V uv+  let constants = map constant init+      (addr, g') = case width $ head constants of+        1  -> (length $ gInit8  g, g { gInit8  = gInit8  g ++ constants })+        8  -> (length $ gInit8  g, g { gInit8  = gInit8  g ++ constants })+        16 -> (length $ gInit16 g, g { gInit16 = gInit16 g ++ constants })+        32 -> (length $ gInit32 g, g { gInit32 = gInit32 g ++ constants })+        64 -> (length $ gInit64 g, g { gInit64 = gInit64 g ++ constants })+        _  -> error "Elaboration.array: unknown width"+      ua = UA addr name constants+  put (g', atom)+  return $ A ua  addName :: Name -> Atom Name addName name = do@@ -189,6 +200,7 @@       put (g, atom { atomNames = name : atomNames atom })       return $ atomName atom ++ "." ++ name +{- ruleGraph :: Name -> [Rule] -> [UV] -> IO () ruleGraph name rules uvs = do   putStrLn $ "Writing rule graph (" ++ name ++ ".dot)..."@@ -214,4 +226,4 @@   ruleUVRefs r = nub $ concatMap uvSet ues     where     ues = ruleEnable r : snd (unzip (ruleAssigns r)) ++ concat (snd (unzip (ruleActions r)))-+-}

@@ -16,6 +16,7 @@   , "#include <stdio.h>"   , "unsigned long int a;"   , "unsigned long int b;"+  , "unsigned long int x;"   , "unsigned char running = 1;"   ] @@ -24,12 +25,12 @@   [ "int main(int argc, char* argv[]) {"   , "  a = atoi(argv[1]);"   , "  b = atoi(argv[2]);"-  , "  printf(\"Computing the GCD of %i and %i...\\n\", a, b);"+  , "  printf(\"Computing the GCD of %lu and %lu...\\n\", a, b);"   , "  while(running) {"   , "    example();"-  , "    printf(\"iteration:  a = %i  b = %i\\n\", a, b);"+  , "    printf(\"iteration:  a = %lu  b = %lu\\n\", a, b);"   , "  }"-  , "  printf(\"GCD result: %i\\n\", a);"+  , "  printf(\"GCD result: %lu\\n\", a);"   , "  return 0;"   , "}"   ]@@ -62,5 +63,4 @@   atom "stop" $ do     cond $ value a ==. value b     running <== false- 

@@ -6,20 +6,21 @@   , UE    (..)   , UV    (..)   , UVLocality (..)+  , A     (..)+  , UA    (..)   , Expr  (..)   , Expression (..)   , Variable   (..)   , Type  (..)   , Const (..)   , Width (..)-  , constType+  , TypeOf (..)+  , bytes   , ue   , uv-  , ueType-  , uvType   , ueUpstream-  , uvSet   , NumE+  , IntegralE   , FloatingE   , EqE   , OrdE@@ -53,6 +54,9 @@   , mod_   -- * Conditional Operator   , mux+  -- * Array Indexing+  , (!)+  , (!.)   -- * Smart constructors for untyped expressions.   , ubool   , unot@@ -71,6 +75,7 @@ --infixl 7 /., %. --infixl 6 +., -. --infixr 5 ++.+infixl 9 !, !. infix  4 ==., /=., <., <=., >., >=. infixl 3 &&. --, ^. -- , &&&, $&, $&& infixl 2 ||. -- , |||, $$, $:, $|@@ -120,20 +125,6 @@     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)@@ -164,14 +155,18 @@ -- | Variables updated by state transition rules. data V a = V UV deriving Eq --- | Unsigned variables.-data UV = UV Int String UVLocality deriving Show-instance Eq   UV where UV a _ _  == UV b _ _ = a == b-instance Ord  UV where compare (UV a _ _) (UV b _ _) = compare a b+-- | Untyped variables.+data UV = UV UVLocality deriving (Show, Eq, Ord)  -- | UV locality.-data UVLocality = Local Const | External Type deriving Show+data UVLocality = Array UA UE | External String Type deriving (Show, Eq, Ord) +-- | A typed array.+data A a = A UA deriving Eq++-- | An untyped array.+data UA = UA Int String [Const] deriving (Show, Eq, Ord)+ -- | A typed expression. data E a where   VRef    :: V a -> E a@@ -230,6 +225,9 @@ class Width a where   width :: a -> Int +bytes :: Width a => a -> Int+bytes a = div (width a) 8 + if mod (width a) 8 == 0 then 0 else 1+ instance Width Type where   width t = case t of     Bool   -> 1@@ -244,11 +242,69 @@     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+instance Width Const           where width = width . typeOf+instance Expr a => Width (E a) where width = width . typeOf+instance Expr a => Width (V a) where width = width . typeOf+instance Width UE              where width = width . typeOf +class TypeOf a where typeOf :: a -> Type++instance TypeOf Const where+  typeOf a = case a of+    CBool   _ -> Bool+    CInt8   _ -> Int8+    CInt16  _ -> Int16+    CInt32  _ -> Int32+    CInt64  _ -> Int64+    CWord8  _ -> Word8+    CWord16 _ -> Word16+    CWord32 _ -> Word32+    CWord64 _ -> Word64+    CFloat  _ -> Float+    CDouble _ -> Double++instance TypeOf UV where+  typeOf a = case a of+    UV (Array a _)  -> typeOf a+    UV (External _ t) -> t++instance TypeOf (V a) where+  typeOf (V uv) = typeOf uv++instance TypeOf UA where+  typeOf (UA _ _ c) = typeOf $ head c++instance TypeOf (A a) where+  typeOf (A ua) = typeOf ua++instance TypeOf UE where+  typeOf t = case t of+    UVRef uvar -> typeOf uvar+    UCast t _  -> t+    UConst c   -> typeOf c+    UAdd a _   -> typeOf a+    USub a _   -> typeOf a+    UMul a _   -> typeOf a+    UDiv a _   -> typeOf a+    UMod a _   -> typeOf a+    UNot _     -> Bool+    UAnd _     -> Bool+    UBWNot a   -> typeOf a+    UBWAnd a _ -> typeOf a+    UBWOr  a _ -> typeOf a+    UShift a _ -> typeOf a+    UEq  _ _   -> Bool+    ULt  _ _   -> Bool+    UMux _ a _ -> typeOf a+    UF2B _     -> Word32+    UD2B _     -> Word64+    UB2F _     -> Float+    UB2D _     -> Double++instance Expr a => TypeOf (E a) where+  typeOf = eType++ class Eq a => Expr a where   eType      :: E a -> Type   constant   :: a -> Const@@ -545,67 +601,21 @@ 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+-- | Array index to variable.+(!) :: (Expr a, IntegralE b) => A a -> E b -> V a+(A ua) ! e = V $ UV $ Array ua $ ue e -uvList :: UE -> [UV]-uvList t = case t of-  UVRef v      -> [v]-  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+-- | Array index to expression.+(!.) :: (Expr a, IntegralE b) => A a -> E b -> E a+a !. i = value $ a ! i -uvType :: UV -> Type-uvType (UV _ _ (Local c))    = constType c-uvType (UV _ _ (External t)) = t --- | The type of an UE.-ueType :: UE -> Type-ueType t = case t of-  UVRef uvar -> uvType uvar-  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 _   -> []+  UVRef (UV (Array _ ue))   -> [ue]+  UVRef (UV (External _ _)) -> []   UCast _ a   -> [a]   UConst _    -> []   UAdd a b    -> [a, b]@@ -741,7 +751,7 @@  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 b t f | typeOf 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

@@ -13,12 +13,10 @@   , Assign (..)   , incr   , decr-  -- ** Performance Constraints-  --, required-  --, priority   -- * Variable Declarations   , var   , var'+  , array   , bool   , bool'   , int8@@ -43,8 +41,6 @@   , double'   -- * Custom Actions   , action-  -- * Assertions-  , assert   -- * Probing   , probe   , probes@@ -108,7 +104,7 @@  -- | Local boolean variable declaration. bool :: Name -> Bool -> Atom (V Bool)-bool name init = var name $ CBool init+bool = var  -- | External boolean variable declaration. bool' :: Name -> Atom (V Bool)@@ -116,7 +112,7 @@  -- | Local int8 variable declaration. int8 :: Name -> Int8 -> Atom (V Int8)-int8 name init = var name $ CInt8 init+int8 = var  -- | External int8 variable declaration. int8' :: Name -> Atom (V Int8)@@ -124,7 +120,7 @@  -- | Local int16 variable declaration. int16 :: Name -> Int16 -> Atom (V Int16)-int16 name init = var name $ CInt16 init+int16 = var  -- | External int16 variable declaration. int16' :: Name -> Atom (V Int16)@@ -132,7 +128,7 @@  -- | Local int32 variable declaration. int32 :: Name -> Int32 -> Atom (V Int32)-int32 name init = var name $ CInt32 init+int32 = var  -- | External int32 variable declaration. int32' :: Name -> Atom (V Int32)@@ -140,7 +136,7 @@  -- | Local int64 variable declaration. int64 :: Name -> Int64 -> Atom (V Int64)-int64 name init = var name $ CInt64 init+int64 = var  -- | External int64 variable declaration. int64' :: Name -> Atom (V Int64)@@ -148,7 +144,7 @@  -- | Local word8 variable declaration. word8 :: Name -> Word8 -> Atom (V Word8)-word8 name init = var name $ CWord8 init+word8 = var  -- | External word8 variable declaration. word8' :: Name -> Atom (V Word8)@@ -156,7 +152,7 @@  -- | Local word16 variable declaration. word16 :: Name -> Word16 -> Atom (V Word16)-word16 name init = var name $ CWord16 init+word16 = var  -- | External word16 variable declaration. word16' :: Name -> Atom (V Word16)@@ -164,7 +160,7 @@  -- | Local word32 variable declaration. word32 :: Name -> Word32 -> Atom (V Word32)-word32 name init = var name $ CWord32 init+word32 = var  -- | External word32 variable declaration. word32' :: Name -> Atom (V Word32)@@ -172,7 +168,7 @@  -- | Local word64 variable declaration. word64 :: Name -> Word64 -> Atom (V Word64)-word64 name init = var name $ CWord64 init+word64 = var  -- | External word64 variable declaration. word64' :: Name -> Atom (V Word64)@@ -180,7 +176,7 @@  -- | Local float variable declaration. float :: Name -> Float -> Atom (V Float)-float name init = var name $ CFloat init+float = var  -- | External float variable declaration. float' :: Name -> Atom (V Float)@@ -188,7 +184,7 @@  -- | Local double variable declaration. double :: Name -> Double -> Atom (V Double)-double name init = var name $ CDouble init+double = var  -- | External double variable declaration. double' :: Name -> Atom (V Double)@@ -200,18 +196,13 @@   (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)+  if any (\ (n, _, _) -> name == n) $ gProbes g+    then error $ "ERROR: Duplicated probe name: " ++ name+    else put (g { gProbes = (name, eType a, rawBits a) : gProbes g }, atom)   -- | Fetches all declared probes to current design point.@@ -231,7 +222,7 @@   class Expr a => Assign a where-  -- | Assigns a 'E' to a 'V'.+  -- | Assign an 'E' to a 'V'.   (<==) :: V a -> E a -> Atom ()   v <== e = do     (g, atom) <- get@@ -259,11 +250,11 @@  -- | Reference to the 64-bit free running clock. clock :: E Word64-clock = value (V (UV (-1) "__clock" (External Word64)))+clock = value $ V $ UV $ External "__clock" Word64  -- | Rule coverage information.  (current coverage index, coverage data) nextCoverage :: Atom (E Word32, E Word32) nextCoverage = do   action (\_ -> "__coverage_index = (__coverage_index + 1) % __coverage_len") []-  return (value (V (UV (-2) "__coverage_index" (External Word32))), value (V (UV (-3) "__coverage[__coverage_index]" (External Word32))))+  return (value $ V $ UV $ External "__coverage_index" Word32, value $ V $ UV $ External "__coverage[__coverage_index]" Word32) 

@@ -39,7 +39,12 @@ 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)))+                   printf "                 %5i\n" (sum $ map ruleComplexity (concat (concat s))) ++ "\n" +++                   "Heirarchical Expression Count\n\n" +++                   "  Total   Local     Rule\n" +++                   "  ------  ------    ----\n" +++                   reportUsage "" (usage $ concat $ concat s) +++                   "\n"  reportPeriod (period, p) = concatMap (reportCycle period) (zip [0..] p) @@ -49,4 +54,33 @@ reportRule period cycle rule = printf "  %6i  %5i  %5i  %s\n" period cycle (ruleComplexity rule) (show rule)  +data Usage = Usage String Int [Usage] deriving Eq++instance Ord Usage where compare (Usage a _ _) (Usage b _ _) = compare a b++reportUsage :: String -> Usage -> String+reportUsage i node@(Usage name n subs) = printf "  %6i  %6i    %s\n" (totalComplexity node) n (i ++ name) ++ concatMap (reportUsage ("  " ++ i)) subs++totalComplexity :: Usage -> Int+totalComplexity (Usage _ n subs) = n + sum (map totalComplexity subs)++usage :: [Rule] -> Usage+usage rules = head $ foldl insertUsage [] $ map usage' rules++usage' :: Rule -> Usage+usage' rule = f $ split $ ruleName rule+  where+  f :: [String] -> Usage+  f [] = undefined+  f [name] = Usage name (ruleComplexity rule) []+  f (name:names) = Usage name 0 [f names]++split :: String -> [String]+split "" = []+split s = a : if null b then [] else split (tail b) where (a,b) = span (/= '.') s++insertUsage :: [Usage] -> Usage -> [Usage]+insertUsage [] u = [u]+insertUsage (a@(Usage n1 i1 s1) : rest) b@(Usage n2 i2 s2) | n1 == n2  = Usage n1 (max i1 i2) (sort $ foldl insertUsage s1 s2) : rest+                                                           | otherwise = a : insertUsage rest b 

@@ -1,215 +0,0 @@-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 _ _ (Local c)) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"-  initialize (UV _ _ (External _)) = ""-  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]--}

@@ -1,3 +1,12 @@+atom 0.0.4    05/19/2009++- Made local variables static in generated C.+- Added checking for duplicate probe names.+- Added hierarchical expression count report.+- Removed dot graph for rule-variable relationships.+- Added support for arrays.  See array, (!), and (!.).+  WARNING: No checks for index out of bounds or overlapping assignments.+ atom 0.0.3    05/05/2009  - Set build-depends: process >= 1.0.1.1 for readProcess

@@ -1,5 +1,5 @@ Name:           atom-Version:        0.0.3+Version:        0.0.4 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@@ -26,8 +26,7 @@     Language.Atom.Example,     Language.Atom.Expressions,     Language.Atom.Language,-    Language.Atom.Scheduling,-    Language.Atom.Verify+    Language.Atom.Scheduling   extensions:      GADTs   ghc-options:     -W   Other-Modules: