{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- | Extern neutering (the retired Crust pass's successor).
--   Decides, per extern, whether the user-supplied Haskell implementation
--   (rwPrimExtern's seventh argument) can serve as a model for the
--   interpreter, and replaces it with an inert error placeholder
--   otherwise, so the simplifier never descends into extern
--   implementations. An implementation is kept only when it is a
--   reference to a top-level definition — other than the extern's own
--   enclosing definition, since @f = extern "f" f@ is the conventional
--   no-model idiom — whose reachable definitions are all non-recursive
--   and representable. Implementations that look like real models but
--   fail the checks are neutered with a warning.
--
--   Cryptol foreign functions (rwPrimCryptol's third argument, the
--   GHC-side implementation) are neutered unconditionally and silently:
--   their meaning is the Cryptol source, compiled to an ordinary
--   definition by the fold, so there is never a model to keep — only the
--   argument's type survives (the fold reads the use-site monotype off
--   the placeholder).
--
--   After INLINE inlining, an extern application is still wrapped in the
--   beta redexes left by inlining the extern/externWithSig wrappers, so
--   definitions containing externs are reduced first to expose the
--   implementation argument. (On Eidos this needs no isolated freshness
--   counter: the pass's supply is seeded above the program and perturbs
--   nothing else.) This pass must run before the simplifier.
module ReWire.Eidos.Externs (neuterExterns) where

import ReWire.Annotation (Annote, ann)
import ReWire.Builtins (Builtin (Error, Extern, Cryptol))
import ReWire.Error (AstError, MonadError, Warning (..))
import ReWire.Eidos.Simplify (SimpT, runSimpT, reduceExp, dictTyCons)
import ReWire.Eidos.Subst (freeUniqs)
import ReWire.Eidos.Syntax
import ReWire.Eidos.Types (typeOf, flattenApp, higherOrder, fundamental, synthable)

import Data.HashSet (HashSet)
import Data.Maybe (isJust)
import Data.Text (Text)

import qualified Data.HashSet       as Set
import qualified Data.IntMap.Strict as IM
import qualified Data.IntSet        as IS

-- | Returns the neutered program and the warnings for discarded models
--   (emitted by the caller, which holds the Config).
neuterExterns :: forall m. MonadError AstError m => Program -> m (Program, [Warning])
neuterExterns :: forall (m :: * -> *).
MonadError AstError m =>
Program -> m (Program, [Warning])
neuterExterns p :: Program
p@(Program [DataDefn]
datas [Defn]
defns Id
top) = do
      defns' <- Program -> SimpT m [Defn] -> m [Defn]
forall (m :: * -> *) a. Monad m => Program -> SimpT m a -> m a
runSimpT Program
p (SimpT m [Defn] -> m [Defn]) -> SimpT m [Defn] -> m [Defn]
forall a b. (a -> b) -> a -> b
$ (Defn -> StateT SimpSt m Defn) -> [Defn] -> SimpT m [Defn]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Defn -> StateT SimpSt m Defn
reduce1 [Defn]
defns
          -- Stage 1: neuter self-referential implementations silently
          -- (the no-model idiom), so they don't appear as spurious cycles
          -- in stage 2's recursion check.
      let ds1   = (Defn -> Defn) -> [Defn] -> [Defn]
forall a b. (a -> b) -> [a] -> [b]
map (\ Defn
d -> Defn
d { defnBody = neuterImpl (isSelf d) $ defnBody d }) [Defn]
defns'
          dmap1 = [(Int, Defn)] -> IntMap Defn
forall a. [(Int, a)] -> IntMap a
IM.fromList [ (Id -> Int
idUniq (Id -> Int) -> Id -> Int
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d, Defn
d) | Defn
d <- [Defn]
ds1 ]
          -- Stage 2: neuter everything else that isn't a usable model.
          ds2   = (Defn -> Defn) -> [Defn] -> [Defn]
forall a b. (a -> b) -> [a] -> [b]
map (\ Defn
d -> Defn
d { defnBody = neuterImpl (isJust . disposition dmap1) $ defnBody d }) [Defn]
ds1
          warns = [ Annote -> TyConId -> Warning
Warning (Defn -> Annote
defnAnnote Defn
d) (TyConId -> Warning) -> TyConId -> Warning
forall a b. (a -> b) -> a -> b
$ TyConId
"Ignoring the Haskell model for extern '" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Exp -> TyConId
exName Exp
ex
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
"': " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
reason TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
"; the interpreter will not be able to evaluate this extern."
                  | Defn
d <- [Defn]
ds1
                  , (Exp
ex, Exp
e) <- Exp -> [(Exp, Exp)]
externApps (Exp -> [(Exp, Exp)]) -> Exp -> [(Exp, Exp)]
forall a b. (a -> b) -> a -> b
$ Defn -> Exp
defnBody Defn
d
                  , Just (Just TyConId
reason) <- [IntMap Defn -> Exp -> Maybe (Maybe TyConId)
disposition IntMap Defn
dmap1 Exp
e]
                  ]
      pure (Program datas ds2 top, warns)
      where tops :: IS.IntSet
            tops :: IntSet
tops = [Int] -> IntSet
IS.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Defn -> Int) -> [Defn] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Int
idUniq (Id -> Int) -> (Defn -> Id) -> Defn -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Id
defnId) [Defn]
defns

            reduce1 :: Defn -> SimpT m Defn
            reduce1 :: Defn -> StateT SimpSt m Defn
reduce1 Defn
d
                  | Defn -> Bool
hasExtern Defn
d = (\ Exp
b -> Defn
d { defnBody = b }) (Exp -> Defn) -> StateT SimpSt m Exp -> StateT SimpSt m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> HashSet TyConId -> Exp -> StateT SimpSt m Exp
forall (m :: * -> *).
MonadError AstError m =>
IntSet -> HashSet TyConId -> Exp -> SimpT m Exp
reduceExp IntSet
tops ([DataDefn] -> HashSet TyConId
dictTyCons [DataDefn]
datas) (Defn -> Exp
defnBody Defn
d)
                  | Bool
otherwise   = Defn -> StateT SimpSt m Defn
forall a. a -> StateT SimpSt m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Defn
d

            hasExtern :: Defn -> Bool
            hasExtern :: Defn -> Bool
hasExtern = Exp -> Bool
go (Exp -> Bool) -> (Defn -> Exp) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Exp
defnBody
                  where go :: Exp -> Bool
                        go :: Exp -> Bool
go = \ case
                              Prim Annote
_ Ty
_ Builtin
Extern  -> Bool
True
                              Prim Annote
_ Ty
_ Builtin
Cryptol -> Bool
True
                              App Annote
_ Exp
f Arg
a       -> Exp -> Bool
go Exp
f Bool -> Bool -> Bool
|| Arg -> Bool
goArg Arg
a
                              Lam Annote
_ Id
_ Exp
b       -> Exp -> Bool
go Exp
b
                              Let Annote
_ Bind
b Exp
body    -> Bind -> Bool
goBind Bind
b Bool -> Bool -> Bool
|| Exp -> Bool
go Exp
body
                              Jump Annote
_ JoinId
_ [Exp]
es     -> (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Exp -> Bool
go [Exp]
es
                              Case Annote
_ Ty
_ Exp
s Id
_ [Alt]
as -> Exp -> Bool
go Exp
s Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Exp -> Bool
go Exp
b | Alt Annote
_ AltCon
_ [Id]
_ Exp
b <- [Alt]
as ]
                              LitList Annote
_ Ty
_ [Exp]
es  -> (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Exp -> Bool
go [Exp]
es
                              LitVec Annote
_ Ty
_ [Exp]
es   -> (Exp -> Bool) -> [Exp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Exp -> Bool
go [Exp]
es
                              Exp
_               -> Bool
False

                        goArg :: Arg -> Bool
                        goArg :: Arg -> Bool
goArg = \ case
                              EArg Exp
e -> Exp -> Bool
go Exp
e
                              Arg
_      -> Bool
False

                        goBind :: Bind -> Bool
                        goBind :: Bind -> Bool
goBind = \ case
                              NonRec Id
_ Exp
rhs -> Exp -> Bool
go Exp
rhs
                              Rec [(Id, Exp)]
bs       -> ((Id, Exp) -> Bool) -> [(Id, Exp)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Exp -> Bool
go (Exp -> Bool) -> ((Id, Exp) -> Exp) -> (Id, Exp) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Exp
forall a b. (a, b) -> b
snd) [(Id, Exp)]
bs
                              Join JoinId
_ [Id]
_ Exp
b   -> Exp -> Bool
go Exp
b

            isSelf :: Defn -> Exp -> Bool
            isSelf :: Defn -> Exp -> Bool
isSelf Defn
d = \ case
                  Var Annote
_ Id
x -> Id -> Int
idUniq Id
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Id -> Int
idUniq (Defn -> Id
defnId Defn
d)
                  Exp
_       -> Bool
False

            -- | Nothing: keep as a model. Just Nothing: neuter silently
            --   (already a placeholder, or a local name — the body of a
            --   generic wrapper, not a use site). Just (Just r): neuter,
            --   warning r.
            disposition :: IM.IntMap Defn -> Exp -> Maybe (Maybe Text)
            disposition :: IntMap Defn -> Exp -> Maybe (Maybe TyConId)
disposition IntMap Defn
dmap = \ case
                  Exp
e | Exp -> Bool
isPlaceholder Exp
e -> Maybe TyConId -> Maybe (Maybe TyConId)
forall a. a -> Maybe a
Just Maybe TyConId
forall a. Maybe a
Nothing
                  Var Annote
_ Id
x | Int -> IntSet -> Bool
IS.member (Id -> Int
idUniq Id
x) IntSet
tops -> TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just (TyConId -> Maybe TyConId)
-> Maybe TyConId -> Maybe (Maybe TyConId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap Defn -> HashSet Int -> Id -> Maybe TyConId
verdict IntMap Defn
dmap HashSet Int
forall a. Monoid a => a
mempty Id
x
                          | Bool
otherwise                 -> Maybe TyConId -> Maybe (Maybe TyConId)
forall a. a -> Maybe a
Just Maybe TyConId
forall a. Maybe a
Nothing
                  Exp
_ -> Maybe TyConId -> Maybe (Maybe TyConId)
forall a. a -> Maybe a
Just (Maybe TyConId -> Maybe (Maybe TyConId))
-> Maybe TyConId -> Maybe (Maybe TyConId)
forall a b. (a -> b) -> a -> b
$ TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just TyConId
"only a reference to a top-level definition can be used as a model"

            -- | DFS from a definition: every reachable definition must
            --   exist, have a usable type, and the call graph must be
            --   acyclic. Returns the first reason for rejection, or
            --   Nothing if usable as a model.
            verdict :: IM.IntMap Defn -> HashSet Uniq -> Id -> Maybe Text
            verdict :: IntMap Defn -> HashSet Int -> Id -> Maybe TyConId
verdict IntMap Defn
dmap HashSet Int
stack Id
x
                  | Int -> HashSet Int -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member (Id -> Int
idUniq Id
x) HashSet Int
stack = TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just (TyConId -> Maybe TyConId) -> TyConId -> Maybe TyConId
forall a b. (a -> b) -> a -> b
$ Id -> TyConId
idOcc Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is recursive"
                  | Bool
otherwise = case Int -> IntMap Defn -> Maybe Defn
forall a. Int -> IntMap a -> Maybe a
IM.lookup (Id -> Int
idUniq Id
x) IntMap Defn
dmap of
                        Maybe Defn
Nothing -> TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just (TyConId -> Maybe TyConId) -> TyConId -> Maybe TyConId
forall a b. (a -> b) -> a -> b
$ Id -> TyConId
idOcc Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" does not refer to a top-level definition"
                        Just Defn
d  -> case Defn -> Maybe TyConId
typeReason Defn
d of
                              Just TyConId
r  -> TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just TyConId
r
                              Maybe TyConId
Nothing -> (Id -> Maybe TyConId -> Maybe TyConId)
-> Maybe TyConId -> [Id] -> Maybe TyConId
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Maybe TyConId -> Maybe TyConId -> Maybe TyConId
forall a. Maybe a -> Maybe a -> Maybe a
orElse (Maybe TyConId -> Maybe TyConId -> Maybe TyConId)
-> (Id -> Maybe TyConId) -> Id -> Maybe TyConId -> Maybe TyConId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap Defn -> HashSet Int -> Id -> Maybe TyConId
verdict IntMap Defn
dmap (Int -> HashSet Int -> HashSet Int
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert (Id -> Int
idUniq Id
x) HashSet Int
stack)) Maybe TyConId
forall a. Maybe a
Nothing ([Id] -> Maybe TyConId) -> [Id] -> Maybe TyConId
forall a b. (a -> b) -> a -> b
$ Defn -> [Id]
succs Defn
d
                  where orElse :: Maybe a -> Maybe a -> Maybe a
                        orElse :: forall a. Maybe a -> Maybe a -> Maybe a
orElse Maybe a
a Maybe a
b = Maybe a -> (a -> Maybe a) -> Maybe a -> Maybe a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe a
b a -> Maybe a
forall a. a -> Maybe a
Just Maybe a
a

            typeReason :: Defn -> Maybe Text
            typeReason :: Defn -> Maybe TyConId
typeReason Defn
d
                  | Ty -> Bool
higherOrder Ty
t       = TyConId -> Maybe TyConId
reason TyConId
"has a higher-order type"
                  | Bool -> Bool
not (Ty -> Bool
fundamental Ty
t) = TyConId -> Maybe TyConId
reason TyConId
"has String or Integer arguments"
                  | Bool -> Bool
not ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs)      = TyConId -> Maybe TyConId
reason TyConId
"is polymorphic"
                  | Bool -> Bool
not (Ty -> Bool
synthable Ty
t)   = TyConId -> Maybe TyConId
reason TyConId
"has an unsynthesizable type"
                  | Bool
otherwise           = Maybe TyConId
forall a. Maybe a
Nothing
                  where Sig [TyVar]
tvs Ty
t = Id -> Sig
idSig (Id -> Sig) -> Id -> Sig
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d

                        reason :: Text -> Maybe Text
                        reason :: TyConId -> Maybe TyConId
reason TyConId
r = TyConId -> Maybe TyConId
forall a. a -> Maybe a
Just (TyConId -> Maybe TyConId) -> TyConId -> Maybe TyConId
forall a b. (a -> b) -> a -> b
$ Id -> TyConId
idOcc (Defn -> Id
defnId Defn
d) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
r

            -- | Top-level definitions referenced by a definition's body,
            --   as occurrence Ids (any occurrence serves — it carries the
            --   binder's signature).
            succs :: Defn -> [Id]
            succs :: Defn -> [Id]
succs Defn
d = IntMap Id -> [Id]
forall a. IntMap a -> [a]
IM.elems (IntMap Id -> [Id]) -> IntMap Id -> [Id]
forall a b. (a -> b) -> a -> b
$ IntMap Id -> IntSet -> IntMap Id
forall a. IntMap a -> IntSet -> IntMap a
IM.restrictKeys (Exp -> IntMap Id
occIds (Exp -> IntMap Id) -> Exp -> IntMap Id
forall a b. (a -> b) -> a -> b
$ Defn -> Exp
defnBody Defn
d) (IntSet -> IntMap Id) -> IntSet -> IntMap Id
forall a b. (a -> b) -> a -> b
$ Exp -> IntSet
freeUniqs (Defn -> Exp
defnBody Defn
d) IntSet -> IntSet -> IntSet
`IS.intersection` IntSet
tops
                  where occIds :: Exp -> IM.IntMap Id
                        occIds :: Exp -> IntMap Id
occIds = \ case
                              Var Annote
_ Id
v         -> Int -> Id -> IntMap Id
forall a. Int -> a -> IntMap a
IM.singleton (Id -> Int
idUniq Id
v) Id
v
                              App Annote
_ Exp
f Arg
a       -> Exp -> IntMap Id
occIds Exp
f IntMap Id -> IntMap Id -> IntMap Id
forall a. Semigroup a => a -> a -> a
<> Arg -> IntMap Id
occIdsArg Arg
a
                              Lam Annote
_ Id
_ Exp
b       -> Exp -> IntMap Id
occIds Exp
b
                              Let Annote
_ Bind
b Exp
body    -> Bind -> IntMap Id
occIdsBind Bind
b IntMap Id -> IntMap Id -> IntMap Id
forall a. Semigroup a => a -> a -> a
<> Exp -> IntMap Id
occIds Exp
body
                              Jump Annote
_ JoinId
_ [Exp]
es     -> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ (Exp -> IntMap Id) -> [Exp] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> IntMap Id
occIds [Exp]
es
                              Case Annote
_ Ty
_ Exp
s Id
_ [Alt]
as -> Exp -> IntMap Id
occIds Exp
s IntMap Id -> IntMap Id -> IntMap Id
forall a. Semigroup a => a -> a -> a
<> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions [ Exp -> IntMap Id
occIds Exp
b | Alt Annote
_ AltCon
_ [Id]
_ Exp
b <- [Alt]
as ]
                              LitList Annote
_ Ty
_ [Exp]
es  -> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ (Exp -> IntMap Id) -> [Exp] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> IntMap Id
occIds [Exp]
es
                              LitVec Annote
_ Ty
_ [Exp]
es   -> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ (Exp -> IntMap Id) -> [Exp] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> IntMap Id
occIds [Exp]
es
                              Exp
_               -> IntMap Id
forall a. Monoid a => a
mempty

                        occIdsArg :: Arg -> IM.IntMap Id
                        occIdsArg :: Arg -> IntMap Id
occIdsArg = \ case
                              EArg Exp
e -> Exp -> IntMap Id
occIds Exp
e
                              Arg
_      -> IntMap Id
forall a. Monoid a => a
mempty

                        occIdsBind :: Bind -> IM.IntMap Id
                        occIdsBind :: Bind -> IntMap Id
occIdsBind = \ case
                              NonRec Id
_ Exp
rhs -> Exp -> IntMap Id
occIds Exp
rhs
                              Rec [(Id, Exp)]
bs       -> [IntMap Id] -> IntMap Id
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IM.unions ([IntMap Id] -> IntMap Id) -> [IntMap Id] -> IntMap Id
forall a b. (a -> b) -> a -> b
$ ((Id, Exp) -> IntMap Id) -> [(Id, Exp)] -> [IntMap Id]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> IntMap Id
occIds (Exp -> IntMap Id) -> ((Id, Exp) -> Exp) -> (Id, Exp) -> IntMap Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Exp
forall a b. (a, b) -> b
snd) [(Id, Exp)]
bs
                              Join JoinId
_ [Id]
_ Exp
b   -> Exp -> IntMap Id
occIds Exp
b

            -- | Rewrite every extern implementation argument selected by
            --   the predicate into an inert placeholder.
            neuterImpl :: (Exp -> Bool) -> Exp -> Exp
            neuterImpl :: (Exp -> Bool) -> Exp -> Exp
neuterImpl Exp -> Bool
sel = Exp -> Exp
go
                  where go :: Exp -> Exp
                        go :: Exp -> Exp
go Exp
e = case Exp
e of
                              App Annote
an Exp
ex (EArg Exp
impl) | Exp -> Bool
isExtern Exp
ex, Exp -> Bool
sel Exp
impl, Bool -> Bool
not (Exp -> Bool
isPlaceholder Exp
impl) ->
                                    Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Exp
goE Exp
ex) (Arg -> Exp) -> Arg -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Arg
EArg (Exp -> Arg) -> Exp -> Arg
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> TyConId -> Exp
mkError (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
impl) (Exp -> Ty
typeOf Exp
impl) TyConId
"Extern expression placeholder"
                              App Annote
an Exp
cx (EArg Exp
impl) | Exp -> Bool
isCryptol Exp
cx, Bool -> Bool
not (Exp -> Bool
isPlaceholder Exp
impl) ->
                                    Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Exp
goE Exp
cx) (Arg -> Exp) -> Arg -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Arg
EArg (Exp -> Arg) -> Exp -> Arg
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> TyConId -> Exp
mkError (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
impl) (Exp -> Ty
typeOf Exp
impl) TyConId
"Cryptol expression placeholder"
                              App Annote
an Exp
f Arg
a      -> Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Exp
goE Exp
f) (Arg -> Exp) -> Arg -> Exp
forall a b. (a -> b) -> a -> b
$ Arg -> Arg
goA Arg
a
                              Exp
_               -> Exp -> Exp
goE Exp
e

                        goE :: Exp -> Exp
                        goE :: Exp -> Exp
goE Exp
e = case Exp
e of
                              App {}          -> Exp -> Exp
go Exp
e
                              Lam Annote
an Id
x Exp
b      -> Annote -> Id -> Exp -> Exp
Lam Annote
an Id
x (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
b
                              Let Annote
an Bind
b Exp
body   -> Annote -> Bind -> Exp -> Exp
Let Annote
an (Bind -> Bind
goB Bind
b) (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
go Exp
body
                              Jump Annote
an JoinId
j [Exp]
es    -> Annote -> JoinId -> [Exp] -> Exp
Jump Annote
an JoinId
j ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              Case Annote
an Ty
t Exp
s Id
cb [Alt]
alts -> Annote -> Ty -> Exp -> Id -> [Alt] -> Exp
Case Annote
an Ty
t (Exp -> Exp
go Exp
s) Id
cb [ Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
aan AltCon
c [Id]
xs (Exp -> Exp
go Exp
b) | Alt Annote
aan AltCon
c [Id]
xs Exp
b <- [Alt]
alts ]
                              LitList Annote
an Ty
t [Exp]
es -> Annote -> Ty -> [Exp] -> Exp
LitList Annote
an Ty
t ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              LitVec Annote
an Ty
t [Exp]
es  -> Annote -> Ty -> [Exp] -> Exp
LitVec Annote
an Ty
t ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
go [Exp]
es
                              Exp
_               -> Exp
e

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

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

            -- | All (extern-application, implementation-argument) pairs.
            externApps :: Exp -> [(Exp, Exp)]
            externApps :: Exp -> [(Exp, Exp)]
externApps Exp
e = [(Exp, Exp)]
here [(Exp, Exp)] -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. Semigroup a => a -> a -> a
<> [(Exp, Exp)]
below
                  where here :: [(Exp, Exp)]
here = case Exp
e of
                              App Annote
_ Exp
ex (EArg Exp
impl) | Exp -> Bool
isExtern Exp
ex -> [(Exp
ex, Exp
impl)]
                              Exp
_                                  -> []

                        below :: [(Exp, Exp)]
below = case Exp
e of
                              App Annote
_ Exp
f Arg
a       -> Exp -> [(Exp, Exp)]
externApps Exp
f [(Exp, Exp)] -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. Semigroup a => a -> a -> a
<> (case Arg
a of { EArg Exp
x -> Exp -> [(Exp, Exp)]
externApps Exp
x; Arg
_ -> [] })
                              Lam Annote
_ Id
_ Exp
b       -> Exp -> [(Exp, Exp)]
externApps Exp
b
                              Let Annote
_ Bind
b Exp
body    -> Bind -> [(Exp, Exp)]
bindApps Bind
b [(Exp, Exp)] -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. Semigroup a => a -> a -> a
<> Exp -> [(Exp, Exp)]
externApps Exp
body
                              Jump Annote
_ JoinId
_ [Exp]
es     -> (Exp -> [(Exp, Exp)]) -> [Exp] -> [(Exp, Exp)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Exp, Exp)]
externApps [Exp]
es
                              Case Annote
_ Ty
_ Exp
s Id
_ [Alt]
as -> Exp -> [(Exp, Exp)]
externApps Exp
s [(Exp, Exp)] -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. Semigroup a => a -> a -> a
<> [[(Exp, Exp)]] -> [(Exp, Exp)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Exp -> [(Exp, Exp)]
externApps Exp
b | Alt Annote
_ AltCon
_ [Id]
_ Exp
b <- [Alt]
as ]
                              LitList Annote
_ Ty
_ [Exp]
es  -> (Exp -> [(Exp, Exp)]) -> [Exp] -> [(Exp, Exp)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Exp, Exp)]
externApps [Exp]
es
                              LitVec Annote
_ Ty
_ [Exp]
es   -> (Exp -> [(Exp, Exp)]) -> [Exp] -> [(Exp, Exp)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Exp, Exp)]
externApps [Exp]
es
                              Exp
_               -> []

                        bindApps :: Bind -> [(Exp, Exp)]
                        bindApps :: Bind -> [(Exp, Exp)]
bindApps = \ case
                              NonRec Id
_ Exp
rhs -> Exp -> [(Exp, Exp)]
externApps Exp
rhs
                              Rec [(Id, Exp)]
bs       -> ((Id, Exp) -> [(Exp, Exp)]) -> [(Id, Exp)] -> [(Exp, Exp)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Exp -> [(Exp, Exp)]
externApps (Exp -> [(Exp, Exp)])
-> ((Id, Exp) -> Exp) -> (Id, Exp) -> [(Exp, Exp)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Exp
forall a b. (a, b) -> b
snd) [(Id, Exp)]
bs
                              Join JoinId
_ [Id]
_ Exp
b   -> Exp -> [(Exp, Exp)]
externApps Exp
b

            -- | A saturated extern application (six arguments; the
            --   seventh is the implementation).
            isExtern :: Exp -> Bool
            isExtern :: Exp -> Bool
isExtern Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
_ Ty
_ Builtin
Extern, [Arg]
args) -> [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ () | EArg Exp
_ <- [Arg]
args ] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
6
                  (Exp, [Arg])
_                       -> Bool
False

            -- | A saturated Cryptol foreign-function application (two
            --   arguments; the third is the GHC-side implementation).
            isCryptol :: Exp -> Bool
            isCryptol :: Exp -> Bool
isCryptol Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
_ Ty
_ Builtin
Cryptol, [Arg]
args) -> [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ () | EArg Exp
_ <- [Arg]
args ] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
                  (Exp, [Arg])
_                        -> Bool
False

            isPlaceholder :: Exp -> Bool
            isPlaceholder :: Exp -> Bool
isPlaceholder Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Prim Annote
_ Ty
_ Builtin
Error, [Arg]
_) -> Bool
True
                  (Exp, [Arg])
_                   -> Bool
False

            exName :: Exp -> Text
            exName :: Exp -> TyConId
exName Exp
e = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Exp
_, [Arg
_, Arg
_, Arg
_, Arg
_, Arg
_, EArg (LitStr Annote
_ TyConId
s)]) -> TyConId
s
                  (Exp, [Arg])
_                                       -> TyConId
"<unknown>"

mkError :: Annote -> Ty -> Text -> Exp
mkError :: Annote -> Ty -> TyConId -> Exp
mkError Annote
an Ty
t TyConId
m = Annote -> Exp -> Arg -> Exp
App Annote
an (Annote -> Ty -> Builtin -> Exp
Prim Annote
an (Annote -> Ty -> Ty -> Ty
Arrow Annote
an (Annote -> TyConId -> Ty
TyCon Annote
an TyConId
"String") Ty
t) Builtin
Error) (Arg -> Exp) -> Arg -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Arg
EArg (Exp -> Arg) -> Exp -> Arg
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> Exp
LitStr Annote
an TyConId
m