{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Translate Copilot specifications into IL specifications.
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       (forM, liftM2, when)
import Control.Monad.State

import Data.Char
import Data.List (find)

import Text.Printf

import GHC.Float (float2Double)

import Data.Typeable (Typeable)

-- 'nc' stands for naming convention.
ncSeq :: C.Id -> SeqId
ncSeq :: Id -> SeqId
ncSeq = SeqId -> Id -> SeqId
forall r. PrintfType r => SeqId -> r
printf SeqId
"s%d"

-- We assume all local variables have distinct names whatever their scopes.
ncLocal :: C.Name -> SeqId
ncLocal :: SeqId -> SeqId
ncLocal SeqId
s = SeqId
"l" SeqId -> SeqId -> SeqId
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> SeqId -> SeqId
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
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_" SeqId -> SeqId -> SeqId
forall a. [a] -> [a] -> [a]
++ SeqId
n

ncUnhandledOp :: String -> String
ncUnhandledOp :: SeqId -> SeqId
ncUnhandledOp = SeqId -> SeqId
forall a. a -> a
id

ncMux :: Integer -> SeqId
ncMux :: Integer -> SeqId
ncMux Integer
n = SeqId
"mux" SeqId -> SeqId -> SeqId
forall a. [a] -> [a] -> [a]
++ Integer -> SeqId
forall a. Show a => a -> SeqId
show Integer
n

-- | Translate a Copilot specification to an IL specification.
translate :: C.Spec -> IL
translate :: Spec -> IL
translate = Bool -> Spec -> IL
translate' Bool
False

-- | Translate a Copilot specification to an IL specification, adding
-- constraints for limiting the values of numeric expressions to known bounds
-- based on their specific types (only for integers or natural numbers).
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 :: [Stream]
specStreams :: Spec -> [Stream]
C.specStreams, [Property]
specProperties :: [Property]
specProperties :: Spec -> [Property]
C.specProperties}) = Bool -> Trans IL -> IL
forall a. Bool -> Trans a -> a
runTrans Bool
b (Trans IL -> IL) -> Trans IL -> IL
forall a b. (a -> b) -> a -> b
$ do

  let modelInit :: [Expr]
modelInit = (Stream -> [Expr]) -> [Stream] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Stream -> [Expr]
streamInit [Stream]
specStreams

  [Expr]
mainConstraints <- (Stream -> StateT TransST Identity Expr)
-> [Stream] -> StateT TransST Identity [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Stream -> StateT TransST Identity Expr
streamRec [Stream]
specStreams

  [Expr]
localConstraints <- StateT TransST Identity [Expr]
popLocalConstraints
  Map SeqId ([Expr], Expr)
properties <- [(SeqId, ([Expr], Expr))] -> Map SeqId ([Expr], Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SeqId, ([Expr], Expr))] -> Map SeqId ([Expr], Expr))
-> StateT TransST Identity [(SeqId, ([Expr], Expr))]
-> StateT TransST Identity (Map SeqId ([Expr], Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [Property]
-> (Property -> StateT TransST Identity (SeqId, ([Expr], Expr)))
-> StateT TransST Identity [(SeqId, ([Expr], Expr))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Property]
specProperties
      (\(C.Property {SeqId
propertyName :: SeqId
propertyName :: Property -> SeqId
C.propertyName, Prop
propertyProp :: Prop
propertyProp :: Property -> Prop
C.propertyProp}) -> do
        -- Soundness note: it is OK to call `extractProp` here to drop the
        -- quantifier from the proposition `propertyProp`. This is because we
        -- IL translation always occurs within the context of a function that
        -- returns a `Proof`, and these `Proof` functions are always careful to
        -- use `Prover`s that respect the propositions's quantifier.
        Expr
e' <- Expr Bool -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr (Prop -> Expr Bool
C.extractProp Prop
propertyProp)
        [Expr]
propConds <- StateT TransST Identity [Expr]
popLocalConstraints
        (SeqId, ([Expr], Expr))
-> StateT TransST Identity (SeqId, ([Expr], Expr))
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqId
propertyName, ([Expr]
propConds, Expr
e')))

  IL -> Trans IL
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return IL
    { [Expr]
modelInit :: [Expr]
modelInit :: [Expr]
modelInit
    , modelRec :: [Expr]
modelRec = [Expr]
mainConstraints [Expr] -> [Expr] -> [Expr]
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Stream] -> Bool
forall a. [a] -> Bool
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    -> Type Int8 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int8
C.Int8
  Type a
C.Int16   -> Type Int16 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int16
C.Int16
  Type a
C.Int32   -> Type Int32 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int32
C.Int32
  Type a
C.Int64   -> Type Int64 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Int64
C.Int64
  Type a
C.Word8   -> Type Word8 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word8
C.Word8
  Type a
C.Word16  -> Type Word16 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word16
C.Word16
  Type a
C.Word32  -> Type Word32 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word32
C.Word32
  Type a
C.Word64  -> Type Word64 -> Trans ()
forall a. (Bounded a, Integral a) => Type a -> Trans ()
bound' Type Word64
C.Word64
  Type a
_         -> () -> Trans ()
forall a. a -> StateT TransST Identity 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 (TransST -> Bool)
-> StateT TransST Identity TransST -> StateT TransST Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransST Identity TransST
forall s (m :: * -> *). MonadState s m => m s
get
      Bool -> Trans () -> Trans ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (Trans () -> Trans ()) -> Trans () -> Trans ()
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 (Type a -> a -> Expr
forall a. Type a -> a -> Expr
trConst Type a
t a
forall a. Bounded a => a
minBound) Expr
s)
        (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Ge (Type a -> a -> Expr
forall a. Type a -> a -> Expr
trConst Type a
t a
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 }) =
  (Integer -> a -> Expr) -> [Integer] -> [a] -> [Expr]
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 (Type a -> Type
forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (Integer -> SeqIndex
Fixed Integer
p))
      (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Type a -> a -> Expr
forall a. Type a -> a -> Expr
trConst Type a
t a
v

streamRec :: C.Stream -> Trans Expr
streamRec :: Stream -> StateT TransST Identity 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 (Type a -> Type
forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (Id -> SeqIndex
forall a. Integral a => a -> SeqIndex
_n_plus (Id -> SeqIndex) -> Id -> SeqIndex
forall a b. (a -> b) -> a -> b
$ [a] -> Id
forall a. [a] -> Id
forall (t :: * -> *) a. Foldable t => t a -> Id
length [a]
b)
  Expr -> Type a -> Trans ()
forall a. Expr -> Type a -> Trans ()
bound Expr
s Type a
t
  Expr
e' <- Expr a -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a
e
  Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
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 -> StateT TransST Identity Expr
expr (C.Const Type a
t a
v) = Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
forall a b. (a -> b) -> a -> b
$ Type a -> a -> Expr
forall a. Type a -> a -> Expr
trConst Type a
t a
v

expr (C.Label Type a
_ SeqId
_ Expr a
e) = Expr a -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a
e

expr (C.Drop Type a
t Word32
k Id
id) = Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
forall a b. (a -> b) -> a -> b
$ Type -> SeqId -> SeqIndex -> Expr
SVal (Type a -> Type
forall a. Type a -> Type
trType Type a
t) (Id -> SeqId
ncSeq Id
id) (Word32 -> SeqIndex
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' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
ea
  Expr -> Trans ()
localConstraint (Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
Bool Op2
Eq (Type -> SeqId -> SeqIndex -> Expr
SVal (Type a1 -> Type
forall a. Type a -> Type
trType Type a1
ta) (SeqId -> SeqId
ncLocal SeqId
name) SeqIndex
_n_) Expr
ea')
  Expr a -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a
eb

expr (C.Var Type a
t SeqId
name) = Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
forall a b. (a -> b) -> a -> b
$ Type -> SeqId -> SeqIndex -> Expr
SVal (Type a -> Type
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]
_) = Expr -> Type a -> Trans ()
forall a. Expr -> Type a -> Trans ()
bound Expr
s Type a
t Trans ()
-> StateT TransST Identity Expr -> StateT TransST Identity Expr
forall a b.
StateT TransST Identity a
-> StateT TransST Identity b -> StateT TransST Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
s
  where
    s :: Expr
s = Type -> SeqId -> SeqIndex -> Expr
SVal (Type a -> Type
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   -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
C.Int16  -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
C.Int32  -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
C.Int64  -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
C.Float  -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
C.Double -> Type a1 -> Expr a1 -> StateT TransST Identity Expr
forall a.
(Typeable a, Ord a, Num a) =>
Type a -> Expr a -> StateT TransST Identity Expr
trSign Type a1
ta Expr a1
e
  Type a1
_        -> Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr (Expr a1 -> StateT TransST Identity Expr)
-> Expr a1 -> StateT TransST Identity Expr
forall a b. (a -> b) -> a -> b
$ Type a1 -> a1 -> Expr a1
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 -> StateT TransST Identity Expr
trSign Type a
ta Expr a
e =
      Expr a -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr (Op3 Bool a a a -> Expr Bool -> Expr a -> Expr a -> Expr a
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 (Type a -> Op3 Bool a a a
forall b. Type b -> Op3 Bool b b b
C.Mux Type a
ta)
        (Op2 a a Bool -> Expr a -> Expr a -> Expr Bool
forall a1 b a.
(Typeable a1, Typeable b) =>
Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
C.Op2 (Type a -> Op2 a a Bool
forall a. Ord a => Type a -> Op2 a a Bool
C.Lt Type a
ta) Expr a
e (Type a -> a -> Expr a
forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
0))
        (Type a -> a -> Expr a
forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta (-a
1))
        (Op3 Bool a a a -> Expr Bool -> Expr a -> Expr a -> Expr a
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 (Type a -> Op3 Bool a a a
forall b. Type b -> Op3 Bool b b b
C.Mux Type a
ta)
          (Op2 a a Bool -> Expr a -> Expr a -> Expr Bool
forall a1 b a.
(Typeable a1, Typeable b) =>
Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
C.Op2 (Type a -> Op2 a a Bool
forall a. Ord a => Type a -> Op2 a a Bool
C.Gt Type a
ta) Expr a
e (Type a -> a -> Expr a
forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
0))
          (Type a -> a -> Expr a
forall a. Typeable a => Type a -> a -> Expr a
C.Const Type a
ta a
1)
          (Type a -> a -> Expr a
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' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
e
  Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
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) = Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
e
expr (C.Op1 Op1 a1 a
op Expr a1
e) = do
  Expr
e' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
e
  Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
forall a b. (a -> b) -> a -> b
$ Type -> Op1 -> Expr -> Expr
Op1 Type
t' Op1
op' Expr
e'
  where
    (Op1
op', Type
t') = Op1 a1 a -> (Op1, Type)
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' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
e1
  Expr
e2' <- Expr b -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr b
e2
  Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
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' = Type a1 -> Type
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' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
e1
  Expr
e2' <- Expr b -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr b
e2
  Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT TransST Identity Expr)
-> Expr -> StateT TransST Identity Expr
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') = Op2 a1 b a -> (Op2, Type)
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' <- Expr a1 -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr a1
cond
  Expr
e1'   <- Expr b -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr b
e1
  Expr
e2'   <- Expr c -> StateT TransST Identity Expr
forall a. Typeable a => Expr a -> StateT TransST Identity Expr
expr Expr c
e2
  Expr -> Type -> Expr -> Expr -> StateT TransST Identity Expr
newMux Expr
cond' (Type b -> Type
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
Bool
v
  Type a
C.Float  -> Double -> Expr
negifyR (Float -> Double
float2Double a
Float
v)
  Type a
C.Double -> Double -> Expr
negifyR a
Double
v
  t :: Type a
t@Type a
C.Int8   -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Int16  -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Int32  -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Int64  -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Word8  -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Word16 -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Word32 -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  t :: Type a
t@Type a
C.Word64 -> a -> Type -> Expr
forall a. Integral a => a -> Type -> Expr
negifyI a
v (Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  where
    negifyR :: Double -> Expr
    negifyR :: Double -> Expr
negifyR Double
v
      | Double
v Double -> Double -> Bool
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 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Double -> Expr
ConstR (Double -> Expr) -> Double -> Expr
forall a b. (a -> b) -> a -> b
$ Double -> Double
forall a. Num a => a -> a
negate (Double -> Double) -> Double -> Double
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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0    = Type -> Integer -> Expr
ConstI Type
t (Integer -> Expr) -> Integer -> Expr
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a. Integral a => a -> Integer
toInteger a
v
      | Bool
otherwise = Type -> Op1 -> Expr -> Expr
Op1 Type
t Op1
Neg (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Type -> Integer -> Expr
ConstI Type
t (Integer -> Expr) -> Integer -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ a -> Integer
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, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  -- C.Sign t  ->
  -- C.Recip t ->
  C.Exp Type a
t   -> (Op1
Exp, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  -- C.Sqrt t  ->
  C.Log Type a
t   -> (Op1
Log, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Sin Type a
t   -> (Op1
Sin, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Tan Type a
t   -> (Op1
Tan, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Cos Type a
t   -> (Op1
Cos, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Asin Type a
t  -> (Op1
Asin, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Atan Type a
t  -> (Op1
Atan, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Acos Type a
t  -> (Op1
Acos, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Sinh Type a
t  -> (Op1
Sinh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Tanh Type a
t  -> (Op1
Tanh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Cosh Type a
t  -> (Op1
Cosh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Asinh Type a
t -> (Op1
Asinh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Atanh Type a
t -> (Op1
Atanh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Acosh Type a
t -> (Op1
Acosh, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  -- C.BwNot t ->
  -- C.Cast t  ->
  Op1 a b
_ -> SeqId -> (Op1, Type)
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, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Sub Type a
t        -> (Op2
Sub, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Mul Type a
t        -> (Op2
Mul, Type a -> Type
forall a. Type a -> Type
trType Type a
t)

  C.Mod Type a
t        -> (Op2
Mod, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  -- C.Div t        ->

  C.Fdiv Type a
t       -> (Op2
Fdiv, Type a -> Type
forall a. Type a -> Type
trType Type a
t)

  C.Pow Type a
t        -> (Op2
Pow, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  -- C.Logb t       ->

  C.Eq Type a
_         -> (Op2
Eq, Type
Bool)
  -- C.Ne t         ->

  C.Le Type a
t         -> (Op2
Le, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Ge Type a
t         -> (Op2
Ge, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Lt Type a
t         -> (Op2
Lt, Type a -> Type
forall a. Type a -> Type
trType Type a
t)
  C.Gt Type a
t         -> (Op2
Gt, Type a -> Type
forall a. Type a -> Type
trType Type a
t)

  -- C.BwAnd t      ->
  -- C.BwOr t       ->
  -- C.BwXor t      ->
  -- C.BwShiftL t _ ->
  -- C.BwShiftR t _ ->

  Op2 a b c
_ -> SeqId -> (Op2, Type)
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

-- | Translation state.
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 -> StateT TransST Identity Expr
newMux Expr
c Type
t Expr
e1 Expr
e2 = do
  [(Expr, (Expr, Type, Expr, Expr))]
ms <- TransST -> [(Expr, (Expr, Type, Expr, Expr))]
muxes (TransST -> [(Expr, (Expr, Type, Expr, Expr))])
-> StateT TransST Identity TransST
-> StateT TransST Identity [(Expr, (Expr, Type, Expr, Expr))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransST Identity TransST
forall s (m :: * -> *). MonadState s m => m s
get
  case ((Expr, (Expr, Type, Expr, Expr)) -> Bool)
-> [(Expr, (Expr, Type, Expr, Expr))]
-> Maybe (Expr, (Expr, Type, Expr, Expr))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (((Expr, Type, Expr, Expr) -> (Expr, Type, Expr, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
==(Expr, Type, Expr, Expr)
mux) ((Expr, Type, Expr, Expr) -> Bool)
-> ((Expr, (Expr, Type, Expr, Expr)) -> (Expr, Type, Expr, Expr))
-> (Expr, (Expr, Type, Expr, Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, (Expr, Type, Expr, Expr)) -> (Expr, Type, Expr, Expr)
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_
      (TransST -> TransST) -> Trans ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransST -> TransST) -> Trans ())
-> (TransST -> TransST) -> Trans ()
forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st { muxes = (v, mux) : ms }
      Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
    Just (Expr
v, (Expr, Type, Expr, Expr)
_) -> Expr -> StateT TransST Identity Expr
forall a. a -> StateT TransST Identity a
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 :: StateT TransST Identity [Expr]
getMuxes = TransST -> [(Expr, (Expr, Type, Expr, Expr))]
muxes (TransST -> [(Expr, (Expr, Type, Expr, Expr))])
-> StateT TransST Identity TransST
-> StateT TransST Identity [(Expr, (Expr, Type, Expr, Expr))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransST Identity TransST
forall s (m :: * -> *). MonadState s m => m s
get StateT TransST Identity [(Expr, (Expr, Type, Expr, Expr))]
-> ([(Expr, (Expr, Type, Expr, Expr))]
    -> StateT TransST Identity [Expr])
-> StateT TransST Identity [Expr]
forall a b.
StateT TransST Identity a
-> (a -> StateT TransST Identity b) -> StateT TransST Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Expr] -> StateT TransST Identity [Expr]
forall a. a -> StateT TransST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> StateT TransST Identity [Expr])
-> ([(Expr, (Expr, Type, Expr, Expr))] -> [Expr])
-> [(Expr, (Expr, Type, Expr, Expr))]
-> StateT TransST Identity [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Expr]] -> [Expr])
-> ([(Expr, (Expr, Type, Expr, Expr))] -> [[Expr]])
-> [(Expr, (Expr, Type, Expr, Expr))]
-> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Expr, (Expr, Type, Expr, Expr)) -> [Expr])
-> [(Expr, (Expr, Type, Expr, Expr))] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, (Expr, Type, Expr, Expr)) -> [Expr]
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)
      ]

-- | A state monad over the translation state ('TransST').
type Trans = State TransST

fresh :: Trans Integer
fresh :: Trans Integer
fresh = do
  (TransST -> TransST) -> Trans ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransST -> TransST) -> Trans ())
-> (TransST -> TransST) -> Trans ()
forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {nextFresh = nextFresh st + 1}
  TransST -> Integer
nextFresh (TransST -> Integer)
-> StateT TransST Identity TransST -> Trans Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransST Identity TransST
forall s (m :: * -> *). MonadState s m => m s
get

localConstraint :: Expr -> Trans ()
localConstraint :: Expr -> Trans ()
localConstraint Expr
c =
  (TransST -> TransST) -> Trans ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransST -> TransST) -> Trans ())
-> (TransST -> TransST) -> Trans ()
forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {localConstraints = c : localConstraints st}

popLocalConstraints :: Trans [Expr]
popLocalConstraints :: StateT TransST Identity [Expr]
popLocalConstraints = ([Expr] -> [Expr] -> [Expr])
-> StateT TransST Identity [Expr]
-> StateT TransST Identity [Expr]
-> StateT TransST Identity [Expr]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
(++) (TransST -> [Expr]
localConstraints (TransST -> [Expr])
-> StateT TransST Identity TransST
-> StateT TransST Identity [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TransST Identity TransST
forall s (m :: * -> *). MonadState s m => m s
get) StateT TransST Identity [Expr]
getMuxes
  StateT TransST Identity [Expr]
-> Trans () -> StateT TransST Identity [Expr]
forall a b.
StateT TransST Identity a
-> StateT TransST Identity b -> StateT TransST Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ((TransST -> TransST) -> Trans ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TransST -> TransST) -> Trans ())
-> (TransST -> TransST) -> Trans ()
forall a b. (a -> b) -> a -> b
$ \TransST
st -> TransST
st {localConstraints = [], muxes = []})

runTrans :: Bool -> Trans a -> a
runTrans :: forall a. Bool -> Trans a -> a
runTrans Bool
b Trans a
m = Trans a -> TransST -> a
forall s a. State s a -> s -> a
evalState Trans a
m (TransST -> a) -> TransST -> a
forall a b. (a -> b) -> a -> b
$ [Expr]
-> [(Expr, (Expr, Type, Expr, Expr))] -> Integer -> Bool -> TransST
TransST [] [] Integer
0 Bool
b