{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- | purify (doc/synolon.md §8): convert the reactive fragment of a
--   monomorphic ANF program into one process. The traversal is
--   CPS-shaped — @compile e k@ compiles a reactive computation under a
--   continuation — which right-associates binds by construction:
--
--   * @rwPrimSignal o >>= k@ becomes @pause o -> L_k@ (the continuation
--     block's last parameter is the resumed input);
--   * @rwPrimReturn v@ becomes @goto L_k (v)@ (or @halt v@ at the root);
--   * lifted @rwPrimGet@/@rwPrimPut@ become cell commands, the cell
--     resolved from the operation's own residual state stack;
--   * @rwPrimExtrude m s@ is a cell write (@put@) followed by @m@ — cells
--     written in entry before the first pause become register initials
--     (doc/synolon.md §3.4), so no separate initials extraction exists;
--   * a reactive case becomes a terminator case (arms with commands get
--     their own blocks — continuations are shared blocks, so the retired
--     lift-once rule is the default by construction);
--   * join points become blocks; jumps become gotos;
--   * a reactive call is compiled once per continuation — block-graph
--     splicing memoized on @(definition, continuation)@, the retired
--     unfoldHead's successor; recursion closes through the memo table
--     (a tail self-call recurs under the same continuation, so it hits
--     the memo and becomes a goto). Two shapes are rejected with located
--     errors: a NOINLINE reactive callee on the left-hand side of a bind
--     (the user's opt-out from per-continuation splicing), and recursion
--     THROUGH a bind's left-hand side (re-entering a definition whose
--     splice is still open mints a fresh continuation per iteration —
--     each pending continuation is a resumption-stack frame, and the
--     machine has no stack).
--
--   Blocks are closure-converted afterward: a fixpoint over the block
--   graph computes each block's live-in locals, which become leading
--   parameters, with every pause/goto site supplying them (this is the
--   machine record's @args@ field).
--
--   This stage constructs the process — the Eidos-to-Synolon boundary; the
--   block graph is then cleaned by "ReWire.Synolon.Transform", checked by
--   the machine lint ("ReWire.Synolon.Lint"), and lowered by the
--   Synolon-to-Hyle fold ("ReWire.Synolon.ToHyle").
module ReWire.Eidos.ToSynolon (purify) where

import ReWire.Annotation (Annote, ann, noAnn)
import ReWire.Builtins (Builtin (..))
import ReWire.Error (AstError, MonadError, failAt)
import ReWire.Eidos.Naming (blockLabel)
import ReWire.Eidos.Pretty ()
import ReWire.Eidos.Subst (nextUniq, freeUniqs, occIds, substVars)
import ReWire.Eidos.Types (typeOf, flattenApp, flattenArrow, flattenTyApp, reacOrStateT, machineDefn)
import ReWire.Pretty (showt, prettyPrint)
import ReWire.SYB (query, queryWith)
import ReWire.Synolon.Syntax

import Control.Monad (when)
import Control.Monad.State.Strict (StateT, evalStateT, gets, modify)
import Data.Data (Data)
import Data.HashSet (HashSet)
import Data.Maybe (fromMaybe)
import Data.Text (Text)

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 ReWire.Eidos.Syntax as E (Program (..))

-- | The Synolon program of an Eidos program: the process compiled from
--   the reactive root, over the definitions the machine calls
--   ('machineDefn', in their order — Hyle names are assigned by position;
--   the consumed reactive definitions and the builtin signature carriers
--   do not ride along) and the datatypes those mention ('usedDatas'). The
--   root must be a nullary @ReacT@ computation (the mono lint's device
--   rule).
purify :: forall m. MonadError AstError m => E.Program -> m Program
purify :: forall (m :: * -> *). MonadError AstError m => Program -> m Program
purify p :: Program
p@(E.Program [DataDefn]
datas [Defn]
defns Id
top)
      | (TyCon Annote
_ Text
"ReacT", [Ty
ti, Ty
to, Ty
_, Ty
_]) <- Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
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
top
      , [] <- ([Ty], Ty) -> [Ty]
forall a b. (a, b) -> a
fst (Ty -> ([Ty], Ty)
flattenArrow (Ty -> ([Ty], Ty)) -> Ty -> ([Ty], Ty)
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
top) = do
            let cells :: [Cell]
cells = [Ty] -> [Cell]
stackCells ([Ty] -> [Cell]) -> [Ty] -> [Cell]
forall a b. (a -> b) -> a -> b
$ [[Ty]] -> [Ty]
maxStack
                      ([[Ty]] -> [Ty]) -> [[Ty]] -> [Ty]
forall a b. (a -> b) -> a -> b
$ (Defn -> [[Ty]]) -> [Defn] -> [[Ty]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Ty -> [[Ty]]
stackOfTy (Ty -> [[Ty]]) -> (Defn -> Ty) -> Defn -> [[Ty]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Ty
typeOf (Exp -> Ty) -> (Defn -> Exp) -> Defn -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Exp
defnBody) [Defn]
reactives
                     [[Ty]] -> [[Ty]] -> [[Ty]]
forall a. Semigroup a => a -> a -> a
<> (Defn -> [[Ty]]) -> [Defn] -> [[Ty]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Ty -> [[Ty]]) -> Exp -> [[Ty]]
forall a b r. (Data a, Typeable b) => (b -> [r]) -> a -> [r]
queryWith Ty -> [[Ty]]
stackOfTy (Exp -> [[Ty]]) -> (Defn -> Exp) -> Defn -> [[Ty]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Exp
defnBody) [Defn]
liveReactives
            pr <- StateT PSt m Proc -> PSt -> m Proc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Ty -> Ty -> [Cell] -> StateT PSt m Proc
compileRoot Ty
ti Ty
to [Cell]
cells) (PSt -> m Proc) -> PSt -> m Proc
forall a b. (a -> b) -> a -> b
$ Uniq
-> [(Id, Block)]
-> HashMap (Uniq, Uniq) Id
-> HashMap Text Uniq
-> IntSet
-> PSt
PSt (Program -> Uniq
forall a. Data a => a -> Uniq
nextUniq Program
p) [] HashMap (Uniq, Uniq) Id
forall a. Monoid a => a
mempty HashMap Text Uniq
forall a. Monoid a => a
mempty IntSet
forall a. Monoid a => a
mempty
            let defns' = (Defn -> Bool) -> [Defn] -> [Defn]
forall a. (a -> Bool) -> [a] -> [a]
filter Defn -> Bool
machineDefn [Defn]
defns
            pure $ Program (usedDatas datas defns' [pr]) defns' [pr]
      | Bool
otherwise = Annote -> Text -> m Program
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Ty -> Annote
forall a. Annotated a => a -> Annote
ann (Ty -> Annote) -> Ty -> Annote
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
top)
            (Text -> m Program) -> Text -> m Program
forall a b. (a -> b) -> a -> b
$ Text
"the device root " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
top Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" is not a reactive computation (its type is "
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
top) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"; a device root has type ReacT i o Identity a)."
      where dmap :: IM.IntMap Defn
            dmap :: IntMap Defn
dmap = [(Uniq, Defn)] -> IntMap Defn
forall a. [(Uniq, a)] -> IntMap a
IM.fromList [ (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d, Defn
d) | Defn
d <- [Defn]
defns ]

            -- The datatypes the machine mentions: those named by some
            -- type in the definitions or the process (a constructor
            -- occurrence carries its instantiated type; a case alternative
            -- names its constructor; a definition's provenance tag does
            -- not count), closed under the field types of their
            -- constructors. The rest is dropped — the reactive
            -- stack, retired with the reactive fragment, and the unused
            -- part of the primitive basis and the tuple family — so a
            -- Synolon program declares the type universe it lives in and
            -- nothing else. (The certify validator re-adds the absent
            -- basis declarations itself; its basis gate rejects only a
            -- declaration that is present and differs from the canonical
            -- one.)
            usedDatas :: [DataDefn] -> [Defn] -> [Proc] -> [DataDefn]
            usedDatas :: [DataDefn] -> [Defn] -> [Proc] -> [DataDefn]
usedDatas [DataDefn]
ds [Defn]
defns' [Proc]
procs = [ DataDefn
d | DataDefn
d <- [DataDefn]
ds, DataDefn -> Text
dataName DataDefn
d Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Text
keep ]
                  where keep :: HashSet TyConId
                        keep :: HashSet Text
keep = HashSet Text -> HashSet Text
close (HashSet Text -> HashSet Text) -> HashSet Text -> HashSet Text
forall a b. (a -> b) -> a -> b
$ [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
$ ([Defn], [Proc]) -> [Text]
forall a. Data a => a -> [Text]
tyCons ([Defn]
code, [Proc]
procs) [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ([Defn], [Proc]) -> [Text]
forall a. Data a => a -> [Text]
altDatas ([Defn]
code, [Proc]
procs)

                        code :: [Defn]
                        code :: [Defn]
code = [ Defn
d { defnOrigin = Nothing } | Defn
d <- [Defn]
defns' ]

                        dtab :: Map.HashMap TyConId DataDefn
                        dtab :: HashMap Text DataDefn
dtab = [(Text, DataDefn)] -> HashMap Text DataDefn
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (DataDefn -> Text
dataName DataDefn
d, DataDefn
d) | DataDefn
d <- [DataDefn]
ds ]

                        ctab :: Map.HashMap DataConId TyConId
                        ctab :: HashMap Text Text
ctab = [(Text, Text)] -> HashMap Text Text
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Text
c, DataDefn -> Text
dataName DataDefn
d) | DataDefn
d <- [DataDefn]
ds, DataCon Annote
_ Text
c Sig
_ <- DataDefn -> [DataCon]
dataCons DataDefn
d ]

                        tyCons :: Data a => a -> [TyConId]
                        tyCons :: forall a. Data a => a -> [Text]
tyCons a
x = [ Text
c | TyCon Annote
_ Text
c <- a -> [Ty]
forall a b. (Data a, Data b) => a -> [b]
query a
x ]

                        altDatas :: Data a => a -> [TyConId]
                        altDatas :: forall a. Data a => a -> [Text]
altDatas a
x = [ Text
t | DataAlt Text
c <- a -> [AltCon]
forall a b. (Data a, Data b) => a -> [b]
query a
x, Just Text
t <- [Text -> HashMap Text Text -> Maybe Text
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
c HashMap Text Text
ctab] ]

                        close :: HashSet TyConId -> HashSet TyConId
                        close :: HashSet Text -> HashSet Text
close HashSet Text
s | HashSet Text
s' HashSet Text -> HashSet Text -> Bool
forall a. Eq a => a -> a -> Bool
== HashSet Text
s   = HashSet Text
s
                                | Bool
otherwise = HashSet Text -> HashSet Text
close HashSet Text
s'
                              where s' :: HashSet Text
s' = HashSet Text -> HashSet Text -> HashSet Text
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
Set.union HashSet Text
s (HashSet Text -> HashSet Text) -> HashSet Text -> HashSet Text
forall a b. (a -> b) -> a -> b
$ [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]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ DataDefn -> [Text]
forall a. Data a => a -> [Text]
tyCons DataDefn
d | Text
n <- HashSet Text -> [Text]
forall a. HashSet a -> [a]
Set.toList HashSet Text
s, Just DataDefn
d <- [Text -> HashMap Text DataDefn -> Maybe DataDefn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
n HashMap Text DataDefn
dtab] ]

            -- The reactive code (monomorphic; the polymorphic rwPrim*
            -- signature carriers are type assumptions, not code).
            reactives :: [Defn]
            reactives :: [Defn]
reactives = [ Defn
d | Defn
d <- [Defn]
defns, 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
                            , [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyVar] -> Bool) -> [TyVar] -> Bool
forall a b. (a -> b) -> a -> b
$ 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 ]

            -- The state cells: one per layer of the deepest reactive
            -- stack — among the reactive definitions' own types (listed
            -- first, so that among stacks of equal depth the definition's
            -- spelling of the type wins) and every type the reachable
            -- reactive code carries: the partial evaluator inlines a
            -- single-use stateful computation into its extrude site, and
            -- then its state layer is visible in expression types only.
            -- Only reachable code counts there — a definition the last
            -- partial-evaluation round orphaned must not mint a cell.
            -- Outermost first, named s0, s1, ....
            maxStack :: [[Ty]] -> [Ty]
            maxStack :: [[Ty]] -> [Ty]
maxStack = \ case
                  [] -> []
                  [[Ty]]
ss -> ([Ty] -> [Ty] -> [Ty]) -> [[Ty]] -> [Ty]
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ [Ty]
a [Ty]
b -> if [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
a Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
>= [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
b then [Ty]
a else [Ty]
b) [[Ty]]
ss

            liveReactives :: [Defn]
            liveReactives :: [Defn]
liveReactives = [ Defn
d | Defn
d <- [Defn]
reactives, Uniq -> IntSet -> Bool
IS.member (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d) IntSet
reachable ]

            -- The definitions reachable from the device root.
            reachable :: IS.IntSet
            reachable :: IntSet
reachable = IntSet -> [Uniq] -> IntSet
go IntSet
IS.empty [Id -> Uniq
idUniq Id
top]
                  where go :: IS.IntSet -> [Uniq] -> IS.IntSet
                        go :: IntSet -> [Uniq] -> IntSet
go IntSet
seen = \ case
                              []                          -> IntSet
seen
                              Uniq
u : [Uniq]
us | Uniq -> IntSet -> Bool
IS.member Uniq
u IntSet
seen   -> IntSet -> [Uniq] -> IntSet
go IntSet
seen [Uniq]
us
                                     | Bool
otherwise          -> IntSet -> [Uniq] -> IntSet
go (Uniq -> IntSet -> IntSet
IS.insert Uniq
u IntSet
seen)
                                          ([Uniq] -> IntSet) -> [Uniq] -> IntSet
forall a b. (a -> b) -> a -> b
$ [Uniq] -> (Defn -> [Uniq]) -> Maybe Defn -> [Uniq]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Uniq]
us (([Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
<> [Uniq]
us) ([Uniq] -> [Uniq]) -> (Defn -> [Uniq]) -> Defn -> [Uniq]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Uniq]
IS.toList (IntSet -> [Uniq]) -> (Defn -> IntSet) -> Defn -> [Uniq]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntSet -> IntSet -> IntSet
`IS.intersection` IntMap Defn -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet IntMap Defn
dmap) (IntSet -> IntSet) -> (Defn -> IntSet) -> Defn -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> IntSet
freeUniqs (Exp -> IntSet) -> (Defn -> Exp) -> Defn -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Exp
defnBody)
                                                (Uniq -> IntMap Defn -> Maybe Defn
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup Uniq
u IntMap Defn
dmap) 

            stackOfTy :: Ty -> [[Ty]]
            stackOfTy :: Ty -> [[Ty]]
stackOfTy Ty
t = [ [Ty]
st | Just [Ty]
st <- [Ty -> Maybe [Ty]
stackOf Ty
t], Bool -> Bool
not ([Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
st) ]

            stackCells :: [Ty] -> [Cell]
            stackCells :: [Ty] -> [Cell]
stackCells [Ty]
ts = [ Annote -> Text -> Ty -> Maybe Exp -> Cell
Cell (Ty -> Annote
forall a. Annotated a => a -> Annote
ann Ty
t) (Text
"s" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Uniq -> Text
forall a. TextShow a => a -> Text
showt Uniq
i) Ty
t Maybe Exp
forall a. Maybe a
Nothing | (Uniq
i, Ty
t) <- [Uniq] -> [Ty] -> [(Uniq, Ty)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Uniq
0 :: Int ..] [Ty]
ts ]

            compileRoot :: Ty -> Ty -> [Cell] -> PM m Proc
            compileRoot :: Ty -> Ty -> [Cell] -> StateT PSt m Proc
compileRoot Ty
ti Ty
to [Cell]
cells = do
                  let cx :: Cx
cx = Cx { cxIn :: Ty
cxIn = Ty
ti, cxOut :: Ty
cxOut = Ty
to, cxCells :: [(Text, Ty)]
cxCells = (Cell -> (Text, Ty)) -> [Cell] -> [(Text, Ty)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Cell
c -> (Cell -> Text
cellName Cell
c, Cell -> Ty
cellTy Cell
c)) [Cell]
cells
                              , cxJoins :: IntMap Id
cxJoins = IntMap Id
forall a. Monoid a => a
mempty, cxRLets :: IntMap Exp
cxRLets = IntMap Exp
forall a. Monoid a => a
mempty }
                  body <- case Uniq -> IntMap Defn -> Maybe Defn
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup (Id -> Uniq
idUniq Id
top) IntMap Defn
dmap of
                        Just Defn
d  -> Exp -> StateT PSt m Exp
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> StateT PSt m Exp) -> Exp -> StateT PSt m Exp
forall a b. (a -> b) -> a -> b
$ Defn -> Exp
defnBody Defn
d
                        Maybe Defn
Nothing -> Annote -> Text -> StateT PSt m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Ty -> Annote
forall a. Annotated a => a -> Annote
ann (Ty -> Annote) -> Ty -> Annote
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
top) Text
"purify: device root has no definition (rwc bug)."
                  (cmds, term) <- compile cx body KHalt
                  blks <- gets stBlocks
                  pure $ closureConvert Proc
                        { procAnnote = ann body
                        , procName   = "main"
                        , procInTy   = ti
                        , procOutTy  = to
                        , procClock  = Nothing
                        , procCells  = cells
                        , procEntry  = Block (ann body) [] cmds term
                        , procBlocks = reverse blks
                        }

            -- The compile-time context: device i/o types, the cell table
            -- (name and type, outermost layer first), joins in scope
            -- (label and parameter count), and reactive let bindings
            -- (compiled at use).
            compile :: Cx -> Exp -> K -> PM m ([Cmd], Term)
            compile :: Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx Exp
e K
k = case Exp
e of
                  Let Annote
an (NonRec Id
x Exp
rhs) Exp
body
                        | 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
x ->
                              Cx -> Exp -> K -> PM m ([Cmd], Term)
compile (Cx
cx { cxRLets = IM.insert (idUniq x) rhs $ cxRLets cx }) Exp
body K
k
                        | Bool
otherwise -> do
                              (cmds, term) <- Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx Exp
body K
k
                              pure (CmdBind an x rhs : cmds, term)
                  Let Annote
_ (Join JoinId
j [Id]
ps Exp
b) Exp
body -> do
                        l <- Text -> [Ty] -> Ty -> PM m Id
forall (m :: * -> *). Monad m => Text -> [Ty] -> Ty -> PM m Id
freshLabel (Id -> Text
idOcc (Id -> Text) -> Id -> Text
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j) ((Id -> Ty) -> [Id] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map (Sig -> Ty
sigTy (Sig -> Ty) -> (Id -> Sig) -> Id -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Sig
idSig) [Id]
ps) (Ty -> PM m Id) -> Ty -> PM m Id
forall a b. (a -> b) -> a -> b
$ Cx -> Ty
cxOut Cx
cx
                        -- The join body compiles under the SAME continuation
                        -- (it is a tail of the definition); its block binds
                        -- the join parameters.
                        (jcmds, jterm) <- compile cx b k
                        emitBlock l $ Block (ann b) ps jcmds jterm
                        compile (cx { cxJoins = IM.insert (idUniq $ jpId j) l $ cxJoins cx }) body k
                  Let Annote
an (Rec [(Id, Exp)]
_) Exp
_ -> Annote -> Text -> PM m ([Cmd], Term)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"purify: unsupported local recursive binding."
                  Jump Annote
an JoinId
j [Exp]
args -> case Uniq -> IntMap Id -> Maybe Id
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j) (IntMap Id -> Maybe Id) -> IntMap Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Cx -> IntMap Id
cxJoins Cx
cx of
                        Just Id
l  -> ([Cmd], Term) -> PM m ([Cmd], Term)
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Annote -> Id -> [Exp] -> Term
Goto Annote
an Id
l [Exp]
args)
                        Maybe Id
Nothing -> Annote -> Text -> PM m ([Cmd], Term)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"purify: jump to an uncompiled join point (rwc bug)."
                  Case Annote
an Ty
t Exp
s Id
cb [Alt]
alts | Ty -> Bool
reacOrStateT Ty
t -> do
                        -- A terminator case has no binder: the case binder
                        -- aliases the scrutinee, an atom in ANF output, so
                        -- where it is live (GHC's case-binder swap leaves
                        -- it referenced in the alternatives) the scrutinee
                        -- takes its place.
                        let live :: Bool
live  = Uniq -> IntSet -> Bool
IS.member (Id -> Uniq
idUniq Id
cb) (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Alt -> IntSet) -> [Alt] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> IntSet
freeUniqs (Exp -> IntSet) -> (Alt -> Exp) -> Alt -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alt -> Exp
altBody) [Alt]
alts
                            alts0 :: [Alt]
alts0 | Bool
live      = [ Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
aan AltCon
c [Id]
xs (Exp -> Alt) -> Exp -> Alt
forall a b. (a -> b) -> a -> b
$ IntMap Exp -> Exp -> Exp
substVars (Uniq -> Exp -> IntMap Exp
forall a. Uniq -> a -> IntMap a
IM.singleton (Id -> Uniq
idUniq Id
cb) Exp
s) Exp
b | Alt Annote
aan AltCon
c [Id]
xs Exp
b <- [Alt]
alts ]
                                  | Bool
otherwise = [Alt]
alts
                        alts' <- (Alt -> StateT PSt m TAlt) -> [Alt] -> StateT PSt m [TAlt]
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 (Cx -> K -> Alt -> StateT PSt m TAlt
arm Cx
cx K
k) [Alt]
alts0
                        pure ([], TCase an s alts')
                  Var Annote
an Id
x
                        | Just Exp
rhs <- Uniq -> IntMap Exp -> Maybe Exp
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup (Id -> Uniq
idUniq Id
x) (IntMap Exp -> Maybe Exp) -> IntMap Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Cx -> IntMap Exp
cxRLets Cx
cx -> Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx Exp
rhs K
k
                        | Bool
otherwise -> Cx -> Annote -> Id -> [Exp] -> K -> PM m ([Cmd], Term)
call Cx
cx Annote
an Id
x [] K
k
                  App {}  -> Cx -> Exp -> K -> PM m ([Cmd], Term)
spine Cx
cx Exp
e K
k
                  Prim {} -> Cx -> Exp -> K -> PM m ([Cmd], Term)
spine Cx
cx Exp
e K
k -- bare nullary operation (get)
                  Exp
_ -> Annote -> Text -> PM m ([Cmd], Term)
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
"purify: unsupported reactive tail."

            altBody :: Alt -> Exp
            altBody :: Alt -> Exp
altBody (Alt Annote
_ AltCon
_ [Id]
_ Exp
b) = Exp
b

            arm :: Cx -> K -> Alt -> PM m TAlt
            arm :: Cx -> K -> Alt -> StateT PSt m TAlt
arm Cx
cx K
k (Alt Annote
an AltCon
c [Id]
xs Exp
b) = do
                  (cmds, term) <- Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx Exp
b K
k
                  if null cmds then pure $ TAlt an c xs term else do
                        l <- freshLabel "arm" (map (sigTy . idSig) xs) $ cxOut cx
                        emitBlock l $ Block an xs cmds term
                        pure $ TAlt an c xs $ Goto an l $ map (Var an) xs

            spine :: Cx -> Exp -> K -> PM m ([Cmd], Term)
            spine :: Cx -> Exp -> K -> PM m ([Cmd], Term)
spine Cx
cx Exp
e K
k = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
an Ty
_ Builtin
Bind, [EArg Exp
m, EArg Exp
kont]) -> do
                        k' <- Cx -> Annote -> Exp -> K -> PM m K
contOf Cx
cx Annote
an Exp
kont K
k
                        compile cx m k'
                  (Prim Annote
an Ty
_ Builtin
Signal, [EArg Exp
o]) -> do
                        l <- Cx -> Annote -> K -> PM m Id
resumeLabel Cx
cx Annote
an K
k
                        pure ([], Pause an o l [])
                  (Prim Annote
an Ty
_ Builtin
Return, [EArg Exp
v]) -> Annote -> Cx -> K -> Exp -> PM m ([Cmd], Term)
applyK Annote
an Cx
cx K
k Exp
v
                  (Prim Annote
an Ty
_ Builtin
Extrude, [EArg Exp
m, EArg Exp
s]) -> do
                        c <- Cx -> Annote -> Ty -> PM m Text
cellFor Cx
cx Annote
an (Ty -> PM m Text) -> Ty -> PM m Text
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
m
                        (cmds, term) <- compile cx m k
                        pure (CmdPut an c s : cmds, term)
                  -- Lift is a type-adjusting identity: cells resolve from
                  -- each operation's own residual state stack, so the
                  -- wrapper carries no information.
                  (Prim Annote
_ Ty
_ Builtin
Lift, [EArg Exp
inner]) -> Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx Exp
inner K
k
                  (Prim Annote
an Ty
t Builtin
Get, []) -> do
                        c <- Cx -> Annote -> Ty -> PM m Text
cellFor Cx
cx Annote
an Ty
t
                        x <- freshId (resultTy t) "$s"
                        (cmds, term) <- applyK an cx k $ Var an x
                        pure (CmdGet an x c : cmds, term)
                  (Prim Annote
an Ty
t Builtin
Put, [EArg Exp
v]) -> do
                        c <- Cx -> Annote -> Ty -> PM m Text
cellFor Cx
cx Annote
an Ty
t
                        (cmds, term) <- applyK an cx k unitE
                        pure (CmdPut an c v : cmds, term)
                  (Prim Annote
an Ty
t Builtin
Error, [EArg Exp
msg]) -> do
                        x <- Ty -> Text -> PM m Id
forall (m :: * -> *). Monad m => Ty -> Text -> PM m Id
freshId (Ty -> Ty
resultTy Ty
t) Text
"$err"
                        let t' = Annote -> Ty -> Ty -> Ty
Arrow Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"String") (Ty -> Ty) -> Ty -> Ty
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
                        pure ([CmdBind an x $ App an (Prim an t' Error) $ EArg msg], Halt an $ Var an x)
                  (Var Annote
an Id
f, [Arg]
args) -> Cx -> Annote -> Id -> [Exp] -> K -> PM m ([Cmd], Term)
call Cx
cx Annote
an Id
f [ Exp
a | EArg Exp
a <- [Arg]
args ] K
k
                  -- A residual reactive beta redex (the simplifier's single
                  -- round can leave one): lower to a let.
                  (Lam Annote
lan Id
x Exp
b, EArg Exp
a : [Arg]
rest) ->
                        Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx (Annote -> Bind -> Exp -> Exp
Let Annote
lan (Id -> Exp -> Bind
NonRec Id
x 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
lan) Exp
b [Arg]
rest) K
k
                  -- A let-headed application: hoist the application inside
                  -- (the arguments predate the binder, so this is scope-safe).
                  (Let Annote
lan Bind
bnd Exp
body, [Arg]
args) ->
                        Cx -> Exp -> K -> PM m ([Cmd], Term)
compile Cx
cx (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
body [Arg]
args) K
k
                  (Exp
h, [Arg]
_) -> Annote -> Text -> PM m ([Cmd], Term)
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 -> PM m ([Cmd], Term)) -> Text -> PM m ([Cmd], Term)
forall a b. (a -> b) -> a -> b
$ Text
"purify: unsupported reactive computation (head: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Exp -> Text
headKind Exp
h Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")."

            -- Apply the continuation to a value: goto (or halt at the root).
            applyK :: Annote -> Cx -> K -> Exp -> PM m ([Cmd], Term)
            applyK :: Annote -> Cx -> K -> Exp -> PM m ([Cmd], Term)
applyK Annote
an Cx
_ K
KHalt Exp
v        = ([Cmd], Term) -> PM m ([Cmd], Term)
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Annote -> Exp -> Term
Halt Annote
an Exp
v)
            applyK Annote
an Cx
_ (KLabel Id
l Uniq
_) Exp
v = ([Cmd], Term) -> PM m ([Cmd], Term)
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Annote -> Id -> [Exp] -> Term
Goto Annote
an Id
l [Exp
v])

            -- The label a pause resumes at: the continuation's own block
            -- (its last parameter is the resumed input), or a fresh
            -- halt-adapter block at the root.
            resumeLabel :: Cx -> Annote -> K -> PM m Id
            resumeLabel :: Cx -> Annote -> K -> PM m Id
resumeLabel Cx
_ Annote
_ (KLabel Id
l Uniq
_) = Id -> PM m Id
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
l
            resumeLabel Cx
cx Annote
an K
KHalt      = do
                  x <- Ty -> Text -> PM m Id
forall (m :: * -> *). Monad m => Ty -> Text -> PM m Id
freshId (Cx -> Ty
cxIn Cx
cx) Text
"$i"
                  l <- freshLabel "halt" [sigTy $ idSig x] $ cxOut cx
                  emitBlock l $ Block an [x] [] $ Halt an $ Var an x
                  pure l

            -- The continuation of a bind: a lambda becomes a block (bind
            -- its parameter, last); anything else eta-expands first.
            contOf :: Cx -> Annote -> Exp -> K -> PM m K
            contOf :: Cx -> Annote -> Exp -> K -> PM m K
contOf Cx
cx Annote
an Exp
kont K
k = case Exp
kont of
                  Lam Annote
_ Id
x Exp
b -> do
                        l <- Text -> [Ty] -> Ty -> PM m Id
forall (m :: * -> *). Monad m => Text -> [Ty] -> Ty -> PM m Id
freshLabel (Id -> Text
idOcc Id
x) [Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x] (Ty -> PM m Id) -> Ty -> PM m Id
forall a b. (a -> b) -> a -> b
$ Cx -> Ty
cxOut Cx
cx
                        (cmds, term) <- compile cx b k
                        emitBlock l $ Block (ann b) [x] cmds term
                        pure $ KLabel l 1
                  Exp
_ -> do
                        x <- Ty -> Text -> PM m Id
forall (m :: * -> *). Monad m => Ty -> Text -> PM m Id
freshId (Ty -> Ty
contDom (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
kont) Text
"$x"
                        contOf cx an (Lam an x $ App an kont $ EArg $ Var an x) k
                  where contDom :: Ty -> Ty
                        contDom :: Ty -> Ty
contDom Ty
t = case Ty -> ([Ty], Ty)
flattenArrow Ty
t of
                              (Ty
dom : [Ty]
_, Ty
_) -> Ty
dom
                              ([Ty], Ty)
_            -> Ty
t

            -- A reactive call: compiled once per continuation (memoized
            -- block-graph splicing).
            -- Rejected: NOINLINE at bind-LHS (the splicing opt-out), and
            -- re-entry into a definition whose splice is still open under
            -- a fresh continuation (recursion through a bind's LHS needs
            -- an unbounded resumption stack; only tail recursion — which
            -- re-enters under the SAME continuation and hits the memo —
            -- compiles to a finite machine).
            call :: Cx -> Annote -> Id -> [Exp] -> K -> PM m ([Cmd], Term)
            call :: Cx -> Annote -> Id -> [Exp] -> K -> PM m ([Cmd], Term)
call Cx
cx Annote
an Id
f [Exp]
args K
k = do
                  d <- StateT PSt m Defn
-> (Defn -> StateT PSt m Defn) -> Maybe Defn -> StateT PSt m Defn
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> StateT PSt m Defn
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> StateT PSt m Defn) -> Text -> StateT PSt m Defn
forall a b. (a -> b) -> a -> b
$ Text
"purify: call to an unknown reactive definition: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
f) Defn -> StateT PSt m Defn
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                        (Maybe Defn -> StateT PSt m Defn)
-> Maybe Defn -> StateT PSt m Defn
forall a b. (a -> b) -> a -> b
$ Uniq -> IntMap Defn -> Maybe Defn
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup (Id -> Uniq
idUniq Id
f) IntMap Defn
dmap
                  let noinline = Defn -> Maybe DefnAttr
defnAttr Defn
d Maybe DefnAttr -> Maybe DefnAttr -> Bool
forall a. Eq a => a -> a -> Bool
== DefnAttr -> Maybe DefnAttr
forall a. a -> Maybe a
Just DefnAttr
NoInline
                      bindLhs  = case K
k of { K
KHalt -> Bool
False; KLabel {} -> Bool
True }
                  when (bindLhs && noinline) $ failAt an
                        $ "the reactive computation " <> idOcc f <> " on the left-hand side of a bind might pause"
                        <> " (a NOINLINE reactive definition may only be called in tail position)"
                  mm <- gets $ Map.lookup (idUniq f, kKey k) . stMemo
                  l  <- case mm of
                        Just Id
l  -> Id -> PM m Id
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
l
                        Maybe Id
Nothing -> do
                              active <- (PSt -> IntSet) -> StateT PSt m IntSet
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PSt -> IntSet
stActive
                              when (IS.member (idUniq f) active) $ failAt an
                                    $ "the reactive computation " <> idOcc f <> " recurses on the left-hand side of a bind,"
                                    <> " which would need an unbounded resumption stack"
                                    <> " (recursion must reach itself in tail position to compile to a finite machine)"
                              l <- freshLabel (idOcc f) (map (sigTy . idSig) $ defnParams d) $ cxOut cx
                              modify $ \ PSt
st -> PSt
st { stMemo   = Map.insert (idUniq f, kKey k) l $ stMemo st
                                                  , stActive = IS.insert (idUniq f) $ stActive st }
                              (cmds, term) <- compile cx (defnBody d) k
                              modify $ \ PSt
st -> PSt
st { stActive = IS.delete (idUniq f) $ stActive st }
                              emitBlock l $ Block an (defnParams d) cmds term
                              pure l
                  pure ([], Goto an l args)

            cellFor :: Cx -> Annote -> Ty -> PM m Text
            cellFor :: Cx -> Annote -> Ty -> PM m Text
cellFor Cx
cx Annote
an Ty
t = case Ty -> Maybe [Ty]
stackOf Ty
t of
                  Just [Ty]
st | Bool -> Bool
not ([Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
st)
                          , Uniq
idx <- [(Text, Ty)] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length (Cx -> [(Text, Ty)]
cxCells Cx
cx) Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
- [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
st
                          , Uniq
idx Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
>= Uniq
0, Uniq
idx Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
< [(Text, Ty)] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length (Cx -> [(Text, Ty)]
cxCells Cx
cx) -> Text -> PM m Text
forall a. a -> StateT PSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> PM m Text) -> Text -> PM m Text
forall a b. (a -> b) -> a -> b
$ (Text, Ty) -> Text
forall a b. (a, b) -> a
fst ((Text, Ty) -> Text) -> (Text, Ty) -> Text
forall a b. (a -> b) -> a -> b
$ Cx -> [(Text, Ty)]
cxCells Cx
cx [(Text, Ty)] -> Uniq -> (Text, Ty)
forall a. HasCallStack => [a] -> Uniq -> a
!! Uniq
idx
                  Maybe [Ty]
_ -> Annote -> Text -> PM m Text
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"purify: cannot resolve the state cell for this operation (rwc bug)."

headKind :: Exp -> Text
headKind :: Exp -> Text
headKind = \ case
      Var {}     -> Text
"variable"
      Con {}     -> Text
"constructor"
      Prim Annote
_ Ty
_ Builtin
b -> Text
"primitive " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Builtin -> Text
forall a. TextShow a => a -> Text
showt Builtin
b
      Lam {}     -> Text
"lambda"
      Let {}     -> Text
"let"
      Case {}    -> Text
"case"
      Jump {}    -> Text
"jump"
      LitInt {}  -> Text
"integer literal"
      LitStr {}  -> Text
"string literal"
      LitList {} -> Text
"list literal"
      LitVec {}  -> Text
"vector literal"
      App {}     -> Text
"application"

data Cx = Cx
      { Cx -> Ty
cxIn    :: !Ty
      , Cx -> Ty
cxOut   :: !Ty
      , Cx -> [(Text, Ty)]
cxCells :: ![(Text, Ty)]
      , Cx -> IntMap Id
cxJoins :: !(IM.IntMap Id)
      , Cx -> IntMap Exp
cxRLets :: !(IM.IntMap Exp)
      }

data K = KHalt | KLabel !Id !Int

kKey :: K -> Uniq
kKey :: K -> Uniq
kKey = \ case
      K
KHalt      -> Uniq
forall a. Bounded a => a
minBound
      KLabel Id
l Uniq
_ -> Id -> Uniq
idUniq Id
l

data PSt = PSt
      { PSt -> Uniq
stSupply :: !Uniq
      , PSt -> [(Id, Block)]
stBlocks :: ![(Id, Block)]
      , PSt -> HashMap (Uniq, Uniq) Id
stMemo   :: !(Map.HashMap (Uniq, Uniq) Id)
      , PSt -> HashMap Text Uniq
stOrds   :: !(Map.HashMap Text Int) -- ^ Per-source-name label ordinals.
      , PSt -> IntSet
stActive :: !IS.IntSet -- ^ Definitions whose splice is in progress.
      }

type PM m = StateT PSt m

freshU :: Monad m => PM m Uniq
freshU :: forall (m :: * -> *). Monad m => PM m Uniq
freshU = do
      u <- (PSt -> Uniq) -> StateT PSt m Uniq
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PSt -> Uniq
stSupply
      modify $ \ PSt
st -> PSt
st { stSupply = u + 1 }
      pure u

freshId :: Monad m => Ty -> Text -> PM m Id
freshId :: forall (m :: * -> *). Monad m => Ty -> Text -> PM m Id
freshId Ty
t Text
occ = do
      u <- PM m Uniq
forall (m :: * -> *). Monad m => PM m Uniq
freshU
      pure $ Id occ u $ monoSig t

freshLabel :: Monad m => Text -> [Ty] -> Ty -> PM m Id
freshLabel :: forall (m :: * -> *). Monad m => Text -> [Ty] -> Ty -> PM m Id
freshLabel Text
src [Ty]
ptys Ty
ot = do
      i <- (PSt -> Uniq) -> StateT PSt m Uniq
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((PSt -> Uniq) -> StateT PSt m Uniq)
-> (PSt -> Uniq) -> StateT PSt m Uniq
forall a b. (a -> b) -> a -> b
$ Uniq -> Text -> HashMap Text Uniq -> Uniq
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.findWithDefault Uniq
1 Text
src (HashMap Text Uniq -> Uniq)
-> (PSt -> HashMap Text Uniq) -> PSt -> Uniq
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PSt -> HashMap Text Uniq
stOrds
      modify $ \ PSt
st -> PSt
st { stOrds = Map.insert src (i + 1) $ stOrds st }
      u <- freshU
      pure $ Id (blockLabel src i) u $ monoSig $ foldr (Arrow (ann ot)) ot ptys

emitBlock :: Monad m => Id -> Block -> PM m ()
emitBlock :: forall (m :: * -> *). Monad m => Id -> Block -> PM m ()
emitBlock Id
l Block
b = (PSt -> PSt) -> StateT PSt m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((PSt -> PSt) -> StateT PSt m ())
-> (PSt -> PSt) -> StateT PSt m ()
forall a b. (a -> b) -> a -> b
$ \ PSt
st -> PSt
st { stBlocks = (l, b) : stBlocks st }

unitE :: Exp
unitE :: Exp
unitE = Annote -> Ty -> Text -> Exp
Con Annote
noAnn (Annote -> Text -> Ty
TyCon Annote
noAnn Text
"()") Text
"()"

-- | The result type of a reactive/monadic type (last type application).
resultTy :: Ty -> Ty
resultTy :: Ty -> Ty
resultTy Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ ([Ty], Ty) -> Ty
forall a b. (a, b) -> b
snd (([Ty], Ty) -> Ty) -> ([Ty], Ty) -> Ty
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow Ty
t of
      (Ty
_, [Ty]
args) | Bool -> Bool
not ([Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
args) -> [Ty] -> Ty
forall a. HasCallStack => [a] -> a
last [Ty]
args
      (Ty, [Ty])
_                           -> Ty
t

-- | The state stack of a reactive or state-monadic type: the cell types,
--   outermost first.
stackOf :: Ty -> Maybe [Ty]
stackOf :: Ty -> Maybe [Ty]
stackOf Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ ([Ty], Ty) -> Ty
forall a b. (a, b) -> b
snd (([Ty], Ty) -> Ty) -> ([Ty], Ty) -> Ty
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow Ty
t of
      (TyCon Annote
_ Text
"ReacT", [Ty
_, Ty
_, Ty
m, Ty
_])  -> [Ty] -> Maybe [Ty]
forall a. a -> Maybe a
Just ([Ty] -> Maybe [Ty]) -> [Ty] -> Maybe [Ty]
forall a b. (a -> b) -> a -> b
$ Ty -> [Ty]
layers Ty
m
      (TyCon Annote
_ Text
"StateT", [Ty
s, Ty
m, Ty
_])    -> [Ty] -> Maybe [Ty]
forall a. a -> Maybe a
Just ([Ty] -> Maybe [Ty]) -> [Ty] -> Maybe [Ty]
forall a b. (a -> b) -> a -> b
$ Ty
s Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: Ty -> [Ty]
layers Ty
m
      (Ty, [Ty])
_                                -> Maybe [Ty]
forall a. Maybe a
Nothing
      where layers :: Ty -> [Ty]
            layers :: Ty -> [Ty]
layers Ty
ty = case Ty -> (Ty, [Ty])
flattenTyApp Ty
ty of
                  (TyCon Annote
_ Text
"StateT", [Ty
s, Ty
m']) -> Ty
s Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: Ty -> [Ty]
layers Ty
m'
                  (TyCon Annote
_ Text
"StateT", [Ty
s, Ty
m', Ty
_]) -> Ty
s Ty -> [Ty] -> [Ty]
forall a. a -> [a] -> [a]
: Ty -> [Ty]
layers Ty
m'
                  (Ty, [Ty])
_                           -> []

-- | Closure conversion: a fixpoint over the block graph computes each
--   block's live-in locals; they become leading parameters, and every
--   transfer site supplies them.
closureConvert :: Proc -> Proc
closureConvert :: Proc -> Proc
closureConvert Proc
pr = Proc
pr { procEntry  = patchBlock $ procEntry pr
                       , procBlocks = [ (l, (patchBlock b) { blkParams = capIds l <> blkParams b }) | (l, b) <- procBlocks pr ]
                       }
      where blocks :: [(Id, Block)]
            blocks :: [(Id, Block)]
blocks = Proc -> [(Id, Block)]
procBlocks Proc
pr

            binfo :: IM.IntMap Block
            binfo :: IntMap Block
binfo = [(Uniq, Block)] -> IntMap Block
forall a. [(Uniq, a)] -> IntMap a
IM.fromList [ (Id -> Uniq
idUniq Id
l, Block
b) | (Id
l, Block
b) <- [(Id, Block)]
blocks ]

            -- Locals bound within a block.
            bound :: Block -> IS.IntSet
            bound :: Block -> IntSet
bound Block
b = [Uniq] -> IntSet
IS.fromList ([Uniq] -> IntSet) -> [Uniq] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Id -> Uniq) -> [Id] -> [Uniq]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Uniq
idUniq (Block -> [Id]
blkParams Block
b) [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
<> (Cmd -> [Uniq]) -> [Cmd] -> [Uniq]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Cmd -> [Uniq]
cmdB (Block -> [Cmd]
blkCmds Block
b) [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
<> Term -> [Uniq]
termB (Block -> Term
blkTerm Block
b)
                  where cmdB :: Cmd -> [Uniq]
                        cmdB :: Cmd -> [Uniq]
cmdB = \ case
                              CmdBind Annote
_ Id
x Exp
_ -> [Id -> Uniq
idUniq Id
x]
                              CmdGet Annote
_ Id
x Text
_  -> [Id -> Uniq
idUniq Id
x]
                              CmdPut {}     -> []

                        termB :: Term -> [Uniq]
                        termB :: Term -> [Uniq]
termB = \ case
                              TCase Annote
_ Exp
_ [TAlt]
alts -> [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Id -> Uniq) -> [Id] -> [Uniq]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Uniq
idUniq [Id]
xs [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
<> Term -> [Uniq]
termB Term
t | TAlt Annote
_ AltCon
_ [Id]
xs Term
t <- [TAlt]
alts ]
                              Term
_              -> []

            -- Direct free locals of a block's expressions (excluding
            -- top-level definitions, which occIds distinguishes by never
            -- being block-bound; anything not bound in the process is a
            -- top-level reference and is dropped by intersecting with
            -- process-bound uniques).
            procBound :: IS.IntSet
            procBound :: IntSet
procBound = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Block -> IntSet) -> [Block] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map Block -> IntSet
bound ([Block] -> [IntSet]) -> [Block] -> [IntSet]
forall a b. (a -> b) -> a -> b
$ 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 [(Id, Block)]
blocks

            ownFree :: Block -> IS.IntSet
            ownFree :: Block -> IntSet
ownFree Block
b = ([IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions ((Exp -> IntSet) -> [Exp] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> IntSet
freeUniqs ([Exp] -> [IntSet]) -> [Exp] -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Block -> [Exp]
blockExps Block
b) IntSet -> IntSet -> IntSet
`IS.intersection` IntSet
procBound) IntSet -> IntSet -> IntSet
IS.\\ Block -> IntSet
bound Block
b

            blockExps :: Block -> [Exp]
            blockExps :: Block -> [Exp]
blockExps Block
b = (Cmd -> [Exp]) -> [Cmd] -> [Exp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Cmd -> [Exp]
ce (Block -> [Cmd]
blkCmds Block
b) [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> Term -> [Exp]
te (Block -> Term
blkTerm Block
b)
                  where ce :: Cmd -> [Exp]
                        ce :: Cmd -> [Exp]
ce = \ case
                              CmdBind Annote
_ Id
_ Exp
e -> [Exp
e]
                              CmdGet {}     -> []
                              CmdPut Annote
_ Text
_ Exp
e  -> [Exp
e]

                        te :: Term -> [Exp]
                        te :: Term -> [Exp]
te = \ case
                              Pause Annote
_ Exp
a Id
_ [Exp]
as -> Exp
a Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
as
                              Goto Annote
_ Id
_ [Exp]
as    -> [Exp]
as
                              Halt Annote
_ Exp
a       -> [Exp
a]
                              TCase Annote
_ Exp
a [TAlt]
alts -> Exp
a Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Term -> [Exp]
te Term
t | TAlt Annote
_ AltCon
_ [Id]
_ Term
t <- [TAlt]
alts ]

            targets :: Block -> [Uniq]
            targets :: Block -> [Uniq]
targets Block
b = Term -> [Uniq]
go (Term -> [Uniq]) -> Term -> [Uniq]
forall a b. (a -> b) -> a -> b
$ Block -> Term
blkTerm Block
b
                  where go :: Term -> [Uniq]
                        go :: Term -> [Uniq]
go = \ case
                              Pause Annote
_ Exp
_ Id
l [Exp]
_  -> [Id -> Uniq
idUniq Id
l]
                              Goto Annote
_ Id
l [Exp]
_     -> [Id -> Uniq
idUniq Id
l]
                              TCase Annote
_ Exp
_ [TAlt]
alts -> [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Term -> [Uniq]
go Term
t | TAlt Annote
_ AltCon
_ [Id]
_ Term
t <- [TAlt]
alts ]
                              Halt {}        -> []

            -- live(L) = ownFree(L) ∪ ⋃_{L'∈targets} live(L') , minus bound(L).
            live :: IM.IntMap IS.IntSet
            live :: IntMap IntSet
live = IntMap IntSet -> IntMap IntSet
go (IntMap IntSet -> IntMap IntSet) -> IntMap IntSet -> IntMap IntSet
forall a b. (a -> b) -> a -> b
$ (Block -> IntSet) -> IntMap Block -> IntMap IntSet
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map Block -> IntSet
ownFree IntMap Block
binfo
                  where go :: IM.IntMap IS.IntSet -> IM.IntMap IS.IntSet
                        go :: IntMap IntSet -> IntMap IntSet
go IntMap IntSet
cur =
                              let nxt :: IntMap IntSet
nxt = (Uniq -> IntSet -> IntSet) -> IntMap IntSet -> IntMap IntSet
forall a b. (Uniq -> a -> b) -> IntMap a -> IntMap b
IM.mapWithKey (\ Uniq
u IntSet
s ->
                                          let b :: Block
b = IntMap Block
binfo IntMap Block -> Uniq -> Block
forall a. IntMap a -> Uniq -> a
IM.! Uniq
u
                                          in (IntSet
s IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IS.unions [ IntSet -> Uniq -> IntMap IntSet -> IntSet
forall a. a -> Uniq -> IntMap a -> a
IM.findWithDefault IntSet
forall a. Monoid a => a
mempty Uniq
t IntMap IntSet
cur | Uniq
t <- Block -> [Uniq]
targets Block
b ]) IntSet -> IntSet -> IntSet
IS.\\ Block -> IntSet
bound Block
b) IntMap IntSet
cur
                              in if IntMap IntSet
nxt IntMap IntSet -> IntMap IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntMap IntSet
cur then IntMap IntSet
cur else IntMap IntSet -> IntMap IntSet
go IntMap IntSet
nxt

            ids :: IM.IntMap Id
            ids :: IntMap Id
ids = [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ (Block -> IntMap Id) -> [Block] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map (\ Block
b -> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ (Exp -> IntMap Id) -> [Exp] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> IntMap Id
occIds ([Exp] -> [IntMap Id]) -> [Exp] -> [IntMap Id]
forall a b. (a -> b) -> a -> b
$ Block -> [Exp]
blockExps Block
b) (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 [(Id, Block)]
blocks)
                  [IntMap Id] -> [IntMap Id] -> [IntMap Id]
forall a. Semigroup a => a -> a -> a
<> [ [(Uniq, Id)] -> IntMap Id
forall a. [(Uniq, a)] -> IntMap a
IM.fromList [ (Id -> Uniq
idUniq Id
x, Id
x) | Id
x <- Block -> [Id]
blkParams Block
b [Id] -> [Id] -> [Id]
forall a. Semigroup a => a -> a -> a
<> Block -> [Id]
cmdIds Block
b ] | Block
b <- 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 [(Id, Block)]
blocks ]
                  where cmdIds :: Block -> [Id]
                        cmdIds :: Block -> [Id]
cmdIds Block
b = [ Id
x | CmdBind Annote
_ Id
x Exp
_ <- Block -> [Cmd]
blkCmds Block
b ] [Id] -> [Id] -> [Id]
forall a. Semigroup a => a -> a -> a
<> [ Id
x | CmdGet Annote
_ Id
x Text
_ <- Block -> [Cmd]
blkCmds Block
b ]

            capIds :: Id -> [Id]
            capIds :: Id -> [Id]
capIds Id
l = [ Id -> Maybe Id -> Id
forall a. a -> Maybe a -> a
fromMaybe (Uniq -> Id
idPanic Uniq
u) (Maybe Id -> Id) -> Maybe Id -> Id
forall a b. (a -> b) -> a -> b
$ Uniq -> IntMap Id -> Maybe Id
forall a. Uniq -> IntMap a -> Maybe a
IM.lookup Uniq
u IntMap Id
ids | Uniq
u <- IntSet -> [Uniq]
IS.toList (IntSet -> [Uniq]) -> IntSet -> [Uniq]
forall a b. (a -> b) -> a -> b
$ IntSet -> Uniq -> IntMap IntSet -> IntSet
forall a. a -> Uniq -> IntMap a -> a
IM.findWithDefault IntSet
forall a. Monoid a => a
mempty (Id -> Uniq
idUniq Id
l) IntMap IntSet
live ]
                  where idPanic :: Uniq -> Id
                        idPanic :: Uniq -> Id
idPanic Uniq
u = Text -> Uniq -> Sig -> Id
Id Text
"$cap" Uniq
u (Sig -> Id) -> Sig -> Id
forall a b. (a -> b) -> a -> b
$ Ty -> Sig
monoSig (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon (Proc -> Annote
procAnnote Proc
pr) Text
"()"

            patchBlock :: Block -> Block
            patchBlock :: Block -> Block
patchBlock Block
b = Block
b { blkTerm = patchTerm $ blkTerm b }

            patchTerm :: Term -> Term
            patchTerm :: Term -> Term
patchTerm = \ case
                  Pause Annote
an Exp
a Id
l [Exp]
as -> Annote -> Exp -> Id -> [Exp] -> Term
Pause Annote
an Exp
a Id
l ([Exp] -> Term) -> [Exp] -> Term
forall a b. (a -> b) -> a -> b
$ Annote -> Id -> [Exp]
caps Annote
an Id
l [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> [Exp]
as
                  Goto Annote
an Id
l [Exp]
as    -> Annote -> Id -> [Exp] -> Term
Goto Annote
an Id
l ([Exp] -> Term) -> [Exp] -> Term
forall a b. (a -> b) -> a -> b
$ Annote -> Id -> [Exp]
caps Annote
an Id
l [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> [Exp]
as
                  TCase Annote
an Exp
a [TAlt]
alts -> Annote -> Exp -> [TAlt] -> Term
TCase Annote
an Exp
a [ Annote -> AltCon -> [Id] -> Term -> TAlt
TAlt Annote
aan AltCon
c [Id]
xs (Term -> Term
patchTerm Term
t) | TAlt Annote
aan AltCon
c [Id]
xs Term
t <- [TAlt]
alts ]
                  Term
t               -> Term
t
                  where caps :: Annote -> Id -> [Exp]
                        caps :: Annote -> Id -> [Exp]
caps Annote
an Id
l = (Id -> Exp) -> [Id] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> Id -> Exp
Var Annote
an) ([Id] -> [Exp]) -> [Id] -> [Exp]
forall a b. (a -> b) -> a -> b
$ Id -> [Id]
capIds Id
l