{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | Well-formedness checking for Synolon programs: the per-process machine
--   rules of doc/synolon.md §4 — signal-guardedness (the goto-only
--   subgraph of the block graph is acyclic), representability (every
--   binder, block parameter, cell, port, and halt answer has a fixed bit
--   width, by "ReWire.Synolon.Repr"), block normal form (command
--   right-hand sides are simple computations; terminator operands and put
--   payloads are atoms or primitive expressions), cell-initial constness
--   and typing, full-arity pauses and gotos, the resumed-input parameter
--   rule, and "the process pauses" — over the expression-level checker
--   of "ReWire.Eidos.Lint" at mono+ANF strength with the reactive types
--   out of the type grammar,
--   plus the program rules: name distinctness, global uniqueness over the
--   datatype-and-definition fragment, the definition rules on the
--   definitions the machine calls, and pure-acyclicity (the call graph of
--   the definitions reachable from a process is acyclic, and no recursive
--   let is reachable).
--
--   Process binding sites are scoped, not globally unique: purify splices
--   one definition per continuation and passes one binder along goto
--   chains, so a unique is legitimately bound by several blocks. Labels
--   and cells are distinct per process; within a block every binding site
--   is distinct and disjoint from the definition-level sites; and in-block
--   binding is validated by scoping and occurrence-signature agreement.
module ReWire.Synolon.Lint (lint, lintPre, lintProc, isOperand) where

import ReWire.Annotation (Annote, Annotated (ann))
import ReWire.Eidos.ANF (isAtom, isPrimExp)
import ReWire.Eidos.Lint (Env (..), LintMode (..), envFromDecls, bindVar, nonTail, checkExp, checkAgainst, checkTy, checkRepr, checkValueBinder, checkOccSig, checkDistinct, checkDataDefn, checkDefn, lookupCon, dconFieldTys, LitRep (..), litRep, fitsRep, declSites, expSites, idSite)
import ReWire.Eidos.Types (tyEq, typeOf, flattenApp, hasArrow)
import ReWire.Error (AstError, MonadError, failAt)
import ReWire.Eidos.Pretty ()
import ReWire.Pretty (prettyPrint, showt)
import ReWire.Synolon.Repr (dataEnv, sizeOf)
import ReWire.Synolon.Syntax

import Control.Monad (foldM, foldM_, unless, when, zipWithM_)
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.Maybe (mapMaybe)
import Data.Text (Text)

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

-- | The environment of the machine rules: the datatypes and every
--   definition in scope, at mono+ANF strength, with the reactive types
--   banned from the type grammar and every binder required to have a
--   fixed bit width.
machineEnv :: Program -> Env
machineEnv :: Program -> Env
machineEnv (Program [DataDefn]
datas [Defn]
defns [Proc]
_) = (LintMode -> [DataDefn] -> [Defn] -> Env
envFromDecls LintMode
LintMonoANF [DataDefn]
datas [Defn]
defns)
      { envBanReactive = True
      , envRepr        = Just $ sizeOf $ dataEnv datas
      }

-- | Check a whole program: name distinctness, global uniqueness over the
--   datatype-and-definition fragment, the datatypes, every definition
--   (all of them are the machine's: pure, monomorphic, first-order),
--   every process, and pure-acyclicity.
lint :: MonadError AstError m => Program -> m ()
lint :: forall (m :: * -> *). MonadError AstError m => Program -> m ()
lint = Bool -> Program -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Bool -> Program -> m ()
lintWith Bool
True

-- | 'lint' for the program before the block-graph cleanup: the same rules
--   except signal-guardedness, the one rule the cleanup may establish
--   (purify can leave an orphaned, unguarded block — the continuation of
--   a computation that never returns — which the cleanup removes).
lintPre :: MonadError AstError m => Program -> m ()
lintPre :: forall (m :: * -> *). MonadError AstError m => Program -> m ()
lintPre = Bool -> Program -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Bool -> Program -> m ()
lintWith Bool
False

lintWith :: forall m. MonadError AstError m => Bool -> Program -> m ()
lintWith :: forall (m :: * -> *).
MonadError AstError m =>
Bool -> Program -> m ()
lintWith Bool
guarded p :: Program
p@(Program [DataDefn]
datas [Defn]
defns [Proc]
procs) = do
      [(Uniq, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [(Uniq, Annote, Text)]
decls
      [(Text, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [ (DataDefn -> Text
dataName DataDefn
d, DataDefn -> Annote
dataAnnote DataDefn
d, Text
"datatype name " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> DataDefn -> Text
dataName DataDefn
d) | DataDefn
d <- [DataDefn]
datas ]
      [(Text, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [ (Text
c, Annote
an, Text
"data constructor name " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c) | DataDefn
d <- [DataDefn]
datas, DataCon Annote
an Text
c Sig
_ <- DataDefn -> [DataCon]
dataCons DataDefn
d ]
      [(Text, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [ (Proc -> Text
procName Proc
pr, Proc -> Annote
procAnnote Proc
pr, Text
"process name " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Proc -> Text
procName Proc
pr) | Proc
pr <- [Proc]
procs ]
      (DataDefn -> m ()) -> [DataDefn] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> DataDefn -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> DataDefn -> m ()
checkDataDefn Env
env) [DataDefn]
datas
      (Defn -> m ()) -> [Defn] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn Env
env) [Defn]
defns
      (Proc -> m ()) -> [Proc] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
forall (m :: * -> *).
MonadError AstError m =>
[(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
checkProcWith [(Uniq, Annote, Text)]
decls Bool
guarded Env
env) [Proc]
procs
      [Defn] -> [Proc] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
[Defn] -> [Proc] -> m ()
checkPureAcyclic [Defn]
defns [Proc]
procs
      where env :: Env
            env :: Env
env = Program -> Env
machineEnv Program
p

            decls :: [(Uniq, Annote, Text)]
            decls :: [(Uniq, Annote, Text)]
decls = [DataDefn] -> [Defn] -> [(Uniq, Annote, Text)]
declSites [DataDefn]
datas [Defn]
defns

-- | Check a single process (the machine rules, and pure-acyclicity from
--   it) against a program's global context.
lintProc :: MonadError AstError m => Program -> Proc -> m ()
lintProc :: forall (m :: * -> *).
MonadError AstError m =>
Program -> Proc -> m ()
lintProc p :: Program
p@(Program [DataDefn]
datas [Defn]
defns [Proc]
_) Proc
pr = do
      [(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
forall (m :: * -> *).
MonadError AstError m =>
[(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
checkProcWith ([DataDefn] -> [Defn] -> [(Uniq, Annote, Text)]
declSites [DataDefn]
datas [Defn]
defns) Bool
True (Program -> Env
machineEnv Program
p) Proc
pr
      [Defn] -> [Proc] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
[Defn] -> [Proc] -> m ()
checkPureAcyclic [Defn]
defns [Proc
pr]

---
--- Processes (doc/synolon.md §4): the machine rules, per-proc.
---


-- | The machine rules of one process, given the program's definition-level
--   binding sites (every block's own sites must be disjoint from them) and
--   whether to check signal-guardedness.
checkProcWith :: forall m. MonadError AstError m => [(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
checkProcWith :: forall (m :: * -> *).
MonadError AstError m =>
[(Uniq, Annote, Text)] -> Bool -> Env -> Proc -> m ()
checkProcWith [(Uniq, Annote, Text)]
decls Bool
guarded Env
env pr :: Proc
pr@(Proc Annote
an Text
n Ty
it Ty
ot Maybe Text
_clk [Cell]
cells Block
entry [(Id, Block)]
blocks) = do
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
it
      Env -> Annote -> Text -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Ty -> m ()
checkRepr Env
env Annote
an (Text
"the input type of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n) Ty
it
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
ot
      Env -> Annote -> Text -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Ty -> m ()
checkRepr Env
env Annote
an (Text
"the output type of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n) Ty
ot
      [(Text, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [ (Cell -> Text
cellName Cell
c, Cell -> Annote
cellAnnote Cell
c, Text
"state cell " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Cell -> Text
cellName Cell
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n) | Cell
c <- [Cell]
cells ]
      [(Uniq, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct [ (Id -> Uniq
idUniq Id
l, Block -> Annote
blkAnnote Block
b, Text
"block label " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
forall a. Pretty a => a -> Text
prettyPrint 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
<> Text
n) | (Id
l, Block
b) <- [(Id, Block)]
blocks ]
      (Cell -> m ()) -> [Cell] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Cell -> m ()
checkCell [Cell]
cells
      Block -> m ()
checkBlock Block
entry
      ((Id, Block) -> m ()) -> [(Id, Block)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Block -> m ()
checkBlock (Block -> m ()) -> ((Id, Block) -> Block) -> (Id, Block) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Block) -> Block
forall a b. (a, b) -> b
snd) [(Id, Block)]
blocks
      ((Id, Block) -> m ()) -> [(Id, Block)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Id, Block) -> m ()
checkInput [(Id, Block)]
blocks
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Term] -> Bool
anyPause ([Term] -> Bool) -> [Term] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Id, Block) -> Term) -> [(Id, Block)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Block -> Term
blkTerm (Block -> Term) -> ((Id, Block) -> Block) -> (Id, Block) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Block) -> Block
forall a b. (a, b) -> b
snd) [(Id, Block)]
blocks [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [Block -> Term
blkTerm Block
entry]) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an
            (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" never pauses (no machine to generate)"
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
guarded m ()
checkGuarded
      where ltab :: HashMap Uniq (Id, Block)
            ltab :: HashMap Uniq (Id, Block)
ltab = [(Uniq, (Id, Block))] -> HashMap Uniq (Id, Block)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Id -> Uniq
idUniq Id
l, (Id
l, Block
b)) | (Id
l, Block
b) <- [(Id, Block)]
blocks ]

            ctab :: HashMap Text Ty
            ctab :: HashMap Text Ty
ctab = [(Text, Ty)] -> HashMap Text Ty
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Cell -> Text
cellName Cell
c, Cell -> Ty
cellTy Cell
c) | Cell
c <- [Cell]
cells ]

            -- Cells are representable; their initials are closed (checked
            -- in the top-level-only environment: no locals are in scope),
            -- cell-typed, and simple computations.
            checkCell :: Cell -> m ()
            checkCell :: Cell -> m ()
checkCell (Cell Annote
can Text
s Ty
t Maybe Exp
e0) = do
                  Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
can Ty
t
                  Env -> Annote -> Text -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Ty -> m ()
checkRepr Env
env Annote
can (Text
"state cell " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" of process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n) Ty
t
                  case Maybe Exp
e0 of
                        Maybe Exp
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Just Exp
e  -> do
                              t' <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env) Exp
e
                              unless (tyEq t t') $ failAt can
                                    $ "the initial value of state cell " <> s <> " has type "
                                    <> prettyPrint t' <> ", not the cell's type " <> prettyPrint t
                              rhsOk e

            checkBlock :: Block -> m ()
            checkBlock :: Block -> m ()
checkBlock b :: Block
b@(Block Annote
ban [Id]
ps [Cmd]
cmds Term
term) = do
                  [(Uniq, Annote, Text)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, Text)] -> m ()
checkDistinct ([(Uniq, Annote, Text)] -> m ()) -> [(Uniq, Annote, Text)] -> m ()
forall a b. (a -> b) -> a -> b
$ [(Uniq, Annote, Text)]
decls [(Uniq, Annote, Text)]
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. Semigroup a => a -> a -> a
<> Block -> [(Uniq, Annote, Text)]
blockSites Block
b
                  (Id -> m ()) -> [Id] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Annote -> Text -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Id -> m ()
checkValueBinder Env
env Annote
ban Text
"block parameter") [Id]
ps
                  env' <- (Env -> Cmd -> m Env) -> Env -> [Cmd] -> m Env
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Env -> Cmd -> m Env
checkCmd ((Id -> Env -> Env) -> Env -> [Id] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Env -> Env
bindVar Env
env [Id]
ps) [Cmd]
cmds
                  checkTerm env' term

            checkCmd :: Env -> Cmd -> m Env
            checkCmd :: Env -> Cmd -> m Env
checkCmd Env
env' = \ case
                  CmdBind Annote
can Id
x Exp
rhs -> do
                        Env -> Annote -> Text -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Id -> m ()
checkValueBinder Env
env' Annote
can Text
"command binder" Id
x
                        Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env') Exp
rhs (Ty -> m ()) -> Ty -> m ()
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
                        Exp -> m ()
forall (m :: * -> *). MonadError AstError m => Exp -> m ()
rhsOk Exp
rhs
                        Env -> m Env
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env -> m Env) -> Env -> m Env
forall a b. (a -> b) -> a -> b
$ Id -> Env -> Env
bindVar Id
x Env
env'
                  CmdGet Annote
can Id
x Text
s    -> do
                        Env -> Annote -> Text -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> Id -> m ()
checkValueBinder Env
env' Annote
can Text
"command binder" Id
x
                        t <- Annote -> Text -> m Ty
cell Annote
can Text
s
                        unless (tyEq (sigTy $ idSig x) t) $ failAt can
                              $ "get: binder " <> prettyPrint x <> " has type " <> prettyPrint (sigTy $ idSig x)
                              <> ", not the type of state cell " <> s <> " (" <> prettyPrint t <> ")"
                        pure $ bindVar x env'
                  CmdPut Annote
can Text
s Exp
a    -> do
                        t <- Annote -> Text -> m Ty
cell Annote
can Text
s
                        checkAgainst (nonTail env') a t
                        operand can "put payload" a
                        pure env'

            -- Every binding site of a block: its parameters, its command
            -- binders, the binders inside its expressions, and its
            -- terminator alternatives' pattern binders.
            blockSites :: Block -> [(Uniq, Annote, Text)]
            blockSites :: Block -> [(Uniq, Annote, Text)]
blockSites (Block Annote
ban [Id]
ps [Cmd]
cmds Term
term) =
                  (Id -> (Uniq, Annote, Text)) -> [Id] -> [(Uniq, Annote, Text)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> Text -> Id -> (Uniq, Annote, Text)
idSite Annote
ban Text
"block parameter") [Id]
ps
                        [(Uniq, Annote, Text)]
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. Semigroup a => a -> a -> a
<> (Cmd -> [(Uniq, Annote, Text)]) -> [Cmd] -> [(Uniq, Annote, Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Cmd -> [(Uniq, Annote, Text)]
cmdSites [Cmd]
cmds
                        [(Uniq, Annote, Text)]
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. Semigroup a => a -> a -> a
<> Term -> [(Uniq, Annote, Text)]
termSites Term
term
                  where cmdSites :: Cmd -> [(Uniq, Annote, Text)]
                        cmdSites :: Cmd -> [(Uniq, Annote, Text)]
cmdSites = \ case
                              CmdBind Annote
can Id
x Exp
e -> Annote -> Text -> Id -> (Uniq, Annote, Text)
idSite Annote
can Text
"command binder" Id
x (Uniq, Annote, Text)
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. a -> [a] -> [a]
: Exp -> [(Uniq, Annote, Text)]
expSites Exp
e
                              CmdGet Annote
can Id
x Text
_  -> [Annote -> Text -> Id -> (Uniq, Annote, Text)
idSite Annote
can Text
"command binder" Id
x]
                              CmdPut Annote
_ Text
_ Exp
e    -> Exp -> [(Uniq, Annote, Text)]
expSites Exp
e

                        termSites :: Term -> [(Uniq, Annote, Text)]
                        termSites :: Term -> [(Uniq, Annote, Text)]
termSites = \ case
                              TCase Annote
_ Exp
a [TAlt]
alts -> Exp -> [(Uniq, Annote, Text)]
expSites Exp
a [(Uniq, Annote, Text)]
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. Semigroup a => a -> a -> a
<> [[(Uniq, Annote, Text)]] -> [(Uniq, Annote, Text)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Id -> (Uniq, Annote, Text)) -> [Id] -> [(Uniq, Annote, Text)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> Text -> Id -> (Uniq, Annote, Text)
idSite Annote
tan Text
"pattern binder") [Id]
xs [(Uniq, Annote, Text)]
-> [(Uniq, Annote, Text)] -> [(Uniq, Annote, Text)]
forall a. Semigroup a => a -> a -> a
<> Term -> [(Uniq, Annote, Text)]
termSites Term
t | TAlt Annote
tan AltCon
_ [Id]
xs Term
t <- [TAlt]
alts ]
                              Term
t              -> (Exp -> [(Uniq, Annote, Text)]) -> [Exp] -> [(Uniq, Annote, Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Uniq, Annote, Text)]
expSites ([Exp] -> [(Uniq, Annote, Text)])
-> [Exp] -> [(Uniq, Annote, Text)]
forall a b. (a -> b) -> a -> b
$ Term -> [Exp]
termExps Term
t

            cell :: Annote -> Text -> m Ty
            cell :: Annote -> Text -> m Ty
cell Annote
can Text
s = m Ty -> (Ty -> m Ty) -> Maybe Ty -> m Ty
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> Text -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
can (Text -> m Ty) -> Text -> m Ty
forall a b. (a -> b) -> a -> b
$ Text
"unknown state cell: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  (Maybe Ty -> m Ty) -> Maybe Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Text -> HashMap Text Ty -> Maybe Ty
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Text
s HashMap Text Ty
ctab

            checkTerm :: Env -> Term -> m ()
            checkTerm :: Env -> Term -> m ()
checkTerm Env
env' = \ case
                  Pause Annote
tan Exp
a Id
l [Exp]
args -> do
                        Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env') Exp
a Ty
ot
                        Annote -> Text -> Exp -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Text -> Exp -> m ()
operand Annote
tan Text
"pause output" Exp
a
                        (lB, b) <- Annote -> Id -> m (Id, Block)
target Annote
tan Id
l
                        when (null $ blkParams b) $ failAt tan
                              $ "pause target " <> prettyPrint lB <> " has no parameters (the last is the resumed input)"
                        unless (length args == length (blkParams b) - 1) $ failAt tan
                              $ "pause to " <> prettyPrint lB <> " supplies " <> showt (length args)
                              <> " arguments (its target takes " <> showt (length (blkParams b) - 1)
                              <> " plus the resumed input)"
                        zipWithM_ (\ Exp
a' Id
p -> Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env') Exp
a' (Ty -> m ()) -> Ty -> m ()
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
p) args $ blkParams b
                        mapM_ (operand tan "pause argument") args
                  Goto Annote
tan Id
l [Exp]
args    -> do
                        (lB, b) <- Annote -> Id -> m (Id, Block)
target Annote
tan Id
l
                        unless (length args == length (blkParams b)) $ failAt tan
                              $ "goto " <> prettyPrint lB <> " supplies " <> showt (length args)
                              <> " arguments (its target takes " <> showt (length $ blkParams b) <> ")"
                        zipWithM_ (\ Exp
a' Id
p -> Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env') Exp
a' (Ty -> m ()) -> Ty -> m ()
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
p) args $ blkParams b
                        mapM_ (operand tan "goto argument") args
                  Halt Annote
tan Exp
a         -> do
                        t <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env') Exp
a
                        checkRepr env tan ("a halt answer of process " <> n) t
                        operand tan "halt answer" a
                  TCase Annote
tan Exp
a [TAlt]
alts   -> do
                        ts <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env') Exp
a
                        operand tan "terminator case scrutinee" a
                        case [ tan' | TAlt tan' DefaultAlt _ _ <- drop 1 alts ] of
                              Annote
tan' : [Annote]
_ -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan' Text
"the default terminator alternative must come first"
                              []       -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        checkDistinct [ (c, tan', "terminator alternative for constructor " <> c) | TAlt tan' (DataAlt c) _ _ <- alts ]
                        when (null alts) $ failAt tan "terminator case with no alternatives"
                        mapM_ (checkTAlt env' ts) alts

            checkTAlt :: Env -> Ty -> TAlt -> m ()
            checkTAlt :: Env -> Ty -> TAlt -> m ()
checkTAlt Env
env' Ty
ts (TAlt Annote
tan AltCon
c [Id]
xs Term
t) = case AltCon
c of
                  AltCon
DefaultAlt -> do
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
xs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan Text
"default terminator alternative binds fields"
                        Env -> Term -> m ()
checkTerm Env
env' Term
t
                  LitAlt Integer
ln  -> do
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
xs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan Text
"literal terminator alternative binds fields"
                        case Ty -> LitRep
litRep Ty
ts of
                              LitRep
RepBad -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"literal terminator alternative on a scrutinee of type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint Ty
ts
                              LitRep
rep    -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LitRep -> Integer -> Bool
fitsRep LitRep
rep Integer
ln) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan
                                    (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"literal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
forall a. TextShow a => a -> Text
showt Integer
ln Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" is not representable at the scrutinee type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint Ty
ts
                        Env -> Term -> m ()
checkTerm Env
env' Term
t
                  DataAlt Text
c' -> do
                        (tcon, sig) <- Env -> Annote -> Text -> m (Text, Sig)
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Text -> m (Text, Sig)
lookupCon Env
env Annote
tan Text
c'
                        fields      <- dconFieldTys tan c' tcon sig ts
                        unless (length xs == length fields) $ failAt tan
                              $ "terminator alternative for " <> c' <> " binds " <> showt (length xs)
                              <> " fields (the constructor has " <> showt (length fields) <> ")"
                        mapM_ (checkValueBinder env' tan "pattern binder") xs
                        checkTerm (foldr bindVar env' xs) t

            target :: Annote -> Id -> m (Id, Block)
            target :: Annote -> Id -> m (Id, Block)
target Annote
tan Id
l = case Uniq -> HashMap Uniq (Id, Block) -> Maybe (Id, Block)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Id -> Uniq
idUniq Id
l) HashMap Uniq (Id, Block)
ltab of
                  Just (Id, Block)
lb -> Annote -> Id -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Id -> Id -> m ()
checkOccSig Annote
tan Id
l ((Id, Block) -> Id
forall a b. (a, b) -> a
fst (Id, Block)
lb) m () -> m (Id, Block) -> m (Id, Block)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Id, Block) -> m (Id, Block)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id, Block)
lb
                  Maybe (Id, Block)
Nothing -> Annote -> Text -> m (Id, Block)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
tan (Text -> m (Id, Block)) -> Text -> m (Id, Block)
forall a b. (a -> b) -> a -> b
$ Text
"terminator targets an undeclared block label: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
forall a. Pretty a => a -> Text
prettyPrint Id
l

            anyPause :: [Term] -> Bool
            anyPause :: [Term] -> Bool
anyPause = (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Term -> Bool
go
                  where go :: Term -> Bool
                        go :: Term -> Bool
go = \ case
                              Pause {}       -> Bool
True
                              TCase Annote
_ Exp
_ [TAlt]
alts -> (TAlt -> Bool) -> [TAlt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (TAlt Annote
_ AltCon
_ [Id]
_ Term
t) -> Term -> Bool
go Term
t) [TAlt]
alts
                              Term
_              -> Bool
False

            -- Pause targets: their last parameter is the resumed input.
            checkInput :: (Id, Block) -> m ()
            checkInput :: (Id, Block) -> m ()
checkInput (Id
l, Block
b)
                  | Id -> Uniq
idUniq Id
l Uniq -> HashSet Uniq -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet Uniq
pauseTargets
                  , Id
p : [Id]
_ <- [Id] -> [Id]
forall a. [a] -> [a]
reverse ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ Block -> [Id]
blkParams Block
b
                  , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Bool
tyEq (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
p) Ty
it = Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Block -> Annote
blkAnnote Block
b)
                        (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"the last parameter of pause target " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
forall a. Pretty a => a -> Text
prettyPrint Id
l
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (the resumed input) has type " 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
p)
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", not the process input type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Ty -> Text
forall a. Pretty a => a -> Text
prettyPrint Ty
it
                  | Bool
otherwise = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

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

            -- Signal-guardedness (doc/synolon.md §4): the goto-only subgraph of the
            -- block graph is acyclic — every cycle crosses a pause.
            checkGuarded :: m ()
            checkGuarded :: m ()
checkGuarded = (Uniq -> m ()) -> [Uniq] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HashSet Uniq -> Uniq -> m ()
visit HashSet Uniq
forall a. Monoid a => a
mempty) ([Uniq] -> m ()) -> [Uniq] -> m ()
forall a b. (a -> b) -> a -> b
$ HashMap Uniq [Id] -> [Uniq]
forall k v. HashMap k v -> [k]
Map.keys HashMap Uniq [Id]
gotoEdges
                  where gotoEdges :: HashMap Uniq [Id]
                        gotoEdges :: HashMap Uniq [Id]
gotoEdges = [(Uniq, [Id])] -> HashMap Uniq [Id]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(Uniq, [Id])] -> HashMap Uniq [Id])
-> [(Uniq, [Id])] -> HashMap Uniq [Id]
forall a b. (a -> b) -> a -> b
$ (Uniq
entryKey, Term -> [Id]
gotos (Term -> [Id]) -> Term -> [Id]
forall a b. (a -> b) -> a -> b
$ Block -> Term
blkTerm Block
entry)
                              (Uniq, [Id]) -> [(Uniq, [Id])] -> [(Uniq, [Id])]
forall a. a -> [a] -> [a]
: [ (Id -> Uniq
idUniq Id
l, Term -> [Id]
gotos (Term -> [Id]) -> Term -> [Id]
forall a b. (a -> b) -> a -> b
$ Block -> Term
blkTerm Block
b) | (Id
l, Block
b) <- [(Id, Block)]
blocks ]

                        entryKey :: Uniq
                        entryKey :: Uniq
entryKey = Uniq
forall a. Bounded a => a
minBound

                        gotos :: Term -> [Id]
                        gotos :: Term -> [Id]
gotos = \ case
                              Goto Annote
_ Id
l [Exp]
_     -> [Id
l]
                              TCase Annote
_ Exp
_ [TAlt]
alts -> (TAlt -> [Id]) -> [TAlt] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (TAlt Annote
_ AltCon
_ [Id]
_ Term
t) -> Term -> [Id]
gotos Term
t) [TAlt]
alts
                              Term
_              -> []

                        visit :: HashSet Uniq -> Uniq -> m ()
                        visit :: HashSet Uniq -> Uniq -> m ()
visit HashSet Uniq
stack Uniq
u
                              | Uniq -> HashSet Uniq -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member Uniq
u HashSet Uniq
stack = Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Proc -> Annote
procAnnote Proc
pr)
                                    (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": a cycle of gotos crosses no pause (is recursion guarded by signal?)"
                              | Bool
otherwise = (Id -> m ()) -> [Id] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HashSet Uniq -> Uniq -> m ()
visit (Uniq -> HashSet Uniq -> HashSet Uniq
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Uniq
u HashSet Uniq
stack) (Uniq -> m ()) -> (Id -> Uniq) -> Id -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Uniq
idUniq)
                                    ([Id] -> m ()) -> [Id] -> m ()
forall a b. (a -> b) -> a -> b
$ [Id] -> Uniq -> HashMap Uniq [Id] -> [Id]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.lookupDefault [] Uniq
u HashMap Uniq [Id]
gotoEdges

---
--- Block normal form (doc/synolon.md §3.2).
---

-- | A right-hand side is a simple computation: an atom, a saturated call
--   of a definition or constructor, a primitive expression, or a case
--   over an atom whose alternatives are let chains of such right-hand
--   sides ending in an atom. A call's arguments are atoms or primitive
--   expressions (which nest freely: the pure data path is a tree of
--   primitives over atoms), or the naming-exempt lambda and
--   function-typed forms — the higher-order builtins' function
--   arguments, kept in place with A-normalized bodies, and partial
--   applications. A-normalization establishes this shape for the
--   reactive fragment (doc/eidos.md §6), purification carries it into
--   blocks, and the cleanup transforms preserve it (epsilon inlining
--   substitutes operands for block parameters only where the result is
--   still in the form, 'isOperand').
rhsOk :: forall m. MonadError AstError m => Exp -> m ()
rhsOk :: forall (m :: * -> *). MonadError AstError m => Exp -> m ()
rhsOk Exp
r = case Exp
r of
      Exp
_ | Exp -> Bool
isAtom Exp
r         -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Case Annote
an Ty
_ Exp
s Id
_ [Alt]
alts -> do
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Exp -> Bool
isAtom Exp
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"block normal form: a case scrutinee is not an atom (it must be let-bound)"
            (Alt -> m ()) -> [Alt] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Alt Annote
_ AltCon
_ [Id]
_ Exp
b) -> Text -> Exp -> m ()
tailOk Text
"an alternative" Exp
b) [Alt]
alts
      App {}             -> Exp -> m ()
spineOk Exp
r
      Exp
_                  -> Annote -> Text -> 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
r)
            Text
"block normal form: a right-hand side must be an atom, a saturated call, or a case over an atom"
      where spineOk :: Exp -> m ()
            spineOk :: Exp -> m ()
spineOk Exp
e = do
                  let (Exp
h, [Arg]
args) = Exp -> (Exp, [Arg])
flattenApp Exp
e
                  case Exp
h of
                        Var {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Con {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Prim {} -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Lam {}  -> Annote -> Text -> 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
e) Text
"block normal form: a residual beta-redex (the application's lambda head must be let-bound)"
                        Exp
_       -> Annote -> Text -> 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
e) Text
"block normal form: the application's head is not a definition, constructor, or primitive"
                  (Exp -> m ()) -> [Exp] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Exp -> m ()
argOk [ Exp
a | EArg Exp
a <- [Arg]
args ]

            argOk :: Exp -> m ()
            argOk :: Exp -> m ()
argOk Exp
a
                  | Exp -> Bool
isAtom Exp
a           = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  | Lam Annote
_ Id
_ Exp
b <- Exp
a     = Text -> Exp -> m ()
tailOk Text
"a lambda body" Exp
b
                  | Exp -> Bool
isPrimExp Exp
a        = Exp -> m ()
spineOk Exp
a
                  | Ty -> Bool
hasArrow (Ty -> Bool) -> Ty -> Bool
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a = case Exp
a of
                        App {}  -> Exp -> m ()
spineOk Exp
a
                        Con {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- a bare constructor reference
                        Prim {} -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- a bare operator primitive
                        Exp
_       -> Annote -> Text -> 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
a) Text
"block normal form: a function-typed argument must be a lambda, a partial application, or a definition, constructor, or primitive reference"
                  | Bool
otherwise          = Annote -> Text -> 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
a) Text
"block normal form: a computed argument (must be let-bound)"

            tailOk :: Text -> Exp -> m ()
            tailOk :: Text -> Exp -> m ()
tailOk Text
what Exp
e = case Exp
e of
                  Exp
_ | Exp -> Bool
isAtom Exp
e               -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  Let Annote
_ (NonRec Id
_ Exp
r') Exp
body -> Exp -> m ()
forall (m :: * -> *). MonadError AstError m => Exp -> m ()
rhsOk Exp
r' m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Text -> Exp -> m ()
tailOk Text
what Exp
body
                  Let Annote
an (Join {}) Exp
_       -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"block normal form: a join point in a block (join points and jumps occur only in definition bodies)"
                  Jump Annote
an JoinId
_ [Exp]
_              -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"block normal form: a jump in a block (join points and jumps occur only in definition bodies)"
                  Exp
_                        -> Annote -> Text -> 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
e)
                        (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"block normal form: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
what Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" must be a let chain of simple computations ending in an atom"

-- | Is the expression an operand (an atom, or a primitive expression over
--   such)? The pure form of 'operand', for the cleanup's epsilon inliner.
isOperand :: Exp -> Bool
isOperand :: Exp -> Bool
isOperand Exp
e = case Annote -> Text -> Exp -> Either AstError ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Text -> Exp -> m ()
operand (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) Text
"" Exp
e :: Either AstError () of
      Left AstError
_  -> Bool
False
      Right ()
_ -> Bool
True

-- | A terminator operand or put payload is an atom or a primitive
--   expression (over such operands).
operand :: MonadError AstError m => Annote -> Text -> Exp -> m ()
operand :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> Text -> Exp -> m ()
operand Annote
an Text
what Exp
e
      | Exp -> Bool
isAtom Exp
e    = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      | Exp -> Bool
isPrimExp Exp
e = Exp -> m ()
forall (m :: * -> *). MonadError AstError m => Exp -> m ()
rhsOk Exp
e
      | Bool
otherwise   = Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an
            (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"block normal form: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
what Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" is neither an atom nor a primitive expression (it must be let-bound)"

---
--- Pure-acyclicity (doc/synolon.md §4).
---

-- | The call graph of the definitions reachable from a process — through
--   its cell initials, command right-hand sides, put payloads, and
--   terminator operands, transitively — is acyclic, and no recursive let
--   is reachable. Recursion in a device compiles only when it is guarded
--   by signal, and that recursion is reactive: it became the block graph,
--   which signal-guardedness checks.
checkPureAcyclic :: forall m. MonadError AstError m => [Defn] -> [Proc] -> m ()
checkPureAcyclic :: forall (m :: * -> *).
MonadError AstError m =>
[Defn] -> [Proc] -> m ()
checkPureAcyclic [Defn]
defns [Proc]
procs = (HashSet Uniq -> Proc -> m (HashSet Uniq))
-> HashSet Uniq -> [Proc] -> m ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (\ HashSet Uniq
done Proc
pr -> Proc -> m [Uniq]
procRefs Proc
pr m [Uniq] -> ([Uniq] -> m (HashSet Uniq)) -> m (HashSet Uniq)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (HashSet Uniq -> Uniq -> m (HashSet Uniq))
-> HashSet Uniq -> [Uniq] -> m (HashSet Uniq)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashSet Uniq -> HashSet Uniq -> Uniq -> m (HashSet Uniq)
visit HashSet Uniq
forall a. Monoid a => a
mempty) HashSet Uniq
done) HashSet Uniq
forall a. Monoid a => a
mempty [Proc]
procs
      where dtab :: HashMap Uniq Defn
            dtab :: HashMap Uniq Defn
dtab = [(Uniq, Defn)] -> HashMap Uniq Defn
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.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 ]

            procRefs :: Proc -> m [Uniq]
            procRefs :: Proc -> m [Uniq]
procRefs Proc
pr = [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Uniq]] -> [Uniq]) -> m [[Uniq]] -> m [Uniq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m [Uniq]) -> [Exp] -> m [[Uniq]]
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 -> m [Uniq]
refs ((Cell -> Maybe Exp) -> [Cell] -> [Exp]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Cell -> Maybe Exp
cellInit (Proc -> [Cell]
procCells Proc
pr) [Exp] -> [Exp] -> [Exp]
forall a. Semigroup a => a -> a -> a
<> (Block -> [Exp]) -> [Block] -> [Exp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Block -> [Exp]
blockExps (Proc -> [Block]
allBlocks Proc
pr))

            -- Depth-first over the definitions, with the current path as
            -- the stack and the fully explored definitions as done.
            visit :: HashSet Uniq -> HashSet Uniq -> Uniq -> m (HashSet Uniq)
            visit :: HashSet Uniq -> HashSet Uniq -> Uniq -> m (HashSet Uniq)
visit HashSet Uniq
stack HashSet Uniq
done Uniq
u = case Uniq -> HashMap Uniq Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Uniq
u HashMap Uniq Defn
dtab of
                  Maybe Defn
Nothing -> HashSet Uniq -> m (HashSet Uniq)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet Uniq
done
                  Just Defn
d
                        | Uniq -> HashSet Uniq -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member Uniq
u HashSet Uniq
stack -> Annote -> Text -> m (HashSet Uniq)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt (Defn -> Annote
defnAnnote Defn
d)
                              (Text -> m (HashSet Uniq)) -> Text -> m (HashSet Uniq)
forall a b. (a -> b) -> a -> b
$ Text
"unsupported use of recursion: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
forall a. Pretty a => a -> Text
prettyPrint (Defn -> Id
defnId Defn
d)
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" is recursive and reachable from a process (the pure call graph of a machine must be acyclic; only recursion guarded by signal compiles)"
                        | Uniq -> HashSet Uniq -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member Uniq
u HashSet Uniq
done  -> HashSet Uniq -> m (HashSet Uniq)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet Uniq
done
                        | Bool
otherwise          -> do
                              rs    <- Exp -> m [Uniq]
refs (Exp -> m [Uniq]) -> Exp -> m [Uniq]
forall a b. (a -> b) -> a -> b
$ Defn -> Exp
defnBody Defn
d
                              done' <- foldM (visit $ Set.insert u stack) done rs
                              pure $ Set.insert u done'

            -- The variable occurrences of an expression (locals are
            -- filtered by the table lookup); a recursive let is rejected
            -- on sight.
            refs :: Exp -> m [Uniq]
            refs :: Exp -> m [Uniq]
refs = \ case
                  Var Annote
_ Id
x                   -> [Uniq] -> m [Uniq]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Id -> Uniq
idUniq Id
x]
                  App Annote
_ Exp
f Arg
a                 -> [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
(<>) ([Uniq] -> [Uniq] -> [Uniq]) -> m [Uniq] -> m ([Uniq] -> [Uniq])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m [Uniq]
refs Exp
f m ([Uniq] -> [Uniq]) -> m [Uniq] -> m [Uniq]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg -> m [Uniq]
argRefs Arg
a
                  Lam Annote
_ Id
_ Exp
b                 -> Exp -> m [Uniq]
refs Exp
b
                  Let Annote
an (Rec [(Id, Exp)]
_) Exp
_          -> Annote -> Text -> m [Uniq]
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an
                        Text
"unsupported use of recursion: a recursive let binding is reachable from a process (the pure call graph of a machine must be acyclic)"
                  Let Annote
_ (NonRec Id
_ Exp
rhs) Exp
body -> [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
(<>) ([Uniq] -> [Uniq] -> [Uniq]) -> m [Uniq] -> m ([Uniq] -> [Uniq])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m [Uniq]
refs Exp
rhs m ([Uniq] -> [Uniq]) -> m [Uniq] -> m [Uniq]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> m [Uniq]
refs Exp
body
                  Let Annote
_ (Join JoinId
_ [Id]
_ Exp
b) Exp
body   -> [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
(<>) ([Uniq] -> [Uniq] -> [Uniq]) -> m [Uniq] -> m ([Uniq] -> [Uniq])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m [Uniq]
refs Exp
b m ([Uniq] -> [Uniq]) -> m [Uniq] -> m [Uniq]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> m [Uniq]
refs Exp
body
                  Jump Annote
_ JoinId
_ [Exp]
es               -> [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Uniq]] -> [Uniq]) -> m [[Uniq]] -> m [Uniq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m [Uniq]) -> [Exp] -> m [[Uniq]]
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 -> m [Uniq]
refs [Exp]
es
                  Case Annote
_ Ty
_ Exp
s Id
_ [Alt]
alts         -> [Uniq] -> [Uniq] -> [Uniq]
forall a. Semigroup a => a -> a -> a
(<>) ([Uniq] -> [Uniq] -> [Uniq]) -> m [Uniq] -> m ([Uniq] -> [Uniq])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m [Uniq]
refs Exp
s m ([Uniq] -> [Uniq]) -> m [Uniq] -> m [Uniq]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Uniq]] -> [Uniq]) -> m [[Uniq]] -> m [Uniq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Alt -> m [Uniq]) -> [Alt] -> m [[Uniq]]
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 (\ (Alt Annote
_ AltCon
_ [Id]
_ Exp
b) -> Exp -> m [Uniq]
refs Exp
b) [Alt]
alts)
                  LitList Annote
_ Ty
_ [Exp]
es            -> [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Uniq]] -> [Uniq]) -> m [[Uniq]] -> m [Uniq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m [Uniq]) -> [Exp] -> m [[Uniq]]
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 -> m [Uniq]
refs [Exp]
es
                  LitVec Annote
_ Ty
_ [Exp]
es             -> [[Uniq]] -> [Uniq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Uniq]] -> [Uniq]) -> m [[Uniq]] -> m [Uniq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m [Uniq]) -> [Exp] -> m [[Uniq]]
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 -> m [Uniq]
refs [Exp]
es
                  Exp
_                         -> [Uniq] -> m [Uniq]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

            argRefs :: Arg -> m [Uniq]
            argRefs :: Arg -> m [Uniq]
argRefs = \ case
                  EArg Exp
e -> Exp -> m [Uniq]
refs Exp
e
                  TArg Ty
_ -> [Uniq] -> m [Uniq]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []