VarDecl.hs revision 4d5d65e4f55ba8eaa02a4dab14348abeda75cf6b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- |
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichMaintainer : maeder@tzi.de
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiStability : provisional
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiPortability : non-portable (MonadState)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskianalyse generic var (or type var) decls
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski-}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimodule HasCASL.VarDecl where
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Data.Maybe
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Data.List as List
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Control.Monad
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Common.Lib.Map as Map
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Common.Lib.Set as Set
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Common.Id
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Common.AS_Annotation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimport Common.Lib.State
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Common.Result
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Common.PrettyPrint
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Common.Lexer
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimport Common.AnnoState
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Text.ParserCombinators.Parsec hiding (State)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.ParseTerm
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.As
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.Le
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.ClassAna
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.TypeAna
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.Unify
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.Merge
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport HasCASL.Builtin
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski-- | add diagnostic messages
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiaddDiags :: [Diagnosis] -> State Env ()
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiaddDiags ds =
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski do e <- get
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski put $ e {envDiags = reverse ds ++ envDiags e}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski-- | add sentences
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiappendSentences :: [Named Sentence] -> State Env ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiappendSentences fs =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do e <- get
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski put $ e {sentences = reverse fs ++ sentences e}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | store local assumptions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputLocalVars :: Map.Map Id Type -> State Env ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputLocalVars vs = do { e <- get; put e { localVars = vs } }
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaStarType :: Type -> State Env (Maybe Type)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaStarType t = do mp <- fromResult $ anaStarTypeR t . typeMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return $ fmap snd mp
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaInstTypes :: [Type] -> State Env [Type]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaInstTypes ts = if null ts then return []
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski else do mp <- fromResult $ anaType (Nothing, head ts) . typeMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski rs <- anaInstTypes $ tail ts
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return $ case mp of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Nothing -> rs
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Just (_, ty) -> ty:rs
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaTypeScheme (TypeScheme tArgs ty p) =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do tm <- gets typeMap -- save global variables
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski mArgs <- mapM anaddTypeVarDecl tArgs
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski let newArgs = catMaybes mArgs
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange mt <- anaStarType ty
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski putTypeMap tm -- forget local variables
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case mt of
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange Nothing -> return Nothing
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange Just newTy -> do
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange let newSc = TypeScheme newArgs newTy p
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange gTy <- if null newArgs then return $ generalize newSc
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange else generalizeS newSc
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange return $ Just gTy
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph LangegeneralizeS :: TypeScheme -> State Env TypeScheme
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph LangegeneralizeS sc = do
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange addDiags $ generalizable sc
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange return $ generalize sc
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaKind :: Kind -> State Env Kind
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaKind k = toState star $ anaKindM k
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskitoState :: a -> (Env -> Result a) -> State Env a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskitoState bot r = do
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ma <- fromResult r
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case ma of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Nothing -> return bot
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Just a -> return a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromResult :: (Env -> Result a) -> State Env (Maybe a)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromResult f = do
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski e <- get
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski let r = f e
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski addDiags $ diags r
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return $ maybeResult r
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- ---------------------------------------------------------------------------
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- storing type ids with their kind and definition
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- ---------------------------------------------------------------------------
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | store a complete type map
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputTypeMap :: TypeMap -> State Env ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputTypeMap tk = do { e <- get; put e { typeMap = tk } }
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | store type id and check kind arity (warn on redeclared types)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeId :: Bool -> TypeDefn -> Instance -> Kind -> Id -> State Env (Maybe Id)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeId warn defn _ k i =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do let nk = rawKind k
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski if placeCount i <= kindArity TopLevel nk then
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do addTypeKind warn defn i k
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return $ Just i
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski else do addDiags [mkDiag Error "wrong arity of" i]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return Nothing
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | store type as is (warn on redeclared types)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeKind warn d i k =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do tk <- gets typeMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski let rk = rawKind k
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case Map.lookup i tk of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Nothing -> case d of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski TypeVarDefn _ -> do
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (_, v) <- toEnvState $ freshVar (posOfId i)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski putTypeMap $ Map.insert i
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (TypeInfo rk [k] [] $ TypeVarDefn v) tk
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski _ -> putTypeMap $ Map.insert i (TypeInfo rk [k] [] d) tk
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Just (TypeInfo ok ks sups defn) ->
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski if rk == ok
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski then do let isKnownInst = k `elem` ks
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski insts = if isKnownInst then ks else
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Set.toList $ mkIntersection (k:ks)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Result ds mDef = mergeTypeDefn defn d
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski if warn && isKnownInst && case (defn, d) of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (PreDatatype, DatatypeDefn _) -> False
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski _ -> True
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski then
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski addDiags [mkDiag Hint
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski "redeclared type" i]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski else return ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case mDef of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Just newDefn -> putTypeMap $ Map.insert i
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (TypeInfo ok insts sups newDefn) tk
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Nothing -> addDiags $ map (improveDiag i) ds
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski else addDiags $ diffKindDiag i ok rk
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | analyse a type argument and look up a missing kind
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaddTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskianaddTypeVarDecl(TypeArg t k s ps) =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case k of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski MissingKind -> do
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski tk <- gets typeMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski let rm = getIdKind tk t
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case maybeResult rm of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Nothing -> anaddTypeVarDecl(TypeArg t star s ps)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Just oldK -> addTypeVarDecl False (TypeArg t oldK s ps)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski _ -> do nk <- anaKind k
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski addTypeVarDecl True $ TypeArg t nk s ps
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | add an analysed type argument (warn on redeclared types)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeVarDecl :: Bool -> TypeArg -> State Env (Maybe TypeArg)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiaddTypeVarDecl warn ta@(TypeArg t k _ _) =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski do mi <- addTypeId warn (TypeVarDefn 0) Plain k t
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski return $ fmap (const ta) mi
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | compute arity from a 'Kind'
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskikindArity :: ApplMode -> Kind -> Int
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskikindArity m k =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski case k of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski FunKind k1 k2 _ -> case m of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski TopLevel -> kindArity OnlyArg k1 +
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski kindArity TopLevel k2
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski OnlyArg -> 1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Intersection [] _ -> case m of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski TopLevel -> 0
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder OnlyArg -> 1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ClassKind _ ck -> kindArity m ck
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Downset _ _ dk _ -> kindArity m dk
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Intersection (k1:_) _ -> kindArity m k1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ExtKind ek _ _ -> kindArity m ek
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski _ -> error "kindArity"
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- ---------------------------------------------------------------------------
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- for storing selectors and constructors
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- ---------------------------------------------------------------------------
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | store assumptions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputAssumps :: Assumps -> State Env ()
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiputAssumps as = do { e <- get; put e { assumps = as } }
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | get matching information of uninstantiated identifier
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifindOpId :: Env -> UninstOpId -> TypeScheme -> Maybe OpInfo
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifindOpId e i sc = listToMaybe $ fst $ partitionOpId e i sc
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | partition information of an uninstantiated identifier
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskipartitionOpId :: Env -> UninstOpId -> TypeScheme -> ([OpInfo], [OpInfo])
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskipartitionOpId e i sc =
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski let l = Map.findWithDefault (OpInfos []) i $ assumps e
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski in partition (isUnifiable (typeMap e) (counter e) sc . opType) $ opInfos l
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder
30256573a343132354b122097b0ee1215dda1364Till MossakowskicheckUnusedTypevars :: TypeScheme -> State Env TypeScheme
30256573a343132354b122097b0ee1215dda1364Till MossakowskicheckUnusedTypevars sc@(TypeScheme tArgs t ps) = do
30256573a343132354b122097b0ee1215dda1364Till Mossakowski let ls = map snd $ leaves (< 0) t -- generic vars
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski rest = tArgs List.\\ ls
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski if null rest then return sc
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski else do
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski addDiags [mkDiag Warning "unused type variables" rest]
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski return $ TypeScheme ls t ps
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | storing an operation
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiaddOpId :: UninstOpId -> TypeScheme -> [OpAttr] -> OpDefn
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski -> State Env (Maybe UninstOpId)
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiaddOpId i oldSc attrs defn =
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski do sc <- checkUnusedTypevars oldSc
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski e <- get
30256573a343132354b122097b0ee1215dda1364Till Mossakowski let as = assumps e
30256573a343132354b122097b0ee1215dda1364Till Mossakowski tm = typeMap e
30256573a343132354b122097b0ee1215dda1364Till Mossakowski TypeScheme _ ty _ = sc
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ds = if placeCount i > 1 then case unalias ty of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski FunType arg _ _ _ -> case unalias arg of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ProductType ts _ -> if placeCount i /= length ts then
30256573a343132354b122097b0ee1215dda1364Till Mossakowski [mkDiag Error "wrong number of places in" i]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else []
30256573a343132354b122097b0ee1215dda1364Till Mossakowski _ -> [mkDiag Error "expected tuple argument for" i]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski _ -> [mkDiag Error "expected function type for" i]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else []
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (l, r) = partitionOpId e i sc
30256573a343132354b122097b0ee1215dda1364Till Mossakowski oInfo = OpInfo sc attrs defn
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if null ds then
30256573a343132354b122097b0ee1215dda1364Till Mossakowski do let Result es mo = foldM (mergeOpInfo tm) oInfo l
30256573a343132354b122097b0ee1215dda1364Till Mossakowski addDiags $ map (improveDiag i) es
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if i `elem` map fst bList then addDiags $ [mkDiag Warning
30256573a343132354b122097b0ee1215dda1364Till Mossakowski "ignoring declaration for builtin identifier" i]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else return ()
30256573a343132354b122097b0ee1215dda1364Till Mossakowski case mo of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Nothing -> return Nothing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Just oi -> do putAssumps $ Map.insert i
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (OpInfos (oi : r)) as
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ Just i
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else do addDiags ds
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return Nothing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski----------------------------------------------------------------------------
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- local variables
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-----------------------------------------------------------------------------
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | add a local variable with an analysed type (if True then warn)
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddLocalVar :: Bool -> VarDecl -> State Env ()
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddLocalVar b (VarDecl v t _ _) =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski do ass <- gets assumps
30256573a343132354b122097b0ee1215dda1364Till Mossakowski vs <- gets localVars
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if b then if Map.member v ass then
30256573a343132354b122097b0ee1215dda1364Till Mossakowski addDiags [mkDiag Hint "variable shadows global name(s)" v]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else if Map.member v vs then
30256573a343132354b122097b0ee1215dda1364Till Mossakowski addDiags [mkDiag Hint "shadowing by variable" v]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else return ()
3952a5c632e9e4ed036aa2eb378b9ef86070ca6dChristoph Lange else return ()
30256573a343132354b122097b0ee1215dda1364Till Mossakowski putLocalVars $ Map.insert v t vs
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | add a local variable with an analysed type
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddGenLocalVar :: GenVarDecl -> State Env ()
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddGenLocalVar d = case d of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski GenVarDecl v -> addLocalVar False v
30256573a343132354b122097b0ee1215dda1364Till Mossakowski GenTypeVarDecl t -> addTypeVarDecl False t >> return ()
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski----------------------------------------------------------------------------
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- GenVarDecl
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-----------------------------------------------------------------------------
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddGenVarDecl :: GenVarDecl -> State Env (Maybe GenVarDecl)
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddGenVarDecl(GenVarDecl v) = do mv <- addVarDecl v
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ fmap GenVarDecl mv
30256573a343132354b122097b0ee1215dda1364Till MossakowskiaddGenVarDecl(GenTypeVarDecl t) = do mt <- addTypeVarDecl True t
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ fmap GenTypeVarDecl mt
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | analyse and add global (True) or local variable or type declaration
30256573a343132354b122097b0ee1215dda1364Till MossakowskianaddGenVarDecl :: Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
3952a5c632e9e4ed036aa2eb378b9ef86070ca6dChristoph LangeanaddGenVarDecl b gv = case gv of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski GenVarDecl v -> optAnaddVarDecl b v
30256573a343132354b122097b0ee1215dda1364Till Mossakowski GenTypeVarDecl t -> anaddTypeVarDecl t >>= (return . fmap GenTypeVarDecl)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till MossakowskiconvertTypeToKind :: Env -> Type -> Result Kind
30256573a343132354b122097b0ee1215dda1364Till MossakowskiconvertTypeToKind e ty = let s = showPretty ty "" in
30256573a343132354b122097b0ee1215dda1364Till Mossakowski case runParser (extKind << eof) (emptyAnnos ()) "" s of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Right k -> anaKindM k e
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Left _ -> fail $ "not a kind '" ++ s ++ "'"
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | add global or local variable or type declaration (True means global)
30256573a343132354b122097b0ee1215dda1364Till MossakowskioptAnaddVarDecl :: Bool -> VarDecl -> State Env (Maybe GenVarDecl)
30256573a343132354b122097b0ee1215dda1364Till MossakowskioptAnaddVarDecl b vd@(VarDecl v t s q) =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski let varDecl = do mvd <- anaVarDecl vd
30256573a343132354b122097b0ee1215dda1364Till Mossakowski case mvd of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Nothing -> return Nothing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Just nvd -> let movd = makeMonomorph nvd in
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if b then do
30256573a343132354b122097b0ee1215dda1364Till Mossakowski mmvd <- addVarDecl movd
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ fmap GenVarDecl mmvd
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else do
30256573a343132354b122097b0ee1215dda1364Till Mossakowski addLocalVar True movd
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ Just $ GenVarDecl movd
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in if isSimpleId v then
30256573a343132354b122097b0ee1215dda1364Till Mossakowski do e <- get
30256573a343132354b122097b0ee1215dda1364Till Mossakowski let Result ds mk = convertTypeToKind e t
30256573a343132354b122097b0ee1215dda1364Till Mossakowski case mk of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Just k -> do
30256573a343132354b122097b0ee1215dda1364Till Mossakowski addDiags [mkDiag Hint "is type variable" v]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski tv <- anaddTypeVarDecl $ TypeArg v k s q
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ fmap GenTypeVarDecl tv
30256573a343132354b122097b0ee1215dda1364Till Mossakowski _ -> do addDiags $ map ( \ d -> Diag Hint (diagString d) q) ds
30256573a343132354b122097b0ee1215dda1364Till Mossakowski varDecl
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else varDecl
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till MossakowskimakeMonomorph :: VarDecl -> VarDecl
30256573a343132354b122097b0ee1215dda1364Till MossakowskimakeMonomorph (VarDecl v t sk ps) = VarDecl v (monoType t) sk ps
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till MossakowskimonoType :: Type -> Type
30256573a343132354b122097b0ee1215dda1364Till MossakowskimonoType t = subst (Map.fromList $
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map ( \ (v, TypeArg i k _ _) ->
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (v, TypeName i k 0)) $ leaves (> 0) t) t
30256573a343132354b122097b0ee1215dda1364Till Mossakowski
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | analyse variable declaration
30256573a343132354b122097b0ee1215dda1364Till MossakowskianaVarDecl :: VarDecl -> State Env (Maybe VarDecl)
30256573a343132354b122097b0ee1215dda1364Till MossakowskianaVarDecl(VarDecl v oldT sk ps) =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski do mt <- anaStarType oldT
30256573a343132354b122097b0ee1215dda1364Till Mossakowski return $ case mt of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Nothing -> Nothing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Just t -> Just $ VarDecl v t sk ps
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder-- | add a local variable with an analysed type
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaederaddVarDecl :: VarDecl -> State Env (Maybe VarDecl)
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaederaddVarDecl vd@(VarDecl v t _ _) =
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder do newV <- addOpId v (simpleTypeScheme t) [] VarDefn
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder return $ fmap (const vd) newV
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder-- | get the variable
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaedergetVar :: VarDecl -> Id
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaedergetVar(VarDecl v _ _ _) = v
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder-- | check uniqueness of variables
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaedercheckUniqueVars :: [VarDecl] -> State Env ()
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen KuksacheckUniqueVars = addDiags . checkUniqueness . map getVar
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- | filter out assumption
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen KuksafilterAssumps :: (OpInfo -> Bool) -> Assumps -> Assumps
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen KuksafilterAssumps p =
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa Map.filter (not . null . opInfos) .
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa Map.map (OpInfos . filter p . opInfos)
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski-- | analyse types in typed patterns, and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski-- create fresh type vars for unknown ids tagged with type MixfixType [].
a17349d0247036407c22e632ece0e8f2b736253cTill MossakowskianaPattern :: Pattern -> State Env Pattern
a17349d0247036407c22e632ece0e8f2b736253cTill MossakowskianaPattern pat =
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski case pat of
3952a5c632e9e4ed036aa2eb378b9ef86070ca6dChristoph Lange QualVar vd -> do newVd <- checkVarDecl vd
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ QualVar newVd
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski ResolvedMixTerm i pats ps -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski l <- mapM anaPattern pats
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ ResolvedMixTerm i l ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski ApplTerm p1 p2 ps -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski p3 <- anaPattern p1
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski p4 <- anaPattern p2
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ ApplTerm p3 p4 ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski TupleTerm pats ps -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski l <- mapM anaPattern pats
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ TupleTerm l ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski TypedTerm p q ty ps -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski mt <- anaStarType ty
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski let newT = case mt of Just t -> t
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski _ -> ty
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski case p of
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski QualVar (VarDecl v (MixfixType []) ok qs) ->
3952a5c632e9e4ed036aa2eb378b9ef86070ca6dChristoph Lange let newVd = VarDecl v newT ok (qs ++ ps) in
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ QualVar newVd
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski _ -> do newP <- anaPattern p
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ TypedTerm newP q newT ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski AsPattern vd p2 ps -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski newVd <- checkVarDecl vd
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski p4 <- anaPattern p2
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ AsPattern newVd p4 ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski _ -> return pat
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski where checkVarDecl vd@(VarDecl v t ok ps) = case t of
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski MixfixType [] -> do
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski (tvar, c) <- toEnvState $ freshVar $ posOfId v
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski return $ VarDecl v (TypeName tvar star c) ok ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski _ -> do mt <- anaStarType t
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski case mt of
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Just ty -> return $ VarDecl v ty ok ps
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski _ -> return vd
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski