    {-# 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

      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

      localConstraints <- popLocalConstraints
      properties <- Map.fromList <$>
        forM 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.
            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)
            propConds <- popLocalConstraints
            return (propertyName, (propConds, e')))

      return IL
        { modelInit
        , modelRec = mainConstraints ++ localConstraints
        , properties
        , inductive = not $ null 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
          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
          when b $ localConstraint (Op2 Bool And
            (Op2 Bool Le (trConst t minBound) s)
            (Op2 Bool Ge (trConst t maxBound) 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
      e' <- Expr a -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a
    e
      return $ Op2 Bool Eq s 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
      ea' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    ea
      localConstraint (Op2 Bool Eq (SVal (trType ta) (ncLocal name) _n_) ea')
      expr 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
      e' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    e
      return $ Op2 Real Pow e' (ConstR 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
      e' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    e
      return $ Op1 t' op' 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
      e1' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    e1
      e2' <- expr e2
      return $ Op1 Bool Not (Op2 t' Eq e1' 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
      e1' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    e1
      e2' <- expr e2
      return $ Op2 t' op' e1' 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
      cond' <- Expr a1 -> StateT TransST Identity Expr
    forall a. Typeable a => Expr a -> StateT TransST Identity Expr
    expr Expr a1
    cond
      e1'   <- expr e1
      e2'   <- expr e2
      newMux cond' (trType t) e1' 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
      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 find ((==mux) . snd) ms of
        Maybe (Expr, (Expr, Type, Expr, Expr))
    Nothing -> do
          f <- Trans Integer
    fresh
          let v = Type -> SeqId -> SeqIndex -> Expr
    SVal Type
    t (Integer -> SeqId
    ncMux Integer
    f) SeqIndex
    _n_
          modify $ \TransST
    st -> TransST
    st { muxes = (v, mux) : ms }
          return 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