-- |
-- Module      :  Cryptol.Eval.Generic
-- Copyright   :  (c) 2013-2020 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Cryptol.Eval.Generic where

import qualified Control.Exception as X
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad (join, unless)
import System.Random.TF.Gen (seedTFGen)

import Data.Bits (testBit, (.&.), shiftR)

import Data.Maybe (fromMaybe)
import Data.Ratio ((%))

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,widthInteger)
import Cryptol.Backend
import Cryptol.Backend.Concrete (Concrete(..))
import Cryptol.Backend.Monad ( Eval, evalPanic, EvalError(..), Unsupported(..) )
import Cryptol.Testing.Random( randomValue )

import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.RecordMap



{-# SPECIALIZE mkLit :: Concrete -> TValue -> Integer -> Eval (GenValue Concrete)
  #-}

-- | Make a numeric literal value at the given type.
mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit :: sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty Integer
i =
  case TValue
ty of
    TValue
TVBit                        -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0))
    TValue
TVInteger                    -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue 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
i
    TVIntMod Integer
m
      | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0                   -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"mkLit" [String
"0 modulus not allowed"]
      | Bool
otherwise                -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue 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
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)
    TVFloat Integer
e Integer
p                  -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Integer
i)
    TVSeq Integer
w TValue
TVBit                -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> Integer -> GenValue sym
forall sym.
Backend sym =>
sym -> Integer -> Integer -> GenValue sym
word sym
sym Integer
w Integer
i
    TValue
TVRational                   -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
i)
    TValue
_                            -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Cryptol.Eval.Prim.evalConst"
                                    [ String
"Invalid type for number" ]

{-# SPECIALIZE ecNumberV :: Concrete -> GenValue Concrete
  #-}

-- | Make a numeric constant.
ecNumberV :: Backend sym => sym -> GenValue sym
ecNumberV :: sym -> GenValue sym
ecNumberV sym
sym =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \Nat'
valT ->
  (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
ty ->
  case Nat'
valT of
    Nat Integer
v -> sym -> TValue -> Integer -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty Integer
v
    Nat'
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Cryptol.Eval.Prim.evalConst"
             [String
"Unexpected Inf in constant."
             , Nat' -> String
forall a. Show a => a -> String
show Nat'
valT
             , TValue -> String
forall a. Show a => a -> String
show TValue
ty
             ]



{-# SPECIALIZE intV :: Concrete -> Integer -> TValue -> Eval (GenValue Concrete)
  #-}
intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV :: sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i = sym
-> (Integer -> SEval sym (SWord sym))
-> SEval sym (SInteger sym)
-> (Integer -> SEval sym (SInteger sym))
-> SEval sym (SRational sym)
-> (Integer -> Integer -> SEval sym (SFloat sym))
-> TValue
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (Integer -> SEval sym (SWord sym))
-> SEval sym (SInteger sym)
-> (Integer -> SEval sym (SInteger sym))
-> SEval sym (SRational sym)
-> (Integer -> Integer -> SEval sym (SFloat sym))
-> TValue
-> SEval sym (GenValue sym)
ringNullary sym
sym (\Integer
w -> sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt sym
sym Integer
w SInteger sym
i) (SInteger sym -> SEval sym (SInteger sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
i) (\Integer
m -> sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
intToZn sym
sym Integer
m SInteger sym
i) (sym -> SInteger sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym SInteger sym
i)
            (\Integer
e Integer
p -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SFloat sym)) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> Integer
-> Integer
-> SWord sym
-> SInteger sym
-> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SInteger sym
-> SEval sym (SFloat sym)
fpFromInteger sym
sym Integer
e Integer
p SWord sym
r SInteger sym
i)

{-# SPECIALIZE ratioV :: Concrete -> GenValue Concrete #-}
ratioV :: Backend sym => sym -> GenValue sym
ratioV :: sym -> GenValue sym
ratioV sym
sym =
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
y ->
    do SInteger sym
x' <- GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SInteger sym)
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
       SInteger sym
y' <- GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SInteger sym)
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
       SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
x' SInteger sym
y'

{-# SPECIALIZE ecFractionV :: Concrete -> GenValue Concrete
  #-}
ecFractionV :: Backend sym => sym -> GenValue sym
ecFractionV :: sym -> GenValue sym
ecFractionV sym
sym =
  (Integer -> GenValue sym) -> GenValue sym
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam  \Integer
n ->
  (Integer -> GenValue sym) -> GenValue sym
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam  \Integer
d ->
  (Integer -> GenValue sym) -> GenValue sym
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam  \Integer
_r ->
  (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly \TValue
ty ->
    case TValue
ty of
      TVFloat Integer
e Integer
p -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat    (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p (Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
d)
      TValue
TVRational ->
        do SInteger sym
x <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
n
           SInteger sym
y <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
d
           SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
x SInteger sym
y

      TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ecFractionV"
            [ String
"Unexpected `FLiteral` type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
ty ]



{-# SPECIALIZE fromZV :: Concrete -> GenValue Concrete #-}
fromZV :: Backend sym => sym -> GenValue sym
fromZV :: sym -> GenValue sym
fromZV sym
sym =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \(Nat' -> Integer
finNat' -> Integer
n) ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
v -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znToInt sym
sym Integer
n (SInteger sym -> SEval sym (SInteger sym))
-> (GenValue sym -> SInteger sym)
-> GenValue sym
-> SEval sym (SInteger sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SEval sym (SInteger sym))
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v)

-- Operation Lifting -----------------------------------------------------------


type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)

{-# SPECIALIZE binary :: Binary Concrete -> GenValue Concrete
  #-}
binary :: Backend sym => Binary sym -> GenValue sym
binary :: Binary sym -> GenValue sym
binary Binary sym
f = (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ TValue
ty ->
            (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
a  -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
            (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
b  -> do
               --io $ putStrLn "Entering a binary function"
               SEval sym (SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Binary sym
f TValue
ty (GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
a SEval sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (GenValue sym)
b)

type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym)

{-# SPECIALIZE unary :: Unary Concrete -> GenValue Concrete
  #-}
unary :: Backend sym => Unary sym -> GenValue sym
unary :: Unary sym -> GenValue sym
unary Unary sym
f = (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ TValue
ty ->
           (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
a  -> Unary sym
f TValue
ty (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
a


type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)

{-# SPECIALIZE ringBinary :: Concrete -> BinWord Concrete ->
      (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
      (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
      (SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->
      (SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
      Binary Concrete
  #-}

ringBinary :: forall sym.
  Backend sym =>
  sym ->
  BinWord sym ->
  (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
  (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
  (SRational sym -> SRational sym -> SEval sym (SRational sym)) ->
  (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->
  Binary sym
ringBinary :: sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym BinWord sym
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp = Binary sym
loop
  where
  loop' :: TValue
        -> SEval sym (GenValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (GenValue sym)
  loop' :: TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r = SEval sym (SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Binary sym
loop TValue
ty (GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
l SEval sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (GenValue sym)
r)

  loop :: TValue
       -> GenValue sym
       -> GenValue sym
       -> SEval sym (GenValue sym)
  loop :: Binary sym
loop TValue
ty GenValue sym
l GenValue sym
r = case TValue
ty of
    TValue
TVBit ->
      String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringBinary" [String
"Bit not in class Ring"]

    TValue
TVInteger ->
      SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)

    TVIntMod Integer
n ->
      SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
n (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)

    TVFloat {} ->
      SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
l) (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
r)

    TValue
TVRational ->
      SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRational sym -> SRational sym -> SEval sym (SRational sym)
opq (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
l) (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
r)

    TVArray{} ->
      String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithBinary" [String
"Array not in class Ring"]

    TVSeq Integer
w TValue
a
      -- words and finite sequences
      | TValue -> Bool
isTBit TValue
a -> do
                  SWord sym
lw <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringLeft" GenValue sym
l
                  SWord sym
rw <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringRight" GenValue sym
r
                  GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinWord sym
opw Integer
w SWord sym
lw SWord sym
rw)
      | Bool
otherwise -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
w (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (SEval sym (SeqMap sym)) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
(GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
zipSeqMap (Binary sym
loop TValue
a) (SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym)
-> SEval sym (SeqMap sym -> SEval sym (SeqMap sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                      (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringBinary left" GenValue sym
l) SEval sym (SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym) -> SEval sym (SEval sym (SeqMap sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                      (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringBinary right" GenValue sym
r)))

    TVStream TValue
a ->
      -- streams
      SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (SEval sym (SeqMap sym)) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
(GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
zipSeqMap (Binary sym
loop TValue
a) (SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym)
-> SEval sym (SeqMap sym -> SEval sym (SeqMap sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                             (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringBinary left" GenValue sym
l) SEval sym (SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym) -> SEval sym (SEval sym (SeqMap sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                             (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringBinary right" GenValue sym
r)))

    -- functions
    TVFun TValue
_ TValue
ety ->
      GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
x -> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
ety (GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall sym.
GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
fromVFun GenValue sym
l SEval sym (GenValue sym)
x) (GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall sym.
GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
fromVFun GenValue sym
r SEval sym (GenValue sym)
x)

    -- tuples
    TVTuple [TValue]
tys ->
      do [SEval sym (GenValue sym)]
ls <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)]
-> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing) (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
l)
         [SEval sym (GenValue sym)]
rs <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)]
-> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing) (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
r)
         GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ((TValue
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym))
-> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' [TValue]
tys [SEval sym (GenValue sym)]
ls [SEval sym (GenValue sym)]
rs)

    -- records
    TVRec RecordMap Ident TValue
fs ->
      do RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            (Ident -> TValue -> SEval sym (SEval sym (GenValue sym)))
-> RecordMap Ident TValue
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
              (\Ident
f TValue
fty -> sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
fty (Ident -> GenValue sym -> SEval sym (GenValue sym)
forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
l) (Ident -> GenValue sym -> SEval sym (GenValue sym)
forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
r)))
              RecordMap Ident TValue
fs

    TVAbstract {} ->
      String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringBinary" [String
"Abstract type not in `Ring`"]

type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)


{-# SPECIALIZE ringUnary ::
  Concrete ->
  UnaryWord Concrete ->
  (SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
  (Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
  (SRational Concrete -> SEval Concrete (SRational Concrete)) ->
  (SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
  Unary Concrete
  #-}
ringUnary :: forall sym.
  Backend sym =>
  sym ->
  UnaryWord sym ->
  (SInteger sym -> SEval sym (SInteger sym)) ->
  (Integer -> SInteger sym -> SEval sym (SInteger sym)) ->
  (SRational sym -> SEval sym (SRational sym)) ->
  (SFloat sym -> SEval sym (SFloat sym)) ->
  Unary sym
ringUnary :: sym
-> UnaryWord sym
-> (SInteger sym -> SEval sym (SInteger sym))
-> (Integer -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SEval sym (SFloat sym))
-> Unary sym
ringUnary sym
sym UnaryWord sym
opw SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SEval sym (SFloat sym)
opfp = Unary sym
loop
  where
  loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
  loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
v = Unary sym
loop TValue
ty (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v

  loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)
  loop :: Unary sym
loop TValue
ty GenValue sym
v = case TValue
ty of

    TValue
TVBit ->
      String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringUnary" [String
"Bit not in class Ring"]

    TValue
TVInteger ->
      SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SEval sym (SInteger sym)
opi (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v)

    TVIntMod Integer
n ->
      SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
n (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v)

    TVFloat {} ->
      SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SEval sym (SFloat sym)
opfp (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v)

    TValue
TVRational ->
      SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRational sym -> SEval sym (SRational sym)
opq (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v)

    TVArray{} ->
      String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithUnary" [String
"Array not in class Ring"]

    TVSeq Integer
w TValue
a
      -- words and finite sequences
      | TValue -> Bool
isTBit TValue
a -> do
              SWord sym
wx <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringUnary" GenValue sym
v
              GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnaryWord sym
opw Integer
w SWord sym
wx)
      | Bool
otherwise -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
w (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
(GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
mapSeqMap (Unary sym
loop TValue
a) (SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringUnary" GenValue sym
v)

    TVStream TValue
a ->
      SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
(GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
mapSeqMap (Unary sym
loop TValue
a) (SeqMap sym -> SEval sym (SeqMap sym))
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ringUnary" GenValue sym
v)

    -- functions
    TVFun TValue
_ TValue
ety ->
      GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
y -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
ety (GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall sym.
GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
fromVFun GenValue sym
v SEval sym (GenValue sym)
y)

    -- tuples
    TVTuple [TValue]
tys ->
      do [SEval sym (GenValue sym)]
as <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)]
-> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing) (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v)
         GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ((TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' [TValue]
tys [SEval sym (GenValue sym)]
as)

    -- records
    TVRec RecordMap Ident TValue
fs ->
      RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Ident -> TValue -> SEval sym (SEval sym (GenValue sym)))
-> RecordMap Ident TValue
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
          (\Ident
f TValue
fty -> sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
fty (Ident -> GenValue sym -> SEval sym (GenValue sym)
forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
v)))
          RecordMap Ident TValue
fs

    TVAbstract {} -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringUnary" [String
"Abstract type not in `Ring`"]

{-# SPECIALIZE ringNullary ::
  Concrete ->
  (Integer -> SEval Concrete (SWord Concrete)) ->
  SEval Concrete (SInteger Concrete) ->
  (Integer -> SEval Concrete (SInteger Concrete)) ->
  SEval Concrete (SRational Concrete) ->
  (Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->
  TValue ->
  SEval Concrete (GenValue Concrete)
  #-}

ringNullary :: forall sym.
  Backend sym =>
  sym ->
  (Integer -> SEval sym (SWord sym)) ->
  SEval sym (SInteger sym) ->
  (Integer -> SEval sym (SInteger sym)) ->
  SEval sym (SRational sym) ->
  (Integer -> Integer -> SEval sym (SFloat sym)) ->
  TValue ->
  SEval sym (GenValue sym)
ringNullary :: sym
-> (Integer -> SEval sym (SWord sym))
-> SEval sym (SInteger sym)
-> (Integer -> SEval sym (SInteger sym))
-> SEval sym (SRational sym)
-> (Integer -> Integer -> SEval sym (SFloat sym))
-> TValue
-> SEval sym (GenValue sym)
ringNullary sym
sym Integer -> SEval sym (SWord sym)
opw SEval sym (SInteger sym)
opi Integer -> SEval sym (SInteger sym)
opz SEval sym (SRational sym)
opq Integer -> Integer -> SEval sym (SFloat sym)
opfp = TValue -> SEval sym (GenValue sym)
loop
  where
    loop :: TValue -> SEval sym (GenValue sym)
    loop :: TValue -> SEval sym (GenValue sym)
loop TValue
ty =
      case TValue
ty of
        TValue
TVBit -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringNullary" [String
"Bit not in class Ring"]

        TValue
TVInteger -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SInteger sym)
opi

        TVIntMod Integer
n -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SEval sym (SInteger sym)
opz Integer
n

        TVFloat Integer
e Integer
p -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> SEval sym (SFloat sym)
opfp Integer
e Integer
p

        TValue
TVRational -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SRational sym)
opq

        TVArray{} -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithNullary" [String
"Array not in class Ring"]

        TVSeq Integer
w TValue
a
          -- words and finite sequences
          | TValue -> Bool
isTBit TValue
a -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SEval sym (SWord sym)
opw Integer
w)
          | Bool
otherwise ->
             do SEval sym (GenValue sym)
v <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (TValue -> SEval sym (GenValue sym)
loop TValue
a)
                GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
w (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const SEval sym (GenValue sym)
v

        TVStream TValue
a ->
             do SEval sym (GenValue sym)
v <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (TValue -> SEval sym (GenValue sym)
loop TValue
a)
                GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const SEval sym (GenValue sym)
v

        TVFun TValue
_ TValue
b ->
             do SEval sym (GenValue sym)
v <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (TValue -> SEval sym (GenValue sym)
loop TValue
b)
                GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym)
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const (SEval sym (GenValue sym)
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym)
v

        TVTuple [TValue]
tys ->
             do [SEval sym (GenValue sym)]
xs <- (TValue -> SEval sym (SEval sym (GenValue sym)))
-> [TValue] -> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> (TValue -> SEval sym (GenValue sym))
-> TValue
-> SEval sym (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> SEval sym (GenValue sym)
loop) [TValue]
tys
                GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple [SEval sym (GenValue sym)]
xs

        TVRec RecordMap Ident TValue
fs ->
             do RecordMap Ident (SEval sym (GenValue sym))
xs <- (TValue -> SEval sym (SEval sym (GenValue sym)))
-> RecordMap Ident TValue
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> (TValue -> SEval sym (GenValue sym))
-> TValue
-> SEval sym (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> SEval sym (GenValue sym)
loop) RecordMap Ident TValue
fs
                GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
xs

        TVAbstract {} ->
          String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringNullary" [String
"Abstract type not in `Ring`"]

{-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->
      (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
      Binary Concrete
  #-}

integralBinary :: forall sym.
  Backend sym =>
  sym ->
  BinWord sym ->
  (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
  Binary sym
integralBinary :: sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym BinWord sym
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi TValue
ty GenValue sym
l GenValue sym
r = case TValue
ty of
    TValue
TVInteger ->
      SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)

    -- bitvectors
    TVSeq Integer
w TValue
a
      | TValue -> Bool
isTBit TValue
a ->
          do SWord sym
wl <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"integralBinary left" GenValue sym
l
             SWord sym
wr <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"integralBinary right" GenValue sym
r
             GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinWord sym
opw Integer
w SWord sym
wl SWord sym
wr)

    TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"integralBinary" [TValue -> String
forall a. Show a => a -> String
show TValue
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not int class `Integral`"]


---------------------------------------------------------------------------
-- Ring

{-# SPECIALIZE fromIntegerV :: Concrete -> GenValue Concrete
  #-}
-- | Convert an unbounded integer to a value in Ring
fromIntegerV :: Backend sym => sym -> GenValue sym
fromIntegerV :: sym -> GenValue sym
fromIntegerV sym
sym =
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ TValue
a ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
v ->
  do SInteger sym
i <- GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SInteger sym)
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v
     sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i TValue
a

{-# INLINE addV #-}
addV :: Backend sym => sym -> Binary sym
addV :: sym -> Binary sym
addV sym
sym = sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym BinWord sym
forall p. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
  where
    opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordPlus sym
sym SWord sym
x SWord sym
y
    opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = 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
x SInteger sym
y
    opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znPlus sym
sym Integer
m SInteger sym
x SInteger sym
y
    opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq 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)
rationalAdd sym
sym SRational sym
x SRational sym
y
    opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SFloat sym)) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> FPArith2 sym
forall sym. Backend sym => FPArith2 sym
fpPlus sym
sym SWord sym
r SFloat sym
x SFloat sym
y

{-# INLINE subV #-}
subV :: Backend sym => sym -> Binary sym
subV :: sym -> Binary sym
subV sym
sym = sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym BinWord sym
forall p. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
  where
    opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMinus sym
sym SWord sym
x SWord sym
y
    opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = 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
x SInteger sym
y
    opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMinus sym
sym Integer
m SInteger sym
x SInteger sym
y
    opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq 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)
rationalSub sym
sym SRational sym
x SRational sym
y
    opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SFloat sym)) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> FPArith2 sym
forall sym. Backend sym => FPArith2 sym
fpMinus sym
sym SWord sym
r SFloat sym
x SFloat sym
y

{-# INLINE negateV #-}
negateV :: Backend sym => sym -> Unary sym
negateV :: sym -> Unary sym
negateV sym
sym = sym
-> UnaryWord sym
-> (SInteger sym -> SEval sym (SInteger sym))
-> (Integer -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SEval sym (SFloat sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> UnaryWord sym
-> (SInteger sym -> SEval sym (SInteger sym))
-> (Integer -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SEval sym (SFloat sym))
-> Unary sym
ringUnary sym
sym UnaryWord sym
forall p. p -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SEval sym (SFloat sym)
opfp
  where
    opw :: p -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x = sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordNegate sym
sym SWord sym
x
    opi :: SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x = sym -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
x
    opz :: Integer -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x = sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znNegate sym
sym Integer
m SInteger sym
x
    opq :: SRational sym -> SEval sym (SRational sym)
opq SRational sym
x = sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalNegate sym
sym SRational sym
x
    opfp :: SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x = sym -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym SFloat sym
x

{-# INLINE mulV #-}
mulV :: Backend sym => sym -> Binary sym
mulV :: sym -> Binary sym
mulV sym
sym = sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym BinWord sym
forall p. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
  where
    opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMult sym
sym SWord sym
x SWord sym
y
    opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = 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
x SInteger sym
y
    opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMult sym
sym Integer
m SInteger sym
x SInteger sym
y
    opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq 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
y
    opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SFloat sym)) -> SEval sym (SFloat sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> FPArith2 sym
forall sym. Backend sym => FPArith2 sym
fpMult sym
sym SWord sym
r SFloat sym
x SFloat sym
y

--------------------------------------------------
-- Integral

{-# INLINE divV #-}
divV :: Backend sym => sym -> Binary sym
divV :: sym -> Binary sym
divV sym
sym = sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym BinWord sym
forall p. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi
  where
    opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordDiv sym
sym SWord sym
x SWord sym
y
    opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = 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
x SInteger sym
y

{-# SPECIALIZE expV :: Concrete -> GenValue Concrete #-}
expV :: Backend sym => sym -> GenValue sym
expV :: sym -> GenValue sym
expV sym
sym =
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
aty ->
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
ety ->
   (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
am -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
   (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
em ->
     do GenValue sym
a <- SEval sym (GenValue sym)
am
        GenValue sym
e <- SEval sym (GenValue sym)
em
        case TValue
ety of
          TValue
TVInteger ->
            let ei :: SInteger sym
ei = GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
e in
            case sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
ei of
              Just Integer
n
                | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 ->
                   do SInteger sym
onei <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1
                      sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
onei TValue
aty

                | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ->
                    do [SBit sym]
ebits <- sym -> Integer -> SInteger sym -> SEval sym [SBit sym]
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym [SBit sym]
enumerateIntBits' sym
sym Integer
n SInteger sym
ei
                       sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
ebits

                | Bool
otherwise -> sym -> EvalError -> SEval sym (GenValue sym)
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym EvalError
NegativeExponent

              Maybe Integer
Nothing -> IO (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Unsupported -> IO (GenValue sym)
forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"integer exponentiation"))

          TVSeq Integer
_w TValue
el | TValue -> Bool
isTBit TValue
el ->
            do [SBit sym]
ebits <- sym -> WordValue sym -> SEval sym [SBit sym]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (WordValue sym -> SEval sym [SBit sym])
-> SEval sym (WordValue sym) -> SEval sym [SBit sym]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"(^^)" GenValue sym
e
               sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
ebits

          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"expV" [TValue -> String
forall a. Show a => a -> String
show TValue
ety String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not int class `Integral`"]


{-# SPECIALIZE computeExponent ::
      Concrete -> TValue -> GenValue Concrete -> [SBit Concrete] -> SEval Concrete (GenValue Concrete)
  #-}
computeExponent :: Backend sym =>
  sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent :: sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
bs0 =
  do SInteger sym
onei <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1
     GenValue sym
one <- sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
onei TValue
aty
     GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
one ([SBit sym] -> [SBit sym]
dropLeadingZeros [SBit sym]
bs0)

 where
 dropLeadingZeros :: [SBit sym] -> [SBit sym]
dropLeadingZeros [] = []
 dropLeadingZeros (SBit sym
b:[SBit sym]
bs)
   | Just Bool
False <- sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = [SBit sym] -> [SBit sym]
dropLeadingZeros [SBit sym]
bs
   | Bool
otherwise = (SBit sym
bSBit sym -> [SBit sym] -> [SBit sym]
forall a. a -> [a] -> [a]
:[SBit sym]
bs)

 loop :: GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
acc [] = GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
acc
 loop GenValue sym
acc (SBit sym
b:[SBit sym]
bs) =
   do GenValue sym
sq <- sym -> Binary sym
forall sym. Backend sym => sym -> Binary sym
mulV sym
sym TValue
aty GenValue sym
acc GenValue sym
acc
      GenValue sym
acc' <- sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
b
                (sym -> Binary sym
forall sym. Backend sym => sym -> Binary sym
mulV sym
sym TValue
aty GenValue sym
a GenValue sym
sq)
                (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
sq)
      GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
acc' [SBit sym]
bs

{-# INLINE modV #-}
modV :: Backend sym => sym -> Binary sym
modV :: sym -> Binary sym
modV sym
sym = sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym BinWord sym
forall p. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi
  where
    opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMod sym
sym SWord sym
x SWord sym
y
    opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = 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
y

{-# SPECIALIZE toIntegerV :: Concrete -> GenValue Concrete #-}
-- | Convert a word to a non-negative integer.
toIntegerV :: Backend sym => sym -> GenValue sym
toIntegerV :: sym -> GenValue sym
toIntegerV sym
sym =
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
v ->
    case TValue
a of
      TVSeq Integer
_w TValue
el | TValue -> Bool
isTBit TValue
el ->
        SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SWord sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SInteger sym)
wordToInt sym
sym (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SWord sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"toInteger" (GenValue sym -> SEval sym (SWord sym))
-> SEval sym (GenValue sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v))
      TValue
TVInteger -> SEval sym (GenValue sym)
v
      TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"toInteger" [TValue -> String
forall a. Show a => a -> String
show TValue
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not in class `Integral`"]

-----------------------------------------------------------------------------
-- Field

{-# SPECIALIZE recipV :: Concrete -> GenValue Concrete #-}
recipV :: Backend sym => sym -> GenValue sym
recipV :: sym -> GenValue sym
recipV sym
sym =
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x ->
    case TValue
a of
      TValue
TVRational -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalRecip sym
sym (SRational sym -> SEval sym (SRational sym))
-> (GenValue sym -> SRational sym)
-> GenValue sym
-> SEval sym (SRational sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational (GenValue sym -> SEval sym (SRational sym))
-> SEval sym (GenValue sym) -> SEval sym (SRational sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x)
      TVFloat Integer
e Integer
p ->
        do SFloat sym
one <- sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
1
           SWord sym
r   <- sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym
           SFloat sym
xv  <- GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat (GenValue sym -> SFloat sym)
-> SEval sym (GenValue sym) -> SEval sym (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
           SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FPArith2 sym
forall sym. Backend sym => FPArith2 sym
fpDiv sym
sym SWord sym
r SFloat sym
one SFloat sym
xv
      TVIntMod Integer
m -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znRecip sym
sym Integer
m (SInteger sym -> SEval sym (SInteger sym))
-> (GenValue sym -> SInteger sym)
-> GenValue sym
-> SEval sym (SInteger sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SEval sym (SInteger sym))
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x)
      TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"recip"  [TValue -> String
forall a. Show a => a -> String
show TValue
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"is not a Field"]

{-# SPECIALIZE fieldDivideV :: Concrete -> GenValue Concrete #-}
fieldDivideV :: Backend sym => sym -> GenValue sym
fieldDivideV :: sym -> GenValue sym
fieldDivideV sym
sym =
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
y ->
    case TValue
a of
      TValue
TVRational ->
        do SRational sym
x' <- GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational (GenValue sym -> SRational sym)
-> SEval sym (GenValue sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
           SRational sym
y' <- GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational (GenValue sym -> SRational sym)
-> SEval sym (GenValue sym) -> SEval sym (SRational sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
           SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalDivide sym
sym SRational sym
x' SRational sym
y'
      TVFloat Integer
_e Integer
_p ->
        do SFloat sym
xv <- GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat (GenValue sym -> SFloat sym)
-> SEval sym (GenValue sym) -> SEval sym (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
           SFloat sym
yv <- GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat (GenValue sym -> SFloat sym)
-> SEval sym (GenValue sym) -> SEval sym (SFloat sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
           SWord sym
r  <- sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym
           SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FPArith2 sym
forall sym. Backend sym => FPArith2 sym
fpDiv sym
sym SWord sym
r SFloat sym
xv SFloat sym
yv
      TVIntMod Integer
m ->
        do SInteger sym
x' <- GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SInteger sym)
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
           SInteger sym
y' <- GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger (GenValue sym -> SInteger sym)
-> SEval sym (GenValue sym) -> SEval sym (SInteger sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
           SInteger sym
yinv <- sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znRecip sym
sym Integer
m SInteger sym
y'
           SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMult sym
sym Integer
m SInteger sym
x' SInteger sym
yinv

      TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"recip"  [TValue -> String
forall a. Show a => a -> String
show TValue
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"is not a Field"]

--------------------------------------------------------------
-- Round

{-# SPECIALIZE roundOp ::
  Concrete ->
  String ->
  (SRational Concrete -> SEval Concrete (SInteger Concrete)) ->
  (SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->
  Unary Concrete #-}

roundOp ::
  Backend sym =>
  sym ->
  String ->
  (SRational sym -> SEval sym (SInteger sym)) ->
  (SFloat sym -> SEval sym (SInteger sym)) ->
  Unary sym
roundOp :: sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
_sym String
nm SRational sym -> SEval sym (SInteger sym)
qop SFloat sym -> SEval sym (SInteger sym)
opfp TValue
ty GenValue sym
v =
  case TValue
ty of
    TValue
TVRational  -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SRational sym -> SEval sym (SInteger sym)
qop (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v))
    TVFloat Integer
_ Integer
_ -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SEval sym (SInteger sym)
opfp (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v)
    TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
nm [TValue -> String
forall a. Show a => a -> String
show TValue
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a Field"]

{-# INLINE floorV #-}
floorV :: Backend sym => sym -> Unary sym
floorV :: sym -> Unary sym
floorV sym
sym = sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"floor" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
  where
  opq :: SRational sym -> SEval sym (SInteger sym)
opq = sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym
  opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTN sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"floor" SWord sym
r SFloat sym
x

{-# INLINE ceilingV #-}
ceilingV :: Backend sym => sym -> Unary sym
ceilingV :: sym -> Unary sym
ceilingV sym
sym = sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"ceiling" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
  where
  opq :: SRational sym -> SEval sym (SInteger sym)
opq = sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling sym
sym
  opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTP sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"ceiling" SWord sym
r SFloat sym
x

{-# INLINE truncV #-}
truncV :: Backend sym => sym -> Unary sym
truncV :: sym -> Unary sym
truncV sym
sym = sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"trunc" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
  where
  opq :: SRational sym -> SEval sym (SInteger sym)
opq = sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalTrunc sym
sym
  opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTZ sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"trunc" SWord sym
r SFloat sym
x

{-# INLINE roundAwayV #-}
roundAwayV :: Backend sym => sym -> Unary sym
roundAwayV :: sym -> Unary sym
roundAwayV sym
sym = sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"roundAway" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
  where
  opq :: SRational sym -> SEval sym (SInteger sym)
opq = sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundAway sym
sym
  opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNA sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"roundAway" SWord sym
r SFloat sym
x

{-# INLINE roundToEvenV #-}
roundToEvenV :: Backend sym => sym -> Unary sym
roundToEvenV :: sym -> Unary sym
roundToEvenV sym
sym = sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"roundToEven" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
  where
  opq :: SRational sym -> SEval sym (SInteger sym)
opq = sym -> SRational sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundToEven sym
sym
  opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> sym -> SEval sym (SWord sym)
forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNE sym
sym SEval sym (SWord sym)
-> (SWord sym -> SEval sym (SInteger sym))
-> SEval sym (SInteger sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"roundToEven" SWord sym
r SFloat sym
x

--------------------------------------------------------------
-- Logic

{-# INLINE andV #-}
andV :: Backend sym => sym -> Binary sym
andV :: sym -> Binary sym
andV sym
sym = sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym) (sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym)

{-# INLINE orV #-}
orV :: Backend sym => sym -> Binary sym
orV :: sym -> Binary sym
orV sym
sym = sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym) (sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordOr sym
sym)

{-# INLINE xorV #-}
xorV :: Backend sym => sym -> Binary sym
xorV :: sym -> Binary sym
xorV sym
sym = sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitXor sym
sym) (sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordXor sym
sym)

{-# INLINE complementV #-}
complementV :: Backend sym => sym -> Unary sym
complementV :: sym -> Unary sym
complementV sym
sym = sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> Unary sym
forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> Unary sym
logicUnary sym
sym (sym -> SBit sym -> SEval sym (SBit sym)
forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym) (sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym)

-- Bitvector signed div and modulus

{-# INLINE lg2V #-}
lg2V :: Backend sym => sym -> GenValue sym
lg2V :: sym -> GenValue sym
lg2V sym
sym =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \(Nat' -> Integer
finNat' -> Integer
w) ->
  sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym ((SWord sym -> SEval sym (GenValue sym)) -> GenValue sym)
-> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SWord sym
x -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordLg2 sym
sym SWord sym
x)

{-# SPECIALIZE sdivV :: Concrete -> GenValue Concrete #-}
sdivV :: Backend sym => sym -> GenValue sym
sdivV :: sym -> GenValue sym
sdivV sym
sym =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \(Nat' -> Integer
finNat' -> Integer
w) ->
  sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym ((SWord sym -> SEval sym (GenValue sym)) -> GenValue sym)
-> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SWord sym
x -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym ((SWord sym -> SEval sym (GenValue sym)) -> GenValue sym)
-> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SWord sym
y -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedDiv sym
sym SWord sym
x SWord sym
y)

{-# SPECIALIZE smodV :: Concrete -> GenValue Concrete #-}
smodV :: Backend sym => sym -> GenValue sym
smodV :: sym -> GenValue sym
smodV sym
sym  =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \(Nat' -> Integer
finNat' -> Integer
w) ->
  sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym ((SWord sym -> SEval sym (GenValue sym)) -> GenValue sym)
-> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SWord sym
x -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym ((SWord sym -> SEval sym (GenValue sym)) -> GenValue sym)
-> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SWord sym
y -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$
  Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedMod sym
sym SWord sym
x SWord sym
y)

-- Cmp -------------------------------------------------------------------------

{-# SPECIALIZE cmpValue ::
  Concrete ->
  (SBit Concrete -> SBit Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (SWord Concrete -> SWord Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
  (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
  #-}

cmpValue ::
  Backend sym =>
  sym ->
  (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) ->
  (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) ->
  (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
  (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
  (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
  (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
  (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
cmpValue :: sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym -> SBit sym -> SEval sym a -> SEval sym a
fb SWord sym -> SWord sym -> SEval sym a -> SEval sym a
fw SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fi Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fz SRational sym -> SRational sym -> SEval sym a -> SEval sym a
fq SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a
ff = TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp
  where
    cmp :: TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp TValue
ty GenValue sym
v1 GenValue sym
v2 SEval sym a
k =
      case TValue
ty of
        TValue
TVBit         -> SBit sym -> SBit sym -> SEval sym a -> SEval sym a
fb (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v1) (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v2) SEval sym a
k
        TValue
TVInteger     -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fi (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v1) (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v2) SEval sym a
k
        TVFloat Integer
_ Integer
_   -> SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a
ff (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v1) (GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v2) SEval sym a
k
        TVIntMod Integer
n    -> Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fz Integer
n (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v1) (GenValue sym -> SInteger sym
forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v2) SEval sym a
k
        TValue
TVRational    -> SRational sym -> SRational sym -> SEval sym a -> SEval sym a
fq (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v1) (GenValue sym -> SRational sym
forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v2) SEval sym a
k
        TVArray{}     -> String -> [String] -> SEval sym a
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
                               [ String
"Arrays are not comparable" ]
        TVSeq Integer
n TValue
t
          | TValue -> Bool
isTBit TValue
t  -> do SWord sym
w1 <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"cmpValue" GenValue sym
v1
                            SWord sym
w2 <- sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"cmpValue" GenValue sym
v2
                            SWord sym -> SWord sym -> SEval sym a -> SEval sym a
fw SWord sym
w1 SWord sym
w2 SEval sym a
k
          | Bool
otherwise -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues (TValue -> [TValue]
forall a. a -> [a]
repeat TValue
t)
                           (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (GenValue sym -> SeqMap sym
forall sym. GenValue sym -> SeqMap sym
fromVSeq GenValue sym
v1))
                           (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (GenValue sym -> SeqMap sym
forall sym. GenValue sym -> SeqMap sym
fromVSeq GenValue sym
v2))
                           SEval sym a
k
        TVStream TValue
_    -> String -> [String] -> SEval sym a
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
                                [ String
"Infinite streams are not comparable" ]
        TVFun TValue
_ TValue
_     -> String -> [String] -> SEval sym a
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
                               [ String
"Functions are not comparable" ]
        TVTuple [TValue]
tys   -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues [TValue]
tys (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v1) (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v2) SEval sym a
k
        TVRec RecordMap Ident TValue
fields  -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues
                            (RecordMap Ident TValue -> [TValue]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident TValue
fields)
                            (RecordMap Ident (SEval sym (GenValue sym))
-> [SEval sym (GenValue sym)]
forall a b. RecordMap a b -> [b]
recordElements (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
v1))
                            (RecordMap Ident (SEval sym (GenValue sym))
-> [SEval sym (GenValue sym)]
forall a b. RecordMap a b -> [b]
recordElements (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
v2))
                            SEval sym a
k
        TVAbstract {} -> String -> [String] -> SEval sym a
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"cmpValue"
                          [ String
"Abstract type not in `Cmp`" ]

    cmpValues :: [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues (TValue
t : [TValue]
ts) (SEval sym (GenValue sym)
x1 : [SEval sym (GenValue sym)]
xs1) (SEval sym (GenValue sym)
x2 : [SEval sym (GenValue sym)]
xs2) SEval sym a
k =
      do GenValue sym
x1' <- SEval sym (GenValue sym)
x1
         GenValue sym
x2' <- SEval sym (GenValue sym)
x2
         TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp TValue
t GenValue sym
x1' GenValue sym
x2' ([TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues [TValue]
ts [SEval sym (GenValue sym)]
xs1 [SEval sym (GenValue sym)]
xs2 SEval sym a
k)
    cmpValues [TValue]
_ [SEval sym (GenValue sym)]
_ [SEval sym (GenValue sym)]
_ SEval sym a
k = SEval sym a
k


{-# INLINE bitLessThan #-}
bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan sym
sym SBit sym
x SBit sym
y =
  do SBit sym
xnot <- sym -> SBit sym -> SEval sym (SBit sym)
forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
x
     sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
xnot SBit sym
y

{-# INLINE bitGreaterThan #-}
bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan sym
sym SBit sym
x SBit sym
y = sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan sym
sym SBit sym
y SBit sym
x

{-# INLINE valEq #-}
valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq :: sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = sym
-> (SBit sym
    -> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SWord sym
    -> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SInteger sym
    -> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (Integer
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SBit sym)
    -> SEval sym (SBit sym))
-> (SRational sym
    -> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SFloat sym
    -> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit sym -> SEval sym (SBit sym))
-> SBit sym -> SEval sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)
  where
  fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq  sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
  fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
  fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (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
x SInteger sym
y) SEval sym (SBit sym)
k
  fz :: Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
fz Integer
m SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (sym
-> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
znEq sym
sym Integer
m SInteger sym
x SInteger sym
y) SEval sym (SBit sym)
k
  fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
  ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k

{-# INLINE valLt #-}
valLt :: Backend sym =>
  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valLt :: sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 SBit sym
final = sym
-> (SBit sym
    -> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SWord sym
    -> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SInteger sym
    -> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (Integer
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SBit sym)
    -> SEval sym (SBit sym))
-> (SRational sym
    -> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SFloat sym
    -> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall p p p p a. p -> p -> p -> p -> a
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
final)
  where
  fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan  sym
sym SBit sym
x SBit sym
y) (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq  sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
  fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordLessThan sym
sym SWord sym
x SWord sym
y) (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
  fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (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
x SInteger sym
y) (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
x SInteger sym
y) SEval sym (SBit sym)
k
  fz :: p -> p -> p -> p -> a
fz p
_ p
_ p
_ p
_ = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"valLt" [String
"Z_n is not in `Cmp`"]
  fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (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
x SRational sym
y) (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
  ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpLessThan   sym
sym SFloat sym
x SFloat sym
y) (sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq   sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k

{-# INLINE valGt #-}
valGt :: Backend sym =>
  sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valGt :: sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 SBit sym
final = sym
-> (SBit sym
    -> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SWord sym
    -> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SInteger sym
    -> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (Integer
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SBit sym)
    -> SEval sym (SBit sym))
-> (SRational sym
    -> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SFloat sym
    -> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall p p p p a. p -> p -> p -> p -> a
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
final)
  where
  fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan  sym
sym SBit sym
x SBit sym
y) (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq  sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
  fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordGreaterThan sym
sym SWord sym
x SWord sym
y) (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
  fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intGreaterThan  sym
sym SInteger sym
x SInteger sym
y) (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
x SInteger sym
y) SEval sym (SBit sym)
k
  fz :: p -> p -> p -> p -> a
fz p
_ p
_ p
_ p
_ = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"valGt" [String
"Z_n is not in `Cmp`"]
  fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (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
x SRational sym
y) (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
  ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpGreaterThan   sym
sym SFloat sym
x SFloat sym
y) (sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq   sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k

{-# INLINE eqCombine #-}
eqCombine :: Backend sym =>
  sym ->
  SEval sym (SBit sym) ->
  SEval sym (SBit sym) ->
  SEval sym (SBit sym)
eqCombine :: sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym SEval sym (SBit sym)
eq SEval sym (SBit sym)
k = SEval sym (SEval sym (SBit sym)) -> SEval sym (SBit sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> SEval sym (SBit sym)
-> SEval sym (SBit sym -> SEval sym (SBit sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SBit sym)
eq SEval sym (SBit sym -> SEval sym (SBit sym))
-> SEval sym (SBit sym) -> SEval sym (SEval sym (SBit sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (SBit sym)
k)

{-# INLINE lexCombine #-}
lexCombine :: Backend sym =>
  sym ->
  SEval sym (SBit sym) ->
  SEval sym (SBit sym) ->
  SEval sym (SBit sym) ->
  SEval sym (SBit sym)
lexCombine :: sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym SEval sym (SBit sym)
cmp SEval sym (SBit sym)
eq SEval sym (SBit sym)
k =
  do SBit sym
c <- SEval sym (SBit sym)
cmp
     SBit sym
e <- SEval sym (SBit sym)
eq
     sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym SBit sym
c (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 -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
e (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
=<< SEval sym (SBit sym)
k

{-# INLINE eqV #-}
eqV :: Backend sym => sym -> Binary sym
eqV :: sym -> Binary sym
eqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2

{-# INLINE distinctV #-}
distinctV :: Backend sym => sym -> Binary sym
distinctV :: sym -> Binary sym
distinctV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2)

{-# INLINE lessThanV #-}
lessThanV :: Backend sym => sym -> Binary sym
lessThanV :: sym -> Binary sym
lessThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)

{-# INLINE lessThanEqV #-}
lessThanEqV :: Backend sym => sym -> Binary sym
lessThanEqV :: sym -> Binary sym
lessThanEqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)

{-# INLINE greaterThanV #-}
greaterThanV :: Backend sym => sym -> Binary sym
greaterThanV :: sym -> Binary sym
greaterThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)

{-# INLINE greaterThanEqV #-}
greaterThanEqV :: Backend sym => sym -> Binary sym
greaterThanEqV :: sym -> Binary sym
greaterThanEqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)

{-# INLINE signedLessThanV #-}
signedLessThanV :: Backend sym => sym -> Binary sym
signedLessThanV :: sym -> Binary sym
signedLessThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (SBit sym
    -> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SWord sym
    -> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SInteger sym
    -> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (Integer
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SBit sym)
    -> SEval sym (SBit sym))
-> (SRational sym
    -> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> (SFloat sym
    -> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym))
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
    -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall p p p a. p -> p -> p -> a
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall p p p a. p -> p -> p -> a
fi Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall a p p p a. Show a => a -> p -> p -> p -> a
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall p p p a. p -> p -> p -> a
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall p p p a. p -> p -> p -> a
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit sym -> SEval sym (SBit sym))
-> SBit sym -> SEval sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)
  where
  fb :: p -> p -> p -> a
fb p
_ p
_ p
_   = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on bit type"]
  fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k   = sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordSignedLessThan sym
sym SWord sym
x SWord sym
y) (sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
  fi :: p -> p -> p -> a
fi p
_ p
_ p
_   = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Integer type"]
  fz :: a -> p -> p -> p -> a
fz a
m p
_ p
_ p
_ = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Z_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" type"]
  fq :: p -> p -> p -> a
fq p
_ p
_ p
_   = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Rational type"]
  ff :: p -> p -> p -> a
ff p
_ p
_ p
_   = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Float"]



{-# SPECIALIZE zeroV ::
  Concrete ->
  TValue ->
  SEval Concrete (GenValue Concrete)
  #-}
zeroV :: forall sym.
  Backend sym =>
  sym ->
  TValue ->
  SEval sym (GenValue sym)
zeroV :: sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ty = case TValue
ty of

  -- bits
  TValue
TVBit ->
    GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False))

  -- integers
  TValue
TVInteger ->
    SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue 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
0

  -- integers mod n
  TVIntMod Integer
_ ->
    SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue 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
0

  TValue
TVRational ->
    SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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)

  TVArray{} -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"zeroV" [String
"Array not in class Zero"]

  -- floating point
  TVFloat Integer
e Integer
p ->
    SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
0

  -- sequences
  TVSeq Integer
w TValue
ety
      | TValue -> Bool
isTBit TValue
ety -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> Integer -> GenValue sym
forall sym.
Backend sym =>
sym -> Integer -> Integer -> GenValue sym
word sym
sym Integer
w Integer
0
      | Bool
otherwise  ->
           do SEval sym (GenValue sym)
z <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ety)
              GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
w ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const SEval sym (GenValue sym)
z)

  TVStream TValue
ety ->
     do SEval sym (GenValue sym)
z <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ety)
        GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ SEval sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const SEval sym (GenValue sym)
z)

  -- functions
  TVFun TValue
_ TValue
bty ->
     do SEval sym (GenValue sym)
z <- sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
bty)
        GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam (SEval sym (GenValue sym)
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a b. a -> b -> a
const SEval sym (GenValue sym)
z)

  -- tuples
  TVTuple [TValue]
tys ->
      do [SEval sym (GenValue sym)]
xs <- (TValue -> SEval sym (SEval sym (GenValue sym)))
-> [TValue] -> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> (TValue -> SEval sym (GenValue sym))
-> TValue
-> SEval sym (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym) [TValue]
tys
         GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple [SEval sym (GenValue sym)]
xs

  -- records
  TVRec RecordMap Ident TValue
fields ->
      do RecordMap Ident (SEval sym (GenValue sym))
xs <- (TValue -> SEval sym (SEval sym (GenValue sym)))
-> RecordMap Ident TValue
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> (TValue -> SEval sym (GenValue sym))
-> TValue
-> SEval sym (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym) RecordMap Ident TValue
fields
         GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
xs

  TVAbstract {} -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"zeroV" [ String
"Abstract type not in `Zero`" ]

--  | otherwise = evalPanic "zeroV" ["invalid type for zero"]

{-# INLINE joinWordVal #-}
joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal :: sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym (WordVal SWord sym
w1) (WordVal SWord sym
w2)
  | sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
largeBitSize
  = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
w1 SWord sym
w2
joinWordVal sym
sym WordValue sym
w1 WordValue sym
w2
  = WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal (Integer
n1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
n2) (Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
forall sym. Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
concatSeqMap Integer
n1 (sym -> WordValue sym -> SeqMap sym
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap sym
sym WordValue sym
w1) (sym -> WordValue sym -> SeqMap sym
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap sym
sym WordValue sym
w2))
 where n1 :: Integer
n1 = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w1
       n2 :: Integer
n2 = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w2


{-# SPECIALIZE joinWords ::
  Concrete ->
  Integer ->
  Integer ->
  SeqMap Concrete ->
  SEval Concrete (GenValue Concrete)
  #-}
joinWords :: forall sym.
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  SeqMap sym ->
  SEval sym (GenValue sym)
joinWords :: sym -> Integer -> Integer -> SeqMap sym -> SEval sym (GenValue sym)
joinWords sym
sym Integer
nParts Integer
nEach SeqMap sym
xs =
  SEval sym (WordValue sym)
-> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
loop (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
0 Integer
0) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
nParts SeqMap sym
xs)

 where
 loop :: SEval sym (WordValue sym) -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
 loop :: SEval sym (WordValue sym)
-> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
loop !SEval sym (WordValue sym)
wv [] =
    Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (Integer
nParts Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
nEach) (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (SEval sym (WordValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Maybe String
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing SEval sym (WordValue sym)
wv
 loop !SEval sym (WordValue sym)
wv (SEval sym (GenValue sym)
w : [SEval sym (GenValue sym)]
ws) =
    SEval sym (GenValue sym)
w SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      VWord Integer
_ SEval sym (WordValue sym)
w' ->
        SEval sym (WordValue sym)
-> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
loop (SEval sym (SEval sym (WordValue sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym (WordValue sym -> WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym -> SEval sym (WordValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym)
wv SEval sym (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (WordValue sym)
w')) [SEval sym (GenValue sym)]
ws
      GenValue sym
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"joinWords: expected word value" []

{-# SPECIALIZE joinSeq ::
  Concrete ->
  Nat' ->
  Integer ->
  TValue ->
  SeqMap Concrete ->
  SEval Concrete (GenValue Concrete)
  #-}
joinSeq ::
  Backend sym =>
  sym ->
  Nat' ->
  Integer ->
  TValue ->
  SeqMap sym ->
  SEval sym (GenValue sym)

-- Special case for 0 length inner sequences.
joinSeq :: sym
-> Nat'
-> Integer
-> TValue
-> SeqMap sym
-> SEval sym (GenValue sym)
joinSeq sym
sym Nat'
_parts Integer
0 TValue
a SeqMap sym
_xs
  = sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym (Integer -> TValue -> TValue
TVSeq Integer
0 TValue
a)

-- finite sequence of words
joinSeq sym
sym (Nat Integer
parts) Integer
each TValue
TVBit SeqMap sym
xs
  | Integer
parts Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
each Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
largeBitSize
  = sym -> Integer -> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SeqMap sym -> SEval sym (GenValue sym)
joinWords sym
sym Integer
parts Integer
each SeqMap sym
xs
  | Bool
otherwise
  = do let zs :: SeqMap sym
zs = (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
                  do let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
                     WordValue sym
ys <- String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"join seq" (GenValue sym -> SEval sym (WordValue sym))
-> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
q
                     SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
ys Integer
r
       GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (Integer
parts Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
each) (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal (Integer
parts Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
each) SeqMap sym
zs

-- infinite sequence of words
joinSeq sym
sym Nat'
Inf Integer
each TValue
TVBit SeqMap sym
xs
  = GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
         WordValue sym
ys <- String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"join seq" (GenValue sym -> SEval sym (WordValue sym))
-> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
q
         SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
ys Integer
r

-- finite or infinite sequence of non-words
joinSeq sym
_sym Nat'
parts Integer
each TValue
_a SeqMap sym
xs
  = GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
vSeq (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
      let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
      SeqMap sym
ys <- String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"join seq" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
q
      SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
ys Integer
r
  where
  len :: Nat'
len = Nat'
parts Nat' -> Nat' -> Nat'
`nMul` (Integer -> Nat'
Nat Integer
each)
  vSeq :: SeqMap sym -> GenValue sym
vSeq = case Nat'
len of
           Nat'
Inf    -> SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream
           Nat Integer
n  -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n


{-# INLINE joinV #-}

-- | Join a sequence of sequences into a single sequence.
joinV ::
  Backend sym =>
  sym ->
  Nat' ->
  Integer ->
  TValue ->
  GenValue sym ->
  SEval sym (GenValue sym)
joinV :: sym
-> Nat'
-> Integer
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
joinV sym
sym Nat'
parts Integer
each TValue
a GenValue sym
val = sym
-> Nat'
-> Integer
-> TValue
-> SeqMap sym
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SeqMap sym
-> SEval sym (GenValue sym)
joinSeq sym
sym Nat'
parts Integer
each TValue
a (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"joinV" GenValue sym
val


{-# INLINE splitWordVal #-}

splitWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym, WordValue sym)
splitWordVal :: sym
-> Integer
-> Integer
-> WordValue sym
-> SEval sym (WordValue sym, WordValue sym)
splitWordVal sym
sym Integer
leftWidth Integer
rightWidth (WordVal SWord sym
w) =
  do (SWord sym
lw, SWord sym
rw) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym Integer
leftWidth Integer
rightWidth SWord sym
w
     (WordValue sym, WordValue sym)
-> SEval sym (WordValue sym, WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
lw, SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
rw)
splitWordVal sym
_ Integer
leftWidth Integer
rightWidth (LargeBitsVal Integer
_n SeqMap sym
xs) =
  let (SeqMap sym
lxs, SeqMap sym
rxs) = Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
forall sym. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
leftWidth SeqMap sym
xs
   in (WordValue sym, WordValue sym)
-> SEval sym (WordValue sym, WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
leftWidth SeqMap sym
lxs, Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
rightWidth SeqMap sym
rxs)

{-# INLINE splitAtV #-}
splitAtV ::
  Backend sym =>
  sym ->
  Nat' ->
  Nat' ->
  TValue ->
  GenValue sym ->
  SEval sym (GenValue sym)
splitAtV :: sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
splitAtV sym
sym Nat'
front Nat'
back TValue
a GenValue sym
val =
  case Nat'
back of

    Nat Integer
rightWidth | Bool
aBit -> do
          SEval sym (WordValue sym, WordValue sym)
ws <- sym
-> Maybe String
-> SEval sym (WordValue sym, WordValue sym)
-> SEval sym (SEval sym (WordValue sym, WordValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (sym
-> Integer
-> Integer
-> WordValue sym
-> SEval sym (WordValue sym, WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> WordValue sym
-> SEval sym (WordValue sym, WordValue sym)
splitWordVal sym
sym Integer
leftWidth Integer
rightWidth (WordValue sym -> SEval sym (WordValue sym, WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym, WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"splitAtV" GenValue sym
val)
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple
                   [ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
leftWidth  (SEval sym (WordValue sym) -> GenValue sym)
-> ((WordValue sym, WordValue sym) -> SEval sym (WordValue sym))
-> (WordValue sym, WordValue sym)
-> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> ((WordValue sym, WordValue sym) -> WordValue sym)
-> (WordValue sym, WordValue sym)
-> SEval sym (WordValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WordValue sym, WordValue sym) -> WordValue sym
forall a b. (a, b) -> a
fst ((WordValue sym, WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym, WordValue sym)
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym, WordValue sym)
ws
                   , Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
rightWidth (SEval sym (WordValue sym) -> GenValue sym)
-> ((WordValue sym, WordValue sym) -> SEval sym (WordValue sym))
-> (WordValue sym, WordValue sym)
-> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> ((WordValue sym, WordValue sym) -> WordValue sym)
-> (WordValue sym, WordValue sym)
-> SEval sym (WordValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WordValue sym, WordValue sym) -> WordValue sym
forall a b. (a, b) -> b
snd ((WordValue sym, WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym, WordValue sym)
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym, WordValue sym)
ws
                   ]

    Nat'
Inf | Bool
aBit -> do
       SEval sym (SeqMap sym)
vs <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"splitAtV" GenValue sym
val)
       SEval sym (SeqMap sym)
ls <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing ((SeqMap sym, SeqMap sym) -> SeqMap sym
forall a b. (a, b) -> a
fst ((SeqMap sym, SeqMap sym) -> SeqMap sym)
-> (SeqMap sym -> (SeqMap sym, SeqMap sym))
-> SeqMap sym
-> SeqMap sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
forall sym. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
leftWidth (SeqMap sym -> SeqMap sym)
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
vs)
       SEval sym (SeqMap sym)
rs <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing ((SeqMap sym, SeqMap sym) -> SeqMap sym
forall a b. (a, b) -> b
snd ((SeqMap sym, SeqMap sym) -> SeqMap sym)
-> (SeqMap sym -> (SeqMap sym, SeqMap sym))
-> SeqMap sym
-> SeqMap sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
forall sym. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
leftWidth (SeqMap sym -> SeqMap sym)
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
vs)
       GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple [ GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
leftWidth (Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
leftWidth (SeqMap sym -> WordValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
ls)
                       , SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
rs
                       ]

    Nat'
_ -> do
       SEval sym (SeqMap sym)
vs <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"splitAtV" GenValue sym
val)
       SEval sym (SeqMap sym)
ls <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing ((SeqMap sym, SeqMap sym) -> SeqMap sym
forall a b. (a, b) -> a
fst ((SeqMap sym, SeqMap sym) -> SeqMap sym)
-> (SeqMap sym -> (SeqMap sym, SeqMap sym))
-> SeqMap sym
-> SeqMap sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
forall sym. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
leftWidth (SeqMap sym -> SeqMap sym)
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
vs)
       SEval sym (SeqMap sym)
rs <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing ((SeqMap sym, SeqMap sym) -> SeqMap sym
forall a b. (a, b) -> b
snd ((SeqMap sym, SeqMap sym) -> SeqMap sym)
-> (SeqMap sym -> (SeqMap sym, SeqMap sym))
-> SeqMap sym
-> SeqMap sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
forall sym. Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
leftWidth (SeqMap sym -> SeqMap sym)
-> SEval sym (SeqMap sym) -> SEval sym (SeqMap sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
vs)
       GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple [ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
leftWidth (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
ls
                       , Nat' -> TValue -> SeqMap sym -> GenValue sym
forall sym.
Backend sym =>
Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq Nat'
back TValue
a (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SeqMap sym)
rs
                       ]

  where
  aBit :: Bool
aBit = TValue -> Bool
isTBit TValue
a

  leftWidth :: Integer
leftWidth = case Nat'
front of
    Nat Integer
n -> Integer
n
    Nat'
_     -> String -> [String] -> Integer
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"splitAtV" [String
"invalid `front` len"]


{-# INLINE extractWordVal #-}

-- | Extract a subsequence of bits from a @WordValue@.
--   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 `extractWordVal n i w` is equivalent to
--   first shifting `w` right by `i` bits, and then truncating to
--   `n` bits.
extractWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
extractWordVal :: sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start (WordVal SWord sym
w) =
   SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
extractWord sym
sym Integer
len Integer
start SWord sym
w
extractWordVal sym
_ Integer
len Integer
start (LargeBitsVal Integer
n SeqMap sym
xs) =
   let xs' :: SeqMap sym
xs' = Integer -> SeqMap sym -> SeqMap sym
forall sym. Integer -> SeqMap sym -> SeqMap sym
dropSeqMap (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
start Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
len) SeqMap sym
xs
    in WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
len SeqMap sym
xs'

{-# INLINE ecSplitV #-}

-- | Split implementation.
ecSplitV :: Backend sym => sym -> GenValue sym
ecSplitV :: sym -> GenValue sym
ecSplitV sym
sym =
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ Nat'
parts ->
  (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> GenValue sym) -> GenValue sym)
-> (Nat' -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ Nat'
each  ->
  (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> GenValue sym) -> GenValue sym)
-> (TValue -> GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ TValue
a     ->
  (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \ SEval sym (GenValue sym)
val ->
    case (Nat'
parts, Nat'
each) of
       (Nat Integer
p, Nat Integer
e) | TValue -> Bool
isTBit TValue
a -> do
          ~(VWord Integer
_ SEval sym (WordValue sym)
val') <- SEval sym (GenValue sym)
val
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
p (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
e (sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
e ((Integer
pInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
e) (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
val')
       (Nat'
Inf, Nat Integer
e) | TValue -> Bool
isTBit TValue
a -> do
          SEval sym (SeqMap sym)
val' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ecSplitV" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
e (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
e (SeqMap sym -> WordValue sym) -> SeqMap sym -> WordValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
j ->
              let idx :: Integer
idx = Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
j
               in Integer
idx Integer -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
`seq` do
                      SeqMap sym
xs <- SEval sym (SeqMap sym)
val'
                      SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
idx
       (Nat Integer
p, Nat Integer
e) -> do
          SEval sym (SeqMap sym)
val' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ecSplitV" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
p (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
e (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
j -> do
              SeqMap sym
xs <- SEval sym (SeqMap sym)
val'
              SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs (Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
       (Nat'
Inf  , Nat Integer
e) -> do
          SEval sym (SeqMap sym)
val' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ecSplitV" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
e (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
j -> do
              SeqMap sym
xs <- SEval sym (SeqMap sym)
val'
              SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs (Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
       (Nat', Nat')
_              -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"splitV" [String
"invalid type arguments to split"]

{-# INLINE reverseV #-}

reverseV :: forall sym.
  Backend sym =>
  sym ->
  GenValue sym ->
  SEval sym (GenValue sym)
reverseV :: sym -> GenValue sym -> SEval sym (GenValue sym)
reverseV sym
_ (VSeq Integer
n SeqMap sym
xs) =
  GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> SeqMap sym
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap sym
xs
reverseV sym
sym (VWord Integer
n SEval sym (WordValue sym)
x) = GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
n (WordValue sym -> WordValue sym
revword (WordValue sym -> WordValue sym)
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym)
x))
 where
 revword :: WordValue sym -> WordValue sym
revword WordValue sym
wv =
   let m :: Integer
m = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
wv in
   Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
m (SeqMap sym -> WordValue sym) -> SeqMap sym -> WordValue sym
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> SeqMap sym
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
m (SeqMap sym -> SeqMap sym) -> SeqMap sym -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ sym -> WordValue sym -> SeqMap sym
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap sym
sym WordValue sym
wv
reverseV sym
_ GenValue sym
_ =
  String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"reverseV" [String
"Not a finite sequence"]

{-# INLINE transposeV #-}

transposeV ::
  Backend sym =>
  sym ->
  Nat' ->
  Nat' ->
  TValue ->
  GenValue sym ->
  SEval sym (GenValue sym)
transposeV :: sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
transposeV sym
sym Nat'
a Nat'
b TValue
c GenValue sym
xs
  | TValue -> Bool
isTBit TValue
c, Nat Integer
na <- Nat'
a = -- Fin a => [a][b]Bit -> [b][a]Bit
      GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
bseq (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
        GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
na (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
na (SeqMap sym -> WordValue sym) -> SeqMap sym -> WordValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
ai ->
         do GenValue sym
ys <- (SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
ai) (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"transposeV" GenValue sym
xs
            case GenValue sym
ys of
              VStream SeqMap sym
ys' -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
ys' Integer
bi
              VWord Integer
_ SEval sym (WordValue sym)
wv  -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) Integer
bi (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
wv)
              GenValue sym
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"transpose" [String
"expected sequence of bits"]

  | TValue -> Bool
isTBit TValue
c, Nat'
Inf <- Nat'
a = -- [inf][b]Bit -> [b][inf]Bit
      GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
bseq (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
        GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
ai ->
         do GenValue sym
ys <- (SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap Integer
ai (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"transposeV" GenValue sym
xs
            case GenValue sym
ys of
              VStream SeqMap sym
ys' -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
ys' Integer
bi
              VWord Integer
_ SEval sym (WordValue sym)
wv  -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) Integer
bi (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
wv)
              GenValue sym
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"transpose" [String
"expected sequence of bits"]

  | Bool
otherwise = -- [a][b]c -> [b][a]c
      GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
bseq (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
        GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
aseq (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
ai -> do
          GenValue sym
ys  <- (SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap Integer
ai (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"transposeV 1" GenValue sym
xs
          GenValue sym
z   <- (SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap Integer
bi (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"transposeV 2" GenValue sym
ys
          GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
z

 where
  bseq :: SeqMap sym -> GenValue sym
bseq =
        case Nat'
b of
          Nat Integer
nb -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
nb
          Nat'
Inf    -> SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream
  aseq :: SeqMap sym -> GenValue sym
aseq =
        case Nat'
a of
          Nat Integer
na -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
na
          Nat'
Inf    -> SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream


{-# INLINE ccatV #-}

ccatV ::
  Backend sym =>
  sym ->
  Nat' ->
  Nat' ->
  TValue ->
  (GenValue sym) ->
  (GenValue sym) ->
  SEval sym (GenValue sym)

ccatV :: sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
ccatV sym
sym Nat'
_front Nat'
_back TValue
_elty (VWord Integer
m SEval sym (WordValue sym)
l) (VWord Integer
n SEval sym (WordValue sym)
r) =
  GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
n) (SEval sym (SEval sym (WordValue sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym (WordValue sym -> WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym -> SEval sym (WordValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym)
l SEval sym (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (WordValue sym)
r))

ccatV sym
sym Nat'
_front Nat'
_back TValue
_elty (VWord Integer
m SEval sym (WordValue sym)
l) (VStream SeqMap sym
r) = do
  SEval sym (WordValue sym)
l' <- sym
-> Maybe String
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing SEval sym (WordValue sym)
l
  GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
m then
      SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) Integer
i (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
l')
    else
      SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
r (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m)

ccatV sym
sym Nat'
front Nat'
back TValue
elty GenValue sym
l GenValue sym
r = do
       SEval sym (SeqMap sym)
l'' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ccatV left" GenValue sym
l)
       SEval sym (SeqMap sym)
r'' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"ccatV right" GenValue sym
r)
       let Nat Integer
n = Nat'
front
       Nat' -> TValue -> SeqMap sym -> GenValue sym
forall sym.
Backend sym =>
Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq (TFun -> [Nat'] -> Nat'
evalTF TFun
TCAdd [Nat'
front,Nat'
back]) TValue
elty (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
        if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n then do
         SeqMap sym
ls <- SEval sym (SeqMap sym)
l''
         SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
ls Integer
i
        else do
         SeqMap sym
rs <- SEval sym (SeqMap sym)
r''
         SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
rs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n))

{-# INLINE wordValLogicOp #-}

wordValLogicOp ::
  Backend sym =>
  sym ->
  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->
  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->
  WordValue sym ->
  WordValue sym ->
  SEval sym (WordValue sym)
wordValLogicOp :: sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
wordValLogicOp sym
_sym SBit sym -> SBit sym -> SEval sym (SBit sym)
_ SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (WordVal SWord sym
w1) (WordVal SWord sym
w2) = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w1 SWord sym
w2

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
_ WordValue sym
w1 WordValue sym