{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | The Cryptol backend on Hyle: the width-preserving embedding of
--   doc/hyle.md, section 8.4. Every Hyle defn becomes a Cryptol function
--   over bitvectors; the device becomes a step function @rw_step@ (registers
--   and inputs to outputs and next-register values, as one concatenated
--   vector) wrapped in the standard Mealy stream idiom @rw_device@, matching
--   the Hyle interpreter bit for bit.
--
--   Because Hyle widths are explicit and exact, no width reconstruction
--   happens here: slices flip to Cryptol's MSB-first order, division gets
--   the SMT-LIB division-by-zero guard (doc/hyle.md, section 5.2), and
--   coercions and reductions map to small fixed helpers; everything else is
--   a per-construct template.
--
--   Combinational externs without models become uninterpreted functions in a
--   @parameter@ block (generic arguments become leading 32-bit arguments);
--   externs with models become ordinary calls to the model's function.
--   Devices with instances (sequential externs) are rejected: a pure target
--   has no equivalent.
module ReWire.Hyle.ToCryptol (compileProgram) where

import ReWire.Annotation (Annote, Annotated (ann))
import ReWire.BitVector (zeros, ones)

import qualified ReWire.BitVector as BV
import ReWire.Config (Config)
import ReWire.Cryptol.Syntax (cryptolName)
import ReWire.Error (failAt, failInternal, AstError, MonadError)
import ReWire.Hyle.Syntax
import ReWire.Pretty (showt)

import qualified ReWire.Cryptol.Syntax as Cry

import Control.Monad (foldM)
import Control.Monad.State (StateT, evalStateT, gets, modify)
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.List (sortOn)
import Data.Text (Text)

import qualified Data.HashMap.Strict as Map
import qualified Data.HashSet        as Set
import qualified Data.Text           as T

-- | Global environment: Hyle global names to Cryptol names; extern decls.
data Env = Env
      { Env -> HashMap Text Text
envNames   :: HashMap GId Cry.Name
      , Env -> HashMap Text Extern
envExterns :: HashMap Name Extern
      , Env -> HashMap Text Text
envExtNames :: HashMap Name Cry.Name -- ^ Extern to its parameter-block name.
      }

-- | Per-defn state: a fresh counter, the where-bindings in creation order,
--   and the local-name map (Hyle locals to legal Cryptol locals).
data TCS = TCS
      { TCS -> Int
tcsCtr    :: !Int
      , TCS -> [Bind]
tcsBinds  :: ![Cry.Bind]
      , TCS -> HashMap Text Text
tcsLocals :: !(HashMap Name Cry.Name)
      }

type TCM m = StateT TCS m

compileProgram :: forall m. MonadError AstError m => Config -> Program -> m Cry.Module
compileProgram :: forall (m :: * -> *).
MonadError AstError m =>
Config -> Program -> m Module
compileProgram Config
_conf (Program [Extern]
exts [Defn]
ds Device
dev) = do
      case Device -> [Instance]
devInstances Device
dev of
            Instance Annote
an Text
_ Text
ex [Natural]
_ : [Instance]
_ -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"Clocked extern '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ex
                                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' cannot be translated to a pure Cryptol function."
            []                    -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      defns <- (Defn -> m Defn) -> [Defn] -> m [Defn]
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 (Env -> Defn -> m Defn
forall (m :: * -> *).
MonadError AstError m =>
Env -> Defn -> m Defn
transDefn Env
env) [Defn]
ds
      step  <- stepDefn env dev
      pure $ Cry.Module modName comments params $ defns <> [step, deviceDefn dev]
      where env :: Env
            env :: Env
env = HashMap Text Text
-> HashMap Text Extern -> HashMap Text Text -> Env
Env HashMap Text Text
names ([(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) HashMap Text Text
extNames

            (HashMap Text Text
names, HashMap Text Text
extNames) = [Defn] -> [Extern] -> (HashMap Text Text, HashMap Text Text)
buildNames [Defn]
ds [Extern]
exts

            modName :: Cry.Name
            modName :: Text
modName | Text -> Bool
T.null Text
top = Text
"device"
                    | Bool
otherwise  = Text
top
                  where top :: Text
top = Text -> Text
cryptolName (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Device -> Text
devName Device
dev

            comments :: [Text]
            comments :: [Text]
comments = [ Text
"Generated by rwc from device: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Device -> Text
devName Device
dev Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"."
                       , Text
"rw_device maps a sequence of per-cycle inputs to per-cycle outputs."
                       ]

            -- | Model-less combinational externs, as uninterpreted functions:
            --   generic parameters become leading 32-bit arguments.
            params :: [Cry.Param]
            params :: [Param]
params = (Param -> Text) -> [Param] -> [Param]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\ (Cry.Param Text
n [Size]
_ Size
_) -> Text
n)
                  [ Text -> [Size] -> Size -> Param
Cry.Param Text
n ((Text -> Size) -> [Text] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Size -> Text -> Size
forall a b. a -> b -> a
const Size
32) (Extern -> [Text]
extGenerics Extern
e) [Size] -> [Size] -> [Size]
forall a. Semigroup a => a -> a -> a
<> ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd (Extern -> [(Text, Size)]
extInputs Extern
e)) (Extern -> Size
externResultSize Extern
e)
                  | Extern
e <- [Extern]
exts
                  , Extern -> Maybe Text
extModel Extern
e Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Text
forall a. Maybe a
Nothing
                  , Extern -> ExternKind
extKind Extern
e ExternKind -> ExternKind -> Bool
forall a. Eq a => a -> a -> Bool
== ExternKind
Comb
                  , Just Text
n <- [Text -> HashMap Text Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Extern -> Text
extName Extern
e) HashMap Text Text
extNames]
                  ]

-- | Assigns each defn a Cryptol name @rw_\<sanitized\>@ and each extern
--   @ext_\<sanitized\>@, deduplicating with numeric suffixes and avoiding the
--   reserved @rw_step@/@rw_device@.
buildNames :: [Defn] -> [Extern] -> (HashMap GId Cry.Name, HashMap Name Cry.Name)
buildNames :: [Defn] -> [Extern] -> (HashMap Text Text, HashMap Text Text)
buildNames [Defn]
ds [Extern]
exts = (HashMap Text Text
dnames, HashMap Text Text
extnames)
      where (HashMap Text Text
dnames, HashSet Text
used') = ((HashMap Text Text, HashSet Text)
 -> Text -> (HashMap Text Text, HashSet Text))
-> (HashMap Text Text, HashSet Text)
-> [Text]
-> (HashMap Text Text, HashSet Text)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Text
-> (HashMap Text Text, HashSet Text)
-> Text
-> (HashMap Text Text, HashSet Text)
add Text
"rw_") (HashMap Text Text
forall a. Monoid a => a
mempty, [Text] -> HashSet Text
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList [Text
"rw_device", Text
"rw_step"]) ([Text] -> (HashMap Text Text, HashSet Text))
-> [Text] -> (HashMap Text Text, HashSet Text)
forall a b. (a -> b) -> a -> b
$ (Defn -> Text) -> [Defn] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Defn -> Text
defnName [Defn]
ds
            (HashMap Text Text
extnames, HashSet Text
_)   = ((HashMap Text Text, HashSet Text)
 -> Text -> (HashMap Text Text, HashSet Text))
-> (HashMap Text Text, HashSet Text)
-> [Text]
-> (HashMap Text Text, HashSet Text)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Text
-> (HashMap Text Text, HashSet Text)
-> Text
-> (HashMap Text Text, HashSet Text)
add Text
"ext_") (HashMap Text Text
forall a. Monoid a => a
mempty, HashSet Text
used') ([Text] -> (HashMap Text Text, HashSet Text))
-> [Text] -> (HashMap Text Text, HashSet Text)
forall a b. (a -> b) -> a -> b
$ (Extern -> Text) -> [Extern] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Extern -> Text
extName [Extern]
exts

            add :: Text -> (HashMap Text Cry.Name, HashSet Cry.Name) -> Text -> (HashMap Text Cry.Name, HashSet Cry.Name)
            add :: Text
-> (HashMap Text Text, HashSet Text)
-> Text
-> (HashMap Text Text, HashSet Text)
add Text
pfx (HashMap Text Text
m, HashSet Text
used) Text
k = (Text -> Text -> HashMap Text Text -> HashMap Text Text
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
k Text
n HashMap Text Text
m, Text -> HashSet Text -> HashSet Text
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Text
n HashSet Text
used)
                  where n :: Text
n = HashSet Text -> Text -> Text
freshen HashSet Text
used (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
pfx Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
cryptolName Text
k

            freshen :: HashSet Cry.Name -> Cry.Name -> Cry.Name
            freshen :: HashSet Text -> Text -> Text
freshen HashSet Text
used Text
b | Text
b Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
used = Int -> Text
forall {a}. (Num a, TextShow a) => a -> Text
go (Int
2 :: Int)
                           | Bool
otherwise           = Text
b
                  where go :: a -> Text
go a
i | Text
n Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
used = a -> Text
go (a -> Text) -> a -> Text
forall a b. (a -> b) -> a -> b
$ a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
                             | Bool
otherwise           = Text
n
                              where n :: Text
n = Text
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. TextShow a => a -> Text
showt a
i

-- | Look up a defn's Cryptol name.
defnNm' :: MonadError AstError m => Env -> Annote -> GId -> m Cry.Name
defnNm' :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> m Text
defnNm' Env
env Annote
an Text
g = case Text -> HashMap Text Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
g (HashMap Text Text -> Maybe Text)
-> HashMap Text Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Text Text
envNames Env
env of
      Just Text
n  -> Text -> m Text
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
n
      Maybe Text
Nothing -> Annote -> Text -> m Text
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> m Text) -> Text -> m Text
forall a b. (a -> b) -> a -> b
$ Text
"unknown definition: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
g

fresh :: Monad m => TCM m Cry.Name
fresh :: forall (m :: * -> *). Monad m => TCM m Text
fresh = do
      ctr <- (TCS -> Int) -> StateT TCS m Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TCS -> Int
tcsCtr
      modify $ \ TCS
ts -> TCS
ts { tcsCtr = ctr + 1 }
      pure $ "s" <> showt ctr

-- | Bind a Hyle local name to a fresh Cryptol local.
bindLocal :: Monad m => Name -> TCM m Cry.Name
bindLocal :: forall (m :: * -> *). Monad m => Text -> TCM m Text
bindLocal Text
x = do
      n <- TCM m Text
forall (m :: * -> *). Monad m => TCM m Text
fresh
      modify $ \ TCS
ts -> TCS
ts { tcsLocals = Map.insert x n $ tcsLocals ts }
      pure n

pushBind :: Monad m => Cry.Name -> Size -> Cry.Exp -> TCM m ()
pushBind :: forall (m :: * -> *). Monad m => Text -> Size -> Exp -> TCM m ()
pushBind Text
n Size
sz Exp
e = (TCS -> TCS) -> StateT TCS m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TCS -> TCS) -> StateT TCS m ())
-> (TCS -> TCS) -> StateT TCS m ()
forall a b. (a -> b) -> a -> b
$ \ TCS
ts -> TCS
ts { tcsBinds = tcsBinds ts <> [Cry.Bind n (Cry.TBits sz) e] }

transDefn :: MonadError AstError m => Env -> Defn -> m Cry.Defn
transDefn :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Defn -> m Defn
transDefn Env
env (Defn Annote
an Text
g (Sig Annote
_ [Size]
argSzs Size
res) [Text]
ps Exp
body Bool
_ Blind [Text]
_) = (StateT TCS m Defn -> TCS -> m Defn)
-> TCS -> StateT TCS m Defn -> m Defn
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT TCS m Defn -> TCS -> m Defn
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Int -> [Bind] -> HashMap Text Text -> TCS
TCS Int
0 [] HashMap Text Text
forall a. Monoid a => a
mempty) (StateT TCS m Defn -> m Defn) -> StateT TCS m Defn -> m Defn
forall a b. (a -> b) -> a -> b
$ do
      let xs :: [Text]
xs = (Int -> Text -> Text) -> [Int] -> [Text] -> [Text]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Text
_ -> Text
"x" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
i) [Int
0 :: Int ..] [Text]
ps
      (TCS -> TCS) -> StateT TCS m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TCS -> TCS) -> StateT TCS m ())
-> (TCS -> TCS) -> StateT TCS m ()
forall a b. (a -> b) -> a -> b
$ \ TCS
ts -> TCS
ts { tcsLocals = Map.fromList $ zip ps xs }
      n     <- Env -> Annote -> Text -> StateT TCS m Text
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> m Text
defnNm' Env
env Annote
an Text
g
      e     <- transExp env body
      binds <- gets tcsBinds
      pure $ Cry.Defn comments n False (zip xs $ map Cry.TBits argSzs) (Cry.TBits res) e binds
      where comments :: [Text]
            comments :: [Text]
comments = [Text
g | Text -> Text
cryptolName Text
g Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
g]

transExp :: forall m. MonadError AstError m => Env -> Exp -> TCM m Cry.Exp
transExp :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env = Exp -> TCM m Exp
go
      where go :: Exp -> TCM m Cry.Exp
            go :: Exp -> TCM m Exp
go = \ case
                  Lit Annote
_ BV
bv        -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TCM m Exp) -> Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ BV -> Exp
Cry.Lit BV
bv
                  Undef Annote
_ Size
sz      -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TCM m Exp) -> Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ BV -> Exp
Cry.Lit (BV -> Exp) -> BV -> Exp
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      -> (TCS -> Maybe Text) -> StateT TCS m (Maybe Text)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Text -> HashMap Text Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
x (HashMap Text Text -> Maybe Text)
-> (TCS -> HashMap Text Text) -> TCS -> Maybe Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCS -> HashMap Text Text
tcsLocals) StateT TCS m (Maybe Text) -> (Maybe Text -> TCM m Exp) -> TCM m Exp
forall a b.
StateT TCS m a -> (a -> StateT TCS m b) -> StateT TCS m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                        Just Text
n  -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TCM m Exp) -> Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
Cry.Var Text
n
                        Maybe Text
Nothing -> Annote -> Text -> TCM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> TCM m Exp) -> Text -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unbound variable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
                  e :: Exp
e@Cat {}        -> [Exp] -> Exp
Cry.cat ([Exp] -> Exp) -> StateT TCS m [Exp] -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> TCM m Exp) -> [Exp] -> StateT TCS m [Exp]
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 Exp -> TCM m Exp
go (Exp -> [Exp]
gather Exp
e)
                  Slice Annote
_ Size
i Size
k Exp
e   -> Size -> Size -> Size -> Exp -> Exp
Cry.slice (Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
e) (Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
e Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
i Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
k) Size
k (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TCM m Exp
go Exp
e
                  Prim Annote
an Size
sz Op
op [Exp]
es -> Env -> Annote -> Size -> Op -> [Exp] -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Size -> Op -> [Exp] -> TCM m Exp
transPrim Env
env Annote
an Size
sz Op
op [Exp]
es
                  Call Annote
an Size
_ Text
g [Exp]
es  -> Text -> [Exp] -> Exp
Cry.Call (Text -> [Exp] -> Exp)
-> StateT TCS m Text -> StateT TCS m ([Exp] -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Annote -> Text -> StateT TCS m Text
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> m Text
defnNm' Env
env Annote
an Text
g StateT TCS m ([Exp] -> Exp) -> StateT TCS m [Exp] -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Exp -> TCM m Exp) -> [Exp] -> StateT TCS m [Exp]
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 Exp -> TCM m Exp
go [Exp]
es
                  XCall Annote
an Size
_ Text
x [Natural]
cs [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 (HashMap Text Extern -> Maybe Extern)
-> HashMap Text Extern -> Maybe Extern
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Text Extern
envExterns Env
env of
                        Maybe Extern
Nothing -> Annote -> Text -> TCM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> TCM m Exp) -> Text -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unknown extern: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
                        Just Extern
ex -> case Extern -> Maybe Text
extModel Extern
ex of
                              Just Text
g  -> Text -> [Exp] -> Exp
Cry.Call (Text -> [Exp] -> Exp)
-> StateT TCS m Text -> StateT TCS m ([Exp] -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Annote -> Text -> StateT TCS m Text
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> m Text
defnNm' Env
env Annote
an Text
g StateT TCS m ([Exp] -> Exp) -> StateT TCS m [Exp] -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Exp -> TCM m Exp) -> [Exp] -> StateT TCS m [Exp]
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 Exp -> TCM m Exp
go [Exp]
es
                              Maybe Text
Nothing -> case Text -> HashMap Text Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
x (HashMap Text Text -> Maybe Text)
-> HashMap Text Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Text Text
envExtNames Env
env of
                                    Maybe Text
Nothing -> Annote -> Text -> TCM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> TCM m Exp) -> Text -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unknown extern: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
                                    Just Text
n  -> Text -> [Exp] -> Exp
Cry.Call Text
n ([Exp] -> Exp) -> ([Exp] -> [Exp]) -> [Exp] -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Natural -> Exp) -> [Natural] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (BV -> Exp
Cry.Lit (BV -> Exp) -> (Natural -> BV) -> Natural -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
BV.bitVec Int
32 (Integer -> BV) -> (Natural -> Integer) -> Natural -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger) [Natural]
cs [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<>) ([Exp] -> Exp) -> StateT TCS m [Exp] -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> TCM m Exp) -> [Exp] -> StateT TCS m [Exp]
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 Exp -> TCM m Exp
go [Exp]
es
                  If Annote
_ Size
_ Exp
c Exp
t Exp
e    -> Exp -> Exp -> Exp -> Exp
Cry.If (Exp -> Exp -> Exp -> Exp)
-> TCM m Exp -> StateT TCS m (Exp -> Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
c StateT TCS m (Exp -> Exp -> Exp)
-> TCM m Exp -> StateT TCS m (Exp -> Exp)
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> TCM m Exp
go Exp
t StateT TCS m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> TCM m Exp
go Exp
e
                  Let Annote
_ Size
_ Text
x Exp
e1 Exp
e2 -> do
                        e1' <- Exp -> TCM m Exp
go Exp
e1
                        n   <- bindLocal x
                        pushBind n (sizeOf e1) e1'
                        go e2

-- | A [1]-valued Hyle expression as a Cryptol Bit: comparisons and
--   width-1 logical structure translate directly, anything else is indexed.
transBit :: forall m. MonadError AstError m => Env -> Exp -> TCM m Cry.Exp
transBit :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
e = case Exp
e of
      Prim Annote
_ Size
_ Op
op [Exp
a, Exp
b] | Just Text
cop <- Size -> Op -> Maybe Text
cmpName (Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a) Op
op
                        -> Text -> Exp -> Exp -> Exp
Cry.BinOp Text
cop (Exp -> Exp -> Exp) -> TCM m Exp -> StateT TCS m (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a StateT TCS m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
b
      Prim Annote
_ Size
1 Op
And [Exp
a, Exp
b] -> Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"&&" (Exp -> Exp -> Exp) -> TCM m Exp -> StateT TCS m (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
a StateT TCS m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
b
      Prim Annote
_ Size
1 Op
Or  [Exp
a, Exp
b] -> Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"||" (Exp -> Exp -> Exp) -> TCM m Exp -> StateT TCS m (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
a StateT TCS m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
b
      Prim Annote
_ Size
1 Op
Not [Exp
a]    -> Text -> Exp -> Exp
Cry.UnOp Text
"~" (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env Exp
a
      Prim Annote
_ Size
1 Op
RedOr [Exp
a]  -> (\ Exp
a' -> Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"!=" Exp
a' (Text -> Exp
Cry.Var Text
"zero")) (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      Exp
_                   -> (Exp -> Natural -> Exp) -> Natural -> Exp -> Exp
forall a b c. (a -> b -> c) -> b -> a -> c
flip Exp -> Natural -> Exp
Cry.Index Natural
0 (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
e
      where cmpName :: Size -> Op -> Maybe Cry.Name
            cmpName :: Size -> Op -> Maybe Text
cmpName Size
w = \ case
                  Op
Eq  -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"=="
                  Op
Ne  -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"!="
                  Op
ULt -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"<"
                  Op
ULe -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"<="
                  Op
UGt -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
">"
                  Op
UGe -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
">="
                  Op
SLt | Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>= Size
1 -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"<$"
                  Op
SLe | Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>= Size
1 -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"<=$"
                  Op
SGt | Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>= Size
1 -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
">$"
                  Op
SGe | Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>= Size
1 -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
">=$"
                  Op
_   -> Maybe Text
forall a. Maybe a
Nothing

-- | Primitive templates (doc/hyle.md, sections 5.2 and 8.2). Widths are
--   exact by construction, so no resizing happens except where the operator
--   itself changes width.
transPrim :: forall m. MonadError AstError m => Env -> Annote -> Size -> Op -> [Exp] -> TCM m Cry.Exp
transPrim :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Size -> Op -> [Exp] -> TCM m Exp
transPrim Env
env Annote
an Size
sz Op
op [Exp]
args = case (Op
op, [Exp]
args) of
      (Op
Add   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"+" Exp
a Exp
b
      (Op
Sub   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"-" Exp
a Exp
b
      (Op
Mul   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"*" Exp
a Exp
b
      (Op
Pow   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"^^" Exp
a Exp
b
      (Op
UDiv  , [Exp
a, Exp
b]) -> Exp -> TCM m Exp -> TCM m Exp -> TCM m Exp
divGuard Exp
b (Size -> TCM m Exp
allOnes (Size -> TCM m Exp) -> Size -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a) (TCM m Exp -> TCM m Exp) -> TCM m Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp -> TCM m Exp
bin Text
"/" Exp
a Exp
b
      (Op
UMod  , [Exp
a, Exp
b]) -> Exp -> TCM m Exp -> TCM m Exp -> TCM m Exp
divGuard Exp
b (Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a) (TCM m Exp -> TCM m Exp) -> TCM m Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp -> TCM m Exp
bin Text
"%" Exp
a Exp
b
      (Op
And   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"&&" Exp
a Exp
b
      (Op
Or    , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"||" Exp
a Exp
b
      (Op
XOr   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"^" Exp
a Exp
b
      (Op
Not   , [Exp
a])    -> Text -> Exp -> Exp
Cry.UnOp Text
"~" (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Op
Shl   , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
"<<" Exp
a Exp
b
      (Op
LShr  , [Exp
a, Exp
b]) -> Text -> Exp -> Exp -> TCM m Exp
bin Text
">>" Exp
a Exp
b
      (Op
AShr  , [Exp
a, Exp
b])
            | Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
Cry.nil
            | Bool
otherwise     -> Text -> Exp -> Exp -> TCM m Exp
bin Text
">>$" Exp
a Exp
b
      (Op
Eq    , [Exp]
_)      -> TCM m Exp
cmp
      (Op
Ne    , [Exp]
_)      -> TCM m Exp
cmp
      (Op
ULt   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
ULe   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
UGt   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
UGe   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
SLt   , [Exp
a, Exp
_]) | Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
false1
      (Op
SGt   , [Exp
a, Exp
_]) | Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
false1
      (Op
SLe   , [Exp
a, Exp
_]) | Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
true1
      (Op
SGe   , [Exp
a, Exp
_]) | Exp -> Size
forall a. SizeAnnotated a => a -> Size
sizeOf Exp
a Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
true1
      (Op
SLt   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
SLe   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
SGt   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
SGe   , [Exp]
_)      -> TCM m Exp
cmp
      (Op
RedAnd, [Exp
a])    -> (\ Exp
a' -> Exp -> Exp
Cry.Sing (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"==" Exp
a' (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp
Cry.UnOp Text
"~" (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
Cry.Var Text
"zero") (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Op
RedOr , [Exp
a])    -> (\ Exp
a' -> Exp -> Exp
Cry.Sing (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"!=" Exp
a' (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
Cry.Var Text
"zero") (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Op
RedXOr, [Exp
a])    -> (\ Exp
a' -> Exp -> Exp
Cry.Sing (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> [Exp] -> Exp
Cry.Call Text
"rw'parity" [Exp
a']) (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (ZExt Size
m, [Exp
a])    -> Size -> Exp -> Exp
Cry.resize Size
m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Trunc Size
m, [Exp
a])   -> Size -> Exp -> Exp
Cry.resize Size
m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (SExt Size
m, [Exp
a])    -> (\ Exp
a' -> Text -> Natural -> [Exp] -> Exp
Cry.TCall Text
"rw'sext" (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
m) [Exp
a']) (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Rep Natural
k , [Exp
a])    -> (\ Exp
a' -> Text -> Natural -> [Exp] -> Exp
Cry.TCall Text
"rw'repl" Natural
k [Exp
a']) (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a
      (Op, [Exp])
_                -> Annote -> Text -> TCM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> TCM m Exp) -> Text -> TCM m Exp
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 ([Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" arguments."
      where bin :: Cry.Name -> Exp -> Exp -> TCM m Cry.Exp
            bin :: Text -> Exp -> Exp -> TCM m Exp
bin Text
o Exp
a Exp
b = Text -> Exp -> Exp -> Exp
Cry.BinOp Text
o (Exp -> Exp -> Exp) -> TCM m Exp -> StateT TCS m (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
a StateT TCS m (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall a b.
StateT TCS m (a -> b) -> StateT TCS m a -> StateT TCS m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
b

            -- | Comparisons yield a Bit; wrap as [1].
            cmp :: TCM m Cry.Exp
            cmp :: TCM m Exp
cmp = Exp -> Exp
Cry.Sing (Exp -> Exp) -> TCM m Exp -> TCM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transBit Env
env (Annote -> Size -> Op -> [Exp] -> Exp
Prim Annote
an Size
sz Op
op [Exp]
args)

            -- | SMT-LIB division by zero: a zero divisor yields the default.
            divGuard :: Exp -> TCM m Cry.Exp -> TCM m Cry.Exp -> TCM m Cry.Exp
            divGuard :: Exp -> TCM m Exp -> TCM m Exp -> TCM m Exp
divGuard Exp
b TCM m Exp
dflt TCM m Exp
whole = do
                  b'  <- Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
b
                  Cry.If (Cry.BinOp "==" b' $ Cry.Var "zero") <$> dflt <*> whole

            allOnes :: Size -> TCM m Cry.Exp
            allOnes :: Size -> TCM m Exp
allOnes Size
w = Exp -> TCM m Exp
forall a. a -> StateT TCS m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TCM m Exp) -> Exp -> TCM m Exp
forall a b. (a -> b) -> a -> b
$ BV -> Exp
Cry.Lit (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> BV
ones (Int -> BV) -> Int -> BV
forall a b. (a -> b) -> a -> b
$ Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
w

            false1, true1 :: Cry.Exp
            false1 :: Exp
false1 = BV -> Exp
Cry.Lit (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> BV
zeros Int
1
            true1 :: Exp
true1  = BV -> Exp
Cry.Lit (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> BV
ones Int
1

-- | The device's per-cycle step function: registers and inputs (each as one
--   concatenated vector, MSB-first in declaration order) to the
--   concatenation of outputs and next-register values.
stepDefn :: forall m. MonadError AstError m => Env -> Device -> m Cry.Defn
stepDefn :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Device -> m Defn
stepDefn Env
env Device
dev = (StateT TCS m Defn -> TCS -> m Defn)
-> TCS -> StateT TCS m Defn -> m Defn
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT TCS m Defn -> TCS -> m Defn
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Int -> [Bind] -> HashMap Text Text -> TCS
TCS Int
0 [] HashMap Text Text
forall a. Monoid a => a
mempty) (StateT TCS m Defn -> m Defn) -> StateT TCS m Defn -> m Defn
forall a b. (a -> b) -> a -> b
$ do
      ((Text, Size, Size, Text) -> StateT TCS m ())
-> [(Text, Size, Size, Text)] -> StateT TCS m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Text, Size, Size, Text) -> StateT TCS m ()
bindSlice ([(Text, Size, Size, Text)] -> StateT TCS m ())
-> [(Text, Size, Size, Text)] -> StateT TCS m ()
forall a b. (a -> b) -> a -> b
$ Text -> [(Text, Size)] -> [(Text, Size, Size, Text)]
wireLayout Text
"st" [(Text, Size)]
regWires
      ((Text, Size, Size, Text) -> StateT TCS m ())
-> [(Text, Size, Size, Text)] -> StateT TCS m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Text, Size, Size, Text) -> StateT TCS m ()
bindSlice ([(Text, Size, Size, Text)] -> StateT TCS m ())
-> [(Text, Size, Size, Text)] -> StateT TCS m ()
forall a b. (a -> b) -> a -> b
$ Text -> [(Text, Size)] -> [(Text, Size, Size, Text)]
wireLayout Text
"i" ([(Text, Size)] -> [(Text, Size, Size, Text)])
-> [(Text, Size)] -> [(Text, Size, Size, Text)]
forall a b. (a -> b) -> a -> b
$ Device -> [(Text, Size)]
devInputs Device
dev
      (outs, nexts) <- ((HashMap Text Exp, HashMap Text Exp)
 -> Stmt -> StateT TCS m (HashMap Text Exp, HashMap Text Exp))
-> (HashMap Text Exp, HashMap Text Exp)
-> [Stmt]
-> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashMap Text Exp, HashMap Text Exp)
-> Stmt -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
stmt (HashMap Text Exp
forall a. Monoid a => a
mempty, HashMap Text Exp
forall a. Monoid a => a
mempty) ([Stmt] -> StateT TCS m (HashMap Text Exp, HashMap Text Exp))
-> [Stmt] -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
forall a b. (a -> b) -> a -> b
$ Device -> [Stmt]
devBody Device
dev
      result <- catOf outs (devOutputs dev) "output"
      result' <- catOf nexts regWires "register"
      binds <- gets tcsBinds
      pure $ Cry.Defn ["Per-cycle step: outputs # next register values."] "rw_step" False args (Cry.TBits $ ow + rsz)
            (Cry.cat $ result <> result') binds
      where regWires :: [(Name, Size)]
            regWires :: [(Text, Size)]
regWires = [ (Text
x, Size
sz) | Register Annote
_ Text
x Size
sz BV
_ <- Device -> [Register]
devRegisters Device
dev ]

            rsz, iw, ow :: Size
            rsz :: Size
rsz = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd [(Text, Size)]
regWires
            iw :: Size
iw  = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd ([(Text, Size)] -> [Size]) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> a -> b
$ Device -> [(Text, Size)]
devInputs Device
dev
            ow :: Size
ow  = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd ([(Text, Size)] -> [Size]) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> a -> b
$ Device -> [(Text, Size)]
devOutputs Device
dev

            args :: [(Cry.Name, Cry.Ty)]
            args :: [(Text, Ty)]
args = [ (Text
"st", Size -> Ty
Cry.TBits Size
rsz) | Size
rsz Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0 ] [(Text, Ty)] -> [(Text, Ty)] -> [(Text, Ty)]
forall a. Semigroup a => a -> a -> a
<> [ (Text
"i", Size -> Ty
Cry.TBits Size
iw) | Size
iw Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0 ]

            -- | (wire name, width, MSB offset within the vector, vector name)
            wireLayout :: Cry.Name -> [(Name, Size)] -> [(Name, Size, Size, Cry.Name)]
            wireLayout :: Text -> [(Text, Size)] -> [(Text, Size, Size, Text)]
wireLayout Text
v [(Text, Size)]
ws = (Size, [(Text, Size, Size, Text)]) -> [(Text, Size, Size, Text)]
forall a b. (a, b) -> b
snd ((Size, [(Text, Size, Size, Text)]) -> [(Text, Size, Size, Text)])
-> (Size, [(Text, Size, Size, Text)]) -> [(Text, Size, Size, Text)]
forall a b. (a -> b) -> a -> b
$ ((Size, [(Text, Size, Size, Text)])
 -> (Text, Size) -> (Size, [(Text, Size, Size, Text)]))
-> (Size, [(Text, Size, Size, Text)])
-> [(Text, Size)]
-> (Size, [(Text, Size, Size, Text)])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ (Size
off, [(Text, Size, Size, Text)]
acc) (Text
x, Size
sz) -> (Size
off Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz, [(Text, Size, Size, Text)]
acc [(Text, Size, Size, Text)]
-> [(Text, Size, Size, Text)] -> [(Text, Size, Size, Text)]
forall a. Semigroup a => a -> a -> a
<> [(Text
x, Size
sz, Size
off, Text
v)])) (Size
0, []) [(Text, Size)]
ws

            bindSlice :: (Name, Size, Size, Cry.Name) -> TCM m ()
            bindSlice :: (Text, Size, Size, Text) -> StateT TCS m ()
bindSlice (Text
x, Size
sz, Size
off, Text
v) = do
                  n <- Text -> TCM m Text
forall (m :: * -> *). Monad m => Text -> TCM m Text
bindLocal Text
x
                  let total = if Text
v Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"st" then Size
rsz else Size
iw
                  pushBind n sz $ Cry.slice total off sz $ Cry.Var v

            stmt :: (HashMap Name Cry.Exp, HashMap Name Cry.Exp) -> Stmt -> TCM m (HashMap Name Cry.Exp, HashMap Name Cry.Exp)
            stmt :: (HashMap Text Exp, HashMap Text Exp)
-> Stmt -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
stmt (HashMap Text Exp
outs, HashMap Text Exp
nexts) = \ case
                  SLet Annote
_ Text
x Exp
e -> do
                        e' <- Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
e
                        n  <- bindLocal x
                        pushBind n (sizeOf e) e'
                        pure (outs, nexts)
                  SOutput Annote
_ Text
x Exp
e -> (\ Exp
e' -> (Text -> Exp -> HashMap Text Exp -> HashMap Text Exp
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
x Exp
e' HashMap Text Exp
outs, HashMap Text Exp
nexts)) (Exp -> (HashMap Text Exp, HashMap Text Exp))
-> TCM m Exp -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
e
                  SNext Annote
_ Text
x Exp
e   -> (\ Exp
e' -> (HashMap Text Exp
outs, Text -> Exp -> HashMap Text Exp -> HashMap Text Exp
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert Text
x Exp
e' HashMap Text Exp
nexts)) (Exp -> (HashMap Text Exp, HashMap Text Exp))
-> TCM m Exp -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> TCM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> TCM m Exp
transExp Env
env Exp
e
                  SInstIn Annote
an' Text
_ Text
_ Exp
_ -> Annote -> Text -> StateT TCS m (HashMap Text Exp, HashMap Text Exp)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an' Text
"instance input in a device without instances"

            catOf :: HashMap Name Cry.Exp -> [(Name, Size)] -> Text -> TCM m [Cry.Exp]
            catOf :: HashMap Text Exp -> [(Text, Size)] -> Text -> TCM m [Exp]
catOf HashMap Text Exp
m [(Text, Size)]
ws Text
what = ((Text, Size) -> TCM m Exp) -> [(Text, Size)] -> TCM m [Exp]
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 (Text, Size) -> TCM m Exp
forall {f :: * -> *} {b}.
MonadError AstError f =>
(Text, b) -> f Exp
lk [(Text, Size)]
ws
                  where lk :: (Text, b) -> f Exp
lk (Text
x, b
_) = case Text -> HashMap Text Exp -> Maybe Exp
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
x HashMap Text Exp
m of
                              Just Exp
e  -> Exp -> f Exp
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
                              Maybe Exp
Nothing -> Annote -> Text -> f Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal (Device -> Annote
forall a. Annotated a => a -> Annote
ann Device
dev) (Text -> f Exp) -> Text -> f Exp
forall a b. (a -> b) -> a -> b
$ Text
what Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" is never assigned"

-- | The Mealy-machine wrapper around @rw_step@ (the standard stream idiom):
--   @rw_step@'s result has the layout outputs # next-registers.
deviceDefn :: Device -> Cry.Defn
deviceDefn :: Device -> Defn
deviceDefn Device
dev
      | Size
rsz Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0 = [Text]
-> Text -> Bool -> [(Text, Ty)] -> Ty -> Exp -> [Bind] -> Defn
Cry.Defn [Text]
comments Text
"rw_device" Bool
True [(Text
"ins", Ty
insTy)] Ty
outsTy (Text -> Exp
Cry.Var Text
"outs")
            [ Text -> Ty -> Exp -> Bind
Cry.Bind Text
"rs" (Len -> Ty -> Ty
Cry.TSeq Len
Cry.LenVar (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Size -> Ty
Cry.TBits (Size -> Ty) -> Size -> Ty
forall a b. (a -> b) -> a -> b
$ Size
ow Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
rsz)
                  (Exp -> Bind) -> Exp -> Bind
forall a b. (a -> b) -> a -> b
$ Exp -> [(Text, Exp)] -> Exp
Cry.Comp (Text -> [Exp] -> Exp
Cry.Call Text
"rw_step" ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ [Text -> Exp
Cry.Var Text
"st"] [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> [Text -> Exp
Cry.Var Text
"i" | Size
iw Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0])
                  ([(Text, Exp)] -> Exp) -> [(Text, Exp)] -> Exp
forall a b. (a -> b) -> a -> b
$ (Text
"st", Text -> Exp
Cry.Var Text
"sts") (Text, Exp) -> [(Text, Exp)] -> [(Text, Exp)]
forall a. a -> [a] -> [a]
: [(Text, Exp)
inArm]
            , Text -> Ty -> Exp -> Bind
Cry.Bind Text
"sts" (Len -> Ty -> Ty
Cry.TSeq Len
Cry.LenSucc (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Size -> Ty
Cry.TBits Size
rsz)
                  (Exp -> Bind) -> Exp -> Bind
forall a b. (a -> b) -> a -> b
$ Text -> Exp -> Exp -> Exp
Cry.BinOp Text
"#" ([Exp] -> Exp
Cry.SeqLit [BV -> Exp
Cry.Lit BV
inits])
                  (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [(Text, Exp)] -> Exp
Cry.Comp (Exp -> Exp
nxt (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
Cry.Var Text
"r") [(Text
"r", Text -> Exp
Cry.Var Text
"rs")]
            , Text -> Ty -> Exp -> Bind
Cry.Bind Text
"outs" Ty
outsTy
                  (Exp -> Bind) -> Exp -> Bind
forall a b. (a -> b) -> a -> b
$ Exp -> [(Text, Exp)] -> Exp
Cry.Comp (Exp -> Exp
out (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
Cry.Var Text
"r") [(Text
"r", Text -> Exp
Cry.Var Text
"rs")]
            ]
      | Bool
otherwise = [Text]
-> Text -> Bool -> [(Text, Ty)] -> Ty -> Exp -> [Bind] -> Defn
Cry.Defn [Text]
comments Text
"rw_device" Bool
True [(Text
"ins", Ty
insTy)] Ty
outsTy
            (Exp -> [(Text, Exp)] -> Exp
Cry.Comp (Exp -> Exp
out (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> [Exp] -> Exp
Cry.Call Text
"rw_step" [Text -> Exp
Cry.Var Text
"i" | Size
iw Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0]) [(Text, Exp)
inArm]) []
      where rsz, iw, ow :: Size
            rsz :: Size
rsz = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ Size
sz | Register Annote
_ Text
_ Size
sz BV
_ <- Device -> [Register]
devRegisters Device
dev ]
            iw :: Size
iw  = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd ([(Text, Size)] -> [Size]) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> a -> b
$ Device -> [(Text, Size)]
devInputs Device
dev
            ow :: Size
ow  = [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Size) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Size
forall a b. (a, b) -> b
snd ([(Text, Size)] -> [Size]) -> [(Text, Size)] -> [Size]
forall a b. (a -> b) -> a -> b
$ Device -> [(Text, Size)]
devOutputs Device
dev

            inits :: BV.BV
            inits :: BV
inits = [BV] -> BV
forall a. Monoid a => [a] -> a
mconcat [ BV
bv | Register Annote
_ Text
_ Size
_ BV
bv <- Device -> [Register]
devRegisters Device
dev ]

            insTy, outsTy :: Cry.Ty
            insTy :: Ty
insTy  = Len -> Ty -> Ty
Cry.TSeq Len
Cry.LenVar (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Size -> Ty
Cry.TBits Size
iw
            outsTy :: Ty
outsTy = Len -> Ty -> Ty
Cry.TSeq Len
Cry.LenVar (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Size -> Ty
Cry.TBits Size
ow

            inArm :: (Cry.Name, Cry.Exp)
            inArm :: (Text, Exp)
inArm | Size
iw Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0    = (Text
"i", Text -> Exp
Cry.Var Text
"ins")
                  | Bool
otherwise = (Text
"_", Text -> Exp
Cry.Var Text
"ins")

            out, nxt :: Cry.Exp -> Cry.Exp
            out :: Exp -> Exp
out = Size -> Size -> Size -> Exp -> Exp
Cry.slice (Size
ow Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
rsz) Size
0 Size
ow
            nxt :: Exp -> Exp
nxt = Size -> Size -> Size -> Exp -> Exp
Cry.slice (Size
ow Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
rsz) Size
ow Size
rsz

            comments :: [Text]
            comments :: [Text]
comments = [ Text
"Device: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Device -> Text
devName Device
dev
                       , Text
"Inputs, MSB-first: "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [(Text, Size)] -> Text
wires (Device -> [(Text, Size)]
devInputs Device
dev)
                       , Text
"Outputs, MSB-first: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [(Text, Size)] -> Text
wires (Device -> [(Text, Size)]
devOutputs Device
dev)
                       ]

            wires :: [(Name, Size)] -> Text
            wires :: [(Text, Size)] -> Text
wires = \ case
                  [] -> Text
"(none)"
                  [(Text, Size)]
ws -> Text -> [Text] -> Text
T.intercalate Text
", " ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Text) -> [(Text, Size)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Text
n, Size
s) -> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" : [" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Size -> Text
forall a. TextShow a => a -> Text
showt Size
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]") [(Text, Size)]
ws