{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
module Cryptol.TypeCheck.Monad
( module Cryptol.TypeCheck.Monad
, module Cryptol.TypeCheck.InferTypes
) where
import qualified Control.Applicative as A
import qualified Control.Monad.Fail as Fail
import Control.Monad.Fix(MonadFix(..))
import Data.Text(Text)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Map (Map)
import Data.Set (Set)
import Data.List(find, foldl')
import Data.List.NonEmpty(NonEmpty((:|)))
import Data.Semigroup(sconcat)
import Data.Maybe(mapMaybe,fromMaybe)
import Data.IORef
import GHC.Generics (Generic)
import Control.DeepSeq
import MonadLib hiding (mapM)
import Cryptol.ModuleSystem.Name
(FreshM(..),Supply,mkLocal,asLocal
, nameInfo, NameInfo(..),NameSource(..), nameTopModule)
import qualified Cryptol.ModuleSystem.Interface as If
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Interface(genIfaceWithNames,genIfaceNames)
import Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)
, Path, rootPath)
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Error( Warning(..),Error(..)
, cleanupErrors, computeFreeVarNames
)
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import Cryptol.TypeCheck.PP(NameMap)
import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets,debugShowUniques)
import Cryptol.Utils.Ident(Ident,Namespace(..),ModName)
import Cryptol.Utils.Panic(panic)
data InferInput = InferInput
{ InferInput -> Range
inpRange :: Range
, InferInput -> Map Name Schema
inpVars :: Map Name Schema
, InferInput -> Map Name TySyn
inpTSyns :: Map Name TySyn
, InferInput -> Map Name Newtype
inpNewtypes :: Map Name Newtype
, InferInput -> Map Name AbstractType
inpAbstractTypes :: Map Name AbstractType
, InferInput -> Map Name ModParamNames
inpSignatures :: !(Map Name ModParamNames)
, InferInput -> ModName -> Maybe (ModuleG (), IfaceG ())
inpTopModules :: ModName -> Maybe (ModuleG (), If.IfaceG ())
, InferInput -> ModName -> Maybe ModParamNames
inpTopSignatures :: ModName -> Maybe ModParamNames
, InferInput -> ModParamNames
inpParams :: !ModParamNames
, InferInput -> NameSeeds
inpNameSeeds :: NameSeeds
, InferInput -> Bool
inpMonoBinds :: Bool
, InferInput -> Bool
inpCallStacks :: Bool
, InferInput -> [String]
inpSearchPath :: [FilePath]
, InferInput -> PrimMap
inpPrimNames :: !PrimMap
, InferInput -> Supply
inpSupply :: !Supply
, InferInput -> Solver
inpSolver :: SMT.Solver
}
data NameSeeds = NameSeeds
{ NameSeeds -> Int
seedTVar :: !Int
, NameSeeds -> Int
seedGoal :: !Int
} deriving (Int -> NameSeeds -> ShowS
[NameSeeds] -> ShowS
NameSeeds -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameSeeds] -> ShowS
$cshowList :: [NameSeeds] -> ShowS
show :: NameSeeds -> String
$cshow :: NameSeeds -> String
showsPrec :: Int -> NameSeeds -> ShowS
$cshowsPrec :: Int -> NameSeeds -> ShowS
Show, forall x. Rep NameSeeds x -> NameSeeds
forall x. NameSeeds -> Rep NameSeeds x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NameSeeds x -> NameSeeds
$cfrom :: forall x. NameSeeds -> Rep NameSeeds x
Generic, NameSeeds -> ()
forall a. (a -> ()) -> NFData a
rnf :: NameSeeds -> ()
$crnf :: NameSeeds -> ()
NFData)
nameSeeds :: NameSeeds
nameSeeds :: NameSeeds
nameSeeds = NameSeeds { seedTVar :: Int
seedTVar = Int
10, seedGoal :: Int
seedGoal = Int
0 }
data InferOutput a
= InferFailed NameMap [(Range,Warning)] [(Range,Error)]
| InferOK NameMap [(Range,Warning)] NameSeeds Supply a
deriving Int -> InferOutput a -> ShowS
forall a. Show a => Int -> InferOutput a -> ShowS
forall a. Show a => [InferOutput a] -> ShowS
forall a. Show a => InferOutput a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InferOutput a] -> ShowS
$cshowList :: forall a. Show a => [InferOutput a] -> ShowS
show :: InferOutput a -> String
$cshow :: forall a. Show a => InferOutput a -> String
showsPrec :: Int -> InferOutput a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> InferOutput a -> ShowS
Show
bumpCounter :: InferM ()
bumpCounter :: InferM ()
bumpCounter = do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
forall a. IO a -> InferM a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
iSolveCounter (forall a. Num a => a -> a -> a
+Int
1)
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM :: forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
info InferM a
m0 =
do let IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m = forall a. InferM a -> InferM a
selectorScope InferM a
m0
IORef Int
counter <- forall a. a -> IO (IORef a)
newIORef Int
0
let allPs :: ModParamNames
allPs = InferInput -> ModParamNames
inpParams InferInput
info
let env :: Map Name VarType
env = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Schema -> VarType
ExtVar (InferInput -> Map Name Schema
inpVars InferInput
info)
forall a. Semigroup a => a -> a -> a
<> forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ (Newtype -> Name
ntConName Newtype
nt, Schema -> VarType
ExtVar (Newtype -> Schema
newtypeConType Newtype
nt))
| Newtype
nt <- forall k a. Map k a -> [a]
Map.elems (InferInput -> Map Name Newtype
inpNewtypes InferInput
info)
]
forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Schema -> VarType
ExtVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModVParam -> Schema
mvpType) (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
allPs)
let ro :: RO
ro = RO { iRange :: Range
iRange = InferInput -> Range
inpRange InferInput
info
, iVars :: Map Name VarType
iVars = Map Name VarType
env
, iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iExtModules = InferInput -> ModName -> Maybe (ModuleG (), IfaceG ())
inpTopModules InferInput
info
, iExtSignatures :: ModName -> Maybe ModParamNames
iExtSignatures = InferInput -> ModName -> Maybe ModParamNames
inpTopSignatures InferInput
info
, iExtScope :: ModuleG ScopeName
iExtScope = (forall mname. mname -> ModuleG mname
emptyModule ScopeName
ExternalScope)
{ mTySyns :: Map Name TySyn
mTySyns = InferInput -> Map Name TySyn
inpTSyns InferInput
info forall a. Semigroup a => a -> a -> a
<>
ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
allPs
, mNewtypes :: Map Name Newtype
mNewtypes = InferInput -> Map Name Newtype
inpNewtypes InferInput
info
, mPrimTypes :: Map Name AbstractType
mPrimTypes = InferInput -> Map Name AbstractType
inpAbstractTypes InferInput
info
, mParamTypes :: Map Name ModTParam
mParamTypes = ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
allPs
, mParamFuns :: Map Name ModVParam
mParamFuns = ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
allPs
, mParamConstraints :: [Located Type]
mParamConstraints = ModParamNames -> [Located Type]
mpnConstraints ModParamNames
allPs
, mSignatures :: Map Name ModParamNames
mSignatures = InferInput -> Map Name ModParamNames
inpSignatures InferInput
info
}
, iTVars :: [TParam]
iTVars = []
, iSolvedHasLazy :: Map Int HasGoalSln
iSolvedHasLazy = forall k a. Map k a
Map.empty
, iMonoBinds :: Bool
iMonoBinds = InferInput -> Bool
inpMonoBinds InferInput
info
, iCallStacks :: Bool
iCallStacks = InferInput -> Bool
inpCallStacks InferInput
info
, iSolver :: Solver
iSolver = InferInput -> Solver
inpSolver InferInput
info
, iPrimNames :: PrimMap
iPrimNames = InferInput -> PrimMap
inpPrimNames InferInput
info
, iSolveCounter :: IORef Int
iSolveCounter = IORef Int
counter
}
Either [(Range, Error)] (a, RW)
mb <- forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
runExceptionT (forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT RW
rw (forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT RO
ro ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m))
case Either [(Range, Error)] (a, RW)
mb of
Left [(Range, Error)]
errs -> forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [] [(Range, Error)]
errs
Right (a
result, RW
finalRW) ->
do let theSu :: Subst
theSu = RW -> Subst
iSubst RW
finalRW
defSu :: Subst
defSu = Subst -> Subst
defaultingSubst Subst
theSu
warns :: [(Range, Warning)]
warns = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu)) (RW -> [(Range, Warning)]
iWarnings RW
finalRW)
case RW -> [(Range, Error)]
iErrors RW
finalRW of
[] ->
case RW -> Goals
iCts RW
finalRW of
Goals
cts
| Goals -> Bool
nullGoals Goals
cts -> forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> NameSeeds -> Supply -> a -> f (InferOutput a)
inferOk [(Range, Warning)]
warns
(RW -> NameSeeds
iNameSeeds RW
finalRW)
(RW -> Supply
iSupply RW
finalRW)
(forall t. TVars t => Subst -> t -> t
apSubst Subst
defSu a
result)
Goals
cts ->
forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [(Range, Warning)]
warns
[ ( Goal -> Range
goalRange Goal
g
, [Goal] -> Error
UnsolvedGoals [forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu Goal
g]
) | Goal
g <- Goals -> [Goal]
fromGoals Goals
cts
]
[(Range, Error)]
errs -> forall {f :: * -> *} {a}.
Applicative f =>
[(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [(Range, Warning)]
warns [(Range
r,forall t. TVars t => Subst -> t -> t
apSubst Subst
theSu Error
e) | (Range
r,Error
e) <- [(Range, Error)]
errs]
where
inferOk :: [(Range, Warning)] -> NameSeeds -> Supply -> a -> f (InferOutput a)
inferOk [(Range, Warning)]
ws NameSeeds
a Supply
b a
c = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a.
NameMap
-> [(Range, Warning)] -> NameSeeds -> Supply -> a -> InferOutput a
InferOK ([(Range, Warning)] -> [(Range, Error)] -> NameMap
computeFreeVarNames [(Range, Warning)]
ws []) [(Range, Warning)]
ws NameSeeds
a Supply
b a
c)
inferFailed :: [(Range, Warning)] -> [(Range, Error)] -> f (InferOutput a)
inferFailed [(Range, Warning)]
ws [(Range, Error)]
es =
let es1 :: [(Range, Error)]
es1 = [(Range, Error)] -> [(Range, Error)]
cleanupErrors [(Range, Error)]
es
in forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a.
NameMap -> [(Range, Warning)] -> [(Range, Error)] -> InferOutput a
InferFailed ([(Range, Warning)] -> [(Range, Error)] -> NameMap
computeFreeVarNames [(Range, Warning)]
ws [(Range, Error)]
es1) [(Range, Warning)]
ws [(Range, Error)]
es1)
rw :: RW
rw = RW { iErrors :: [(Range, Error)]
iErrors = []
, iWarnings :: [(Range, Warning)]
iWarnings = []
, iSubst :: Subst
iSubst = Subst
emptySubst
, iExistTVars :: [Map Name Type]
iExistTVars = []
, iNameSeeds :: NameSeeds
iNameSeeds = InferInput -> NameSeeds
inpNameSeeds InferInput
info
, iCts :: Goals
iCts = Goals
emptyGoals
, iHasCts :: [[HasGoal]]
iHasCts = []
, iSolvedHas :: Map Int HasGoalSln
iSolvedHas = forall k a. Map k a
Map.empty
, iSupply :: Supply
iSupply = InferInput -> Supply
inpSupply InferInput
info
, iScope :: [ModuleG ScopeName]
iScope = []
, iBindTypes :: Map Name Schema
iBindTypes = forall a. Monoid a => a
mempty
}
selectorScope :: InferM a -> InferM a
selectorScope :: forall a. InferM a -> InferM a
selectorScope (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m1) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
RW
rw <- forall (m :: * -> *) i. StateM m i => m i
get
Either [(Range, Error)] (a, RW)
mb <- forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
inBase
do rec let ro1 :: RO
ro1 = RO
ro { iSolvedHasLazy :: Map Int HasGoalSln
iSolvedHasLazy = Map Int HasGoalSln
solved }
rw1 :: RW
rw1 = RW
rw { iHasCts :: [[HasGoal]]
iHasCts = [] forall a. a -> [a] -> [a]
: RW -> [[HasGoal]]
iHasCts RW
rw }
Either [(Range, Error)] (a, RW)
mb <- forall i (m :: * -> *) a. ExceptionT i m a -> m (Either i a)
runExceptionT (forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT RW
rw1 (forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT RO
ro1 ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m1))
let solved :: Map Int HasGoalSln
solved = case Either [(Range, Error)] (a, RW)
mb of
Left {} -> forall k a. Map k a
Map.empty
Right (a
_,RW
rw2) -> RW -> Map Int HasGoalSln
iSolvedHas RW
rw2
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either [(Range, Error)] (a, RW)
mb
case Either [(Range, Error)] (a, RW)
mb of
Left [(Range, Error)]
err -> forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise [(Range, Error)]
err
Right (a
a,RW
rw1) ->
case RW -> [[HasGoal]]
iHasCts RW
rw1 of
[HasGoal]
us : [[HasGoal]]
cs ->
do let errs :: [(Range, Error)]
errs = [ (Goal -> Range
goalRange Goal
g, [Goal] -> Error
UnsolvedGoals [Goal
g])
| Goal
g <- forall a b. (a -> b) -> [a] -> [b]
map HasGoal -> Goal
hasGoal [HasGoal]
us ]
forall (m :: * -> *) i. StateM m i => i -> m ()
set RW
rw1 { iErrors :: [(Range, Error)]
iErrors = [(Range, Error)]
errs forall a. [a] -> [a] -> [a]
++ RW -> [(Range, Error)]
iErrors RW
rw1, iHasCts :: [[HasGoal]]
iHasCts = [[HasGoal]]
cs }
forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM (InferM ()
abortIfErrors)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
[] -> forall a. HasCallStack => String -> [String] -> a
panic String
"selectorScope" [String
"No selector scope"]
newtype InferM a = IM { forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM :: ReaderT RO
( StateT RW
( ExceptionT [(Range,Error)]
IO
)) a }
data ScopeName = ExternalScope
| LocalScope
| SubModule Name
| SignatureScope Name (Maybe Text)
| TopSignatureScope P.ModName
| MTopModule P.ModName
data RO = RO
{ RO -> Range
iRange :: Range
, RO -> Map Name VarType
iVars :: Map Name VarType
, RO -> [TParam]
iTVars :: [TParam]
, RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iExtModules :: ModName -> Maybe (ModuleG (), If.IfaceG ())
, RO -> ModName -> Maybe ModParamNames
iExtSignatures :: ModName -> Maybe ModParamNames
, RO -> ModuleG ScopeName
iExtScope :: ModuleG ScopeName
, RO -> Map Int HasGoalSln
iSolvedHasLazy :: Map Int HasGoalSln
, RO -> Bool
iMonoBinds :: Bool
, RO -> Bool
iCallStacks :: Bool
, RO -> Solver
iSolver :: SMT.Solver
, RO -> PrimMap
iPrimNames :: !PrimMap
, RO -> IORef Int
iSolveCounter :: !(IORef Int)
}
data RW = RW
{ RW -> [(Range, Error)]
iErrors :: ![(Range,Error)]
, RW -> [(Range, Warning)]
iWarnings :: ![(Range,Warning)]
, RW -> Subst
iSubst :: !Subst
, RW -> [Map Name Type]
iExistTVars :: [Map Name Type]
, RW -> Map Int HasGoalSln
iSolvedHas :: Map Int HasGoalSln
, RW -> NameSeeds
iNameSeeds :: !NameSeeds
, RW -> Goals
iCts :: !Goals
, RW -> [[HasGoal]]
iHasCts :: ![[HasGoal]]
, RW -> [ModuleG ScopeName]
iScope :: ![ModuleG ScopeName]
, RW -> Map Name Schema
iBindTypes :: !(Map Name Schema)
, RW -> Supply
iSupply :: !Supply
}
instance Functor InferM where
fmap :: forall a b. (a -> b) -> InferM a -> InferM b
fmap a -> b
f (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m)
instance A.Applicative InferM where
pure :: forall a. a -> InferM a
pure a
x = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
<*> :: forall a b. InferM (a -> b) -> InferM a -> InferM b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad InferM where
return :: forall a. a -> InferM a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m >>= :: forall a b. InferM a -> (a -> InferM b) -> InferM b
>>= a -> InferM b
f = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> InferM b
f)
instance Fail.MonadFail InferM where
fail :: forall a. String -> InferM a
fail String
x = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
x)
instance MonadFix InferM where
mfix :: forall a. (a -> InferM a) -> InferM a
mfix a -> InferM a
f = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (forall a.
InferM a
-> ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
unIM forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> InferM a
f))
instance FreshM InferM where
liftSupply :: forall a. (Supply -> (a, Supply)) -> InferM a
liftSupply Supply -> (a, Supply)
f = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$
do RW
rw <- forall (m :: * -> *) i. StateM m i => m i
get
let (a
a,Supply
s') = Supply -> (a, Supply)
f (RW -> Supply
iSupply RW
rw)
forall (m :: * -> *) i. StateM m i => i -> m ()
set RW
rw { iSupply :: Supply
iSupply = Supply
s' }
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
io :: IO a -> InferM a
io :: forall a. IO a -> InferM a
io IO a
m = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
inBase IO a
m
inRange :: Range -> InferM a -> InferM a
inRange :: forall a. Range -> InferM a -> InferM a
inRange Range
r (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m) = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
ro -> RO
ro { iRange :: Range
iRange = Range
r }) ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m
inRangeMb :: Maybe Range -> InferM a -> InferM a
inRangeMb :: forall a. Maybe Range -> InferM a -> InferM a
inRangeMb Maybe Range
Nothing InferM a
m = InferM a
m
inRangeMb (Just Range
r) InferM a
m = forall a. Range -> InferM a -> InferM a
inRange Range
r InferM a
m
curRange :: InferM Range
curRange :: InferM Range
curRange = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Range
iRange
recordError :: Error -> InferM ()
recordError :: Error -> InferM ()
recordError = Maybe Range -> Error -> InferM ()
recordErrorLoc forall a. Maybe a
Nothing
recordErrorLoc :: Maybe Range -> Error -> InferM ()
recordErrorLoc :: Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng Error
e =
do Range
r <- case Maybe Range
rng of
Just Range
r -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
Maybe Range
Nothing -> case Error
e of
AmbiguousSize TVarInfo
d Maybe Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
Error
_ -> InferM Range
curRange
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iErrors :: [(Range, Error)]
iErrors = (Range
r,Error
e) forall a. a -> [a] -> [a]
: RW -> [(Range, Error)]
iErrors RW
s }
abortIfErrors :: InferM ()
abortIfErrors :: InferM ()
abortIfErrors =
do RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
case RW -> [(Range, Error)]
iErrors RW
rw of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
[(Range, Error)]
es ->
do [(Range, Error)]
es1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Range, Error)]
es \(Range
l,Error
e) ->
do Error
e1 <- forall t. TVars t => t -> InferM t
applySubst Error
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range
l,Error
e1)
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise [(Range, Error)]
es1)
recordWarning :: Warning -> InferM ()
recordWarning :: Warning -> InferM ()
recordWarning Warning
w =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ignore forall a b. (a -> b) -> a -> b
$
do Range
r <- case Warning
w of
DefaultingTo TVarInfo
d Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (TVarInfo -> Range
tvarSource TVarInfo
d)
Warning
_ -> InferM Range
curRange
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iWarnings :: [(Range, Warning)]
iWarnings = (Range
r,Warning
w) forall a. a -> [a] -> [a]
: RW -> [(Range, Warning)]
iWarnings RW
s }
where
ignore :: Bool
ignore
| DefaultingTo TVarInfo
d Type
_ <- Warning
w
, Just Name
n <- TypeSource -> Maybe Name
tvSourceName (TVarInfo -> TypeSource
tvarDesc TVarInfo
d)
, GlobalName NameSource
SystemName OrigName
_ <- Name -> NameInfo
nameInfo Name
n
= Bool
True
| Bool
otherwise = Bool
False
getSolver :: InferM SMT.Solver
getSolver :: InferM Solver
getSolver =
do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
iSolver
getPrimMap :: InferM PrimMap
getPrimMap :: InferM PrimMap
getPrimMap =
do RO { Bool
[TParam]
Map Int HasGoalSln
Map Name VarType
IORef Int
Range
PrimMap
ModuleG ScopeName
Solver
ModName -> Maybe (ModuleG (), IfaceG ())
ModName -> Maybe ModParamNames
iSolveCounter :: IORef Int
iPrimNames :: PrimMap
iSolver :: Solver
iCallStacks :: Bool
iMonoBinds :: Bool
iSolvedHasLazy :: Map Int HasGoalSln
iExtScope :: ModuleG ScopeName
iExtSignatures :: ModName -> Maybe ModParamNames
iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: [TParam]
iVars :: Map Name VarType
iRange :: Range
iSolveCounter :: RO -> IORef Int
iPrimNames :: RO -> PrimMap
iSolver :: RO -> Solver
iCallStacks :: RO -> Bool
iMonoBinds :: RO -> Bool
iSolvedHasLazy :: RO -> Map Int HasGoalSln
iExtScope :: RO -> ModuleG ScopeName
iExtSignatures :: RO -> ModName -> Maybe ModParamNames
iExtModules :: RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iTVars :: RO -> [TParam]
iVars :: RO -> Map Name VarType
iRange :: RO -> Range
.. } <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) a. Monad m => a -> m a
return PrimMap
iPrimNames
newGoal :: ConstraintSource -> Prop -> InferM Goal
newGoal :: ConstraintSource -> Type -> InferM Goal
newGoal ConstraintSource
goalSource Type
goal =
do Range
goalRange <- InferM Range
curRange
forall (m :: * -> *) a. Monad m => a -> m a
return Goal { Range
Type
ConstraintSource
goal :: Type
goalSource :: ConstraintSource
goalRange :: Range
goal :: Type
goalSource :: ConstraintSource
goalRange :: Range
.. }
newGoals :: ConstraintSource -> [Prop] -> InferM ()
newGoals :: ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
src [Type]
ps = [Goal] -> InferM ()
addGoals forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ConstraintSource -> Type -> InferM Goal
newGoal ConstraintSource
src) [Type]
ps
getGoals :: InferM [Goal]
getGoals :: InferM [Goal]
getGoals =
do Goals
goals <- forall t. TVars t => t -> InferM t
applySubst forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets forall a b. (a -> b) -> a -> b
$ \RW
s -> (RW -> Goals
iCts RW
s, RW
s { iCts :: Goals
iCts = Goals
emptyGoals }))
forall (m :: * -> *) a. Monad m => a -> m a
return (Goals -> [Goal]
fromGoals Goals
goals)
addGoals :: [Goal] -> InferM ()
addGoals :: [Goal] -> InferM ()
addGoals [Goal]
gs0 = [Goal] -> InferM ()
doAdd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Goal] -> InferM [Goal]
simpGoals [Goal]
gs0
where
doAdd :: [Goal] -> InferM ()
doAdd [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
doAdd [Goal]
gs = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iCts :: Goals
iCts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip Goal -> Goals -> Goals
insertGoal) (RW -> Goals
iCts RW
s) [Goal]
gs }
collectGoals :: InferM a -> InferM (a, [Goal])
collectGoals :: forall a. InferM a -> InferM (a, [Goal])
collectGoals InferM a
m =
do Goals
origGs <- forall t. TVars t => t -> InferM t
applySubst forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InferM Goals
getGoals'
a
a <- InferM a
m
[Goal]
newGs <- InferM [Goal]
getGoals
Goals -> InferM ()
setGoals' Goals
origGs
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Goal]
newGs)
where
getGoals' :: InferM Goals
getGoals' = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets forall a b. (a -> b) -> a -> b
$ \ RW { [[HasGoal]]
[(Range, Error)]
[(Range, Warning)]
[Map Name Type]
[ModuleG ScopeName]
Map Int HasGoalSln
Map Name Schema
Supply
Subst
Goals
NameSeeds
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iCts :: Goals
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: RW -> Map Name Schema
iScope :: RW -> [ModuleG ScopeName]
iSolvedHas :: RW -> Map Int HasGoalSln
iHasCts :: RW -> [[HasGoal]]
iExistTVars :: RW -> [Map Name Type]
iSupply :: RW -> Supply
iNameSeeds :: RW -> NameSeeds
iCts :: RW -> Goals
iErrors :: RW -> [(Range, Error)]
iWarnings :: RW -> [(Range, Warning)]
iSubst :: RW -> Subst
.. } -> (Goals
iCts, RW { iCts :: Goals
iCts = Goals
emptyGoals, [[HasGoal]]
[(Range, Error)]
[(Range, Warning)]
[Map Name Type]
[ModuleG ScopeName]
Map Int HasGoalSln
Map Name Schema
Supply
Subst
NameSeeds
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iSolvedHas :: Map Int HasGoalSln
iHasCts :: [[HasGoal]]
iExistTVars :: [Map Name Type]
iSupply :: Supply
iNameSeeds :: NameSeeds
iErrors :: [(Range, Error)]
iWarnings :: [(Range, Warning)]
iSubst :: Subst
.. })
setGoals' :: Goals -> InferM ()
setGoals' Goals
gs = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets forall a b. (a -> b) -> a -> b
$ \ RW { [[HasGoal]]
[(Range, Error)]
[(Range, Warning)]
[Map Name Type]
[ModuleG ScopeName]
Map Int HasGoalSln
Map Name Schema
Supply
Subst
Goals
NameSeeds
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iCts :: Goals
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: RW -> Map Name Schema
iScope :: RW -> [ModuleG ScopeName]
iSolvedHas :: RW -> Map Int HasGoalSln
iHasCts :: RW -> [[HasGoal]]
iExistTVars :: RW -> [Map Name Type]
iSupply :: RW -> Supply
iNameSeeds :: RW -> NameSeeds
iCts :: RW -> Goals
iErrors :: RW -> [(Range, Error)]
iWarnings :: RW -> [(Range, Warning)]
iSubst :: RW -> Subst
.. } -> ((), RW { iCts :: Goals
iCts = Goals
gs, [[HasGoal]]
[(Range, Error)]
[(Range, Warning)]
[Map Name Type]
[ModuleG ScopeName]
Map Int HasGoalSln
Map Name Schema
Supply
Subst
NameSeeds
iSupply :: Supply
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iHasCts :: [[HasGoal]]
iNameSeeds :: NameSeeds
iSolvedHas :: Map Int HasGoalSln
iExistTVars :: [Map Name Type]
iSubst :: Subst
iWarnings :: [(Range, Warning)]
iErrors :: [(Range, Error)]
iBindTypes :: Map Name Schema
iScope :: [ModuleG ScopeName]
iSolvedHas :: Map Int HasGoalSln
iHasCts :: [[HasGoal]]
iExistTVars :: [Map Name Type]
iSupply :: Supply
iNameSeeds :: NameSeeds
iErrors :: [(Range, Error)]
iWarnings :: [(Range, Warning)]
iSubst :: Subst
.. })
simpGoal :: Goal -> InferM [Goal]
simpGoal :: Goal -> InferM [Goal]
simpGoal Goal
g =
case Ctxt -> Type -> Type
Simple.simplify forall a. Monoid a => a
mempty (Goal -> Type
goal Goal
g) of
Type
p | Just Type
t <- Type -> Maybe Type
tIsError Type
p ->
do Error -> InferM ()
recordError forall a b. (a -> b) -> a -> b
$ [Goal] -> Error
UnsolvableGoals [Goal
g { goal :: Type
goal = Type
t }]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| [Type]
ps <- Type -> [Type]
pSplitAnd Type
p -> forall (m :: * -> *) a. Monad m => a -> m a
return [ Goal
g { goal :: Type
goal = Type
pr } | Type
pr <- [Type]
ps ]
simpGoals :: [Goal] -> InferM [Goal]
simpGoals :: [Goal] -> InferM [Goal]
simpGoals [Goal]
gs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Goal -> InferM [Goal]
simpGoal [Goal]
gs
newHasGoal :: P.Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal Selector
l Type
ty Type
f =
do Int
goalName <- InferM Int
newGoalName
Goal
g <- ConstraintSource -> Type -> InferM Goal
newGoal ConstraintSource
CtSelector (Selector -> Type -> Type -> Type
pHas Selector
l Type
ty Type
f)
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
s -> case RW -> [[HasGoal]]
iHasCts RW
s of
[HasGoal]
cs : [[HasGoal]]
more ->
RW
s { iHasCts :: [[HasGoal]]
iHasCts = (Int -> Goal -> HasGoal
HasGoal Int
goalName Goal
g forall a. a -> [a] -> [a]
: [HasGoal]
cs) forall a. a -> [a] -> [a]
: [[HasGoal]]
more }
[] -> forall a. HasCallStack => String -> [String] -> a
panic String
"newHasGoal" [String
"no selector scope"]
Map Int HasGoalSln
solns <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RO -> Map Int HasGoalSln
iSolvedHasLazy forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
goalName Map Int HasGoalSln
solns of
Just HasGoalSln
e1 -> HasGoalSln
e1
Maybe HasGoalSln
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"newHasGoal" [String
"Unsolved has goal in result"]
addHasGoal :: HasGoal -> InferM ()
addHasGoal :: HasGoal -> InferM ()
addHasGoal HasGoal
g = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
s -> case RW -> [[HasGoal]]
iHasCts RW
s of
[HasGoal]
cs : [[HasGoal]]
more -> RW
s { iHasCts :: [[HasGoal]]
iHasCts = (HasGoal
g forall a. a -> [a] -> [a]
: [HasGoal]
cs) forall a. a -> [a] -> [a]
: [[HasGoal]]
more }
[] -> forall a. HasCallStack => String -> [String] -> a
panic String
"addHasGoal" [String
"No selector scope"]
getHasGoals :: InferM [HasGoal]
getHasGoals :: InferM [HasGoal]
getHasGoals =
do [HasGoal]
gs <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
s -> case RW -> [[HasGoal]]
iHasCts RW
s of
[HasGoal]
cs : [[HasGoal]]
more -> ([HasGoal]
cs, RW
s { iHasCts :: [[HasGoal]]
iHasCts = [] forall a. a -> [a] -> [a]
: [[HasGoal]]
more })
[] -> forall a. HasCallStack => String -> [String] -> a
panic String
"getHasGoals" [String
"No selector scope"]
forall t. TVars t => t -> InferM t
applySubst [HasGoal]
gs
solveHasGoal :: Int -> HasGoalSln -> InferM ()
solveHasGoal :: Int -> HasGoalSln -> InferM ()
solveHasGoal Int
n HasGoalSln
e =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iSolvedHas :: Map Int HasGoalSln
iSolvedHas = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
n HasGoalSln
e (RW -> Map Int HasGoalSln
iSolvedHas RW
s) }
newLocalName :: Namespace -> Ident -> InferM Name
newLocalName :: Namespace -> Ident -> InferM Name
newLocalName Namespace
ns Ident
x =
do Range
r <- InferM Range
curRange
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Namespace -> Ident -> Range -> Supply -> (Name, Supply)
mkLocal Namespace
ns Ident
x Range
r)
newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
newName :: forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName NameSeeds -> (a, NameSeeds)
upd = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets forall a b. (a -> b) -> a -> b
$ \RW
s -> let (a
x,NameSeeds
seeds) = NameSeeds -> (a, NameSeeds)
upd (RW -> NameSeeds
iNameSeeds RW
s)
in (a
x, RW
s { iNameSeeds :: NameSeeds
iNameSeeds = NameSeeds
seeds })
newGoalName :: InferM Int
newGoalName :: InferM Int
newGoalName = forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName forall a b. (a -> b) -> a -> b
$ \NameSeeds
s -> let x :: Int
x = NameSeeds -> Int
seedGoal NameSeeds
s
in (Int
x, NameSeeds
s { seedGoal :: Int
seedGoal = Int
x forall a. Num a => a -> a -> a
+ Int
1})
newTVar :: TypeSource -> Kind -> InferM TVar
newTVar :: TypeSource -> Kind -> InferM TVar
newTVar TypeSource
src Kind
k = TypeSource -> Set TParam -> Kind -> InferM TVar
newTVar' TypeSource
src forall a. Set a
Set.empty Kind
k
newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar
newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar
newTVar' TypeSource
src Set TParam
extraBound Kind
k =
do Range
r <- InferM Range
curRange
Set TParam
bound <- InferM (Set TParam)
getBoundInScope
let vs :: Set TParam
vs = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TParam
extraBound Set TParam
bound
msg :: TVarInfo
msg = TVarInfo { tvarDesc :: TypeSource
tvarDesc = TypeSource
src, tvarSource :: Range
tvarSource = Range
r }
forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName forall a b. (a -> b) -> a -> b
$ \NameSeeds
s -> let x :: Int
x = NameSeeds -> Int
seedTVar NameSeeds
s
in (Int -> Kind -> Set TParam -> TVarInfo -> TVar
TVFree Int
x Kind
k Set TParam
vs TVarInfo
msg, NameSeeds
s { seedTVar :: Int
seedTVar = Int
x forall a. Num a => a -> a -> a
+ Int
1 })
checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()
checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()
checkParamKind TParam
tp TPFlavor
flav Kind
k =
case TPFlavor
flav of
TPModParam Name
_ -> InferM ()
starOrHash
TPPropSynParam Name
_ -> InferM ()
starOrHashOrProp
TPTySynParam Name
_ -> InferM ()
starOrHash
TPSchemaParam Name
_ -> InferM ()
starOrHash
TPNewtypeParam Name
_ -> InferM ()
starOrHash
TPPrimParam Name
_ -> InferM ()
starOrHash
TPFlavor
TPUnifyVar -> InferM ()
starOrHash
where
starOrHashOrProp :: InferM ()
starOrHashOrProp =
case Kind
k of
Kind
KNum -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Kind
KType -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Kind
KProp -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Kind
_ -> Error -> InferM ()
recordError (TParam -> Kind -> Error
BadParameterKind TParam
tp Kind
k)
starOrHash :: InferM ()
starOrHash =
case Kind
k of
Kind
KNum -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Kind
KType -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Kind
_ -> Error -> InferM ()
recordError (TParam -> Kind -> Error
BadParameterKind TParam
tp Kind
k)
newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
newTParam TParam Name
nm TPFlavor
flav Kind
k =
do let desc :: TVarInfo
desc = TVarInfo { tvarDesc :: TypeSource
tvarDesc = Name -> TypeSource
TVFromSignature (forall n. TParam n -> n
P.tpName TParam Name
nm)
, tvarSource :: Range
tvarSource = forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (forall n. TParam n -> Maybe Range
P.tpRange TParam Name
nm)
}
TParam
tp <- forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName forall a b. (a -> b) -> a -> b
$ \NameSeeds
s ->
let x :: Int
x = NameSeeds -> Int
seedTVar NameSeeds
s
in (TParam { tpUnique :: Int
tpUnique = Int
x
, tpKind :: Kind
tpKind = Kind
k
, tpFlav :: TPFlavor
tpFlav = TPFlavor
flav
, tpInfo :: TVarInfo
tpInfo = TVarInfo
desc
}
, NameSeeds
s { seedTVar :: Int
seedTVar = Int
x forall a. Num a => a -> a -> a
+ Int
1 })
TParam -> TPFlavor -> Kind -> InferM ()
checkParamKind TParam
tp TPFlavor
flav Kind
k
forall (m :: * -> *) a. Monad m => a -> m a
return TParam
tp
freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
freshTParam Name -> TPFlavor
mkF TParam
tp = forall a. (NameSeeds -> (a, NameSeeds)) -> InferM a
newName \NameSeeds
s ->
let u :: Int
u = NameSeeds -> Int
seedTVar NameSeeds
s
in ( TParam
tp { tpUnique :: Int
tpUnique = Int
u
, tpFlav :: TPFlavor
tpFlav = case TParam -> Maybe Name
tpName TParam
tp of
Just Name
n -> Name -> TPFlavor
mkF (Namespace -> Name -> Name
asLocal Namespace
NSType Name
n)
Maybe Name
Nothing -> TParam -> TPFlavor
tpFlav TParam
tp
}
, NameSeeds
s { seedTVar :: Int
seedTVar = Int
u forall a. Num a => a -> a -> a
+ Int
1 }
)
newType :: TypeSource -> Kind -> InferM Type
newType :: TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
k = TVar -> Type
TVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` TypeSource -> Kind -> InferM TVar
newTVar TypeSource
src Kind
k
unify :: TypeWithSource -> Type -> InferM [Prop]
unify :: TypeWithSource -> Type -> InferM [Type]
unify (WithSource Type
t1 TypeSource
src Maybe Range
rng) Type
t2 =
do Type
t1' <- forall t. TVars t => t -> InferM t
applySubst Type
t1
Type
t2' <- forall t. TVars t => t -> InferM t
applySubst Type
t2
let ((Subst
su1, [Type]
ps), [(Path, UnificationError)]
errs) = forall a. Result a -> (a, [(Path, UnificationError)])
runResult (Type -> Type -> Result MGU
doMGU Type
t1' Type
t2')
Subst -> InferM ()
extendSubst Subst
su1
let toError :: (Path,UnificationError) -> Error
toError :: (Path, UnificationError) -> Error
toError (Path
pa,UnificationError
err) =
case UnificationError
err of
UniTypeLenMismatch Int
_ Int
_ -> TypeSource -> Path -> Type -> Type -> Error
TypeMismatch TypeSource
src Path
rootPath Type
t1' Type
t2'
UniTypeMismatch Type
s1 Type
s2 -> TypeSource -> Path -> Type -> Type -> Error
TypeMismatch TypeSource
src Path
pa Type
s1 Type
s2
UniKindMismatch Kind
k1 Kind
k2 -> Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (forall a. a -> Maybe a
Just TypeSource
src) Kind
k1 Kind
k2
UniRecursive TVar
x Type
t -> TypeSource -> Path -> Type -> Type -> Error
RecursiveType TypeSource
src Path
pa (TVar -> Type
TVar TVar
x) Type
t
UniNonPolyDepends TVar
x [TParam]
vs -> TypeSource -> Path -> Type -> [TParam] -> Error
TypeVariableEscaped TypeSource
src Path
pa (TVar -> Type
TVar TVar
x) [TParam]
vs
UniNonPoly TVar
x Type
t -> TypeSource -> Path -> TVar -> Type -> Error
NotForAll TypeSource
src Path
pa TVar
x Type
t
case [(Path, UnificationError)]
errs of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ps
[(Path, UnificationError)]
_ -> do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Path, UnificationError) -> Error
toError) [(Path, UnificationError)]
errs
forall (m :: * -> *) a. Monad m => a -> m a
return []
applySubst :: TVars t => t -> InferM t
applySubst :: forall t. TVars t => t -> InferM t
applySubst t
t =
do Subst
su <- InferM Subst
getSubst
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. TVars t => Subst -> t -> t
apSubst Subst
su t
t)
applySubstPreds :: [Prop] -> InferM [Prop]
applySubstPreds :: [Type] -> InferM [Type]
applySubstPreds [Type]
ps =
do [Type]
ps1 <- forall t. TVars t => t -> InferM t
applySubst [Type]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
ps1)
applySubstGoals :: [Goal] -> InferM [Goal]
applySubstGoals :: [Goal] -> InferM [Goal]
applySubstGoals [Goal]
gs =
do [Goal]
gs1 <- forall t. TVars t => t -> InferM t
applySubst [Goal]
gs
forall (m :: * -> *) a. Monad m => a -> m a
return [ Goal
g { goal :: Type
goal = Type
p } | Goal
g <- [Goal]
gs1, Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g) ]
getSubst :: InferM Subst
getSubst :: InferM Subst
getSubst = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> Subst
iSubst forall (m :: * -> *) i. StateM m i => m i
get
extendSubst :: Subst -> InferM ()
extendSubst :: Subst -> InferM ()
extendSubst Subst
su =
do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TVar, Type) -> InferM ()
check (Subst -> [(TVar, Type)]
substToList Subst
su)
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iSubst :: Subst
iSubst = Subst
su Subst -> Subst -> Subst
@@ RW -> Subst
iSubst RW
s }
where
check :: (TVar, Type) -> InferM ()
check :: (TVar, Type) -> InferM ()
check (TVar
v, Type
ty) =
case TVar
v of
TVBound TParam
_ ->
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Monad.extendSubst"
[ String
"Substitution instantiates bound variable:"
, String
"Variable: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp TVar
v)
, String
"Type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Type
ty)
]
TVFree Int
_ Kind
_ Set TParam
tvs TVarInfo
_ ->
do let escaped :: Set TParam
escaped = forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall t. FVS t => t -> Set TParam
freeParams Type
ty) Set TParam
tvs
if forall a. Set a -> Bool
Set.null Set TParam
escaped then forall (m :: * -> *) a. Monad m => a -> m a
return () else
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Monad.extendSubst"
[ String
"Escaped quantified variables:"
, String
"Substitution: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp TVar
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":=" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Type
ty)
, String
"Vars in scope: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Doc -> Doc
brackets ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (forall a. Set a -> [a]
Set.toList Set TParam
tvs))))
, String
"Escaped: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Doc -> Doc
brackets ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (forall a. Set a -> [a]
Set.toList Set TParam
escaped))))
]
varsWithAsmps :: InferM (Set TVar)
varsWithAsmps :: InferM (Set TVar)
varsWithAsmps =
do [VarType]
env <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k a. Map k a -> [a]
Map.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> Map Name VarType
iVars) forall (m :: * -> *) i. ReaderM m i => m i
ask
[Set TVar]
fromEnv <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VarType]
env forall a b. (a -> b) -> a -> b
$ \VarType
v ->
case VarType
v of
ExtVar Schema
sch -> forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars Schema
sch
CurSCC Expr
_ Type
t -> forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars Type
t
[[HasGoal]]
hasCts <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (RW -> [[HasGoal]]
iHasCts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) i. StateM m i => m i
get)
let sels :: [Type]
sels = forall a b. (a -> b) -> [a] -> [b]
map (Goal -> Type
goal forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasGoal -> Goal
hasGoal) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HasGoal]]
hasCts)
[Set TVar]
fromSels <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars [Type]
sels
Set TVar
fromEx <- (forall {a}. (FVS a, TVars a) => a -> InferM (Set TVar)
getVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall k a. Map k a -> [a]
Map.elems) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> [Map Name Type]
iExistTVars forall (m :: * -> *) i. StateM m i => m i
get)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set TVar]
fromEnv forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set TVar]
fromSels
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TVar
fromEx)
where
getVars :: a -> InferM (Set TVar)
getVars a
x = forall t. FVS t => t -> Set TVar
fvs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall t. TVars t => t -> InferM t
applySubst a
x
lookupVar :: Name -> InferM VarType
lookupVar :: Name -> InferM VarType
lookupVar Name
x =
do Maybe VarType
mb <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> Map Name VarType
iVars
case Maybe VarType
mb of
Just VarType
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VarType
a
Maybe VarType
Nothing ->
do Maybe Schema
mb1 <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> Map Name Schema
iBindTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
case Maybe Schema
mb1 of
Just Schema
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Schema -> VarType
ExtVar Schema
a)
Maybe Schema
Nothing ->
do Map Name VarType
mp <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Map Name VarType
iVars
forall a. HasCallStack => String -> [String] -> a
panic String
"lookupVar" forall a b. (a -> b) -> a -> b
$ [ String
"Undefined vairable"
, forall a. Show a => a -> String
show Name
x
, String
"IVARS"
] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
debugShowUniques forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
pp) (forall k a. Map k a -> [k]
Map.keys Map Name VarType
mp)
lookupTParam :: Name -> InferM (Maybe TParam)
lookupTParam :: Name -> InferM (Maybe TParam)
lookupTParam Name
x = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find TParam -> Bool
this forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> [TParam]
iTVars
where this :: TParam -> Bool
this TParam
tp = TParam -> Maybe Name
tpName TParam
tp forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Name
x
lookupTSyn :: Name -> InferM (Maybe TySyn)
lookupTSyn :: Name -> InferM (Maybe TySyn)
lookupTSyn Name
x = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name TySyn)
getTSyns
lookupNewtype :: Name -> InferM (Maybe Newtype)
lookupNewtype :: Name -> InferM (Maybe Newtype)
lookupNewtype Name
x = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name Newtype)
getNewtypes
lookupAbstractType :: Name -> InferM (Maybe AbstractType)
lookupAbstractType :: Name -> InferM (Maybe AbstractType)
lookupAbstractType Name
x = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name AbstractType)
getAbstractTypes
lookupParamType :: Name -> InferM (Maybe ModTParam)
lookupParamType :: Name -> InferM (Maybe ModTParam)
lookupParamType Name
x = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
lookupSignature :: P.ImpName Name -> InferM ModParamNames
lookupSignature :: ImpName Name -> InferM ModParamNames
lookupSignature ImpName Name
nx =
case ImpName Name
nx of
P.ImpNested Name
x ->
do Map Name ModParamNames
sigs <- InferM (Map Name ModParamNames)
getSignatures
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name ModParamNames
sigs of
Just ModParamNames
ips -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModParamNames
ips
Maybe ModParamNames
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupSignature"
[ String
"Missing signature", forall a. Show a => a -> String
show Name
x ]
P.ImpTop ModName
t ->
do ModName -> Maybe ModParamNames
loaded <- RO -> ModName -> Maybe ModParamNames
iExtSignatures forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
case ModName -> Maybe ModParamNames
loaded ModName
t of
Just ModParamNames
ps -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModParamNames
ps
Maybe ModParamNames
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupSignature"
[ String
"Top level signature is not loaded", forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp ImpName Name
nx) ]
lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), If.IfaceG ()))
lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
lookupTopModule ModName
m =
do ModName -> Maybe (ModuleG (), IfaceG ())
ms <- RO -> ModName -> Maybe (ModuleG (), IfaceG ())
iExtModules forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModName -> Maybe (ModuleG (), IfaceG ())
ms ModName
m)
lookupFunctor :: P.ImpName Name -> InferM (ModuleG ())
lookupFunctor :: ImpName Name -> InferM (ModuleG ())
lookupFunctor ImpName Name
iname =
case ImpName Name
iname of
P.ImpTop ModName
m -> forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Maybe a -> a
fromMb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
lookupTopModule ModName
m
P.ImpNested Name
m ->
do Map Name (ModuleG Name)
localFuns <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m Map Name (ModuleG Name)
localFuns of
Just ModuleG Name
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG Name
a { mName :: ()
mName = () }
Maybe (ModuleG Name)
Nothing ->
do Maybe (ModuleG (), IfaceG ())
mbTop <- ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
lookupTopModule (Name -> ModName
nameTopModule Name
m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {a}. Maybe a -> a
fromMb do ModuleG ()
a <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ModuleG (), IfaceG ())
mbTop
ModuleG Name
b <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ()
a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG Name
b { mName :: ()
mName = () })
where
fromMb :: Maybe a -> a
fromMb Maybe a
mb = case Maybe a
mb of
Just a
a -> a
a
Maybe a
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupFunctor"
[ String
"Missing functor", forall a. Show a => a -> String
show ImpName Name
iname ]
lookupModule :: P.ImpName Name -> InferM (If.IfaceG ())
lookupModule :: ImpName Name -> InferM (IfaceG ())
lookupModule ImpName Name
iname =
case ImpName Name
iname of
P.ImpTop ModName
m -> forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Maybe a -> a
fromMb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
lookupTopModule ModName
m
P.ImpNested Name
m ->
do Map Name (IfaceNames Name)
localMods <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m Map Name (IfaceNames Name)
localMods of
Just IfaceNames Name
names ->
do IfaceG Name
n <- forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames IfaceNames Name
names forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (ModuleG ())
getCurDecls
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall name. IfaceG name -> IfaceG ()
If.ifaceForgetName IfaceG Name
n)
Maybe (IfaceNames Name)
Nothing ->
do Maybe (ModuleG (), IfaceG ())
mb <- ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
lookupTopModule (Name -> ModName
nameTopModule Name
m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {a}. Maybe a -> a
fromMb
do IfaceG ()
iface <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ModuleG (), IfaceG ())
mb
IfaceNames Name
names <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
m
(IfaceDecls -> Map Name (IfaceNames Name)
If.ifModules (forall name. IfaceG name -> IfaceDecls
If.ifDefines IfaceG ()
iface))
forall (f :: * -> *) a. Applicative f => a -> f a
pure IfaceG ()
iface
{ ifNames :: IfaceNames ()
If.ifNames = IfaceNames Name
names { ifsName :: ()
If.ifsName = () } })
where
fromMb :: Maybe a -> a
fromMb Maybe a
mb = case Maybe a
mb of
Just a
a -> a
a
Maybe a
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupModule"
[ String
"Missing module", forall a. Show a => a -> String
show ImpName Name
iname ]
lookupModParam :: P.Ident -> InferM (Maybe ModParam)
lookupModParam :: Ident -> InferM (Maybe ModParam)
lookupModParam Ident
p =
do FunctorParams
scope <- forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> FunctorParams
mParams
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
p FunctorParams
scope)
existVar :: Name -> Kind -> InferM Type
existVar :: Name -> Kind -> InferM Type
existVar Name
x Kind
k =
do [Map Name Type]
scopes <- RW -> [Map Name Type]
iExistTVars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
case forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x) [Map Name Type]
scopes) of
Just Type
ty -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
Maybe Type
Nothing ->
case [Map Name Type]
scopes of
[] ->
do Error -> InferM ()
recordError (Name -> Error
UndefinedExistVar Name
x)
TypeSource -> Kind -> InferM Type
newType TypeSource
TypeErrorPlaceHolder Kind
k
Map Name Type
sc : [Map Name Type]
more ->
do Type
ty <- TypeSource -> Kind -> InferM Type
newType TypeSource
TypeErrorPlaceHolder Kind
k
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s{ iExistTVars :: [Map Name Type]
iExistTVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type
ty Map Name Type
sc forall a. a -> [a] -> [a]
: [Map Name Type]
more }
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
getTSyns :: InferM (Map Name TySyn)
getTSyns :: InferM (Map Name TySyn)
getTSyns = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name TySyn
mTySyns
getNewtypes :: InferM (Map Name Newtype)
getNewtypes :: InferM (Map Name Newtype)
getNewtypes = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
getAbstractTypes :: InferM (Map Name AbstractType)
getAbstractTypes :: InferM (Map Name AbstractType)
getAbstractTypes = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes
getParamTypes :: InferM (Map Name ModTParam)
getParamTypes :: InferM (Map Name ModTParam)
getParamTypes = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes
getParamConstraints :: InferM [Located Prop]
getParamConstraints :: InferM [Located Type]
getParamConstraints = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> [Located Type]
mParamConstraints
getTVars :: InferM (Set Name)
getTVars :: InferM (Set Name)
getTVars = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName forall b c a. (b -> c) -> (a -> b) -> a -> c
. RO -> [TParam]
iTVars
getBoundInScope :: InferM (Set TParam)
getBoundInScope :: InferM (Set TParam)
getBoundInScope =
do RO
ro <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
Set TParam
params <- forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
let bound :: Set TParam
bound = forall a. Ord a => [a] -> Set a
Set.fromList (RO -> [TParam]
iTVars RO
ro)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TParam
params Set TParam
bound
getMonoBinds :: InferM Bool
getMonoBinds :: InferM Bool
getMonoBinds = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Bool
iMonoBinds)
getCallStacks :: InferM Bool
getCallStacks :: InferM Bool
getCallStacks = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM (forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks RO -> Bool
iCallStacks)
getSignatures :: InferM (Map Name ModParamNames)
getSignatures :: InferM (Map Name ModParamNames)
getSignatures = forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures
checkTShadowing :: String -> Name -> InferM ()
checkTShadowing :: String -> Name -> InferM ()
checkTShadowing String
this Name
new =
do Map Name TySyn
tsyns <- InferM (Map Name TySyn)
getTSyns
RO
ro <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
let shadowed :: Maybe String
shadowed =
do TySyn
_ <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
new Map Name TySyn
tsyns
forall (m :: * -> *) a. Monad m => a -> m a
return String
"type synonym"
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
do forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Name
new forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName (RO -> [TParam]
iTVars RO
ro))
forall (m :: * -> *) a. Monad m => a -> m a
return String
"type variable"
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
do Type
_ <- forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
new) (RW -> [Map Name Type]
iExistTVars RW
rw))
forall (m :: * -> *) a. Monad m => a -> m a
return String
"type"
case Maybe String
shadowed of
Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just String
that ->
Error -> InferM ()
recordError (String -> Name -> String -> Error
TypeShadowing String
this Name
new String
that)
withTParam :: TParam -> InferM a -> InferM a
withTParam :: forall a. TParam -> InferM a -> InferM a
withTParam TParam
p (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m) =
do case TParam -> Maybe Name
tpName TParam
p of
Just Name
x -> String -> Name -> InferM ()
checkTShadowing String
"variable" Name
x
Maybe Name
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
r -> RO
r { iTVars :: [TParam]
iTVars = TParam
p forall a. a -> [a] -> [a]
: RO -> [TParam]
iTVars RO
r }) ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m
withTParams :: [TParam] -> InferM a -> InferM a
withTParams :: forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
ps InferM a
m = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. TParam -> InferM a -> InferM a
withTParam InferM a
m [TParam]
ps
newScope :: ScopeName -> InferM ()
newScope :: ScopeName -> InferM ()
newScope ScopeName
nm = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = forall mname. mname -> ModuleG mname
emptyModule ScopeName
nm forall a. a -> [a] -> [a]
: RW -> [ModuleG ScopeName]
iScope RW
rw }
newLocalScope :: InferM ()
newLocalScope :: InferM ()
newLocalScope = ScopeName -> InferM ()
newScope ScopeName
LocalScope
newSignatureScope :: Name -> Maybe Text -> InferM ()
newSignatureScope :: Name -> Maybe Text -> InferM ()
newSignatureScope Name
x Maybe Text
doc =
do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
o -> ModuleG ScopeName
o { mNested :: Set Name
mNested = forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x (forall mname. ModuleG mname -> Set Name
mNested ModuleG ScopeName
o) }
ScopeName -> InferM ()
newScope (Name -> Maybe Text -> ScopeName
SignatureScope Name
x Maybe Text
doc)
newTopSignatureScope :: ModName -> InferM ()
newTopSignatureScope :: ModName -> InferM ()
newTopSignatureScope ModName
x = ScopeName -> InferM ()
newScope (ModName -> ScopeName
TopSignatureScope ModName
x)
newSubmoduleScope ::
Name -> Maybe Text -> ExportSpec Name -> InferM ()
newSubmoduleScope :: Name -> Maybe Text -> ExportSpec Name -> InferM ()
newSubmoduleScope Name
x Maybe Text
docs ExportSpec Name
e =
do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
o -> ModuleG ScopeName
o { mNested :: Set Name
mNested = forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x (forall mname. ModuleG mname -> Set Name
mNested ModuleG ScopeName
o) }
ScopeName -> InferM ()
newScope (Name -> ScopeName
SubModule Name
x)
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mDoc :: Maybe Text
mDoc = Maybe Text
docs, mExports :: ExportSpec Name
mExports = ExportSpec Name
e }
newModuleScope :: P.ModName -> ExportSpec Name -> InferM ()
newModuleScope :: ModName -> ExportSpec Name -> InferM ()
newModuleScope ModName
x ExportSpec Name
e =
do ScopeName -> InferM ()
newScope (ModName -> ScopeName
MTopModule ModName
x)
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
m -> ModuleG ScopeName
m { mDoc :: Maybe Text
mDoc = forall a. Maybe a
Nothing, mExports :: ExportSpec Name
mExports = ExportSpec Name
e }
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope ModuleG ScopeName -> ModuleG ScopeName
f = forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = [ModuleG ScopeName] -> [ModuleG ScopeName]
upd (RW -> [ModuleG ScopeName]
iScope RW
rw) }
where
upd :: [ModuleG ScopeName] -> [ModuleG ScopeName]
upd [ModuleG ScopeName]
r =
case [ModuleG ScopeName]
r of
[] -> forall a. HasCallStack => String -> [String] -> a
panic String
"updTopScope" [ String
"No top scope" ]
ModuleG ScopeName
s : [ModuleG ScopeName]
more -> ModuleG ScopeName -> ModuleG ScopeName
f ModuleG ScopeName
s forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more
endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
endLocalScope =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
rw ->
case RW -> [ModuleG ScopeName]
iScope RW
rw of
ModuleG ScopeName
x : [ModuleG ScopeName]
xs | ScopeName
LocalScope <- forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
( (forall a. [a] -> [a]
reverse (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x), forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x), RW
rw { iScope :: [ModuleG ScopeName]
iScope = [ModuleG ScopeName]
xs })
[ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endLocalScope" [String
"Missing local scope"]
endSubmodule :: InferM ()
endSubmodule :: InferM ()
endSubmodule =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw ->
case RW -> [ModuleG ScopeName]
iScope RW
rw of
x :: ModuleG ScopeName
x@Module { mName :: forall mname. ModuleG mname -> mname
mName = SubModule Name
m } : ModuleG ScopeName
y : [ModuleG ScopeName]
more -> RW
rw { iScope :: [ModuleG ScopeName]
iScope = ModuleG ScopeName
z forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more }
where
x1 :: ModuleG Name
x1 = ModuleG ScopeName
x { mName :: Name
mName = Name
m, mDecls :: [DeclGroup]
mDecls = forall a. [a] -> [a]
reverse (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x) }
isFun :: Bool
isFun = forall mname. ModuleG mname -> Bool
isParametrizedModule ModuleG Name
x1
add :: Monoid a => (ModuleG ScopeName -> a) -> a
add :: forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add ModuleG ScopeName -> a
f = if Bool
isFun then ModuleG ScopeName -> a
f ModuleG ScopeName
y else ModuleG ScopeName -> a
f ModuleG ScopeName
x forall a. Semigroup a => a -> a -> a
<> ModuleG ScopeName -> a
f ModuleG ScopeName
y
z :: ModuleG ScopeName
z = Module
{ mName :: ScopeName
mName = forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
y
, mDoc :: Maybe Text
mDoc = forall mname. ModuleG mname -> Maybe Text
mDoc ModuleG ScopeName
y
, mExports :: ExportSpec Name
mExports = forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG ScopeName
y
, mParamTypes :: Map Name ModTParam
mParamTypes = forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
y
, mParamFuns :: Map Name ModVParam
mParamFuns = forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
y
, mParamConstraints :: [Located Type]
mParamConstraints = forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
y
, mParams :: FunctorParams
mParams = forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ScopeName
y
, mNested :: Set Name
mNested = forall mname. ModuleG mname -> Set Name
mNested ModuleG ScopeName
y
, mTySyns :: Map Name TySyn
mTySyns = forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add forall mname. ModuleG mname -> Map Name TySyn
mTySyns
, mNewtypes :: Map Name Newtype
mNewtypes = forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
, mPrimTypes :: Map Name AbstractType
mPrimTypes = forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes
, mDecls :: [DeclGroup]
mDecls = forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add forall mname. ModuleG mname -> [DeclGroup]
mDecls
, mSignatures :: Map Name ModParamNames
mSignatures = forall a. Monoid a => (ModuleG ScopeName -> a) -> a
add forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures
, mSubmodules :: Map Name (IfaceNames Name)
mSubmodules = if Bool
isFun
then forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ScopeName
y
else forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m (forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG Name
x1)
(forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ScopeName
x forall a. Semigroup a => a -> a -> a
<> forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ScopeName
y)
, mFunctors :: Map Name (ModuleG Name)
mFunctors = if Bool
isFun
then forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m ModuleG Name
x1 (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
y)
else forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
x forall a. Semigroup a => a -> a -> a
<> forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
y
}
[ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endSubmodule" [ String
"Not a submodule" ]
endModule :: InferM TCTopEntity
endModule :: InferM TCTopEntity
endModule =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
rw ->
case RW -> [ModuleG ScopeName]
iScope RW
rw of
[ ModuleG ScopeName
x ] | MTopModule ModName
m <- forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
( ModuleG ModName -> TCTopEntity
TCTopModule ModuleG ScopeName
x { mName :: ModName
mName = ModName
m, mDecls :: [DeclGroup]
mDecls = forall a. [a] -> [a]
reverse (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
x) }
, RW
rw { iScope :: [ModuleG ScopeName]
iScope = [] }
)
[ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endModule" [ String
"Not a single top module" ]
endSignature :: InferM ()
endSignature :: InferM ()
endSignature =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw ->
case RW -> [ModuleG ScopeName]
iScope RW
rw of
x :: ModuleG ScopeName
x@Module { mName :: forall mname. ModuleG mname -> mname
mName = SignatureScope Name
m Maybe Text
doc } : ModuleG ScopeName
y : [ModuleG ScopeName]
more ->
RW
rw { iScope :: [ModuleG ScopeName]
iScope = ModuleG ScopeName
z forall a. a -> [a] -> [a]
: [ModuleG ScopeName]
more }
where
z :: ModuleG ScopeName
z = ModuleG ScopeName
y { mSignatures :: Map Name ModParamNames
mSignatures = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
m ModParamNames
sig (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ScopeName
y) }
sig :: ModParamNames
sig = ModParamNames
{ mpnTypes :: Map Name ModTParam
mpnTypes = forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
x
, mpnConstraints :: [Located Type]
mpnConstraints = forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
x
, mpnFuns :: Map Name ModVParam
mpnFuns = forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
x
, mpnTySyn :: Map Name TySyn
mpnTySyn = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x
, mpnDoc :: Maybe Text
mpnDoc = Maybe Text
doc
}
[ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endSignature" [ String
"Not a signature scope" ]
endTopSignature :: InferM TCTopEntity
endTopSignature :: InferM TCTopEntity
endTopSignature =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. StateM m s => (s -> (a, s)) -> m a
sets \RW
rw ->
case RW -> [ModuleG ScopeName]
iScope RW
rw of
[ ModuleG ScopeName
x ] | TopSignatureScope ModName
m <- forall mname. ModuleG mname -> mname
mName ModuleG ScopeName
x ->
( ModName -> ModParamNames -> TCTopEntity
TCTopSignature ModName
m ModParamNames
{ mpnTypes :: Map Name ModTParam
mpnTypes = forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
x
, mpnConstraints :: [Located Type]
mpnConstraints = forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
x
, mpnFuns :: Map Name ModVParam
mpnFuns = forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
x
, mpnTySyn :: Map Name TySyn
mpnTySyn = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
x
, mpnDoc :: Maybe Text
mpnDoc = forall a. Maybe a
Nothing
}
, RW
rw { iScope :: [ModuleG ScopeName]
iScope = [] }
)
[ModuleG ScopeName]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"endTopSignature" [ String
"Not a top-level signature" ]
getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope :: forall a. Semigroup a => (ModuleG ScopeName -> a) -> InferM a
getScope ModuleG ScopeName -> a
f =
do RO
ro <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Semigroup a => NonEmpty a -> a
sconcat (ModuleG ScopeName -> a
f (RO -> ModuleG ScopeName
iExtScope RO
ro) forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
map ModuleG ScopeName -> a
f (RW -> [ModuleG ScopeName]
iScope RW
rw)))
getCurDecls :: InferM (ModuleG ())
getCurDecls :: InferM (ModuleG ())
getCurDecls =
do RO
ro <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. ReaderM m i => m i
ask
RW
rw <- forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ModuleG ScopeName
m1 ModuleG ()
m2 -> forall {mname}. ModuleG mname -> ModuleG mname -> ModuleG ()
mergeDecls (forall {mname}. ModuleG mname -> ModuleG ()
forget ModuleG ScopeName
m1) ModuleG ()
m2)
(forall {mname}. ModuleG mname -> ModuleG ()
forget (RO -> ModuleG ScopeName
iExtScope RO
ro)) (RW -> [ModuleG ScopeName]
iScope RW
rw))
where
forget :: ModuleG mname -> ModuleG ()
forget ModuleG mname
m = ModuleG mname
m { mName :: ()
mName = () }
mergeDecls :: ModuleG mname -> ModuleG mname -> ModuleG ()
mergeDecls ModuleG mname
m1 ModuleG mname
m2 =
Module
{ mName :: ()
mName = ()
, mDoc :: Maybe Text
mDoc = forall a. Maybe a
Nothing
, mExports :: ExportSpec Name
mExports = forall a. Monoid a => a
mempty
, mParams :: FunctorParams
mParams = forall a. Monoid a => a
mempty
, mParamTypes :: Map Name ModTParam
mParamTypes = forall a. Monoid a => a
mempty
, mParamConstraints :: [Located Type]
mParamConstraints = forall a. Monoid a => a
mempty
, mParamFuns :: Map Name ModVParam
mParamFuns = forall a. Monoid a => a
mempty
, mNested :: Set Name
mNested = forall a. Monoid a => a
mempty
, mTySyns :: Map Name TySyn
mTySyns = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name TySyn
mTySyns
, mNewtypes :: Map Name Newtype
mNewtypes = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
, mPrimTypes :: Map Name AbstractType
mPrimTypes = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes
, mDecls :: [DeclGroup]
mDecls = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> [DeclGroup]
mDecls
, mSubmodules :: Map Name (IfaceNames Name)
mSubmodules = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules
, mFunctors :: Map Name (ModuleG Name)
mFunctors = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors
, mSignatures :: Map Name ModParamNames
mSignatures = forall {a}. Semigroup a => (ModuleG mname -> a) -> a
uni forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures
}
where
uni :: (ModuleG mname -> a) -> a
uni ModuleG mname -> a
f = ModuleG mname -> a
f ModuleG mname
m1 forall a. Semigroup a => a -> a -> a
<> ModuleG mname -> a
f ModuleG mname
m2
addDecls :: DeclGroup -> InferM ()
addDecls :: DeclGroup -> InferM ()
addDecls DeclGroup
ds =
do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mDecls :: [DeclGroup]
mDecls = DeclGroup
ds forall a. a -> [a] -> [a]
: forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ScopeName
r }
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = RW -> Map Name Schema
new RW
rw }
where
add :: Decl -> Map Name Schema -> Map Name Schema
add Decl
d = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Decl -> Name
dName Decl
d) (Decl -> Schema
dSignature Decl
d)
new :: RW -> Map Name Schema
new RW
rw = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Decl -> Map Name Schema -> Map Name Schema
add (RW -> Map Name Schema
iBindTypes RW
rw) (DeclGroup -> [Decl]
groupDecls DeclGroup
ds)
addTySyn :: TySyn -> InferM ()
addTySyn :: TySyn -> InferM ()
addTySyn TySyn
t =
do let x :: Name
x = TySyn -> Name
tsName TySyn
t
String -> Name -> InferM ()
checkTShadowing String
"synonym" Name
x
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mTySyns :: Map Name TySyn
mTySyns = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x TySyn
t (forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ScopeName
r) }
addNewtype :: Newtype -> InferM ()
addNewtype :: Newtype -> InferM ()
addNewtype Newtype
t =
do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mNewtypes :: Map Name Newtype
mNewtypes = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Newtype -> Name
ntName Newtype
t) Newtype
t (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ScopeName
r) }
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Newtype -> Name
ntConName Newtype
t)
(Newtype -> Schema
newtypeConType Newtype
t)
(RW -> Map Name Schema
iBindTypes RW
rw) }
addPrimType :: AbstractType -> InferM ()
addPrimType :: AbstractType -> InferM ()
addPrimType AbstractType
t =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r ->
ModuleG ScopeName
r { mPrimTypes :: Map Name AbstractType
mPrimTypes = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (AbstractType -> Name
atName AbstractType
t) AbstractType
t (forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG ScopeName
r) }
addParamType :: ModTParam -> InferM ()
addParamType :: ModTParam -> InferM ()
addParamType ModTParam
a =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParamTypes :: Map Name ModTParam
mParamTypes = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModTParam -> Name
mtpName ModTParam
a) ModTParam
a (forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG ScopeName
r) }
addSignatures :: Map Name ModParamNames -> InferM ()
addSignatures :: Map Name ModParamNames -> InferM ()
addSignatures Map Name ModParamNames
mp =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mSignatures :: Map Name ModParamNames
mSignatures = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name ModParamNames
mp (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ScopeName
r) }
addSubmodules :: Map Name (If.IfaceNames Name) -> InferM ()
addSubmodules :: Map Name (IfaceNames Name) -> InferM ()
addSubmodules Map Name (IfaceNames Name)
mp =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mSubmodules :: Map Name (IfaceNames Name)
mSubmodules = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (IfaceNames Name)
mp (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ScopeName
r) }
addFunctors :: Map Name (ModuleG Name) -> InferM ()
addFunctors :: Map Name (ModuleG Name) -> InferM ()
addFunctors Map Name (ModuleG Name)
mp =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mFunctors :: Map Name (ModuleG Name)
mFunctors = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (ModuleG Name)
mp (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ScopeName
r) }
addParamFun :: ModVParam -> InferM ()
addParamFun :: ModVParam -> InferM ()
addParamFun ModVParam
x =
do (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParamFuns :: Map Name ModVParam
mParamFuns = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModVParam -> Name
mvpName ModVParam
x) ModVParam
x (forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG ScopeName
r) }
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ \RW
rw -> RW
rw { iBindTypes :: Map Name Schema
iBindTypes = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModVParam -> Name
mvpName ModVParam
x) (ModVParam -> Schema
mvpType ModVParam
x)
(RW -> Map Name Schema
iBindTypes RW
rw) }
addParameterConstraints :: [Located Prop] -> InferM ()
addParameterConstraints :: [Located Type] -> InferM ()
addParameterConstraints [Located Type]
ps =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParamConstraints :: [Located Type]
mParamConstraints = [Located Type]
ps forall a. [a] -> [a] -> [a]
++ forall mname. ModuleG mname -> [Located Type]
mParamConstraints ModuleG ScopeName
r }
addModParam :: ModParam -> InferM ()
addModParam :: ModParam -> InferM ()
addModParam ModParam
p =
(ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
updScope \ModuleG ScopeName
r -> ModuleG ScopeName
r { mParams :: FunctorParams
mParams = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModParam -> Ident
mpName ModParam
p) ModParam
p (forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ScopeName
r) }
inNewScope :: InferM a -> InferM a
inNewScope :: forall a. InferM a -> InferM a
inNewScope InferM a
m =
do [Map Name Type]
curScopes <- RW -> [Map Name Type]
iExistTVars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall (m :: * -> *) i. StateM m i => m i
get
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iExistTVars :: [Map Name Type]
iExistTVars = forall k a. Map k a
Map.empty forall a. a -> [a] -> [a]
: [Map Name Type]
curScopes }
a
a <- InferM a
m
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
s -> RW
s { iExistTVars :: [Map Name Type]
iExistTVars = [Map Name Type]
curScopes }
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
withVarType :: Name -> VarType -> InferM a -> InferM a
withVarType :: forall a. Name -> VarType -> InferM a -> InferM a
withVarType Name
x VarType
s (IM ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m) =
forall a.
ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
-> InferM a
IM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
r -> RO
r { iVars :: Map Name VarType
iVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x VarType
s (RO -> Map Name VarType
iVars RO
r) }) ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
m
withVarTypes :: [(Name,VarType)] -> InferM a -> InferM a
withVarTypes :: forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
xs InferM a
m = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Name -> VarType -> InferM a -> InferM a
withVarType) InferM a
m [(Name, VarType)]
xs
withVar :: Name -> Schema -> InferM a -> InferM a
withVar :: forall a. Name -> Schema -> InferM a -> InferM a
withVar Name
x Schema
s = forall a. Name -> VarType -> InferM a -> InferM a
withVarType Name
x (Schema -> VarType
ExtVar Schema
s)
withMonoType :: (Name,Located Type) -> InferM a -> InferM a
withMonoType :: forall a. (Name, Located Type) -> InferM a -> InferM a
withMonoType (Name
x,Located Type
lt) = forall a. Name -> Schema -> InferM a -> InferM a
withVar Name
x ([TParam] -> [Type] -> Type -> Schema
Forall [] [] (forall a. Located a -> a
thing Located Type
lt))
withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a
withMonoTypes :: forall a. Map Name (Located Type) -> InferM a -> InferM a
withMonoTypes Map Name (Located Type)
xs InferM a
m = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Name, Located Type) -> InferM a -> InferM a
withMonoType InferM a
m (forall k a. Map k a -> [(k, a)]
Map.toList Map Name (Located Type)
xs)
newtype KindM a = KM { forall a. KindM a -> ReaderT KRO (StateT KRW InferM) a
unKM :: ReaderT KRO (StateT KRW InferM) a }
data KRO = KRO { KRO -> Map Name TParam
lazyTParams :: Map Name TParam
, KRO -> AllowWildCards
allowWild :: AllowWildCards
}
data AllowWildCards = AllowWildCards | NoWildCards
data KRW = KRW { KRW -> Map Name Kind
typeParams :: Map Name Kind
, KRW -> [(ConstraintSource, [Type])]
kCtrs :: [(ConstraintSource,[Prop])]
}
instance Functor KindM where
fmap :: forall a b. (a -> b) -> KindM a -> KindM b
fmap a -> b
f (KM ReaderT KRO (StateT KRW InferM) a
m) = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ReaderT KRO (StateT KRW InferM) a
m)
instance A.Applicative KindM where
pure :: forall a. a -> KindM a
pure a
x = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
<*> :: forall a b. KindM (a -> b) -> KindM a -> KindM b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad KindM where
return :: forall a. a -> KindM a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
KM ReaderT KRO (StateT KRW InferM) a
m >>= :: forall a b. KindM a -> (a -> KindM b) -> KindM b
>>= a -> KindM b
k = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (ReaderT KRO (StateT KRW InferM) a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. KindM a -> ReaderT KRO (StateT KRW InferM) a
unKM forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> KindM b
k)
instance Fail.MonadFail KindM where
fail :: forall a. String -> KindM a
fail String
x = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
x)
runKindM :: AllowWildCards
-> [(Name, Maybe Kind, TParam)]
-> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource,[Prop])])
runKindM :: forall a.
AllowWildCards
-> [(Name, Maybe Kind, TParam)]
-> KindM a
-> InferM (a, Map Name Kind, [(ConstraintSource, [Type])])
runKindM AllowWildCards
wildOK [(Name, Maybe Kind, TParam)]
vs (KM ReaderT KRO (StateT KRW InferM) a
m) =
do (a
a,KRW
kw) <- forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT KRW
krw (forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT KRO
kro ReaderT KRO (StateT KRW InferM) a
m)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, KRW -> Map Name Kind
typeParams KRW
kw, KRW -> [(ConstraintSource, [Type])]
kCtrs KRW
kw)
where
tps :: Map Name TParam
tps = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
x,TParam
t) | (Name
x,Maybe Kind
_,TParam
t) <- [(Name, Maybe Kind, TParam)]
vs ]
kro :: KRO
kro = KRO { allowWild :: AllowWildCards
allowWild = AllowWildCards
wildOK, lazyTParams :: Map Name TParam
lazyTParams = Map Name TParam
tps }
krw :: KRW
krw = KRW { typeParams :: Map Name Kind
typeParams = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
x,Kind
k) | (Name
x,Just Kind
k,TParam
_) <- [(Name, Maybe Kind, TParam)]
vs ]
, kCtrs :: [(ConstraintSource, [Type])]
kCtrs = []
}
data LkpTyVar = TLocalVar TParam (Maybe Kind)
| TOuterVar TParam
kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
kLookupTyVar Name
x = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$
do Map Name TParam
vs <- KRO -> Map Name TParam
lazyTParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (m :: * -> *) i. ReaderM m i => m i
ask
KRW
ss <- forall (m :: * -> *) i. StateM m i => m i
get
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Map Name TParam
vs of
Just TParam
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TParam -> Maybe Kind -> LkpTyVar
TLocalVar TParam
t forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall a b. (a -> b) -> a -> b
$ KRW -> Map Name Kind
typeParams KRW
ss
Maybe TParam
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do Maybe TParam
t <- Name -> InferM (Maybe TParam)
lookupTParam Name
x
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TParam -> LkpTyVar
TOuterVar Maybe TParam
t)
kWildOK :: KindM AllowWildCards
kWildOK :: KindM AllowWildCards
kWildOK = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap KRO -> AllowWildCards
allowWild forall (m :: * -> *) i. ReaderM m i => m i
ask
kRecordError :: Error -> KindM ()
kRecordError :: Error -> KindM ()
kRecordError Error
e = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Error -> InferM ()
recordError Error
e
kRecordWarning :: Warning -> KindM ()
kRecordWarning :: Warning -> KindM ()
kRecordWarning Warning
w = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Warning -> InferM ()
recordWarning Warning
w
kIO :: IO a -> KindM a
kIO :: forall a. IO a -> KindM a
kIO IO a
m = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IO a -> InferM a
io IO a
m
kNewType :: TypeSource -> Kind -> KindM Type
kNewType :: TypeSource -> Kind -> KindM Type
kNewType TypeSource
src Kind
k =
do Set TParam
tps <- forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ do Map Name TParam
vs <- forall (m :: * -> *) r a. ReaderM m r => (r -> a) -> m a
asks KRO -> Map Name TParam
lazyTParams
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map Name TParam
vs)
forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ TVar -> Type
TVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` TypeSource -> Set TParam -> Kind -> InferM TVar
newTVar' TypeSource
src Set TParam
tps Kind
k
kLookupTSyn :: Name -> KindM (Maybe TySyn)
kLookupTSyn :: Name -> KindM (Maybe TySyn)
kLookupTSyn Name
x = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Name -> InferM (Maybe TySyn)
lookupTSyn Name
x
kLookupNewtype :: Name -> KindM (Maybe Newtype)
kLookupNewtype :: Name -> KindM (Maybe Newtype)
kLookupNewtype Name
x = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Name -> InferM (Maybe Newtype)
lookupNewtype Name
x
kLookupParamType :: Name -> KindM (Maybe ModTParam)
kLookupParamType :: Name -> KindM (Maybe ModTParam)
kLookupParamType Name
x = forall a. InferM a -> KindM a
kInInferM (Name -> InferM (Maybe ModTParam)
lookupParamType Name
x)
kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
kLookupAbstractType Name
x = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Name -> InferM (Maybe AbstractType)
lookupAbstractType Name
x
kExistTVar :: Name -> Kind -> KindM Type
kExistTVar :: Name -> Kind -> KindM Type
kExistTVar Name
x Kind
k = forall a. InferM a -> KindM a
kInInferM forall a b. (a -> b) -> a -> b
$ Name -> Kind -> InferM Type
existVar Name
x Kind
k
kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
kInstantiateT Type
t [(TParam, Type)]
as = forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
where su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
as
kSetKind :: Name -> Kind -> KindM ()
kSetKind :: Name -> Kind -> KindM ()
kSetKind Name
v Kind
k = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \KRW
s -> KRW
s{ typeParams :: Map Name Kind
typeParams = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
v Kind
k (KRW -> Map Name Kind
typeParams KRW
s)}
kInRange :: Range -> KindM a -> KindM a
kInRange :: forall a. Range -> KindM a -> KindM a
kInRange Range
r (KM ReaderT KRO (StateT KRW InferM) a
m) = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$
do KRO
e <- forall (m :: * -> *) i. ReaderM m i => m i
ask
KRW
s <- forall (m :: * -> *) i. StateM m i => m i
get
(a
a,KRW
s1) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Range -> InferM a -> InferM a
inRange Range
r forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT KRW
s forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT KRO
e ReaderT KRO (StateT KRW InferM) a
m
forall (m :: * -> *) i. StateM m i => i -> m ()
set KRW
s1
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kNewGoals :: ConstraintSource -> [Type] -> KindM ()
kNewGoals ConstraintSource
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
kNewGoals ConstraintSource
c [Type]
ps = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \KRW
s -> KRW
s { kCtrs :: [(ConstraintSource, [Type])]
kCtrs = (ConstraintSource
c,[Type]
ps) forall a. a -> [a] -> [a]
: KRW -> [(ConstraintSource, [Type])]
kCtrs KRW
s }
kInInferM :: InferM a -> KindM a
kInInferM :: forall a. InferM a -> KindM a
kInInferM InferM a
m = forall a. ReaderT KRO (StateT KRW InferM) a -> KindM a
KM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift InferM a
m