atom 0.1.3 → 0.1.4

raw patch · 6 files changed

+23/−239 lines, 6 filesdep −yicesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: yices

API changes (from Hackage documentation)

Files

• Language/Atom.hs +8/−6
• Language/Atom/Code.hs +2/−10
• Language/Atom/Language.hs +5/−0
• Language/Atom/Verification.hs +0/−219
• RELEASE-NOTES +6/−0
• atom.cabal +2/−4

@@ -1,8 +1,12 @@ {- |-  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.+  Atom is a Haskell DSL for designing hard realtime embedded software.+  Based on guarded atomic actions (similar to STM), Atom enables highly+  concurrent programming without the need for mutex locking.+  In addition, Atom performs compile-time task scheduling and generates code+  with deterministic execution time and constant memory use, simplifying the+  process of timing verification and memory consumption in hard realtime+  applications. Without mutex locking and run-time task scheduling,+  Atom eliminates the need and overhead of RTOSs for many embedded applications. -}  module Language.Atom@@ -11,7 +15,6 @@   , module Language.Atom.Common   , module Language.Atom.Language   , module Language.Atom.Unit-  , module Language.Atom.Verification   ) where  import Language.Atom.Code@@ -19,4 +22,3 @@ import Language.Atom.Common import Language.Atom.Language import Language.Atom.Unit-import Language.Atom.Verification

@@ -12,10 +12,8 @@ import Data.List import Data.Maybe import Data.Function-import Data.Word import System.IO import Text.Printf-import Unsafe.Coerce  import Language.Atom.Analysis import Language.Atom.Elaboration@@ -181,14 +179,8 @@   CWord16 a   -> show a   CWord32 a   -> show a ++ "UL"   CWord64 a   -> show a ++ "ULL"-  CFloat  a   -> show $ floatBits  a-  CDouble a   -> show $ doubleBits a--floatBits :: Float -> Word32-floatBits = unsafeCoerce--doubleBits :: Double -> Word64-doubleBits = unsafeCoerce+  CFloat  a   -> show a ++ "F"+  CDouble a   -> show a  codeRule :: Config -> Rule -> String codeRule config rule@(Rule _ _ _ _ _ _ _) =

@@ -44,6 +44,7 @@   , double'   -- * Custom Actions   , action+  , call   -- * Probing   , probe   , probes@@ -223,6 +224,10 @@ action f ues = do   (g, a) <- get   put (g, a { atomActions = atomActions a ++ [(f, ues)] })++-- | Calls an external C function of type 'void f(void)'.+call :: Name -> Atom ()+call n = action (\ _ -> n ++ "()") []  -- | Declares a probe. probe :: Expr a => Name -> E a -> Atom ()

@@ -1,219 +0,0 @@-module Language.Atom.Verification-  ( Model-  , model-  -- , verify-  -- , kInduction-  -- , boundedModelChecking-  , test-  ) where--import Data.Char ()-import Data.Function ()-import Data.Int ()-import Data.List ()-import Data.Ratio ()-import Data.Word ()-import Math.SMT.Yices.Pipe-import Math.SMT.Yices.Syntax-import System.Process ()--import Language.Atom.Elaboration ()-import Language.Atom.Expressions-import Language.Atom.Scheduling---- | A model of a scheduled program for model checking.-data Model = Model-  --{ transition :: Int -> [Name] -> ([CmdY], [CmdY])-  --, names :: [(Name, Int)]-  --, -  --}---- | Create a model from a scheduled program.-model :: Schedule -> [UV] -> [UA] -> Model -model _ _ _ = Model---- | A list of assertions captured by a model.---assertions :: Model -> [Name]---- | Bounded model checking starting from the initial state.---boundedModelChecking :: Model -> Int -> Name -> IO (Maybe Witness)---- | K-induction model checking given a min and a max k-depth.---kInduction :: Model -> Int -> Int -> Name -> IO ()---test :: IO ()-test = do-  print test-  result <- runY test-  print result-  where-  test =-    [ DEFINE ("a", VarT "int") Nothing-    , DEFINE ("b", VarT "int") Nothing-    , ASSERT (VarE "a" := VarE "b")-    -- , ASSERT (YNe (YVar "a") (YVar "b"))-    ]-  --- | Runs a Yices program.  Returns a list of variable values if satisfiable.-runY :: [CmdY] -> IO ResY-runY a = do-  p <- createYicesPipe "yices" []-  runCmdsY p a-  r <- checkY p-  exitY p-  return r----{--yType :: Type -> YT-yType t = case t of-  Bool   -> YBool-  Int8   -> YInt-  Int16  -> YInt-  Int32  -> YInt-  Int64  -> YInt-  Word8  -> YNat-  Word16 -> YNat-  Word32 -> YNat-  Word64 -> YNat-  Float  -> YReal-  Double -> YReal--}--{--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 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,9 @@+atom 0.1.4    12/16/2009++- Added 'call' function. +- Bug fix to float and double variable initialization.+- Moved Language.Atom.Verification to new project: afv.+ atom 0.1.3    12/03/2009  - Added linear lookup (Common). 

@@ -1,5 +1,5 @@ name:    atom-version: 0.1.3+version: 0.1.4  category: Language @@ -35,8 +35,7 @@     build-depends:         base       >= 4       && < 5,         mtl        >= 1.1.0.1 && < 1.2,-        process    >= 1.0.1.1 && < 1.2,-        yices      >= 0.0.0.4+        process    >= 1.0.1.1 && < 1.2      exposed-modules:         Language.Atom@@ -50,7 +49,6 @@         Language.Atom.Language         Language.Atom.Scheduling         Language.Atom.Unit-        Language.Atom.Verification      extensions: GADTs