{-|
Module      : What4.Expr.Builder
Description : Main definitions of the What4 expression representation
Copyright   : (c) Galois Inc, 2015-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

This module defines the canonical implementation of the solver interface
from "What4.Interface". Type @'ExprBuilder' t st@ is
an instance of the classes 'IsExprBuilder' and 'IsSymExprBuilder'.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.Builder
  ( -- * ExprBuilder
    ExprBuilder
  , newExprBuilder
  , getSymbolVarBimap
  , sbMakeExpr
  , sbNonceExpr
  , curProgramLoc
  , sbUnaryThreshold
  , sbCacheStartSize
  , sbBVDomainRangeLimit
  , sbStateManager
  , exprCounter
  , startCaching
  , stopCaching

    -- * Specialized representations
  , bvUnary
  , natSum
  , intSum
  , realSum
  , bvSum
  , scalarMul

    -- * configuration options
  , unaryThresholdOption
  , bvdomainRangeLimitOption
  , cacheStartSizeOption
  , cacheTerms

    -- * Expr
  , Expr(..)
  , asApp
  , asNonceApp
  , iteSize
  , exprLoc
  , ppExpr
  , ppExprTop
  , exprMaybeId
  , asConjunction
  , asDisjunction
  , Polarity(..)
  , BM.negatePolarity
    -- ** AppExpr
  , AppExpr
  , appExprId
  , appExprLoc
  , appExprApp
    -- ** NonceAppExpr
  , NonceAppExpr
  , nonceExprId
  , nonceExprLoc
  , nonceExprApp
    -- ** Type abbreviations
  , BoolExpr
  , NatExpr
  , IntegerExpr
  , RealExpr
  , BVExpr
  , CplxExpr
  , StringExpr

    -- * App
  , App(..)
  , traverseApp
  , appType
    -- * NonceApp
  , NonceApp(..)
  , nonceAppType

    -- * Bound Variable information
  , ExprBoundVar
  , bvarId
  , bvarLoc
  , bvarName
  , bvarType
  , bvarKind
  , bvarAbstractValue
  , VarKind(..)
  , boundVars
  , ppBoundVar
  , evalBoundVars

    -- * Symbolic Function
  , ExprSymFn(..)
  , SymFnInfo(..)
  , symFnArgTypes
  , symFnReturnType

    -- * SymbolVarBimap
  , SymbolVarBimap
  , SymbolBinding(..)
  , emptySymbolVarBimap
  , lookupBindingOfSymbol
  , lookupSymbolOfBinding

    -- * IdxCache
  , IdxCache
  , newIdxCache
  , lookupIdx
  , lookupIdxValue
  , insertIdxValue
  , deleteIdxValue
  , clearIdxCache
  , idxCacheEval
  , idxCacheEval'

    -- * Flags
  , type FloatMode
  , FloatModeRepr(..)
  , FloatIEEE
  , FloatUninterpreted
  , FloatReal
  , Flags

    -- * BV Or Set
  , BVOrSet
  , bvOrToList
  , bvOrSingleton
  , bvOrInsert
  , bvOrUnion
  , bvOrAbs
  , traverseBVOrSet

    -- * Re-exports
  , SymExpr
  , What4.Interface.bvWidth
  , What4.Interface.exprType
  , What4.Interface.IndexLit(..)
  , What4.Interface.ArrayResultWrapper(..)
  ) where

import qualified Control.Exception as Ex
import           Control.Lens hiding (asIndex, (:>), Empty)
import           Control.Monad
import           Control.Monad.IO.Class
import           Control.Monad.ST
import           Control.Monad.Trans.Writer.Strict (writer, runWriter)
import qualified Data.BitVector.Sized as BV
import           Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import qualified Data.Binary.IEEE754 as IEEE754
import           Data.Foldable
import qualified Data.HashTable.Class as H (toList)
import qualified Data.HashTable.ST.Basic as H
import           Data.Hashable
import           Data.IORef
import           Data.Kind
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Monoid (Any(..))
import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.HashTable as PH
import qualified Data.Parameterized.Map as PM
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Ratio (numerator, denominator)
import           Data.STRef
import qualified Data.Sequence as Seq
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Word (Word64)
import           GHC.Generics (Generic)
import           Numeric.Natural
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))

import           What4.BaseTypes
import           What4.Concrete
import qualified What4.Config as CFG
import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.ProgramLoc
import qualified What4.SemiRing as SR
import           What4.Symbol
import           What4.Expr.App
import qualified What4.Expr.ArrayUpdateMap as AUM
import           What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..))
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.MATLAB
import           What4.Expr.WeightedSum (WeightedSum, SemiRingProduct)
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.StringSeq as SSeq
import           What4.Expr.UnaryBV (UnaryBV)
import qualified What4.Expr.UnaryBV as UnaryBV

import           What4.Utils.AbstractDomains
import           What4.Utils.Arithmetic
import qualified What4.Utils.BVDomain as BVD
import           What4.Utils.Complex
import           What4.Utils.StringLiteral

------------------------------------------------------------------------
-- Utilities

toDouble :: Rational -> Double
toDouble = fromRational

cachedEval :: (HashableF k, TestEquality k)
           => PH.HashTable RealWorld k a
           -> k tp
           -> IO (a tp)
           -> IO (a tp)
cachedEval tbl k action = do
  mr <- stToIO $ PH.lookup tbl k
  case mr of
    Just r -> return r
    Nothing -> do
      r <- action
      seq r $ do
      stToIO $ PH.insert tbl k r
      return r

-- | This type represents 'Expr' values that were built from a
-- 'NonceApp'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'NonceAppExpr' values,
-- but the constructor is kept hidden. The preferred way to construct
-- an 'Expr' from a 'NonceApp' is to use 'sbNonceExpr'.
data NonceAppExpr t (tp :: BaseType)
   = NonceAppExprCtor { nonceExprId  :: {-# UNPACK #-} !(Nonce t tp)
                     , nonceExprLoc :: !ProgramLoc
                     , nonceExprApp :: !(NonceApp t (Expr t) tp)
                     , nonceExprAbsValue :: !(AbstractValue tp)
                     }

-- | This type represents 'Expr' values that were built from an 'App'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'AppExpr' values, but
-- the constructor is kept hidden. The preferred way to construct an
-- 'Expr' from an 'App' is to use 'sbMakeExpr'.
data AppExpr t (tp :: BaseType)
   = AppExprCtor { appExprId  :: {-# UNPACK #-} !(Nonce t tp)
                , appExprLoc :: !ProgramLoc
                , appExprApp :: !(App (Expr t) tp)
                , appExprAbsValue :: !(AbstractValue tp)
                }

------------------------------------------------------------------------
-- Expr

-- | The main ExprBuilder expression datastructure.  The non-trivial @Expr@
-- values constructed by this module are uniquely identified by a
-- nonce value that is used to explicitly represent sub-term sharing.
-- When traversing the structure of an @Expr@ it is usually very important
-- to memoize computations based on the values of these identifiers to avoid
-- exponential blowups due to shared term structure.
--
-- Type parameter @t@ is a phantom type brand used to relate nonces to
-- a specific nonce generator (similar to the @s@ parameter of the
-- @ST@ monad). The type index @tp@ of kind 'BaseType' indicates the
-- type of the values denoted by the given expression.
--
-- Type @'Expr' t@ instantiates the type family @'SymExpr'
-- ('ExprBuilder' t st)@.
data Expr t (tp :: BaseType) where
  SemiRingLiteral :: !(SR.SemiRingRepr sr) -> !(SR.Coefficient sr) -> !ProgramLoc -> Expr t (SR.SemiRingBase sr)
  BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
  StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
  -- Application
  AppExpr :: {-# UNPACK #-} !(AppExpr t tp) -> Expr t tp
  -- An atomic predicate
  NonceAppExpr :: {-# UNPACK #-} !(NonceAppExpr t tp) -> Expr t tp
  -- A bound variable
  BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp

-- | Destructor for the 'AppExpr' constructor.
{-# INLINE asApp #-}
asApp :: Expr t tp -> Maybe (App (Expr t) tp)
asApp (AppExpr a) = Just (appExprApp a)
asApp _ = Nothing

-- | Destructor for the 'NonceAppExpr' constructor.
{-# INLINE asNonceApp #-}
asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp (NonceAppExpr a) = Just (nonceExprApp a)
asNonceApp _ = Nothing

exprLoc :: Expr t tp -> ProgramLoc
exprLoc (SemiRingLiteral _ _ l) = l
exprLoc (BoolExpr _ l) = l
exprLoc (StringExpr _ l) = l
exprLoc (NonceAppExpr a)  = nonceExprLoc a
exprLoc (AppExpr a)   = appExprLoc a
exprLoc (BoundVarExpr v) = bvarLoc v

mkExpr :: Nonce t tp
      -> ProgramLoc
      -> App (Expr t) tp
      -> AbstractValue tp
      -> Expr t tp
mkExpr n l a v = AppExpr $ AppExprCtor { appExprId  = n
                                    , appExprLoc = l
                                    , appExprApp = a
                                    , appExprAbsValue = v
                                    }

type BoolExpr t = Expr t BaseBoolType
type NatExpr  t = Expr t BaseNatType
type BVExpr t n = Expr t (BaseBVType n)
type IntegerExpr t = Expr t BaseIntegerType
type RealExpr t = Expr t BaseRealType
type CplxExpr t = Expr t BaseComplexType
type StringExpr t si = Expr t (BaseStringType si)



iteSize :: Expr t tp -> Integer
iteSize e =
  case asApp e of
    Just (BaseIte _ sz _ _ _) -> sz
    _ -> 0

instance IsExpr (Expr t) where
  asConstantPred = exprAbsValue

  asNat (SemiRingLiteral SR.SemiRingNatRepr n _) = Just n
  asNat _ = Nothing

  natBounds x = exprAbsValue x

  asInteger (SemiRingLiteral SR.SemiRingIntegerRepr n _) = Just n
  asInteger _ = Nothing

  integerBounds x = exprAbsValue x

  asRational (SemiRingLiteral SR.SemiRingRealRepr r _) = Just r
  asRational _ = Nothing

  rationalBounds x = ravRange $ exprAbsValue x

  asComplex e
    | Just (Cplx c) <- asApp e = traverse asRational c
    | otherwise = Nothing

  exprType (SemiRingLiteral sr _ _) = SR.semiRingBase sr
  exprType (BoolExpr _ _) = BaseBoolRepr
  exprType (StringExpr s _) = BaseStringRepr (stringLiteralInfo s)
  exprType (NonceAppExpr e)  = nonceAppType (nonceExprApp e)
  exprType (AppExpr e) = appType (appExprApp e)
  exprType (BoundVarExpr i) = bvarType i

  asBV (SemiRingLiteral (SR.SemiRingBVRepr _ _) i _) = Just i
  asBV _ = Nothing

  unsignedBVBounds x = Just $ BVD.ubounds $ exprAbsValue x
  signedBVBounds x = Just $ BVD.sbounds (bvWidth x) $ exprAbsValue x

  asAffineVar e = case exprType e of
    BaseNatRepr
      | Just (a, x, b) <- WSum.asAffineVar $
          asWeightedSum SR.SemiRingNatRepr e ->
        Just (ConcreteNat a, x, ConcreteNat b)
    BaseIntegerRepr
      | Just (a, x, b) <- WSum.asAffineVar $
          asWeightedSum SR.SemiRingIntegerRepr e ->
        Just (ConcreteInteger a, x, ConcreteInteger b)
    BaseRealRepr
      | Just (a, x, b) <- WSum.asAffineVar $
          asWeightedSum SR.SemiRingRealRepr e ->
        Just (ConcreteReal a, x, ConcreteReal b)
    BaseBVRepr w
      | Just (a, x, b) <- WSum.asAffineVar $
          asWeightedSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e ->
        Just (ConcreteBV w a, x, ConcreteBV w b)
    _ -> Nothing

  asString (StringExpr x _) = Just x
  asString _ = Nothing

  asConstantArray (asApp -> Just (ConstantArray _ _ def)) = Just def
  asConstantArray _ = Nothing

  asStruct (asApp -> Just (StructCtor _ flds)) = Just flds
  asStruct _ = Nothing

  printSymExpr = pretty


asSemiRingLit :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (SR.Coefficient sr)
asSemiRingLit sr (SemiRingLiteral sr' x _loc)
  | Just Refl <- testEquality sr sr'
  = Just x

  -- special case, ignore the BV ring flavor for this purpose
  | SR.SemiRingBVRepr _ w  <- sr
  , SR.SemiRingBVRepr _ w' <- sr'
  , Just Refl <- testEquality w w'
  = Just x

asSemiRingLit _ _ = Nothing

asSemiRingSum :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum sr (asSemiRingLit sr -> Just x) = Just (WSum.constant sr x)
asSemiRingSum sr (asApp -> Just (SemiRingSum x))
   | Just Refl <- testEquality sr (WSum.sumRepr x) = Just x
asSemiRingSum _ _ = Nothing

asSemiRingProd :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
asSemiRingProd sr (asApp -> Just (SemiRingProd x))
  | Just Refl <- testEquality sr (WSum.prodRepr x) = Just x
asSemiRingProd _ _ = Nothing

-- | This privides a view of a semiring expr as a weighted sum of values.
data SemiRingView t sr
   = SR_Constant !(SR.Coefficient sr)
   | SR_Sum  !(WeightedSum (Expr t) sr)
   | SR_Prod !(SemiRingProduct (Expr t) sr)
   | SR_General

viewSemiRing:: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> SemiRingView t sr
viewSemiRing sr x
  | Just r <- asSemiRingLit sr x  = SR_Constant r
  | Just s <- asSemiRingSum sr x  = SR_Sum s
  | Just p <- asSemiRingProd sr x = SR_Prod p
  | otherwise = SR_General

asWeightedSum :: HashableF (Expr t) => SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum sr x
  | Just r <- asSemiRingLit sr x = WSum.constant sr r
  | Just s <- asSemiRingSum sr x = s
  | otherwise = WSum.var sr x

asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asConjunction (BoolExpr True _) = []
asConjunction (asApp -> Just (ConjPred xs)) =
 case BM.viewBoolMap xs of
   BoolMapUnit     -> []
   BoolMapDualUnit -> [(BoolExpr False initializationLoc, Positive)]
   BoolMapTerms (tm:|tms) -> tm:tms
asConjunction x = [(x,Positive)]


asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asDisjunction (BoolExpr False _) = []
asDisjunction (asApp -> Just (NotPred (asApp -> Just (ConjPred xs)))) =
 case BM.viewBoolMap xs of
   BoolMapUnit     -> []
   BoolMapDualUnit -> [(BoolExpr True initializationLoc, Positive)]
   BoolMapTerms (tm:|tms) -> map (over _2 BM.negatePolarity) (tm:tms)
asDisjunction x = [(x,Positive)]

asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asPosAtom (asApp -> Just (NotPred x)) = (x, Negative)
asPosAtom x                           = (x, Positive)

asNegAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asNegAtom (asApp -> Just (NotPred x)) = (x, Positive)
asNegAtom x                           = (x, Negative)

------------------------------------------------------------------------
-- SymbolVarBimap

-- | A bijective map between vars and their canonical name for printing
-- purposes.
-- Parameter @t@ is a phantom type brand used to track nonces.
newtype SymbolVarBimap t = SymbolVarBimap (Bimap SolverSymbol (SymbolBinding t))

-- | This describes what a given SolverSymbol is associated with.
-- Parameter @t@ is a phantom type brand used to track nonces.
data SymbolBinding t
   = forall tp . VarSymbolBinding !(ExprBoundVar t tp)
     -- ^ Solver
   | forall args ret . FnSymbolBinding  !(ExprSymFn t (Expr t) args ret)

instance Eq (SymbolBinding t) where
  VarSymbolBinding x == VarSymbolBinding y = isJust (testEquality x y)
  FnSymbolBinding  x == FnSymbolBinding  y = isJust (testEquality (symFnId x) (symFnId y))
  _ == _ = False

instance Ord (SymbolBinding t) where
  compare (VarSymbolBinding x) (VarSymbolBinding y) =
    toOrdering (compareF x y)
  compare VarSymbolBinding{} _ = LT
  compare _ VarSymbolBinding{} = GT
  compare (FnSymbolBinding  x) (FnSymbolBinding  y) =
    toOrdering (compareF (symFnId x) (symFnId y))

-- | Empty symbol var bimap
emptySymbolVarBimap :: SymbolVarBimap t
emptySymbolVarBimap = SymbolVarBimap Bimap.empty

lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t)
lookupBindingOfSymbol s (SymbolVarBimap m) = Bimap.lookup s m

lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol
lookupSymbolOfBinding b (SymbolVarBimap m) = Bimap.lookupR b m

------------------------------------------------------------------------
-- MatlabSolverFn

-- Parameter @t@ is a phantom type brand used to track nonces.
data MatlabFnWrapper t c where
   MatlabFnWrapper :: !(MatlabSolverFn (Expr t) a r) -> MatlabFnWrapper t (a::> r)

instance TestEquality (MatlabFnWrapper t) where
  testEquality (MatlabFnWrapper f) (MatlabFnWrapper g) = do
    Refl <- testSolverFnEq f g
    return Refl


instance HashableF (MatlabFnWrapper t) where
  hashWithSaltF s (MatlabFnWrapper f) = hashWithSalt s f

data ExprSymFnWrapper t c
   = forall a r . (c ~ (a ::> r)) => ExprSymFnWrapper (ExprSymFn t (Expr t) a r)

data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)

------------------------------------------------------------------------
-- ExprBuilder

-- | Mode flag for how floating-point values should be interpreted.
data FloatMode where
  FloatIEEE :: FloatMode
  FloatUninterpreted :: FloatMode
  FloatReal :: FloatMode
type FloatIEEE = 'FloatIEEE
type FloatUninterpreted = 'FloatUninterpreted
type FloatReal = 'FloatReal

data Flags (fi :: FloatMode)


data FloatModeRepr :: FloatMode -> Type where
  FloatIEEERepr          :: FloatModeRepr FloatIEEE
  FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
  FloatRealRepr          :: FloatModeRepr FloatReal

instance Show (FloatModeRepr fm) where
  showsPrec _ FloatIEEERepr          = showString "FloatIEEE"
  showsPrec _ FloatUninterpretedRepr = showString "FloatUninterpreted"
  showsPrec _ FloatRealRepr          = showString "FloatReal"

instance ShowF FloatModeRepr

instance KnownRepr FloatModeRepr FloatIEEE          where knownRepr = FloatIEEERepr
instance KnownRepr FloatModeRepr FloatUninterpreted where knownRepr = FloatUninterpretedRepr
instance KnownRepr FloatModeRepr FloatReal          where knownRepr = FloatRealRepr

instance TestEquality FloatModeRepr where
  testEquality FloatIEEERepr           FloatIEEERepr           = return Refl
  testEquality FloatUninterpretedRepr  FloatUninterpretedRepr  = return Refl
  testEquality FloatRealRepr           FloatRealRepr           = return Refl
  testEquality _ _ = Nothing


-- | Cache for storing dag terms.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprBuilder t (st :: Type -> Type) (fs :: Type)
   = forall fm. (fs ~ (Flags fm)) =>
     SB { sbTrue  :: !(BoolExpr t)
        , sbFalse :: !(BoolExpr t)
          -- | Constant zero.
        , sbZero  :: !(RealExpr t)
          -- | Configuration object for this symbolic backend
        , sbConfiguration :: !CFG.Config
          -- | Flag used to tell the backend whether to evaluate
          -- ground rational values as double precision floats when
          -- a function cannot be evaluated as a rational.
        , sbFloatReduce :: !Bool
          -- | The maximum number of distinct values a term may have and use the
          -- unary representation.
        , sbUnaryThreshold :: !(CFG.OptionSetting BaseIntegerType)
          -- | The maximum number of distinct ranges in a BVDomain expression.
        , sbBVDomainRangeLimit :: !(CFG.OptionSetting BaseIntegerType)
          -- | The starting size when building a new cache
        , sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType)
          -- | Counter to generate new unique identifiers for elements and functions.
        , exprCounter :: !(NonceGenerator IO t)
          -- | Reference to current allocator for expressions.
        , curAllocator :: !(IORef (ExprAllocator t))
          -- | Number of times an 'Expr' for a non-linear operation has been
          -- created.
        , sbNonLinearOps :: !(IORef Integer)
          -- | The current program location
        , sbProgramLoc :: !(IORef ProgramLoc)
          -- | Additional state maintained by the state manager
        , sbStateManager :: !(IORef (st t))

        , sbVarBindings :: !(IORef (SymbolVarBimap t))
        , sbUninterpFnCache :: !(IORef (Map (SolverSymbol, Some (Ctx.Assignment BaseTypeRepr)) (SomeSymFn (ExprBuilder t st fs))))
          -- | Cache for Matlab functions
        , sbMatlabFnCache
          :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
        , sbSolverLogger
          :: !(IORef (Maybe (SolverEvent -> IO ())))
          -- | Flag dictating how floating-point values/operations are translated
          -- when passed to the solver.
        , sbFloatMode :: !(FloatModeRepr fm)
        }

type instance SymFn (ExprBuilder t st fs) = ExprSymFn t (Expr t)
type instance SymExpr (ExprBuilder t st fs) = Expr t
type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t
type instance SymAnnotation (ExprBuilder t st fs) = Nonce t

-- | Get abstract value associated with element.
exprAbsValue :: Expr t tp -> AbstractValue tp
exprAbsValue (SemiRingLiteral sr x _) =
  case sr of
    SR.SemiRingNatRepr  -> natSingleRange x
    SR.SemiRingIntegerRepr  -> singleRange x
    SR.SemiRingRealRepr -> ravSingle x
    SR.SemiRingBVRepr _ w -> BVD.singleton w (BV.asUnsigned x)

exprAbsValue (StringExpr l _) = stringAbsSingle l
exprAbsValue (BoolExpr b _)   = Just b
exprAbsValue (NonceAppExpr e) = nonceExprAbsValue e
exprAbsValue (AppExpr e)      = appExprAbsValue e
exprAbsValue (BoundVarExpr v) =
  fromMaybe (unconstrainedAbsValue (bvarType v)) (bvarAbstractValue v)

instance HasAbsValue (Expr t) where
  getAbsValue = exprAbsValue

------------------------------------------------------------------------
-- | ExprAllocator provides an interface for creating expressions from
-- an applications.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprAllocator t
   = ExprAllocator { appExpr  :: forall tp
                            .  ProgramLoc
                            -> App (Expr t) tp
                            -> AbstractValue tp
                            -> IO (Expr t tp)
                  , nonceExpr :: forall tp
                             .  ProgramLoc
                             -> NonceApp t (Expr t) tp
                             -> AbstractValue tp
                             -> IO (Expr t tp)
                  }

------------------------------------------------------------------------
-- Expr operations

{-# INLINE compareExpr #-}
compareExpr :: Expr t x -> Expr t y -> OrderingF x y

-- Special case, ignore the BV semiring flavor for this purpose
compareExpr (SemiRingLiteral (SR.SemiRingBVRepr _ wx) x _) (SemiRingLiteral (SR.SemiRingBVRepr _ wy) y _) =
  case compareF wx wy of
    LTF -> LTF
    EQF -> fromOrdering (compare x y)
    GTF -> GTF
compareExpr (SemiRingLiteral srx x _) (SemiRingLiteral sry y _) =
  case compareF srx sry of
    LTF -> LTF
    EQF -> fromOrdering (SR.sr_compare srx x y)
    GTF -> GTF
compareExpr SemiRingLiteral{} _ = LTF
compareExpr _ SemiRingLiteral{} = GTF

compareExpr (StringExpr x _) (StringExpr y _) =
  case compareF x y of
    LTF -> LTF
    EQF -> EQF
    GTF -> GTF

compareExpr StringExpr{} _ = LTF
compareExpr _ StringExpr{} = GTF

compareExpr (BoolExpr x _) (BoolExpr y _) = fromOrdering (compare x y)
compareExpr BoolExpr{} _ = LTF
compareExpr _ BoolExpr{} = GTF

compareExpr (NonceAppExpr x) (NonceAppExpr y) = compareF x y
compareExpr NonceAppExpr{} _ = LTF
compareExpr _ NonceAppExpr{} = GTF

compareExpr (AppExpr x) (AppExpr y) = compareF (appExprId x) (appExprId y)
compareExpr AppExpr{} _ = LTF
compareExpr _ AppExpr{} = GTF

compareExpr (BoundVarExpr x) (BoundVarExpr y) = compareF x y

instance TestEquality (NonceAppExpr t) where
  testEquality x y =
    case compareF x y of
      EQF -> Just Refl
      _ -> Nothing

instance OrdF (NonceAppExpr t)  where
  compareF x y = compareF (nonceExprId x) (nonceExprId y)

instance Eq (NonceAppExpr t tp) where
  x == y = isJust (testEquality x y)

instance Ord (NonceAppExpr t tp) where
  compare x y = toOrdering (compareF x y)

instance TestEquality (Expr t) where
  testEquality x y =
    case compareF x y of
      EQF -> Just Refl
      _ -> Nothing

instance OrdF (Expr t)  where
  compareF = compareExpr

instance Eq (Expr t tp) where
  x == y = isJust (testEquality x y)

instance Ord (Expr t tp) where
  compare x y = toOrdering (compareF x y)

instance Hashable (Expr t tp) where
  hashWithSalt s (BoolExpr b _) = hashWithSalt (hashWithSalt s (0::Int)) b
  hashWithSalt s (SemiRingLiteral sr x _) =
    case sr of
      SR.SemiRingNatRepr     -> hashWithSalt (hashWithSalt s (1::Int)) x
      SR.SemiRingIntegerRepr -> hashWithSalt (hashWithSalt s (2::Int)) x
      SR.SemiRingRealRepr    -> hashWithSalt (hashWithSalt s (3::Int)) x
      SR.SemiRingBVRepr _ w  -> hashWithSalt (hashWithSaltF (hashWithSalt s (4::Int)) w) x

  hashWithSalt s (StringExpr x _) = hashWithSalt (hashWithSalt s (5::Int)) x
  hashWithSalt s (AppExpr x)      = hashWithSalt (hashWithSalt s (6::Int)) (appExprId x)
  hashWithSalt s (NonceAppExpr x) = hashWithSalt (hashWithSalt s (7::Int)) (nonceExprId x)
  hashWithSalt s (BoundVarExpr x) = hashWithSalt (hashWithSalt s (8::Int)) x

instance PH.HashableF (Expr t) where
  hashWithSaltF = hashWithSalt

------------------------------------------------------------------------
-- PPIndex

data PPIndex
   = ExprPPIndex {-# UNPACK #-} !Word64
   | RatPPIndex !Rational
  deriving (Eq, Ord, Generic)

instance Hashable PPIndex

------------------------------------------------------------------------
-- countOccurrences

countOccurrences :: Expr t tp -> Map.Map PPIndex Int
countOccurrences e0 = runST $ do
  visited <- H.new
  countOccurrences' visited e0
  Map.fromList <$> H.toList visited

type OccurrenceTable s = H.HashTable s PPIndex Int


incOccurrence :: OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence visited idx sub = do
  mv <- H.lookup visited idx
  case mv of
    Just i -> H.insert visited idx $! i+1
    Nothing -> sub >> H.insert visited idx 1

-- FIXME... why does this ignore Nat and Int literals?
countOccurrences' :: forall t tp s . OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' visited (SemiRingLiteral SR.SemiRingRealRepr r _) = do
  incOccurrence visited (RatPPIndex r) $
    return ()
countOccurrences' visited (AppExpr e) = do
  let idx = ExprPPIndex (indexValue (appExprId e))
  incOccurrence visited idx $ do
    traverseFC_ (countOccurrences' visited) (appExprApp e)
countOccurrences' visited (NonceAppExpr e) = do
  let idx = ExprPPIndex (indexValue (nonceExprId e))
  incOccurrence visited idx $ do
    traverseFC_ (countOccurrences' visited) (nonceExprApp e)
countOccurrences' _ _ = return ()

------------------------------------------------------------------------
-- boundVars

type BoundVarMap s t = H.HashTable s PPIndex (Set (Some (ExprBoundVar t)))

cache :: (Eq k, Hashable k) => H.HashTable s k r -> k -> ST s r -> ST s r
cache h k m = do
  mr <- H.lookup h k
  case mr of
    Just r -> return r
    Nothing -> do
      r <- m
      H.insert h k r
      return r


boundVars :: Expr t tp -> ST s (BoundVarMap s t)
boundVars e0 = do
  visited <- H.new
  _ <- boundVars' visited e0
  return visited

boundVars' :: BoundVarMap s t
           -> Expr t tp
           -> ST s (Set (Some (ExprBoundVar t)))
boundVars' visited (AppExpr e) = do
  let idx = indexValue (appExprId e)
  cache visited (ExprPPIndex idx) $ do
    sums <- sequence (toListFC (boundVars' visited) (appExprApp e))
    return $ foldl' Set.union Set.empty sums
boundVars' visited (NonceAppExpr e) = do
  let idx = indexValue (nonceExprId e)
  cache visited (ExprPPIndex idx) $ do
    sums <- sequence (toListFC (boundVars' visited) (nonceExprApp e))
    return $ foldl' Set.union Set.empty sums
boundVars' visited (BoundVarExpr v)
  | QuantifierVarKind <- bvarKind v = do
      let idx = indexValue (bvarId v)
      cache visited (ExprPPIndex idx) $
        return (Set.singleton (Some v))
boundVars' _ _ = return Set.empty

------------------------------------------------------------------------
-- Pretty printing

instance Show (Expr t tp) where
  show = show . ppExpr

instance Pretty (Expr t tp) where
  pretty = ppExpr


-- | @AppPPExpr@ represents a an application, and it may be let bound.
data AppPPExpr
   = APE { apeIndex :: !PPIndex
         , apeLoc :: !ProgramLoc
         , apeName :: !Text
         , apeExprs :: ![PPExpr]
         , apeLength :: !Int
           -- ^ Length of AppPPExpr not including parenthesis.
         }

data PPExpr
   = FixedPPExpr !Doc ![Doc] !Int
     -- ^ A fixed doc with length.
   | AppPPExpr !AppPPExpr
     -- ^ A doc that can be let bound.

-- | Pretty print a AppPPExpr
apeDoc :: AppPPExpr -> (Doc, [Doc])
apeDoc a = (text (Text.unpack (apeName a)), ppExprDoc True <$> apeExprs a)

textPPExpr :: Text -> PPExpr
textPPExpr t = FixedPPExpr (text (Text.unpack t)) [] (Text.length t)

stringPPExpr :: String -> PPExpr
stringPPExpr t = FixedPPExpr (text t) [] (length t)

-- | Get length of Expr including parens.
ppExprLength :: PPExpr -> Int
ppExprLength (FixedPPExpr _ [] n) = n
ppExprLength (FixedPPExpr _ _ n) = n + 2
ppExprLength (AppPPExpr a) = apeLength a + 2

parenIf :: Bool -> Doc -> [Doc] -> Doc
parenIf _ h [] = h
parenIf False h l = hsep (h:l)
parenIf True h l = parens (hsep (h:l))

-- | Pretty print PPExpr
ppExprDoc :: Bool -> PPExpr -> Doc
ppExprDoc b (FixedPPExpr d a _) = parenIf b d a
ppExprDoc b (AppPPExpr a) = uncurry (parenIf b) (apeDoc a)

data PPExprOpts = PPExprOpts { ppExpr_maxWidth :: Int
                           , ppExpr_useDecimal :: Bool
                           }

defaultPPExprOpts :: PPExprOpts
defaultPPExprOpts =
  PPExprOpts { ppExpr_maxWidth = 68
            , ppExpr_useDecimal = True
            }

-- | Pretty print an 'Expr' using let bindings to create the term.
ppExpr :: Expr t tp -> Doc
ppExpr e
     | Prelude.null bindings = ppExprDoc False r
     | otherwise =
         text "let" <+> align (vcat bindings) PP.<$>
         text " in" <+> align (ppExprDoc False r)
  where (bindings,r) = runST (ppExpr' e defaultPPExprOpts)

instance ShowF (Expr t)

-- | Pretty print the top part of an element.
ppExprTop :: Expr t tp -> Doc
ppExprTop e = ppExprDoc False r
  where (_,r) = runST (ppExpr' e defaultPPExprOpts)

-- | Contains the elements before, the index, doc, and width and
-- the elements after.
type SplitPPExprList = Maybe ([PPExpr], AppPPExpr, [PPExpr])

findExprToRemove :: [PPExpr] -> SplitPPExprList
findExprToRemove exprs0 = go [] exprs0 Nothing
  where go :: [PPExpr] -> [PPExpr] -> SplitPPExprList -> SplitPPExprList
        go _ [] mr = mr
        go prev (e@FixedPPExpr{} : exprs) mr = do
          go (e:prev) exprs mr
        go prev (AppPPExpr a:exprs) mr@(Just (_,a',_))
          | apeLength a < apeLength a' = go (AppPPExpr a:prev) exprs mr
        go prev (AppPPExpr a:exprs) _ = do
          go (AppPPExpr a:prev) exprs (Just (reverse prev, a, exprs))


ppExpr' :: forall t tp s . Expr t tp -> PPExprOpts -> ST s ([Doc], PPExpr)
ppExpr' e0 o = do
  let max_width = ppExpr_maxWidth o
  let use_decimal = ppExpr_useDecimal o
  -- Get map that counts number of elements.
  let m = countOccurrences e0
  -- Return number of times a term is referred to in dag.
  let isShared :: PPIndex -> Bool
      isShared w = fromMaybe 0 (Map.lookup w m) > 1

  -- Get bounds variables.
  bvars <- boundVars e0

  bindingsRef <- newSTRef Seq.empty

  visited <- H.new :: ST s (H.HashTable s PPIndex PPExpr)
  visited_fns <- H.new :: ST s (H.HashTable s Word64 Text)

  let -- Add a binding to the list of bindings
      addBinding :: AppPPExpr -> ST s PPExpr
      addBinding a = do
        let idx = apeIndex a
        cnt <- Seq.length <$> readSTRef bindingsRef

        vars <- fromMaybe Set.empty <$> H.lookup bvars idx
        let args :: [String]
            args = viewSome ppBoundVar <$> Set.toList vars

        let nm = case idx of
                   ExprPPIndex e -> "v" ++ show e
                   RatPPIndex _ -> "r" ++ show cnt
        let lhs = parenIf False (text nm) (text <$> args)
        let doc = text "--" <+> pretty (plSourceLoc (apeLoc a)) <$$>
                  lhs <+> text "=" <+> uncurry (parenIf False) (apeDoc a)
        modifySTRef' bindingsRef (Seq.|> doc)
        let len = length nm + sum ((\arg_s -> length arg_s + 1) <$> args)
        let nm_expr = FixedPPExpr (text nm) (map text args) len
        H.insert visited idx $! nm_expr
        return nm_expr

  let fixLength :: Int
                -> [PPExpr]
                -> ST s ([PPExpr], Int)
      fixLength cur_width exprs
        | cur_width > max_width
        , Just (prev_e, a, next_e) <- findExprToRemove exprs = do
          r <- addBinding a
          let exprs' = prev_e ++ [r] ++ next_e
          fixLength (cur_width - apeLength a + ppExprLength r) exprs'
      fixLength cur_width exprs = do
        return $! (exprs, cur_width)

  -- Pretty print an argument.
  let renderArg :: PrettyArg (Expr t) -> ST s PPExpr
      renderArg (PrettyArg e) = getBindings e
      renderArg (PrettyText txt) = return (textPPExpr txt)
      renderArg (PrettyFunc nm args) =
        do exprs0 <- traverse renderArg args
           let total_width = Text.length nm + sum ((\e -> 1 + ppExprLength e) <$> exprs0)
           (exprs1, cur_width) <- fixLength total_width exprs0
           let exprs = map (ppExprDoc True) exprs1
           return (FixedPPExpr (text (Text.unpack nm)) exprs cur_width)

      renderApp :: PPIndex
                -> ProgramLoc
                -> Text
                -> [PrettyArg (Expr t)]
                -> ST s AppPPExpr
      renderApp idx loc nm args = Ex.assert (not (Prelude.null args)) $ do
        exprs0 <- traverse renderArg args
        -- Get width not including parenthesis of outer app.
        let total_width = Text.length nm + sum ((\e -> 1 + ppExprLength e) <$> exprs0)
        (exprs, cur_width) <- fixLength total_width exprs0
        return APE { apeIndex = idx
                   , apeLoc = loc
                   , apeName = nm
                   , apeExprs = exprs
                   , apeLength = cur_width
                   }

      cacheResult :: PPIndex
                  -> ProgramLoc
                  -> PrettyApp (Expr t)
                  -> ST s PPExpr
      cacheResult _ _ (nm,[]) = do
        return (textPPExpr nm)
      cacheResult idx loc (nm,args) = do
        mr <- H.lookup visited idx
        case mr of
          Just d -> return d
          Nothing -> do
            a <- renderApp idx loc nm args
            if isShared idx then
              addBinding a
             else
              return (AppPPExpr a)

      bindFn :: ExprSymFn t (Expr t) idx ret -> ST s (PrettyArg (Expr t))
      bindFn f = do
        let idx = indexValue (symFnId f)
        mr <- H.lookup visited_fns idx
        case mr of
          Just d -> return (PrettyText d)
          Nothing -> do
            case symFnInfo f of
              UninterpFnInfo{} -> do
                let def_doc = text (show f) <+> text "=" <+> text "??"
                modifySTRef' bindingsRef (Seq.|> def_doc)
              DefinedFnInfo vars rhs _ -> do
                let pp_vars = toListFC (text . ppBoundVar) vars
                let def_doc = text (show f) <+> hsep pp_vars <+> text "=" <+> ppExpr rhs
                modifySTRef' bindingsRef (Seq.|> def_doc)
              MatlabSolverFnInfo fn_id _ _ -> do
                let def_doc = text (show f) <+> text "=" <+> ppMatlabSolverFn fn_id
                modifySTRef' bindingsRef (Seq.|> def_doc)

            let d = Text.pack (show f)
            H.insert visited_fns idx $! d
            return $! PrettyText d

      -- Collect definitions for all applications that occur multiple times
      -- in term.
      getBindings :: Expr t u -> ST s PPExpr
      getBindings (SemiRingLiteral sr x l) =
        case sr of
          SR.SemiRingNatRepr ->
            return $ stringPPExpr (show x)
          SR.SemiRingIntegerRepr ->
            return $ stringPPExpr (show x)
          SR.SemiRingRealRepr -> cacheResult (RatPPIndex x) l app
             where n = numerator x
                   d = denominator x
                   app | d == 1      = prettyApp (fromString (show n)) []
                       | use_decimal = prettyApp (fromString (show (fromRational x :: Double))) []
                       | otherwise   = prettyApp "divReal"  [ showPrettyArg n, showPrettyArg d ]
          SR.SemiRingBVRepr _ w ->
            return $ stringPPExpr $ BV.ppHex w x

      getBindings (StringExpr x _) =
        return $ stringPPExpr $ (show x)
      getBindings (BoolExpr b _) =
        return $ stringPPExpr (if b then "true" else "false")
      getBindings (NonceAppExpr e) =
        cacheResult (ExprPPIndex (indexValue (nonceExprId e))) (nonceExprLoc e)
          =<< ppNonceApp bindFn (nonceExprApp e)
      getBindings (AppExpr e) =
        cacheResult (ExprPPIndex (indexValue (appExprId e)))
                    (appExprLoc e)
                    (ppApp' (appExprApp e))
      getBindings (BoundVarExpr i) =
        return $ stringPPExpr $ ppBoundVar i

  r <- getBindings e0
  bindings <- toList <$> readSTRef bindingsRef
  return (toList bindings, r)


------------------------------------------------------------------------
-- Uncached storage

-- | Create a new storage that does not do hash consing.
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage g = do
  return $! ExprAllocator { appExpr = uncachedExprFn g
                         , nonceExpr = uncachedNonceExpr g
                         }

uncachedExprFn :: NonceGenerator IO t
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
uncachedExprFn g pc a v = do
  n <- freshNonce g
  return $! mkExpr n pc a v

uncachedNonceExpr :: NonceGenerator IO t
                 -> ProgramLoc
                 -> NonceApp t (Expr t) tp
                 -> AbstractValue tp
                 -> IO (Expr t tp)
uncachedNonceExpr g pc p v = do
  n <- freshNonce g
  return $! NonceAppExpr $ NonceAppExprCtor { nonceExprId = n
                                          , nonceExprLoc = pc
                                          , nonceExprApp = p
                                          , nonceExprAbsValue = v
                                          }

------------------------------------------------------------------------
-- Cached storage

cachedNonceExpr :: NonceGenerator IO t
               -> PH.HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
               -> ProgramLoc
               -> NonceApp t (Expr t) tp
               -> AbstractValue tp
               -> IO (Expr t tp)
cachedNonceExpr g h pc p v = do
  me <- stToIO $ PH.lookup h p
  case me of
    Just e -> return e
    Nothing -> do
      n <- freshNonce g
      let e = NonceAppExpr $ NonceAppExprCtor { nonceExprId = n
                                            , nonceExprLoc = pc
                                            , nonceExprApp = p
                                            , nonceExprAbsValue = v
                                            }
      seq e $ stToIO $ PH.insert h p e
      return $! e


cachedAppExpr :: forall t tp
               . NonceGenerator IO t
              -> PH.HashTable RealWorld (App (Expr t)) (Expr t)
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
cachedAppExpr g h pc a v = do
  me <- stToIO $ PH.lookup h a
  case me of
    Just e -> return e
    Nothing -> do
      n <- freshNonce g
      let e = mkExpr n pc a v
      seq e $ stToIO $ PH.insert h a e
      return e

-- | Create a storage that does hash consing.
newCachedStorage :: forall t
                  . NonceGenerator IO t
                 -> Int
                 -> IO (ExprAllocator t)
newCachedStorage g sz = stToIO $ do
  appCache  <- PH.newSized sz
  predCache <- PH.newSized sz
  return $ ExprAllocator { appExpr = cachedAppExpr g appCache
                        , nonceExpr = cachedNonceExpr g predCache
                        }

instance PolyEq (Expr t x) (Expr t y) where
  polyEqF x y = do
    Refl <- testEquality x y
    return Refl


------------------------------------------------------------------------
-- IdxCache

-- | An IdxCache is used to map expressions with type @Expr t tp@ to
-- values with a corresponding type @f tp@. It is a mutable map using
-- an 'IO' hash table. Parameter @t@ is a phantom type brand used to
-- track nonces.
newtype IdxCache t (f :: BaseType -> Type)
      = IdxCache { cMap :: IORef (PM.MapF (Nonce t) f) }

-- | Create a new IdxCache
newIdxCache :: MonadIO m => m (IdxCache t f)
newIdxCache = liftIO $ IdxCache <$> newIORef PM.empty

{-# INLINE lookupIdxValue #-}
-- | Return the value associated to the expr in the index.
lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp))
lookupIdxValue _ SemiRingLiteral{} = return Nothing
lookupIdxValue _ StringExpr{} = return Nothing
lookupIdxValue _ BoolExpr{} = return Nothing
lookupIdxValue c (NonceAppExpr e) = lookupIdx c (nonceExprId e)
lookupIdxValue c (AppExpr e)  = lookupIdx c (appExprId e)
lookupIdxValue c (BoundVarExpr i) = lookupIdx c (bvarId i)

{-# INLINE lookupIdx #-}
lookupIdx :: (MonadIO m) => IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx c n = liftIO $ PM.lookup n <$> readIORef (cMap c)

{-# INLINE insertIdxValue #-}
-- | Bind the value to the given expr in the index.
insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m ()
insertIdxValue c e v = seq v $ liftIO $ modifyIORef (cMap c) $ PM.insert e v

{-# INLINE deleteIdxValue #-}
-- | Remove a value from the IdxCache
deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m ()
deleteIdxValue c e = liftIO $ modifyIORef (cMap c) $ PM.delete e

-- | Remove all values from the IdxCache
clearIdxCache :: MonadIO m => IdxCache t f -> m ()
clearIdxCache c = liftIO $ writeIORef (cMap c) PM.empty

exprMaybeId :: Expr t tp -> Maybe (Nonce t tp)
exprMaybeId SemiRingLiteral{} = Nothing
exprMaybeId StringExpr{} = Nothing
exprMaybeId BoolExpr{} = Nothing
exprMaybeId (NonceAppExpr e) = Just $! nonceExprId e
exprMaybeId (AppExpr  e) = Just $! appExprId e
exprMaybeId (BoundVarExpr e) = Just $! bvarId e

-- | Implements a cached evaluated using the given element.  Given an element
-- this function returns the value of the element if bound, and otherwise
-- calls the evaluation function, stores the result in the cache, and
-- returns the value.
{-# INLINE idxCacheEval #-}
idxCacheEval :: (MonadIO m)
             => IdxCache t f
             -> Expr t tp
             -> m (f tp)
             -> m (f tp)
idxCacheEval c e m = do
  case exprMaybeId e of
    Nothing -> m
    Just n -> idxCacheEval' c n m

-- | Implements a cached evaluated using the given element.  Given an element
-- this function returns the value of the element if bound, and otherwise
-- calls the evaluation function, stores the result in the cache, and
-- returns the value.
{-# INLINE idxCacheEval' #-}
idxCacheEval' :: (MonadIO m)
              => IdxCache t f
              -> Nonce t tp
              -> m (f tp)
              -> m (f tp)
idxCacheEval' c n m = do
  mr <- lookupIdx c n
  case mr of
    Just r -> return r
    Nothing -> do
      r <- m
      insertIdxValue c n r
      return r

------------------------------------------------------------------------
-- ExprBuilder operations

curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc sym = readIORef (sbProgramLoc sym)

-- | Create an element from a nonce app.
sbNonceExpr :: ExprBuilder t st fs
           -> NonceApp t (Expr t) tp
           -> IO (Expr t tp)
sbNonceExpr sym a = do
  s <- readIORef (curAllocator sym)
  pc <- curProgramLoc sym
  nonceExpr s pc a (quantAbsEval exprAbsValue a)

semiRingLit :: ExprBuilder t st fs
            -> SR.SemiRingRepr sr
            -> SR.Coefficient sr
            -> IO (Expr t (SR.SemiRingBase sr))
semiRingLit sb sr x = do
  l <- curProgramLoc sb
  return $! SemiRingLiteral sr x l

sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr sym a = do
  s <- readIORef (curAllocator sym)
  pc <- curProgramLoc sym
  let v = abstractEval exprAbsValue a
  when (isNonLinearApp a) $
    modifyIORef' (sbNonLinearOps sym) (+1)
  case appType a of
    -- Check if abstract interpretation concludes this is a constant.
    BaseBoolRepr | Just b <- v -> return $ backendPred sym b
    BaseNatRepr  | Just c <- asSingleNatRange v -> natLit sym c
    BaseIntegerRepr | Just c <- asSingleRange v -> intLit sym c
    BaseRealRepr | Just c <- asSingleRange (ravRange v) -> realLit sym c
    BaseBVRepr w | Just x <- BVD.asSingleton v -> bvLit sym w (BV.mkBV w x)
    _ -> appExpr s pc a v

-- | Update the binding to point to the current variable.
updateVarBinding :: ExprBuilder t st fs
                 -> SolverSymbol
                 -> SymbolBinding t
                 -> IO ()
updateVarBinding sym nm v
  | nm == emptySymbol = return ()
  | otherwise =
    modifyIORef' (sbVarBindings sym) $ (ins nm $! v)
  where ins n x (SymbolVarBimap m) = SymbolVarBimap (Bimap.insert n x m)

-- | Creates a new bound var.
sbMakeBoundVar :: ExprBuilder t st fs
               -> SolverSymbol
               -> BaseTypeRepr tp
               -> VarKind
               -> Maybe (AbstractValue tp)
               -> IO (ExprBoundVar t tp)
sbMakeBoundVar sym nm tp k absVal = do
  n  <- sbFreshIndex sym
  pc <- curProgramLoc sym
  return $! BVar { bvarId   = n
                 , bvarLoc  = pc
                 , bvarName = nm
                 , bvarType = tp
                 , bvarKind = k
                 , bvarAbstractValue = absVal
                 }

-- | Create fresh index
sbFreshIndex :: ExprBuilder t st fs -> IO (Nonce t (tp::BaseType))
sbFreshIndex sb = freshNonce (exprCounter sb)

sbFreshSymFnNonce :: ExprBuilder t st fs -> IO (Nonce t (ctx:: Ctx BaseType))
sbFreshSymFnNonce sb = freshNonce (exprCounter sb)

------------------------------------------------------------------------
-- Configuration option for controlling the maximum number of value a unary
-- threshold may have.

-- | Maximum number of values in unary bitvector encoding.
--
--   This option is named \"backend.unary_threshold\"
unaryThresholdOption :: CFG.ConfigOption BaseIntegerType
unaryThresholdOption = CFG.configOption BaseIntegerRepr "backend.unary_threshold"

-- | The configuration option for setting the maximum number of
-- values a unary threshold may have.
unaryThresholdDesc :: CFG.ConfigDesc
unaryThresholdDesc = CFG.mkOpt unaryThresholdOption sty help (Just (ConcreteInteger 0))
  where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)
        help = Just (text "Maximum number of values in unary bitvector encoding.")

------------------------------------------------------------------------
-- Configuration option for controlling how many disjoint ranges
-- should be allowed in bitvector domains.

-- | Maximum number of ranges in bitvector abstract domains.
--
--   This option is named \"backend.bvdomain_range_limit\"
bvdomainRangeLimitOption :: CFG.ConfigOption BaseIntegerType
bvdomainRangeLimitOption = CFG.configOption BaseIntegerRepr "backend.bvdomain_range_limit"

bvdomainRangeLimitDesc :: CFG.ConfigDesc
bvdomainRangeLimitDesc = CFG.mkOpt bvdomainRangeLimitOption sty help (Just (ConcreteInteger 2))
  where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)
        help = Just (text "Maximum number of ranges in bitvector domains.")

------------------------------------------------------------------------
-- Cache start size

-- | Starting size for element cache when caching is enabled.
--
--   This option is named \"backend.cache_start_size\"
cacheStartSizeOption :: CFG.ConfigOption BaseIntegerType
cacheStartSizeOption = CFG.configOption BaseIntegerRepr "backend.cache_start_size"

-- | The configuration option for setting the size of the initial hash set
-- used by simple builder
cacheStartSizeDesc :: CFG.ConfigDesc
cacheStartSizeDesc = CFG.mkOpt cacheStartSizeOption sty help (Just (ConcreteInteger 100000))
  where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)
        help = Just (text "Starting size for element cache")

------------------------------------------------------------------------
-- Cache terms

-- | Indicates if we should cache terms.  When enabled, hash-consing
--   is used to find and deduplicate common subexpressions.
--
--   This option is named \"use_cache\"
cacheTerms :: CFG.ConfigOption BaseBoolType
cacheTerms = CFG.configOption BaseBoolRepr "use_cache"

cacheOptStyle ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  CFG.OptionSetting BaseIntegerType ->
  CFG.OptionStyle BaseBoolType
cacheOptStyle gen storageRef szSetting =
  CFG.boolOptSty & CFG.set_opt_onset
        (\mb b -> f (fmap fromConcreteBool mb) (fromConcreteBool b) >> return CFG.optOK)
 where
 f :: Maybe Bool -> Bool -> IO ()
 f mb b | mb /= Just b = if b then start else stop
        | otherwise = return ()

 stop  = do s <- newStorage gen
            writeIORef storageRef s

 start = do sz <- CFG.getOpt szSetting
            s <- newCachedStorage gen (fromInteger sz)
            writeIORef storageRef s

cacheOptDesc ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  CFG.OptionSetting BaseIntegerType ->
  CFG.ConfigDesc
cacheOptDesc gen storageRef szSetting =
  CFG.mkOpt
    cacheTerms
    (cacheOptStyle gen storageRef szSetting)
    (Just (text "Use hash-consing during term construction"))
    (Just (ConcreteBool False))


newExprBuilder ::
  FloatModeRepr fm
  -- ^ Float interpretation mode (i.e., how are floats translated for the solver).
  -> st t
  -- ^ Current state for simple builder.
  -> NonceGenerator IO t
  -- ^ Nonce generator for names
  ->  IO (ExprBuilder t st (Flags fm))
newExprBuilder floatMode st gen = do
  st_ref <- newIORef st
  es <- newStorage gen

  let t = BoolExpr True initializationLoc
  let f = BoolExpr False initializationLoc
  let z = SemiRingLiteral SR.SemiRingRealRepr 0 initializationLoc

  loc_ref       <- newIORef initializationLoc
  storage_ref   <- newIORef es
  bindings_ref  <- newIORef emptySymbolVarBimap
  uninterp_fn_cache_ref <- newIORef Map.empty
  matlabFnCache <- stToIO $ PH.new
  loggerRef     <- newIORef Nothing

  -- Set up configuration options
  cfg <- CFG.initialConfig 0
           [ unaryThresholdDesc
           , bvdomainRangeLimitDesc
           , cacheStartSizeDesc
           ]
  unarySetting       <- CFG.getOptionSetting unaryThresholdOption cfg
  domainRangeSetting <- CFG.getOptionSetting bvdomainRangeLimitOption cfg
  cacheStartSetting  <- CFG.getOptionSetting cacheStartSizeOption cfg
  CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg
  nonLinearOps <- newIORef 0

  return $! SB { sbTrue  = t
               , sbFalse = f
               , sbZero = z
               , sbConfiguration = cfg
               , sbFloatReduce = True
               , sbUnaryThreshold = unarySetting
               , sbBVDomainRangeLimit = domainRangeSetting
               , sbCacheStartSize = cacheStartSetting
               , sbProgramLoc = loc_ref
               , exprCounter = gen
               , curAllocator = storage_ref
               , sbNonLinearOps = nonLinearOps
               , sbStateManager = st_ref
               , sbVarBindings = bindings_ref
               , sbUninterpFnCache = uninterp_fn_cache_ref
               , sbMatlabFnCache = matlabFnCache
               , sbSolverLogger = loggerRef
               , sbFloatMode = floatMode
               }

-- | Get current variable bindings.
getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap sym = readIORef (sbVarBindings sym)

-- | Stop caching applications in backend.
stopCaching :: ExprBuilder t st fs -> IO ()
stopCaching sb = do
  s <- newStorage (exprCounter sb)
  writeIORef (curAllocator sb) s

-- | Restart caching applications in backend (clears cache if it is currently caching).
startCaching :: ExprBuilder t st fs -> IO ()
startCaching sb = do
  sz <- CFG.getOpt (sbCacheStartSize sb)
  s <- newCachedStorage (exprCounter sb) (fromInteger sz)
  writeIORef (curAllocator sb) s

bvBinDivOp :: (1 <= w)
            => (NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)
            -> (NatRepr w -> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w))
            -> ExprBuilder t st fs
            -> BVExpr t w
            -> BVExpr t w
            -> IO (BVExpr t w)
bvBinDivOp f c sb x y = do
  let w = bvWidth x
  case (asBV x, asBV y) of
    (Just i, Just j) | j /= BV.zero w -> bvLit sb w $ f w i j
    _ -> sbMakeExpr sb $ c w x y

asConcreteIndices :: IsExpr e
                  => Ctx.Assignment e ctx
                  -> Maybe (Ctx.Assignment IndexLit ctx)
asConcreteIndices = traverseFC f
  where f :: IsExpr e => e tp -> Maybe (IndexLit tp)
        f x =
          case exprType x of
            BaseNatRepr  -> NatIndexLit . fromIntegral <$> asNat x
            BaseBVRepr w -> BVIndexLit w <$> asBV x
            _ -> Nothing

symbolicIndices :: forall sym ctx
                 . IsExprBuilder sym
                => sym
                -> Ctx.Assignment IndexLit ctx
                -> IO (Ctx.Assignment (SymExpr sym) ctx)
symbolicIndices sym = traverseFC f
  where f :: IndexLit tp -> IO (SymExpr sym tp)
        f (NatIndexLit n)  = natLit sym n
        f (BVIndexLit w i) = bvLit sym w i

-- | This evaluate a symbolic function against a set of arguments.
betaReduce :: ExprBuilder t st fs
           -> ExprSymFn t (Expr t) args ret
           -> Ctx.Assignment (Expr t) args
           -> IO (Expr t ret)
betaReduce sym f args =
  case symFnInfo f of
    UninterpFnInfo{} ->
      sbNonceExpr sym $! FnApp f args
    DefinedFnInfo bound_vars e _ -> do
      evalBoundVars sym e bound_vars args
    MatlabSolverFnInfo fn_id _ _ -> do
      evalMatlabSolverFn fn_id sym args

-- | This runs one action, and if it returns a value different from the input,
-- then it runs the second.  Otherwise it returns the result value passed in.
--
-- It is used when an action may modify a value, and we only want to run a
-- second action if the value changed.
runIfChanged :: Eq e
             => e
             -> (e -> IO e) -- ^ First action to run
             -> r           -- ^ Result if no change.
             -> (e -> IO r) -- ^ Second action to run
             -> IO r
runIfChanged x f unChanged onChange = do
  y <- f x
  if x == y then
    return unChanged
   else
    onChange y

-- | This adds a binding from the variable to itself in the hashtable
-- to ensure it can't be rebound.
recordBoundVar :: PH.HashTable RealWorld (Expr t) (Expr t)
                  -> ExprBoundVar t tp
                  -> IO ()
recordBoundVar tbl v = do
  let e = BoundVarExpr v
  mr <- stToIO $ PH.lookup tbl e
  case mr of
    Just r -> do
      when (r /= e) $ do
        fail $ "Simulator internal error; do not support rebinding variables."
    Nothing -> do
      -- Bind variable to itself to ensure we catch when it is used again.
      stToIO $ PH.insert tbl e e


-- | The CachedSymFn is used during evaluation to store the results of reducing
-- the definitions of symbolic functions.
--
-- For each function it stores a pair containing a 'Bool' that is true if the
-- function changed as a result of evaluating it, and the reduced function
-- after evaluation.
--
-- The second arguments contains the arguments with the return type appended.
data CachedSymFn t c
  = forall a r
    . (c ~ (a ::> r))
    => CachedSymFn Bool (ExprSymFn t (Expr t) a r)

-- | Data structure used for caching evaluation.
data EvalHashTables t
   = EvalHashTables { exprTable :: !(PH.HashTable RealWorld (Expr t) (Expr t))
                    , fnTable  :: !(PH.HashTable RealWorld (Nonce t) (CachedSymFn t))
                    }

-- | Evaluate a simple function.
--
-- This returns whether the function changed as a Boolean and the function itself.
evalSimpleFn :: EvalHashTables t
             -> ExprBuilder t st fs
             -> ExprSymFn t (Expr t) idx ret
             -> IO (Bool,ExprSymFn t (Expr t) idx ret)
evalSimpleFn tbl sym f =
  case symFnInfo f of
    UninterpFnInfo{} -> return (False, f)
    DefinedFnInfo vars e evalFn -> do
      let n = symFnId f
      let nm = symFnName f
      CachedSymFn changed f' <-
        cachedEval (fnTable tbl) n $ do
          traverseFC_ (recordBoundVar (exprTable tbl)) vars
          e' <- evalBoundVars' tbl sym e
          if e == e' then
            return $! CachedSymFn False f
           else
            CachedSymFn True <$> definedFn sym nm vars e' evalFn
      return (changed, f')
    MatlabSolverFnInfo{} -> return (False, f)

evalBoundVars' :: forall t st fs ret
               .  EvalHashTables t
               -> ExprBuilder t st fs
               -> Expr t ret
               -> IO (Expr t ret)
evalBoundVars' tbls sym e0 =
  case e0 of
    SemiRingLiteral{} -> return e0
    StringExpr{} -> return e0
    BoolExpr{} -> return e0
    AppExpr ae -> cachedEval (exprTable tbls) e0 $ do
      let a = appExprApp ae
      a' <- traverseApp (evalBoundVars' tbls sym) a
      if a == a' then
        return e0
       else
        reduceApp sym bvUnary a'
    NonceAppExpr ae -> cachedEval (exprTable tbls) e0 $ do
      case nonceExprApp ae of
        Annotation tpr n a -> do
          a' <- evalBoundVars' tbls sym a
          if a == a' then
            return e0
          else
            sbNonceExpr sym $ Annotation tpr n a'
        Forall v e -> do
          recordBoundVar (exprTable tbls) v
          -- Regenerate forallPred if e is changed by evaluation.
          runIfChanged e (evalBoundVars' tbls sym) e0 (forallPred sym v)
        Exists v e -> do
          recordBoundVar (exprTable tbls) v
          -- Regenerate forallPred if e is changed by evaluation.
          runIfChanged e (evalBoundVars' tbls sym) e0 (existsPred sym v)
        ArrayFromFn f -> do
          (changed, f') <- evalSimpleFn tbls sym f
          if not changed then
            return e0
           else
            arrayFromFn sym f'
        MapOverArrays f _ args -> do
          (changed, f') <- evalSimpleFn tbls sym f
          let evalWrapper :: ArrayResultWrapper (Expr t) (idx ::> itp) utp
                          -> IO (ArrayResultWrapper (Expr t) (idx ::> itp) utp)
              evalWrapper (ArrayResultWrapper a) =
                ArrayResultWrapper <$> evalBoundVars' tbls sym a
          args' <- traverseFC evalWrapper args
          if not changed && args == args' then
            return e0
           else
            arrayMap sym f' args'
        ArrayTrueOnEntries f a -> do
          (changed, f') <- evalSimpleFn tbls sym f
          a' <- evalBoundVars' tbls sym a
          if not changed && a == a' then
            return e0
           else
            arrayTrueOnEntries sym f' a'
        FnApp f a -> do
          (changed, f') <- evalSimpleFn tbls sym f
          a' <- traverseFC (evalBoundVars' tbls sym) a
          if not changed && a == a' then
            return e0
           else
            applySymFn sym f' a'

    BoundVarExpr{} -> cachedEval (exprTable tbls) e0 $ return e0

initHashTable :: (HashableF key, TestEquality key)
              => Ctx.Assignment key args
              -> Ctx.Assignment val args
              -> ST s (PH.HashTable s key val)
initHashTable keys vals = do
  let sz = Ctx.size keys
  tbl <- PH.newSized (Ctx.sizeInt sz)
  Ctx.forIndexM sz $ \i -> do
    PH.insert tbl (keys Ctx.! i) (vals Ctx.! i)
  return tbl

-- | This evaluates the term with the given bound variables rebound to
-- the given arguments.
--
-- The algorithm works by traversing the subterms in the term in a bottom-up
-- fashion while using a hash-table to memoize results for shared subterms.  The
-- hash-table is pre-populated so that the bound variables map to the element,
-- so we do not need any extra map lookup when checking to see if a variable is
-- bound.
--
-- NOTE: This function assumes that variables in the substitution are not
-- themselves bound in the term (e.g. in a function definition or quantifier).
-- If this is not respected, then 'evalBoundVars' will call 'fail' with an
-- error message.
evalBoundVars :: ExprBuilder t st fs
              -> Expr t ret
              -> Ctx.Assignment (ExprBoundVar t) args
              -> Ctx.Assignment (Expr t) args
              -> IO (Expr t ret)
evalBoundVars sym e vars exprs = do
  expr_tbl <- stToIO $ initHashTable (fmapFC BoundVarExpr vars) exprs
  fn_tbl  <- stToIO $ PH.new
  let tbls = EvalHashTables { exprTable = expr_tbl
                            , fnTable  = fn_tbl
                            }
  evalBoundVars' tbls sym e

-- | This attempts to lookup an entry in a symbolic array.
--
-- It patterns maps on the array constructor.
sbConcreteLookup :: forall t st fs d tp range
                 . ExprBuilder t st fs
                   -- ^ Simple builder for creating terms.
                 -> Expr t (BaseArrayType (d::>tp) range)
                    -- ^ Array to lookup value in.
                 -> Maybe (Ctx.Assignment IndexLit (d::>tp))
                    -- ^ A concrete index that corresponds to the index or nothing
                    -- if the index is symbolic.
                 -> Ctx.Assignment (Expr t) (d::>tp)
                    -- ^ The index to lookup.
                 -> IO (Expr t range)
sbConcreteLookup sym arr0 mcidx idx
    -- Try looking up a write to a concrete address.
  | Just (ArrayMap _ _ entry_map def) <- asApp arr0
  , Just cidx <- mcidx =
      case AUM.lookup cidx entry_map of
        Just v -> return v
        Nothing -> sbConcreteLookup sym def mcidx idx
    -- Evaluate function arrays on ground values.
  | Just (ArrayFromFn f) <- asNonceApp arr0 = do
      betaReduce sym f idx

    -- Lookups on constant arrays just return value
  | Just (ConstantArray _ _ v) <- asApp arr0 = do
      return v
    -- Lookups on mux arrays just distribute over mux.
  | Just (BaseIte _ _ p x y) <- asApp arr0 = do
      xv <- sbConcreteLookup sym x mcidx idx
      yv <- sbConcreteLookup sym y mcidx idx
      baseTypeIte sym p xv yv
  | Just (MapOverArrays f _ args) <- asNonceApp arr0 = do
      let eval :: ArrayResultWrapper (Expr t) (d::>tp) utp
               -> IO (Expr t utp)
          eval a = sbConcreteLookup sym (unwrapArrayResult a) mcidx idx
      betaReduce sym f =<< traverseFC eval args
    -- Create select index.
  | otherwise = do
    case exprType arr0 of
      BaseArrayRepr _ range ->
        sbMakeExpr sym (SelectArray range arr0 idx)

----------------------------------------------------------------------
-- Expression builder instances

-- | Evaluate a weighted sum of natural number values.
natSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SR.SemiRingNat -> IO (NatExpr t)
natSum sym s = semiRingSum sym s

-- | Evaluate a weighted sum of integer values.
intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SR.SemiRingInteger -> IO (IntegerExpr t)
intSum sym s = semiRingSum sym s

-- | Evaluate a weighted sum of real values.
realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SR.SemiRingReal -> IO (RealExpr t)
realSum sym s = semiRingSum sym s

bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SR.SemiRingBV flv w) -> IO (BVExpr t w)
bvSum sym s = semiRingSum sym s

conjPred :: ExprBuilder t st fs -> BoolMap (Expr t) -> IO (BoolExpr t)
conjPred sym bm =
  case BM.viewBoolMap bm of
    BoolMapUnit     -> return $ truePred sym
    BoolMapDualUnit -> return $ falsePred sym
    BoolMapTerms ((x,p):|[]) ->
      case p of
        Positive -> return x
        Negative -> notPred sym x
    _ -> sbMakeExpr sym $ ConjPred bm

bvUnary :: (1 <= w) => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary sym u
  -- BGS: We probably don't need to re-truncate the result, but
  -- until we refactor UnaryBV to use BV w instead of integer,
  -- that'll have to wait.
  | Just v <-  UnaryBV.asConstant u = bvLit sym w (BV.mkBV w v)
  | otherwise = sbMakeExpr sym (BVUnaryTerm u)
  where w = UnaryBV.width u

asUnaryBV :: (?unaryThreshold :: Int)
          => ExprBuilder t st fs
          -> BVExpr t n
          -> Maybe (UnaryBV (BoolExpr t) n)
asUnaryBV sym e
  | Just (BVUnaryTerm u) <- asApp e = Just u
  | ?unaryThreshold == 0 = Nothing
  | SemiRingLiteral (SR.SemiRingBVRepr _ w) v _ <- e = Just $ UnaryBV.constant sym w (BV.asUnsigned v)
  | otherwise = Nothing

-- | This create a unary bitvector representing if the size is not too large.
sbTryUnaryTerm :: (1 <= w, ?unaryThreshold :: Int)
               => ExprBuilder t st fs
               -> Maybe (IO (UnaryBV (BoolExpr t) w))
               -> IO (BVExpr t w)
               -> IO (BVExpr t w)
sbTryUnaryTerm _sym Nothing fallback = fallback
sbTryUnaryTerm sym (Just mku) fallback =
  do u <- mku
     if UnaryBV.size u < ?unaryThreshold then
       bvUnary sym u
     else
       fallback

semiRingProd ::
  ExprBuilder t st fs ->
  SemiRingProduct (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingProd sym pd
  | WSum.nullProd pd = semiRingLit sym (WSum.prodRepr pd) (SR.one (WSum.prodRepr pd))
  | Just v <- WSum.asProdVar pd = return v
  | otherwise = sbMakeExpr sym $ SemiRingProd pd

semiRingSum ::
  ExprBuilder t st fs ->
  WeightedSum (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingSum sym s
    | Just c <- WSum.asConstant s = semiRingLit sym (WSum.sumRepr s) c
    | Just r <- WSum.asVar s      = return r
    | otherwise                   = sum' sym s

sum' ::
  ExprBuilder t st fs ->
  WeightedSum (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
sum' sym s = sbMakeExpr sym $ SemiRingSum s
{-# INLINE sum' #-}

scalarMul ::
   ExprBuilder t st fs ->
   SR.SemiRingRepr sr ->
   SR.Coefficient sr ->
   Expr t (SR.SemiRingBase sr) ->
   IO (Expr t (SR.SemiRingBase sr))
scalarMul sym sr c x
  | SR.eq sr (SR.zero sr) c = semiRingLit sym sr (SR.zero sr)
  | SR.eq sr (SR.one sr)  c = return x
  | Just r <- asSemiRingLit sr x =
    semiRingLit sym sr (SR.mul sr c r)
  | Just s <- asSemiRingSum sr x =
    sum' sym (WSum.scale sr c s)
  | otherwise =
    sum' sym (WSum.scaledVar sr c x)

semiRingIte ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t BaseBoolType ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingIte sym sr c x y
    -- evaluate as constants
  | Just True  <- asConstantPred c = return x
  | Just False <- asConstantPred c = return y

    -- reduce negations
  | Just (NotPred c') <- asApp c
  = semiRingIte sym sr c' y x

    -- remove the ite if the then and else cases are the same
  | x == y = return x

    -- Try to extract common sum information.
  | (z, x',y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y)
  , not (WSum.isZero sr z) = do
    xr <- semiRingSum sym x'
    yr <- semiRingSum sym y'
    let sz = 1 + iteSize xr + iteSize yr
    r <- sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c xr yr)
    semiRingSum sym $! WSum.addVar sr z r

    -- final fallback, create the ite term
  | otherwise =
      let sz = 1 + iteSize x + iteSize y in
      sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c x y)


mkIte ::
  ExprBuilder t st fs ->
  Expr t BaseBoolType ->
  Expr t bt ->
  Expr t bt ->
  IO (Expr t bt)
mkIte sym c x y
    -- evaluate as constants
  | Just True  <- asConstantPred c = return x
  | Just False <- asConstantPred c = return y

    -- reduce negations
  | Just (NotPred c') <- asApp c
  = mkIte sym c' y x

    -- remove the ite if the then and else cases are the same
  | x == y = return x

  | otherwise =
      let sz = 1 + iteSize x + iteSize y in
      sbMakeExpr sym (BaseIte (exprType x) sz c x y)

semiRingLe ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))
      {- ^ recursive call for simplifications -} ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t BaseBoolType)
semiRingLe sym osr rec x y
      -- Check for syntactic equality.
    | x == y = return (truePred sym)

      -- Strength reductions on a non-linear constraint to piecewise linear.
    | Just c <- asSemiRingLit sr x
    , SR.eq sr c (SR.zero sr)
    , Just (SemiRingProd pd) <- asApp y
    , Just Refl <- testEquality sr (WSum.prodRepr pd)
    = prodNonneg sym osr pd

      -- Another strength reduction
    | Just c <- asSemiRingLit sr y
    , SR.eq sr c (SR.zero sr)
    , Just (SemiRingProd pd) <- asApp x
    , Just Refl <- testEquality sr (WSum.prodRepr pd)
    = prodNonpos sym osr pd

      -- Push some comparisons under if/then/else
    | SemiRingLiteral _ _ _ <- x
    , Just (BaseIte _ _ c a b) <- asApp y
    = join (itePred sym c <$> rec x a <*> rec x b)

      -- Push some comparisons under if/then/else
    | Just (BaseIte tp _ c a b) <- asApp x
    , SemiRingLiteral _ _ _ <- y
    , Just Refl <- testEquality tp (SR.semiRingBase sr)
    = join (itePred sym c <$> rec a y <*> rec b y)

      -- Try to extract common sum information.
    | (z, x',y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y)
    , not (WSum.isZero sr z) = do
      xr <- semiRingSum sym x'
      yr <- semiRingSum sym y'
      rec xr yr

      -- Default case
    | otherwise = sbMakeExpr sym $ SemiRingLe osr x y

 where sr = SR.orderedSemiRing osr


semiRingEq ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))
    {- ^ recursive call for simplifications -} ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t BaseBoolType)
semiRingEq sym sr rec x y
  -- Check for syntactic equality.
  | x == y = return (truePred sym)

    -- Push some equalities under if/then/else
  | SemiRingLiteral _ _ _ <- x
  , Just (BaseIte _ _ c a b) <- asApp y
  = join (itePred sym c <$> rec x a <*> rec x b)

    -- Push some equalities under if/then/else
  | Just (BaseIte _ _ c a b) <- asApp x
  , SemiRingLiteral _ _ _ <- y
  = join (itePred sym c <$> rec a y <*> rec b y)

  | (z, x',y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y)
  , not (WSum.isZero sr z) =
    case (WSum.asConstant x', WSum.asConstant y') of
      (Just a, Just b) -> return $! backendPred sym (SR.eq sr a b)
      _ -> do xr <- semiRingSum sym x'
              yr <- semiRingSum sym y'
              sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)

  | otherwise =
    sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min x y) (max x y)

semiRingAdd ::
  forall t st fs sr.
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingAdd sym sr x y =
    case (viewSemiRing sr x, viewSemiRing sr y) of
      (SR_Constant c, _) | SR.eq sr c (SR.zero sr) -> return y
      (_, SR_Constant c) | SR.eq sr c (SR.zero sr) -> return x

      (SR_Constant xc, SR_Constant yc) ->
        semiRingLit sym sr (SR.add sr xc yc)

      (SR_Constant xc, SR_Sum ys) ->
        sum' sym (WSum.addConstant sr ys xc)
      (SR_Sum xs, SR_Constant yc) ->
        sum' sym (WSum.addConstant sr xs yc)

      (SR_Constant xc, _)
        | Just (BaseIte _ _ cond a b) <- asApp y
        , isConstantSemiRingExpr a || isConstantSemiRingExpr b -> do
            xa <- semiRingAdd sym sr x a
            xb <- semiRingAdd sym sr x b
            semiRingIte sym sr cond xa xb
        | otherwise ->
            sum' sym (WSum.addConstant sr (WSum.var sr y) xc)

      (_, SR_Constant yc)
        | Just (BaseIte _ _ cond a b) <- asApp x
        , isConstantSemiRingExpr a || isConstantSemiRingExpr b -> do
            ay <- semiRingAdd sym sr a y
            by <- semiRingAdd sym sr b y
            semiRingIte sym sr cond ay by
        | otherwise ->
            sum' sym (WSum.addConstant sr (WSum.var sr x) yc)

      (SR_Sum xs, SR_Sum ys) -> semiRingSum sym (WSum.add sr xs ys)
      (SR_Sum xs, _)         -> semiRingSum sym (WSum.addVar sr xs y)
      (_ , SR_Sum ys)        -> semiRingSum sym (WSum.addVar sr ys x)
      _                      -> semiRingSum sym (WSum.addVars sr x y)
  where isConstantSemiRingExpr :: Expr t (SR.SemiRingBase sr) -> Bool
        isConstantSemiRingExpr (viewSemiRing sr -> SR_Constant _) = True
        isConstantSemiRingExpr _ = False

semiRingMul ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingMul sym sr x y =
  case (viewSemiRing sr x, viewSemiRing sr y) of
    (SR_Constant c, _) -> scalarMul sym sr c y
    (_, SR_Constant c) -> scalarMul sym sr c x

    (SR_Sum (WSum.asAffineVar -> Just (c,x',o)), _) ->
      do cxy <- scalarMul sym sr c =<< semiRingMul sym sr x' y
         oy  <- scalarMul sym sr o y
         semiRingAdd sym sr cxy oy

    (_, SR_Sum (WSum.asAffineVar -> Just (c,y',o))) ->
      do cxy <- scalarMul sym sr c =<< semiRingMul sym sr x y'
         ox  <- scalarMul sym sr o x
         semiRingAdd sym sr cxy ox

    (SR_Prod px, SR_Prod py) -> semiRingProd sym (WSum.prodMul px py)
    (SR_Prod px, _)          -> semiRingProd sym (WSum.prodMul px (WSum.prodVar sr y))
    (_, SR_Prod py)          -> semiRingProd sym (WSum.prodMul (WSum.prodVar sr x) py)
    _                        -> semiRingProd sym (WSum.prodMul (WSum.prodVar sr x) (WSum.prodVar sr y))


prodNonneg ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType)
prodNonneg sym osr pd =
  do let sr = SR.orderedSemiRing osr
     zero <- semiRingLit sym sr (SR.zero sr)
     fst <$> computeNonnegNonpos sym osr zero pd

prodNonpos ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType)
prodNonpos sym osr pd =
  do let sr = SR.orderedSemiRing osr
     zero <- semiRingLit sym sr (SR.zero sr)
     snd <$> computeNonnegNonpos sym osr zero pd

computeNonnegNonpos ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) {- zero element -} ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType, Expr t BaseBoolType)
computeNonnegNonpos sym osr zero pd =
   fromMaybe (truePred sym, falsePred sym) <$> WSum.prodEvalM merge single pd
 where

 single x = (,) <$> reduceApp sym bvUnary (SemiRingLe osr zero x) -- nonnegative
                <*> reduceApp sym bvUnary (SemiRingLe osr x zero) -- nonpositive

 merge (nn1, np1) (nn2, np2) =
   do nn <- join (orPred sym <$> andPred sym nn1 nn2 <*> andPred sym np1 np2)
      np <- join (orPred sym <$> andPred sym nn1 np2 <*> andPred sym np1 nn2)
      return (nn, np)



arrayResultIdxType :: BaseTypeRepr (BaseArrayType (idx ::> itp) d)
                   -> Ctx.Assignment BaseTypeRepr (idx ::> itp)
arrayResultIdxType (BaseArrayRepr idx _) = idx

-- | This decomposes A ExprBuilder array expression into a set of indices that
-- have been updated, and an underlying index.
data ArrayMapView i f tp
   = ArrayMapView { _arrayMapViewIndices :: !(AUM.ArrayUpdateMap f i tp)
                  , _arrayMapViewExpr    :: !(f (BaseArrayType i tp))
                  }

-- | Construct an 'ArrayMapView' for an element.
viewArrayMap :: Expr t (BaseArrayType i tp)
             -> ArrayMapView i (Expr t) tp
viewArrayMap  x
  | Just (ArrayMap _ _ m c) <- asApp x = ArrayMapView m c
  | otherwise = ArrayMapView AUM.empty x

-- | Construct an 'ArrayMapView' for an element.
underlyingArrayMapExpr :: ArrayResultWrapper (Expr t) i tp
                      -> ArrayResultWrapper (Expr t) i tp
underlyingArrayMapExpr x
  | Just (ArrayMap _ _ _ c) <- asApp (unwrapArrayResult x) = ArrayResultWrapper c
  | otherwise = x

-- | Return set of addresss in assignment that are written to by at least one expr
concreteArrayEntries :: forall t i ctx
                     .  Ctx.Assignment (ArrayResultWrapper (Expr t) i) ctx
                     -> Set (Ctx.Assignment IndexLit i)
concreteArrayEntries = foldlFC' f Set.empty
  where f :: Set (Ctx.Assignment IndexLit i)
          -> ArrayResultWrapper (Expr t) i tp
          -> Set (Ctx.Assignment IndexLit i)
        f s e
          | Just (ArrayMap _ _ m _) <- asApp (unwrapArrayResult  e) =
            Set.union s (AUM.keysSet m)
          | otherwise = s

data NatLit tp = (tp ~ BaseNatType) => NatLit Natural

asNatBounds :: Ctx.Assignment (Expr t) idx -> Maybe (Ctx.Assignment NatLit idx)
asNatBounds = traverseFC f
  where f :: Expr t tp -> Maybe (NatLit tp)
        f (SemiRingLiteral SR.SemiRingNatRepr n _) = Just (NatLit n)
        f _ = Nothing

foldBoundLeM :: (r -> Natural -> IO r) -> r -> Natural -> IO r
foldBoundLeM _ r 0 = pure r
foldBoundLeM f r n = do
  r' <- foldBoundLeM f r (n-1)
  f r' n

foldIndicesInRangeBounds :: forall sym idx r
                         .  IsExprBuilder sym
                         => sym
                         -> (r -> Ctx.Assignment (SymExpr sym) idx -> IO r)
                         -> r
                         -> Ctx.Assignment NatLit idx
                         -> IO r
foldIndicesInRangeBounds sym f0 a0 bnds0 = do
  case bnds0 of
    Ctx.Empty -> f0 a0 Ctx.empty
    bnds Ctx.:> NatLit b -> foldIndicesInRangeBounds sym (g f0) a0 bnds
      where g :: (r -> Ctx.Assignment (SymExpr sym) (idx0 ::> BaseNatType) -> IO r)
              -> r
              -> Ctx.Assignment (SymExpr sym) idx0
              -> IO r
            g f a i = foldBoundLeM (h f i) a b

            h :: (r -> Ctx.Assignment (SymExpr sym) (idx0 ::> BaseNatType) -> IO r)
              -> Ctx.Assignment (SymExpr sym) idx0
              -> r
              -> Natural
              -> IO r
            h f i a j = do
              je <- natLit sym j
              f a (i Ctx.:> je)

-- | Examine the list of terms, and determine if any one of them
--   appears in the given @BoolMap@ with the same polarity.
checkAbsorption ::
  BoolMap (Expr t) ->
  [(BoolExpr t, Polarity)] ->
  Bool
checkAbsorption _bm [] = False
checkAbsorption bm ((x,p):_)
  | Just p' <- BM.contains bm x, p == p' = True
checkAbsorption bm (_:xs) = checkAbsorption bm xs

-- | If @tryAndAbsorption x y@ returns @True@, that means that @y@
-- implies @x@, so that the conjunction @x AND y = y@. A @False@
-- result gives no information.
tryAndAbsorption ::
  BoolExpr t ->
  BoolExpr t ->
  Bool
tryAndAbsorption (asApp -> Just (NotPred (asApp -> Just (ConjPred as)))) (asConjunction -> bs)
  = checkAbsorption (BM.reversePolarities as) bs
tryAndAbsorption _ _ = False


-- | If @tryOrAbsorption x y@ returns @True@, that means that @x@
-- implies @y@, so that the disjunction @x OR y = y@. A @False@
-- result gives no information.
tryOrAbsorption ::
  BoolExpr t ->
  BoolExpr t ->
  Bool
tryOrAbsorption (asApp -> Just (ConjPred as)) (asDisjunction -> bs)
  = checkAbsorption as bs
tryOrAbsorption _ _ = False


-- | A slightly more aggressive syntactic equality check than testEquality,
--   `sameTerm` will recurse through a small collection of known syntax formers.
sameTerm :: Expr t a -> Expr t b -> Maybe (a :~: b)

sameTerm (asApp -> Just (FloatToBinary fppx x)) (asApp -> Just (FloatToBinary fppy y)) =
  do Refl <- testEquality fppx fppy
     Refl <- sameTerm x y
     return Refl

sameTerm x y = testEquality x y

instance IsExprBuilder (ExprBuilder t st fs) where
  getConfiguration = sbConfiguration

  setSolverLogListener sb = writeIORef (sbSolverLogger sb)
  getSolverLogListener sb = readIORef (sbSolverLogger sb)

  logSolverEvent sb ev =
    readIORef (sbSolverLogger sb) >>= \case
      Nothing -> return ()
      Just f  -> f ev

  getStatistics sb = do
    allocs <- countNoncesGenerated (exprCounter sb)
    nonLinearOps <- readIORef (sbNonLinearOps sb)
    return $ Statistics { statAllocs = allocs
                        , statNonLinearOps = nonLinearOps }

  annotateTerm sym e =
    case e of
      NonceAppExpr (nonceExprApp -> Annotation _ n _) -> return (n, e)
      _ -> do
        let tpr = exprType e
        n <- sbFreshIndex sym
        e' <- sbNonceExpr sym (Annotation tpr n e)
        return (n, e')

  ----------------------------------------------------------------------
  -- Program location operations

  getCurrentProgramLoc = curProgramLoc
  setCurrentProgramLoc sym l = writeIORef (sbProgramLoc sym) l

  ----------------------------------------------------------------------
  -- Bool operations.

  truePred  = sbTrue
  falsePred = sbFalse

  notPred sym x
    | Just b <- asConstantPred x
    = return (backendPred sym $! not b)

    | Just (NotPred x') <- asApp x
    = return x'

    | otherwise
    = sbMakeExpr sym (NotPred x)

  eqPred sym x y
    | x == y
    = return (truePred sym)

    | Just (NotPred x') <- asApp x
    = xorPred sym x' y

    | Just (NotPred y') <- asApp y
    = xorPred sym x y'

    | otherwise
    = case (asConstantPred x, asConstantPred y) of
        (Just False, _)    -> notPred sym y
        (Just True, _)     -> return y
        (_, Just False)    -> notPred sym x
        (_, Just True)     -> return x
        _ -> sbMakeExpr sym $ BaseEq BaseBoolRepr (min x y) (max x y)

  xorPred sym x y = notPred sym =<< eqPred sym x y

  andPred sym x y =
    case (asConstantPred x, asConstantPred y) of
      (Just True, _)  -> return y
      (Just False, _) -> return x
      (_, Just True)  -> return x
      (_, Just False) -> return y
      _ | x == y -> return x -- and is idempotent
        | otherwise -> go x y

   where
   go a b
     | Just (ConjPred as) <- asApp a
     , Just (ConjPred bs) <- asApp b
     = conjPred sym $ BM.combine as bs

     | tryAndAbsorption a b
     = return b

     | tryAndAbsorption b a
     = return a

     | Just (ConjPred as) <- asApp a
     = conjPred sym $ uncurry BM.addVar (asPosAtom b) as

     | Just (ConjPred bs) <- asApp b
     = conjPred sym $ uncurry BM.addVar (asPosAtom a) bs

     | otherwise
     = conjPred sym $ BM.fromVars [asPosAtom a, asPosAtom b]

  orPred sym x y =
    case (asConstantPred x, asConstantPred y) of
      (Just True, _)  -> return x
      (Just False, _) -> return y
      (_, Just True)  -> return y
      (_, Just False) -> return x
      _ | x == y -> return x -- or is idempotent
        | otherwise -> go x y

   where
   go a b
     | Just (NotPred (asApp -> Just (ConjPred as))) <- asApp a
     , Just (NotPred (asApp -> Just (ConjPred bs))) <- asApp b
     = notPred sym =<< conjPred sym (BM.combine as bs)

     | tryOrAbsorption a b
     = return b

     | tryOrAbsorption b a
     = return a

     | Just (NotPred (asApp -> Just (ConjPred as))) <- asApp a
     = notPred sym =<< conjPred sym (uncurry BM.addVar (asNegAtom b) as)

     | Just (NotPred (asApp -> Just (ConjPred bs))) <- asApp b
     = notPred sym =<< conjPred sym (uncurry BM.addVar (asNegAtom a) bs)

     | otherwise
     = notPred sym =<< conjPred sym (BM.fromVars [asNegAtom a, asNegAtom b])

  itePred sb c x y
      -- ite c c y = c || y
    | c == x = orPred sb c y

      -- ite c x c = c && x
    | c == y = andPred sb c x

      -- ite c x x = x
    | x == y = return x

      -- ite 1 x y = x
    | Just True  <- asConstantPred c = return x

      -- ite 0 x y = y
    | Just False <- asConstantPred c = return y

      -- ite !c x y = ite c y x
    | Just (NotPred c') <- asApp c = itePred sb c' y x

      -- ite c 1 y = c || y
    | Just True  <- asConstantPred x = orPred sb c y

      -- ite c 0 y = !c && y
    | Just False <- asConstantPred x = andPred sb y =<< notPred sb c

      -- ite c x 1 = !c || x
    | Just True  <- asConstantPred y = orPred sb x =<< notPred sb c

      -- ite c x 0 = c && x
    | Just False <- asConstantPred y = andPred sb c x

      -- Default case
    | otherwise =
        let sz = 1 + iteSize x + iteSize y in
        sbMakeExpr sb $ BaseIte BaseBoolRepr sz c x y

  ----------------------------------------------------------------------
  -- Nat operations.

  natLit sym n = semiRingLit sym SR.SemiRingNatRepr n

  natAdd sym x y = semiRingAdd sym SR.SemiRingNatRepr x y

  natSub sym x y = do
    xr <- natToInteger sym x
    yr <- natToInteger sym y
    integerToNat sym =<< intSub sym xr yr

  natMul sym x y = semiRingMul sym SR.SemiRingNatRepr x y

  natDiv sym x y
    | Just m <- asNat x, Just n <- asNat y, n /= 0 = do
      natLit sym (m `div` n)
      -- 0 / y
    | Just 0 <- asNat x = do
      return x
      -- x / 1
    | Just 1 <- asNat y = do
      return