content: {-|
  Module      : What4.Expr.MATLAB
  Description : Low-level support for MATLAB-style arithmetic operations
  Copyright   : (c) Galois, Inc, 2016-2020
  License     : BSD3
  Maintainer  : Joe Hendrix <jhendrix@galois.com>
  
  This module provides an interface that a symbolic backend should
  implement to support MATLAB intrinsics.
  -}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeOperators #-}
  module What4.Expr.MATLAB
    ( MatlabSolverFn(..)
    , matlabSolverArgTypes
    , matlabSolverReturnType
    , ppMatlabSolverFn
    , evalMatlabSolverFn
    , testSolverFnEq
    , traverseMatlabSolverFn
    , MatlabSymbolicArrayBuilder(..)
  
      -- * Utilities for definition
    , clampedIntAdd
    , clampedIntSub
    , clampedIntMul
    , clampedIntNeg
    , clampedIntAbs
    , clampedUIntAdd
    , clampedUIntSub
    , clampedUIntMul
    ) where
  
  import           Control.Monad (join)
  import qualified Data.BitVector.Sized as BV
  import           Data.Kind (Type)
  import           Data.Hashable
  import           Data.Parameterized.Classes
  import           Data.Parameterized.Context as Ctx
  import           Data.Parameterized.TH.GADT
  import           Data.Parameterized.TraversableFC
  import           Prettyprinter
  
  import           What4.BaseTypes
  import           What4.Interface
  import           What4.Utils.Complex
  import           What4.Utils.OnlyIntRepr
  
  ------------------------------------------------------------------------
  -- MatlabSolverFn
  
  
  clampedIntAdd :: (IsExprBuilder sym, 1 <= w)
                => sym
                -> SymBV sym w
                -> SymBV sym w
                -> IO (SymBV sym w)
  clampedIntAdd sym x y = do
    let w = bvWidth x
    withAddPrefixLeq w (knownNat :: NatRepr 1) $ do
    -- Compute result with 1 additional bit to catch clamping
    let w' = incNat w
    x'  <- bvSext sym w' x
    y'  <- bvSext sym w' y
    -- Compute result.
    r'  <- bvAdd sym x' y'
  
    -- Check is result is greater than or equal to max value.
    too_high <- bvSgt sym r' =<< bvLit sym w' (BV.maxSigned w')
    max_int <- bvLit sym w (BV.maxSigned w)
  
    -- Check is result is less than min value.
    too_low <- bvSlt sym r' =<< bvLit sym w' (BV.minSigned w')
    min_int <- bvLit sym w (BV.minSigned w)
  
    -- Clamp integer range.
    r <- bvTrunc sym w r'
    r_low <- bvIte sym too_low min_int r
    bvIte sym too_high max_int r_low
  
  clampedIntSub :: (IsExprBuilder sym, 1 <= w)
                => sym
                -> SymBV sym w
                -> SymBV sym w
                -> IO (SymBV sym w)
  clampedIntSub sym x y = do
    let w = bvWidth x
    (ov, xy) <- subSignedOF sym x y
    ysign  <- bvIsNeg sym y
    minint <- minSignedBV sym w
    maxint <- maxSignedBV sym w
    ov_val <- bvIte sym ysign maxint minint
    bvIte sym ov ov_val xy
  
  clampedIntMul :: (IsExprBuilder sym, 1 <= w)
                => sym
                -> SymBV sym w
                -> SymBV sym w
                -> IO (SymBV sym w)
  clampedIntMul sym x y = do
    let w = bvWidth x
    (hi,lo) <- signedWideMultiplyBV sym x y
    zro    <- bvZero sym w
    ones   <- maxUnsignedBV sym w
    ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo)
                                <*> bvEq sym hi zro
    ok_neg <- join $ andPred sym <$> bvIsNeg sym lo
                                <*> bvEq sym hi ones
    ov     <- notPred sym =<< orPred sym ok_pos ok_neg
  
    minint <- minSignedBV sym w
    maxint <- maxSignedBV sym w
    hisign <- bvIsNeg sym hi
    ov_val <- bvIte sym hisign minint maxint
    bvIte sym ov ov_val lo
  
  
  -- | Compute the clamped negation of a signed bitvector.
  --
  --   The only difference between this operation and the usual
  --   2's complement negation function is the handling of MIN_INT.
  --   The usual 2's complement negation sends MIN_INT to MIN_INT;
  --   however, the clamped version instead sends MIN_INT to MAX_INT.
  clampedIntNeg :: (IsExprBuilder sym, 1 <= w)
                => sym
                -> SymBV sym w
                -> IO (SymBV sym w)
  clampedIntNeg sym x = do
    let w = bvWidth x
    minint <- minSignedBV sym w
  
    -- return maxint when x == minint, and neg(x) otherwise
    p <- bvEq sym x minint
    iteM bvIte sym p (maxSignedBV sym w) (bvNeg sym x)
  
  -- | Compute the clamped absolute value of a signed bitvector.
  --
  --   The only difference between this operation and the usual 2's
  --   complement operation is the handling of MIN_INT.  The usual 2's
  --   complement absolute value function sends MIN_INT to MIN_INT;
  --   however, the clamped version instead sends MIN_INT to MAX_INT.
  clampedIntAbs :: (IsExprBuilder sym, 1 <= w)
                => sym
                -> SymBV sym w
                -> IO (SymBV sym w)
  clampedIntAbs sym x = do
    isNeg  <- bvIsNeg sym x
    iteM bvIte sym isNeg (clampedIntNeg sym x) (pure x)
  
  
  clampedUIntAdd :: (IsExprBuilder sym, 1 <= w)
                 => sym
                 -> SymBV sym w
                 -> SymBV sym w
                 -> IO (SymBV sym w)
  clampedUIntAdd sym x y = do
    let w = bvWidth x
    (ov, xy) <- addUnsignedOF sym x y
    maxint   <- maxUnsignedBV sym w
    bvIte sym ov maxint xy
  
  clampedUIntSub :: (IsExprBuilder sym, 1 <= w)
                 => sym
                 -> SymBV sym w
                 -> SymBV sym w
                 -> IO (SymBV sym w)
  clampedUIntSub sym x y = do
    let w = bvWidth x
    no_underflow <- bvUge sym x y
  
    iteM bvIte
         sym
         no_underflow
         (bvSub sym x y) -- Perform subtraction if y >= x
         (bvZero sym w) -- Otherwise return min int
  
  clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
                 => sym
                 -> SymBV sym w
                 -> SymBV sym w
                 -> IO (SymBV sym w)
  clampedUIntMul sym x y = do
    let w = bvWidth x
    (hi, lo) <- unsignedWideMultiplyBV sym x y
    maxint   <- maxUnsignedBV sym w
    ov       <- bvIsNonzero sym hi
    bvIte sym ov maxint lo
  
  ------------------------------------------------------------------------
  -- MatlabSolverFn
  
  -- | Builtin functions that can be used to generate symbolic functions.
  --
  -- These functions are expected to be total, but the value returned may not be
  -- specified.  e.g. 'IntegerToNatFn' must return some natural number for every
  -- integer, but for negative integers, the particular number is unspecified.
  data MatlabSolverFn (f :: BaseType -> Type) args ret where
  
    -- Or two Boolean variables
    BoolOrFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType ::> BaseBoolType) BaseBoolType
  
    -- Returns true if the real value is an integer.
    IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
  
    -- Return true if first value is less than or equal to second.
    IntLeFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseBoolType
  
    -- A function for mapping a unsigned bitvector to an integer.
    BVToIntegerFn :: (1 <= w)
              => !(NatRepr w)
              ->  MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
    -- A function for mapping a signed bitvector to a integer.
    SBVToIntegerFn :: (1 <= w)
                   => !(NatRepr w)
                   -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
  
    -- A function for mapping an integer to equivalent real.
    IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
  
    -- A function for mapping a real to equivalent integer.
    --
    -- Function may return any value if input is not an integer.
    RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
  
    -- A function that maps Booleans logical value to an integer
    -- (either 0 for false, or 1 for true)
    PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
  
    -- 'IntSeqFn base c' denotes the function '\i _ -> base + c*i
    IntSeqFn :: !(f BaseIntegerType)
             -> !(f BaseIntegerType)
             -> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseIntegerType
  
    -- 'RealSeqFn base c' denotes the function '\_ i -> base + c*i
    RealSeqFn :: !(f BaseRealType)
              -> !(f BaseRealType)
              -> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseRealType
  
    -- 'IndicesInRange tps upper_bounds' returns a predicate that is true if all the arguments
    -- (which must be natural numbers) are between 1 and the given upper bounds (inclusive).
    IndicesInRange :: !(Assignment OnlyIntRepr (idx ::> itp))
                   -> !(Assignment f (idx ::> itp))
                      -- Upper bounds on indices
                   -> MatlabSolverFn f (idx ::> itp) BaseBoolType
  
    IsEqFn :: !(BaseTypeRepr tp)
           -> MatlabSolverFn f (EmptyCtx ::> tp ::> tp) BaseBoolType
  
    ------------------------------------------------------------------------
    -- Bitvector functions
  
    -- Returns true if the bitvector is non-zero.
    BVIsNonZeroFn :: (1 <= w)
                  => !(NatRepr w)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
  
    -- Negate a signed bitvector
    ClampedIntNegFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
  
    -- Get absolute value of a signed bitvector
    ClampedIntAbsFn :: (1 <= w)
           => !(NatRepr w)
           -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
  
    -- Add two values without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedIntAddFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Subtract one value from another without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedIntSubFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Multiple two values without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedIntMulFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Add two values without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedUIntAddFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Subtract one value from another without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedUIntSubFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Multiple two values without wrapping but rather rounding to
    -- 0/max value when the result is out of range.
    ClampedUIntMulFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f
                   (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                   (BaseBVType w)
  
    -- Convert a signed integer to the nearest signed integer with the
    -- given width.  This clamps the value to min-int or max int when truncated
    -- the width.
    IntSetWidthFn :: (1 <= m, 1 <= n)
                  => !(NatRepr m)
                  -> !(NatRepr n)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
  
    -- Convert a unsigned integer to the nearest unsigned integer with the
    -- given width.  This clamps the value to min-int or max int when truncated
    -- the width.
    UIntSetWidthFn :: (1 <= m, 1 <= n)
                   => !(NatRepr m)
                   -> !(NatRepr n)
                   -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
  
    -- Convert a unsigned integer to the nearest signed integer with the
    -- given width.  This clamps the value to min-int or max int when truncated
    -- the width.
    UIntToIntFn :: (1 <= m, 1 <= n)
                  => !(NatRepr m)
                  -> !(NatRepr n)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
  
    -- Convert a signed integer to the nearest unsigned integer with the
    -- given width.  This clamps the value to min-int or max int when truncated
    -- the width.
    IntToUIntFn :: (1 <= m, 1 <= n)
                => !(NatRepr m)
                -> !(NatRepr n)
                -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
  
    ------------------------------------------------------------------------
    -- Real functions
  
    -- Returns true if the complex number is non-zero.
    RealIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
  
    RealCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
    RealSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
  
    ------------------------------------------------------------------------
    -- Conversion functions
  
    RealToSBVFn :: (1 <= w)
                => !(NatRepr w)
                -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
  
    RealToUBVFn :: (1 <= w)
                => !(NatRepr w)
                -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
  
    -- Return 1 if the predicate is true; 0 otherwise.
    PredToBVFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
  
    ------------------------------------------------------------------------
    -- Complex functions
  
    -- Returns true if the complex number is non-zero.
    CplxIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
  
    -- Returns true if the imaginary part of complex number is zero.
    CplxIsRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
  
    -- A function for mapping a real to equivalent complex with imaginary number equals 0.
    RealToComplexFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseComplexType
    -- Returns the real component out of a complex number.
    RealPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
    -- Returns the imag component out of a complex number.
    ImagPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
  
    -- Return the complex number formed by negating both components.
    CplxNegFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
  
    -- Add two complex values.
    CplxAddFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                   BaseComplexType
  
    -- Subtract one complex value from another.
    CplxSubFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                   BaseComplexType
  
    -- Multiply two complex values.
    CplxMulFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                   BaseComplexType
  
    -- Return the complex number formed by rounding both components.
    --
    -- Rounding is away from zero.
    CplxRoundFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
    -- Return the complex number formed by taking floor of both components.
    CplxFloorFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
    -- Return the complex number formed by taking ceiling of both components.
    CplxCeilFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
  
    -- Return magningture of complex number.
    CplxMagFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
  
    -- Return the principal square root of a complex number.
    CplxSqrtFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
  
    -- Returns complex exponential of input
    CplxExpFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType)
                   BaseComplexType
    -- Returns complex natural logarithm of input
    CplxLogFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType)
                   BaseComplexType
    -- Returns complex natural logarithm of input
    CplxLogBaseFn :: !Integer
                  -> MatlabSolverFn f
                       (EmptyCtx ::> BaseComplexType)
                       BaseComplexType
    -- Returns complex sine of input
    CplxSinFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType)
                   BaseComplexType
    -- Returns complex cosine of input
    CplxCosFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType)
                   BaseComplexType
    -- Returns tangent of input.
    --
    CplxTanFn :: MatlabSolverFn f
                   (EmptyCtx ::> BaseComplexType)
                   BaseComplexType
  
  -- Dummy declaration splice to bring App into template haskell scope.
  $(return [])
  
  traverseMatlabSolverFn :: Applicative m
                         => (forall tp . e tp -> m (f tp))
                         -> MatlabSolverFn e a r
                         -> m (MatlabSolverFn f a r)
  traverseMatlabSolverFn f fn_id =
    case fn_id of
      BoolOrFn             -> pure $ BoolOrFn
      IsIntegerFn          -> pure $ IsIntegerFn
      IntLeFn              -> pure $ IntLeFn
      BVToIntegerFn w      -> pure $ BVToIntegerFn w
      SBVToIntegerFn w     -> pure $ SBVToIntegerFn w
      IntegerToRealFn      -> pure $ IntegerToRealFn
      RealToIntegerFn      -> pure $ RealToIntegerFn
      PredToIntegerFn      -> pure $ PredToIntegerFn
      IntSeqFn  b i        -> IntSeqFn <$> f b <*> f i
      RealSeqFn b i        -> RealSeqFn <$> f b <*> f i
      IndicesInRange tps a -> IndicesInRange tps <$> traverseFC f a
      IsEqFn tp            -> pure $ IsEqFn tp
  
      BVIsNonZeroFn w      -> pure $ BVIsNonZeroFn w
  
      ClampedIntNegFn w    -> pure $ ClampedIntNegFn w
      ClampedIntAbsFn w    -> pure $ ClampedIntAbsFn w
      ClampedIntAddFn w    -> pure $ ClampedIntAddFn w
      ClampedIntSubFn w    -> pure $ ClampedIntSubFn w
      ClampedIntMulFn w    -> pure $ ClampedIntMulFn w
  
      ClampedUIntAddFn w   -> pure $ ClampedUIntAddFn w
      ClampedUIntSubFn w   -> pure $ ClampedUIntSubFn w
      ClampedUIntMulFn w   -> pure $ ClampedUIntMulFn w
  
      IntSetWidthFn i o    -> pure $ IntSetWidthFn i o
      UIntSetWidthFn i o   -> pure $ UIntSetWidthFn i o
      UIntToIntFn i o      -> pure $ UIntToIntFn i o
      IntToUIntFn i o      -> pure $ IntToUIntFn i o
  
      RealCosFn            -> pure $ RealCosFn
      RealSinFn            -> pure $ RealSinFn
      RealIsNonZeroFn      -> pure $ RealIsNonZeroFn
  
      RealToSBVFn w        -> pure $ RealToSBVFn w
      RealToUBVFn w        -> pure $ RealToUBVFn w
      PredToBVFn  w        -> pure $ PredToBVFn  w
  
  
      CplxIsNonZeroFn      -> pure $ CplxIsNonZeroFn
      CplxIsRealFn         -> pure $ CplxIsRealFn
      RealToComplexFn      -> pure $ RealToComplexFn
      RealPartOfCplxFn     -> pure $ RealPartOfCplxFn
      ImagPartOfCplxFn     -> pure $ ImagPartOfCplxFn
      CplxNegFn            -> pure $ CplxNegFn
      CplxAddFn            -> pure $ CplxAddFn
      CplxSubFn            -> pure $ CplxSubFn
      CplxMulFn            -> pure $ CplxMulFn
      CplxRoundFn          -> pure $ CplxRoundFn
      CplxFloorFn          -> pure $ CplxFloorFn
      CplxCeilFn           -> pure $ CplxCeilFn
      CplxMagFn            -> pure $ CplxMagFn
      CplxSqrtFn           -> pure $ CplxSqrtFn
      CplxExpFn            -> pure $ CplxExpFn
      CplxLogFn            -> pure $ CplxLogFn
      CplxLogBaseFn b      -> pure $ CplxLogBaseFn b
      CplxSinFn            -> pure $ CplxSinFn
      CplxCosFn            -> pure $ CplxCosFn
      CplxTanFn            -> pure $ CplxTanFn
  
  -- | Utilities to make a pair with the same value.
  binCtx :: BaseTypeRepr tp -> Ctx.Assignment BaseTypeRepr (EmptyCtx ::> tp ::> tp)
  binCtx tp = Ctx.empty Ctx.:> tp Ctx.:> tp
  
  -- | Get arg tpyes of solver fn.
  matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
  matlabSolverArgTypes f =
    case f of
      BoolOrFn             -> knownRepr
      IsIntegerFn          -> knownRepr
      IntLeFn              -> knownRepr
      BVToIntegerFn w      -> Ctx.singleton (BaseBVRepr w)
      SBVToIntegerFn w     -> Ctx.singleton (BaseBVRepr w)
      IntegerToRealFn      -> knownRepr
      RealToIntegerFn      -> knownRepr
      PredToIntegerFn      -> knownRepr
      IntSeqFn{}           -> knownRepr
      IndicesInRange tps _ -> fmapFC toBaseTypeRepr tps
      RealSeqFn _ _        -> knownRepr
      IsEqFn tp            -> binCtx tp
  
      BVIsNonZeroFn w      -> Ctx.singleton (BaseBVRepr w)
      ClampedIntNegFn w    -> Ctx.singleton (BaseBVRepr w)
      ClampedIntAbsFn w    -> Ctx.singleton (BaseBVRepr w)
      ClampedIntAddFn w    -> binCtx (BaseBVRepr w)
      ClampedIntSubFn w    -> binCtx (BaseBVRepr w)
      ClampedIntMulFn w    -> binCtx (BaseBVRepr w)
      ClampedUIntAddFn w   -> binCtx (BaseBVRepr w)
      ClampedUIntSubFn w   -> binCtx (BaseBVRepr w)
      ClampedUIntMulFn w   -> binCtx (BaseBVRepr w)
      IntSetWidthFn  i _   -> Ctx.singleton (BaseBVRepr i)
      UIntSetWidthFn i _   -> Ctx.singleton (BaseBVRepr i)
      UIntToIntFn i _      -> Ctx.singleton (BaseBVRepr i)
      IntToUIntFn i _      -> Ctx.singleton (BaseBVRepr i)
  
      RealCosFn            -> knownRepr
      RealSinFn            -> knownRepr
      RealIsNonZeroFn      -> knownRepr
  
      RealToSBVFn _        -> knownRepr
      RealToUBVFn _        -> knownRepr
      PredToBVFn  _        -> knownRepr
  
      CplxIsNonZeroFn      -> knownRepr
      CplxIsRealFn         -> knownRepr
      RealToComplexFn      -> knownRepr
      RealPartOfCplxFn     -> knownRepr
      ImagPartOfCplxFn     -> knownRepr
      CplxNegFn            -> knownRepr
      CplxAddFn            -> knownRepr
      CplxSubFn            -> knownRepr
      CplxMulFn            -> knownRepr
      CplxRoundFn          -> knownRepr
      CplxFloorFn          -> knownRepr
      CplxCeilFn           -> knownRepr
      CplxMagFn            -> knownRepr
      CplxSqrtFn           -> knownRepr
      CplxExpFn            -> knownRepr
      CplxLogFn            -> knownRepr
      CplxLogBaseFn _      -> knownRepr
      CplxSinFn            -> knownRepr
      CplxCosFn            -> knownRepr
      CplxTanFn            -> knownRepr
  
  -- | Get return type of solver fn.
  matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret
  matlabSolverReturnType f =
    case f of
      BoolOrFn             -> knownRepr
      IsIntegerFn          -> knownRepr
      IntLeFn              -> knownRepr
      BVToIntegerFn{}      -> knownRepr
      SBVToIntegerFn{}     -> knownRepr
      IntegerToRealFn      -> knownRepr
      RealToIntegerFn      -> knownRepr
      PredToIntegerFn      -> knownRepr
      IntSeqFn{}           -> knownRepr
      IndicesInRange{}     -> knownRepr
      RealSeqFn _ _        -> knownRepr
      IsEqFn{}             -> knownRepr
  
      BVIsNonZeroFn _      -> knownRepr
      ClampedIntNegFn w    -> BaseBVRepr w
      ClampedIntAbsFn w    -> BaseBVRepr w
      ClampedIntAddFn w    -> BaseBVRepr w
      ClampedIntSubFn w    -> BaseBVRepr w
      ClampedIntMulFn w    -> BaseBVRepr w
      ClampedUIntAddFn w   -> BaseBVRepr w
      ClampedUIntSubFn w   -> BaseBVRepr w
      ClampedUIntMulFn w   -> BaseBVRepr w
      IntSetWidthFn  _ o   -> BaseBVRepr o
      UIntSetWidthFn _ o   -> BaseBVRepr o
      UIntToIntFn _ o      -> BaseBVRepr o
      IntToUIntFn _ o      -> BaseBVRepr o
  
      RealCosFn            -> knownRepr
      RealSinFn            -> knownRepr
      RealIsNonZeroFn      -> knownRepr
  
      RealToSBVFn w        -> BaseBVRepr w
      RealToUBVFn w        -> BaseBVRepr w
      PredToBVFn  w        -> BaseBVRepr w
  
      CplxIsNonZeroFn      -> knownRepr
      CplxIsRealFn         -> knownRepr
      RealToComplexFn      -> knownRepr
      RealPartOfCplxFn     -> knownRepr
      ImagPartOfCplxFn     -> knownRepr
      CplxNegFn            -> knownRepr
      CplxAddFn            -> knownRepr
      CplxSubFn            -> knownRepr
      CplxMulFn            -> knownRepr
      CplxRoundFn          -> knownRepr
      CplxFloorFn          -> knownRepr
      CplxCeilFn           -> knownRepr
      CplxMagFn            -> knownRepr
      CplxSqrtFn           -> knownRepr
      CplxExpFn            -> knownRepr
      CplxLogFn            -> knownRepr
      CplxLogBaseFn _      -> knownRepr
      CplxSinFn            -> knownRepr
      CplxCosFn            -> knownRepr
      CplxTanFn            -> knownRepr
  
  ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
  ppMatlabSolverFn f =
    case f of
      BoolOrFn             -> pretty "bool_or"
      IsIntegerFn          -> pretty "is_integer"
      IntLeFn              -> pretty "int_le"
      BVToIntegerFn w      -> parens $ pretty "bv_to_int" <+> ppNatRepr w
      SBVToIntegerFn w     -> parens $ pretty "sbv_to_int" <+> ppNatRepr w
      IntegerToRealFn      -> pretty "integer_to_real"
      RealToIntegerFn      -> pretty "real_to_integer"
      PredToIntegerFn      -> pretty "pred_to_integer"
      IntSeqFn  b i        -> parens $ pretty "nat_seq"  <+> printSymExpr b <+> printSymExpr i
      RealSeqFn b i        -> parens $ pretty "real_seq" <+> printSymExpr b <+> printSymExpr i
      IndicesInRange _ bnds ->
        parens (pretty "indices_in_range" <+> sep (toListFC printSymExpr bnds))
      IsEqFn{}             -> pretty "is_eq"
  
      BVIsNonZeroFn w      -> parens $ pretty "bv_is_nonzero" <+> ppNatRepr w
      ClampedIntNegFn w    -> parens $ pretty "clamped_int_neg" <+> ppNatRepr w
      ClampedIntAbsFn w    -> parens $ pretty "clamped_neg_abs" <+> ppNatRepr w
      ClampedIntAddFn w    -> parens $ pretty "clamped_int_add" <+> ppNatRepr w
      ClampedIntSubFn w    -> parens $ pretty "clamped_int_sub" <+> ppNatRepr w
      ClampedIntMulFn w    -> parens $ pretty "clamped_int_mul" <+> ppNatRepr w
      ClampedUIntAddFn w   -> parens $ pretty "clamped_uint_add" <+> ppNatRepr w
      ClampedUIntSubFn w   -> parens $ pretty "clamped_uint_sub" <+> ppNatRepr w
      ClampedUIntMulFn w   -> parens $ pretty "clamped_uint_mul" <+> ppNatRepr w
  
      IntSetWidthFn i o    -> parens $ pretty "int_set_width"  <+> ppNatRepr i <+> ppNatRepr o
      UIntSetWidthFn i o   -> parens $ pretty "uint_set_width" <+> ppNatRepr i <+> ppNatRepr o
      UIntToIntFn i o      -> parens $ pretty "uint_to_int"  <+> ppNatRepr i <+> ppNatRepr o
      IntToUIntFn i o      -> parens $ pretty "int_to_uint"  <+> ppNatRepr i <+> ppNatRepr o
  
      RealCosFn            -> pretty "real_cos"
      RealSinFn            -> pretty "real_sin"
      RealIsNonZeroFn      -> pretty "real_is_nonzero"
  
      RealToSBVFn w        -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
      RealToUBVFn w        -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
      PredToBVFn  w        -> parens $ pretty "pred_to_bv"  <+> ppNatRepr w
  
      CplxIsNonZeroFn      -> pretty "cplx_is_nonzero"
      CplxIsRealFn         -> pretty "cplx_is_real"
      RealToComplexFn      -> pretty "real_to_complex"
      RealPartOfCplxFn     -> pretty "real_part_of_complex"
      ImagPartOfCplxFn     -> pretty "imag_part_of_complex"
  
      CplxNegFn            -> pretty "cplx_neg"
      CplxAddFn            -> pretty "cplx_add"
      CplxSubFn            -> pretty "cplx_sub"
      CplxMulFn            -> pretty "cplx_mul"
  
      CplxRoundFn          -> pretty "cplx_round"
      CplxFloorFn          -> pretty "cplx_floor"
      CplxCeilFn           -> pretty "cplx_ceil"
      CplxMagFn            -> pretty "cplx_mag"
      CplxSqrtFn           -> pretty "cplx_sqrt"
      CplxExpFn            -> pretty "cplx_exp"
      CplxLogFn            -> pretty "cplx_log"
      CplxLogBaseFn b      -> parens $ pretty "cplx_log_base" <+> pretty b
      CplxSinFn            -> pretty "cplx_sin"
      CplxCosFn            -> pretty "cplx_cos"
      CplxTanFn            -> pretty "cplx_tan"
  
  ppNatRepr :: NatRepr w -> Doc ann
  ppNatRepr = viaShow
  
  -- | Test 'MatlabSolverFn' values for equality.
  testSolverFnEq :: TestEquality f
                 => MatlabSolverFn f ax rx
                 -> MatlabSolverFn f ay ry
                 -> Maybe ((ax ::> rx) :~: (ay ::> ry))
  testSolverFnEq = $(structuralTypeEquality [t|MatlabSolverFn|]
                     [ ( DataArg 0 `TypeApp` AnyType
                       , [|testEquality|]
                       )
                     , ( ConType [t|NatRepr|] `TypeApp` AnyType
                       , [|testEquality|]
                       )
                     , ( ConType [t|Assignment|] `TypeApp` AnyType `TypeApp` AnyType
                       , [|testEquality|]
                       )
                     , ( ConType [t|BaseTypeRepr|] `TypeApp` AnyType
                       , [|testEquality|]
                       )
                     ]
                    )
  
  instance TestEquality f => Eq (MatlabSolverFn f args tp) where
    x == y = isJust (testSolverFnEq x y)
  
  instance ( Hashable (f BaseRealType)
           , Hashable (f BaseIntegerType)
           , HashableF f
           , TestEquality f
           )
           => Hashable (MatlabSolverFn f args tp) where
    hashWithSalt = $(structuralHashWithSalt [t|MatlabSolverFn|] [])
  
  realIsNonZero :: IsExprBuilder sym => sym -> SymReal sym -> IO (Pred sym)
  realIsNonZero sym = realNe sym (realZero sym)
  
  evalMatlabSolverFn :: forall sym args ret
                     .  IsExprBuilder sym
                     => MatlabSolverFn (SymExpr sym) args ret
                     -> sym
                     -> Assignment (SymExpr sym) args
                     -> IO (SymExpr sym ret)
  evalMatlabSolverFn f sym =
    case f of
      BoolOrFn         -> uncurryAssignment $ orPred sym
  
      IsIntegerFn      -> uncurryAssignment $ isInteger sym
      IntLeFn          -> uncurryAssignment $ intLe sym
      BVToIntegerFn{}  -> uncurryAssignment $ bvToInteger sym
      SBVToIntegerFn{} -> uncurryAssignment $ sbvToInteger sym
      IntegerToRealFn  -> uncurryAssignment $ integerToReal sym
      RealToIntegerFn  -> uncurryAssignment $ realToInteger sym
      PredToIntegerFn  -> uncurryAssignment $ \p ->
        iteM intIte sym p (intLit sym 1) (intLit sym 0)
      IntSeqFn b inc   -> uncurryAssignment $ \idx _ -> do
        intAdd sym b =<< intMul sym inc idx
      RealSeqFn b inc -> uncurryAssignment $ \_ idx -> do
        realAdd sym b =<< realMul sym inc =<< integerToReal sym idx
      IndicesInRange tps0 bnds0 -> \args ->
          Ctx.forIndex (Ctx.size tps0) (g tps0 bnds0 args) (pure (truePred sym))
        where g :: Assignment OnlyIntRepr ctx
                -> Assignment (SymExpr sym) ctx
                -> Assignment (SymExpr sym) ctx
                -> IO (Pred sym)
                -> Index ctx tp
                -> IO (Pred sym)
              g tps bnds args m i = do
                case tps Ctx.! i of
                  OnlyIntRepr -> do
                    let v = args ! i
                    let bnd = bnds ! i
                    one <- intLit sym 1
                    p <- join $ andPred sym <$> intLe sym one v <*> intLe sym v bnd
                    andPred sym p =<< m
      IsEqFn{} -> Ctx.uncurryAssignment $ \x y -> do
        isEq sym x y
  
      BVIsNonZeroFn _    -> Ctx.uncurryAssignment $ bvIsNonzero sym
      ClampedIntNegFn _  -> Ctx.uncurryAssignment $ clampedIntNeg sym
      ClampedIntAbsFn _  -> Ctx.uncurryAssignment $ clampedIntAbs sym
      ClampedIntAddFn _  -> Ctx.uncurryAssignment $ clampedIntAdd sym
      ClampedIntSubFn _  -> Ctx.uncurryAssignment $ clampedIntSub sym
      ClampedIntMulFn _  -> Ctx.uncurryAssignment $ clampedIntMul sym
      ClampedUIntAddFn _ -> Ctx.uncurryAssignment $ clampedUIntAdd sym
      ClampedUIntSubFn _ -> Ctx.uncurryAssignment $ clampedUIntSub sym
      ClampedUIntMulFn _ -> Ctx.uncurryAssignment $ clampedUIntMul sym
  
      IntSetWidthFn  _ o -> Ctx.uncurryAssignment $ \v -> intSetWidth  sym v o
      UIntSetWidthFn _ o -> Ctx.uncurryAssignment $ \v -> uintSetWidth sym v o
      UIntToIntFn _ o    -> Ctx.uncurryAssignment $ \v -> uintToInt sym v o
      IntToUIntFn _ o    -> Ctx.uncurryAssignment $ \v -> intToUInt sym v o
  
      RealIsNonZeroFn    -> Ctx.uncurryAssignment $ realIsNonZero sym
      RealCosFn          -> Ctx.uncurryAssignment $ realCos sym
      RealSinFn          -> Ctx.uncurryAssignment $ realSin sym
  
      RealToSBVFn w      -> Ctx.uncurryAssignment $ \v -> realToSBV sym v w
      RealToUBVFn w      -> Ctx.uncurryAssignment $ \v -> realToBV  sym v w
      PredToBVFn  w      -> Ctx.uncurryAssignment $ \v -> predToBV  sym v w
  
      CplxIsNonZeroFn  -> Ctx.uncurryAssignment $ \x -> do
        (real_x :+ imag_x) <- cplxGetParts sym x
        join $ orPred sym <$> realIsNonZero sym real_x <*> realIsNonZero sym imag_x
      CplxIsRealFn     -> Ctx.uncurryAssignment $ isReal sym
      RealToComplexFn  -> Ctx.uncurryAssignment $ cplxFromReal sym
      RealPartOfCplxFn -> Ctx.uncurryAssignment $ getRealPart sym
      ImagPartOfCplxFn -> Ctx.uncurryAssignment $ getImagPart sym
  
      CplxNegFn        -> Ctx.uncurryAssignment $ cplxNeg sym
      CplxAddFn        -> Ctx.uncurryAssignment $ cplxAdd sym
      CplxSubFn        -> Ctx.uncurryAssignment $ cplxSub sym
      CplxMulFn        -> Ctx.uncurryAssignment $ cplxMul sym
  
      CplxRoundFn      -> Ctx.uncurryAssignment $ cplxRound sym
      CplxFloorFn      -> Ctx.uncurryAssignment $ cplxFloor sym
      CplxCeilFn       -> Ctx.uncurryAssignment $ cplxCeil  sym
      CplxMagFn        -> Ctx.uncurryAssignment $ cplxMag   sym
      CplxSqrtFn       -> Ctx.uncurryAssignment $ cplxSqrt  sym
      CplxExpFn        -> Ctx.uncurryAssignment $ cplxExp   sym
      CplxLogFn        -> Ctx.uncurryAssignment $ cplxLog   sym
      CplxLogBaseFn b  -> Ctx.uncurryAssignment $ cplxLogBase (toRational b) sym
      CplxSinFn        -> Ctx.uncurryAssignment $ cplxSin  sym
      CplxCosFn        -> Ctx.uncurryAssignment $ cplxCos  sym
      CplxTanFn        -> Ctx.uncurryAssignment $ cplxTan  sym
  
  -- | This class is provides functions needed to implement the symbolic
  -- array intrinsic functions
  class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
  
    -- | Create a Matlab solver function from its prototype.
    mkMatlabSolverFn :: sym
                     -> MatlabSolverFn (SymExpr sym) args ret
                     -> IO (SymFn sym args ret)
  