#if __GLASGOW_HASKELL__ >= 706
#else
#endif
module Cryptol.TypeCheck.Monad
( module Cryptol.TypeCheck.Monad
, module Cryptol.TypeCheck.InferTypes
) where
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
import Cryptol.TypeCheck.InferTypes
import Cryptol.Utils.PP(pp, (<+>), Doc, text, quotes)
import Cryptol.Utils.Panic(panic)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Map (Map)
import Data.Set (Set)
import Data.List(find)
import Data.Maybe(mapMaybe)
import MonadLib
import qualified Control.Applicative as A
import Control.Monad.Fix(MonadFix(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Functor
#endif
data InferInput = InferInput
{ inpRange :: Range
, inpVars :: Map QName Schema
, inpTSyns :: Map QName TySyn
, inpNewtypes :: Map QName Newtype
, inpNameSeeds :: NameSeeds
, inpMonoBinds :: Bool
} deriving Show
data NameSeeds = NameSeeds
{ seedTVar :: !Int
, seedGoal :: !Int
} deriving Show
nameSeeds :: NameSeeds
nameSeeds = NameSeeds { seedTVar = 10, seedGoal = 0 }
data InferOutput a
= InferFailed [(Range,Warning)] [(Range,Error)]
| InferOK [(Range,Warning)] NameSeeds a
deriving Show
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM info (IM m) =
do rec ro <- return RO { iRange = inpRange info
, iVars = Map.map ExtVar (inpVars info)
, iTVars = []
, iTSyns = fmap mkExternal (inpTSyns info)
, iNewtypes = fmap mkExternal (inpNewtypes info)
, iSolvedHasLazy = iSolvedHas finalRW
, iMonoBinds = inpMonoBinds info
}
(result, finalRW) <- runStateT rw $ runReaderT ro m
let theSu = iSubst finalRW
defSu = defaultingSubst theSu
warns = [(r,apSubst theSu w) | (r,w) <- iWarnings finalRW ]
case iErrors finalRW of
[] ->
case (iCts finalRW, iHasCts finalRW) of
(cts,[])
| nullGoals cts
-> return $ InferOK warns
(iNameSeeds finalRW)
(apSubst defSu result)
(cts,has) -> return $ InferFailed warns
[ ( goalRange g
, UnsolvedGoal (apSubst theSu g)
) | g <- fromGoals cts ++ map hasGoal has
]
errs -> return $ InferFailed warns [(r,apSubst theSu e) | (r,e) <- errs]
where
mkExternal x = (IsExternal, x)
rw = RW { iErrors = []
, iWarnings = []
, iSubst = emptySubst
, iExistTVars = []
, iNameSeeds = inpNameSeeds info
, iCts = emptyGoals
, iHasCts = []
, iSolvedHas = Map.empty
}
newtype InferM a = IM { unIM :: ReaderT RO (StateT RW IO) a }
data DefLoc = IsLocal | IsExternal
data RO = RO
{ iRange :: Range
, iVars :: Map QName VarType
, iTVars :: [TParam]
, iTSyns :: Map QName (DefLoc, TySyn)
, iNewtypes :: Map QName (DefLoc, Newtype)
, iSolvedHasLazy :: Map Int (Expr -> Expr)
, iMonoBinds :: Bool
}
data RW = RW
{ iErrors :: ![(Range,Error)]
, iWarnings :: ![(Range,Warning)]
, iSubst :: !Subst
, iExistTVars :: [Map QName Type]
, iSolvedHas :: Map Int (Expr -> Expr)
, iNameSeeds :: !NameSeeds
, iCts :: !Goals
, iHasCts :: ![HasGoal]
}
instance Functor InferM where
fmap f (IM m) = IM (fmap f m)
instance A.Applicative InferM where
pure = return
(<*>) = ap
instance Monad InferM where
return x = IM (return x)
fail x = IM (fail x)
IM m >>= f = IM (m >>= unIM . f)
instance MonadFix InferM where
mfix f = IM (mfix (unIM . f))
io :: IO a -> InferM a
io m = IM $ inBase m
inRange :: Range -> InferM a -> InferM a
inRange r (IM m) = IM $ mapReader (\ro -> ro { iRange = r }) m
inRangeMb :: Maybe Range -> InferM a -> InferM a
inRangeMb Nothing m = m
inRangeMb (Just r) m = inRange r m
curRange :: InferM Range
curRange = IM $ asks iRange
recordError :: Error -> InferM ()
recordError e =
do r <- curRange
IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s }
recordWarning :: Warning -> InferM ()
recordWarning w =
do r <- curRange
IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s }
newGoal :: ConstraintSource -> Prop -> InferM Goal
newGoal goalSource goal =
do goalRange <- curRange
return Goal { .. }
newGoals :: ConstraintSource -> [Prop] -> InferM ()
newGoals src ps = addGoals =<< mapM (newGoal src) ps
getGoals :: InferM [Goal]
getGoals =
do goals <- applySubst =<< IM (sets $ \s -> (iCts s, s { iCts = emptyGoals }))
return (fromGoals goals)
addGoals :: [Goal] -> InferM ()
addGoals gs = IM $ sets_ $ \s -> s { iCts = foldl (flip insertGoal) (iCts s) gs }
collectGoals :: InferM a -> InferM (a, [Goal])
collectGoals m =
do origGs <- applySubst =<< getGoals'
a <- m
newGs <- getGoals
setGoals' origGs
return (a, newGs)
where
getGoals' = IM $ sets $ \ RW { .. } -> (iCts, RW { iCts = emptyGoals, .. })
setGoals' gs = IM $ sets $ \ RW { .. } -> ((), RW { iCts = gs, .. })
newHasGoal :: P.Selector -> Type -> Type -> InferM (Expr -> Expr)
newHasGoal l ty f =
do goalName <- newGoalName
g <- newGoal CtSelector (pHas l ty f)
IM $ sets_ $ \s -> s { iHasCts = HasGoal goalName g : iHasCts s }
solns <- IM $ fmap iSolvedHasLazy ask
return $ case Map.lookup goalName solns of
Just e1 -> e1
Nothing -> panic "newHasGoal" ["Unsolved has goal in result"]
addHasGoal :: HasGoal -> InferM ()
addHasGoal g = IM $ sets_ $ \s -> s { iHasCts = g : iHasCts s }
getHasGoals :: InferM [HasGoal]
getHasGoals = do gs <- IM $ sets $ \s -> (iHasCts s, s { iHasCts = [] })
applySubst gs
solveHasGoal :: Int -> (Expr -> Expr) -> InferM ()
solveHasGoal n e =
IM $ sets_ $ \s -> s { iSolvedHas = Map.insert n e (iSolvedHas s) }
newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a
newName upd = IM $ sets $ \s -> let (x,seeds) = upd (iNameSeeds s)
in (x, s { iNameSeeds = seeds })
newGoalName :: InferM Int
newGoalName = newName $ \s -> let x = seedGoal s
in (x, s { seedGoal = x + 1})
newTVar :: Doc -> Kind -> InferM TVar
newTVar src k = newTVar' src Set.empty k
newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar
newTVar' src extraBound k =
do bound <- getBoundInScope
let vs = Set.union extraBound bound
newName $ \s -> let x = seedTVar s
in (TVFree x k vs src, s { seedTVar = x + 1 })
newTParam :: Maybe QName -> Kind -> InferM TParam
newTParam nm k = newName $ \s -> let x = seedTVar s
in (TParam { tpUnique = x
, tpKind = k
, tpName = nm
}
, s { seedTVar = x + 1 })
newType :: Doc -> Kind -> InferM Type
newType src k = TVar `fmap` newTVar src k
unify :: Type -> Type -> InferM [Prop]
unify t1 t2 =
do t1' <- applySubst t1
t2' <- applySubst t2
case mgu t1' t2' of
OK (su1,ps) -> extendSubst su1 >> return ps
Error err ->
do case err of
UniTypeLenMismatch _ _ -> recordError (TypeMismatch t1' t2')
UniTypeMismatch s1 s2 -> recordError (TypeMismatch s1 s2)
UniKindMismatch k1 k2 -> recordError (KindMismatch k1 k2)
UniRecursive x t -> recordError (RecursiveType (TVar x) t)
UniNonPolyDepends x vs -> recordError
(TypeVariableEscaped (TVar x) vs)
UniNonPoly x t -> recordError (NotForAll x t)
return []
applySubst :: TVars t => t -> InferM t
applySubst t =
do su <- getSubst
return (apSubst su t)
getSubst :: InferM Subst
getSubst = IM $ fmap iSubst get
extendSubst :: Subst -> InferM ()
extendSubst su = IM $ sets_ $ \s -> s { iSubst = su @@ iSubst s }
varsWithAsmps :: InferM (Set TVar)
varsWithAsmps =
do env <- IM $ fmap (Map.elems . iVars) ask
fromEnv <- forM env $ \v ->
case v of
ExtVar sch -> getVars sch
CurSCC _ t -> getVars t
sels <- IM $ fmap (map (goal . hasGoal) . iHasCts) get
fromSels <- mapM getVars sels
fromEx <- (getVars . concatMap Map.elems) =<< IM (fmap iExistTVars get)
return (Set.unions fromEnv `Set.union` Set.unions fromSels
`Set.union` fromEx)
where
getVars x = fvs `fmap` applySubst x
lookupVar :: QName -> InferM VarType
lookupVar x =
do mb <- IM $ asks $ Map.lookup x . iVars
case mb of
Just t -> return t
Nothing ->
do mbNT <- lookupNewtype x
case mbNT of
Just nt -> return (ExtVar (newtypeConType nt))
Nothing -> do recordError $ UndefinedVariable x
a <- newType (text "type of" <+> pp x) KType
return $ ExtVar $ Forall [] [] a
lookupTVar :: QName -> InferM (Maybe Type)
lookupTVar x = IM $ asks $ fmap (TVar . tpVar) . find this . iTVars
where this tp = tpName tp == Just x
lookupTSyn :: QName -> InferM (Maybe TySyn)
lookupTSyn x = fmap (fmap snd . Map.lookup x) getTSyns
lookupNewtype :: QName -> InferM (Maybe Newtype)
lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes
existVar :: QName -> Kind -> InferM Type
existVar x k =
do scopes <- iExistTVars <$> IM get
case msum (map (Map.lookup x) scopes) of
Just ty -> return ty
Nothing ->
case scopes of
[] ->
do recordError $ ErrorMsg $
text "Undefined type" <+> quotes (pp x)
newType (text "undefined existential type varible" <+>
quotes (pp x)) k
sc : more ->
do ty <- newType (text "existential type variable"
<+> quotes (pp x)) k
IM $ sets_ $ \s -> s{ iExistTVars = Map.insert x ty sc : more }
return ty
getTSyns :: InferM (Map QName (DefLoc,TySyn))
getTSyns = IM $ asks iTSyns
getNewtypes :: InferM (Map QName (DefLoc,Newtype))
getNewtypes = IM $ asks iNewtypes
getTVars :: InferM (Set QName)
getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars
getBoundInScope :: InferM (Set TVar)
getBoundInScope = IM $ asks $ Set.fromList . map tpVar . iTVars
getMonoBinds :: InferM Bool
getMonoBinds = IM (asks iMonoBinds)
checkTShadowing :: String -> QName -> InferM ()
checkTShadowing this new =
do ro <- IM ask
rw <- IM get
let shadowed =
do _ <- Map.lookup new (iTSyns ro)
return "type synonym"
`mplus`
do guard (new `elem` mapMaybe tpName (iTVars ro))
return "type variable"
`mplus`
do _ <- msum (map (Map.lookup new) (iExistTVars rw))
return "type"
case shadowed of
Nothing -> return ()
Just that ->
recordError $ ErrorMsg $
text "Type" <+> text this <+> quotes (pp new) <+>
text "shadows an existing" <+>
text that <+> text "with the same name."
withTParam :: TParam -> InferM a -> InferM a
withTParam p (IM m) =
do case tpName p of
Just x -> checkTShadowing "variable" x
Nothing -> return ()
IM $ mapReader (\r -> r { iTVars = p : iTVars r }) m
withTParams :: [TParam] -> InferM a -> InferM a
withTParams ps m = foldr withTParam m ps
withTySyn :: TySyn -> InferM a -> InferM a
withTySyn t (IM m) =
do let x = tsName t
checkTShadowing "synonym" x
IM $ mapReader (\r -> r { iTSyns = Map.insert x (IsLocal,t) (iTSyns r) }) m
withNewtype :: Newtype -> InferM a -> InferM a
withNewtype t (IM m) =
IM $ mapReader
(\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t)
(iNewtypes r) }) m
withVarType :: QName -> VarType -> InferM a -> InferM a
withVarType x s (IM m) =
IM $ mapReader (\r -> r { iVars = Map.insert x s (iVars r) }) m
withVarTypes :: [(QName,VarType)] -> InferM a -> InferM a
withVarTypes xs m = foldr (uncurry withVarType) m xs
withVar :: QName -> Schema -> InferM a -> InferM a
withVar x s = withVarType x (ExtVar s)
withMonoType :: (QName,Located Type) -> InferM a -> InferM a
withMonoType (x,lt) = withVar x (Forall [] [] (thing lt))
withMonoTypes :: Map QName (Located Type) -> InferM a -> InferM a
withMonoTypes xs m = foldr withMonoType m (Map.toList xs)
withDecls :: ([TySyn], Map QName Schema) -> InferM a -> InferM a
withDecls (ts,vs) m = foldr withTySyn (foldr add m (Map.toList vs)) ts
where
add (x,t) = withVar x t
inNewScope :: InferM a -> InferM a
inNewScope m =
do curScopes <- iExistTVars <$> IM get
IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes }
a <- m
IM $ sets_ $ \s -> s { iExistTVars = curScopes }
return a
newtype KindM a = KM { unKM :: ReaderT KRO (StateT KRW InferM) a }
data KRO = KRO { lazyTVars :: Map QName Type
, allowWild :: Bool
}
data KRW = KRW { typeParams :: Map QName Kind
}
instance Functor KindM where
fmap f (KM m) = KM (fmap f m)
instance A.Applicative KindM where
pure = return
(<*>) = ap
instance Monad KindM where
return x = KM (return x)
fail x = KM (fail x)
KM m >>= k = KM (m >>= unKM . k)
runKindM :: Bool
-> [(QName, Maybe Kind, Type)]
-> KindM a -> InferM (a, Map QName Kind)
runKindM wildOK vs (KM m) =
do (a,kw) <- runStateT krw (runReaderT kro m)
return (a, typeParams kw)
where
tys = Map.fromList [ (x,t) | (x,_,t) <- vs ]
kro = KRO { allowWild = wildOK, lazyTVars = tys }
krw = KRW { typeParams = Map.fromList [ (x,k) | (x,Just k,_) <- vs ] }
data LkpTyVar = TLocalVar Type (Maybe Kind)
| TOuterVar Type
kLookupTyVar :: QName -> KindM (Maybe LkpTyVar)
kLookupTyVar x = KM $
do vs <- lazyTVars `fmap` ask
ss <- get
case Map.lookup x vs of
Just t -> return $ Just $ TLocalVar t $ Map.lookup x $ typeParams ss
Nothing -> lift $ lift $ do t <- lookupTVar x
return (fmap TOuterVar t)
kWildOK :: KindM Bool
kWildOK = KM $ fmap allowWild ask
kRecordError :: Error -> KindM ()
kRecordError e = kInInferM $ recordError e
kRecordWarning :: Warning -> KindM ()
kRecordWarning w = kInInferM $ recordWarning w
kNewType :: Doc -> Kind -> KindM Type
kNewType src k =
do tps <- KM $ do vs <- asks lazyTVars
return $ Set.fromList [ tv | TVar tv <- Map.elems vs ]
kInInferM $ TVar `fmap` newTVar' src tps k
kLookupTSyn :: QName -> KindM (Maybe TySyn)
kLookupTSyn x = kInInferM $ lookupTSyn x
kLookupNewtype :: QName -> KindM (Maybe Newtype)
kLookupNewtype x = kInInferM $ lookupNewtype x
kExistTVar :: QName -> Kind -> KindM Type
kExistTVar x k = kInInferM $ existVar x k
kInstantiateT :: Type -> [(TParam,Type)] -> KindM Type
kInstantiateT t as = return (apSubst su t)
where su = listSubst [ (tpVar x, t1) | (x,t1) <- as ]
kSetKind :: QName -> Kind -> KindM ()
kSetKind v k = KM $ sets_ $ \s -> s{ typeParams = Map.insert v k (typeParams s)}
kInRange :: Range -> KindM a -> KindM a
kInRange r (KM m) = KM $
do e <- ask
s <- get
(a,s1) <- lift $ lift $ inRange r $ runStateT s $ runReaderT e m
set s1
return a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kNewGoals c ps = kInInferM $ newGoals c ps
kInInferM :: InferM a -> KindM a
kInInferM m = KM $ lift $ lift m