{-# Language FlexibleContexts #-}
{-# Language TypeFamilies #-}
module Cryptol.Backend
  ( Backend(..)
  , sDelay
  , invalidIndex
  , cryUserError
  , cryNoPrimError
  , FPArith2

    -- * Rationals
  , SRational(..)
  , intToRational
  , ratio
  , rationalAdd
  , rationalSub
  , rationalNegate
  , rationalMul
  , rationalRecip
  , rationalDivide
  , rationalFloor
  , rationalCeiling
  , rationalTrunc
  , rationalRoundAway
  , rationalRoundToEven
  , rationalEq
  , rationalLessThan
  , rationalGreaterThan
  , iteRational
  ) where

import Control.Monad.IO.Class
import Data.Kind (Type)

import Cryptol.Backend.FloatHelpers (BF)
import Cryptol.Backend.Monad
  ( EvalError(..), CallStack, pushCallFrame )
import Cryptol.ModuleSystem.Name(Name)
import Cryptol.Parser.Position

invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
invalidIndex :: sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
i = sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (Maybe Integer -> EvalError
InvalidIndex (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i))

cryUserError :: Backend sym => sym -> String -> SEval sym a
cryUserError :: sym -> String -> SEval sym a
cryUserError sym
sym String
msg = sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (String -> EvalError
UserError String
msg)

cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a
cryNoPrimError :: sym -> Name -> SEval sym a
cryNoPrimError sym
sym Name
nm = sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (Name -> EvalError
NoPrim Name
nm)

{-# INLINE sDelay #-}
-- | Delay the given evaluation computation, returning a thunk
--   which will run the computation when forced.  Raise a loop
--   error if the resulting thunk is forced during its own evaluation.
sDelay :: Backend sym => sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay :: sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym SEval sym a
m = sym
-> SEval sym a
-> Maybe (SEval sym a)
-> String
-> SEval sym (SEval sym a)
forall sym a.
Backend sym =>
sym
-> SEval sym a
-> Maybe (SEval sym a)
-> String
-> SEval sym (SEval sym a)
sDelayFill sym
sym SEval sym a
m Maybe (SEval sym a)
forall a. Maybe a
Nothing String
""

-- | Representation of rational numbers.
--     Invariant: denominator is not 0
data SRational sym =
  SRational
  { SRational sym -> SInteger sym
sNum :: SInteger sym
  , SRational sym -> SInteger sym
sDenom :: SInteger sym
  }

intToRational :: Backend sym => sym -> SInteger sym -> SEval sym (SRational sym)
intToRational :: sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym SInteger sym
x = SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
x (SInteger sym -> SRational sym)
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1)

ratio :: Backend sym => sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio :: sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio sym
sym SInteger sym
n SInteger sym
d =
  do SBit sym
pz  <- sym -> SBit sym -> SEval sym (SBit sym)
forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym (SBit sym -> SEval sym (SBit sym))
-> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
d (SInteger sym -> SEval sym (SBit sym))
-> SEval sym (SInteger sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
     sym -> SBit sym -> EvalError -> SEval sym ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
pz EvalError
DivideByZero
     SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
n SInteger sym
d)

rationalRecip :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
rationalRecip :: sym -> SRational sym -> SEval sym (SRational sym)
rationalRecip sym
sym (SRational SInteger sym
a SInteger sym
b) = sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio sym
sym SInteger sym
b SInteger sym
a

rationalDivide :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalDivide :: sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalDivide sym
sym SRational sym
x SRational sym
y = sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalMul sym
sym SRational sym
x (SRational sym -> SEval sym (SRational sym))
-> SEval sym (SRational sym) -> SEval sym (SRational sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalRecip sym
sym SRational sym
y

rationalFloor :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
 -- NB, relies on integer division being round-to-negative-inf division
rationalFloor :: sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym (SRational SInteger sym
n SInteger sym
d) = sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intDiv sym
sym SInteger sym
n SInteger sym
d

rationalCeiling :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling :: sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling sym
sym SRational sym
r = sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym (SInteger sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym (SRational sym -> SEval sym (SInteger sym))
-> SEval sym (SRational sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalNegate sym
sym SRational sym
r

rationalTrunc :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
rationalTrunc :: sym -> SRational sym -> SEval sym (SInteger sym)
rationalTrunc sym
sym SRational sym
r =
  do SBit sym
p <- sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym SRational sym
r (SRational sym -> SEval sym (SBit sym))
-> SEval sym (SRational sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SInteger sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym (SInteger sym -> SEval sym (SRational sym))
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
     SInteger sym
cr <- sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling sym
sym SRational sym
r
     SInteger sym
fr <- sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym SRational sym
r
     sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
cr SInteger sym
fr

rationalRoundAway :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundAway :: sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundAway sym
sym SRational sym
r =
  do SBit sym
p <- sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym SRational sym
r (SRational sym -> SEval sym (SBit sym))
-> SEval sym (SRational sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SInteger sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym (SInteger sym -> SEval sym (SRational sym))
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
     SRational sym
half <- SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational (SInteger sym -> SInteger sym -> SRational sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym -> SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1 SEval sym (SInteger sym -> SRational sym)
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
2
     SInteger sym
cr <- sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling sym
sym (SRational sym -> SEval sym (SInteger sym))
-> SEval sym (SRational sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalSub sym
sym SRational sym
r SRational sym
half
     SInteger sym
fr <- sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym (SRational sym -> SEval sym (SInteger sym))
-> SEval sym (SRational sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalAdd sym
sym SRational sym
r SRational sym
half
     sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
cr SInteger sym
fr

rationalRoundToEven :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundToEven :: sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundToEven sym
sym SRational sym
r =
  do SInteger sym
lo <- sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym SRational sym
r
     SInteger sym
hi <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intPlus sym
sym SInteger sym
lo (SInteger sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1
     -- NB: `diff` will be nonnegative because `lo <= r`
     SRational sym
diff <- sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalSub sym
sym SRational sym
r (SRational sym -> SEval sym (SRational sym))
-> SEval sym (SRational sym) -> SEval sym (SRational sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SInteger sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym SInteger sym
lo
     SRational sym
half <- SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational (SInteger sym -> SInteger sym -> SRational sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym -> SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1 SEval sym (SInteger sym -> SRational sym)
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
2

     SEval sym (SBit sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
ite (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym SRational sym
diff SRational sym
half) (SInteger sym -> SEval sym (SInteger sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
lo) (SEval sym (SInteger sym) -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
forall a b. (a -> b) -> a -> b
$
       SEval sym (SBit sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
ite (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalGreaterThan sym
sym SRational sym
diff SRational sym
half) (SInteger sym -> SEval sym (SInteger sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
hi) (SEval sym (SInteger sym) -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
forall a b. (a -> b) -> a -> b
$
         SEval sym (SBit sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
ite (SInteger sym -> SEval sym (SBit sym)
isEven SInteger sym
lo) (SInteger sym -> SEval sym (SInteger sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
lo) (SInteger sym -> SEval sym (SInteger sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
hi)

 where
 isEven :: SInteger sym -> SEval sym (SBit sym)
isEven SInteger sym
x =
   do SInteger sym
parity <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMod sym
sym SInteger sym
x (SInteger sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
2
      sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
parity (SInteger sym -> SEval sym (SBit sym))
-> SEval sym (SInteger sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0

 ite :: SEval sym (SBit sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym)
ite SEval sym (SBit sym)
x SEval sym (SInteger sym)
t SEval sym (SInteger sym)
e =
   do SBit sym
x' <- SEval sym (SBit sym)
x
      case sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
x' of
        Just Bool
True -> SEval sym (SInteger sym)
t
        Just Bool
False -> SEval sym (SInteger sym)
e
        Maybe Bool
Nothing ->
          do SInteger sym
t' <- SEval sym (SInteger sym)
t
             SInteger sym
e' <- SEval sym (SInteger sym)
e
             sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
x' SInteger sym
t' SInteger sym
e'


rationalAdd :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalAdd :: sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalAdd sym
sym (SRational SInteger sym
a SInteger sym
b) (SRational SInteger sym
c SInteger sym
d) =
  do SInteger sym
ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
a SInteger sym
d
     SInteger sym
bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
c
     SInteger sym
bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
d
     SInteger sym
ad_bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intPlus sym
sym SInteger sym
ad SInteger sym
bc
     SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
ad_bc SInteger sym
bd)

rationalSub :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalSub :: sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalSub sym
sym (SRational SInteger sym
a SInteger sym
b) (SRational SInteger sym
c SInteger sym
d) =
  do SInteger sym
ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
a SInteger sym
d
     SInteger sym
bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
c
     SInteger sym
bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
d
     SInteger sym
ad_bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMinus sym
sym SInteger sym
ad SInteger sym
bc
     SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
ad_bc SInteger sym
bd)

rationalNegate :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
rationalNegate :: sym -> SRational sym -> SEval sym (SRational sym)
rationalNegate sym
sym (SRational SInteger sym
a SInteger sym
b) =
  do SInteger sym
aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
a
     SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
aneg SInteger sym
b)

rationalMul :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalMul :: sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalMul sym
sym (SRational SInteger sym
a SInteger sym
b) (SRational SInteger sym
c SInteger sym
d) =
  do SInteger sym
ac <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
a SInteger sym
c
     SInteger sym
bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
d
     SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
ac SInteger sym
bd)

rationalEq :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq :: sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym (SRational SInteger sym
a SInteger sym
b) (SRational SInteger sym
c SInteger sym
d) =
  do SInteger sym
ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
a SInteger sym
d
     SInteger sym
bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
c
     sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
ad SInteger sym
bc

normalizeSign :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
normalizeSign :: sym -> SRational sym -> SEval sym (SRational sym)
normalizeSign sym
sym (SRational SInteger sym
a SInteger sym
b) =
  do SBit sym
p <- sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
b (SInteger sym -> SEval sym (SBit sym))
-> SEval sym (SInteger sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
     case sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
p of
       Just Bool
False -> SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
a SInteger sym
b)
       Just Bool
True  ->
         do SInteger sym
aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
a
            SInteger sym
bneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
b
            SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
aneg SInteger sym
bneg)
       Maybe Bool
Nothing ->
         do SInteger sym
aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
a
            SInteger sym
bneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
b
            SInteger sym
a' <- sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
aneg SInteger sym
a
            SInteger sym
b' <- sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
bneg SInteger sym
b
            SRational sym -> SEval sym (SRational sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
a' SInteger sym
b')

rationalLessThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan :: sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym SRational sym
x SRational sym
y =
  do SRational SInteger sym
a SInteger sym
b <- sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
normalizeSign sym
sym SRational sym
x
     SRational SInteger sym
c SInteger sym
d <- sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
normalizeSign sym
sym SRational sym
y
     SInteger sym
ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
a SInteger sym
d
     SInteger sym
bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
b SInteger sym
c
     sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
ad SInteger sym
bc

rationalGreaterThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalGreaterThan :: sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalGreaterThan sym
sym = (SRational sym -> SRational sym -> SEval sym (SBit sym))
-> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym)

iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
iteRational :: sym
-> SBit sym
-> SRational sym
-> SRational sym
-> SEval sym (SRational sym)
iteRational sym
sym SBit sym
p (SRational SInteger sym
a SInteger sym
b) (SRational SInteger sym
c SInteger sym
d) =
  SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational (SInteger sym -> SInteger sym -> SRational sym)
-> SEval sym (SInteger sym)
-> SEval sym (SInteger sym -> SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
a SInteger sym
c SEval sym (SInteger sym -> SRational sym)
-> SEval sym (SInteger sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
b SInteger sym
d

-- | This type class defines a collection of operations on bits, words and integers that
--   are necessary to define generic evaluator primitives that operate on both concrete
--   and symbolic values uniformly.
class MonadIO (SEval sym) => Backend sym where
  type SBit sym :: Type
  type SWord sym :: Type
  type SInteger sym :: Type
  type SFloat sym :: Type
  type SEval sym :: Type -> Type

  -- ==== Evaluation monad operations ====

  -- | Check if an operation is "ready", which means its
  --   evaluation will be trivial.
  isReady :: sym -> SEval sym a -> Bool

  -- | Produce a thunk value which can be filled with its associated computation
  --   after the fact.  A preallocated thunk is returned, along with an operation to
  --   fill the thunk with the associated computation.
  --   This is used to implement recursive declaration groups.
  sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())

  -- | Delay the given evaluation computation, returning a thunk
  --   which will run the computation when forced.  Run the 'retry'
  --   computation instead if the resulting thunk is forced during
  --   its own evaluation.
  sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)

  -- | Begin evaluating the given computation eagerly in a separate thread
  --   and return a thunk which will await the completion of the given computation
  --   when forced.
  sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)

  -- | Push a call frame on to the current call stack while evaluating the given action
  sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a
  sPushFrame sym
sym Name
nm Range
rng SEval sym a
m = sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (Name -> Range -> CallStack -> CallStack
pushCallFrame Name
nm Range
rng) SEval sym a
m

  -- | Use the given call stack while evaluating the given action
  sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a
  sWithCallStack sym
sym CallStack
stk SEval sym a
m = sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
_ -> CallStack
stk) SEval sym a
m

  -- | Apply the given function to the current call stack while evaluating the given action
  sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a

  -- | Retrieve the current evaluation call stack
  sGetCallStack :: sym -> SEval sym CallStack

  -- | Merge the two given computations according to the predicate.
  mergeEval ::
     sym ->
     (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} ->
     SBit sym {- ^ The condition -} ->
     SEval sym a {- ^ The "then" computation -} ->
     SEval sym a {- ^ The "else" computation -} ->
     SEval sym a

  -- | Assert that a condition must hold, and indicate what sort of
  --   error is indicated if the condition fails.
  assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym ()

  -- | Indiciate that an error condition exists
  raiseError :: sym -> EvalError -> SEval sym a

  -- ==== Identifying literal values ====

  -- | Determine if this symbolic bit is a boolean literal
  bitAsLit :: sym -> SBit sym -> Maybe Bool

  -- | The number of bits in a word value.
  wordLen :: sym -> SWord sym -> Integer

  -- | Determine if this symbolic word is a literal.
  --   If so, return the bit width and value.
  wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer)

  -- | Attempt to render a word value as an ASCII character.  Return 'Nothing'
  --   if the character value is unknown (e.g., for symbolic values).
  wordAsChar :: sym -> SWord sym -> Maybe Char

  -- | Determine if this symbolic integer is a literal
  integerAsLit :: sym -> SInteger sym -> Maybe Integer

  -- | Determine if this symbolic floating-point value is a literal
  fpAsLit :: sym -> SFloat sym -> Maybe BF

  -- ==== Creating literal values ====

  -- | Construct a literal bit value from a boolean.
  bitLit :: sym -> Bool -> SBit sym

  -- | Construct a literal word value given a bit width and a value.
  wordLit ::
    sym ->
    Integer {- ^ Width -} ->
    Integer {- ^ Value -} ->
    SEval sym (SWord sym)

  -- | Construct a literal integer value from the given integer.
  integerLit ::
    sym ->
    Integer {- ^ Value -} ->
    SEval sym (SInteger sym)

  -- | Construct a floating point value from the given rational.
  fpLit ::
    sym ->
    Integer  {- ^ exponent bits -} ->
    Integer  {- ^ precision bits -} ->
    Rational {- ^ The rational -} ->
    SEval sym (SFloat sym)

  -- | Construct a floating point value from the given bit-precise
  --   floating-point representation.
  fpExactLit :: sym -> BF -> SEval sym (SFloat sym)

  -- ==== If/then/else operations ====
  iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)

  -- ==== Bit operations ====
  bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  bitOr  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  bitComplement :: sym -> SBit sym -> SEval sym (SBit sym)

  -- ==== Word operations ====

  -- | Extract the numbered bit from the word.
  --
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   bit numbered 0 is the most significant bit.
  wordBit ::
    sym ->
    SWord sym ->
    Integer {- ^ Bit position to extract -} ->
    SEval sym (SBit sym)

  -- | Update the numbered bit in the word.
  --
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   bit numbered 0 is the most significant bit.
  wordUpdate ::
    sym ->
    SWord sym ->
    Integer {- ^ Bit position to update -} ->
    SBit sym ->
    SEval sym (SWord sym)

  -- | Construct a word value from a finite sequence of bits.
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   first element of the list will be the most significant bit.
  packWord ::
    sym ->
    [SBit sym] ->
    SEval sym (SWord sym)

  -- | Deconstruct a packed word value in to a finite sequence of bits.
  --   NOTE: this produces a list of bits that represent a big-endian word, so
  --   the most significant bit is the first element of the list.
  unpackWord ::
    sym ->
    SWord sym ->
    SEval sym [SBit sym]

  -- | Construct a packed word of the specified width from an integer value.
  wordFromInt ::
    sym ->
    Integer {- ^ bit-width -} ->
    SInteger sym ->
    SEval sym (SWord sym)

  -- | Concatenate the two given word values.
  --   NOTE: the first argument represents the more-significant bits
  joinWord ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Take the most-significant bits, and return
  --   those bits and the remainder.  The first element
  --   of the pair is the most significant bits.
  --   The two integer sizes must sum to the length of the given word value.
  splitWord ::
    sym ->
    Integer {- ^ left width -} ->
    Integer {- ^ right width -} ->
    SWord sym ->
    SEval sym (SWord sym, SWord sym)

  -- | Extract a subsequence of bits from a packed word value.
  --   The first integer argument is the number of bits in the
  --   resulting word.  The second integer argument is the
  --   number of less-significant digits to discard.  Stated another
  --   way, the operation @extractWord n i w@ is equivalent to
  --   first shifting @w@ right by @i@ bits, and then truncating to
  --   @n@ bits.
  extractWord ::
    sym ->
    Integer {- ^ Number of bits to take -} ->
    Integer {- ^ starting bit -} ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Bitwise OR
  wordOr ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Bitwise AND
  wordAnd ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Bitwise XOR
  wordXor ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Bitwise complement
  wordComplement ::
    sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement addition of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. Overflow is silently
  --   discarded.
  wordPlus ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement subtraction of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. Overflow is silently
  --   discarded.
  wordMinus ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement multiplication of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. The high bits of the
  --   multiplication are silently discarded.
  wordMult ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement unsigned division of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width.  It is illegal to
  --   call with a second argument concretely equal to 0.
  wordDiv ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement unsigned modulus of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width.  It is illegal to
  --   call with a second argument concretely equal to 0.
  wordMod ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement signed division of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width.  It is illegal to
  --   call with a second argument concretely equal to 0.
  wordSignedDiv ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement signed modulus of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width.  It is illegal to
  --   call with a second argument concretely equal to 0.
  wordSignedMod ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | 2's complement negation of bitvectors
  wordNegate ::
    sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Compute rounded-up log-2 of the input
  wordLg2 ::
    sym ->
    SWord sym ->
    SEval sym (SWord sym)

  -- | Test if two words are equal.  Arguments must have the same width.
  wordEq ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SBit sym)

  -- | Signed less-than comparison on words.  Arguments must have the same width.
  wordSignedLessThan ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SBit sym)

  -- | Unsigned less-than comparison on words.  Arguments must have the same width.
  wordLessThan ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SBit sym)

  -- | Unsigned greater-than comparison on words.  Arguments must have the same width.
  wordGreaterThan ::
    sym ->
    SWord sym ->
    SWord sym ->
    SEval sym (SBit sym)

  -- | Construct an integer value from the given packed word.
  wordToInt ::
    sym ->
    SWord sym ->
    SEval sym (SInteger sym)

  -- ==== Integer operations ====

  -- | Addition of unbounded integers.
  intPlus ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Negation of unbounded integers
  intNegate ::
    sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Subtraction of unbounded integers.
  intMinus ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Multiplication of unbounded integers.
  intMult ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Integer division, rounding down. It is illegal to
  --   call with a second argument concretely equal to 0.
  --   Same semantics as Haskell's @div@ operation.
  intDiv ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Integer modulus, with division rounding down. It is illegal to
  --   call with a second argument concretely equal to 0.
  --   Same semantics as Haskell's @mod@ operation.
  intMod ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Equality comparison on integers
  intEq ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SBit sym)

  -- | Less-than comparison on integers
  intLessThan ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SBit sym)

  -- | Greater-than comparison on integers
  intGreaterThan ::
    sym ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SBit sym)


  -- ==== Operations on Z_n ====

  -- | Turn an integer into a value in Z_n
  intToZn ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Transform a Z_n value into an integer, ensuring the value is properly
  --   reduced modulo n
  znToInt ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Addition of integers modulo n, for a concrete positive integer n.
  znPlus ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Additive inverse of integers modulo n
  znNegate ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Subtraction of integers modulo n, for a concrete positive integer n.
  znMinus ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Multiplication of integers modulo n, for a concrete positive integer n.
  znMult ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- | Equality test of integers modulo n
  znEq ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SInteger sym ->
    SEval sym (SBit sym)

  -- | Multiplicative inverse in (Z n).
  --   PRECONDITION: the modulus is a prime
  znRecip ::
    sym ->
    Integer {- ^ modulus -} ->
    SInteger sym ->
    SEval sym (SInteger sym)

  -- == Float Operations ==
  fpEq          :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  fpLessThan    :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)

  fpLogicalEq   :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)

  fpNaN    :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)
  fpPosInf :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)

  fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
  fpNeg, fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym)
  fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym)

  fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)

  fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym)

  fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym)
  fpFromBits ::
    sym ->
    Integer {- ^ exponent bits -} ->
    Integer {- ^ precision bits -} ->
    SWord sym ->
    SEval sym (SFloat sym)

  fpToInteger ::
    sym ->
    String {- ^ Name of the function for error reporting -} ->
    SWord sym {- ^ Rounding mode -} ->
    SFloat sym ->
    SEval sym (SInteger sym)

  fpFromInteger ::
    sym ->
    Integer         {- ^ exp width -} ->
    Integer         {- ^ prec width -} ->
    SWord sym       {- ^ rounding mode -} ->
    SInteger sym    {- ^ the integer to use -} ->
    SEval sym (SFloat sym)

  fpToRational ::
    sym ->
    SFloat sym ->
    SEval sym (SRational sym)

  fpFromRational ::
    sym ->
    Integer         {- ^ exp width -} ->
    Integer         {- ^ prec width -} ->
    SWord sym       {- ^ rounding mode -} ->
    SRational sym ->
    SEval sym (SFloat sym)

type FPArith2 sym =
  sym ->
  SWord sym ->
  SFloat sym ->
  SFloat sym ->
  SEval sym (SFloat sym)