{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE CPP #-}

-- | This module implements the check that the transformed code is
-- typable in the single tick calculus.

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, -- ^ recursively defined variables 
    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

-- should be equatable
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{
  -- if present, contains the variable of the primitive applied so we can report its position
  -- in case of an error, and the clock for the primitive
  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

-- Combines two CheckResults such that the clocks therein are compatible.
-- If both CheckResults have PrimVars, one is picked arbitrarily.
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'}