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

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

module Rattus.Plugin.CheckSingleTick
  (checkExpr, CheckExpr (..)) where

#if __GLASGOW_HASKELL__ >= 900
import GHC.Plugins
#else
import GhcPlugins
#endif

import Rattus.Plugin.Utils 

import Prelude hiding ((<>))
import Control.Monad
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Applicative
import Data.Foldable

type LCtx = Set Var
data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef | DelayApp
type Hidden = Map Var HiddenReason

data Prim = Delay | Adv | Box | Arr

data TypeError = TypeError SrcSpan SDoc

instance Outputable Prim where
  ppr :: Prim -> SDoc
ppr Prim
Delay = SDoc
"delay"
  ppr Prim
Adv = SDoc
"adv"
  ppr Prim
Box = SDoc
"box"
  ppr Prim
Arr = SDoc
"arr"
  
data Ctx = Ctx
  { Ctx -> LCtx
current :: LCtx,
    Ctx -> Hidden
hidden :: Hidden,
    Ctx -> Maybe LCtx
earlier :: Maybe LCtx,
    Ctx -> SrcSpan
srcLoc :: SrcSpan,
    Ctx -> LCtx
recDef :: Set Var, -- ^ recursively defined variables 
    Ctx -> LCtx
stableTypes :: Set Var,
    Ctx -> Map Var Prim
primAlias :: Map Var Prim,
    -- number of ticks (for recursive calls). This is to allow
    -- recursive definitions of the form @f = delay (delay (adv f))@.
    Ctx -> Int
ticks :: Int} 

primMap :: Map FastString Prim
primMap :: Map FastString Prim
primMap = [(FastString, Prim)] -> Map FastString Prim
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [(FastString
"delay", Prim
Delay),
   (FastString
"adv", Prim
Adv),
   (FastString
"box", Prim
Box),
   (FastString
"arr", Prim
Arr)
   ]


isPrim :: Ctx -> Var -> Maybe Prim
isPrim :: Ctx -> Var -> Maybe Prim
isPrim Ctx
c Var
v
  | Just Prim
p <- Var -> Map Var Prim -> Maybe Prim
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v (Ctx -> Map Var Prim
primAlias Ctx
c) = Prim -> Maybe Prim
forall a. a -> Maybe a
Just Prim
p
  | Bool
otherwise = do
  (FastString
name,FastString
mod) <- Var -> Maybe (FastString, FastString)
forall a. NamedThing a => a -> Maybe (FastString, FastString)
getNameModule Var
v
  if FastString -> Bool
isRattModule FastString
mod then FastString -> Map FastString Prim -> Maybe Prim
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FastString
name Map FastString Prim
primMap
  else Maybe Prim
forall a. Maybe a
Nothing



stabilize :: HiddenReason -> Ctx -> Ctx
stabilize :: HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
hr Ctx
c = Ctx
c
  {current :: LCtx
current = LCtx
forall a. Set a
Set.empty,
   earlier :: Maybe LCtx
earlier = Maybe LCtx
forall a. Maybe a
Nothing,
   hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c Hidden -> Hidden -> Hidden
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` (Var -> HiddenReason) -> LCtx -> Hidden
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (HiddenReason -> Var -> HiddenReason
forall a b. a -> b -> a
const HiddenReason
hr) LCtx
ctxHid,
   ticks :: Int
ticks = Int
0}
  where ctxHid :: LCtx
ctxHid = LCtx -> (LCtx -> LCtx) -> Maybe LCtx -> LCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> LCtx
current Ctx
c) (LCtx -> LCtx -> LCtx
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> LCtx
current Ctx
c)) (Ctx -> Maybe LCtx
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 -> LCtx -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Ctx -> LCtx
recDef Ctx
c then
      if Ctx -> Int
ticks Ctx
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Scope
Visible
      else SDoc -> Scope
Hidden (SDoc
"(Mutually) recursive call to " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> 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 (LCtx -> Type -> Bool
isStable (Ctx -> LCtx
stableTypes Ctx
c) (Var -> Type
varType Var
v)) then Scope
Visible
        else case HiddenReason
reason of
          NestedRec Var
rv -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
$$ SDoc
"It appears in a local recursive definition (namely of " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
rv SDoc -> SDoc -> SDoc
<> SDoc
")"
                       SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          HiddenReason
BoxApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
$$
                       SDoc
"It occurs under " SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
keyword SDoc
"box" SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          HiddenReason
AdvApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope: It occurs under adv.")
        
          HiddenReason
FunDef -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> 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
<> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", and is bound outside delay")
          HiddenReason
DelayApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope: It occurs under two occurrences of delay and is a of a non-stable type " SDoc -> SDoc -> SDoc
<> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
v))
      Maybe HiddenReason
Nothing
          | Bool -> (LCtx -> Bool) -> Maybe LCtx -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Var -> LCtx -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v) (Ctx -> Maybe LCtx
earlier Ctx
c) ->
            if LCtx -> Type -> Bool
isStable (Ctx -> LCtx
stableTypes Ctx
c) (Var -> Type
varType Var
v) then Scope
Visible
            else SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
$$
                         SDoc
"It occurs under delay" SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          | Var -> LCtx -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v (Ctx -> LCtx
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 -> CoreM (Maybe TypeError)
typeError :: Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
cxt Var
var SDoc
doc =
  Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeError -> Maybe TypeError
forall a. a -> Maybe a
Just (SrcSpan -> SDoc -> TypeError
TypeError (SrcSpan -> SrcSpan -> SrcSpan
pickFirst (Ctx -> SrcSpan
srcLoc Ctx
cxt) (Name -> SrcSpan
nameSrcSpan (Var -> Name
varName Var
var))) SDoc
doc))


emptyCtx :: Set Var -> Ctx
emptyCtx :: LCtx -> Ctx
emptyCtx LCtx
vars =
  Ctx :: LCtx
-> Hidden
-> Maybe LCtx
-> SrcSpan
-> LCtx
-> LCtx
-> Map Var Prim
-> Int
-> Ctx
Ctx { current :: LCtx
current =  LCtx
forall a. Set a
Set.empty,
        earlier :: Maybe LCtx
earlier = Maybe LCtx
forall a. Maybe a
Nothing,
        hidden :: Hidden
hidden = Hidden
forall k a. Map k a
Map.empty,
        srcLoc :: SrcSpan
srcLoc = SrcSpan
noLocationInfo,
        recDef :: LCtx
recDef = LCtx
vars,
        primAlias :: Map Var Prim
primAlias = Map Var Prim
forall k a. Map k a
Map.empty,
        stableTypes :: LCtx
stableTypes = LCtx
forall a. Set a
Set.empty,
        ticks :: Int
ticks = Int
0}


isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim,Var)
isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c (App Expr Var
e (Type Type
_)) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
c (App Expr Var
e Expr Var
e') | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
tcIsLiftedTypeKind (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Expr Var -> Type
exprType Expr Var
e' = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
c (Var Var
v) = (Prim -> (Prim, Var)) -> Maybe Prim -> Maybe (Prim, Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Var
v) (Ctx -> Var -> Maybe Prim
isPrim Ctx
c Var
v)
isPrimExpr Ctx
c (Tick Tickish Var
_ Expr Var
e) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr 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
$ Type -> Bool
tcIsLiftedTypeKind (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
_ Expr Var
_ = Maybe (Prim, Var)
forall a. Maybe a
Nothing


stabilizeLater :: Ctx -> Ctx
stabilizeLater :: Ctx -> Ctx
stabilizeLater Ctx
c =
  case Ctx -> Maybe LCtx
earlier Ctx
c of
    Just LCtx
earl -> Ctx
c {earlier :: Maybe LCtx
earlier = Maybe LCtx
forall a. Maybe a
Nothing,
                    hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c Hidden -> Hidden -> Hidden
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` (Var -> HiddenReason) -> LCtx -> Hidden
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (HiddenReason -> Var -> HiddenReason
forall a b. a -> b -> a
const HiddenReason
FunDef) LCtx
earl}
    Maybe LCtx
Nothing -> Ctx
c 

isStableConstr :: Type -> CoreM (Maybe Var)
isStableConstr :: Type -> CoreM (Maybe Var)
isStableConstr Type
t = 
  case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
t of
    Just (TyCon
con,[Type
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 (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Var
getTyVar_maybe Type
args)
          else Maybe Var -> CoreM (Maybe Var)
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 (m :: * -> *) a. Monad m => a -> m a
return Maybe Var
forall a. Maybe a
Nothing                           
    Maybe (TyCon, [Type])
_ ->  Maybe Var -> CoreM (Maybe Var)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Var
forall a. Maybe a
Nothing


data CheckExpr = CheckExpr{
  CheckExpr -> LCtx
recursiveSet :: Set Var,
  CheckExpr -> Expr Var
oldExpr :: Expr Var,
  CheckExpr -> Bool
fatalError :: Bool,
  CheckExpr -> Bool
verbose :: Bool
  }

checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr CheckExpr
c Expr Var
e = do
  Maybe TypeError
res <- Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (LCtx -> Ctx
emptyCtx (CheckExpr -> LCtx
recursiveSet CheckExpr
c)) Expr Var
e
  case Maybe TypeError
res of
    Maybe TypeError
Nothing -> () -> CoreM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just (TypeError SrcSpan
src SDoc
doc) ->
      let sev :: Severity
sev = if CheckExpr -> Bool
fatalError CheckExpr
c then Severity
SevError else Severity
SevWarning
      in if CheckExpr -> Bool
verbose CheckExpr
c then do
        Severity -> SrcSpan -> SDoc -> CoreM ()
forall (m :: * -> *).
(HasDynFlags m, MonadIO m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
sev SrcSpan
src (SDoc
"Internal error in Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
$$ SDoc
doc)
        IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"-------- old --------"
        IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (SDoc -> String
showSDocUnsafe (Expr Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckExpr -> Expr Var
oldExpr CheckExpr
c)))
        IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"-------- new --------"
        IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (SDoc -> String
showSDocUnsafe (Expr Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Expr Var
e))
         else
        Severity -> SrcSpan -> SDoc -> CoreM ()
forall (m :: * -> *).
(HasDynFlags m, MonadIO m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
sev SrcSpan
noSrcSpan (SDoc
"Internal error in Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
$$
                             SDoc
"Compile with flags \"-fplugin-opt Rattus.Plugin:debug\" and \"-g2\" for detailed information")

checkExpr' :: Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' :: Ctx -> Expr Var -> CoreM (Maybe TypeError)
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
$ Type -> Bool
tcIsLiftedTypeKind (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Expr Var -> Type
exprType Expr Var
e')
  = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' c :: Ctx
c@Ctx{current :: Ctx -> LCtx
current = LCtx
cur, hidden :: Ctx -> Hidden
hidden = Hidden
hid, earlier :: Ctx -> Maybe LCtx
earlier = Maybe LCtx
earl} (App Expr Var
e1 Expr Var
e2) =
  case Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e1 of
    Just (Prim
p,Var
v) -> case Prim
p of
      Prim
Box -> do
        Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
BoxApp Ctx
c) Expr Var
e2
      Prim
Arr -> do
        Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
BoxApp Ctx
c) Expr Var
e2

      Prim
Delay -> case Maybe LCtx
earl of
        Just LCtx
earl' ->
          Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{current :: LCtx
current = LCtx
forall a. Set a
Set.empty, earlier :: Maybe LCtx
earlier = LCtx -> Maybe LCtx
forall a. a -> Maybe a
Just LCtx
cur,
                      ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c Hidden -> Hidden -> Hidden
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` (Var -> HiddenReason) -> LCtx -> Hidden
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (HiddenReason -> Var -> HiddenReason
forall a b. a -> b -> a
const HiddenReason
DelayApp) LCtx
earl'} Expr Var
e2
        Maybe LCtx
Nothing -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{current :: LCtx
current = LCtx
forall a. Set a
Set.empty, earlier :: Maybe LCtx
earlier = LCtx -> Maybe LCtx
forall a. a -> Maybe a
Just LCtx
cur, ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1} Expr Var
e2
      Prim
Adv -> case Maybe LCtx
earl of
        Just LCtx
er -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{earlier :: Maybe LCtx
earlier = Maybe LCtx
forall a. Maybe a
Nothing, current :: LCtx
current = LCtx
er, ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1,
                               hidden :: Hidden
hidden = Hidden
hid Hidden -> Hidden -> Hidden
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` (Var -> HiddenReason) -> LCtx -> Hidden
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (HiddenReason -> Var -> HiddenReason
forall a b. a -> b -> a
const HiddenReason
AdvApp) LCtx
cur} Expr Var
e2
        Maybe LCtx
Nothing -> Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
c Var
v (String -> SDoc
text String
"can only advance under delay")
    Maybe (Prim, Var)
_ -> (Maybe TypeError -> Maybe TypeError -> Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e1)  (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e2)
checkExpr' Ctx
c (Case Expr Var
e Var
v Type
_ [Alt Var]
alts) =
    (Maybe TypeError -> Maybe TypeError -> Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e) (([Maybe TypeError] -> Maybe TypeError)
-> CoreM [Maybe TypeError] -> CoreM (Maybe TypeError)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Maybe TypeError -> Maybe TypeError -> Maybe TypeError)
-> Maybe TypeError -> [Maybe TypeError] -> Maybe TypeError
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) Maybe TypeError
forall a. Maybe a
Nothing) ((Alt Var -> CoreM (Maybe TypeError))
-> [Alt Var] -> CoreM [Maybe TypeError]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (AltCon
_,[Var]
vs,Expr Var
e)-> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var]
vs Ctx
c') Expr Var
e) [Alt Var]
alts))
  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
$ Type -> Bool
tcIsLiftedTypeKind (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v) = do
      Maybe Var
is <- Type -> CoreM (Maybe Var)
isStableConstr (Var -> Type
varType Var
v)
      let c' :: Ctx
c' = case Maybe Var
is of
            Maybe Var
Nothing -> Ctx
c
            Just Var
t -> Ctx
c{stableTypes :: LCtx
stableTypes = Var -> LCtx -> LCtx
forall a. Ord a => a -> Set a -> Set a
Set.insert Var
t (Ctx -> LCtx
stableTypes Ctx
c)}
      Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c' Expr Var
e
  | Bool
otherwise = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var
v] (Ctx -> Ctx
stabilizeLater Ctx
c)) Expr Var
e
checkExpr' Ctx
_ (Type Type
_)  = Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
checkExpr' Ctx
_ (Lit Literal
_)  = Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
checkExpr' Ctx
_ (Coercion Coercion
_)  = Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
checkExpr' Ctx
c (Tick (SourceNote RealSrcSpan
span String
_name) Expr Var
e) =
  Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{srcLoc :: SrcSpan
srcLoc = RealSrcSpan -> SrcSpan
fromRealSrcSpan RealSrcSpan
span} Expr Var
e
checkExpr' Ctx
c (Tick Tickish Var
_ Expr Var
e) = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Cast Expr Var
e Coercion
_) = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Let (NonRec Var
v Expr Var
e1) Expr Var
e2) =
  case Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e1 of
    Just (Prim
p,Var
_) -> (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (Ctx
c{primAlias :: Map Var Prim
primAlias = Var -> Prim -> Map Var Prim -> Map Var Prim
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Prim
p (Ctx -> Map Var Prim
primAlias Ctx
c)}) Expr Var
e2)
    Maybe (Prim, Var)
Nothing -> (Maybe TypeError -> Maybe TypeError -> Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
-> CoreM (Maybe TypeError)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e1)  (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var
v] Ctx
c) Expr Var
e2)
checkExpr' Ctx
_ (Let (Rec ([])) Expr Var
_) = Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
checkExpr' Ctx
c (Let (Rec [(Var, Expr Var)]
binds) Expr Var
e2) = do
    [Maybe TypeError]
r1 <- ((Var, Expr Var) -> CoreM (Maybe TypeError))
-> [(Var, Expr Var)] -> CoreM [Maybe TypeError]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Var
v,Expr Var
e) -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (Var -> Ctx
c' Var
v) Expr Var
e) [(Var, Expr Var)]
binds
    Maybe TypeError
r2 <- Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var]
vs Ctx
c) Expr Var
e2
    Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe TypeError -> Maybe TypeError -> Maybe TypeError)
-> Maybe TypeError -> [Maybe TypeError] -> Maybe TypeError
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) Maybe TypeError
forall a. Maybe a
Nothing [Maybe TypeError]
r1 Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe TypeError
r2)  
  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 :: LCtx
ctxHid = LCtx -> (LCtx -> LCtx) -> Maybe LCtx -> LCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> LCtx
current Ctx
c) (LCtx -> LCtx -> LCtx
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> LCtx
current Ctx
c)) (Ctx -> Maybe LCtx
earlier Ctx
c)
        c' :: Var -> Ctx
c' Var
v = Ctx
c {current :: LCtx
current = LCtx
forall a. Set a
Set.empty,
                  earlier :: Maybe LCtx
earlier = Maybe LCtx
forall a. Maybe a
Nothing,
                  hidden :: Hidden
hidden =  Ctx -> Hidden
hidden Ctx
c Hidden -> Hidden -> Hidden
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union`
                   ((Var -> HiddenReason) -> LCtx -> Hidden
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (HiddenReason -> Var -> HiddenReason
forall a b. a -> b -> a
const (Var -> HiddenReason
NestedRec Var
v)) LCtx
ctxHid),
                  recDef :: LCtx
recDef = Ctx -> LCtx
recDef Ctx
c LCtx -> LCtx -> LCtx
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Var] -> LCtx
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
vs }
checkExpr' Ctx
c  (Var Var
v)
  | Type -> Bool
tcIsLiftedTypeKind (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v =  case Ctx -> Var -> Scope
getScope Ctx
c Var
v of
             Hidden SDoc
reason -> Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
c Var
v SDoc
reason
             Scope
Visible -> Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
  | Bool
otherwise = Maybe TypeError -> CoreM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing



addVars :: [Var] -> Ctx -> Ctx
addVars :: [Var] -> Ctx -> Ctx
addVars [Var]
v Ctx
c = Ctx
c{current :: LCtx
current = [Var] -> LCtx
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
v LCtx -> LCtx -> LCtx
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Ctx -> LCtx
current Ctx
c }