{-# 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
  , ppRational
  ) where

import Control.Monad.IO.Class
import Data.Kind (Type)
import Data.Ratio ( (%), numerator, denominator )

import Cryptol.Backend.FloatHelpers (BF)
import Cryptol.Backend.Monad ( PPOpts(..), EvalError(..) )
import Cryptol.TypeCheck.AST(Name)
import Cryptol.Utils.PP


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

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

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


{-# 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 -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay :: sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
msg SEval sym a
m =
  let msg' :: String
msg'  = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String
"while evaluating "String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
msg
      retry :: SEval sym a
retry = sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (String -> EvalError
LoopError String
msg')
   in sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
sDelayFill sym
sym SEval sym a
m SEval sym a
retry


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

ppRational :: Backend sym => sym -> PPOpts -> SRational sym -> Doc
ppRational :: sym -> PPOpts -> SRational sym -> Doc
ppRational sym
sym PPOpts
opts (SRational SInteger sym
n SInteger sym
d)
  | Just Integer
ni <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
n
  , Just Integer
di <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
d
  = let q :: Ratio Integer
q = Integer
ni Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
di in
      String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
numerator Ratio Integer
q) Doc -> Doc -> Doc
<+> (Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
denominator Ratio Integer
q) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")")

  | Bool
otherwise
  = String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> sym -> PPOpts -> SInteger sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SInteger sym -> Doc
ppInteger sym
sym PPOpts
opts SInteger sym
n Doc -> Doc -> Doc
<+> (sym -> PPOpts -> SInteger sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SInteger sym -> Doc
ppInteger sym
sym PPOpts
opts SInteger sym
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")")

-- | 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 -> SEval sym a -> 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)

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


  -- ==== Pretty printing  ====
  -- | Pretty-print an individual bit
  ppBit :: sym -> SBit sym -> Doc

  -- | Pretty-print a word value
  ppWord :: sym -> PPOpts -> SWord sym -> Doc

  -- | Pretty-print an integer value
  ppInteger :: sym -> PPOpts -> SInteger sym -> Doc

  -- | Pretty-print a floating-point value
  ppFloat :: sym -> PPOpts -> SFloat sym -> Doc


  -- ==== 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

  -- ==== 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)

  -- ==== 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)

  -- | Multiplicitive 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)

  fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
  fpNeg :: sym -> SFloat 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 integeer to use -} ->
    SEval sym (SFloat sym)

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