{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-} -- Trustworthy, not Safe: invokes rwcry (the Cryptol translator).
-- | The Synolon-to-Hyle producer (the direct fold; doc/synolon.md §7): the
--   pure fragment translates per-construct (n-ary cases compile to
--   if-chains over constructor tags; joins are lifted to definitions
--   first), and each process folds to an explicit device: one definition
--   per block (cells threaded as trailing parameters), one dispatch
--   definition (an if-chain over the label tag), and register initials
--   obtained by evaluating the entry block with the Hyle interpreter.
--
--   The machine-step record reproduces the retired purifier's bit layout
--   exactly (so interpreter traces are unchanged): a step is
--   @halted | out | label-tag | pad | args | cells@, where the @halted@
--   bit is present only when a halt is reachable (the successor of the
--   PuRe constructor tag), the label field mirrors the generic ADT layout
--   of the retired @R_@ datatype (tag at the field's MSB, arguments
--   LSB-aligned), and a halt step carries the retired @A_@ encoding (one
--   tag per distinct answer type) in place of @out | label@.
module ReWire.Synolon.ToHyle (synolonToHyle) where

import ReWire.Annotation (Annote, noAnn, Annotated (ann), Provenance (..), Span (..), annProv)
import ReWire.BitVector (BV, bitVec, zeros, nbits)
import ReWire.Builtins (Builtin (..))
import ReWire.Config (Config, inputSigs, outputSigs, stateSigs, top, loadPath, stableNames)
import ReWire.Error (failAt, failAtWith, failInternal, warnAt, AstError, MonadError, Warning (..), relocatingTo)
import ReWire.Eidos.Pretty ()
import ReWire.Synolon.Syntax
import ReWire.Eidos.Naming (liftedJoinName, labelBase, defnBase, originTag)
import ReWire.Eidos.Subst (nextUniq, freeUniqs, occIds)
import ReWire.Eidos.Types (typeOf, flattenApp, flattenArrow, flattenTyApp, evalNat, natNorm, higherOrder, fundamental, reacOrStateT)
import ReWire.Hyle.Interp (evalExp, IEnv (..))
import ReWire.Hyle.Mangle (pickFresh, seedNames)
import ReWire.Hyle.Parse (parseHyleDefns)
import ReWire.Hyle.Transform (hoistInstances)
import ReWire.Pretty (showt, prettyPrint)
import ReWire.SYB (query)
import ReWire.Synolon.Repr (DataEnv (..), dataEnv, Sizes, sizeOfM, isTupleCon)

import Control.Lens ((^.))
import Control.Monad (unless, foldM)
import Control.Monad.Except (catchError)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.State.Strict (StateT (..), MonadState, State, runState, get, put, gets, modify)
import Data.Char (isAlphaNum)
import Data.Containers.ListUtils (nubOrd, nubOrdOn)
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.List (findIndex, genericLength, sortOn)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Text (Text)
import Numeric.Natural (Natural)
import System.Directory (doesFileExist, findExecutable)
import System.Environment (lookupEnv, getExecutablePath)
import System.Exit (ExitCode (..))
import System.FilePath (takeDirectory, isAbsolute, (</>))
import System.Process (readCreateProcessWithExitCode, proc)

import qualified Data.HashMap.Strict as Map
import qualified Data.HashSet        as Set
import qualified Data.IntMap.Strict  as IM
import qualified Data.IntSet         as IS
import qualified Data.Text           as T
import qualified ReWire.BitVector    as BV
import qualified ReWire.Hyle.Syntax  as A
import qualified ReWire.Annotation   as Ann

---
--- Monad and environments.
---

data Env = Env
      { Env -> DataEnv
envData    :: DataEnv                          -- ^ The datatype table (constructors in declaration order, and their signatures).
      , Env -> IntMap Text
envTops    :: IM.IntMap A.GId                  -- ^ Hyle names of the translated top-level definitions.
      , Env -> HashMap (Text, Text, Text) Text
envCry     :: HashMap (Text, Text, Text) A.GId -- ^ Hyle entry names of the compiled Cryptol foreign functions, by (module file, function, type key).
      }

data S = S
      { S -> Sizes
sSizes   :: !Sizes
      , S -> [Warning]
sWarns   :: ![Warning]
      , S -> Int
sCtr     :: !Int
      , S -> HashMap Text Extern
sExterns :: !(HashMap A.Name A.Extern)
      }

s0 :: S
s0 :: S
s0 = Sizes -> [Warning] -> Int -> HashMap Text Extern -> S
S Sizes
forall a. Monoid a => a
mempty [] Int
0 HashMap Text Extern
forall a. Monoid a => a
mempty

type TM m = StateT S m

addWarning :: MonadState S m => Annote -> Text -> m ()
addWarning :: forall (m :: * -> *). MonadState S m => Annote -> Text -> m ()
addWarning Annote
an Text
msg = (S -> S) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> m ()) -> (S -> S) -> m ()
forall a b. (a -> b) -> a -> b
$ \ S
s -> S
s { sWarns = sWarns s <> [Warning an msg] }

freshLocal :: MonadState S m => Text -> m A.Name
freshLocal :: forall (m :: * -> *). MonadState S m => Text -> m Text
freshLocal Text
pfx = do
      i <- (S -> Int) -> m Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> Int
sCtr
      modify $ \ S
s -> S
s { sCtr = i + 1 }
      pure $ pfx <> showt i

-- | Local scope: Eidos binder uniques map to Hyle atoms (a parameter or
--   let-bound name, or the case discriminant's atom for case binders).
data Scope = Scope
      { Scope -> IntMap Exp
scMap  :: !(IM.IntMap A.Exp)
      , Scope -> HashSet Text
scUsed :: !(HashSet A.Name)
      }

scope0 :: Scope
scope0 :: Scope
scope0 = IntMap Exp -> HashSet Text -> Scope
Scope IntMap Exp
forall a. Monoid a => a
mempty HashSet Text
forall a. Monoid a => a
mempty

-- | Bind a local to a readable Hyle name derived from its source name,
--   disambiguating collisions with a numeric suffix. Local names may
--   carry the compiler-owned @$@ prefix (machine binders marked by the
--   bridge, and the generated @$t@\/@$in@\/@$res@ names); the numeric
--   suffixing keeps all of them apart regardless of provenance.
bindLocal :: Annote -> Scope -> Id -> A.Size -> (Scope, A.Name)
bindLocal :: Annote -> Scope -> Id -> Size -> (Scope, Text)
bindLocal Annote
an Scope
sc Id
x Size
sz = Annote -> Scope -> Int -> Text -> Size -> (Scope, Text)
bindLocalText Annote
an Scope
sc (Id -> Int
idUniq Id
x) (Id -> Text
idOcc Id
x) Size
sz

bindLocalText :: Annote -> Scope -> Uniq -> Text -> A.Size -> (Scope, A.Name)
bindLocalText :: Annote -> Scope -> Int -> Text -> Size -> (Scope, Text)
bindLocalText Annote
an Scope
sc Int
u Text
base Size
sz = (Scope
sc', Text
nm)
      where nm :: Text
nm  = HashSet Text -> Text -> Int -> Text
pick (Scope -> HashSet Text
scUsed Scope
sc) Text
base (Int
0 :: Int)
            sc' :: Scope
sc' = IntMap Exp -> HashSet Text -> Scope
Scope (Int -> Exp -> IntMap Exp -> IntMap Exp
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
u (Annote -> Size -> Text -> Exp
A.Var Annote
an Size
sz Text
nm) (IntMap Exp -> IntMap Exp) -> IntMap Exp -> IntMap Exp
forall a b. (a -> b) -> a -> b
$ Scope -> IntMap Exp
scMap Scope
sc) (Text -> HashSet Text -> HashSet Text
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Text
nm (HashSet Text -> HashSet Text) -> HashSet Text -> HashSet Text
forall a b. (a -> b) -> a -> b
$ Scope -> HashSet Text
scUsed Scope
sc)

            pick :: HashSet A.Name -> Text -> Int -> A.Name
            pick :: HashSet Text -> Text -> Int -> Text
pick HashSet Text
used Text
b Int
i | Text
cand Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
used = HashSet Text -> Text -> Int -> Text
pick HashSet Text
used Text
b (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                          | Bool
otherwise              = Text
cand
                  where cand :: Text
cand = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Text
b else Text
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
i

-- | A fresh name in scope, not tied to a binder (cell values).
scopeName :: Scope -> Text -> (Scope, A.Name)
scopeName :: Scope -> Text -> (Scope, Text)
scopeName Scope
sc Text
base = (Scope
sc { scUsed = Set.insert nm $ scUsed sc }, Text
nm)
      where nm :: Text
nm = HashSet Text -> Text -> Int -> Text
pick (Scope -> HashSet Text
scUsed Scope
sc) Text
base (Int
0 :: Int)
            pick :: HashSet A.Name -> Text -> Int -> A.Name
            pick :: HashSet Text -> Text -> Int -> Text
pick HashSet Text
used Text
b Int
i | Text
cand Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
used = HashSet Text -> Text -> Int -> Text
pick HashSet Text
used Text
b (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                          | Bool
otherwise              = Text
cand
                  where cand :: Text
cand = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Text
b else Text
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
i

---
--- Lifting join points to occurrence-stably named definitions.
---

data LSt = LSt { LSt -> Int
lsSup :: !Uniq, LSt -> Int
lsOrd :: !Int, LSt -> [Defn]
lsNew :: ![Defn] }

liftJoins :: Program -> Program
liftJoins :: Program -> Program
liftJoins p :: Program
p@(Program [DataDefn]
datas [Defn]
defns [Proc]
procs) = [DataDefn] -> [Defn] -> [Proc] -> Program
Program [DataDefn]
datas [Defn]
defns' [Proc]
procs
      where tops :: IS.IntSet
            tops :: IntSet
tops = [Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Defn -> Int) -> [Defn] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Int
idUniq (Id -> Int) -> (Defn -> Id) -> Defn -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Id
defnId) [Defn]
defns

            -- Uniques at or above the initial supply are lifted
            -- definitions, not capturable locals.
            sup0 :: Uniq
            sup0 :: Int
sup0 = Program -> Int
forall a. Data a => a -> Int
nextUniq Program
p

            defns' :: [Defn]
            defns' :: [Defn]
defns' = ([Defn], Int) -> [Defn]
forall a b. (a, b) -> a
fst (([Defn], Int) -> [Defn]) -> ([Defn], Int) -> [Defn]
forall a b. (a -> b) -> a -> b
$ (([Defn], Int) -> Defn -> ([Defn], Int))
-> ([Defn], Int) -> [Defn] -> ([Defn], Int)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Defn], Int) -> Defn -> ([Defn], Int)
step ([], Int
sup0) [Defn]
defns

            step :: ([Defn], Uniq) -> Defn -> ([Defn], Uniq)
            step :: ([Defn], Int) -> Defn -> ([Defn], Int)
step ([Defn]
acc, Int
sup) Defn
d =
                  let (Exp
b', LSt
st) = State LSt Exp -> LSt -> (Exp, LSt)
forall s a. State s a -> s -> (a, s)
runState (Text -> Exp -> State LSt Exp
lj (Id -> Text
idOcc (Id -> Text) -> Id -> Text
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d) (Defn -> Exp
defnBody Defn
d)) (LSt -> (Exp, LSt)) -> LSt -> (Exp, LSt)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> [Defn] -> LSt
LSt Int
sup Int
1 []
                  in ([Defn]
acc [Defn] -> [Defn] -> [Defn]
forall a. Semigroup a => a -> a -> a
<> (Defn
d { defnBody = b' } Defn -> [Defn] -> [Defn]
forall a. a -> [a] -> [a]
: [Defn] -> [Defn]
forall a. [a] -> [a]
reverse (LSt -> [Defn]
lsNew LSt
st)), LSt -> Int
lsSup LSt
st)

            lj :: Text -> Exp -> State LSt Exp
            lj :: Text -> Exp -> State LSt Exp
lj Text
focc = Exp -> State LSt Exp
go
                  where go :: Exp -> State LSt Exp
                        go :: Exp -> State LSt Exp
go Exp
e = case Exp
e of
                              Let Annote
an (Join JoinId
j [Id]
ps Exp
b) Exp
body -> do
                                    b' <- Exp -> State LSt Exp
go Exp
b
                                    let capUs = (Int -> Bool) -> IntSet -> IntSet
IS.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sup0) (Exp -> IntSet
freeUniqs Exp
b' IntSet -> IntSet -> IntSet
IS.\\ IntSet
tops)
                                                      IntSet -> IntSet -> IntSet
IS.\\ [Int] -> IntSet
IS.fromList ((Id -> Int) -> [Id] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Int
idUniq [Id]
ps)
                                        caps  = (Int -> Maybe Id) -> [Int] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Int -> IntMap Id -> Maybe Id
forall a. Int -> IntMap a -> Maybe a
`IM.lookup` Exp -> IntMap Id
occIds Exp
b') ([Int] -> [Id]) -> [Int] -> [Id]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IS.toList IntSet
capUs
                                        t     = (Id -> Ty -> Ty) -> Ty -> [Id] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Annote -> Ty -> Ty -> Ty
Arrow Annote
an (Ty -> Ty -> Ty) -> (Id -> Ty) -> Id -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sig -> Ty
sigTy (Sig -> Ty) -> (Id -> Sig) -> Id -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Sig
idSig) (Exp -> Ty
typeOf Exp
b') ([Id] -> Ty) -> [Id] -> Ty
forall a b. (a -> b) -> a -> b
$ [Id]
caps [Id] -> [Id] -> [Id]
forall a. Semigroup a => a -> a -> a
<> [Id]
ps
                                    st <- get
                                    let u  = LSt -> Int
lsSup LSt
st
                                        i  = LSt -> Int
lsOrd LSt
st
                                        x  = Id { idOcc :: Text
idOcc  = Text -> Text -> Int -> Text
liftedJoinName Text
focc (Id -> Text
idOcc (Id -> Text) -> Id -> Text
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j) Int
i
                                                , idUniq :: Int
idUniq = Int
u
                                                , idSig :: Sig
idSig  = [TyVar] -> Ty -> Sig
Sig [] Ty
t
                                                }
                                    put st { lsSup = u + 1, lsOrd = i + 1
                                           , lsNew = Defn an x (caps <> ps) b' Nothing Nothing : lsNew st }
                                    go $ rejump (idUniq $ jpId j) x caps body
                              App Annote
an Exp
f Arg
a       -> Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Arg -> Exp)
-> State LSt Exp -> StateT LSt Identity (Arg -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
f StateT LSt Identity (Arg -> Exp)
-> StateT LSt Identity Arg -> State LSt Exp
forall a b.
StateT LSt Identity (a -> b)
-> StateT LSt Identity a -> StateT LSt Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg -> StateT LSt Identity Arg
goArg Arg
a
                              Lam Annote
an Id
x Exp
b       -> Annote -> Id -> Exp -> Exp
Lam Annote
an Id
x (Exp -> Exp) -> State LSt Exp -> State LSt Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
b
                              Let Annote
an Bind
b Exp
body    -> Annote -> Bind -> Exp -> Exp
Let Annote
an (Bind -> Exp -> Exp)
-> StateT LSt Identity Bind -> StateT LSt Identity (Exp -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bind -> StateT LSt Identity Bind
goBind Bind
b StateT LSt Identity (Exp -> Exp) -> State LSt Exp -> State LSt Exp
forall a b.
StateT LSt Identity (a -> b)
-> StateT LSt Identity a -> StateT LSt Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> State LSt Exp
go Exp
body
                              Jump Annote
an JoinId
j [Exp]
es     -> Annote -> JoinId -> [Exp] -> Exp
Jump Annote
an JoinId
j ([Exp] -> Exp) -> StateT LSt Identity [Exp] -> State LSt Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> State LSt Exp) -> [Exp] -> StateT LSt Identity [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 -> State LSt Exp
go [Exp]
es
                              Case Annote
an Ty
t Exp
s Id
cb [Alt]
alts -> do
                                    s'    <- Exp -> State LSt Exp
go Exp
s
                                    alts' <- mapM (\ (Alt Annote
aan AltCon
c [Id]
xs Exp
b) -> Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
aan AltCon
c [Id]
xs (Exp -> Alt) -> State LSt Exp -> StateT LSt Identity Alt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
b) alts
                                    pure $ Case an t s' cb alts'
                              LitList Annote
an Ty
t [Exp]
es  -> Annote -> Ty -> [Exp] -> Exp
LitList Annote
an Ty
t ([Exp] -> Exp) -> StateT LSt Identity [Exp] -> State LSt Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> State LSt Exp) -> [Exp] -> StateT LSt Identity [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 -> State LSt Exp
go [Exp]
es
                              LitVec Annote
an Ty
t [Exp]
es   -> Annote -> Ty -> [Exp] -> Exp
LitVec Annote
an Ty
t ([Exp] -> Exp) -> StateT LSt Identity [Exp] -> State LSt Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> State LSt Exp) -> [Exp] -> StateT LSt Identity [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 -> State LSt Exp
go [Exp]
es
                              Exp
_                -> Exp -> State LSt Exp
forall a. a -> StateT LSt Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

                        goArg :: Arg -> State LSt Arg
                        goArg :: Arg -> StateT LSt Identity Arg
goArg = \ case
                              EArg Exp
e -> Exp -> Arg
EArg (Exp -> Arg) -> State LSt Exp -> StateT LSt Identity Arg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
e
                              Arg
t      -> Arg -> StateT LSt Identity Arg
forall a. a -> StateT LSt Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Arg
t

                        goBind :: Bind -> State LSt Bind
                        goBind :: Bind -> StateT LSt Identity Bind
goBind = \ case
                              NonRec Id
x Exp
rhs -> Id -> Exp -> Bind
NonRec Id
x (Exp -> Bind) -> State LSt Exp -> StateT LSt Identity Bind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
rhs
                              Rec [(Id, Exp)]
bs       -> [(Id, Exp)] -> Bind
Rec ([(Id, Exp)] -> Bind)
-> StateT LSt Identity [(Id, Exp)] -> StateT LSt Identity Bind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Id, Exp) -> StateT LSt Identity (Id, Exp))
-> [(Id, Exp)] -> StateT LSt Identity [(Id, 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 (\ (Id
x, Exp
rhs) -> (Id
x, ) (Exp -> (Id, Exp))
-> State LSt Exp -> StateT LSt Identity (Id, Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
rhs) [(Id, Exp)]
bs
                              Join JoinId
j [Id]
ps Exp
b  -> JoinId -> [Id] -> Exp -> Bind
Join JoinId
j [Id]
ps (Exp -> Bind) -> State LSt Exp -> StateT LSt Identity Bind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> State LSt Exp
go Exp
b

            -- Rewrite every jump to the lifted join into a call, deeply
            -- (jumps to an outer join from a transitively-tail position
            -- sit inside nested join bindings' bodies too).
            rejump :: Uniq -> Id -> [Id] -> Exp -> Exp
            rejump :: Int -> Id -> [Id] -> Exp -> Exp
rejump Int
ju Id
x [Id]
caps = Exp -> Exp
go
                  where go :: Exp -> Exp
                        go :: Exp -> Exp
go Exp
e = case Exp
e of
                              Jump Annote
an JoinId
j [Exp]
es
                                    | Id -> Int
idUniq (JoinId -> Id
jpId JoinId
j) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ju ->
                                          (Exp -> Arg -> Exp) -> Exp -> [Arg] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Annote -> Exp -> Arg -> Exp
App Annote
an) (Annote -> Id -> Exp
Var Annote
an Id
x) ([Arg] -> Exp) -> [Arg] -> Exp
forall a b. (a -> b) -> a -> b
$ (Id -> Arg) -> [Id] -> [Arg]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> Arg
EArg (Exp -> Arg) -> (Id -> Exp) -> Id -> Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annote -> Id -> Exp
Var Annote
an) [Id]
caps [Arg] -> [Arg] -> [Arg]
forall a. Semigroup a => a -> a -> a
<> (Exp -> Arg) -> [Exp] -> [Arg]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> Arg
EArg (Exp -> Arg) -> (Exp -> Exp) -> Exp -> Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Exp
go) [Exp]
es
                                    | Bool
otherwise             -> Annote -> JoinId -> [Exp] -> Exp
Jump Annote
an JoinId
j ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              App Annote
an Exp
f Arg
a       -> Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Exp
go Exp
f) (Arg -> Exp) -> Arg -> Exp
forall a b. (a -> b) -> a -> b
$ Arg -> Arg
goArg Arg
a
                              Lam Annote
an Id
y Exp
b       -> Annote -> Id -> Exp -> Exp
Lam Annote
an Id
y (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
b
                              Let Annote
an Bind
b Exp
body    -> Annote -> Bind -> Exp -> Exp
Let Annote
an (Bind -> Bind
goBind Bind
b) (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
body
                              Case Annote
an Ty
t Exp
s Id
cb [Alt]
alts -> Annote -> Ty -> Exp -> Id -> [Alt] -> Exp
Case Annote
an Ty
t (Exp -> Exp
go Exp
s) Id
cb [ Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
aan AltCon
c [Id]
xs (Exp -> Exp
go Exp
b) | Alt Annote
aan AltCon
c [Id]
xs Exp
b <- [Alt]
alts ]
                              LitList Annote
an Ty
t [Exp]
es  -> Annote -> Ty -> [Exp] -> Exp
LitList Annote
an Ty
t ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              LitVec Annote
an Ty
t [Exp]
es   -> Annote -> Ty -> [Exp] -> Exp
LitVec Annote
an Ty
t ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              Exp
_                -> Exp
e

                        goArg :: Arg -> Arg
                        goArg :: Arg -> Arg
goArg = \ case
                              EArg Exp
e -> Exp -> Arg
EArg (Exp -> Arg) -> Exp -> Arg
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
e
                              Arg
t      -> Arg
t

                        goBind :: Bind -> Bind
                        goBind :: Bind -> Bind
goBind = \ case
                              NonRec Id
y Exp
rhs -> Id -> Exp -> Bind
NonRec Id
y (Exp -> Bind) -> Exp -> Bind
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
rhs
                              Rec [(Id, Exp)]
bs       -> [(Id, Exp)] -> Bind
Rec [ (Id
y, Exp -> Exp
go Exp
rhs) | (Id
y, Exp
rhs) <- [(Id, Exp)]
bs ]
                              Join JoinId
j [Id]
ps Exp
b  -> JoinId -> [Id] -> Exp -> Bind
Join JoinId
j [Id]
ps (Exp -> Bind) -> Exp -> Bind
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
b

---
--- Entry point.
---

synolonToHyle :: (MonadIO m, MonadError AstError m) => Config -> Program -> m A.Program
synolonToHyle :: forall (m :: * -> *).
(MonadIO m, MonadError AstError m) =>
Config -> Program -> m Program
synolonToHyle Config
conf Program
p0 = do
      let p1 :: Program
p1@(Program [DataDefn]
datas [Defn]
defns [Proc]
procs) = Program -> Program
liftJoins Program
p0
      pr <- case [Proc]
procs of
            [Proc
pr] -> Proc -> m Proc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proc
pr
            [Proc]
_    -> Annote -> Text -> m Proc
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
noAnn (Text -> m Proc) -> Text -> m Proc
forall a b. (a -> b) -> a -> b
$ Text
"expected exactly one process, got " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt ([Proc] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Proc]
procs)
      (cryMap, cryDefns) <- compileCryptols conf p1
      (p, s) <- flip runStateT s0 $ do
            let pures = (Defn -> Bool) -> [Defn] -> [Defn]
forall a. (a -> Bool) -> [a] -> [a]
filter Defn -> Bool
emit [Defn]
defns
                -- One global namespace (Hyle.Check enforces it over defns
                -- AND extern module names): the Cryptol fragments' names
                -- are baked into rwcry's output and extern names are the
                -- user's, so both seed the used map that pure-defn and
                -- block naming disambiguate against.
                (tops, used) = buildNameMap (seedNames $ map A.defnName cryDefns <> mapMaybe externName (query p1)) pures
                env   = Env { envData :: DataEnv
envData    = [DataDefn] -> DataEnv
dataEnv [DataDefn]
datas
                            , envTops :: IntMap Text
envTops    = IntMap Text
tops
                            , envCry :: HashMap (Text, Text, Text) Text
envCry     = HashMap (Text, Text, Text) Text
cryMap
                            }
            pureDefns <- mapM (transDefn env) pures
            transProc conf env used pr (pureDefns <> cryDefns)
      mapM_ (\ (Warning Annote
an Text
msg) -> Config -> Annote -> Text -> m ()
forall (m :: * -> *) an.
(MonadError AstError m, MonadIO m, Annotation an) =>
Config -> an -> Text -> m ()
warnAt Config
conf Annote
an Text
msg) $ nubOrd $ sWarns s
      pure p
      where -- Primitive-named definitions (undotted; the polymorphic prim
            -- carriers among them ride through the Eidos passes untranslated)
            -- and the reactive fragment (subsumed by the processes) don't
            -- lower.
            emit :: Defn -> Bool
            emit :: Defn -> Bool
emit Defn
d = Bool -> Bool
not (Text -> Bool
isPrim (Text -> Bool) -> Text -> Bool
forall a b. (a -> b) -> a -> b
$ Id -> Text
idOcc (Id -> Text) -> Id -> Text
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d)
                  Bool -> Bool -> Bool
&& [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Sig -> [TyVar]
sigTVs (Sig -> [TyVar]) -> Sig -> [TyVar]
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig (Id -> Sig) -> Id -> Sig
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d)
                  Bool -> Bool -> Bool
&& Bool -> Bool
not (Ty -> Bool
reacOrStateT (Ty -> Bool) -> Ty -> Bool
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig (Id -> Sig) -> Id -> Sig
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d)

            isPrim :: Text -> Bool
            isPrim :: Text -> Bool
isPrim = (Char -> Bool) -> Text -> Bool
T.all (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.')

            -- | The module name of a (saturated, post-inlining) extern
            --   use: the sixth value argument, mirroring transBuiltin's
            --   Extern case.
            externName :: Exp -> Maybe Text
            externName :: Exp -> Maybe Text
externName Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
_ Ty
_ Builtin
Extern, [Arg]
args) | (Exp
_ : Exp
_ : Exp
_ : Exp
_ : Exp
_ : LitStr Annote
_ Text
s : [Exp]
_) <- [ Exp
x | EArg Exp
x <- [Arg]
args ] -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
s
                  (Exp, [Arg])
_                                                                                        -> Maybe Text
forall a. Maybe a
Nothing

---
--- Cryptol foreign functions.
---

-- | Compile every Cryptol foreign function the program uses -- one Hyle
--   definition set per distinct (module file, function, type)
--   instantiation -- by invoking the out-of-process translator (rwcry),
--   which loads and typechecks the Cryptol module, checks the use-site
--   type against the function's Cryptol type scheme, and emits a
--   self-contained Hyle fragment. Returns the entry names for the fold
--   ('transBuiltin''s Cryptol case, which is pure -- all the IO happens
--   here, before the fold) and the generated definitions.
compileCryptols :: forall m. (MonadIO m, MonadError AstError m) => Config -> Program -> m (HashMap (Text, Text, Text) A.GId, [A.Defn])
compileCryptols :: forall (m :: * -> *).
(MonadIO m, MonadError AstError m) =>
Config -> Program -> m (HashMap (Text, Text, Text) Text, [Defn])
compileCryptols Config
conf Program
p = case [(Annote, Text, Text, Ty)]
uses of
      []                 -> (HashMap (Text, Text, Text) Text, [Defn])
-> m (HashMap (Text, Text, Text) Text, [Defn])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HashMap (Text, Text, Text) Text
forall a. Monoid a => a
mempty, [])
      (Annote
an0, Text
_, Text
_, Ty
_) : [(Annote, Text, Text, Ty)]
_ -> do
            rwcry <- IO (Maybe String) -> m (Maybe String)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Maybe String)
findRwcry m (Maybe String) -> (Maybe String -> m String) -> m String
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m String -> (String -> m String) -> Maybe String -> m String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> m String
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an0 Text
missingRwcry) String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            foldM (step rwcry) (mempty, []) uses
      where -- One fragment per distinct instantiation, in a canonical order
            -- (by module file, function, and type) rather than the order of
            -- discovery, so that the emitted definitions do not move when
            -- unrelated code around a use changes.
            uses :: [(Annote, Text, Text, Ty)]
            uses :: [(Annote, Text, Text, Ty)]
uses = ((Annote, Text, Text, Ty) -> (Text, Text, Text))
-> [(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Annote, Text, Text, Ty) -> (Text, Text, Text)
key ([(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)])
-> [(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)]
forall a b. (a -> b) -> a -> b
$ ((Annote, Text, Text, Ty) -> (Text, Text, Text))
-> [(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (Annote, Text, Text, Ty) -> (Text, Text, Text)
key ([(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)])
-> [(Annote, Text, Text, Ty)] -> [(Annote, Text, Text, Ty)]
forall a b. (a -> b) -> a -> b
$ (Exp -> Maybe (Annote, Text, Text, Ty))
-> [Exp] -> [(Annote, Text, Text, Ty)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Exp -> Maybe (Annote, Text, Text, Ty)
cryUse ([Exp] -> [(Annote, Text, Text, Ty)])
-> [Exp] -> [(Annote, Text, Text, Ty)]
forall a b. (a -> b) -> a -> b
$ Program -> [Exp]
forall a b. (Data a, Data b) => a -> [b]
query Program
p

            key :: (Annote, Text, Text, Ty) -> (Text, Text, Text)
            key :: (Annote, Text, Text, Ty) -> (Text, Text, Text)
key (Annote
_, Text
f, Text
n, Ty
t) = (Text
f, Text
n, Ty -> Text
tyKey Ty
t)

            step :: FilePath -> (HashMap (Text, Text, Text) A.GId, [A.Defn]) -> (Annote, Text, Text, Ty) -> m (HashMap (Text, Text, Text) A.GId, [A.Defn])
            step :: String
-> (HashMap (Text, Text, Text) Text, [Defn])
-> (Annote, Text, Text, Ty)
-> m (HashMap (Text, Text, Text) Text, [Defn])
step String
rwcry (HashMap (Text, Text, Text) Text
memo, [Defn]
ds) (Annote
an, Text
f, Text
n, Ty
t) = do
                  path <- Annote -> Text -> m String
resolveCry Annote
an Text
f
                  cty  <- either (\ Text
e -> Annote -> Text -> m Text
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m Text) -> Text -> m Text
forall a b. (a -> b) -> a -> b
$ Text
"cryptol: unsupported type at a Cryptol foreign function: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e) pure $ cryTy t
                  -- The entry name carries the instantiation's monotype
                  -- ('cry$grev$8_8'), not a discovery counter, so adding
                  -- an unrelated instantiation doesn't rename this one.
                  -- Entry names are baked into rwcry's output and can't be
                  -- disambiguated later; dodge already-issued ones here.
                  let base  = Text
"cry$" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
sanitize Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"$" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
originTag [Text
cty]
                      taken = [Text] -> HashSet Text
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList ([Text] -> HashSet Text) -> [Text] -> HashSet Text
forall a b. (a -> b) -> a -> b
$ HashMap (Text, Text, Text) Text -> [Text]
forall k v. HashMap k v -> [v]
Map.elems HashMap (Text, Text, Text) Text
memo
                      entry = HashSet Text -> Text -> Text
dodge HashSet Text
taken Text
base
                  (ec, out, err) <- liftIO $ readCreateProcessWithExitCode (proc rwcry [path, T.unpack n, T.unpack cty, T.unpack entry]) ""
                  case ec of
                        ExitCode
ExitSuccess   -> do
                              -- rwcry writes any compile-time warnings to
                              -- stderr, one per "warning: " line; surface
                              -- them through rwc's warning machinery.
                              (Text -> m ()) -> [Text] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Config -> Annote -> Text -> m ()
forall (m :: * -> *) an.
(MonadError AstError m, MonadIO m, Annotation an) =>
Config -> an -> Text -> m ()
warnAt Config
conf Annote
an) [ Text
w | Text
l <- Text -> [Text]
T.lines (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
err, Just Text
w <- [Text -> Text -> Maybe Text
T.stripPrefix Text
"warning: " Text
l] ]
                              ds' <- Text -> String -> m [Defn]
forall (m :: * -> *).
MonadError AstError m =>
Text -> String -> m [Defn]
parseHyleDefns (String -> Text
T.pack String
out) String
path
                              -- The fragment's entry point gets a doc line
                              -- recording the foreign function it compiles.
                              let entryDoc = Text
"cryptol " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"::" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" at " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cty
                                  ds''     = [ if Defn -> Text
A.defnName Defn
d Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
entry then Defn
d { A.defnDoc = A.Blind [entryDoc] } else Defn
d | Defn
d <- [Defn]
ds' ]
                              pure (Map.insert (f, n, tyKey t) entry memo, ds <> ds'')
                        ExitFailure Int
_ -> Annote -> Text -> m (HashMap (Text, Text, Text) Text, [Defn])
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m (HashMap (Text, Text, Text) Text, [Defn]))
-> Text -> m (HashMap (Text, Text, Text) Text, [Defn])
forall a b. (a -> b) -> a -> b
$ case Text -> Text
T.strip (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
err of
                              Text
"" -> Text
"cryptol: the translator (rwcry) failed without a diagnostic."
                              Text
e  -> Text
e

            -- The module file, resolved against the call site's directory,
            -- then the loadpath.
            resolveCry :: Annote -> Text -> m FilePath
            resolveCry :: Annote -> Text -> m String
resolveCry Annote
an Text
f = [String] -> m (Maybe String)
firstExisting [String]
cands m (Maybe String) -> (Maybe String -> m String) -> m String
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                  Just String
p' -> String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
p'
                  Maybe String
Nothing -> Annote -> Text -> m String
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m String) -> Text -> m String
forall a b. (a -> b) -> a -> b
$ Text
"cryptol: module file not found: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
f
                  where fp :: String
fp    = Text -> String
T.unpack Text
f
                        cands :: [String]
cands | String -> Bool
isAbsolute String
fp = [String
fp]
                              | Bool
otherwise     = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
</> String
fp) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> [String]) -> (String -> String) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeDirectory) (Annote -> Maybe String
anFile Annote
an) [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> Config
confConfig -> Getting [String] Config [String] -> [String]
forall s a. s -> Getting a s a -> a
^.Getting [String] Config [String]
Lens' Config [String]
loadPath [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"."]

            firstExisting :: [FilePath] -> m (Maybe FilePath)
            firstExisting :: [String] -> m (Maybe String)
firstExisting = \ case
                  []       -> Maybe String -> m (Maybe String)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
                  String
c : [String]
rest -> IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO Bool
doesFileExist String
c) m Bool -> (Bool -> m (Maybe String)) -> m (Maybe String)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Bool
ok ->
                        if Bool
ok then Maybe String -> m (Maybe String)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
c) else [String] -> m (Maybe String)
firstExisting [String]
rest

            anFile :: Annote -> Maybe FilePath
            anFile :: Annote -> Maybe String
anFile Annote
a = case Annote -> Provenance
annProv Annote
a of
                  FromSource Span
sp          -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Span -> String
spanFile Span
sp
                  Synthesized Text
_ (Span
sp : [Span]
_) -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Span -> String
spanFile Span
sp
                  Provenance
_                      -> Maybe String
forall a. Maybe a
Nothing

            -- RWC_RWCRY, then next to the rwc executable, then the PATH.
            findRwcry :: IO (Maybe FilePath)
            findRwcry :: IO (Maybe String)
findRwcry = String -> IO (Maybe String)
lookupEnv String
"RWC_RWCRY" IO (Maybe String)
-> (Maybe String -> IO (Maybe String)) -> IO (Maybe String)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
                  Just String
r  -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe String -> IO (Maybe String))
-> Maybe String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
r
                  Maybe String
Nothing -> do
                        cand <- (String -> String -> String
</> String
"rwcry") (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeDirectory (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
getExecutablePath
                        doesFileExist cand >>= \ case
                              Bool
True  -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe String -> IO (Maybe String))
-> Maybe String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
cand
                              Bool
False -> String -> IO (Maybe String)
findExecutable String
"rwcry"

            missingRwcry :: Text
            missingRwcry :: Text
missingRwcry = Text
"cryptol: the Cryptol translator (rwcry) was not found next to rwc or on the PATH; it is built and installed along with rwc (or set RWC_RWCRY to its location)."

            sanitize :: Text -> Text
            sanitize :: Text -> Text
sanitize = (Char -> Char) -> Text -> Text
T.map (\ Char
c -> if Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String
"_.$'" :: String) then Char
c else Char
'.')

            dodge :: HashSet A.GId -> Text -> Text
            dodge :: HashSet Text -> Text -> Text
dodge HashSet Text
taken Text
base = [Text] -> Text
go ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text
base Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [ Text
base Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"$" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
k | Int
k <- [Int
2 :: Int ..] ]
                  where go :: [Text] -> Text
                        go :: [Text] -> Text
go = \ case
                              Text
c : [Text]
cs | Text
c Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
taken -> [Text] -> Text
go [Text]
cs
                                     | Bool
otherwise            -> Text
c
                              []                            -> Text
base -- unreachable: the candidate list is infinite

-- | A saturated Cryptol foreign-function application: the module file and
--   function name (literals, after inlining), and the use-site type, read
--   off the implementation argument (which the neutering pass reduced to
--   a placeholder of the same type). The annote is the file literal's --
--   the prim occurrence's annote points into the inlined rewire-user
--   wrapper, while the literal is the user's.
cryUse :: Exp -> Maybe (Annote, Text, Text, Ty)
cryUse :: Exp -> Maybe (Annote, Text, Text, Ty)
cryUse Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
      (Prim Annote
_ Ty
_ Builtin
Cryptol, [Arg]
args) | fl :: Exp
fl@(LitStr Annote
_ Text
f) : LitStr Annote
_ Text
n : Exp
impl : [Exp]
_ <- [ Exp
x | EArg Exp
x <- [Arg]
args ] -> (Annote, Text, Text, Ty) -> Maybe (Annote, Text, Text, Ty)
forall a. a -> Maybe a
Just (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
fl, Text
f, Text
n, Exp -> Ty
typeOf Exp
impl)
      (Exp, [Arg])
_                                                                                            -> Maybe (Annote, Text, Text, Ty)
forall a. Maybe a
Nothing

-- | The memo key for a type: pretty-printed, annotations scrubbed.
tyKey :: Ty -> Text
tyKey :: Ty -> Text
tyKey = Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Text) -> (Ty -> Ty) -> Ty -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn :: Ty -> Ty)

-- | Render a monomorphic Eidos type as Cryptol type text, for the
--   instantiation check on the Cryptol side; the inverse of the
--   correspondence in doc/hyle.md, section 8.4. The supported fragment:
--   Bool, bit vectors, vectors, tuples, and first-order arrows.
cryTy :: Ty -> Either Text Text
cryTy :: Ty -> Either Text Text
cryTy Ty
t = case Ty -> ([Ty], Ty)
flattenArrow Ty
t of
      ([], Ty
tr) -> Ty -> Either Text Text
go Ty
tr
      ([Ty]
ts, Ty
tr) -> do
            ts' <- (Ty -> Either Text Text) -> [Ty] -> Either Text [Text]
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 Ty -> Either Text Text
go [Ty]
ts
            tr' <- go tr
            pure $ T.intercalate " -> " $ ts' <> [tr']
      where go :: Ty -> Either Text Text
            go :: Ty -> Either Text Text
go Ty
t' | (Ty
_ : [Ty]
_, Ty
_) <- Ty -> ([Ty], Ty)
flattenArrow Ty
t' = Text -> Either Text Text
forall a b. a -> Either a b
Left Text
"a function-typed component cannot cross the Cryptol boundary"
                  | Bool
otherwise = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t' of
                        (TyCon Annote
_ Text
"Bool", [])     -> Text -> Either Text Text
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"Bit"
                        (TyCon Annote
_ Text
"Vec", [Ty
n, Ty
te])
                              | Just Natural
k <- Ty -> Maybe Natural
evalNat Ty
n -> do
                                    te' <- Ty -> Either Text Text
go Ty
te
                                    pure $ "[" <> showt k <> "]" <> (if te' == "Bit" then "" else "(" <> te' <> ")")
                        (TyCon Annote
_ Text
c, [Ty]
args)
                              | Text -> Bool
isTupleCon Text
c, Bool -> Bool
not ([Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
args) -> do
                                    args' <- (Ty -> Either Text Text) -> [Ty] -> Either Text [Text]
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 Ty -> Either Text Text
go [Ty]
args
                                    pure $ "(" <> T.intercalate ", " args' <> ")"
                              | Text
c Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"()", [Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
args          -> Text -> Either Text Text
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"()"
                        (Ty, [Ty])
_                        -> Text -> Either Text Text
forall a b. a -> Either a b
Left (Text -> Either Text Text) -> Text -> Either Text Text
forall a b. (a -> b) -> a -> b
$ Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn Ty
t' :: Ty)

-- | Hyle names for the top-level definitions: the occurrence's display
--   base (lifted-definition markers stripped), disambiguated by a numeric
--   suffix in definition order against every name already claimed (the
--   incoming used map carries names that are not ours to move, e.g. the
--   entries and helpers of rwcry-generated Cryptol fragments). Returns
--   the extended used map so the machine fold can name blocks against the
--   same namespace (Hyle global names are program-unique).
buildNameMap :: HashMap Text Int -> [Defn] -> (IM.IntMap A.GId, HashMap Text Int)
buildNameMap :: HashMap Text Int -> [Defn] -> (IntMap Text, HashMap Text Int)
buildNameMap HashMap Text Int
used0 = ((IntMap Text, HashMap Text Int)
 -> Defn -> (IntMap Text, HashMap Text Int))
-> (IntMap Text, HashMap Text Int)
-> [Defn]
-> (IntMap Text, HashMap Text Int)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (IntMap Text, HashMap Text Int)
-> Defn -> (IntMap Text, HashMap Text Int)
step (IntMap Text
forall a. Monoid a => a
mempty, HashMap Text Int
used0)
      where step :: (IM.IntMap A.GId, HashMap Text Int) -> Defn -> (IM.IntMap A.GId, HashMap Text Int)
            step :: (IntMap Text, HashMap Text Int)
-> Defn -> (IntMap Text, HashMap Text Int)
step (IntMap Text
m, HashMap Text Int
used) Defn
d =
                  let (Text
nm, HashMap Text Int
used') = Text -> HashMap Text Int -> Text -> (Text, HashMap Text Int)
pickFresh Text
"" HashMap Text Int
used (Text -> (Text, HashMap Text Int))
-> Text -> (Text, HashMap Text Int)
forall a b. (a -> b) -> a -> b
$ Text -> Text
defnBase (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Id -> Text
idOcc (Id -> Text) -> Id -> Text
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d
                  in (Int -> Text -> IntMap Text -> IntMap Text
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (Id -> Int
idUniq (Id -> Int) -> Id -> Int
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d) Text
nm IntMap Text
m, HashMap Text Int
used')

globalName :: MonadError AstError m => Env -> Annote -> Id -> TM m A.GId
globalName :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> TM m Text
globalName Env
env Annote
an Id
x = TM m Text -> (Text -> TM m Text) -> Maybe Text -> TM m Text
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Text
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> TM m Text) -> Text -> TM m Text
forall a b. (a -> b) -> a -> b
$ Text
"unknown global: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
x) Text -> TM m Text
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      (Maybe Text -> TM m Text) -> Maybe Text -> TM m Text
forall a b. (a -> b) -> a -> b
$ Int -> IntMap Text -> Maybe Text
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Id -> Int
idUniq Id
x) (IntMap Text -> Maybe Text) -> IntMap Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Env -> IntMap Text
envTops Env
env

---
--- Type sizing.
---

intTy :: Ty
intTy :: Ty
intTy = Annote -> Text -> Ty
TyCon Annote
noAnn Text
"Integer"

-- | The width of a type ("ReWire.Synolon.Repr", memoized in 'sSizes'; the
--   Synolon lint has already rejected a binder, block parameter, cell,
--   port, or halt answer whose type has none — a definition's codomain or
--   an expression's instantiation is sized only here). The label names
--   the position in the diagnostic.
sizeOf :: MonadError AstError m => Env -> Text -> Annote -> Ty -> TM m A.Size
sizeOf :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
s Annote
an Ty
t = do
      m <- (S -> Sizes) -> StateT S m Sizes
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> Sizes
sSizes
      case runStateT (sizeOfM (envData env) t) m of
            Left Text
e         -> Annote -> Text -> StateT S m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> StateT S m Size) -> Text -> StateT S m Size
forall a b. (a -> b) -> a -> b
$ Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e
            Right (Natural
sz, Sizes
m') -> do
                  (S -> S) -> StateT S m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S m ()) -> (S -> S) -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ \ S
st -> S
st { sSizes = m' }
                  Size -> StateT S m Size
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> StateT S m Size) -> Size -> StateT S m Size
forall a b. (a -> b) -> a -> b
$ Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
sz

-- | The tag value and width of a constructor of the given (concrete) type.
ctorTag :: MonadError AstError m => Env -> Annote -> Ty -> DataConId -> TM m (A.Value, A.Size)
ctorTag :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Text -> TM m (Integer, Size)
ctorTag Env
env Annote
an Ty
t Text
d = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
      (TyCon Annote
_ Text
c, [Ty]
_)
            | Text -> Bool
isTupleCon Text
c -> (Integer, Size) -> TM m (Integer, Size)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
0, Size
0)
            | Just [Text]
ctors <- Text -> HashMap Text [Text] -> Maybe [Text]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
c (DataEnv -> HashMap Text [Text]
deCtors (DataEnv -> HashMap Text [Text]) -> DataEnv -> HashMap Text [Text]
forall a b. (a -> b) -> a -> b
$ Env -> DataEnv
envData Env
env) -> case (Text -> Bool) -> [Text] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
d) [Text]
ctors of
                  Just Int
idx -> (Integer, Size) -> TM m (Integer, Size)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
idx, Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Size) -> Natural -> Size
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
nbits (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ [Text] -> Natural
forall i a. Num i => [a] -> i
genericLength [Text]
ctors)
                  Maybe Int
Nothing  -> Annote -> Text -> TM m (Integer, Size)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> TM m (Integer, Size)) -> Text -> TM m (Integer, Size)
forall a b. (a -> b) -> a -> b
$ Text
"ctorTag: unknown ctor: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
d Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" of type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c
      (Ty, [Ty])
_ -> Annote -> Text -> TM m (Integer, Size)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> TM m (Integer, Size)) -> Text -> TM m (Integer, Size)
forall a b. (a -> b) -> a -> b
$ Text
"ctorTag: unexpected type: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn Ty
t)

wireOffsets :: [(a, A.Size)] -> [(a, A.Size, A.Index)]
wireOffsets :: forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets = (Size, [(a, Size, Size)]) -> [(a, Size, Size)]
forall a b. (a, b) -> b
snd ((Size, [(a, Size, Size)]) -> [(a, Size, Size)])
-> ([(a, Size)] -> (Size, [(a, Size, Size)]))
-> [(a, Size)]
-> [(a, Size, Size)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Size)
 -> (Size, [(a, Size, Size)]) -> (Size, [(a, Size, Size)]))
-> (Size, [(a, Size, Size)])
-> [(a, Size)]
-> (Size, [(a, Size, Size)])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, Size) -> (Size, [(a, Size, Size)]) -> (Size, [(a, Size, Size)])
forall {b} {c} {a}.
(Integral b, Num c) =>
(a, b) -> (c, [(a, b, c)]) -> (c, [(a, b, c)])
step (Size
0, [])
      where step :: (a, b) -> (c, [(a, b, c)]) -> (c, [(a, b, c)])
step (a
x, b
sz) (c
off, [(a, b, c)]
acc) = (c
off c -> c -> c
forall a. Num a => a -> a -> a
+ b -> c
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
sz, (a
x, b
sz, c
off) (a, b, c) -> [(a, b, c)] -> [(a, b, c)]
forall a. a -> [a] -> [a]
: [(a, b, c)]
acc)

slice0 :: Annote -> A.Index -> A.Size -> A.Exp -> A.Exp
slice0 :: Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an Size
off Size
sz Exp
e | Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0   = Annote -> BV -> Exp
A.Lit Annote
an BV
BV.nil
                   | Bool
otherwise = Annote -> Size -> Size -> Exp -> Exp
A.Slice Annote
an Size
off Size
sz Exp
e

---
--- Pure definitions.
---

transDefn :: MonadError AstError m => Env -> Defn -> TM m A.Defn
transDefn :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Defn -> TM m Defn
transDefn Env
env d :: Defn
d@(Defn Annote
an Id
did [Id]
_ Exp
_ Maybe DefnAttr
_ Maybe SpecOrigin
_) = do
      let t :: Ty
t   = Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
did
          occ :: Text
occ = Id -> Text
idOcc Id
did
      if | Ty -> Bool
higherOrder Ty
t     -> Annote -> Text -> TM m Defn
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> TM m Defn) -> Text -> TM m Defn
forall a b. (a -> b) -> a -> b
$ Text
occ Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" has unsupported higher-order type."
         | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ty -> Bool
fundamental Ty
t -> Annote -> Text -> TM m Defn
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> TM m Defn) -> Text -> TM m Defn
forall a b. (a -> b) -> a -> b
$ Text
occ Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" has un-translatable String or Integer arguments."
         | Bool
otherwise         -> do
               (S -> S) -> StateT S m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S m ()) -> (S -> S) -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ \ S
s -> S
s { sCtr = 0 }
               n' <- Env -> Annote -> Id -> TM m Text
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> TM m Text
globalName Env
env Annote
an Id
did
               let (ps0, body0)  = (defnParams d, defnBody d)
                   (ps1, body1)  = peelLams body0
                   ps            = [Id]
ps0 [Id] -> [Id] -> [Id]
forall a. Semigroup a => a -> a -> a
<> [Id]
ps1
                   (ptys, codTy) = flattenArrow t
               -- Eta-expand an unsaturated definition (a definition whose
               -- body returns a function can't lower to a sized result).
               (ps', body') <- etaExpand an (length ps) (drop (length ps) ptys) ps body1
               ptSzs <- mapM (sizeOf env "transDefn param" an) $ take (length ps') ptys
               codSz <- sizeOf env "transDefn codomain" an codTy
               let sig = Annote -> [Size] -> Size -> Sig
A.Sig Annote
an [Size]
ptSzs Size
codSz
               (sc, pnames) <- pure $ bindParams an scope0 (zip ps' ptSzs)
               body'' <- relocatingTo an $ transExp env sc body'
               pure $ A.Defn an n' sig pnames body'' (defnAttr d == Just NoInline) (A.Blind $ originDoc $ defnOrigin d)
      where -- | Provenance of compiler-minted clones, rendered as doc lines.
            originDoc :: Maybe SpecOrigin -> [Text]
            originDoc :: Maybe SpecOrigin -> [Text]
originDoc = \ case
                  Just (SpecOrigin Text
f [Ty]
ts) -> [ Text
"specialized from '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"'"
                                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if [Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
ts then Text
"" else Text
" at " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " ((Ty -> Text) -> [Ty] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Text
tyKey [Ty]
ts)) ]
                  Just (BakeOrigin Text
f)    -> [ Text
"partially applied from '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"'" ]
                  Maybe SpecOrigin
Nothing                -> []

            peelLams :: Exp -> ([Id], Exp)
            peelLams :: Exp -> ([Id], Exp)
peelLams = \ case
                  Lam Annote
_ Id
x Exp
b -> let ([Id]
xs, Exp
b') = Exp -> ([Id], Exp)
peelLams Exp
b in (Id
x Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
xs, Exp
b')
                  Exp
e         -> ([], Exp
e)

            etaExpand :: MonadError AstError m => Annote -> Int -> [Ty] -> [Id] -> Exp -> TM m ([Id], Exp)
            etaExpand :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> Int -> [Ty] -> [Id] -> Exp -> TM m ([Id], Exp)
etaExpand Annote
_ Int
_ [] [Id]
ps Exp
b = ([Id], Exp) -> StateT S m ([Id], Exp)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Id]
ps, Exp
b)
            etaExpand Annote
an' Int
n [Ty]
missing [Id]
ps Exp
b = do
                  let extras :: [Id]
extras = [ Text -> Int -> Sig -> Id
Id (Text
"$eta" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
i) (- (Id -> Int
idUniq (Defn -> Id
defnId Defn
d) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)) (Ty -> Sig
monoSig Ty
ty)
                               | (Int
i, Ty
ty) <- [Int] -> [Ty] -> [(Int, Ty)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Ty]
missing ]
                  ([Id], Exp) -> StateT S m ([Id], Exp)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Id]
ps [Id] -> [Id] -> [Id]
forall a. Semigroup a => a -> a -> a
<> [Id]
extras, (Exp -> Id -> Exp) -> Exp -> [Id] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ Exp
acc Id
x -> Annote -> Exp -> Arg -> Exp
App Annote
an' Exp
acc (Exp -> Arg
EArg (Exp -> Arg) -> Exp -> Arg
forall a b. (a -> b) -> a -> b
$ Annote -> Id -> Exp
Var Annote
an' Id
x)) Exp
b [Id]
extras)
                  where Int
_ = Int
n

bindParams :: Annote -> Scope -> [(Id, A.Size)] -> (Scope, [A.Name])
bindParams :: Annote -> Scope -> [(Id, Size)] -> (Scope, [Text])
bindParams Annote
an = Scope -> [(Id, Size)] -> (Scope, [Text])
go
      where go :: Scope -> [(Id, Size)] -> (Scope, [Text])
go Scope
sc = \ case
                  []             -> (Scope
sc, [])
                  (Id
x, Size
sz) : [(Id, Size)]
rest -> let (Scope
sc', Text
nm)   = Annote -> Scope -> Id -> Size -> (Scope, Text)
bindLocal Annote
an Scope
sc Id
x Size
sz
                                        (Scope
sc'', [Text]
nms) = Scope -> [(Id, Size)] -> (Scope, [Text])
go Scope
sc' [(Id, Size)]
rest
                                    in (Scope
sc'', Text
nm Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
nms)

---
--- Expression translation.
---

-- | Names an expression unless it is already atomic.
bindAtom :: MonadState S m => Annote -> A.Exp -> (A.Exp -> m A.Exp) -> m A.Exp
bindAtom :: forall (m :: * -> *).
MonadState S m =>
Annote -> Exp -> (Exp -> m Exp) -> m Exp
bindAtom Annote
an Exp
e Exp -> m Exp
k = case Exp
e of
      A.Lit {} -> Exp -> m Exp
k Exp
e
      A.Var {} -> Exp -> m Exp
k Exp
e
      Exp
_        -> do
            x  <- Text -> m Text
forall (m :: * -> *). MonadState S m => Text -> m Text
freshLocal Text
"$t"
            e' <- k $ A.Var an (A.sizeOf e) x
            pure $ A.Let an (A.sizeOf e') x e e'

conj :: Annote -> [A.Exp] -> A.Exp
conj :: Annote -> [Exp] -> Exp
conj Annote
an = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((Exp -> Exp -> Exp) -> [Exp] -> Exp)
-> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a Exp
b -> Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.And [Exp
a, Exp
b]

transExp :: MonadError AstError m => Env -> Scope -> Exp -> TM m A.Exp
transExp :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
e = case Exp
e of
      App {} -> case Exp -> (Exp, [Arg])
flattenApp Exp
e of
            (Prim Annote
an' Ty
_ Builtin
b, [Arg]
args)      -> Env
-> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env
-> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m Exp
transBuiltin Env
env Scope
sc (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) (Exp -> Ty
typeOf Exp
e) Annote
an' (Builtin
b, [ Exp
a | EArg Exp
a <- [Arg]
args ])
            (Con Annote
an' Ty
_ Text
d, [Arg]
args)       -> do
                  args'      <- (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [ Exp
a | EArg Exp
a <- [Arg]
args ]
                  (v, w)     <- ctorTag env an' (typeOf e) d
                  (tag, pad) <- ctorRep an' (typeOf e) (v, w) $ sum $ map A.sizeOf args'
                  pure $ A.cat ([A.Lit an' tag, A.Lit an' pad] <> args')
            (Var Annote
an' Id
x, [Arg]
args)         -> do
                  let eargs :: [Exp]
eargs = [ Exp
a | EArg Exp
a <- [Arg]
args ]
                  sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env (Text
"applied Var " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
x) Annote
an' (Ty -> TM m Size) -> Ty -> TM m Size
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
e
                  case IM.lookup (idUniq x) $ scMap sc of
                        Just Exp
_  -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' (Text -> TM m Exp) -> Text -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unsupported application of a local variable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
x
                        Maybe Exp
Nothing -> Annote -> Size -> Text -> [Exp] -> Exp
A.Call Annote
an' Size
sz (Text -> [Exp] -> Exp)
-> StateT S m Text -> StateT S m ([Exp] -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Annote -> Id -> StateT S m Text
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> TM m Text
globalName Env
env Annote
an' Id
x StateT S m ([Exp] -> Exp) -> StateT S m [Exp] -> TM m Exp
forall a b. StateT S m (a -> b) -> StateT S m a -> StateT S m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [Exp]
eargs
            (Lam Annote
an' Id
p Exp
b, EArg Exp
a : [Arg]
rest) ->
                  Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Bind -> Exp -> Exp
Let Annote
an' (Id -> Exp -> Bind
NonRec Id
p Exp
a) (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Arg -> Exp) -> Exp -> [Arg] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Annote -> Exp -> Arg -> Exp
App Annote
an') Exp
b [Arg]
rest
            -- A let-headed application: hoist the application inside (the
            -- arguments predate the binder, so this is scope-safe).
            (Let Annote
lan Bind
bnd Exp
lbody, [Arg]
args)  ->
                  Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Bind -> Exp -> Exp
Let Annote
lan Bind
bnd (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Arg -> Exp) -> Exp -> [Arg] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Annote -> Exp -> Arg -> Exp
App Annote
lan) Exp
lbody [Arg]
args
            -- A case-headed application: commute into the arms (the
            -- arguments predate the alternative binders).
            (Case Annote
can Ty
_ Exp
cd Id
ccb [Alt]
calts, [Arg]
args) ->
                  Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Exp -> Id -> [Alt] -> Exp
Case Annote
can (Exp -> Ty
typeOf Exp
e) Exp
cd Id
ccb
                        [ Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
aan AltCon
c [Id]
xs (Exp -> Alt) -> Exp -> Alt
forall a b. (a -> b) -> a -> b
$ (Exp -> Arg -> Exp) -> Exp -> [Arg] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Annote -> Exp -> Arg -> Exp
App Annote
can) Exp
b [Arg]
args | Alt Annote
aan AltCon
c [Id]
xs Exp
b <- [Alt]
calts ]
            (Exp, [Arg])
_                         -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) (Text -> TM m Exp) -> Text -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"encountered ill-formed application:\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Exp -> Text
forall a. Pretty a => a -> Text
prettyPrint (Exp -> Exp
forall d. Data d => d -> d
Ann.unAnn Exp
e)
      Prim Annote
an Ty
_ Builtin
b     -> Env
-> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env
-> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m Exp
transBuiltin Env
env Scope
sc Annote
an (Exp -> Ty
typeOf Exp
e) Annote
an (Builtin
b, [])
      Var Annote
an Id
x        -> case Int -> IntMap Exp -> Maybe Exp
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Id -> Int
idUniq Id
x) (IntMap Exp -> Maybe Exp) -> IntMap Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Scope -> IntMap Exp
scMap Scope
sc of
            Just Exp
atom -> Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
atom
            Maybe Exp
Nothing   -> do
                  sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env (Text
"Var " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
x) Annote
an (Ty -> TM m Size) -> Ty -> TM m Size
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x
                  A.Call an sz <$> globalName env an x <*> pure []
      Con Annote
an Ty
t Text
d      -> do
            (v, w)     <- Env -> Annote -> Ty -> Text -> TM m (Integer, Size)
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Text -> TM m (Integer, Size)
ctorTag Env
env Annote
an Ty
t Text
d
            (tag, pad) <- ctorRep an t (v, w) 0
            pure $ A.cat [A.Lit an tag, A.Lit an pad]
      LitInt Annote
an Ty
t Integer
n   -> do
            sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"LitInt" Annote
an Ty
t
            pure $ A.Lit an $ bitVec (fromIntegral sz) n
      LitVec Annote
_ Ty
_ [Exp]
es   -> [Exp] -> Exp
A.cat ([Exp] -> Exp) -> StateT S m [Exp] -> TM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [Exp]
es
      Case Annote
an Ty
t Exp
disc Id
cb [Alt]
alts -> do
            sz    <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"Case" Annote
an Ty
t
            disc' <- transExp env sc disc
            bindAtom (ann disc) disc' $ \ Exp
datom ->
                  Env
-> Scope
-> Annote
-> Size
-> Ty
-> Exp
-> [(Annote, AltCon, [Id], Exp)]
-> (Scope -> Exp -> TM m Exp)
-> TM m Exp
forall (m :: * -> *) body.
MonadError AstError m =>
Env
-> Scope
-> Annote
-> Size
-> Ty
-> Exp
-> [(Annote, AltCon, [Id], body)]
-> (Scope -> body -> TM m Exp)
-> TM m Exp
caseChain Env
env (Scope
sc { scMap = IM.insert (idUniq cb) datom $ scMap sc }) Annote
an Size
sz (Exp -> Ty
typeOf Exp
disc) Exp
datom
                        [ (Annote
aan, AltCon
c, [Id]
xs, Exp
b) | Alt Annote
aan AltCon
c [Id]
xs Exp
b <- [Alt]
alts ]
                        (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env)
      Let Annote
an (NonRec Id
x Exp
rhs) Exp
body -> do
            rhs' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
rhs
            case rhs' of
                  A.Lit {} -> Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env (Scope
sc { scMap = IM.insert (idUniq x) rhs' $ scMap sc }) Exp
body
                  A.Var {} -> Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env (Scope
sc { scMap = IM.insert (idUniq x) rhs' $ scMap sc }) Exp
body
                  Exp
_        -> do
                        let (Scope
sc', Text
nm) = Annote -> Scope -> Id -> Size -> (Scope, Text)
bindLocal Annote
an Scope
sc Id
x (Size -> (Scope, Text)) -> Size -> (Scope, Text)
forall a b. (a -> b) -> a -> b
$ Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
rhs'
                        body' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc' Exp
body
                        pure $ A.Let an (A.sizeOf body') nm rhs' body'
      Let Annote
an (Rec {}) Exp
_  -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"unsupported recursive local binding."
      Let Annote
an (Join {}) Exp
_ -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"join point survived lifting (rwc bug)."
      Jump Annote
an JoinId
_ [Exp]
_        -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"jump survived lifting (rwc bug)."
      Lam Annote
an Id
_ Exp
_         -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"unsupported lambda expression."
      Exp
_                  -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) (Text -> TM m Exp) -> Text -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unsupported expression: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Exp -> Text
forall a. Pretty a => a -> Text
prettyPrint (Exp -> Exp
forall d. Data d => d -> d
Ann.unAnn Exp
e)
      where ctorRep :: MonadError AstError m => Annote -> Ty -> (A.Value, A.Size) -> A.Size -> TM m (BV, BV)
            ctorRep :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> Ty -> (Integer, Size) -> Size -> TM m (BV, BV)
ctorRep Annote
an Ty
t (Integer
v, Size
w) Size
szArgs = do
                  sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"ctorRep" Annote
an Ty
t
                  if | w + szArgs <= sz -> pure (bitVec (fromIntegral w) v, zeros $ fromIntegral sz - fromIntegral w - fromIntegral szArgs)
                     | otherwise        -> failInternal an $ "failing to calculate the bitvector representation of a constructor of type (sz: "
                                                    <> showt sz <> " w: " <> showt w <> " szArgs: " <> showt szArgs <> "):\n" <> prettyPrint (Ann.unAnn t)

-- | The if-chain for an n-ary case, generic over the body language (pure
--   expressions and machine terminators). The default alternative (first,
--   the Core convention) becomes the final else; without one, the last
--   alternative is unconditional.
caseChain :: forall m body. MonadError AstError m
          => Env -> Scope -> Annote -> A.Size -> Ty -> A.Exp
          -> [(Annote, AltCon, [Id], body)]
          -> (Scope -> body -> TM m A.Exp)
          -> TM m A.Exp
caseChain :: forall (m :: * -> *) body.
MonadError AstError m =>
Env
-> Scope
-> Annote
-> Size
-> Ty
-> Exp
-> [(Annote, AltCon, [Id], body)]
-> (Scope -> body -> TM m Exp)
-> TM m Exp
caseChain Env
env Scope
sc Annote
an Size
sz Ty
discTy Exp
datom [(Annote, AltCon, [Id], body)]
alts Scope -> body -> TM m Exp
transBody = case [(Annote, AltCon, [Id], body)]
alts of
      (Annote
aan, AltCon
DefaultAlt, [Id]
_, body
b) : [(Annote, AltCon, [Id], body)]
rest -> [(Annote, AltCon, [Id], body)] -> Maybe Exp -> TM m Exp
go [(Annote, AltCon, [Id], body)]
rest (Maybe Exp -> TM m Exp) -> (Exp -> Maybe Exp) -> Exp -> TM m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> TM m Exp) -> TM m Exp -> TM m Exp
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Scope -> body -> TM m Exp
transBody Scope
sc body
b TM m Exp -> StateT S m Annote -> TM m Exp
forall a b. StateT S m a -> StateT S m b -> StateT S m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Annote -> StateT S m Annote
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Annote
aan
      [(Annote, AltCon, [Id], body)]
rest                           -> [(Annote, AltCon, [Id], body)] -> Maybe Exp -> TM m Exp
go [(Annote, AltCon, [Id], body)]
rest Maybe Exp
forall a. Maybe a
Nothing
      where go :: [(Annote, AltCon, [Id], body)] -> Maybe A.Exp -> TM m A.Exp
            go :: [(Annote, AltCon, [Id], body)] -> Maybe Exp -> TM m Exp
go [] (Just Exp
els) = Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
els
            go []  Maybe Exp
Nothing   = Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"encountered an empty case."
            go [(Annote, AltCon, [Id], body)
a] Maybe Exp
Nothing   = (Annote, AltCon, [Id], body) -> Maybe Exp -> TM m Exp
altExp (Annote, AltCon, [Id], body)
a Maybe Exp
forall a. Maybe a
Nothing
            go ((Annote, AltCon, [Id], body)
a : [(Annote, AltCon, [Id], body)]
rest) Maybe Exp
mels = (Annote, AltCon, [Id], body) -> Maybe Exp -> TM m Exp
altExp (Annote, AltCon, [Id], body)
a (Maybe Exp -> TM m Exp) -> (Exp -> Maybe Exp) -> Exp -> TM m Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> TM m Exp) -> TM m Exp -> TM m Exp
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Annote, AltCon, [Id], body)] -> Maybe Exp -> TM m Exp
go [(Annote, AltCon, [Id], body)]
rest Maybe Exp
mels

            altExp :: (Annote, AltCon, [Id], body) -> Maybe A.Exp -> TM m A.Exp
            altExp :: (Annote, AltCon, [Id], body) -> Maybe Exp -> TM m Exp
altExp (Annote
aan, AltCon
c, [Id]
xs, body
b) Maybe Exp
mrest = do
                  (conds, binds) <- case AltCon
c of
                        DataAlt Text
d  -> do
                              (v, w) <- Env -> Annote -> Ty -> Text -> TM m (Integer, Size)
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Text -> TM m (Integer, Size)
ctorTag Env
env Annote
aan Ty
discTy Text
d
                              szT    <- sizeOf env "caseChain" aan discTy
                              szXs   <- mapM (sizeOf env "caseChain field" aan . sigTy . idSig) xs
                              let fields :: [(Maybe Id, A.Size, A.Index)]
                                  fields = [(Maybe Id, Size)] -> [(Maybe Id, Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets ([(Maybe Id, Size)] -> [(Maybe Id, Size, Size)])
-> [(Maybe Id, Size)] -> [(Maybe Id, Size, Size)]
forall a b. (a -> b) -> a -> b
$ (Maybe Id
forall a. Maybe a
Nothing, Size
w) (Maybe Id, Size) -> [(Maybe Id, Size)] -> [(Maybe Id, Size)]
forall a. a -> [a] -> [a]
: (Maybe Id
forall a. Maybe a
Nothing, Size
szT Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
w Size -> Size -> Size
forall a. Num a => a -> a -> a
- [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Size]
szXs) (Maybe Id, Size) -> [(Maybe Id, Size)] -> [(Maybe Id, Size)]
forall a. a -> [a] -> [a]
: (Id -> Size -> (Maybe Id, Size))
-> [Id] -> [Size] -> [(Maybe Id, Size)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Id
x Size
szx -> (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x, Size
szx)) [Id]
xs [Size]
szXs
                                  conds  = [ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
aan Size
1 Op
A.Eq [Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
aan Size
off Size
w Exp
datom, Annote -> BV -> Exp
A.Lit Annote
aan (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
w) Integer
v]
                                           | (Maybe Id
Nothing, Size
_, Size
off) <- Int -> [(Maybe Id, Size, Size)] -> [(Maybe Id, Size, Size)]
forall a. Int -> [a] -> [a]
take Int
1 [(Maybe Id, Size, Size)]
fields, Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0 ]
                                  binds  = [ (Id
x, Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
aan Size
off Size
szx Exp
datom) | (Just Id
x, Size
szx, Size
off) <- Int -> [(Maybe Id, Size, Size)] -> [(Maybe Id, Size, Size)]
forall a. Int -> [a] -> [a]
drop Int
2 [(Maybe Id, Size, Size)]
fields ]
                              pure (conds, binds)
                        LitAlt Integer
i   -> do
                              szT <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"caseChain" Annote
aan Ty
discTy
                              pure ([ A.Prim aan 1 A.Eq [datom, A.Lit aan $ bitVec (fromIntegral szT) i] ], [])
                        AltCon
DefaultAlt -> Annote -> Text -> StateT S m ([Exp], [(Id, Exp)])
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
aan Text
"default alternative not first."
                  (sc', binds') <- pure $ foldl' (\ (Scope
s, [(Text, Exp)]
acc) (Id
x, Exp
slc) ->
                              let (Scope
s', Text
nm) = Annote -> Scope -> Id -> Size -> (Scope, Text)
bindLocal Annote
aan Scope
s Id
x (Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
slc) in (Scope
s', [(Text, Exp)]
acc [(Text, Exp)] -> [(Text, Exp)] -> [(Text, Exp)]
forall a. Semigroup a => a -> a -> a
<> [(Text
nm, Exp
slc)]))
                        (sc, []) binds
                  body' <- transBody sc' b
                  let lets = ((Text, Exp) -> Exp -> Exp) -> Exp -> [(Text, Exp)] -> Exp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Text
nm, Exp
slc) Exp
acc -> Annote -> Size -> Text -> Exp -> Exp -> Exp
A.Let Annote
aan (Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
acc) Text
nm Exp
slc Exp
acc) Exp
body' [(Text, Exp)]
binds'
                  pure $ case (mrest, conds) of
                        (Just Exp
rest', Exp
_ : [Exp]
_) -> Annote -> Size -> Exp -> Exp -> Exp -> Exp
A.If Annote
aan Size
sz (Annote -> [Exp] -> Exp
conj Annote
aan [Exp]
conds) Exp
lets Exp
rest'
                        (Maybe Exp, [Exp])
_                   -> Exp
lets

---
--- Builtins.
---

transBuiltin :: forall m. MonadError AstError m => Env -> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m A.Exp
transBuiltin :: forall (m :: * -> *).
MonadError AstError m =>
Env
-> Scope -> Annote -> Ty -> Annote -> (Builtin, [Exp]) -> TM m Exp
transBuiltin Env
env Scope
sc Annote
an' Ty
t' Annote
an (Builtin, [Exp])
theExp = case (Builtin, [Exp])
theExp of
      (Builtin
Error, [Exp]
args) -> do
            sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimError" Annote
an Ty
t'
            addWarning an' $ "encountered a live call to the built-in \"error\" function; compiling to a zero (don't-care) value of width " <> showt sz <> "."
                  <> (case args of
                        [LitStr Annote
_ Text
x] -> Text
"\nError message: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
forall a. TextShow a => a -> Text
showt Text
x
                        [Exp]
_            -> Text
forall a. Monoid a => a
mempty)
            pure $ A.Undef an' sz
      (Builtin
Bits, [Exp
arg]) -> Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
arg
      (Builtin
Resize, [Exp
arg]) -> do
            sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimResize" Annote
an Ty
t'
            resize an sz =<< transExp env sc arg
      (Builtin
BitIndex, [Exp
arg, Exp -> Maybe Integer
finLit -> Just Integer
i]) -> Annote -> Exp -> Integer -> Natural -> TM m Exp
subElems Annote
an Exp
arg ((-Integer
i) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Natural
1
      (Builtin
BitSlice, [Exp
arg, Exp -> Maybe Integer
finLit -> Just Integer
j, Exp -> Maybe Integer
finLit -> Just Integer
i]) -> do
            Bool -> StateT S m () -> StateT S m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
i) (StateT S m () -> StateT S m ()) -> StateT S m () -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> StateT S m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
arg)
                  (Text -> StateT S m ()) -> Text -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ Text
"invalid bit slice (j: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
forall a. TextShow a => a -> Text
showt Integer
j Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", i: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
forall a. TextShow a => a -> Text
showt Integer
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")."
            sz <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimBitSlice" Annote
an Ty
t'
            let nBits = Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i
                off   = (-Integer
i) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
nBits
            unless (toInteger nBits == toInteger sz) $ failAt (ann arg)
                  $ "bit slice of width " <> showt nBits <> " (j: " <> showt j <> ", i: " <> showt i
                  <> ") does not match the declared result width " <> showt sz <> "."
            subElems an arg off nBits
      (Builtin
BitSlice, [Exp]
_) -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' Text
"rwPrimBitSlice must have arguments (finite j) (finite i) with LitInts"
      (Builtin
VecIndex, [Exp
arg, Exp
i]) -> Exp -> Exp -> TM m Exp
vecIndex Exp
arg Exp
i
      (Builtin
VecIndexProxy, [Exp
arg, Exp
p]) -> do
            i <- Text -> Exp -> TM m Integer
checkProxyArg Text
"rwPrimVecIndexProxy" Exp
p
            subElems an arg i 1
      (Builtin
NatVal, [Exp
p]) -> do
            i  <- Text -> Exp -> TM m Integer
checkProxyArg Text
"rwPrimNatVal" Exp
p
            sz <- sizeOf env "rwPrimNatVal" an t'
            pure $ A.Lit an $ bitVec (fromIntegral sz) i
      (Builtin
VecSlice, [Exp
p, Exp
arg]) -> do
            i      <- Text -> Exp -> TM m Integer
checkProxyArg Text
"rwPrimVecSlice" Exp
p
            nElems <- checkVecArgSize "rwPrimVecSlice" t'
            subElems an arg i nElems
      (Builtin
VecRSlice, [Exp
p, Exp
arg]) -> do
            i      <- Text -> Exp -> TM m Integer
checkProxyArg Text
"rwPrimVecRSlice" Exp
p
            nElems <- checkVecArgSize "rwPrimVecRSlice" t'
            subElems an arg ((- i) - fromIntegral nElems) nElems
      (Builtin
VecReverse, [Exp
arg]) -> do
            arg'   <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
arg
            nElems <- checkVecArgSize "rwPrimVecReverse" t'
            tyElem <- checkVecArgType "rwPrimVecReverse" t'
            szElem <- sizeOf env "rwPrimVecReverse" an tyElem
            bindAtom an arg' $ \ Exp
a ->
                  Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> Exp
A.cat ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> [Exp]
forall a. [a] -> [a]
reverse [ Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an Size
off Size
szElem Exp
a | (()
_, Size
_, Size
off) <- [((), Size)] -> [((), Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets ([((), Size)] -> [((), Size, Size)])
-> [((), Size)] -> [((), Size, Size)]
forall a b. (a -> b) -> a -> b
$ Int -> ((), Size) -> [((), Size)]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
nElems) ((), Size
szElem) ]
      (Builtin
VecReplicate, [Exp
arg]) -> do
            sz     <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimVecReplicate" Annote
an Ty
t'
            arg'   <- transExp env sc arg
            nElems <- checkVecArgSize "rwPrimVecReplicate" t'
            pure $ if nElems == 0 || sz == 0 then A.Lit an BV.nil
                   else A.Prim an sz (A.Rep nElems) [arg']
      (Builtin
VecMap, [Exp
f, Exp
arg]) -> do
            nElems  <- Text -> Ty -> TM m Natural
checkVecArgSize Text
"rwPrimVecMap" Ty
t'
            tyElemO <- checkVecArgType "rwPrimVecMap" t'
            szElemO <- sizeOf env "rwPrimVecMap" an tyElemO
            tyElemI <- checkVecArgType "rwPrimVecMap" $ typeOf arg
            szElemI <- sizeOf env "rwPrimVecMap" an tyElemI
            arg'    <- transExp env sc arg
            let szV = Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
arg'
            bindAtom an arg' $ \ Exp
a ->
                  [Exp] -> Exp
A.cat ([Exp] -> Exp) -> StateT S m [Exp] -> TM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TM m Exp) -> [Int] -> StateT S 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 (\ Int
i -> Annote -> Size -> Exp -> [Exp] -> TM m Exp
applyFn Annote
an Size
szElemO Exp
f
                              [Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an (Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
szV Size -> Size -> Size
forall a. Num a => a -> a -> a
- (Int -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
szElemI) Size
szElemI Exp
a])
                        [Int
0 .. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
nElems Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 :: Int]
      (Builtin
VecGenerate, [Exp
f]) -> do
            nElems  <- Text -> Ty -> TM m Natural
checkVecArgSize Text
"rwPrimVecGenerate" Ty
t'
            tyElemO <- checkVecArgType "rwPrimVecGenerate" t'
            szElemO <- sizeOf env "rwPrimVecGenerate" an tyElemO
            let finW = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
nbits Natural
nElems
            A.cat <$> mapM (\ Integer
i -> Annote -> Size -> Exp -> [Exp] -> TM m Exp
applyFn Annote
an Size
szElemO Exp
f [Annote -> BV -> Exp
A.Lit Annote
an (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
finW Integer
i])
                  [0 .. toInteger nElems - 1]
      (Builtin
VecConcat, [Exp
arg1, Exp
arg2]) -> [Exp] -> Exp
A.cat ([Exp] -> Exp) -> StateT S m [Exp] -> TM m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [Exp
arg1, Exp
arg2]
      (Builtin
VecFromList, [LitList Annote
_ Ty
_ [Exp]
els]) -> do
            nElems <- Text -> Ty -> TM m Natural
checkVecArgSize Text
"rwPrimVecFromList" Ty
t'
            unless (length els == fromIntegral nElems) $ failAt an'
                  $ "rwPrimVecFromList: list literal has " <> showt (length els)
                  <> " elements, but the result type expects " <> showt nElems <> "."
            A.cat <$> mapM (transExp env sc) els
      (Builtin
VecFromList, [Exp]
_) -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' Text
"rwPrimVecFromList: argument must be a list literal."
      (Builtin
Finite, [Exp
arg]) -> do
            arg' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
arg
            case arg' of
                  A.Lit Annote
an'' (BV -> Integer
BV.nat -> Integer
i) -> do
                        finSz <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimFinite" Ty
t'
                        unless (i >= 0 && i < fromIntegral finSz)
                              $ failAt (ann arg) ("rwPrimFinite: Integer " <> showt i <> " is not representable in Finite " <> showt finSz <> ".")
                        pure $ A.Lit an'' $ bitVec (fromIntegral $ nbits finSz) i
                  Exp
_ -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
arg) Text
"rwPrimFinite: can't determine argument value at compile-time."
      (Builtin
FiniteMinBound, []) -> do
            finSz <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimFiniteMinBound" Ty
t'
            unless (finSz > 0)
                  $ failAt an "rwPrimFiniteMinBound: Finite 0 is uninhabited."
            pure $ A.Lit an $ bitVec (fromIntegral $ nbits finSz) (0 :: Integer)
      (Builtin
FiniteMaxBound, []) -> do
            finSz <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimFiniteMaxBound" Ty
t'
            unless (finSz > 0)
                  $ failAt an "rwPrimFiniteMaxBound: Finite 0 is uninhabited."
            pure $ A.Lit an $ bitVec (fromIntegral $ nbits finSz) $ toInteger finSz - 1
      (Builtin
ToFinite, [Exp
arg]) -> do
            finSz  <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimToFinite" Ty
t'
            sz     <- sizeOf env "rwPrimToFinite" an t'
            nBits  <- checkVecArgSize "rwPrimToFinite" $ typeOf arg
            unless (2 ^ nBits <= (fromIntegral finSz :: Integer))
                  $ failAt (ann arg) ("rwPrimToFinite: bitvector argument (size " <> showt nBits <> ") is not representable in Finite " <> showt finSz <> ".")
            resize an sz =<< transExp env sc arg
      (Builtin
ToFiniteMod, [Exp
arg]) -> do
            finSz   <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimToFiniteMod" Ty
t'
            unless (finSz > 0)
                  $ failAt an "rwPrimToFiniteMod: Finite 0 is uninhabited."
            sz      <- sizeOf env "rwPrimToFiniteMod" an t'
            nBits   <- checkVecArgSize "rwPrimToFiniteMod" $ typeOf arg
            arg'    <- transExp env sc arg
            if 2 ^ nBits <= (fromIntegral finSz :: Integer) then resize an sz arg'
            else do
                  let szLit  = Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Size) -> Natural -> Size
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
nbits Natural
finSz
                      w      = Size -> Size -> Size
forall a. Ord a => a -> a -> a
max (Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
nBits) Size
szLit
                  a <- resize an w arg'
                  resize an sz $ A.Prim an w A.UMod [a, A.Lit an $ bitVec (fromIntegral w) $ toInteger finSz]
      (Builtin
FromFinite, [Exp
arg]) -> do
            finSz <- Text -> Ty -> TM m Natural
checkFinTypeMax Text
"rwPrimFromFinite" (Ty -> TM m Natural) -> Ty -> TM m Natural
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
arg
            nBits <- checkVecArgSize "rwPrimFromFinite" t'
            unless ((fromIntegral finSz :: Integer) <= 2 ^ nBits)
                  $ failAt (ann arg) ("rwPrimFromFinite: Finite " <> showt finSz <> " is not representable in bitvector of size " <> showt nBits <> ".")
            resize an (fromIntegral nBits) =<< transExp env sc arg
      (Builtin
b, [Exp]
args) | Just Annote -> Text -> [Exp] -> Either Text Exp
_ <- Builtin
-> Size
-> Size
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
toPrim Builtin
b Size
0 Size
0 -> do
            sz    <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env (Builtin -> Text
forall a. TextShow a => a -> Text
showt Builtin
b) Annote
an Ty
t'
            args' <- mapM (transExp env sc) args
            applyPrim an sz b args'
      (Builtin
Extern, LitList Annote
_ Ty
_ [Exp]
ps : (Exp -> Maybe Text
litStr -> Just Text
clk) : (Exp -> Maybe Text
litStr -> Just Text
rst) : LitList Annote
_ Ty
_ [Exp]
as : LitList Annote
_ Ty
_ [Exp]
rs : (Exp -> Maybe Text
litStr -> Just Text
s) : Exp
a : (Exp -> Maybe Text
litStr -> Just Text
_inst) : [Exp]
args)
            | [Ty] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Ty], Ty) -> [Ty]
forall a b. (a, b) -> a
fst (([Ty], Ty) -> [Ty]) -> ([Ty], Ty) -> [Ty]
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow (Ty -> ([Ty], Ty)) -> Ty -> ([Ty], Ty)
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
args -> do
            sz    <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimExtern" Annote
an Ty
t'
            args' <- mapM (transExp env sc) args
            applyExtern an' sz (ps, clk, rst, as, rs, s) a args'
      (Builtin
Extern,  [Exp]
_) -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"encountered not-fully-applied extern (after inlining)."
      (Builtin
Cryptol, (Exp -> Maybe Text
litStr -> Just Text
f) : (Exp -> Maybe Text
litStr -> Just Text
n) : Exp
a : [Exp]
args)
            | [Ty] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Ty], Ty) -> [Ty]
forall a b. (a, b) -> a
fst (([Ty], Ty) -> [Ty]) -> ([Ty], Ty) -> [Ty]
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow (Ty -> ([Ty], Ty)) -> Ty -> ([Ty], Ty)
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
args ->
            case (Text, Text, Text) -> HashMap (Text, Text, Text) Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Text
f, Text
n, Ty -> Text
tyKey (Ty -> Text) -> Ty -> Text
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a) (HashMap (Text, Text, Text) Text -> Maybe Text)
-> HashMap (Text, Text, Text) Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Env -> HashMap (Text, Text, Text) Text
envCry Env
env of
                  Just Text
g  -> do
                        sz    <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimCryptol" Annote
an Ty
t'
                        args' <- mapM (transExp env sc) args
                        pure $ A.Call an' sz g args'
                  Maybe Text
Nothing -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"Cryptol foreign function was not precompiled (rwc bug)."
      (Builtin
Cryptol, [Exp]
_) -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"encountered not-fully-applied Cryptol foreign function (after inlining)."
      (Builtin
b, [Exp]
_) | Builtin
b Builtin -> [Builtin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Builtin
Bind, Builtin
Return]
                     -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text
"encountered unsupported builtin use: rwPrim" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Builtin -> Text
forall a. TextShow a => a -> Text
showt Builtin
b
                          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (a monadic operator at a monad other than the ReacT/StateT/Identity stack?).")
      (Builtin
b, [Exp]
_)         -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text
"encountered unsupported builtin use: rwPrim" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Builtin -> Text
forall a. TextShow a => a -> Text
showt Builtin
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".")

      where litStr :: Exp -> Maybe Text
            litStr :: Exp -> Maybe Text
litStr = \ case
                  LitStr Annote
_ Text
x -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
x
                  Exp
_          -> Maybe Text
forall a. Maybe a
Nothing

            finLit :: Exp -> Maybe Integer
            finLit :: Exp -> Maybe Integer
finLit Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
_ Ty
_ Builtin
Finite, [EArg (LitInt Annote
_ Ty
_ Integer
i)]) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i
                  (Exp, [Arg])
_                                        -> Maybe Integer
forall a. Maybe a
Nothing

            -- | Apply a function-valued argument of a built-in vector
            --   operation to translated arguments: a reference to a global
            --   definition becomes a call; a lambda binds in place.
            applyFn :: Annote -> A.Size -> Exp -> [A.Exp] -> TM m A.Exp
            applyFn :: Annote -> Size -> Exp -> [Exp] -> TM m Exp
applyFn Annote
an'' Size
szOut Exp
f [Exp]
args' = case Exp -> (Exp, [Arg])
flattenApp Exp
f of
                  (Var Annote
_ Id
x, [Arg]
pre) | Bool -> Bool
not (Int -> IntMap Exp -> Bool
forall a. Int -> IntMap a -> Bool
IM.member (Id -> Int
idUniq Id
x) (IntMap Exp -> Bool) -> IntMap Exp -> Bool
forall a b. (a -> b) -> a -> b
$ Scope -> IntMap Exp
scMap Scope
sc) -> do
                        pre' <- (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [ Exp
e | EArg Exp
e <- [Arg]
pre ]
                        A.Call an'' szOut <$> globalName env an'' x <*> pure (pre' <> args')
                  (Lam Annote
_ Id
p Exp
b, []) | [Exp
arg'] <- [Exp]
args' -> do
                        x <- Text -> StateT S m Text
forall (m :: * -> *). MonadState S m => Text -> m Text
freshLocal Text
"$f"
                        let sc' = Scope
sc { scMap = IM.insert (idUniq p) (A.Var an'' (A.sizeOf arg') x) $ scMap sc }
                        b' <- transExp env sc' b
                        pure $ A.Let an'' (A.sizeOf b') x arg' b'
                  -- An eta-reduced operator builtin (e.g. @map bnot@):
                  -- apply it directly. Width-directed builtins (resize and
                  -- the like) still need a lambda or a named definition.
                  (Prim Annote
_ Ty
_ Builtin
b, [Arg]
pre) | Just Annote -> Text -> [Exp] -> Either Text Exp
_ <- Builtin
-> Size
-> Size
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
toPrim Builtin
b Size
0 Size
0 -> do
                        pre' <- (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [ Exp
e | EArg Exp
e <- [Arg]
pre ]
                        applyPrim an'' szOut b (pre' <> args')
                  (Exp, [Arg])
_ -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an'' Text
"unsupported function argument to a built-in vector operation (a builtin must be wrapped in a lambda or a named definition unless it is a plain operator)."

            subElems :: Annote -> Exp -> Integer -> Natural -> TM m A.Exp
            subElems :: Annote -> Exp -> Integer -> Natural -> TM m Exp
subElems Annote
an'' Exp
arg Integer
i Natural
nElems = do
                  tyElem <- TM m Ty -> (Ty -> TM m Ty) -> Maybe Ty -> TM m Ty
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
arg) Text
"non-vector type argument to built-in vector function") Ty -> TM m Ty
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                          (Maybe Ty -> TM m Ty) -> Maybe Ty -> TM m Ty
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Ty
vecElemTy (Ty -> Maybe Ty) -> Ty -> Maybe Ty
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
arg
                  szElem <- fromIntegral <$> sizeOf env "subElems" an'' tyElem
                  arg'   <- transExp env sc arg

                  let sz, off, n :: Natural
                      sz  = Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Natural) -> Size -> Natural
forall a b. (a -> b) -> a -> b
$ Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
arg'
                      off = Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ (if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
sz else Integer
0) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
szElem
                      n   = Natural
nElems Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
szElem

                  unless (sz >= off + n)
                        $ failAt an'' $ "invalid bit slice (offset: " <> showt i <> ", num elems: " <> showt nElems <> ") from object size " <> showt sz <> "."

                  -- LSB offset of the slice: fields count from the MSB end.
                  let lsbOff = Natural
sz Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
off Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
n
                  bindAtom an'' arg' $ \ Exp
a -> Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an'' (Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
lsbOff) (Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) Exp
a

            -- | index v i = resize szElem (v >> ((n - i - 1) * szElem)), with
            --   the shift amount computed at the index's width (or the
            --   literal width, whichever is wider).
            vecIndex :: Exp -> Exp -> TM m A.Exp
            vecIndex :: Exp -> Exp -> TM m Exp
vecIndex Exp
v Exp
i = do
                  let tyVec :: Ty
tyVec = Exp -> Ty
typeOf Exp
v
                  szVec  <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"rwPrimIndex" Annote
an Ty
tyVec
                  n      <- maybe (failAt an "rwPrimIndex: invalid Vec argument.") pure $ vecSize tyVec
                  tyElem <- maybe (failAt an "rwPrimIndex: non-vector type argument.") pure $ vecElemTy tyVec
                  szElem <- sizeOf env "rwPrimIndex" an tyElem
                  szIdx  <- sizeOf env "rwPrimIndex" an $ typeOf i
                  szLit  <- sizeOf env "rwPrimIndex" an intTy

                  v' <- transExp env sc v
                  i' <- transExp env sc i

                  -- ((n - i) - 1) * szElem, all at width w.
                  let w = Size -> Size -> Size
forall a. Ord a => a -> a -> a
max Size
szIdx Size
szLit
                  i''  <- resize an w i'
                  let amt = Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
w Op
A.Mul
                              [ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
w Op
A.Sub
                                    [ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
w Op
A.Sub [Annote -> BV -> Exp
A.Lit Annote
an (Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
w) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n), Exp
i'']
                                    , Annote -> BV -> Exp
A.Lit Annote
an (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
w) (Integer
1 :: Integer) ]
                              , Annote -> BV -> Exp
A.Lit Annote
an (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
w) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Size -> Integer
forall a. Integral a => a -> Integer
toInteger Size
szElem ]
                  resize an szElem $ A.Prim an szVec A.LShr [v', amt]

            checkProxyArg :: Text -> Exp -> TM m Integer
            checkProxyArg :: Text -> Exp -> TM m Integer
checkProxyArg Text
t Exp
p = TM m Integer
-> (Natural -> TM m Integer) -> Maybe Natural -> TM m Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Integer
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' (Text -> TM m Integer) -> Text -> TM m Integer
forall a b. (a -> b) -> a -> b
$ Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": invalid Proxy argument.  " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Exp -> Text
forall a. Pretty a => a -> Text
prettyPrint (Exp -> Exp
forall d. Data d => d -> d
Ann.unAnn Exp
p)) (Integer -> TM m Integer
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> TM m Integer)
-> (Natural -> Integer) -> Natural -> TM m Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral)
                        (Maybe Natural -> TM m Integer) -> Maybe Natural -> TM m Integer
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Natural
proxyNat (Ty -> Maybe Natural) -> Ty -> Maybe Natural
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
p

            checkVecArgSize :: Text -> Ty -> TM m Natural
            checkVecArgSize :: Text -> Ty -> TM m Natural
checkVecArgSize Text
s Ty
t = TM m Natural
-> (Natural -> TM m Natural) -> Maybe Natural -> TM m Natural
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Natural
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' (Text -> TM m Natural) -> Text -> TM m Natural
forall a b. (a -> b) -> a -> b
$ Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": invalid Vec size argument: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn Ty
t)) Natural -> TM m Natural
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                        (Maybe Natural -> TM m Natural) -> Maybe Natural -> TM m Natural
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Natural
vecSize Ty
t

            checkVecArgType :: Text -> Ty -> TM m Ty
            checkVecArgType :: Text -> Ty -> TM m Ty
checkVecArgType Text
s Ty
t = TM m Ty -> (Ty -> TM m Ty) -> Maybe Ty -> TM m Ty
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' (Text -> TM m Ty) -> Text -> TM m Ty
forall a b. (a -> b) -> a -> b
$ Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": invalid Vec type argument: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn Ty
t)) Ty -> TM m Ty
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                        (Maybe Ty -> TM m Ty) -> Maybe Ty -> TM m Ty
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Ty
vecElemTy Ty
t

            checkFinTypeMax :: Text -> Ty -> TM m Natural
            checkFinTypeMax :: Text -> Ty -> TM m Natural
checkFinTypeMax Text
s Ty
t = TM m Natural
-> (Natural -> TM m Natural) -> Maybe Natural -> TM m Natural
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Natural
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an' (Text -> TM m Natural) -> Text -> TM m Natural
forall a b. (a -> b) -> a -> b
$ Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": invalid Finite type: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn Ty
t)) Natural -> TM m Natural
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                        (Maybe Natural -> TM m Natural) -> Maybe Natural -> TM m Natural
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Natural
finSz Ty
t

vecSize :: Ty -> Maybe Natural
vecSize :: Ty -> Maybe Natural
vecSize Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
      (TyCon Annote
_ Text
"Vec", [Ty
n, Ty
_]) -> Ty -> Maybe Natural
evalNat Ty
n
      (Ty, [Ty])
_                       -> Maybe Natural
forall a. Maybe a
Nothing

vecElemTy :: Ty -> Maybe Ty
vecElemTy :: Ty -> Maybe Ty
vecElemTy Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
      (TyCon Annote
_ Text
"Vec", [Ty
_, Ty
te]) -> Ty -> Maybe Ty
forall a. a -> Maybe a
Just Ty
te
      (Ty, [Ty])
_                        -> Maybe Ty
forall a. Maybe a
Nothing

proxyNat :: Ty -> Maybe Natural
proxyNat :: Ty -> Maybe Natural
proxyNat Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
      (TyCon Annote
_ Text
"Proxy", [Ty
n]) -> Ty -> Maybe Natural
evalNat Ty
n
      (Ty, [Ty])
_                      -> Maybe Natural
forall a. Maybe a
Nothing

finSz :: Ty -> Maybe Natural
finSz :: Ty -> Maybe Natural
finSz Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
      (TyCon Annote
_ Text
"Finite", [Ty
n]) -> Ty -> Maybe Natural
evalNat Ty
n
      (Ty, [Ty])
_                       -> Maybe Natural
forall a. Maybe a
Nothing

-- | Apply a (width-implicit) primitive to translated arguments, expanding
--   to the Hyle operator set (doc/hyle.md, section 3.3).
applyPrim :: (MonadError AstError m, MonadState S m) => Annote -> A.Size -> Builtin -> [A.Exp] -> m A.Exp
applyPrim :: forall (m :: * -> *).
(MonadError AstError m, MonadState S m) =>
Annote -> Size -> Builtin -> [Exp] -> m Exp
applyPrim Annote
an Size
sz Builtin
b [Exp]
args = do
      x <- Text -> m Text
forall (m :: * -> *). MonadState S m => Text -> m Text
freshLocal Text
"$t" -- may go unused (MSBit needs one)
      case toPrim b sz (case args of { Exp
a : [Exp]
_ -> Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
a; [Exp]
_ -> Size
0 }) of
            Just Annote -> Text -> [Exp] -> Either Text Exp
f  -> (Text -> m Exp) -> (Exp -> m Exp) -> Either Text Exp -> m Exp
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Annote -> Text -> m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an) Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text Exp -> m Exp) -> Either Text Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> [Exp] -> Either Text Exp
f Annote
an Text
x [Exp]
args
            Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
Nothing -> Annote -> Text -> m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an (Text -> m Exp) -> Text -> m Exp
forall a b. (a -> b) -> a -> b
$ Text
"applyPrim: unsupported primitive: rwPrim" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Builtin -> Text
forall a. TextShow a => a -> Text
showt Builtin
b 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."

-- | The primitive table: given the result width and the (first) operand
--   width, a pure applicator (taking a pre-generated fresh name for the
--   cases that need a binding).
toPrim :: Builtin -> A.Size -> A.Size -> Maybe (Annote -> A.Name -> [A.Exp] -> Either Text A.Exp)
toPrim :: Builtin
-> Size
-> Size
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
toPrim Builtin
b Size
sz Size
w = case Builtin
b of
      Builtin
Add         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Add
      Builtin
Sub         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Sub
      Builtin
Mul         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Mul
      Builtin
Div         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.UDiv
      Builtin
Mod         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.UMod
      Builtin
Pow         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Pow
      Builtin
LAnd        -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
two Annote
an ((Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a Exp
b' -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.And [Annote -> Exp -> Exp
redor Annote
an Exp
a, Annote -> Exp -> Exp
redor Annote
an Exp
b']
      Builtin
LOr         -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
two Annote
an ((Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a Exp
b' -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.Or  [Annote -> Exp -> Exp
redor Annote
an Exp
a, Annote -> Exp -> Exp
redor Annote
an Exp
b']
      Builtin
And         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.And
      Builtin
Or          -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Or
      Builtin
XOr         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.XOr
      Builtin
XNor        -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
two Annote
an ((Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a Exp
b' -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz Op
A.Not [Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz Op
A.XOr [Exp
a, Exp
b']]
      Builtin
LShift      -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Shl
      Builtin
RShift      -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.LShr
      Builtin
RShiftArith -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.AShr
      Builtin
Eq          -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.Eq
      Builtin
Gt          -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.UGt
      Builtin
GtEq        -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.UGe
      Builtin
Lt          -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.ULt
      Builtin
LtEq        -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
A.ULe
      Builtin
LNot        -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an ((Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.Not [Annote -> Exp -> Exp
redor Annote
an Exp
a]
      Builtin
Not         -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an ((Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz Op
A.Not [Exp
a]
      Builtin
RAnd        -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
red Op
A.RedAnd
      Builtin
RNAnd       -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
redNot Op
A.RedAnd
      Builtin
ROr         -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
red Op
A.RedOr
      Builtin
RNor        -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
redNot Op
A.RedOr
      Builtin
RXOr        -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
red Op
A.RedXOr
      Builtin
RXNor       -> Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
redNot Op
A.RedXOr
      Builtin
MSBit       -> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
x -> Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an ((Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a ->
            if Size
w Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>= Size
1 then Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ case Exp
a of
                  A.Var {} -> Annote -> Size -> Size -> Exp -> Exp
A.Slice Annote
an (Size
w Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1) Size
1 Exp
a
                  A.Lit {} -> Annote -> Size -> Size -> Exp -> Exp
A.Slice Annote
an (Size
w Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1) Size
1 Exp
a
                  Exp
_        -> Annote -> Size -> Text -> Exp -> Exp -> Exp
A.Let Annote
an Size
1 Text
x Exp
a (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Size -> Exp -> Exp
A.Slice Annote
an (Size
w Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1) Size
1 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Text -> Exp
A.Var Annote
an Size
w Text
x
            else Text -> Either Text Exp
forall a b. a -> Either a b
Left Text
"MSBit of a zero-width value."
      Builtin
_           -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. Maybe a
Nothing
      where bin :: A.Op -> Maybe (Annote -> A.Name -> [A.Exp] -> Either Text A.Exp)
            bin :: Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
bin Op
op = (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
two Annote
an ((Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a Exp
b' -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz Op
op [Exp
a, Exp
b']

            red :: A.Op -> Maybe (Annote -> A.Name -> [A.Exp] -> Either Text A.Exp)
            red :: Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
red Op
op = (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an ((Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
op [Exp
a]

            redNot :: A.Op -> Maybe (Annote -> A.Name -> [A.Exp] -> Either Text A.Exp)
            redNot :: Op -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
redNot Op
op = (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a. a -> Maybe a
Just ((Annote -> Text -> [Exp] -> Either Text Exp)
 -> Maybe (Annote -> Text -> [Exp] -> Either Text Exp))
-> (Annote -> Text -> [Exp] -> Either Text Exp)
-> Maybe (Annote -> Text -> [Exp] -> Either Text Exp)
forall a b. (a -> b) -> a -> b
$ \ Annote
an Text
_ -> Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an ((Exp -> Either Text Exp) -> [Exp] -> Either Text Exp)
-> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
a -> Exp -> Either Text Exp
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Either Text Exp) -> Exp -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.Not [Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
op [Exp
a]]

            redor :: Annote -> A.Exp -> A.Exp
            redor :: Annote -> Exp -> Exp
redor Annote
an Exp
a = Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.RedOr [Exp
a]

            two :: Annote -> (A.Exp -> A.Exp -> Either Text A.Exp) -> [A.Exp] -> Either Text A.Exp
            two :: Annote
-> (Exp -> Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
two Annote
an Exp -> Exp -> Either Text Exp
k = \ case
                  [Exp
a, Exp
b'] -> Exp -> Exp -> Either Text Exp
k Exp
a Exp
b'
                  [Exp]
es      -> Text -> Either Text Exp
forall a b. a -> Either a b
Left (Text -> Either Text Exp) -> Text -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Text
"primitive arity mismatch at " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Annote -> Text
forall a. TextShow a => a -> Text
showt Annote
an Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (expected 2, got " 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]
es) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")."

            one :: Annote -> (A.Exp -> Either Text A.Exp) -> [A.Exp] -> Either Text A.Exp
            one :: Annote -> (Exp -> Either Text Exp) -> [Exp] -> Either Text Exp
one Annote
an Exp -> Either Text Exp
k = \ case
                  [Exp
a] -> Exp -> Either Text Exp
k Exp
a
                  [Exp]
es  -> Text -> Either Text Exp
forall a b. a -> Either a b
Left (Text -> Either Text Exp) -> Text -> Either Text Exp
forall a b. (a -> b) -> a -> b
$ Text
"primitive arity mismatch at " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Annote -> Text
forall a. TextShow a => a -> Text
showt Annote
an Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (expected 1, got " 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]
es) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")."

resize :: (MonadError AstError m, MonadState S m) => Annote -> A.Size -> A.Exp -> m A.Exp
resize :: forall (m :: * -> *).
(MonadError AstError m, MonadState S m) =>
Annote -> Size -> Exp -> m Exp
resize Annote
an Size
sz Exp
a
      | Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0          = Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> m Exp) -> Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> BV -> Exp
A.Lit Annote
an BV
BV.nil -- (as slice0: no operand survives at width 0)
      | Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
a = Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
a
      | Size
sz Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
>  Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
a = Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> m Exp) -> Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz (Size -> Op
A.ZExt Size
sz) [Exp
a]
      | Bool
otherwise        = Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> m Exp) -> Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
sz (Size -> Op
A.Trunc Size
sz) [Exp
a]

---
--- Externs.
---

-- | Declare (or merge) the extern and apply it: a combinational extern
--   becomes an XCall; a clocked one becomes an XCall too, to be hoisted
--   into a device-level instance by hoistInstances. The model argument is
--   attached to the declaration when usable.
applyExtern :: forall m. MonadError AstError m => Annote -> A.Size -> ([Exp], Text, Text, [Exp], [Exp], Text) -> Exp -> [A.Exp] -> TM m A.Exp
applyExtern :: forall (m :: * -> *).
MonadError AstError m =>
Annote
-> Size
-> ([Exp], Text, Text, [Exp], [Exp], Text)
-> Exp
-> [Exp]
-> TM m Exp
applyExtern Annote
an Size
sz ([Exp]
ps, Text
clk, Text
rst, [Exp]
as, [Exp]
rs, Text
s) Exp
a [Exp]
args = do
      model <- case Exp
a of
            Var Annote
_ Id
x
                  | Text -> Bool
T.null Text
clk Bool -> Bool -> Bool
&& Text -> Bool
T.null Text
rst -> Maybe Text -> StateT S m (Maybe Text)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Text -> StateT S m (Maybe Text))
-> Maybe Text -> StateT S m (Maybe Text)
forall a b. (a -> b) -> a -> b
$ Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Id -> Text
idOcc Id
x
                  | Bool
otherwise                -> do
                        Annote -> Text -> StateT S m ()
forall (m :: * -> *). MonadState S m => Annote -> Text -> m ()
addWarning Annote
an (Text -> StateT S m ()) -> Text -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ Text
"Ignoring the Haskell model for clocked extern '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s
                                     Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"': clocked externs are stateful and cannot be modeled by a pure function."
                        Maybe Text -> StateT S m (Maybe Text)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Text
forall a. Maybe a
Nothing
            (Exp -> (Exp, [Arg])
flattenApp -> (Prim Annote
_ Ty
_ Builtin
Error, [Arg]
_)) -> Maybe Text -> StateT S m (Maybe Text)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Text
forall a. Maybe a
Nothing -- The neutered placeholder.
            Exp
_ -> do
                  Annote -> Text -> StateT S m ()
forall (m :: * -> *). MonadState S m => Annote -> Text -> m ()
addWarning Annote
an (Text -> StateT S m ()) -> Text -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ Text
"Ignoring the Haskell model for extern '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s
                               Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"': the model reference did not survive transformation (rwc bug?)."
                  Maybe Text -> StateT S m (Maybe Text)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Text
forall a. Maybe a
Nothing

      let kind | Text -> Bool
T.null Text
clk Bool -> Bool -> Bool
&& Text -> Bool
T.null Text
rst = ExternKind
A.Comb
               | Bool
otherwise                = Maybe Text -> Maybe Text -> ExternKind
A.Seq (Text -> Maybe Text
mb Text
clk) (Text -> Maybe Text
mb Text
rst)
          (gnames, gvals) = unzip $ generics ps
          argSzs   = (Exp -> Size) -> [Exp] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf [Exp]
args
          ins      = Int -> [(Text, Size)] -> [(Text, Size)]
named (ExternKind -> Int
portOffset ExternKind
kind) ([(Text, Size)] -> [(Text, Size)])
-> [(Text, Size)] -> [(Text, Size)]
forall a b. (a -> b) -> a -> b
$ [(Text, Size)] -> Maybe [(Text, Size)] -> [(Text, Size)]
forall a. a -> Maybe a -> a
fromMaybe ((Size -> (Text, Size)) -> [Size] -> [(Text, Size)]
forall a b. (a -> b) -> [a] -> [b]
map (Text
forall a. Monoid a => a
mempty, ) [Size]
argSzs) (Maybe [(Text, Size)] -> [(Text, Size)])
-> Maybe [(Text, Size)] -> [(Text, Size)]
forall a b. (a -> b) -> a -> b
$ [Exp] -> Maybe [(Text, Size)]
ports [Exp]
as
          outs     = Int -> [(Text, Size)] -> [(Text, Size)]
named (ExternKind -> Int
portOffset ExternKind
kind Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(Text, Size)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Text, Size)]
ins) ([(Text, Size)] -> [(Text, Size)])
-> [(Text, Size)] -> [(Text, Size)]
forall a b. (a -> b) -> a -> b
$ [(Text, Size)] -> Maybe [(Text, Size)] -> [(Text, Size)]
forall a. a -> Maybe a -> a
fromMaybe [(Text
forall a. Monoid a => a
mempty, Size
sz)] (Maybe [(Text, Size)] -> [(Text, Size)])
-> Maybe [(Text, Size)] -> [(Text, Size)]
forall a b. (a -> b) -> a -> b
$ [Exp] -> Maybe [(Text, Size)]
ports [Exp]
rs
          decl     = Annote
-> Text
-> [Text]
-> ExternKind
-> [(Text, Size)]
-> [(Text, Size)]
-> Maybe Text
-> Extern
A.Extern Annote
an Text
s [Text]
gnames ExternKind
kind [(Text, Size)]
ins [(Text, Size)]
outs Maybe Text
model

      old <- gets $ Map.lookup s . sExterns
      decl' <- maybe (pure decl) (mergeExt decl) old
      modify $ \ S
st -> S
st { sExterns = Map.insert s decl' $ sExterns st }
      pure $ A.XCall an sz s gvals args
      where mb :: Text -> Maybe A.Name
            mb :: Text -> Maybe Text
mb Text
x | Text -> Bool
T.null Text
x  = Maybe Text
forall a. Maybe a
Nothing
                 | Bool
otherwise = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
x

            -- | Generic parameters: (name, value) pairs from the descriptor.
            generics :: [Exp] -> [(A.Name, Natural)]
            generics :: [Exp] -> [(Text, Natural)]
generics = (Int -> Exp -> (Text, Natural))
-> [Int] -> [Exp] -> [(Text, Natural)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Exp -> (Text, Natural)
forall {b} {a}. (Num b, TextShow a) => a -> Exp -> (Text, b)
generic [Int
0 :: Int ..]
                  where generic :: a -> Exp -> (Text, b)
generic a
i Exp
e = case Exp -> Maybe (Text, Integer)
pair Exp
e of
                              Just (Text
p, Integer
v) | Bool -> Bool
not (Text -> Bool
T.null Text
p) -> (Text
p, Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
                                          | Bool
otherwise      -> (Text
"g" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. TextShow a => a -> Text
showt a
i, Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
                              Maybe (Text, Integer)
_                            -> (Text
"g" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. TextShow a => a -> Text
showt a
i, b
0)

            pair :: Exp -> Maybe (Text, Integer)
            pair :: Exp -> Maybe (Text, Integer)
pair Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Con Annote
_ Ty
_ Text
"(,)", [EArg (LitStr Annote
_ Text
p), EArg (LitInt Annote
_ Ty
_ Integer
v)]) -> (Text, Integer) -> Maybe (Text, Integer)
forall a. a -> Maybe a
Just (Text
p, Integer
v)
                  (Exp, [Arg])
_                                                         -> Maybe (Text, Integer)
forall a. Maybe a
Nothing

            ports :: [Exp] -> Maybe [(Text, A.Size)]
            ports :: [Exp] -> Maybe [(Text, Size)]
ports = \ case
                  [] -> Maybe [(Text, Size)]
forall a. Maybe a
Nothing
                  [Exp]
es -> (Exp -> Maybe (Text, Size)) -> [Exp] -> Maybe [(Text, Size)]
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, Integer) -> (Text, Size))
-> Maybe (Text, Integer) -> Maybe (Text, Size)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Integer -> Size) -> (Text, Integer) -> (Text, Size)
forall a b. (a -> b) -> (Text, a) -> (Text, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral) (Maybe (Text, Integer) -> Maybe (Text, Size))
-> (Exp -> Maybe (Text, Integer)) -> Exp -> Maybe (Text, Size)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe (Text, Integer)
pair) [Exp]
es

            portOffset :: A.ExternKind -> Int
            portOffset :: ExternKind -> Int
portOffset = \ case
                  ExternKind
A.Comb      -> Int
0
                  A.Seq Maybe Text
mc Maybe Text
mr -> [Maybe Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Maybe Text] -> Int) -> [Maybe Text] -> Int
forall a b. (a -> b) -> a -> b
$ (Maybe Text -> Bool) -> [Maybe Text] -> [Maybe Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Text
forall a. Maybe a
Nothing) [Maybe Text
mc, Maybe Text
mr]

            -- | Anonymous ports are named p<i> by their position in the
            --   clock-reset-inputs-outputs list (the established convention).
            named :: Int -> [(Text, A.Size)] -> [(A.Name, A.Size)]
            named :: Int -> [(Text, Size)] -> [(Text, Size)]
named Int
off = (Int -> (Text, Size) -> (Text, Size))
-> [Int] -> [(Text, Size)] -> [(Text, Size)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i (Text
p, Size
psz) -> (if Text -> Bool
T.null Text
p then Text
"p" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. TextShow a => a -> Text
showt Int
i else Text
p, Size
psz)) [Int
off ..]

            mergeExt :: A.Extern -> A.Extern -> TM m A.Extern
            mergeExt :: Extern -> Extern -> StateT S m Extern
mergeExt Extern
new Extern
old
                  | Extern -> ExternKind
A.extKind Extern
new ExternKind -> ExternKind -> Bool
forall a. Eq a => a -> a -> Bool
== Extern -> ExternKind
A.extKind Extern
old
                  , Extern -> [(Text, Size)]
A.extInputs Extern
new [(Text, Size)] -> [(Text, Size)] -> Bool
forall a. Eq a => a -> a -> Bool
== Extern -> [(Text, Size)]
A.extInputs Extern
old
                  , Extern -> [(Text, Size)]
A.extOutputs Extern
new [(Text, Size)] -> [(Text, Size)] -> Bool
forall a. Eq a => a -> a -> Bool
== Extern -> [(Text, Size)]
A.extOutputs Extern
old
                  , Extern -> [Text]
A.extGenerics Extern
new [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== Extern -> [Text]
A.extGenerics Extern
old = case (Extern -> Maybe Text
A.extModel Extern
new, Extern -> Maybe Text
A.extModel Extern
old) of
                        (Just Text
g1, Just Text
g2) | Text
g1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
g2 -> Annote -> Text -> StateT S m Extern
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> StateT S m Extern) -> Text -> StateT S m Extern
forall a b. (a -> b) -> a -> b
$ Text
"Extern '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' has conflicting models (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
g1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
g2 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")."
                        (Maybe Text
mg, Maybe Text
mg')                     -> Extern -> StateT S m Extern
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Extern -> StateT S m Extern) -> Extern -> StateT S m Extern
forall a b. (a -> b) -> a -> b
$ Extern
old { A.extModel = maybe mg' Just mg }
                  | Bool
otherwise = Annote -> Text -> [Label] -> [Text] -> StateT S m Extern
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> [Label] -> [Text] -> m a
failAtWith Annote
an (Text
"Extern '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' is used with inconsistent signatures.")
                        [(Extern -> Annote
forall a. Annotated a => a -> Annote
ann Extern
old, Text
"First used here:")] []

---
--- The machine fold.
---

-- | The step-record accounting for one process (see the module header for
--   the layout).
data Layout = Layout
      { Layout -> Size
loRecW    :: !A.Size                      -- ^ Total record width.
      , Layout -> Size
loPTagW   :: !A.Size                      -- ^ The halted flag: 1 if a halt is reachable, else 0.
      , Layout -> Size
loOutW    :: !A.Size
      , Layout -> Size
loRTagW   :: !A.Size                      -- ^ Label tag width.
      , Layout -> Size
loRPayW   :: !A.Size                      -- ^ Max summed pause-argument width.
      , Layout -> [(Text, Size)]
loCells   :: ![(Text, A.Size)]            -- ^ Cell names and widths, in declaration order.
      , Layout -> [(Int, Integer, [Size])]
loTargets :: ![(Uniq, Integer, [A.Size])] -- ^ Pause targets: unique, tag value, argument widths.
      , Layout -> HashMap Text (Integer, Size)
loHalts   :: !(HashMap Text (Integer, A.Size)) -- ^ Halt answer types (by 'haltKey'): tag value and width.
      , Layout -> Size
loATagW   :: !A.Size
      , Layout -> Size
loAPayW   :: !A.Size
      }

loRW, loCellsW, loAW :: Layout -> A.Size
loRW :: Layout -> Size
loRW Layout
l     = Layout -> Size
loRTagW Layout
l Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Layout -> Size
loRPayW Layout
l
loCellsW :: Layout -> Size
loCellsW Layout
l = [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
$ Layout -> [(Text, Size)]
loCells Layout
l
loAW :: Layout -> Size
loAW Layout
l     = Layout -> Size
loATagW Layout
l Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Layout -> Size
loAPayW Layout
l

-- | The key of a halt answer type in the layout's halt table: the type
--   rendered after nat normalization, so that two spellings of one type
--   (@Vec (+ 7 1) Bool@ and @Vec 8 Bool@, from a generic definition and
--   its call site) share one answer tag — the equality the lint and the
--   certify validator use.
haltKey :: Ty -> Text
haltKey :: Ty -> Text
haltKey = Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Ty -> Text) -> (Ty -> Ty) -> Ty -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Ty
forall d. Data d => d -> d
Ann.unAnn (Ty -> Ty) -> (Ty -> Ty) -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Ty
natNorm

mkLayout :: MonadError AstError m => Env -> Proc -> TM m Layout
mkLayout :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Proc -> TM m Layout
mkLayout Env
env Proc
pr = do
      outW  <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"proc output" (Proc -> Annote
procAnnote Proc
pr) (Ty -> TM m Size) -> Ty -> TM m Size
forall a b. (a -> b) -> a -> b
$ Proc -> Ty
procOutTy Proc
pr
      cells <- mapM (\ Cell
c -> (Cell -> Text
cellName Cell
c, ) (Size -> (Text, Size)) -> TM m Size -> StateT S m (Text, Size)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"cell" (Cell -> Annote
cellAnnote Cell
c) (Cell -> Ty
cellTy Cell
c)) $ procCells pr
      targets <- mapM (\ (Int
i, (Id
l, Block
b)) -> do
                  szs <- (Id -> TM m Size) -> [Id] -> StateT S m [Size]
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 -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"pause target param" (Block -> Annote
blkAnnote Block
b) (Ty -> TM m Size) -> (Id -> Ty) -> Id -> TM m Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sig -> Ty
sigTy (Sig -> Ty) -> (Id -> Sig) -> Id -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Sig
idSig) ([Id] -> StateT S m [Size]) -> [Id] -> StateT S m [Size]
forall a b. (a -> b) -> a -> b
$ [Id] -> [Id]
forall a. [a] -> [a]
initSafe ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ Block -> [Id]
blkParams Block
b
                  pure (idUniq l, toInteger i, szs))
            $ zip [0 :: Int ..] [ (l, b) | (l, b) <- procBlocks pr, idUniq l `Set.member` pauseTargets ]
      haltSzs <- mapM (\ Ty
t -> (Ty -> Text
haltKey Ty
t, ) (Size -> (Text, Size)) -> TM m Size -> StateT S m (Text, Size)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"halt answer" (Proc -> Annote
procAnnote Proc
pr) Ty
t) haltTys
      let haltList = [(Text, Size)] -> [(Text, Size)]
forall a. Ord a => [a] -> [a]
nubOrd [(Text, Size)]
haltSzs
          rTagW  = Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Size) -> Natural -> Size
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
nbits (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ [(Int, Integer, [Size])] -> Natural
forall i a. Num i => [a] -> i
genericLength [(Int, Integer, [Size])]
targets
          rPayW  = [Size] -> Size
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ Size
0 Size -> [Size] -> [Size]
forall a. a -> [a] -> [a]
: [ [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Size]
szs | (Int
_, Integer
_, [Size]
szs) <- [(Int, Integer, [Size])]
targets ]
          aTagW  = Natural -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Size) -> Natural -> Size
forall a b. (a -> b) -> a -> b
$ Natural -> Natural
nbits (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ [(Text, Size)] -> Natural
forall i a. Num i => [a] -> i
genericLength [(Text, Size)]
haltList
          aPayW  = [Size] -> Size
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Size] -> Size) -> [Size] -> Size
forall a b. (a -> b) -> a -> b
$ Size
0 Size -> [Size] -> [Size]
forall 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 [(Text, Size)]
haltList
          pTagW  = if [(Text, Size)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Text, Size)]
haltList then Size
0 else Size
1
          cellsW = [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)]
cells
          pauseLoad = Size
outW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
rTagW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
rPayW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
cellsW
          doneLoad  = Size
aTagW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
aPayW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
cellsW
          recW   = Size
pTagW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size -> Size -> Size
forall a. Ord a => a -> a -> a
max Size
pauseLoad (if [(Text, Size)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Text, Size)]
haltList then Size
0 else Size
doneLoad)
      pure $ Layout { loRecW  = recW,  loPTagW = pTagW, loOutW  = outW
                    , loRTagW = rTagW, loRPayW = rPayW, loCells = cells
                    , loTargets = targets
                    , loHalts = Map.fromList [ (k, (i, w)) | (i, (k, w)) <- zip [0 ..] haltList ]
                    , loATagW = aTagW, loAPayW = aPayW
                    }
      where blocks :: [Block]
            blocks :: [Block]
blocks = Proc -> Block
procEntry Proc
pr Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
: ((Id, Block) -> Block) -> [(Id, Block)] -> [Block]
forall a b. (a -> b) -> [a] -> [b]
map (Id, Block) -> Block
forall a b. (a, b) -> b
snd (Proc -> [(Id, Block)]
procBlocks Proc
pr)

            pauseTargets :: HashSet Uniq
            pauseTargets :: HashSet Int
pauseTargets = [Int] -> HashSet Int
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList ([Int] -> HashSet Int) -> [Int] -> HashSet Int
forall a b. (a -> b) -> a -> b
$ (Block -> [Int]) -> [Block] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Term -> [Int]
pt (Term -> [Int]) -> (Block -> Term) -> Block -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> Term
blkTerm) [Block]
blocks
                  where pt :: Term -> [Uniq]
                        pt :: Term -> [Int]
pt = \ case
                              Pause Annote
_ Exp
_ Id
l [Exp]
_  -> [Id -> Int
idUniq Id
l]
                              TCase Annote
_ Exp
_ [TAlt]
alts -> [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Term -> [Int]
pt Term
t | TAlt Annote
_ AltCon
_ [Id]
_ Term
t <- [TAlt]
alts ]
                              Term
_              -> []

            haltTys :: [Ty]
            haltTys :: [Ty]
haltTys = (Block -> [Ty]) -> [Block] -> [Ty]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Term -> [Ty]
ht (Term -> [Ty]) -> (Block -> Term) -> Block -> [Ty]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> Term
blkTerm) [Block]
blocks
                  where ht :: Term -> [Ty]
                        ht :: Term -> [Ty]
ht = \ case
                              Halt Annote
_ Exp
a       -> [Exp -> Ty
typeOf Exp
a]
                              TCase Annote
_ Exp
_ [TAlt]
alts -> [[Ty]] -> [Ty]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Term -> [Ty]
ht Term
t | TAlt Annote
_ AltCon
_ [Id]
_ Term
t <- [TAlt]
alts ]
                              Term
_              -> []

            initSafe :: [a] -> [a]
            initSafe :: forall a. [a] -> [a]
initSafe = \ case
                  [] -> []
                  [a]
xs -> [a] -> [a]
forall a. HasCallStack => [a] -> [a]
init [a]
xs

-- | The step record for a pause: @halted=Pause | pad | out | tag | pad | args | cells@.
buildPause :: MonadError AstError m => Layout -> Annote -> A.Exp -> Uniq -> [A.Exp] -> [A.Exp] -> TM m A.Exp
buildPause :: forall (m :: * -> *).
MonadError AstError m =>
Layout -> Annote -> Exp -> Int -> [Exp] -> [Exp] -> TM m Exp
buildPause Layout
lo Annote
an Exp
o Int
tgt [Exp]
args [Exp]
cells = do
      tagv <- case [ Integer
v | (Int
u, Integer
v, [Size]
_) <- Layout -> [(Int, Integer, [Size])]
loTargets Layout
lo, Int
u Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tgt ] of
            [Integer
v] -> Integer -> StateT S m Integer
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
v
            [Integer]
_   -> Annote -> Text -> StateT S m Integer
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"pause to an unknown label (rwc bug)."
      let padW  = Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loRecW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loPTagW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loOutW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loRW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loCellsW Layout
lo) :: Integer
          rPadW = Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loRPayW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([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
$ (Exp -> Size) -> [Exp] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf [Exp]
args) :: Integer
      pure $ A.cat $ [ A.Lit an $ bitVec (fromIntegral $ loPTagW lo) (1 :: Integer) | loPTagW lo > 0 ]
                  <> [ A.Lit an $ zeros $ fromIntegral padW ]
                  <> [ o ]
                  <> [ A.Lit an $ bitVec (fromIntegral $ loRTagW lo) tagv | loRTagW lo > 0 ]
                  <> [ A.Lit an $ zeros $ fromIntegral rPadW ]
                  <> args <> cells

-- | The step record for a halt: @halted=Done | pad | A-tag | pad | answer | cells@.
buildHalt :: MonadError AstError m => Layout -> Annote -> Ty -> A.Exp -> [A.Exp] -> TM m A.Exp
buildHalt :: forall (m :: * -> *).
MonadError AstError m =>
Layout -> Annote -> Ty -> Exp -> [Exp] -> TM m Exp
buildHalt Layout
lo Annote
an Ty
aty Exp
a [Exp]
cells = do
      (tagv, _) <- StateT S m (Integer, Size)
-> ((Integer, Size) -> StateT S m (Integer, Size))
-> Maybe (Integer, Size)
-> StateT S m (Integer, Size)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> StateT S m (Integer, Size)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"halt at an unknown answer type (rwc bug).") (Integer, Size) -> StateT S m (Integer, Size)
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (Maybe (Integer, Size) -> StateT S m (Integer, Size))
-> Maybe (Integer, Size) -> StateT S m (Integer, Size)
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text (Integer, Size) -> Maybe (Integer, Size)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Ty -> Text
haltKey Ty
aty) (HashMap Text (Integer, Size) -> Maybe (Integer, Size))
-> HashMap Text (Integer, Size) -> Maybe (Integer, Size)
forall a b. (a -> b) -> a -> b
$ Layout -> HashMap Text (Integer, Size)
loHalts Layout
lo
      let padW  = Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loRecW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loPTagW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loAW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loCellsW Layout
lo) :: Integer
          aPadW = Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loAPayW Layout
lo) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Size -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
a) :: Integer
      pure $ A.cat $ [ A.Lit an $ bitVec (fromIntegral $ loPTagW lo) (0 :: Integer) | loPTagW lo > 0 ]
                  <> [ A.Lit an $ zeros $ fromIntegral padW ]
                  <> [ A.Lit an $ bitVec (fromIntegral $ loATagW lo) tagv | loATagW lo > 0 ]
                  <> [ A.Lit an $ zeros $ fromIntegral aPadW ]
                  <> [ a ] <> cells

-- | Translate one process into its Hyle definitions and the device.
transProc :: forall m. MonadError AstError m => Config -> Env -> HashMap Text Int -> Proc -> [A.Defn] -> TM m A.Program
transProc :: forall (m :: * -> *).
MonadError AstError m =>
Config -> Env -> HashMap Text Int -> Proc -> [Defn] -> TM m Program
transProc Config
conf Env
env HashMap Text Int
used0 Proc
pr [Defn]
pureDefns = do
      lo <- Env -> Proc -> TM m Layout
forall (m :: * -> *).
MonadError AstError m =>
Env -> Proc -> TM m Layout
mkLayout Env
env Proc
pr
      let qual Text
n = Proc -> Text
procName Proc
pr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
          -- Block definitions are named from their labels' display bases
          -- ('$L.Main.getIns' -> 'main.getIns'), disambiguated in
          -- deterministic block order against the whole global namespace
          -- (pure defns, Cryptol entries, externs, the other blocks);
          -- dispatch order and tag values key on the labels' uniques, so
          -- naming is display-only. Under --stable-names the label's
          -- unique key is appended instead: always collision-free and
          -- machine-greppable, at the cost of readability.
          (blockGids, used1)
                | conf^.stableNames = ( IM.fromList [ (idUniq l, qual $ idOcc l <> "$" <> showt (idUniq l)) | (l, _) <- procBlocks pr ]
                                      , used0 )
                | otherwise         = foldl' (\ (IntMap Text
m, HashMap Text Int
u) (Id
l, Block
_) ->
                                          let (Text
nm, HashMap Text Int
u') = Text -> HashMap Text Int -> Text -> (Text, HashMap Text Int)
pickFresh Text
"" HashMap Text Int
u (Text -> (Text, HashMap Text Int))
-> Text -> (Text, HashMap Text Int)
forall a b. (a -> b) -> a -> b
$ Text -> Text
qual (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
labelBase (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Id -> Text
idOcc Id
l
                                          in (Int -> Text -> IntMap Text -> IntMap Text
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (Id -> Int
idUniq Id
l) Text
nm IntMap Text
m, HashMap Text Int
u'))
                                          (mempty, used0) (procBlocks pr)
          (entryGid, used2)   = pickFresh "" used1 $ qual "$entry"
          (dispatchGid, _)    = pickFresh "" used2 $ qual "$dispatch"
          blockGid Id
l = Text -> Int -> IntMap Text -> Text
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault (Text -> Text
qual (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Id -> Text
idOcc Id
l) (Id -> Int
idUniq Id
l) IntMap Text
blockGids
          -- Display names for the resumption-tag values: the pause-target
          -- blocks' GIds with the process qualification stripped, in tag
          -- order. Rendered as the device's 'tag' lines and the dispatch
          -- defn's doc line.
          stripQual Text
g = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
g (Maybe Text -> Text) -> Maybe Text -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Maybe Text
T.stripPrefix (Proc -> Text
procName Proc
pr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".") Text
g
          tagDisplay = [ (Text -> Text
stripQual (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Int -> IntMap Text -> Text
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault Text
"" Int
u IntMap Text
blockGids, Integer
v)
                       | (Int
u, Integer
v, [Size]
_) <- ((Int, Integer, [Size]) -> Integer)
-> [(Int, Integer, [Size])] -> [(Int, Integer, [Size])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\ (Int
_, Integer
v, [Size]
_) -> Integer
v) ([(Int, Integer, [Size])] -> [(Int, Integer, [Size])])
-> [(Int, Integer, [Size])] -> [(Int, Integer, [Size])]
forall a b. (a -> b) -> a -> b
$ Layout -> [(Int, Integer, [Size])]
loTargets Layout
lo ]
          blockDoc Id
l = case [ Integer
v | (Int
u, Integer
v, [Size]
_) <- Layout -> [(Int, Integer, [Size])]
loTargets Layout
lo, Int
u Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Id -> Int
idUniq Id
l ] of
                [Integer
v] -> [ Text
"block '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
l Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Proc -> Text
procName Proc
pr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (state " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
forall a. TextShow a => a -> Text
showt Integer
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" ]
                [Integer]
_   -> [ Text
"block '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
l Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Proc -> Text
procName Proc
pr ]

      inW <- sizeOf env "proc input" (procAnnote pr) $ procInTy pr

      blockDefns <- mapM (\ (Id
l, Block
b) -> Layout
-> Text -> (Id -> Text) -> [Text] -> Block -> StateT S m Defn
transBlock Layout
lo (Id -> Text
blockGid Id
l) Id -> Text
blockGid (Id -> [Text]
blockDoc Id
l) Block
b) $ procBlocks pr
      entryDefn  <- transBlock lo entryGid blockGid [ "entry block of process " <> procName pr ] $ procEntry pr
      dispatch   <- dispatchDefn lo dispatchGid blockGid inW tagDisplay

      exts <- gets $ sortOn A.extName . Map.elems . sExterns
      dev  <- mkDeviceM lo inW entryDefn dispatch (blockDefns <> pureDefns) exts tagDisplay

      hoistInstances $ A.Program exts (dispatch : blockDefns <> pureDefns) dev
      where -- | A block becomes one definition: parameters, then the cells
            --   as trailing parameters; commands become lets; the
            --   terminator builds the step record (pause/halt) or
            --   tail-calls the target block (goto).
            transBlock :: Layout -> A.GId -> (Id -> A.GId) -> [Text] -> Block -> TM m A.Defn
            transBlock :: Layout
-> Text -> (Id -> Text) -> [Text] -> Block -> StateT S m Defn
transBlock Layout
lo Text
gid Id -> Text
blockGid [Text]
doc (Block Annote
an [Id]
ps [Cmd]
cmds Term
term) = do
                  (S -> S) -> StateT S m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S m ()) -> (S -> S) -> StateT S m ()
forall a b. (a -> b) -> a -> b
$ \ S
s -> S
s { sCtr = 0 }
                  pSzs <- (Id -> TM m Size) -> [Id] -> StateT S m [Size]
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 -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"block param" Annote
an (Ty -> TM m Size) -> (Id -> Ty) -> Id -> TM m Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sig -> Ty
sigTy (Sig -> Ty) -> (Id -> Sig) -> Id -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Sig
idSig) [Id]
ps
                  let (sc0, pnames)   = bindParams an scope0 (zip ps pSzs)
                      (sc1, cellNms)  = foldl' (\ (Scope
s, [(Text, Text, Size)]
acc) (Text
c, Size
w) ->
                                          let (Scope
s', Text
nm) = Scope -> Text -> (Scope, Text)
scopeName Scope
s Text
c in (Scope
s', [(Text, Text, Size)]
acc [(Text, Text, Size)]
-> [(Text, Text, Size)] -> [(Text, Text, Size)]
forall a. Semigroup a => a -> a -> a
<> [(Text
c, Text
nm, Size
w)]))
                                          (sc0, []) (loCells lo)
                      cellAtoms       = [(Text, Exp)] -> HashMap Text Exp
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Text
c, Annote -> Size -> Text -> Exp
A.Var Annote
an Size
w Text
nm) | (Text
c, Text
nm, Size
w) <- [(Text, Text, Size)]
cellNms ]
                  body <- goCmds lo blockGid sc1 cellAtoms cmds term
                  pure $ A.Defn an gid (A.Sig an (pSzs <> map snd (loCells lo)) (loRecW lo)) (pnames <> [ nm | (_, nm, _) <- cellNms ]) body False (A.Blind doc)

            goCmds :: Layout -> (Id -> A.GId) -> Scope -> HashMap Text A.Exp -> [Cmd] -> Term -> TM m A.Exp
            goCmds :: Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid Scope
sc HashMap Text Exp
cells = \ case
                  [] -> Layout
-> (Id -> Text) -> Scope -> HashMap Text Exp -> Term -> TM m Exp
transTerm Layout
lo Id -> Text
blockGid Scope
sc HashMap Text Exp
cells
                  (CmdBind Annote
an Id
x Exp
e : [Cmd]
rest) -> \ Term
term -> do
                        e' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
e
                        case e' of
                              A.Lit {} -> Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid (Scope
sc { scMap = IM.insert (idUniq x) e' $ scMap sc }) HashMap Text Exp
cells [Cmd]
rest Term
term
                              A.Var {} -> Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid (Scope
sc { scMap = IM.insert (idUniq x) e' $ scMap sc }) HashMap Text Exp
cells [Cmd]
rest Term
term
                              Exp
_        -> do
                                    let (Scope
sc', Text
nm) = Annote -> Scope -> Id -> Size -> (Scope, Text)
bindLocal Annote
an Scope
sc Id
x (Size -> (Scope, Text)) -> Size -> (Scope, Text)
forall a b. (a -> b) -> a -> b
$ Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
e'
                                    body <- Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid Scope
sc' HashMap Text Exp
cells [Cmd]
rest Term
term
                                    pure $ A.Let an (A.sizeOf body) nm e' body
                  (CmdGet Annote
_ Id
x Text
c : [Cmd]
rest) -> \ Term
term -> do
                        atom <- TM m Exp -> (Exp -> TM m Exp) -> Maybe Exp -> TM m Exp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal (Proc -> Annote
procAnnote Proc
pr) Text
"get from an unknown cell (rwc bug).") Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                              (Maybe Exp -> TM m Exp) -> Maybe Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text Exp -> Maybe Exp
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
c HashMap Text Exp
cells
                        goCmds lo blockGid (sc { scMap = IM.insert (idUniq x) atom $ scMap sc }) cells rest term
                  (CmdPut Annote
an Text
c Exp
e : [Cmd]
rest) -> \ Term
term -> do
                        e' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
e
                        case e' of
                              A.Lit {} -> Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid Scope
sc (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
c Exp
e' HashMap Text Exp
cells) [Cmd]
rest Term
term
                              A.Var {} -> Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid Scope
sc (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
c Exp
e' HashMap Text Exp
cells) [Cmd]
rest Term
term
                              Exp
_        -> do
                                    let (Scope
sc', Text
nm) = Scope -> Text -> (Scope, Text)
scopeName Scope
sc Text
c
                                    body <- Layout
-> (Id -> Text)
-> Scope
-> HashMap Text Exp
-> [Cmd]
-> Term
-> TM m Exp
goCmds Layout
lo Id -> Text
blockGid Scope
sc' (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
c (Annote -> Size -> Text -> Exp
A.Var Annote
an (Exp -> Size
forall a. SizeAnnotated a => a -> Size
A.sizeOf Exp
e') Text
nm) HashMap Text Exp
cells) [Cmd]
rest Term
term
                                    pure $ A.Let an (A.sizeOf body) nm e' body

            transTerm :: Layout -> (Id -> A.GId) -> Scope -> HashMap Text A.Exp -> Term -> TM m A.Exp
            transTerm :: Layout
-> (Id -> Text) -> Scope -> HashMap Text Exp -> Term -> TM m Exp
transTerm Layout
lo Id -> Text
blockGid Scope
sc HashMap Text Exp
cells Term
term = case Term
term of
                  Pause Annote
an Exp
o Id
l [Exp]
es -> do
                        o'  <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
o
                        es' <- mapM (transExp env sc) es
                        buildPause lo an o' (idUniq l) es' $ cellVals cells
                  Goto Annote
an Id
l [Exp]
es    -> do
                        es' <- (Exp -> TM m Exp) -> [Exp] -> StateT S 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 (Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc) [Exp]
es
                        pure $ A.Call an (loRecW lo) (blockGid l) $ es' <> cellVals cells
                  Halt Annote
an Exp
a       -> do
                        a' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
a
                        buildHalt lo an (typeOf a) a' $ cellVals cells
                  TCase Annote
an Exp
scrut [TAlt]
alts -> do
                        scrut' <- Env -> Scope -> Exp -> TM m Exp
forall (m :: * -> *).
MonadError AstError m =>
Env -> Scope -> Exp -> TM m Exp
transExp Env
env Scope
sc Exp
scrut
                        bindAtom (ann scrut) scrut' $ \ Exp
datom ->
                              Env
-> Scope
-> Annote
-> Size
-> Ty
-> Exp
-> [(Annote, AltCon, [Id], Term)]
-> (Scope -> Term -> TM m Exp)
-> TM m Exp
forall (m :: * -> *) body.
MonadError AstError m =>
Env
-> Scope
-> Annote
-> Size
-> Ty
-> Exp
-> [(Annote, AltCon, [Id], body)]
-> (Scope -> body -> TM m Exp)
-> TM m Exp
caseChain Env
env Scope
sc Annote
an (Layout -> Size
loRecW Layout
lo) (Exp -> Ty
typeOf Exp
scrut) Exp
datom
                                    [ (Annote
aan, AltCon
c, [Id]
xs, Term
t) | TAlt Annote
aan AltCon
c [Id]
xs Term
t <- [TAlt]
alts ]
                                    (\ Scope
sc' Term
t -> Layout
-> (Id -> Text) -> Scope -> HashMap Text Exp -> Term -> TM m Exp
transTerm Layout
lo Id -> Text
blockGid Scope
sc' HashMap Text Exp
cells Term
t)
                  where cellVals :: HashMap Text A.Exp -> [A.Exp]
                        cellVals :: HashMap Text Exp -> [Exp]
cellVals HashMap Text Exp
m = [ Exp -> Maybe Exp -> Exp
forall a. a -> Maybe a -> a
fromMaybe (Annote -> BV -> Exp
A.Lit Annote
noAnn (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
w) (Maybe Exp -> Exp) -> Maybe Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text Exp -> Maybe Exp
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
c HashMap Text Exp
m | (Text
c, Size
w) <- Layout -> [(Text, Size)]
loCells Layout
lo ]

            -- | @dispatch (label-tag | args | cells) i@: an if-chain over
            --   the label tag calling the pause-target blocks.
            dispatchDefn :: Layout -> A.GId -> (Id -> A.GId) -> A.Size -> [(Text, Integer)] -> TM m A.Defn
            dispatchDefn :: Layout
-> Text
-> (Id -> Text)
-> Size
-> [(Text, Integer)]
-> StateT S m Defn
dispatchDefn Layout
lo Text
gid Id -> Text
blockGid Size
inW [(Text, Integer)]
tagDisplay = do
                  let an :: Annote
an     = Proc -> Annote
procAnnote Proc
pr
                      stW :: Size
stW    = Layout -> Size
loRW Layout
lo Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Layout -> Size
loCellsW Layout
lo
                      disc :: Exp
disc   = Annote -> Size -> Text -> Exp
A.Var Annote
an Size
stW Text
"disc"
                      i :: Exp
i      = Annote -> Size -> Text -> Exp
A.Var Annote
an Size
inW Text
"i"
                      cellsW :: Size
cellsW = Layout -> Size
loCellsW Layout
lo
                      tag :: Exp
tag    = Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an (Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Layout -> Size
loRPayW Layout
lo) Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
cellsW) (Layout -> Size
loRTagW Layout
lo) Exp
disc
                      cellSlices :: [Exp]
cellSlices = [ Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an Size
off Size
w Exp
disc | ((), Size
w, Size
off) <- [((), Size)] -> [((), Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets [ ((), Size
w) | (Text
_, Size
w) <- Layout -> [(Text, Size)]
loCells Layout
lo ] ]
                      -- Arguments live LSB-aligned under the tag.
                      argSlices :: [Size] -> [Exp]
argSlices [Size]
szs = [ Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an (Size
off Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
cellsW) Size
w Exp
disc | ((), Size
w, Size
off) <- [((), Size)] -> [((), Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets [ ((), Size
w) | Size
w <- [Size]
szs ] ]
                      gidMap :: IntMap Text
gidMap = [(Int, Text)] -> IntMap Text
forall a. [(Int, a)] -> IntMap a
IM.fromList [ (Id -> Int
idUniq Id
l, Id -> Text
blockGid Id
l) | (Id
l, Block
_) <- Proc -> [(Id, Block)]
procBlocks Proc
pr ]
                      call :: (Int, b, [Size]) -> Exp
call (Int
u, b
_, [Size]
szs) = Annote -> Size -> Text -> [Exp] -> Exp
A.Call Annote
an (Layout -> Size
loRecW Layout
lo) (Text -> Int -> IntMap Text -> Text
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault Text
"" Int
u IntMap Text
gidMap) ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ [Size] -> [Exp]
argSlices [Size]
szs [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> [Exp
i] [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> [Exp]
cellSlices
                  body <- case Layout -> [(Int, Integer, [Size])]
loTargets Layout
lo of
                        []  -> Annote -> Text -> TM m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failInternal Annote
an Text
"a process with no pause targets (rwc bug)."
                        [(Int, Integer, [Size])]
tgts -> Exp -> TM m Exp
forall a. a -> StateT S m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> TM m Exp) -> Exp -> TM m Exp
forall a b. (a -> b) -> a -> b
$ ((Int, Integer, [Size]) -> Exp -> Exp)
-> Exp -> [(Int, Integer, [Size])] -> Exp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ t :: (Int, Integer, [Size])
t@(Int
_, Integer
v, [Size]
_) Exp
acc ->
                                          Annote -> Size -> Exp -> Exp -> Exp -> Exp
A.If Annote
an (Layout -> Size
loRecW Layout
lo) (Annote -> Size -> Op -> [Exp] -> Exp
A.Prim Annote
an Size
1 Op
A.Eq [Exp
tag, Annote -> BV -> Exp
A.Lit Annote
an (BV -> Exp) -> BV -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec (Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Int) -> Size -> Int
forall a b. (a -> b) -> a -> b
$ Layout -> Size
loRTagW Layout
lo) Integer
v]) ((Int, Integer, [Size]) -> Exp
forall {b}. (Int, b, [Size]) -> Exp
call (Int, Integer, [Size])
t) Exp
acc)
                                    ((Int, Integer, [Size]) -> Exp
forall {b}. (Int, b, [Size]) -> Exp
call ((Int, Integer, [Size]) -> Exp) -> (Int, Integer, [Size]) -> Exp
forall a b. (a -> b) -> a -> b
$ [(Int, Integer, [Size])] -> (Int, Integer, [Size])
forall a. HasCallStack => [a] -> a
last [(Int, Integer, [Size])]
tgts) ([(Int, Integer, [Size])] -> [(Int, Integer, [Size])]
forall a. HasCallStack => [a] -> [a]
init [(Int, Integer, [Size])]
tgts)
                  let doc = Text
"state dispatch for process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Proc -> Text
procName Proc
pr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": "
                          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [ Integer -> Text
forall a. TextShow a => a -> Text
showt Integer
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"=" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x | (Text
x, Integer
v) <- [(Text, Integer)]
tagDisplay ]
                  pure $ A.Defn an gid (A.Sig an [stW, inW] (loRecW lo)) ["disc", "i"] body False (A.Blind [doc])

            -- | Assemble the device: registers (initials by evaluating the
            --   entry definition with zero-filled cells), the dispatch
            --   call, and the output/next-state slice equations.
            mkDeviceM :: Layout -> A.Size -> A.Defn -> A.Defn -> [A.Defn] -> [A.Extern] -> [(Text, Integer)] -> TM m A.Device
            mkDeviceM :: Layout
-> Size
-> Defn
-> Defn
-> [Defn]
-> [Extern]
-> [(Text, Integer)]
-> TM m Device
mkDeviceM Layout
lo Size
inW Defn
entryDefn Defn
dispatch [Defn]
defns [Extern]
exts [(Text, Integer)]
tagDisplay = do
                  let an :: Annote
an = Proc -> Annote
procAnnote Proc
pr
                  inSzs  <- Annote -> Ty -> StateT S m [Size]
detupleSizes Annote
an (Ty -> StateT S m [Size]) -> Ty -> StateT S m [Size]
forall a b. (a -> b) -> a -> b
$ Proc -> Ty
procInTy Proc
pr
                  outSzs <- detupleSizes an $ procOutTy pr
                  stSzs  <- concat <$> mapM (detupleSizes an . cellTy) (procCells pr)
                  let inWires  = [Text] -> [Size] -> [(Text, Size)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Config
confConfig -> Getting [Text] Config [Text] -> [Text]
forall s a. s -> Getting a s a -> a
^.Getting [Text] Config [Text]
Lens' Config [Text]
inputSigs)  [Size]
inSzs
                      outWires = [Text] -> [Size] -> [(Text, Size)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Config
confConfig -> Getting [Text] Config [Text] -> [Text]
forall s a. s -> Getting a s a -> a
^.Getting [Text] Config [Text]
Lens' Config [Text]
outputSigs) [Size]
outSzs
                      stWires  = [Text] -> [Size] -> [(Text, Size)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Config
confConfig -> Getting [Text] Config [Text] -> [Text]
forall s a. s -> Getting a s a -> a
^.Getting [Text] Config [Text]
Lens' Config [Text]
stateSigs)  [Size]
stSzs
                      rW       = Layout -> Size
loRW Layout
lo
                      regWires = [ (Text
"__resumption_tag", Size
rW) | Size
rW Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
> Size
0 ] [(Text, Size)] -> [(Text, Size)] -> [(Text, Size)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Size)]
stWires
                      padding  = Layout -> Size
loRecW Layout
lo Size -> Size -> Size
forall a. Num a => a -> a -> a
- Layout -> Size
loOutW Layout
lo Size -> Size -> Size
forall a. Num a => a -> a -> a
- [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((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)
                      layout   = [(Text, Size)] -> [(Text, Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets ([(Text, Size)] -> [(Text, Size, Size)])
-> [(Text, Size)] -> [(Text, Size, Size)]
forall a b. (a -> b) -> a -> b
$ (Text
"__padding", Size
padding) (Text, Size) -> [(Text, Size)] -> [(Text, Size)]
forall a. a -> [a] -> [a]
: [(Text, Size)]
outWires [(Text, Size)] -> [(Text, Size)] -> [(Text, Size)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Size)]
regWires

                  regs <- if null regWires then pure []
                        else do
                              let ienv  = 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
A.defnName Defn
d, Defn
d)) ([Defn] -> [(Text, Defn)]) -> [Defn] -> [(Text, Defn)]
forall a b. (a -> b) -> a -> b
$ Defn
dispatch Defn -> [Defn] -> [Defn]
forall a. a -> [a] -> [a]
: Defn
entryDefn Defn -> [Defn] -> [Defn]
forall a. a -> [a] -> [a]
: [Defn]
defns)
                                          ([(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
A.extName Extern
e, Extern
e)) [Extern]
exts)
                                  A.Sig _ argSzs _ = A.defnSig entryDefn
                                  args0 = [(Text, BV)] -> HashMap Text BV
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(Text, BV)] -> HashMap Text BV)
-> [(Text, BV)] -> HashMap Text BV
forall a b. (a -> b) -> a -> b
$ [Text] -> [BV] -> [(Text, BV)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Defn -> [Text]
A.defnParams Defn
entryDefn) ([BV] -> [(Text, BV)]) -> [BV] -> [(Text, BV)]
forall a b. (a -> b) -> a -> b
$ (Size -> BV) -> [Size] -> [BV]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> BV
zeros (Int -> BV) -> (Size -> Int) -> Size -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral) [Size]
argSzs
                              checkInitAcyclic (ann entryDefn) (envDefns ienv) $ A.defnBody entryDefn
                              init0 <- evalExp ienv args0 (A.defnBody entryDefn)
                                    `catchError` \ AstError
_ -> Annote -> Text -> StateT S m BV
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Defn -> Annote
forall a. Annotated a => a -> Annote
ann Defn
entryDefn)
                                          Text
"cannot evaluate the initial state (does it involve an extern?)"
                              pure [ A.Register an x sz $ sliceBV init0 off sz | (x, sz, off) <- wireOffsets regWires ]

                  let stInps   = [(Text, Size)]
regWires [(Text, Size)] -> [(Text, Size)] -> [(Text, Size)]
forall a. Semigroup a => a -> a -> a
<> [(Text, Size)]
inWires
                      inExp    = [Exp] -> Exp
A.cat [ Annote -> Size -> Text -> Exp
A.Var Annote
an Size
sz Text
x | (Text
x, Size
sz) <- [(Text, Size)]
stInps ]
                      loopArgs = [ Annote -> Size -> Size -> Exp -> Exp
slice0 Annote
an Size
off Size
sz (Annote -> Size -> Text -> Exp
A.Var Annote
an ([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)]
stInps) Text
"$in") | (()
_, Size
sz, Size
off) <- [((), Size)] -> [((), Size, Size)]
forall a. [(a, Size)] -> [(a, Size, Size)]
wireOffsets ((Size -> ((), Size)) -> [Size] -> [((), Size)]
forall a b. (a -> b) -> [a] -> [b]
map ((), ) [Size
rW Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Layout -> Size
loCellsW Layout
lo, Size
inW]) ]
                      resVar   = Annote -> Size -> Text -> Exp
A.Var Annote
an (Layout -> Size
loRecW Layout
lo) Text
"$res"
                      outNames = [Text] -> HashSet Text
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList ([Text] -> HashSet Text) -> [Text] -> HashSet Text
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Text) -> [(Text, Size)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Text
forall a b. (a, b) -> a
fst [(Text, Size)]
outWires
                      regNames = [Text] -> HashSet Text
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList ([Text] -> HashSet Text) -> [Text] -> HashSet Text
forall a b. (a -> b) -> a -> b
$ ((Text, Size) -> Text) -> [(Text, Size)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Size) -> Text
forall a b. (a, b) -> a
fst [(Text, Size)]
regWires

                  pure $ A.Device an (conf^.top) inWires outWires regs []
                       (  [ A.SLet an "$in" inExp
                          , A.SLet an "$res" $ A.Call an (loRecW lo) (A.defnName dispatch) loopArgs ]
                       <> [ A.SOutput an x $ slice0 an off sz resVar | (x, sz, off) <- layout, x `Set.member` outNames ]
                       <> [ A.SNext an x $ slice0 an off sz resVar   | (x, sz, off) <- layout, x `Set.member` regNames ] )
                       $ A.Blind tagDisplay
                  where sliceBV :: BV -> A.Index -> A.Size -> BV
                        sliceBV :: BV -> Size -> Size -> BV
sliceBV BV
bv Size
off Size
sz = 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
$ BV -> Integer
BV.nat BV
bv 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
^ Size -> Integer
forall a. Integral a => a -> Integer
toInteger Size
off)

                        -- The retired producer's port convention: one level
                        -- of type-application splitting (the bare head
                        -- sizes the constructor tag; Vec and Finite stay
                        -- whole), a leading residual component, zero
                        -- widths dropped.
                        detupleSizes :: Annote -> Ty -> TM m [A.Size]
                        detupleSizes :: Annote -> Ty -> StateT S m [Size]
detupleSizes Annote
an' Ty
t = do
                              whole <- Env -> Text -> Annote -> Ty -> TM m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Text -> Annote -> Ty -> TM m Size
sizeOf Env
env Text
"device port" Annote
an' Ty
t
                              parts <- mapM (sizeOf env "device port" an') $ detuple t
                              pure $ map fromIntegral $ filter (> 0)
                                   $ (toInteger whole - sum (map toInteger parts)) : map toInteger parts

                        detuple :: Ty -> [Ty]
                        detuple :: Ty -> [Ty]
detuple Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp Ty
t of
                              (TyCon Annote
_ Text
"Vec", [Ty]
_)    -> [Ty
t]
                              (TyCon Annote
_ Text
"Finite", [Ty]
_) -> [Ty
t]
                              (Ty
h, [Ty]
args)             -> Ty
h Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: [Ty]
args

-- | Rejects a cyclic call graph reachable from the initial-state
--   expression: the register-initial evaluation interprets it with no
--   step bound, so a reachable cycle means divergence without this check.
checkInitAcyclic :: MonadError AstError m => Annote -> HashMap A.GId A.Defn -> A.Exp -> m ()
checkInitAcyclic :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> HashMap Text Defn -> Exp -> m ()
checkInitAcyclic Annote
an HashMap Text Defn
defns Exp
e0 = () () -> m (HashSet Text) -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HashSet Text -> HashSet Text -> Exp -> m (HashSet Text)
forall (m :: * -> *).
MonadError AstError m =>
HashSet Text -> HashSet Text -> Exp -> m (HashSet Text)
go HashSet Text
forall a. Monoid a => a
mempty HashSet Text
forall a. Monoid a => a
mempty Exp
e0
      where go :: MonadError AstError m => HashSet A.GId -> HashSet A.GId -> A.Exp -> m (HashSet A.GId)
            go :: forall (m :: * -> *).
MonadError AstError m =>
HashSet Text -> HashSet Text -> Exp -> m (HashSet Text)
go HashSet Text
stack HashSet Text
done Exp
e = (HashSet Text -> Text -> m (HashSet Text))
-> HashSet Text -> [Text] -> m (HashSet Text)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM HashSet Text -> Text -> m (HashSet Text)
forall (m :: * -> *).
MonadError AstError m =>
HashSet Text -> Text -> m (HashSet Text)
goCall HashSet Text
done ([Text] -> m (HashSet Text)) -> [Text] -> m (HashSet Text)
forall a b. (a -> b) -> a -> b
$ Exp -> [Text]
expCalls Exp
e
                  where goCall :: MonadError AstError m => HashSet A.GId -> A.GId -> m (HashSet A.GId)
                        goCall :: forall (m :: * -> *).
MonadError AstError m =>
HashSet Text -> Text -> m (HashSet Text)
goCall HashSet Text
done' Text
g
                              | Text
g Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
stack = Annote -> Text -> m (HashSet Text)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an
                                    (Text -> m (HashSet Text)) -> Text -> m (HashSet Text)
forall a b. (a -> b) -> a -> b
$ Text
"cannot evaluate the initial state: definition is recursive (is recursion guarded by signal?): " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
g
                              | Text
g Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
done' = HashSet Text -> m (HashSet Text)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet Text
done'
                              | 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
defns = Text -> HashSet Text -> HashSet Text
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Text
g (HashSet Text -> HashSet Text)
-> m (HashSet Text) -> m (HashSet Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Text -> HashSet Text -> Exp -> m (HashSet Text)
forall (m :: * -> *).
MonadError AstError m =>
HashSet Text -> HashSet Text -> Exp -> m (HashSet Text)
go (Text -> HashSet Text -> HashSet Text
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Text
g HashSet Text
stack) HashSet Text
done' (Defn -> Exp
A.defnBody Defn
d)
                              | Bool
otherwise = HashSet Text -> m (HashSet Text)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet Text
done'

            expCalls :: A.Exp -> [A.GId]
            expCalls :: Exp -> [Text]
expCalls = \ case
                  A.Call Annote
_ Size
_ Text
g [Exp]
es    -> Text
g Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: (Exp -> [Text]) -> [Exp] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [Text]
expCalls [Exp]
es
                  A.Cat Annote
_ Exp
e1 Exp
e2      -> Exp -> [Text]
expCalls Exp
e1 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> Exp -> [Text]
expCalls Exp
e2
                  A.Slice Annote
_ Size
_ Size
_ Exp
e    -> Exp -> [Text]
expCalls Exp
e
                  A.Prim Annote
_ Size
_ Op
_ [Exp]
es    -> (Exp -> [Text]) -> [Exp] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [Text]
expCalls [Exp]
es
                  A.XCall Annote
_ Size
_ Text
_ [Natural]
_ [Exp]
es -> (Exp -> [Text]) -> [Exp] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [Text]
expCalls [Exp]
es
                  A.If Annote
_ Size
_ Exp
c Exp
t Exp
e     -> Exp -> [Text]
expCalls Exp
c [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> Exp -> [Text]
expCalls Exp
t [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> Exp -> [Text]
expCalls Exp
e
                  A.Let Annote
_ Size
_ Text
_ Exp
e1 Exp
e2  -> Exp -> [Text]
expCalls Exp
e1 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> Exp -> [Text]
expCalls Exp
e2
                  Exp
_                  -> []