{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | The Hyle interpreter: a direct transcription of the denotational
--   semantics in doc/hyle.md (sections 5 and 6). The device denotes a Mealy
--   stream function: registers start at their initial values, outputs and
--   next-register values are computed from the body's equations each cycle.
--
--   Programs containing instances (sequential externs) or calls to
--   model-less combinational externs cannot be evaluated.
module ReWire.Hyle.Interp (interp, evalExp, evalOp, IEnv (..), Ins, Outs, run, subRange, inputValue, yamlPrefixes) where

import ReWire.Annotation (Annote, Annotated (ann))
import ReWire.BitVector (BV, bitVec, nat, width, ones, zeros, ashr)
import ReWire.Config (Config, verbose)
import ReWire.Error (failAt, failInternal, MonadError, AstError)
import ReWire.Hyle.Syntax
import ReWire.Pretty (showt)

import qualified ReWire.BitVector as BV

import Control.Lens ((^.))
import Control.Monad (foldM, unless, when)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.Bits (Bits (..))
import Data.HashMap.Strict (HashMap)
import Data.Machine.MealyT (MealyT (..), runMealyT)
import Data.Text (Text)

import qualified Data.HashMap.Strict as Map
import qualified Data.Text.IO        as T

-- | Per-cycle input values and output bitvectors, by wire name.
type Ins  = HashMap Name Value
type Outs = HashMap Name BV
type Sts  = HashMap Name BV

-- | Runs non-interactively: given a stream of inputs, produces a stream of
--   outputs.
run :: MonadIO m => Config -> MealyT m Ins Outs -> [Ins] -> m [Outs]
run :: forall (m :: * -> *).
MonadIO m =>
Config -> MealyT m Ins Outs -> [Ins] -> m [Outs]
run Config
conf MealyT m Ins Outs
m = \ case
      []         -> [Outs] -> m [Outs]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      (Ins
ip : [Ins]
ips) -> do
            (b, m') <- MealyT m Ins Outs -> Ins -> m (Outs, MealyT m Ins Outs)
forall (m :: * -> *) a b. MealyT m a b -> a -> m (b, MealyT m a b)
runMealyT MealyT m Ins Outs
m Ins
ip
            when (conf^.verbose) $ liftIO $ do
                  T.putStrLn "Debug: Interpreting hyle: completed cycle."
                  T.putStr $ mconcat $ (\ (Text
k, BV
v) -> Text
"\t" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BV -> Text
BV.showHex BV
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n") <$> Map.toList b
            (b :) <$> run conf m' ips

-- | The value driven onto an input wire for a cycle (interp-style inputs:
--   missing wires are driven to zero; values are truncated to the wire
--   width).
inputValue :: Size -> Ins -> Name -> Value
inputValue :: Size -> Ins -> Text -> Integer
inputValue Size
w Ins
ins Text
n = Integer -> Text -> Ins -> Integer
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.findWithDefault Integer
0 Text
n Ins
ins Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Size -> Integer
forall a. Integral a => a -> Integer
toInteger Size
w)

-- | Per-cycle output records in the interpreter's YAML format: the first
--   output prefixed with "- ", the rest indented, in port order.
yamlPrefixes :: [Text]
yamlPrefixes :: [Text]
yamlPrefixes = Text
"- " Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: Text -> [Text]
forall a. a -> [a]
repeat Text
"  "

-- | The inclusive bit range [i, j] of a bitvector.
subRange :: (Int, Int) -> BV -> BV
subRange :: (Int, Int) -> BV -> BV
subRange (Int
i, Int
j) BV
b | Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
b Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
                  | Bool
otherwise  = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
0 (Integer
0 :: Integer)

data IEnv = IEnv
      { IEnv -> HashMap Text Defn
envDefns   :: HashMap GId Defn
      , IEnv -> HashMap Text Extern
envExterns :: HashMap Name Extern
      }

interp :: MonadError AstError m => Config -> Program -> MealyT m Ins Outs
interp :: forall (m :: * -> *).
MonadError AstError m =>
Config -> Program -> MealyT m Ins Outs
interp Config
_conf (Program [Extern]
exts [Defn]
ds Device
dev) = (Outs -> Ins -> m (Outs, Outs)) -> Outs -> MealyT m Ins Outs
forall (m :: * -> *) s a b.
Applicative m =>
(s -> a -> m (b, s)) -> s -> MealyT m a b
unfoldMealyT Outs -> Ins -> m (Outs, Outs)
forall (m :: * -> *).
MonadError AstError m =>
Outs -> Ins -> m (Outs, Outs)
step Outs
sts0
      where env :: IEnv
            env :: IEnv
env = HashMap Text Defn -> HashMap Text Extern -> IEnv
IEnv ([(Text, Defn)] -> HashMap Text Defn
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(Text, Defn)] -> HashMap Text Defn)
-> [(Text, Defn)] -> HashMap Text Defn
forall a b. (a -> b) -> a -> b
$ (Defn -> (Text, Defn)) -> [Defn] -> [(Text, Defn)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Defn
d -> (Defn -> Text
defnName Defn
d, Defn
d)) [Defn]
ds)
                       ([(Text, Extern)] -> HashMap Text Extern
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(Text, Extern)] -> HashMap Text Extern)
-> [(Text, Extern)] -> HashMap Text Extern
forall a b. (a -> b) -> a -> b
$ (Extern -> (Text, Extern)) -> [Extern] -> [(Text, Extern)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Extern
e -> (Extern -> Text
extName Extern
e, Extern
e)) [Extern]
exts)

            sts0 :: Sts
            sts0 :: Outs
sts0 = [(Text, BV)] -> Outs
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Text
x, BV
bv) | Register Annote
_ Text
x Size
_ BV
bv <- Device -> [Register]
devRegisters Device
dev ]

            step :: MonadError AstError m => Sts -> Ins -> m (Outs, Sts)
            step :: forall (m :: * -> *).
MonadError AstError m =>
Outs -> Ins -> m (Outs, Outs)
step Outs
sts Ins
ins = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Instance] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Instance] -> Bool) -> [Instance] -> Bool
forall a b. (a -> b) -> a -> b
$ Device -> [Instance]
devInstances Device
dev) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Device -> Annote
forall a. Annotated a => a -> Annote
ann Device
dev) Text
"cannot evaluate a device with extern instances"
                  let rho0 :: Outs
rho0 = Outs
sts Outs -> Outs -> Outs
forall a. Semigroup a => a -> a -> a
<> [(Text, BV)] -> Outs
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Text
x, Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
sz) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Text -> Ins -> Integer
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.findWithDefault Integer
0 Text
x Ins
ins)
                                                 | (Text
x, Size
sz) <- Device -> [(Text, Size)]
devInputs Device
dev ]
                  (_, outs, sts') <- ((Outs, Outs, Outs) -> Stmt -> m (Outs, Outs, Outs))
-> (Outs, Outs, Outs) -> [Stmt] -> m (Outs, Outs, Outs)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Outs, Outs, Outs) -> Stmt -> m (Outs, Outs, Outs)
forall (m :: * -> *).
MonadError AstError m =>
(Outs, Outs, Outs) -> Stmt -> m (Outs, Outs, Outs)
stmt (Outs
rho0, Outs
forall a. Monoid a => a
mempty, Outs
sts) ([Stmt] -> m (Outs, Outs, Outs)) -> [Stmt] -> m (Outs, Outs, Outs)
forall a b. (a -> b) -> a -> b
$ Device -> [Stmt]
devBody Device
dev
                  pure (outs, sts')

            stmt :: MonadError AstError m => (HashMap Name BV, Outs, Sts) -> Stmt -> m (HashMap Name BV, Outs, Sts)
            stmt :: forall (m :: * -> *).
MonadError AstError m =>
(Outs, Outs, Outs) -> Stmt -> m (Outs, Outs, Outs)
stmt (Outs
rho, Outs
outs, Outs
sts) = \ case
                  SLet Annote
_ Text
x Exp
e      -> (\ BV
v -> (Text -> BV -> Outs -> Outs
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
x BV
v Outs
rho, Outs
outs, Outs
sts)) (BV -> (Outs, Outs, Outs)) -> m BV -> m (Outs, Outs, Outs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IEnv -> Outs -> Exp -> m BV
forall (m :: * -> *).
MonadError AstError m =>
IEnv -> Outs -> Exp -> m BV
evalExp IEnv
env Outs
rho Exp
e
                  SOutput Annote
_ Text
x Exp
e   -> (\ BV
v -> (Outs
rho, Text -> BV -> Outs -> Outs
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
x BV
v Outs
outs, Outs
sts)) (BV -> (Outs, Outs, Outs)) -> m BV -> m (Outs, Outs, Outs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IEnv -> Outs -> Exp -> m BV
forall (m :: * -> *).
MonadError AstError m =>
IEnv -> Outs -> Exp -> m BV
evalExp IEnv
env Outs
rho Exp
e
                  SNext Annote
_ Text
x Exp
e     -> (\ BV
v -> (Outs
rho, Outs
outs, Text -> BV -> Outs -> Outs
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
x BV
v Outs
sts)) (BV -> (Outs, Outs, Outs)) -> m BV -> m (Outs, Outs, Outs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IEnv -> Outs -> Exp -> m BV
forall (m :: * -> *).
MonadError AstError m =>
IEnv -> Outs -> Exp -> m BV
evalExp IEnv
env Outs
rho Exp
e
                  SInstIn Annote
an Text
_ Text
_ Exp
_ -> Annote -> Text -> m (Outs, Outs, Outs)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"cannot evaluate a device with extern instances"

evalExp :: forall m. MonadError AstError m => IEnv -> HashMap Name BV -> Exp -> m BV
evalExp :: forall (m :: * -> *).
MonadError AstError m =>
IEnv -> Outs -> Exp -> m BV
evalExp IEnv
env = Outs -> Exp -> m BV
go
      where go :: HashMap Name BV -> Exp -> m BV
            go :: Outs -> Exp -> m BV
go Outs
rho = \ case
                  Lit Annote
_ BV
bv      -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BV
bv
                  Undef Annote
_ Size
sz    -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> BV
zeros (Int -> BV) -> Int -> BV
forall a b. (a -> b) -> a -> b
$ Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
sz
                  Var Annote
an Size
_ Text
x    -> m BV -> (BV -> m BV) -> Maybe BV -> m BV
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> m BV
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> m BV) -> Text -> m BV
forall a b. (a -> b) -> a -> b
$ Text
"unbound variable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x) BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe BV -> m BV) -> Maybe BV -> m BV
forall a b. (a -> b) -> a -> b
$ Text -> Outs -> Maybe BV
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
x Outs
rho
                  Cat Annote
_ Exp
e1 Exp
e2   -> BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
(<>) (BV -> BV -> BV) -> m BV -> m (BV -> BV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Outs -> Exp -> m BV
go Outs
rho Exp
e1 m (BV -> BV) -> m BV -> m BV
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Outs -> Exp -> m BV
go Outs
rho Exp
e2
                  Slice Annote
_ Size
i Size
k Exp
e -> Size -> Size -> BV -> BV
slice Size
i Size
k (BV -> BV) -> m BV -> m BV
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Outs -> Exp -> m BV
go Outs
rho Exp
e
                  Prim Annote
an Size
_ Op
op [Exp]
es -> (Exp -> m BV) -> [Exp] -> m [BV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Outs -> Exp -> m BV
go Outs
rho) [Exp]
es m [BV] -> ([BV] -> m BV) -> m BV
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Annote -> Op -> [BV] -> m BV
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Op -> [BV] -> m BV
evalOp Annote
an Op
op
                  Call Annote
an Size
_ Text
g [Exp]
es  -> case Text -> HashMap Text Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
g (HashMap Text Defn -> Maybe Defn)
-> HashMap Text Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ IEnv -> HashMap Text Defn
envDefns IEnv
env of
                        Maybe Defn
Nothing -> Annote -> Text -> m BV
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> m BV) -> Text -> m BV
forall a b. (a -> b) -> a -> b
$ Text
"call to unknown definition: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
g
                        Just Defn
d  -> (Exp -> m BV) -> [Exp] -> m [BV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Outs -> Exp -> m BV
go Outs
rho) [Exp]
es m [BV] -> ([BV] -> m BV) -> m BV
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Defn -> [BV] -> m BV
apply Defn
d
                  XCall Annote
an Size
_ Text
x [Natural]
_ [Exp]
es -> case Text -> HashMap Text Extern -> Maybe Extern
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
x (IEnv -> HashMap Text Extern
envExterns IEnv
env) Maybe Extern -> (Extern -> Maybe Text) -> Maybe Text
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Extern -> Maybe Text
extModel of
                        Just Text
g | Just Defn
d <- Text -> HashMap Text Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
g (HashMap Text Defn -> Maybe Defn)
-> HashMap Text Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ IEnv -> HashMap Text Defn
envDefns IEnv
env -> (Exp -> m BV) -> [Exp] -> m [BV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Outs -> Exp -> m BV
go Outs
rho) [Exp]
es m [BV] -> ([BV] -> m BV) -> m BV
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Defn -> [BV] -> m BV
apply Defn
d
                        Maybe Text
_ -> Annote -> Text -> m BV
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m BV) -> Text -> m BV
forall a b. (a -> b) -> a -> b
$ Text
"cannot evaluate extern " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
                                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (no usable Haskell model: see the rwPrimExtern documentation)."
                  If Annote
_ Size
_ Exp
c Exp
t Exp
e  -> do
                        c' <- Outs -> Exp -> m BV
go Outs
rho Exp
c
                        if nat c' /= 0 then go rho t else go rho e
                  Let Annote
_ Size
_ Text
x Exp
e1 Exp
e2 -> do
                        v <- Outs -> Exp -> m BV
go Outs
rho Exp
e1
                        go (Map.insert x v rho) e2

            apply :: Defn -> [BV] -> m BV
            apply :: Defn -> [BV] -> m BV
apply (Defn Annote
_ Text
_ Sig
_ [Text]
ps Exp
body Bool
_ Blind [Text]
_) [BV]
vs = Outs -> Exp -> m BV
go ([(Text, BV)] -> Outs
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(Text, BV)] -> Outs) -> [(Text, BV)] -> Outs
forall a b. (a -> b) -> a -> b
$ [Text] -> [BV] -> [(Text, BV)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
ps [BV]
vs) Exp
body

slice :: Index -> Size -> BV -> BV
slice :: Size -> Size -> BV -> BV
slice Size
i Size
k BV
x | Size
k Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0    = BV
BV.nil
            | Bool
otherwise = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
BV.bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
k) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
i

-- | Primitive denotations (doc/hyle.md, section 5.2).
evalOp :: MonadError AstError m => Annote -> Op -> [BV] -> m BV
evalOp :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> Op -> [BV] -> m BV
evalOp Annote
an Op
op [BV]
vs = case (Op
op, [BV]
vs) of
      (Op
Add   , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
      (Op
Sub   , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b (-)
      (Op
Mul   , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)
      (Op
UDiv  , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ if BV -> Integer
nat BV
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int -> BV
ones (BV -> Int
width BV
a) else Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` BV -> Integer
nat BV
b
      (Op
UMod  , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ if BV -> Integer
nat BV
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then BV
a else Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` BV -> Integer
nat BV
b
      (Op
Pow   , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
powMod (BV -> Integer
nat BV
a) (BV -> Integer
nat BV
b)
            where -- Square-and-multiply mod 2^n: plain (^) would build the
                  -- full Integer power first, which is astronomic for wide
                  -- dynamic exponents (the result cycles mod 2^n anyway).
                  powMod :: Integer -> Integer -> Integer
                  powMod :: Integer -> Integer -> Integer
powMod Integer
x Integer
e | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1    = Integer
0
                             | Bool
otherwise = Integer -> Integer -> Integer -> Integer
forall {t}. Integral t => Integer -> Integer -> t -> Integer
go Integer
1 (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) Integer
e
                        where m :: Integer
m = Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ BV -> Int
width BV
a
                              go :: Integer -> Integer -> t -> Integer
go Integer
acc Integer
_ t
0  = Integer
acc
                              go Integer
acc Integer
s t
e' = Integer -> Integer -> t -> Integer
go (if t -> Bool
forall a. Integral a => a -> Bool
odd t
e' then Integer
acc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
s Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m else Integer
acc) (Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
s Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m) (t
e' t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
2)
      (Op
And   , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.)
      (Op
Or    , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.)
      (Op
XOr   , [BV
a, BV
b]) -> BV -> BV -> (Integer -> Integer -> Integer) -> m BV
forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
xor
      (Op
Not   , [BV
a])    -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Bits a => a -> a
complement (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a
      (Op
Shl   , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> (Integer -> Int -> Integer) -> BV
shiftOp BV
a BV
b ((Integer -> Int -> Integer) -> BV)
-> (Integer -> Int -> Integer) -> BV
forall a b. (a -> b) -> a -> b
$ \ Integer
x Int
s -> Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s
      (Op
LShr  , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> (Integer -> Int -> Integer) -> BV
shiftOp BV
a BV
b ((Integer -> Int -> Integer) -> BV)
-> (Integer -> Int -> Integer) -> BV
forall a b. (a -> b) -> a -> b
$ \ Integer
x Int
s -> Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s
      (Op
AShr  , [BV
a, BV
b]) -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ if BV -> Integer
nat BV
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a. Integral a => a -> Integer
toInteger (BV -> Int
width BV
a)
                                  then (if BV -> Integer
sint BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Int -> BV
ones (BV -> Int
width BV
a) else Int -> BV
zeros (BV -> Int
width BV
a))
                                  else BV -> BV -> BV
ashr BV
a BV
b
      (Op
Eq    , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== BV -> Integer
nat BV
b
      (Op
Ne    , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Integer
nat BV
b
      (Op
ULt   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< BV -> Integer
nat BV
b
      (Op
ULe   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= BV -> Integer
nat BV
b
      (Op
UGt   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV -> Integer
nat BV
b
      (Op
UGe   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= BV -> Integer
nat BV
b
      (Op
SLt   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
sint BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< BV -> Integer
sint BV
b
      (Op
SLe   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
sint BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= BV -> Integer
sint BV
b
      (Op
SGt   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
sint BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV -> Integer
sint BV
b
      (Op
SGe   , [BV
a, BV
b]) -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
sint BV
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= BV -> Integer
sint BV
b
      (Op
RedAnd, [BV
a])    -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ BV -> Int
width BV
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
      (Op
RedOr , [BV
a])    -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0
      (Op
RedXOr, [BV
a])    -> Bool -> m BV
forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp (Bool -> m BV) -> Bool -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> Bool
forall a. Integral a => a -> Bool
odd (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a
      (ZExt Size
m, [BV
a])    -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
mkBV (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
m) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a
      (SExt Size
m, [BV
a])    -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
mkBV (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
m) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
sint BV
a
      (Trunc Size
m, [BV
a])   -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ Size -> Size -> BV -> BV
slice Size
0 Size
m BV
a
      (Rep Natural
k , [BV
a])    -> BV -> m BV
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
forall a b. (a -> b) -> a -> b
$ [BV] -> BV
forall a. Monoid a => [a] -> a
mconcat ([BV] -> BV) -> [BV] -> BV
forall a b. (a -> b) -> a -> b
$ Int -> BV -> [BV]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
k) BV
a
      (Op, [BV])
_                -> Annote -> Text -> m BV
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> m BV) -> Text -> m BV
forall a b. (a -> b) -> a -> b
$ Text
"ill-formed primitive application: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Op -> Text
opName Op
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" with " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt ([BV] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BV]
vs) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" arguments"
      where arith :: Monad m' => BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
            arith :: forall (m' :: * -> *).
Monad m' =>
BV -> BV -> (Integer -> Integer -> Integer) -> m' BV
arith BV
a BV
b Integer -> Integer -> Integer
f = BV -> m' BV
forall a. a -> m' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m' BV) -> BV -> m' BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Integer -> Integer
`f` BV -> Integer
nat BV
b

            cmp :: Monad m' => Bool -> m' BV
            cmp :: forall (m' :: * -> *). Monad m' => Bool -> m' BV
cmp Bool
c = BV -> m' BV
forall a. a -> m' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m' BV) -> BV -> m' BV
forall a b. (a -> b) -> a -> b
$ if Bool
c then Int -> BV
ones Int
1 else Int -> BV
zeros Int
1

            shiftOp :: BV -> BV -> (Integer -> Int -> Integer) -> BV
            shiftOp :: BV -> BV -> (Integer -> Int -> Integer) -> BV
shiftOp BV
a BV
b Integer -> Int -> Integer
f | BV -> Integer
nat BV
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a. Integral a => a -> Integer
toInteger (BV -> Int
width BV
a) = Int -> BV
zeros (Int -> BV) -> Int -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Int
width BV
a
                          | Bool
otherwise                    = Int -> Integer -> BV
mkBV (BV -> Int
width BV
a) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ BV -> Integer
nat BV
a Integer -> Int -> Integer
`f` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BV -> Integer
nat BV
b)

            mkBV :: Int -> Integer -> BV
            mkBV :: Int -> Integer -> BV
mkBV = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec

-- | Signed (two's-complement) reading.
sint :: BV -> Integer
sint :: BV -> Integer
sint BV
x | BV -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0                       = Integer
0
       | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit (BV -> Integer
nat BV
x) (BV -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)      = BV -> Integer
nat BV
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ BV -> Int
width BV
x
       | Bool
otherwise                          = BV -> Integer
nat BV
x

unfoldMealyT :: Applicative m => (s -> a -> m (b, s)) -> s -> MealyT m a b
unfoldMealyT :: forall (m :: * -> *) s a b.
Applicative m =>
(s -> a -> m (b, s)) -> s -> MealyT m a b
unfoldMealyT s -> a -> m (b, s)
f = s -> MealyT m a b
mealy
      where mealy :: s -> MealyT m a b
mealy s
s = (a -> m (b, MealyT m a b)) -> MealyT m a b
forall (m :: * -> *) a b.
(a -> m (b, MealyT m a b)) -> MealyT m a b
MealyT ((a -> m (b, MealyT m a b)) -> MealyT m a b)
-> (a -> m (b, MealyT m a b)) -> MealyT m a b
forall a b. (a -> b) -> a -> b
$ \ a
a -> (\ (b
b, s
s') -> (b
b, s -> MealyT m a b
mealy s
s')) ((b, s) -> (b, MealyT m a b)) -> m (b, s) -> m (b, MealyT m a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s -> a -> m (b, s)
f s
s a
a