{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where
import Copilot.Theorem.IL.Spec
import qualified Copilot.Core as C
import qualified Data.Map.Strict as Map
import Control.Monad.State
import Data.Char
import Data.List (find)
import Text.Printf
import GHC.Float (float2Double)
import Data.Typeable (Typeable)
ncSeq :: C.Id -> SeqId
ncSeq :: Id -> SeqId
ncSeq = forall r. PrintfType r => SeqId -> r
printf SeqId
"s%d"
ncLocal :: C.Name -> SeqId
ncLocal :: SeqId -> SeqId
ncLocal SeqId
s = SeqId
"l" forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isNumber) SeqId
s
ncExternVar :: C.Name -> SeqId
ncExternVar :: SeqId -> SeqId
ncExternVar SeqId
n = SeqId
"ext_" forall a. [a] -> [a] -> [a]
++ SeqId
n
ncUnhandledOp :: String -> String
ncUnhandledOp :: SeqId -> SeqId
ncUnhandledOp = forall a. a -> a
id
ncMux :: Integer -> SeqId
ncMux :: Integer -> SeqId
ncMux Integer
n = SeqId
"mux" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> SeqId
show Integer
n
translate :: C.Spec -> IL
translate :: Spec -> IL
translate = Bool -> Spec -> IL
translate' Bool
False
translateWithBounds :: C.Spec -> IL
translateWithBounds :: Spec -> IL
translateWithBounds = Bool -> Spec -> IL
translate' Bool
True
translate' :: Bool -> C.Spec -> IL
translate' :: Bool -> Spec -> IL
translate' Bool
b (C.Spec {[Stream]
specStreams :: Spec -> [Stream]
specStreams :: [Stream]
C.specStreams, [Property]
specProperties :: Spec -> [Property]
specProperties :: [Property]
C.specProperties}) = forall a. Bool -> Trans a -> a
runTrans Bool
b forall a b. (a -> b) -> a -> b
$ do
let modelInit :: [Expr]
modelInit = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Stream -> [Expr]
streamInit [Stream]
specStreams
[Expr]
mainConstraints <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Stream -> Trans Expr
streamRec [Stream]
specStreams
[Expr]
localConstraints <- Trans [Expr]
popLocalConstraints
Map SeqId ([Expr], Expr)
properties <- forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Property]
specProperties
(\(C.Property {SeqId
propertyName :: Property -> SeqId
propertyName :: SeqId
C.propertyName, Expr Bool
propertyExpr :: Property -> Expr Bool
propertyExpr :: Expr Bool
C.propertyExpr}) -> do
Expr
e' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr Bool
propertyExpr
[Expr]
propConds <- Trans [Expr]
popLocalConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqId
propertyName, ([Expr]
propConds, Expr
e')))
forall (m :: * -> *) a. Monad m => a -> m a
return IL
{ [Expr]
modelInit :: [Expr]
modelInit :: [Expr]
modelInit
, modelRec :: [Expr]
modelRec = [Expr]
mainConstraints forall a. [a] -> [a] -> [a]
++ [Expr]
localConstraints
, Map SeqId ([Expr], Expr)
properties :: Map SeqId ([Expr], Expr)
properties :: Map SeqId ([Expr], Expr)
properties
, inductive :: Bool
inductive = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Stream]
specStreams
}
bound :: Expr -> C.Type a -> Trans ()
bound :: forall a. Expr -> Type a -> Trans ()
bound Expr
s Type a
t = case Type a
t of
Type a
C.Int8 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int8
C.Int8
Type a
C.Int16 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int16
C.Int16
Type a
C.Int32 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int32
C.Int32
Type a
C.Int64 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int64
C.Int64
Type a
C.Word8 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word8
C.Word8
Type a
C.Word16 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word16
C.Word16
Type a
C.Word32 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word32
C.Word32
Type a
C.Word64 -> forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word64
C.Word64
Type a
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()
bound' :: forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type a
t = do
Bool
b <- TransST -> Bool
addBounds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b forall a b. (a -> b) -> a -> b
$ Expr -> Trans ()
localConstraint (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
And
(Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Le (forall a. Type a -> a -> Expr
trConst Type a
t forall a. Bounded a => a
minBound) Expr
s)
(Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Ge (forall a. Type a -> a -> Expr
trConst Type a
t forall a. Bounded a => a
maxBound) Expr
s))
streamInit :: C.Stream -> [Expr]
streamInit :: Stream -> [Expr]
streamInit (C.Stream { streamId :: Stream -> Id
C.streamId = Id
id
, streamBuffer :: ()
C.streamBuffer = [a]
b :: [val]
, streamExprType :: ()
C.streamExprType = Type a
t }) =
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Integer -> a -> Expr
initConstraint [Integer
0..] [a]
b
where
initConstraint :: Integer -> val -> Expr
initConstraint :: Integer -> a -> Expr
initConstraint Integer
p a
v = Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq
(Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (Integer -> SeqIndex
Fixed Integer
p))
forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a -> Expr
trConst Type a
t a
v
streamRec :: C.Stream -> Trans Expr
streamRec :: Stream -> Trans Expr
streamRec (C.Stream { streamId :: Stream -> Id
C.streamId = Id
id
, streamExpr :: ()
C.streamExpr = Expr a
e
, streamBuffer :: ()
C.streamBuffer = [a]
b
, streamExprType :: ()
C.streamExprType = Type a
t })
= do
let s :: Expr
s = Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (forall a. Integral a => a -> SeqIndex
_n_plus forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Id
length [a]
b)
forall a. Expr -> Type a -> Trans ()
bound Expr
s Type a
t
Expr
e' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq Expr
s Expr
e'
expr :: Typeable a => C.Expr a -> Trans Expr
expr :: forall a. Typeable a => Expr a -> Trans Expr
expr (C.Const Type a
t a
v) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a -> Expr
trConst Type a
t a
v
expr (C.Label Type a
_ SeqId
_ Expr a
e) = forall a. Typeable a => Expr a -> Trans Expr
expr Expr a
e
expr (C.Drop Type a
t Word32
k Id
id) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (forall a. Integral a => a -> SeqIndex
_n_plus Word32
k)
expr (C.Local Type a1
ta Type a
_ SeqId
name Expr a1
ea Expr a
eb) = do
Expr
ea' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
ea
Expr -> Trans ()
localConstraint (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq (Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a1
ta) (SeqId -> SeqId
ncLocal SeqId
name) SeqIndex
_n_) Expr
ea')
forall a. Typeable a => Expr a -> Trans Expr
expr Expr a
eb
expr (C.Var Type a
t SeqId
name) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a
t) (SeqId -> SeqId
ncLocal SeqId
name) SeqIndex
_n_
expr (C.ExternVar Type a
t SeqId
name Maybe [a]
_) = forall a. Expr -> Type a -> Trans ()
bound Expr
s Type a
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
s
where
s :: Expr
s = Type -> SeqId -> SeqIndex -> Expr
SVal (forall a. Type a -> Type
trType Type a
t) (SeqId -> SeqId
ncExternVar SeqId
name) SeqIndex
_n_
expr (C.Op1 (C.Sign Type a1
ta) Expr a1
e) = case Type a1
ta of
Type a1
C.Int8 -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
C.Int16 -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
C.Int32 -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
C.Int64 -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
C.Float -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
C.Double -> forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a1
ta Expr a1
e
Type a1
_ -> forall a. Typeable a => Expr a -> Trans Expr
expr forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a1
ta a1
1
where
trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr
trSign :: forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> Trans Expr
trSign Type a
ta Expr a
e =
forall a. Typeable a => Expr a -> Trans Expr
expr (forall a1 b c a.
(Typeable a1, Typeable b, Typeable c) =>
Op3 a1 b c a -> Expr a1 -> Expr b -> Expr c -> Expr a
C.Op3 (forall b. Type b -> Op3 Bool b b b
C.Mux Type a
ta)
(forall a1 b a.
(Typeable a1, Typeable b) =>
Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
C.Op2 (forall a. Ord a => Type a -> Op2 a a Bool
C.Lt Type a
ta) Expr a
e (forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
0))
(forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta (-a
1))
(forall a1 b c a.
(Typeable a1, Typeable b, Typeable c) =>
Op3 a1 b c a -> Expr a1 -> Expr b -> Expr c -> Expr a
C.Op3 (forall b. Type b -> Op3 Bool b b b
C.Mux Type a
ta)
(forall a1 b a.
(Typeable a1, Typeable b) =>
Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
C.Op2 (forall a. Ord a => Type a -> Op2 a a Bool
C.Gt Type a
ta) Expr a
e (forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
0))
(forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
1)
(forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
0)))
expr (C.Op1 (C.Sqrt Type a1
_) Expr a1
e) = do
Expr
e' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Real Op2
Pow Expr
e' (Double -> Expr
ConstR Double
0.5)
expr (C.Op1 (C.Cast Type a1
_ Type a
_) Expr a1
e) = forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
e
expr (C.Op1 Op1 a1 a
op Expr a1
e) = do
Expr
e' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Op1 -> Expr -> Expr
Op1 Type
t' Op1
op' Expr
e'
where
(Op1
op', Type
t') = forall a b. Op1 a b -> (Op1, Type)
trOp1 Op1 a1 a
op
expr (C.Op2 (C.Ne Type a1
t) Expr a1
e1 Expr b
e2) = do
Expr
e1' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
e1
Expr
e2' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr b
e2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
t' Op2
Eq Expr
e1' Expr
e2')
where
t' :: Type
t' = forall a. Type a -> Type
trType Type a1
t
expr (C.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2) = do
Expr
e1' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
e1
Expr
e2' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr b
e2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
t' Op2
op' Expr
e1' Expr
e2'
where
(Op2
op', Type
t') = forall a b c. Op2 a b c -> (Op2, Type)
trOp2 Op2 a1 b a
op
expr (C.Op3 (C.Mux Type b
t) Expr a1
cond Expr b
e1 Expr c
e2) = do
Expr
cond' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr a1
cond
Expr
e1' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr b
e1
Expr
e2' <- forall a. Typeable a => Expr a -> Trans Expr
expr Expr c
e2
Expr -> Type -> Expr -> Expr -> Trans Expr
newMux Expr
cond' (forall a. Type a -> Type
trType Type b
t) Expr
e1' Expr
e2'
trConst :: C.Type a -> a -> Expr
trConst :: forall a. Type a -> a -> Expr
trConst Type a
t a
v = case Type a
t of
Type a
C.Bool -> Bool -> Expr
ConstB a
v
Type a
C.Float -> Double -> Expr
negifyR (Float -> Double
float2Double a
v)
Type a
C.Double -> Double -> Expr
negifyR a
v
t :: Type a
t@Type a
C.Int8 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Int16 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Int32 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Int64 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Word8 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Word16 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Word32 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
t :: Type a
t@Type a
C.Word64 -> forall a. Integral a => a -> Type -> Expr
negifyI a
v (forall a. Type a -> Type
trType Type a
t)
where
negifyR :: Double -> Expr
negifyR :: Double -> Expr
negifyR Double
v
| Double
v forall a. Ord a => a -> a -> Bool
>= Double
0 = Double -> Expr
ConstR Double
v
| Bool
otherwise = Type -> Op1 -> Expr -> Expr
Op1 Type
Real Op1
Neg forall a b. (a -> b) -> a -> b
$ Double -> Expr
ConstR forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ Double
v
negifyI :: Integral a => a -> Type -> Expr
negifyI :: forall a. Integral a => a -> Type -> Expr
negifyI a
v Type
t
| a
v forall a. Ord a => a -> a -> Bool
>= a
0 = Type -> Integer -> Expr
ConstI Type
t forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger a
v
| Bool
otherwise = Type -> Op1 -> Expr -> Expr
Op1 Type
t Op1
Neg forall a b. (a -> b) -> a -> b
$ Type -> Integer -> Expr
ConstI Type
t forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger a
v
trOp1 :: C.Op1 a b -> (Op1, Type)
trOp1 :: forall a b. Op1 a b -> (Op1, Type)
trOp1 = \case
Op1 a b
C.Not -> (Op1
Not, Type
Bool)
C.Abs Type a
t -> (Op1
Abs, forall a. Type a -> Type
trType Type a
t)
C.Exp Type a
t -> (Op1
Exp, forall a. Type a -> Type
trType Type a
t)
C.Log Type a
t -> (Op1
Log, forall a. Type a -> Type
trType Type a
t)
C.Sin Type a
t -> (Op1
Sin, forall a. Type a -> Type
trType Type a
t)
C.Tan Type a
t -> (Op1
Tan, forall a. Type a -> Type
trType Type a
t)
C.Cos Type a
t -> (Op1
Cos, forall a. Type a -> Type
trType Type a
t)
C.Asin Type a
t -> (Op1
Asin, forall a. Type a -> Type
trType Type a
t)
C.Atan Type a
t -> (Op1
Atan, forall a. Type a -> Type
trType Type a
t)
C.Acos Type a
t -> (Op1
Acos, forall a. Type a -> Type
trType Type a
t)
C.Sinh Type a
t -> (Op1
Sinh, forall a. Type a -> Type
trType Type a
t)
C.Tanh Type a
t -> (Op1
Tanh, forall a. Type a -> Type
trType Type a
t)
C.Cosh Type a
t -> (Op1
Cosh, forall a. Type a -> Type
trType Type a
t)
C.Asinh Type a
t -> (Op1
Asinh, forall a. Type a -> Type
trType Type a
t)
C.Atanh Type a
t -> (Op1
Atanh, forall a. Type a -> Type
trType Type a
t)
C.Acosh Type a
t -> (Op1
Acosh, forall a. Type a -> Type
trType Type a
t)
Op1 a b
_ -> forall a. HasCallStack => SeqId -> a
error SeqId
"Unsupported unary operator in input."
trOp2 :: C.Op2 a b c -> (Op2, Type)
trOp2 :: forall a b c. Op2 a b c -> (Op2, Type)
trOp2 = \case
Op2 a b c
C.And -> (Op2
And, Type
Bool)
Op2 a b c
C.Or -> (Op2
Or, Type
Bool)
C.Add Type a
t -> (Op2
Add, forall a. Type a -> Type
trType Type a
t)
C.Sub Type a
t -> (Op2
Sub, forall a. Type a -> Type
trType Type a
t)
C.Mul Type a
t -> (Op2
Mul, forall a. Type a -> Type
trType Type a
t)
C.Mod Type a
t -> (Op2
Mod, forall a. Type a -> Type
trType Type a
t)
C.Fdiv Type a
t -> (Op2
Fdiv, forall a. Type a -> Type
trType Type a
t)
C.Pow Type a
t -> (Op2
Pow, forall a. Type a -> Type
trType Type a
t)
C.Eq Type a
_ -> (Op2
Eq, Type
Bool)
C.Le Type a
t -> (Op2
Le, forall a. Type a -> Type
trType Type a
t)
C.Ge Type a
t -> (Op2
Ge, forall a. Type a -> Type
trType Type a
t)
C.Lt Type a
t -> (Op2
Lt, forall a. Type a -> Type
trType Type a
t)
C.Gt Type a
t -> (Op2
Gt, forall a. Type a -> Type
trType Type a
t)
Op2 a b c
_ -> forall a. HasCallStack => SeqId -> a
error SeqId
"Unsupported binary operator in input."
trType :: C.Type a -> Type
trType :: forall a. Type a -> Type
trType = \case
Type a
C.Bool -> Type
Bool
Type a
C.Int8 -> Type
SBV8
Type a
C.Int16 -> Type
SBV16
Type a
C.Int32 -> Type
SBV32
Type a
C.Int64 -> Type
SBV64
Type a
C.Word8 -> Type
BV8
Type a
C.Word16 -> Type
BV16
Type a
C.Word32 -> Type
BV32
Type a
C.Word64 -> Type
BV64
Type a
C.Float -> Type
Real
Type a
C.Double -> Type
Real
data TransST = TransST
{ TransST -> [Expr]
localConstraints :: [Expr]
, TransST -> [(Expr, (Expr, Type, Expr, Expr))]
muxes :: [(Expr, (Expr, Type, Expr, Expr))]
, TransST -> Integer
nextFresh :: Integer
, TransST -> Bool
addBounds :: Bool
}
newMux :: Expr -> Type -> Expr -> Expr -> Trans Expr
newMux :: Expr -> Type -> Expr -> Expr -> Trans Expr
newMux Expr
c Type
t Expr
e1 Expr
e2 = do
[(Expr, (Expr, Type, Expr, Expr))]
ms <- TransST -> [(Expr, (Expr, Type, Expr, Expr))]
muxes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
==(Expr, Type, Expr, Expr)
mux) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Expr, (Expr, Type, Expr, Expr))]
ms of
Maybe (Expr, (Expr, Type, Expr, Expr))
Nothing -> do
Integer
f <- Trans Integer
fresh
let v :: Expr
v = Type -> SeqId -> SeqIndex -> Expr
SVal Type
t (Integer -> SeqId
ncMux Integer
f) SeqIndex
_n_
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st { muxes :: [(Expr, (Expr, Type, Expr, Expr))]
muxes = (Expr
v, (Expr, Type, Expr, Expr)
mux) forall a. a -> [a] -> [a]
: [(Expr, (Expr, Type, Expr, Expr))]
ms }
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
Just (Expr
v, (Expr, Type, Expr, Expr)
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
where
mux :: (Expr, Type, Expr, Expr)
mux = (Expr
c, Type
t, Expr
e1, Expr
e2)
getMuxes :: Trans [Expr]
getMuxes :: Trans [Expr]
getMuxes = TransST -> [(Expr, (Expr, Type, Expr, Expr))]
muxes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Expr, (Expr, b, Expr, Expr)) -> [Expr]
toConstraints)
where
toConstraints :: (Expr, (Expr, b, Expr, Expr)) -> [Expr]
toConstraints (Expr
v, (Expr
c, b
_, Expr
e1, Expr
e2)) =
[ Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Or (Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not Expr
c) (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq Expr
v Expr
e1)
, Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Or Expr
c (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq Expr
v Expr
e2)
]
type Trans = State TransST
fresh :: Trans Integer
fresh :: Trans Integer
fresh = do
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {nextFresh :: Integer
nextFresh = TransST -> Integer
nextFresh TransST
st forall a. Num a => a -> a -> a
+ Integer
1}
TransST -> Integer
nextFresh forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
localConstraint :: Expr -> Trans ()
localConstraint :: Expr -> Trans ()
localConstraint Expr
c =
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {localConstraints :: [Expr]
localConstraints = Expr
c forall a. a -> [a] -> [a]
: TransST -> [Expr]
localConstraints TransST
st}
popLocalConstraints :: Trans [Expr]
popLocalConstraints :: Trans [Expr]
popLocalConstraints = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. [a] -> [a] -> [a]
(++) (TransST -> [Expr]
localConstraints forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get) Trans [Expr]
getMuxes
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {localConstraints :: [Expr]
localConstraints = [], muxes :: [(Expr, (Expr, Type, Expr, Expr))]
muxes = []})
runTrans :: Bool -> Trans a -> a
runTrans :: forall a. Bool -> Trans a -> a
runTrans Bool
b Trans a
m = forall s a. State s a -> s -> a
evalState Trans a
m forall a b. (a -> b) -> a -> b
$ [Expr]
-> [(Expr, (Expr, Type, Expr, Expr))] -> Integer -> Bool -> TransST
TransST [] [] Integer
0 Bool
b