anaStarType :: Type -> State Env (Maybe Type)
anaStarType t = fmap (fmap snd) $ anaType (Just universe, t)
anaType :: (Maybe Kind, Type)
-> State Env (Maybe ((RawKind,
Set.Set Kind), Type))
anaType p = fromResult $ anaTypeM p
anaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)
anaTypeScheme (TypeScheme tArgs ty p) =
do tvs <- gets localTypeVars -- save global variables
mArgs <- mapM anaddTypeVarDecl tArgs
let newArgs = catMaybes mArgs
Nothing -> do putLocalTypeVars tvs -- forget local variables
let newSc = TypeScheme newArgs newTy p
putLocalTypeVars tvs -- forget local variables
generalizeS :: TypeScheme -> State Env TypeScheme
generalizeS sc@(TypeScheme tArgs ty p) = do
let fvs = leaves (> 0) ty
comp a b = compare (fst a) $ fst b
tvs <- gets localTypeVars
let newArgs = map ( \ (_, (i, _)) -> case
Map.lookup i tvs of
Nothing -> error "generalizeS"
Just (TypeVarDefn v vk rk c) ->
TypeArg i v vk rk c Other nullRange) svs
newSc = TypeScheme (genTypeArgs newArgs) (generalize newArgs ty) p
if null tArgs then return newSc
addDiags $ generalizable False sc
-- | store type id and check kind arity (warn on redeclared types)
addTypeId :: Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId warn dfn k i = do
tvs <- gets localTypeVars
if warn then addDiags[mkDiag Warning
"new type shadows type variable" i]
addDiags [mkDiag Error "class name used as type" i]
Nothing -> addTypeKind warn dfn i k
-- | check if the kind only misses variance indicators of the known raw kind
isLiberalKind :: ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind cm b ok k = case ok of
FunKind ov fok aok _ -> case k of
nfk <- isLiberalKind cm (not b) fok fk
nak <- isLiberalKind cm b aok ak
return $ FunKind (liberalVariance b ov v) nfk nak ps
Just ci -> maybe Nothing (const $ Just k) $ minRawKind "" ok
liberalVariance :: Bool -> Variance -> Variance -> Variance
liberalVariance b v1 v2 = if b then minVariance v1 v2 else
revVariance $ minVariance (revVariance v1) $ revVariance v2
anaKind :: Kind -> State Env RawKind
mrk <- fromResult $ anaKindM k . classMap
Nothing -> error "anaKind"
-- | store type as is (warn on redeclared types)
addTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env Bool
addTypeKind warn d i k = do
addTypeSym ck = if
Map.member i bTypes then return () else
addSymbol $ idToTypeSymbol e i ck
if placeCount i <= kindArity rk then return () else
addDiags [mkDiag Error "wrong arity of" i]
Just (TypeInfo ok oldks sups dfn) ->
case minRawKind "" ok rk of
addDiags $ diffKindDiag i ok rk
Just r -> case isLiberalKind cm True r k of
let isNewInst = newKind cm nk oldks
insts = if isNewInst then addNewKind cm nk oldks else oldks
Result ds mDef = mergeTypeDefn dfn d
if warn && not isNewInst && case (dfn, d) of
(PreDatatype, DatatypeDefn _) -> False
then addDiags [mkDiag Hint "redeclared type" i]
putTypeMap $
Map.insert i (TypeInfo r insts sups newDefn) tm
addDiags $ map (improveDiag i) ds
addDiags [mkDiag Error "cannot refine kind" i]
nonUniqueKind :: (PosItem a, Pretty a) =>
Set.Set Kind -> a ->
(Kind -> State Env (Maybe b)) -> State Env (Maybe b)
_ -> do addDiags [mkDiag Error "non-unique kind for" a]
-- | analyse a type argument
anaddTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl (TypeArg i v vk _ _ s ps) = do
addDiags [mkDiag Error "class used as type variable" i]
let Result ds (Just rk) = anaKindM k cm
addLocalTypeVar True (TypeVarDefn v vk rk c) i
return $ Just $ TypeArg i v vk rk c s ps
mt <- anaType (Nothing, t)
Nothing -> return Nothing
nonUniqueKind ks t $ \ k -> do
addLocalTypeVar True (TypeVarDefn NonVar nd rk c) i
return $ Just $ TypeArg i v (Downset nt) rk c s ps
tvs <- gets localTypeVars
addDiags [mkDiag Error "unknown type variable" i]
let dvk = VarKind universe
addLocalTypeVar True (TypeVarDefn v dvk rStar c) i
return $ Just $ TypeArg i v dvk rStar c s ps
Just (TypeVarDefn v0 dvk rk _) -> do
addLocalTypeVar False (TypeVarDefn v0 dvk rk c) i
return $ Just $ TypeArg i v0 dvk rk c s ps
-- | partition information of an uninstantiated identifier
partitionOpId :: Env -> Id -> TypeScheme -> (
Set.Set OpInfo,
Set.Set OpInfo)
checkUnusedTypevars :: TypeScheme -> State Env TypeScheme
checkUnusedTypevars sc@(TypeScheme tArgs t ps) = do
let ls = map (fst . snd) $ leaves (< 0) t -- generic vars
rest = map getTypeVar tArgs List.\\ ls
if null rest then return ()
else addDiags [Diag Warning ("unused type variables: "
++ show(ppWithCommas rest)) ps]
checkPlaceCount :: Env -> Id -> TypeScheme -> [Diagnosis]
checkPlaceCount e i (TypeScheme _ ty _) =
let (fty, fargs) = getTypeAppl ty in
if length fargs == 2 && lesserType e fty (toFunType PFunArr) then
let (pty, ts) = getTypeAppl (head fargs)
if n > 1 && lesserType e pty (toProdType n nullRange) then
if placeCount i /= n then
[mkDiag Warning "wrong number of places in" i]
else [mkDiag Warning "expected tuple argument for" i]
else [mkDiag Warning "expected function type for" i]
-- | storing an operation
addOpId :: Id -> TypeScheme ->
Set.Set OpAttr -> OpDefn -> State Env Bool
addOpId i oldSc attrs dfn = do
sc@(TypeScheme _ ty _) <- checkUnusedTypevars oldSc
ds = checkPlaceCount e i sc
(l, r) = partitionOpId e i sc
oInfo = OpInfo sc attrs dfn
Result es mo = foldM mergeOpInfo oInfo $
Set.toList l
addDiags $ map (improveDiag i) es
if i `elem` map fst bList then
addDiags [mkDiag Warning "ignoring declaration for builtin identifier" i]
_ -> addDiags [mkDiag Hint ("repeated declaration of '"
++ showId i "' with type") ty]
addSymbol $ idToOpSymbol e i $ opType oi
-- | add a local variable with an analysed type (if True then warn)
addLocalVar :: Bool -> VarDecl -> State Env ()
addLocalVar warn (VarDecl v t _ _) =
addDiags [mkDiag Hint "variable shadows global name(s)" v]
addDiags [mkDiag Hint "rebound variable" v]
-- | add analysed local variable or type variable declaration
addGenVarDecl :: GenVarDecl -> State Env ()
addGenVarDecl(GenVarDecl v) = addLocalVar True v
addGenVarDecl(GenTypeVarDecl t) = addTypeVarDecl False t
-- | analyse and add local variable or type variable declaration
anaddGenVarDecl :: Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl warn gv = case gv of
GenVarDecl v -> optAnaddVarDecl warn v
GenTypeVarDecl t -> anaddTypeVarDecl t >>= (return . fmap GenTypeVarDecl)
convTypeToKind :: Type -> Maybe (Variance, Kind)
convTypeToKind ty = let s = showDoc ty "" in
case runParser (extKind << eof) (emptyAnnos ()) "" s of
Right (v, k) -> Just (v, k)
convertTypeToKind :: Env -> Type -> Result (Variance, Kind)
convertTypeToKind e ty = case convTypeToKind ty of
Just (v, k) -> let Result ds _ = anaKindM k $ classMap e in
if null ds then return (v, k) else Result ds Nothing
_ -> fail $ "not a kind '" ++ showDoc ty "'"
-- | local variable or type variable declaration
optAnaddVarDecl :: Bool -> VarDecl -> State Env (Maybe GenVarDecl)
optAnaddVarDecl warn vd@(VarDecl v t s q) =
let varDecl = do mvd <- anaVarDecl vd
Nothing -> return Nothing
let movd = makeMonomorph nvd
return $ Just $ GenVarDecl movd
let Result ds mk = convertTypeToKind e t
addDiags [mkDiag Hint "is type variable" v]
tv <- anaddTypeVarDecl $ TypeArg v vv (VarKind k) rStar 0 s q
return $ fmap GenTypeVarDecl tv
_ -> do addDiags $ map ( \ d -> Diag Hint (diagString d) q) ds
makeMonomorph :: VarDecl -> VarDecl
makeMonomorph (VarDecl v t sk ps) = VarDecl v (monoType t) sk ps
monoType = foldType mapTypeRec
{ foldTypeName = \ t i k n -> if n > 0 then TypeName i k 0 else t }
-- | analyse variable declaration
anaVarDecl :: VarDecl -> State Env (Maybe VarDecl)
anaVarDecl(VarDecl v oldT sk ps) =
do mt <- anaStarType oldT
Just t -> Just $ VarDecl v t sk ps