module Language.ImProve
(
E
, V
, AllE
, NumE
, Name
, true
, false
, constant
, zero
, ref
, not_
, (&&.)
, (||.)
, and_
, or_
, any_
, all_
, (-->)
, (==.)
, (/=.)
, (<.)
, (<=.)
, (>.)
, (>=.)
, min_
, minimum_
, max_
, maximum_
, limit
, (*.)
, (/.)
, div_
, mod_
, mux
, linear
, Stmt
, (-|)
, var
, var'
, bool
, bool'
, int
, int'
, float
, float'
, input
, global
, Assign (..)
, ifelse
, if_
, case_
, (==>)
, incr
, decr
, assume
, assert
, verify
, C.Target (..)
, code
, analyze
) where
import Control.Monad
import Language.ImProve.Core
import qualified Language.ImProve.Verify as V
import qualified Language.ImProve.Code as C
infixl 7 *., /., `div_`, `mod_`
infix 4 ==., /=., <., <=., >., >=.
infixl 3 &&.
infixl 2 ||.
infixr 1 -->
infixr 0 <==, ==>, -|
true :: E Bool
true = Const True
false :: E Bool
false = Const False
constant :: AllE a => a -> E a
constant = Const
not_ :: E Bool -> E Bool
not_ = Not
(&&.) :: E Bool -> E Bool -> E Bool
(&&.) = And
(||.) :: E Bool -> E Bool -> E Bool
(||.) = Or
and_ :: [E Bool] -> E Bool
and_ = foldl (&&.) true
or_ :: [E Bool] -> E Bool
or_ = foldl (||.) false
all_ :: (a -> E Bool) -> [a] -> E Bool
all_ f a = and_ $ map f a
any_ :: (a -> E Bool) -> [a] -> E Bool
any_ f a = or_ $ map f a
(-->) :: E Bool -> E Bool -> E Bool
a --> b = not_ a ||. b
(==.) :: AllE a => E a -> E a -> E Bool
(==.) = Eq
(/=.) :: AllE a => E a -> E a -> E Bool
a /=. b = not_ (a ==. b)
(<.) :: NumE a => E a -> E a -> E Bool
(<.) = Lt
(>.) :: NumE a => E a -> E a -> E Bool
(>.) = Gt
(<=.) :: NumE a => E a -> E a -> E Bool
(<=.) = Le
(>=.) :: NumE a => E a -> E a -> E Bool
(>=.) = Ge
min_ :: NumE a => E a -> E a -> E a
min_ a b = mux (a <=. b) a b
minimum_ :: NumE a => [E a] -> E a
minimum_ = foldl1 min_
max_ :: NumE a => E a -> E a -> E a
max_ a b = mux (a >=. b) a b
maximum_ :: NumE a => [E a] -> E a
maximum_ = foldl1 max_
limit :: NumE 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
(*.) :: NumE a => E a -> a -> E a
(*.) = Mul
(/.) :: E Float -> Float -> E Float
_ /. 0 = error "divide by zero (/.)"
a /. b = Div a b
div_ :: E Int -> Int -> E Int
div_ _ 0 = error "divide by zero (div_)"
div_ a b = Div a b
mod_ :: E Int -> Int -> E Int
mod_ _ 0 = error "divide by zero (mod_)"
mod_ a b = Mod a b
linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float
linear (x1, y1) (x2, y2) a = a *. slope + constant inter
where
slope = (y2 y1) / (x2 x1)
inter = y1 slope * x1
ref :: AllE a => V a -> E a
ref = Ref
mux :: AllE a => E Bool -> E a -> E a -> E a
mux = Mux
(-|) :: Name -> Stmt a -> Stmt a
name -| stmt = do
(id, path0, stmt0) <- get
put (id, path0 ++ [name], Null)
a <- stmt
(id, _, stmt1) <- get
put (id, path0, stmt0)
statement $ Label name stmt1
return a
get :: Stmt (Int, [Name], Statement)
get = Stmt $ \ a -> (a, a)
put :: (Int, [Name], Statement) -> Stmt ()
put s = Stmt $ \ _ -> ((), s)
getPath :: Stmt [Name]
getPath = do
(_, path, _) <- get
return path
var :: AllE a => Name -> a -> Stmt (V a)
var name init = do
path <- getPath
return $ V False (path ++ [name]) init
var' :: AllE a => Name -> E a -> Stmt (E a)
var' name value = do
a <- var name zero
a <== value
return $ ref a
input :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a
input _ path = ref $ V True path zero
global :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a
global _ path init = V False path init
bool :: Name -> Bool -> Stmt (V Bool)
bool = var
bool' :: Name -> E Bool -> Stmt (E Bool)
bool' name value = do
a <- bool name False
a <== value
return $ ref a
int :: Name -> Int -> Stmt (V Int)
int = var
int' :: Name -> E Int -> Stmt (E Int)
int' name value = do
a <- int name 0
a <== value
return $ ref a
float :: Name -> Float -> Stmt (V Float)
float = var
float' :: Name -> E Float -> Stmt (E Float)
float' name value = do
a <- float name 0
a <== value
return $ ref a
incr :: V Int -> Stmt ()
incr a = a <== ref a + 1
decr :: V Int -> Stmt ()
decr a = a <== ref a 1
data Stmt a = Stmt ((Int, [Name], Statement) -> (a, (Int, [Name], Statement)))
instance Monad Stmt where
return a = Stmt $ \ s -> (a, s)
(Stmt f1) >>= f2 = Stmt f3
where
f3 s1 = f4 s2
where
(a, s2) = f1 s1
Stmt f4 = f2 a
statement :: Statement -> Stmt ()
statement a = Stmt $ \ (id, path, statement) -> ((), (id, path, Sequence statement a))
evalStmt :: Int -> [Name] -> Stmt () -> (Int, [Name], Statement)
evalStmt id path (Stmt f) = snd $ f (id, path, Null)
class Assign a where (<==) :: V a -> E a -> Stmt ()
instance AllE a => Assign a where a <== b = statement $ Assign a b
assume :: Name -> E Bool -> Stmt ()
assume name a = do
(id, path, stmt) <- get
put (id + 1, path, Sequence stmt $ Label name $ Assume id a)
assert :: Name -> Int -> E Bool -> Stmt ()
assert name k proposition
| k < 1 = error $ "k-induction search depth must be > 0: " ++ name ++ " k = " ++ show k
| otherwise = do
(id, path, stmt) <- get
put (id + 1, path, Sequence stmt $ Label name $ Assert id k proposition)
ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
ifelse cond onTrue onFalse = do
(id0, path, stmt) <- get
let (id1, _, stmt1) = evalStmt id0 path onTrue
(id2, _, stmt2) = evalStmt id1 path onFalse
put (id2, path, stmt)
statement $ Branch cond stmt1 stmt2
if_ :: E Bool -> Stmt () -> Stmt()
if_ cond stmt = ifelse cond stmt $ return ()
case_ :: Case () -> Stmt ()
case_ (Case f) = f $ return ()
data Case a = Case (Stmt () -> Stmt ())
instance Monad Case where
return _ = Case id
(>>=) = undefined
(Case f1) >> (Case f2) = Case $ f1 . f2
(==>) :: E Bool -> Stmt () -> Case ()
a ==> s = Case $ ifelse a s
verify :: FilePath -> Stmt () -> IO ()
verify yices program = analyze (V.verify yices) program
code :: C.Target -> Name -> Stmt () -> IO ()
code target name program = analyze (C.code target name) program
analyze :: (Statement -> IO a) -> Stmt () -> IO a
analyze f program = f stmt
where
(_, _, stmt) = evalStmt 0 [] program