Language/Atom/Verify.hs

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]
-}