{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | Well-formedness checking for Hyle programs (doc/hyle.md, section 4):
--   syntax-directed expression typing (every node's cached width is
--   verified), declaration well-formedness, device scoping and
--   exactly-once assignment coverage, and acyclicity of the call graph
--   (including extern-model edges).
module ReWire.Hyle.Check (check) where

import ReWire.Annotation (ann, Annote)
import ReWire.Error (failAt, failInternal, MonadError, AstError)
import ReWire.Hyle.Syntax
import ReWire.Pretty (showt)

import qualified ReWire.BitVector as BV

import Control.Monad (unless, when, foldM, foldM_, zipWithM_)
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.List (sort, group)
import Data.Text (Text)

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

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

type Ctx = HashMap Name Size

check :: MonadError AstError m => Program -> m Program
check :: forall (m :: * -> *). MonadError AstError m => Program -> m Program
check p :: Program
p@(Program [Extern]
exts [Defn]
ds Device
dev) = do
      Annote -> GId -> [GId] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [GId] -> m ()
checkDistinct (Device -> Annote
forall a. Annotated a => a -> Annote
ann Device
dev) GId
"global name" ([GId] -> m ()) -> [GId] -> m ()
forall a b. (a -> b) -> a -> b
$ (Extern -> GId) -> [Extern] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map Extern -> GId
extName [Extern]
exts [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> (Defn -> GId) -> [Defn] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map Defn -> GId
defnName [Defn]
ds
      (Extern -> m ()) -> [Extern] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Extern -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Extern -> m ()
checkExtern Env
env) [Extern]
exts
      (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]
ds
      Env -> Device -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Device -> m ()
checkDevice Env
env Device
dev
      Env -> [Defn] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> [Defn] -> m ()
checkRecursion Env
env [Defn]
ds
      Program -> m Program
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Program
p
      where env :: Env
            env :: Env
env = HashMap GId Defn -> HashMap GId Extern -> Env
Env ([(GId, Defn)] -> HashMap GId Defn
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(GId, Defn)] -> HashMap GId Defn)
-> [(GId, Defn)] -> HashMap GId Defn
forall a b. (a -> b) -> a -> b
$ (Defn -> (GId, Defn)) -> [Defn] -> [(GId, Defn)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Defn
d -> (Defn -> GId
defnName Defn
d, Defn
d)) [Defn]
ds)
                      ([(GId, Extern)] -> HashMap GId Extern
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(GId, Extern)] -> HashMap GId Extern)
-> [(GId, Extern)] -> HashMap GId Extern
forall a b. (a -> b) -> a -> b
$ (Extern -> (GId, Extern)) -> [Extern] -> [(GId, Extern)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Extern
e -> (Extern -> GId
extName Extern
e, Extern
e)) [Extern]
exts)

checkDistinct :: MonadError AstError m => Annote -> Text -> [Name] -> m ()
checkDistinct :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [GId] -> m ()
checkDistinct Annote
an GId
what [GId]
xs = case ([GId] -> Bool) -> [[GId]] -> [[GId]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Int -> Bool) -> ([GId] -> Int) -> [GId] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[GId]] -> [[GId]]) -> [[GId]] -> [[GId]]
forall a b. (a -> b) -> a -> b
$ [GId] -> [[GId]]
forall a. Eq a => [a] -> [[a]]
group ([GId] -> [[GId]]) -> [GId] -> [[GId]]
forall a b. (a -> b) -> a -> b
$ [GId] -> [GId]
forall a. Ord a => [a] -> [a]
sort [GId]
xs of
      []           -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (GId
x : [GId]
_) : [[GId]]
_  -> Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"duplicate " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
what GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x
      [[GId]]
_            -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

---

checkExtern :: MonadError AstError m => Env -> Extern -> m ()
checkExtern :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Extern -> m ()
checkExtern Env
env (Extern Annote
an GId
n [GId]
gs ExternKind
k [(GId, Size)]
ins [(GId, Size)]
outs Maybe GId
m) = do
      Annote -> GId -> [GId] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [GId] -> m ()
checkDistinct Annote
an (GId
"port or generic name of extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n) ([GId] -> m ()) -> [GId] -> m ()
forall a b. (a -> b) -> a -> b
$ [GId]
gs [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> ((GId, Size) -> GId) -> [(GId, Size)] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> GId
forall a b. (a, b) -> a
fst [(GId, Size)]
ins [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> ((GId, Size) -> GId) -> [(GId, Size)] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> GId
forall a b. (a, b) -> a
fst [(GId, Size)]
outs
      ((GId, Size) -> m ()) -> [(GId, Size)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GId -> m ()
forall (m :: * -> *). MonadError AstError m => GId -> m ()
checkPortName (GId -> m ()) -> ((GId, Size) -> GId) -> (GId, Size) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GId, Size) -> GId
forall a b. (a, b) -> a
fst) ([(GId, Size)] -> m ()) -> [(GId, Size)] -> m ()
forall a b. (a -> b) -> a -> b
$ [(GId, Size)]
ins [(GId, Size)] -> [(GId, Size)] -> [(GId, Size)]
forall a. Semigroup a => a -> a -> a
<> [(GId, Size)]
outs
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(GId, Size)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(GId, Size)]
outs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" has no outputs"
      case (ExternKind
k, Maybe GId
m) of
            (ExternKind
Comb, Just GId
g) -> case GId -> HashMap GId Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
g (HashMap GId Defn -> Maybe Defn) -> HashMap GId Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Defn
envDefns Env
env of
                  Maybe Defn
Nothing -> Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": unknown model defn " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
g
                  Just Defn
d | Sig Annote
_ [Size]
args Size
res <- Defn -> Sig
defnSig Defn
d -> do
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Size]
args [Size] -> [Size] -> Bool
forall a. Eq a => a -> a -> Bool
== ((GId, Size) -> Size) -> [(GId, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> Size
forall a b. (a, b) -> b
snd [(GId, Size)]
ins) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": model " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
g GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": argument widths do not match the extern's inputs"
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Size
res Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== [Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((GId, Size) -> Size) -> [(GId, Size)] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> Size
forall a b. (a, b) -> b
snd [(GId, Size)]
outs)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": model " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
g GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": result width does not match the extern's outputs"
            (Seq Maybe GId
_ Maybe GId
_, Just GId
_) -> Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": sequential externs cannot carry a model"
            (ExternKind, Maybe GId)
_                 -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      where checkPortName :: MonadError AstError m => Name -> m ()
            checkPortName :: forall (m :: * -> *). MonadError AstError m => GId -> m ()
checkPortName GId
x = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GId -> Bool
T.null GId
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                  Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": empty port name"

---

checkDefn :: MonadError AstError m => Env -> Defn -> m ()
checkDefn :: forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn Env
env (Defn Annote
an GId
n (Sig Annote
_ [Size]
args Size
res) [GId]
ps Exp
body Bool
_ Blind [GId]
_) = do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [GId]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Size] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
args) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
            Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
n GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": parameter count does not match signature"
      Annote -> GId -> [GId] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [GId] -> m ()
checkDistinct Annote
an (GId
"parameter of " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n) [GId]
ps
      sz <- Env -> Ctx -> Exp -> m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Ctx -> Exp -> m Size
checkExp Env
env ([(GId, Size)] -> Ctx
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(GId, Size)] -> Ctx) -> [(GId, Size)] -> Ctx
forall a b. (a -> b) -> a -> b
$ [GId] -> [Size] -> [(GId, Size)]
forall a b. [a] -> [b] -> [(a, b)]
zip [GId]
ps [Size]
args) Exp
body
      unless (sz == res) $
            failInternal an $ n <> ": body width " <> showt sz <> " does not match declared result width " <> showt res

-- | Verifies every node bottom-up, including its cached width, and returns
--   the expression's width.
checkExp :: MonadError AstError m => Env -> Ctx -> Exp -> m Size
checkExp :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Ctx -> Exp -> m Size
checkExp Env
env = Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go
      where go :: MonadError AstError m => Ctx -> Exp -> m Size
            go :: forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx = \ case
                  Lit Annote
an BV
bv -> do
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BV -> Integer
BV.nat BV
bv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| BV -> Integer
BV.nat BV
bv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ BV -> Int
BV.width BV
bv) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an GId
"literal value out of range for its width"
                        Size -> m Size
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> m Size) -> Size -> m Size
forall a b. (a -> b) -> a -> b
$ Int -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Size) -> Int -> Size
forall a b. (a -> b) -> a -> b
$ BV -> Int
BV.width BV
bv
                  Undef Annote
_ Size
sz -> Size -> m Size
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
sz
                  Var Annote
an Size
sz GId
x -> case GId -> Ctx -> Maybe Size
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
x Ctx
ctx of
                        Just Size
sz' | Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
sz' -> Size -> m Size
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
sz
                                 | Bool
otherwise -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ GId
"variable " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": cached width " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Size -> GId
forall a. TextShow a => a -> GId
showt Size
sz GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" does not match its binding (" GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Size -> GId
forall a. TextShow a => a -> GId
showt Size
sz' GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
")"
                        Maybe Size
Nothing              -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ GId
"unbound variable: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x
                  Cat Annote
_ Exp
e1 Exp
e2 -> Size -> Size -> Size
forall a. Num a => a -> a -> a
(+) (Size -> Size -> Size) -> m Size -> m (Size -> Size)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx Exp
e1 m (Size -> Size) -> m Size -> m Size
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx Exp
e2
                  Slice Annote
an Size
i Size
k Exp
e -> do
                        sz <- Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx Exp
e
                        unless (fromIntegral i + k <= sz) $
                              failAt an $ "slice [" <> showt i <> " +: " <> showt k <> "] out of bounds for width " <> showt sz
                        pure k
                  Prim Annote
an Size
sz Op
op [Exp]
es -> do
                        szs <- (Exp -> m Size) -> [Exp] -> m [Size]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx) [Exp]
es
                        case opResultSize op szs of
                              Just Size
sz' | Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
sz' -> Size -> m Size
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
sz
                                       | Bool
otherwise -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ Op -> GId
opName Op
op GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": cached width mismatch"
                              Maybe Size
Nothing              -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ GId
"ill-typed application of " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Op -> GId
opName Op
op GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" to operand widths " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> [Size] -> GId
forall a. TextShow a => a -> GId
showt [Size]
szs
                  Call Annote
an Size
sz GId
g [Exp]
es -> case GId -> HashMap GId Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
g (HashMap GId Defn -> Maybe Defn) -> HashMap GId Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Defn
envDefns Env
env of
                        Maybe Defn
Nothing -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ GId
"call to unknown definition: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
g
                        Just (Defn -> Sig
defnSig -> Sig Annote
_ [Size]
args Size
res) -> do
                              szs <- (Exp -> m Size) -> [Exp] -> m [Size]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx) [Exp]
es
                              checkArgs an g args szs
                              unless (sz == res) $ failInternal an $ "call to " <> g <> ": cached width mismatch"
                              pure res
                  XCall Annote
an Size
sz GId
x [Natural]
cs [Exp]
es -> case GId -> HashMap GId Extern -> Maybe Extern
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
x (HashMap GId Extern -> Maybe Extern)
-> HashMap GId Extern -> Maybe Extern
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Extern
envExterns Env
env of
                        Maybe Extern
Nothing -> Annote -> GId -> m Size
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failAt Annote
an (GId -> m Size) -> GId -> m Size
forall a b. (a -> b) -> a -> b
$ GId
"call to unknown extern: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x
                        Just Extern
ex -> do
                              Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Extern -> ExternKind
extKind Extern
ex ExternKind -> ExternKind -> Bool
forall a. Eq a => a -> a -> Bool
== ExternKind
Comb) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                                    Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" is sequential and cannot be called (instantiate it at device level)"
                              Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Natural]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Extern -> [GId]
extGenerics Extern
ex)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                                    Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": expected " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([GId] -> Int) -> [GId] -> Int
forall a b. (a -> b) -> a -> b
$ Extern -> [GId]
extGenerics Extern
ex) GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" generic arguments, got " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Natural]
cs)
                              szs <- (Exp -> m Size) -> [Exp] -> m [Size]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx) [Exp]
es
                              checkArgs an x (map snd $ extInputs ex) szs
                              unless (sz == externResultSize ex) $
                                    failInternal an $ "call to extern " <> x <> ": cached width mismatch"
                              pure sz
                  If Annote
an Size
sz Exp
c Exp
t Exp
e -> do
                        szc <- Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx Exp
c
                        unless (szc == 1) $ failInternal an $ "if condition has width " <> showt szc <> " (expected 1)"
                        szt <- go ctx t
                        sze <- go ctx e
                        unless (szt == sze) $ failInternal an $ "if branches have unequal widths (" <> showt szt <> " and " <> showt sze <> ")"
                        unless (sz == szt) $ failInternal an "if: cached width mismatch"
                        pure sz
                  Let Annote
an Size
sz GId
x Exp
e1 Exp
e2 -> do
                        sz1 <- Ctx -> Exp -> m Size
forall (m :: * -> *). MonadError AstError m => Ctx -> Exp -> m Size
go Ctx
ctx Exp
e1
                        sz2 <- go (Map.insert x sz1 ctx) e2
                        unless (sz == sz2) $ failInternal an $ "let " <> x <> ": cached width mismatch"
                        pure sz

            checkArgs :: MonadError AstError m => Annote -> Name -> [Size] -> [Size] -> m ()
            checkArgs :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [Size] -> [Size] -> m ()
checkArgs Annote
an GId
who [Size]
args [Size]
szs = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Size] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Size] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
szs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"call to " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
who GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": expected " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([Size] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
args) GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" arguments, got " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([Size] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
szs)
                  (Int -> (Size, Size) -> m ()) -> [Int] -> [(Size, Size)] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\ Int
i (Size
w, Size
w') -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Size
w Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
w') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"call to " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
who GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": argument " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt Int
i GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" has width " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Size -> GId
forall a. TextShow a => a -> GId
showt Size
w' GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" (expected " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Size -> GId
forall a. TextShow a => a -> GId
showt Size
w GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
")")
                        [Int
0 :: Int ..] ([Size] -> [Size] -> [(Size, Size)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Size]
args [Size]
szs)

---

checkDevice :: MonadError AstError m => Env -> Device -> m ()
checkDevice :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Device -> m ()
checkDevice Env
env (Device Annote
an GId
n [(GId, Size)]
ins [(GId, Size)]
outs [Register]
regs [Instance]
insts [Stmt]
body Blind [(GId, Integer)]
_) = do
      Annote -> GId -> [GId] -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> GId -> [GId] -> m ()
checkDistinct Annote
an (GId
"local name of device " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
n) [GId]
locals
      (GId -> m ()) -> [GId] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ GId -> m ()
forall (m :: * -> *). MonadError AstError m => GId -> m ()
checkLocalName [GId]
locals
      (Register -> m ()) -> [Register] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Register -> m ()
forall (m :: * -> *). MonadError AstError m => Register -> m ()
checkRegister [Register]
regs
      instCtx <- (Ctx -> Instance -> m Ctx) -> Ctx -> [Instance] -> m Ctx
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Ctx -> Instance -> m Ctx
forall (m :: * -> *).
MonadError AstError m =>
Ctx -> Instance -> m Ctx
checkInstance Ctx
forall a. Monoid a => a
mempty [Instance]
insts
      let ambient = [(GId, Size)] -> Ctx
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [(GId, Size)]
ins
                 Ctx -> Ctx -> Ctx
forall a. Semigroup a => a -> a -> a
<> [(GId, Size)] -> Ctx
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ((Register -> (GId, Size)) -> [Register] -> [(GId, Size)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Register Annote
_ GId
x Size
sz BV
_) -> (GId
x, Size
sz)) [Register]
regs)
                 Ctx -> Ctx -> Ctx
forall a. Semigroup a => a -> a -> a
<> Ctx
instCtx
      (_, assigned) <- foldM checkStmt (ambient, mempty) body
      mapM_ (checkAssigned assigned "output" . fst) outs
      mapM_ (\ (Register Annote
_ GId
x Size
_ BV
_) -> HashSet GId -> GId -> GId -> m ()
forall (m :: * -> *).
MonadError AstError m =>
HashSet GId -> GId -> GId -> m ()
checkAssigned HashSet GId
assigned GId
"register" (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"next " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x) regs
      mapM_ (checkInstAssigned assigned) insts
      where locals :: [Name]
            locals :: [GId]
locals = ((GId, Size) -> GId) -> [(GId, Size)] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> GId
forall a b. (a, b) -> a
fst [(GId, Size)]
ins [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> ((GId, Size) -> GId) -> [(GId, Size)] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (GId, Size) -> GId
forall a b. (a, b) -> a
fst [(GId, Size)]
outs [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> (Register -> GId) -> [Register] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Register Annote
_ GId
x Size
_ BV
_) -> GId
x) [Register]
regs
                  [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> (Instance -> GId) -> [Instance] -> [GId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Instance Annote
_ GId
x GId
_ [Natural]
_) -> GId
x) [Instance]
insts [GId] -> [GId] -> [GId]
forall a. Semigroup a => a -> a -> a
<> [ GId
x | SLet Annote
_ GId
x Exp
_ <- [Stmt]
body ]

            outsCtx :: Ctx
            outsCtx :: Ctx
outsCtx = [(GId, Size)] -> Ctx
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [(GId, Size)]
outs

            checkLocalName :: MonadError AstError m => Name -> m ()
            checkLocalName :: forall (m :: * -> *). MonadError AstError m => GId -> m ()
checkLocalName GId
x = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GId -> Bool
T.null GId
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an GId
"empty device-local name"
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GId
"." GId -> GId -> Bool
`T.isInfixOf` GId
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"device-local name may not contain a dot: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x

            checkRegister :: MonadError AstError m => Register -> m ()
            checkRegister :: forall (m :: * -> *). MonadError AstError m => Register -> m ()
checkRegister (Register Annote
an' GId
x Size
sz BV
bv) =
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BV -> Int
BV.width BV
bv) Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
sz) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"register " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": initial value width " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt (BV -> Int
BV.width BV
bv) GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" does not match declared width " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Size -> GId
forall a. TextShow a => a -> GId
showt Size
sz

            -- | Returns the ambient context entries for the instance's
            --   output ports.
            checkInstance :: MonadError AstError m => Ctx -> Instance -> m Ctx
            checkInstance :: forall (m :: * -> *).
MonadError AstError m =>
Ctx -> Instance -> m Ctx
checkInstance Ctx
ctx (Instance Annote
an' GId
x GId
ex [Natural]
cs) = case GId -> HashMap GId Extern -> Maybe Extern
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
ex (HashMap GId Extern -> Maybe Extern)
-> HashMap GId Extern -> Maybe Extern
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Extern
envExterns Env
env of
                  Maybe Extern
Nothing -> Annote -> GId -> m Ctx
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failAt Annote
an' (GId -> m Ctx) -> GId -> m Ctx
forall a b. (a -> b) -> a -> b
$ GId
"instance " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": unknown extern: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
ex
                  Just Extern
e  -> do
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Extern -> ExternKind
extKind Extern
e ExternKind -> ExternKind -> Bool
forall a. Eq a => a -> a -> Bool
== ExternKind
Comb) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"instance " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": extern " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
ex GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" is combinational (call it instead)"
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Natural]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Extern -> [GId]
extGenerics Extern
e)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                              Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
"instance " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
": expected " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([GId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([GId] -> Int) -> [GId] -> Int
forall a b. (a -> b) -> a -> b
$ Extern -> [GId]
extGenerics Extern
e) GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" generic arguments, got " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> Int -> GId
forall a. TextShow a => a -> GId
showt ([Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Natural]
cs)
                        Ctx -> m Ctx
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ctx -> m Ctx) -> Ctx -> m Ctx
forall a b. (a -> b) -> a -> b
$ ((GId, Size) -> Ctx -> Ctx) -> Ctx -> [(GId, Size)] -> Ctx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (GId
p, Size
sz) -> GId -> Size -> Ctx -> Ctx
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert (GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
"." GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
p) Size
sz) Ctx
ctx ([(GId, Size)] -> Ctx) -> [(GId, Size)] -> Ctx
forall a b. (a -> b) -> a -> b
$ Extern -> [(GId, Size)]
extOutputs Extern
e

            checkStmt :: MonadError AstError m => (Ctx, HashSet Name) -> Stmt -> m (Ctx, HashSet Name)
            checkStmt :: forall (m :: * -> *).
MonadError AstError m =>
(Ctx, HashSet GId) -> Stmt -> m (Ctx, HashSet GId)
checkStmt (Ctx
ctx, HashSet GId
assigned) = \ case
                  SLet Annote
_ GId
x Exp
e -> do
                        sz <- Env -> Ctx -> Exp -> m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Ctx -> Exp -> m Size
checkExp Env
env Ctx
ctx Exp
e
                        pure (Map.insert x sz ctx, assigned)
                  SOutput Annote
an' GId
x Exp
e -> case GId -> Ctx -> Maybe Size
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
x Ctx
outsCtx of
                        Maybe Size
Nothing -> Annote -> GId -> m (Ctx, HashSet GId)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m (Ctx, HashSet GId)) -> GId -> m (Ctx, HashSet GId)
forall a b. (a -> b) -> a -> b
$ GId
"assignment to unknown output: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x
                        Just Size
sz -> (, ) Ctx
ctx (HashSet GId -> (Ctx, HashSet GId))
-> m (HashSet GId) -> m (Ctx, HashSet GId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
forall (m :: * -> *).
MonadError AstError m =>
Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
assignOnce Annote
an' HashSet GId
assigned GId
x Size
sz Exp
e Ctx
ctx
                  SNext Annote
an' GId
x Exp
e -> case [ Size
sz | Register Annote
_ GId
x' Size
sz BV
_ <- [Register]
regs, GId
x' GId -> GId -> Bool
forall a. Eq a => a -> a -> Bool
== GId
x ] of
                        [Size
sz] -> (, ) Ctx
ctx (HashSet GId -> (Ctx, HashSet GId))
-> m (HashSet GId) -> m (Ctx, HashSet GId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
forall (m :: * -> *).
MonadError AstError m =>
Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
assignOnce Annote
an' HashSet GId
assigned (GId
"next " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x) Size
sz Exp
e Ctx
ctx
                        [Size]
_    -> Annote -> GId -> m (Ctx, HashSet GId)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m (Ctx, HashSet GId)) -> GId -> m (Ctx, HashSet GId)
forall a b. (a -> b) -> a -> b
$ GId
"next-assignment to unknown register: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x
                  SInstIn Annote
an' GId
x GId
p Exp
e -> case [ Extern
e' | Instance Annote
_ GId
x' GId
ex [Natural]
_ <- [Instance]
insts, GId
x' GId -> GId -> Bool
forall a. Eq a => a -> a -> Bool
== GId
x, Just Extern
e' <- [GId -> HashMap GId Extern -> Maybe Extern
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
ex (HashMap GId Extern -> Maybe Extern)
-> HashMap GId Extern -> Maybe Extern
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Extern
envExterns Env
env] ] of
                        [Extern
ex] -> case GId -> [(GId, Size)] -> Maybe Size
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup GId
p ([(GId, Size)] -> Maybe Size) -> [(GId, Size)] -> Maybe Size
forall a b. (a -> b) -> a -> b
$ Extern -> [(GId, Size)]
extInputs Extern
ex of
                              Maybe Size
Nothing -> Annote -> GId -> m (Ctx, HashSet GId)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m (Ctx, HashSet GId)) -> GId -> m (Ctx, HashSet GId)
forall a b. (a -> b) -> a -> b
$ GId
"instance " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" has no input port " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
p
                              Just Size
sz -> (, ) Ctx
ctx (HashSet GId -> (Ctx, HashSet GId))
-> m (HashSet GId) -> m (Ctx, HashSet GId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
forall (m :: * -> *).
MonadError AstError m =>
Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
assignOnce Annote
an' HashSet GId
assigned (GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
"." GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
p) Size
sz Exp
e Ctx
ctx
                        [Extern]
_    -> Annote -> GId -> m (Ctx, HashSet GId)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m (Ctx, HashSet GId)) -> GId -> m (Ctx, HashSet GId)
forall a b. (a -> b) -> a -> b
$ GId
"assignment to unknown instance: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x

            assignOnce :: MonadError AstError m => Annote -> HashSet Name -> Name -> Size -> Exp -> Ctx -> m (HashSet Name)
            assignOnce :: forall (m :: * -> *).
MonadError AstError m =>
Annote
-> HashSet GId -> GId -> Size -> Exp -> Ctx -> m (HashSet GId)
assignOnce Annote
an' HashSet GId
assigned GId
target Size
sz Exp
e Ctx
ctx = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GId
target GId -> HashSet GId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet GId
assigned) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                        Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an' (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
target GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" is assigned more than once"
                  sz' <- Env -> Ctx -> Exp -> m Size
forall (m :: * -> *).
MonadError AstError m =>
Env -> Ctx -> Exp -> m Size
checkExp Env
env Ctx
ctx Exp
e
                  unless (sz == sz') $
                        failInternal an' $ "assignment to " <> target <> ": width " <> showt sz' <> " (expected " <> showt sz <> ")"
                  pure $ Set.insert target assigned

            checkAssigned :: MonadError AstError m => HashSet Name -> Text -> Name -> m ()
            checkAssigned :: forall (m :: * -> *).
MonadError AstError m =>
HashSet GId -> GId -> GId -> m ()
checkAssigned HashSet GId
assigned GId
what GId
x = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (GId
x GId -> HashSet GId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet GId
assigned) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                  Annote -> GId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failInternal Annote
an (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
what GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
" is never assigned"

            checkInstAssigned :: MonadError AstError m => HashSet Name -> Instance -> m ()
            checkInstAssigned :: forall (m :: * -> *).
MonadError AstError m =>
HashSet GId -> Instance -> m ()
checkInstAssigned HashSet GId
assigned (Instance Annote
_ GId
x GId
ex [Natural]
_) = case GId -> HashMap GId Extern -> Maybe Extern
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
ex (HashMap GId Extern -> Maybe Extern)
-> HashMap GId Extern -> Maybe Extern
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Extern
envExterns Env
env of
                  Maybe Extern
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- already reported by checkInstance
                  Just Extern
e  -> ((GId, Size) -> m ()) -> [(GId, Size)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (GId
p, Size
_) -> HashSet GId -> GId -> GId -> m ()
forall (m :: * -> *).
MonadError AstError m =>
HashSet GId -> GId -> GId -> m ()
checkAssigned HashSet GId
assigned GId
"instance input" (GId -> m ()) -> GId -> m ()
forall a b. (a -> b) -> a -> b
$ GId
x GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
"." GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
p) ([(GId, Size)] -> m ()) -> [(GId, Size)] -> m ()
forall a b. (a -> b) -> a -> b
$ Extern -> [(GId, Size)]
extInputs Extern
e

---

-- | Check that the call graph is acyclic: a depth-first search over calls
--   (and extern-model references, which the interpreter follows like
--   calls), each defn visited at most once.
checkRecursion :: forall m. MonadError AstError m => Env -> [Defn] -> m ()
checkRecursion :: forall (m :: * -> *).
MonadError AstError m =>
Env -> [Defn] -> m ()
checkRecursion Env
env = (HashSet GId -> Defn -> m (HashSet GId))
-> HashSet GId -> [Defn] -> m ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ HashSet GId -> Defn -> m (HashSet GId)
visitDefn HashSet GId
forall a. Monoid a => a
mempty
      where visitDefn :: HashSet GId -> Defn -> m (HashSet GId)
            visitDefn :: HashSet GId -> Defn -> m (HashSet GId)
visitDefn HashSet GId
done (Defn Annote
_ GId
n Sig
_ [GId]
_ Exp
body Bool
_ Blind [GId]
_)
                  | GId
n GId -> HashSet GId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet GId
done = HashSet GId -> m (HashSet GId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet GId
done
                  | Bool
otherwise           = GId -> HashSet GId -> HashSet GId
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert GId
n (HashSet GId -> HashSet GId) -> m (HashSet GId) -> m (HashSet GId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp (GId -> HashSet GId
forall a. Hashable a => a -> HashSet a
Set.singleton GId
n) HashSet GId
done Exp
body

            visitExp :: HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
            visitExp :: HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack HashSet GId
done = \ case
                  Cat Annote
_ Exp
e1 Exp
e2        -> HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack HashSet GId
done Exp
e1 m (HashSet GId)
-> (HashSet GId -> m (HashSet GId)) -> m (HashSet GId)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (HashSet GId -> Exp -> m (HashSet GId))
-> Exp -> HashSet GId -> m (HashSet GId)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) Exp
e2
                  Slice Annote
_ Size
_ Size
_ Exp
e      -> HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack HashSet GId
done Exp
e
                  Prim Annote
_ Size
_ Op
_ [Exp]
es      -> (HashSet GId -> Exp -> m (HashSet GId))
-> HashSet GId -> [Exp] -> m (HashSet GId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) HashSet GId
done [Exp]
es
                  If Annote
_ Size
_ Exp
c Exp
t Exp
e       -> (HashSet GId -> Exp -> m (HashSet GId))
-> HashSet GId -> [Exp] -> m (HashSet GId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) HashSet GId
done [Exp
c, Exp
t, Exp
e]
                  Let Annote
_ Size
_ GId
_ Exp
e1 Exp
e2    -> HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack HashSet GId
done Exp
e1 m (HashSet GId)
-> (HashSet GId -> m (HashSet GId)) -> m (HashSet GId)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (HashSet GId -> Exp -> m (HashSet GId))
-> Exp -> HashSet GId -> m (HashSet GId)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) Exp
e2
                  Call Annote
an Size
_ GId
g [Exp]
es     -> (HashSet GId -> Exp -> m (HashSet GId))
-> HashSet GId -> [Exp] -> m (HashSet GId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) HashSet GId
done [Exp]
es m (HashSet GId)
-> (HashSet GId -> m (HashSet GId)) -> m (HashSet GId)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ HashSet GId
done' -> Annote -> HashSet GId -> HashSet GId -> GId -> m (HashSet GId)
visitCallee Annote
an HashSet GId
stack HashSet GId
done' GId
g
                  XCall Annote
an Size
_ GId
x [Natural]
_ [Exp]
es  -> do
                        done' <- (HashSet GId -> Exp -> m (HashSet GId))
-> HashSet GId -> [Exp] -> m (HashSet GId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp HashSet GId
stack) HashSet GId
done [Exp]
es
                        case Map.lookup x (envExterns env) >>= extModel of
                              Just GId
g  -> Annote -> HashSet GId -> HashSet GId -> GId -> m (HashSet GId)
visitCallee Annote
an HashSet GId
stack HashSet GId
done' GId
g
                              Maybe GId
Nothing -> HashSet GId -> m (HashSet GId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet GId
done'
                  Exp
_                  -> HashSet GId -> m (HashSet GId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet GId
done

            visitCallee :: Annote -> HashSet GId -> HashSet GId -> GId -> m (HashSet GId)
            visitCallee :: Annote -> HashSet GId -> HashSet GId -> GId -> m (HashSet GId)
visitCallee Annote
an HashSet GId
stack HashSet GId
done GId
g
                  | GId
g GId -> HashSet GId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet GId
stack                       = Annote -> GId -> m (HashSet GId)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> GId -> m a
failAt Annote
an (GId -> m (HashSet GId)) -> GId -> m (HashSet GId)
forall a b. (a -> b) -> a -> b
$ GId
"unsupported use of recursion (hyle id: " GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
g GId -> GId -> GId
forall a. Semigroup a => a -> a -> a
<> GId
")"
                  | GId
g GId -> HashSet GId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet GId
done                        = HashSet GId -> m (HashSet GId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet GId
done
                  | Just Defn
d <- GId -> HashMap GId Defn -> Maybe Defn
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup GId
g (HashMap GId Defn -> Maybe Defn) -> HashMap GId Defn -> Maybe Defn
forall a b. (a -> b) -> a -> b
$ Env -> HashMap GId Defn
envDefns Env
env      = GId -> HashSet GId -> HashSet GId
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert GId
g (HashSet GId -> HashSet GId) -> m (HashSet GId) -> m (HashSet GId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet GId -> HashSet GId -> Exp -> m (HashSet GId)
visitExp (GId -> HashSet GId -> HashSet GId
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert GId
g HashSet GId
stack) HashSet GId
done (Defn -> Exp
defnBody Defn
d)
                  | Bool
otherwise                                  = HashSet GId -> m (HashSet GId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet GId
done