{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE CPP #-}
module AsyncRattus.Plugin.CheckClockCompatibility
(checkExpr, CheckExpr (..)) where
import GHC.Types.Tickish
import GHC.Plugins
import AsyncRattus.Plugin.Utils
import qualified AsyncRattus.Plugin.PrimExpr as Prim
import Prelude hiding ((<>))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust)
import Control.Monad (foldM, when)
import Control.Applicative ((<|>))
import System.Exit (exitFailure)
type LCtx = Set Var
data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef | DelayApp
type Hidden = Map Var HiddenReason
data TypeError = TypeError SrcSpan SDoc
data Ctx = Ctx
{ Ctx -> SymbolicClock
current :: LCtx,
Ctx -> Hidden
hidden :: Hidden,
Ctx -> Maybe SymbolicClock
earlier :: Maybe LCtx,
Ctx -> SrcSpan
srcLoc :: SrcSpan,
Ctx -> SymbolicClock
recDef :: Set Var,
Ctx -> SymbolicClock
stableTypes :: Set Var,
Ctx -> Bool
allowRecursion :: Bool,
Ctx -> Bool
allowGuardedRec :: Bool
}
hasTick :: Ctx -> Bool
hasTick :: Ctx -> Bool
hasTick = Maybe SymbolicClock -> Bool
forall a. Maybe a -> Bool
isJust (Maybe SymbolicClock -> Bool)
-> (Ctx -> Maybe SymbolicClock) -> Ctx -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx -> Maybe SymbolicClock
earlier
stabilize :: HiddenReason -> Ctx -> Ctx
stabilize :: HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
hr Ctx
c = Ctx
c
{current = Set.empty,
earlier = Nothing,
hidden = hidden c `Map.union` Map.fromSet (const hr) ctxHid,
allowGuardedRec = False
}
where ctxHid :: SymbolicClock
ctxHid = SymbolicClock
-> (SymbolicClock -> SymbolicClock)
-> Maybe SymbolicClock
-> SymbolicClock
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> SymbolicClock
current Ctx
c) (SymbolicClock -> SymbolicClock -> SymbolicClock
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> SymbolicClock
current Ctx
c)) (Ctx -> Maybe SymbolicClock
earlier Ctx
c)
data Scope = Hidden SDoc | Visible
getScope :: Ctx -> Var -> Scope
getScope :: Ctx -> Var -> Scope
getScope Ctx
c Var
v =
if Var
v Var -> SymbolicClock -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Ctx -> SymbolicClock
recDef Ctx
c then
if Ctx -> Bool
allowGuardedRec Ctx
c Bool -> Bool -> Bool
|| Ctx -> Bool
allowRecursion Ctx
c Bool -> Bool -> Bool
|| Var -> Bool
typeClassFunction Var
v then Scope
Visible
else SDoc -> Scope
Hidden (SDoc
"(Mutually) recursive call to " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" must occur under delay")
else case Var -> Hidden -> Maybe HiddenReason
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v (Ctx -> Hidden
hidden Ctx
c) of
Just HiddenReason
reason ->
if (SymbolicClock -> Kind -> Bool
isStable (Ctx -> SymbolicClock
stableTypes Ctx
c) (Var -> Kind
varType Var
v)) then Scope
Visible
else case HiddenReason
reason of
NestedRec Var
rv ->
if Ctx -> Bool
allowRecursion Ctx
c then Scope
Visible
else SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope:"
SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
"It appears in a local recursive definition (namely of " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
rv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
")"
SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
", which is not stable.")
HiddenReason
BoxApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
SDoc
"It occurs under " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
keyword SDoc
"box" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
", which is not stable.")
HiddenReason
AdvApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope: It occurs under adv.")
HiddenReason
FunDef -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope: It occurs in a function that is defined under a delay, is a of a non-stable type " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
", and is bound outside delay")
HiddenReason
DelayApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope: It occurs under two occurrences of delay and is a of a non-stable type " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v))
Maybe HiddenReason
Nothing
| Bool -> (SymbolicClock -> Bool) -> Maybe SymbolicClock -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Var -> SymbolicClock -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v) (Ctx -> Maybe SymbolicClock
earlier Ctx
c) ->
if SymbolicClock -> Kind -> Bool
isStable (Ctx -> SymbolicClock
stableTypes Ctx
c) (Var -> Kind
varType Var
v) then Scope
Visible
else SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
SDoc
"It occurs under delay" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
", which is not stable.")
| Var -> SymbolicClock -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v (Ctx -> SymbolicClock
current Ctx
c) -> Scope
Visible
| Bool
otherwise -> Scope
Visible
pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
pickFirst s :: SrcSpan
s@RealSrcSpan{} SrcSpan
_ = SrcSpan
s
pickFirst SrcSpan
_ SrcSpan
s = SrcSpan
s
typeError :: Ctx -> Var -> SDoc -> TypeError
typeError :: Ctx -> Var -> SDoc -> TypeError
typeError Ctx
ctx Var
var = SrcSpan -> SDoc -> TypeError
TypeError (SrcSpan -> SrcSpan -> SrcSpan
pickFirst (Ctx -> SrcSpan
srcLoc Ctx
ctx) (Name -> SrcSpan
nameSrcSpan (Var -> Name
varName Var
var)))
instance Outputable TypeError where
ppr :: TypeError -> SDoc
ppr (TypeError SrcSpan
srcLoc SDoc
sdoc) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TypeError at " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
srcLoc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
": " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr SDoc
sdoc
emptyCtx :: CheckExpr -> Ctx
emptyCtx :: CheckExpr -> Ctx
emptyCtx CheckExpr
c =
Ctx { current :: SymbolicClock
current = SymbolicClock
forall a. Set a
Set.empty,
earlier :: Maybe SymbolicClock
earlier = Maybe SymbolicClock
forall a. Maybe a
Nothing,
hidden :: Hidden
hidden = Hidden
forall k a. Map k a
Map.empty,
srcLoc :: SrcSpan
srcLoc = SrcSpan
noLocationInfo,
recDef :: SymbolicClock
recDef = CheckExpr -> SymbolicClock
recursiveSet CheckExpr
c,
stableTypes :: SymbolicClock
stableTypes = SymbolicClock
forall a. Set a
Set.empty,
allowRecursion :: Bool
allowRecursion = CheckExpr -> Bool
allowRecExp CheckExpr
c,
allowGuardedRec :: Bool
allowGuardedRec = Bool
False
}
stabilizeLater :: Ctx -> Ctx
stabilizeLater :: Ctx -> Ctx
stabilizeLater Ctx
c =
case Ctx -> Maybe SymbolicClock
earlier Ctx
c of
Just SymbolicClock
earl -> Ctx
c {earlier = Nothing,
hidden = hidden c `Map.union` Map.fromSet (const FunDef) earl}
Maybe SymbolicClock
Nothing -> Ctx
c
isStableConstr :: Type -> CoreM (Maybe Var)
isStableConstr :: Kind -> CoreM (Maybe Var)
isStableConstr Kind
t =
case (() :: Constraint) => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
splitTyConApp_maybe Kind
t of
Just (TyCon
con,[Kind
args]) ->
case TyCon -> Maybe (FastString, FastString)
forall a. NamedThing a => a -> Maybe (FastString, FastString)
getNameModule TyCon
con of
Just (FastString
name, FastString
mod) ->
if FastString -> Bool
isRattModule FastString
mod Bool -> Bool -> Bool
&& FastString
name FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
"Stable"
then Maybe Var -> CoreM (Maybe Var)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Maybe Var
getTyVar_maybe Kind
args)
else Maybe Var -> CoreM (Maybe Var)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Var
forall a. Maybe a
Nothing
Maybe (FastString, FastString)
_ -> Maybe Var -> CoreM (Maybe Var)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Var
forall a. Maybe a
Nothing
Maybe (TyCon, [Kind])
_ -> Maybe Var -> CoreM (Maybe Var)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Var
forall a. Maybe a
Nothing
type SymbolicClock = Set Var
mkClock1 :: Var -> SymbolicClock
mkClock1 :: Var -> SymbolicClock
mkClock1 = Var -> SymbolicClock
forall a. a -> Set a
Set.singleton
mkClock2 :: Var -> Var -> SymbolicClock
mkClock2 :: Var -> Var -> SymbolicClock
mkClock2 Var
v1 Var
v2 = [Var] -> SymbolicClock
forall a. Ord a => [a] -> Set a
Set.fromList [Var
v1, Var
v2]
newtype CheckResult = CheckResult{
CheckResult -> Maybe (Var, SymbolicClock)
prim :: Maybe (Var, SymbolicClock)
}
instance Outputable CheckResult where
ppr :: CheckResult -> SDoc
ppr (CheckResult Maybe (Var, SymbolicClock)
prim) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CheckResult {prim = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Maybe (Var, SymbolicClock) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe (Var, SymbolicClock)
prim SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"}"
emptyCheckResult :: CheckResult
emptyCheckResult :: CheckResult
emptyCheckResult = CheckResult {prim :: Maybe (Var, SymbolicClock)
prim = Maybe (Var, SymbolicClock)
forall a. Maybe a
Nothing}
data CheckExpr = CheckExpr{
CheckExpr -> SymbolicClock
recursiveSet :: Set Var,
CheckExpr -> Expr Var
oldExpr :: Expr Var,
CheckExpr -> Bool
verbose :: Bool,
CheckExpr -> Bool
allowRecExp :: Bool
}
checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr CheckExpr
c Expr Var
e = do
Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CheckExpr -> Bool
verbose CheckExpr
c) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ SDoc -> CoreM ()
putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"checkExpr: " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Expr Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Expr Var
e
Either TypeError CheckResult
res <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' (CheckExpr -> Ctx
emptyCtx CheckExpr
c) Expr Var
e
case Either TypeError CheckResult
res of
Right CheckResult
_ -> do Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CheckExpr -> Bool
verbose CheckExpr
c) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> CoreM ()
putMsgS String
"checkExpr succeeded."
Left (TypeError SrcSpan
src SDoc
doc) ->
let printErrMsg :: CoreM ()
printErrMsg = if CheckExpr -> Bool
verbose CheckExpr
c
then do
Severity -> SrcSpan -> SDoc -> CoreM ()
forall (m :: * -> *).
(HasDynFlags m, MonadIO m, HasLogger m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
SevError SrcSpan
src (SDoc
"Internal error in Async Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
doc)
String -> CoreM ()
putMsgS String
"-------- old --------"
SDoc -> CoreM ()
putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Expr Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckExpr -> Expr Var
oldExpr CheckExpr
c)
String -> CoreM ()
putMsgS String
"-------- new --------"
SDoc -> CoreM ()
putMsg (Expr Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Expr Var
e)
else do
Severity -> SrcSpan -> SDoc -> CoreM ()
forall (m :: * -> *).
(HasDynFlags m, MonadIO m, HasLogger m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
SevError SrcSpan
noSrcSpan (SDoc
"Internal error in Async Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
SDoc
"Compile with flags \"-fplugin-opt AsyncRattus.Plugin:debug\" and \"-g2\" for detailed information")
in do
CoreM ()
printErrMsg
IO () -> CoreM ()
forall a. IO a -> CoreM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
forall a. IO a
exitFailure
checkExpr' :: Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' :: Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c (App Expr Var
e Expr Var
e') | Expr Var -> Bool
forall {b}. Expr b -> Bool
isType Expr Var
e' Bool -> Bool -> Bool
|| (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind (Kind -> Bool) -> Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Kind -> Kind
Kind -> Kind
typeKind (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Expr Var -> Kind
Expr Var -> Kind
exprType Expr Var
e')
= Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e
checkExpr' c :: Ctx
c@Ctx{current :: Ctx -> SymbolicClock
current = SymbolicClock
cur, earlier :: Ctx -> Maybe SymbolicClock
earlier = Maybe SymbolicClock
earl} expr :: Expr Var
expr@(App Expr Var
e Expr Var
e') =
case Expr Var -> Maybe PrimInfo
Prim.isPrimExpr Expr Var
expr of
Just (Prim.BoxApp Var
_) ->
Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' (HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
BoxApp Ctx
c) Expr Var
e'
Just (Prim.DelayApp Var
f Kind
_) -> do
let c' :: Ctx
c' = case Maybe SymbolicClock
earl of
Maybe SymbolicClock
Nothing -> Ctx
c{current = Set.empty, earlier = Just cur, allowGuardedRec = True}
Just SymbolicClock
earl' -> Ctx
c{ current = Set.empty, earlier = Just cur, allowGuardedRec = True,
hidden = hidden c `Map.union` Map.fromSet (const DelayApp) earl'}
Either TypeError CheckResult
eRes <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c' Expr Var
e'
case Either TypeError CheckResult
eRes of
Left TypeError
err -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left TypeError
err
Right (CheckResult {prim :: CheckResult -> Maybe (Var, SymbolicClock)
prim = Maybe (Var, SymbolicClock)
Nothing}) -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left (TypeError -> Either TypeError CheckResult)
-> TypeError -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ Ctx -> Var -> SDoc -> TypeError
typeError Ctx
c Var
f (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Each delay must contain an adv or select")
Right CheckResult
_ -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
Just (Prim.AdvApp Var
f TypedArg
_) | Bool -> Bool
not (Ctx -> Bool
hasTick Ctx
c) -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left (TypeError -> Either TypeError CheckResult)
-> TypeError -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ Ctx -> Var -> SDoc -> TypeError
typeError Ctx
c Var
f (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"can only use adv under delay")
Just (Prim.AdvApp Var
f (Var
arg, Kind
_)) -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right (CheckResult -> Either TypeError CheckResult)
-> CheckResult -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ CheckResult {prim :: Maybe (Var, SymbolicClock)
prim = (Var, SymbolicClock) -> Maybe (Var, SymbolicClock)
forall a. a -> Maybe a
Just (Var
f, Var -> SymbolicClock
mkClock1 Var
arg)}
Just (Prim.SelectApp Var
f TypedArg
_ TypedArg
_) | Bool -> Bool
not (Ctx -> Bool
hasTick Ctx
c) -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left (TypeError -> Either TypeError CheckResult)
-> TypeError -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ Ctx -> Var -> SDoc -> TypeError
typeError Ctx
c Var
f (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"can only use select under delay")
Just (Prim.SelectApp Var
f (Var
arg1, Kind
_) (Var
arg2, Kind
_))-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right (CheckResult -> Either TypeError CheckResult)
-> CheckResult -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ CheckResult {prim :: Maybe (Var, SymbolicClock)
prim = (Var, SymbolicClock) -> Maybe (Var, SymbolicClock)
forall a. a -> Maybe a
Just (Var
f, Var -> Var -> SymbolicClock
mkClock2 Var
arg1 Var
arg2)}
Maybe PrimInfo
Nothing -> Ctx -> Expr Var -> Expr Var -> CoreM (Either TypeError CheckResult)
checkBoth Ctx
c Expr Var
e Expr Var
e'
checkExpr' Ctx
c (Case Expr Var
e Var
v Kind
_ [Alt Var]
alts) = do
Either TypeError CheckResult
res <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c' Expr Var
e
[Either TypeError CheckResult]
resAll <- (Alt Var -> CoreM (Either TypeError CheckResult))
-> [Alt Var] -> CoreM [Either TypeError CheckResult]
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 AltCon
_ [Var]
_ Expr Var
altE) -> Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
altE) [Alt Var]
alts
(Either TypeError CheckResult
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> [Either TypeError CheckResult]
-> CoreM (Either TypeError CheckResult)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> (Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b.
(a -> b)
-> (Either TypeError CheckResult -> a)
-> Either TypeError CheckResult
-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> (Either TypeError CheckResult
-> Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> Either TypeError CheckResult
combine Ctx
c) Either TypeError CheckResult
res [Either TypeError CheckResult]
resAll
where c' :: Ctx
c' = [Var] -> Ctx -> Ctx
addVars [Var
v] Ctx
c
checkExpr' Ctx
c (Lam Var
v Expr Var
e)
| Var -> Bool
isTyVar Var
v Bool -> Bool -> Bool
|| (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind (Kind -> Bool) -> Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Kind -> Kind
Kind -> Kind
typeKind (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ Var -> Kind
varType Var
v) = do
Maybe Var
is <- Kind -> CoreM (Maybe Var)
isStableConstr (Var -> Kind
varType Var
v)
let c' :: Ctx
c' = case Maybe Var
is of
Maybe Var
Nothing -> Ctx
c
Just Var
t -> Ctx
c{stableTypes = Set.insert t (stableTypes c)}
Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c' Expr Var
e
| Bool
otherwise = Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var
v] (Ctx -> Ctx
stabilizeLater Ctx
c)) Expr Var
e
checkExpr' Ctx
_ (Type Kind
_) = Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
checkExpr' Ctx
_ (Lit Literal
_) = Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
checkExpr' Ctx
_ (Coercion Coercion
_) = Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
checkExpr' Ctx
c (Tick (SourceNote RealSrcSpan
span String
_name) Expr Var
e) =
Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c{srcLoc = fromRealSrcSpan span} Expr Var
e
checkExpr' Ctx
c (Tick GenTickish 'TickishPassCore
_ Expr Var
e) = Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Cast Expr Var
e Coercion
_) = Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Let (NonRec Var
_ Expr Var
e1) Expr Var
e2) = do
Either TypeError CheckResult
res1 <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e1
Either TypeError CheckResult
res2 <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e2
Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ Ctx
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> Either TypeError CheckResult
combine Ctx
c Either TypeError CheckResult
res1 Either TypeError CheckResult
res2
checkExpr' Ctx
c (Let (Rec [(Var, Expr Var)]
binds) Expr Var
e2) = do
[Either TypeError CheckResult]
resAll <- ((Var, Expr Var) -> CoreM (Either TypeError CheckResult))
-> [(Var, Expr Var)] -> CoreM [Either TypeError CheckResult]
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 (\ (Var
v,Expr Var
e) -> Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' (Var -> Ctx
c' Var
v) Expr Var
e) [(Var, Expr Var)]
binds
Either TypeError CheckResult
res <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var]
vs Ctx
c) Expr Var
e2
(Either TypeError CheckResult
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> [Either TypeError CheckResult]
-> CoreM (Either TypeError CheckResult)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> (Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b.
(a -> b)
-> (Either TypeError CheckResult -> a)
-> Either TypeError CheckResult
-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> (Either TypeError CheckResult
-> Either TypeError CheckResult -> Either TypeError CheckResult)
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> Either TypeError CheckResult
combine Ctx
c) Either TypeError CheckResult
res [Either TypeError CheckResult]
resAll
where vs :: [Var]
vs = ((Var, Expr Var) -> Var) -> [(Var, Expr Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Expr Var) -> Var
forall a b. (a, b) -> a
fst [(Var, Expr Var)]
binds
ctxHid :: SymbolicClock
ctxHid = SymbolicClock
-> (SymbolicClock -> SymbolicClock)
-> Maybe SymbolicClock
-> SymbolicClock
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> SymbolicClock
current Ctx
c) (SymbolicClock -> SymbolicClock -> SymbolicClock
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> SymbolicClock
current Ctx
c)) (Ctx -> Maybe SymbolicClock
earlier Ctx
c)
c' :: Var -> Ctx
c' Var
v = Ctx
c {current = Set.empty,
earlier = Nothing,
hidden = hidden c `Map.union`
Map.fromSet (const (NestedRec v)) ctxHid,
recDef = recDef c `Set.union` Set.fromList vs }
checkExpr' Ctx
c (Var Var
v)
| Kind -> Bool
tcIsLiftedTypeKind (Kind -> Bool) -> Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Kind -> Kind
Kind -> Kind
typeKind (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ Var -> Kind
varType Var
v = case Ctx -> Var -> Scope
getScope Ctx
c Var
v of
Hidden SDoc
reason -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left (TypeError -> Either TypeError CheckResult)
-> TypeError -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ Ctx -> Var -> SDoc -> TypeError
typeError Ctx
c Var
v SDoc
reason
Scope
Visible -> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
| Bool
otherwise = Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
emptyCheckResult
addVars :: [Var] -> Ctx -> Ctx
addVars :: [Var] -> Ctx -> Ctx
addVars [Var]
v Ctx
c = Ctx
c{current = Set.fromList v `Set.union` current c }
checkBoth :: Ctx -> CoreExpr -> CoreExpr -> CoreM (Either TypeError CheckResult)
checkBoth :: Ctx -> Expr Var -> Expr Var -> CoreM (Either TypeError CheckResult)
checkBoth Ctx
c Expr Var
e Expr Var
e' = do
Either TypeError CheckResult
c1 <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e
Either TypeError CheckResult
c2 <- Ctx -> Expr Var -> CoreM (Either TypeError CheckResult)
checkExpr' Ctx
c Expr Var
e'
Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult))
-> Either TypeError CheckResult
-> CoreM (Either TypeError CheckResult)
forall a b. (a -> b) -> a -> b
$ Ctx
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> Either TypeError CheckResult
combine Ctx
c Either TypeError CheckResult
c1 Either TypeError CheckResult
c2
combine :: Ctx -> Either TypeError CheckResult -> Either TypeError CheckResult -> Either TypeError CheckResult
combine :: Ctx
-> Either TypeError CheckResult
-> Either TypeError CheckResult
-> Either TypeError CheckResult
combine Ctx
c Either TypeError CheckResult
eRes1 Either TypeError CheckResult
eRes2 = do
CheckResult
res1 <- Either TypeError CheckResult
eRes1
CheckResult
res2 <- Either TypeError CheckResult
eRes2
case (CheckResult
res1, CheckResult
res2) of
(CheckResult (Just (Var
_, SymbolicClock
cl1)), CheckResult (Just (Var
_, SymbolicClock
cl2))) | SymbolicClock
cl1 SymbolicClock -> SymbolicClock -> Bool
forall a. Eq a => a -> a -> Bool
== SymbolicClock
cl2 -> CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right CheckResult
res2
(CheckResult (Just (Var, SymbolicClock)
_), CheckResult (Just (Var
p, SymbolicClock
_))) -> TypeError -> Either TypeError CheckResult
forall a b. a -> Either a b
Left (TypeError -> Either TypeError CheckResult)
-> TypeError -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ Ctx -> Var -> SDoc -> TypeError
typeError Ctx
c Var
p SDoc
"Only one adv/select allowed in a delay"
(CheckResult Maybe (Var, SymbolicClock)
maybeP, CheckResult Maybe (Var, SymbolicClock)
maybeP') -> CheckResult -> Either TypeError CheckResult
forall a b. b -> Either a b
Right (CheckResult -> Either TypeError CheckResult)
-> CheckResult -> Either TypeError CheckResult
forall a b. (a -> b) -> a -> b
$ CheckResult {prim :: Maybe (Var, SymbolicClock)
prim = Maybe (Var, SymbolicClock)
maybeP Maybe (Var, SymbolicClock)
-> Maybe (Var, SymbolicClock) -> Maybe (Var, SymbolicClock)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (Var, SymbolicClock)
maybeP'}