Symbol.hs revision 97ee7048e63953c5617342ce38c30cbcb35cc0be
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{- |
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederModule : $Header$
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederMaintainer : hets@tzi.de
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederStability : experimental
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederPortability : portable
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder HasCASL analysed symbols of a signature
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedermodule HasCASL.Symbol where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport HasCASL.Le
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport HasCASL.HToken
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport HasCASL.As
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport HasCASL.Unify
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport HasCASL.Merge
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Id
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Keywords
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Result
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.PrettyPrint
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Lib.Pretty
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Lib.State
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport qualified Common.Lib.Map as Map
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport qualified Common.Lib.Set as Set
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- new type to defined a different Eq and Ord instance
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata TySc = TySc TypeScheme deriving Show
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Eq TySc where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TySc sc1 == TySc sc2 =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let Result _ ms = mergeScheme Map.empty 0 sc1 sc2
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in maybe False (const True) ms
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Ord TySc where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- this does not match with Eq TypeScheme!
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TySc sc1 <= TySc sc2 =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TySc sc1 == TySc sc2 ||
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let (t1, c) = runState (freshInst sc1) 1
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder t2 = evalState (freshInst sc2) c
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder v1 = varsOf t1
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder v2 = varsOf t2
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in case compare (Set.size v1) $ Set.size v2 of
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder LT -> True
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder EQ -> t1 <= subst (Map.fromAscList $
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder zipWith (\ v (TypeArg i k _ _) ->
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder (v, TypeName i k 1))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (Set.toList v1) $ Set.toList v2) t2
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder GT -> False
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata SymbolType = OpAsItemType TypeScheme
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | TypeAsItemType Kind
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | ClassAsItemType Kind
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder deriving (Show, Eq, Ord)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata SyTy = OpAsITy TySc
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | TypeAsITy Kind
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder | ClassAsITy Kind
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder deriving (Show, Eq, Ord)
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder-- just for the Eq and Ord instances for Symbol
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedertoSyTy :: SymbolType -> SyTy
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedertoSyTy st = case st of
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder OpAsItemType sc -> OpAsITy $ TySc sc
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeAsItemType k -> TypeAsITy k
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ClassAsItemType k -> ClassAsITy k
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance PrettyPrint SymbolType where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder printText0 ga t = case t of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder OpAsItemType sc -> printText0 ga sc
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeAsItemType k -> printText0 ga k
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ClassAsItemType k -> printText0 ga k
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata Symbol = Symbol {symName :: Id, symType :: SymbolType, symEnv :: Env}
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder deriving Show
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Eq Symbol where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder s1 == s2 = (symName s1, toSyTy $ symType s1) ==
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (symName s2, toSyTy $ symType s2)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Ord Symbol where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder s1 <= s2 = (symName s1, toSyTy $ symType s1) <=
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (symName s2, toSyTy $ symType s2)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance PrettyPrint Symbol where
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder printText0 ga s = text (case symType s of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder OpAsItemType _ -> opS
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeAsItemType _ -> typeS
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ClassAsItemType _ -> classS) <+>
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder printText0 ga (symName s) <+> text colonS <+>
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder printText0 ga (symType s)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype SymbolMap = Map.Map Symbol Symbol
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype SymbolSet = Set.Set Symbol
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederidToTypeSymbol :: Env -> Id -> Kind -> Symbol
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederidToTypeSymbol e idt k = Symbol idt (TypeAsItemType k) e
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederidToClassSymbol :: Env -> Id -> Kind -> Symbol
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederidToClassSymbol e idt k = Symbol idt (ClassAsItemType k) e
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederidToOpSymbol :: Env -> Id -> TypeScheme -> Symbol
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederidToOpSymbol e idt typ = Symbol idt (OpAsItemType typ) e
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckSymbols :: SymbolSet -> SymbolSet -> Result a -> Result a
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckSymbols s1 s2 r =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let s = s1 Set.\\ s2 in
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder if Set.isEmpty s then r else
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder pfatal_error
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (ptext "unknown symbols: "
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder <+> printText s) $ posOfId $ symName $ Set.findMin s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederhideSymbol :: Symbol -> Env -> Env
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederhideSymbol sym sig =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let i = symName sym
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder tm = typeMap sig
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder as = assumps sig in
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder case symType sym of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ClassAsItemType _ -> sig
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeAsItemType _ -> sig { typeMap =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Map.delete i tm }
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder OpAsItemType ot ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let OpInfos os = Map.findWithDefault (OpInfos []) i as
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder rs = filter (not . isUnifiable tm 0 ot . opType) os
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in sig { assumps = if null rs then Map.delete i as
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder else Map.insert i (OpInfos rs) as }
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederplainHide :: SymbolSet -> Env -> Env
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederplainHide syms sigma =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let (opSyms, otherSyms) = Set.partition (\ sy -> case symType sy of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder OpAsItemType _ -> True
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder _ -> False) syms
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder in Set.fold hideSymbol (Set.fold hideSymbol sigma otherSyms) opSyms
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder-- | type ids within a type
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaedersubSyms :: Env -> Type -> SymbolSet
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian MaedersubSyms e t = case t of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeName i k n ->
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder if n == 0 then Set.single $ idToTypeSymbol e i k
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder else Set.empty
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder TypeAppl t1 t2 -> Set.union (subSyms e t1) (subSyms e t2)
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder KindedType tk _ _ -> subSyms e tk
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder LazyType tl _ -> subSyms e tl
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ProductType l _ -> Set.unions $ map (subSyms e) l
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder FunType t1 _ t2 _ -> Set.union (subSyms e t1) (subSyms e t2)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder _ -> error ("subSyms: " ++ show t)
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSymsOf :: Symbol -> SymbolSet
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSymsOf sy = case symType sy of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder OpAsItemType (TypeScheme _ (_ :=> ty) _) -> subSyms (symEnv sy) ty
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder _ -> Set.empty
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian MaedercloseSymbSet :: SymbolSet -> SymbolSet
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercloseSymbSet s = Set.unions (s : map subSymsOf (Set.toList s))
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersymOf :: Env -> SymbolSet
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersymOf sigma =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let classes = Map.foldWithKey ( \ i ks s ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Set.insert (Symbol i (ClassAsItemType $
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder Intersection (classKinds ks) []) sigma) s)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Set.empty $ classMap sigma
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder types = Map.foldWithKey ( \ i ti s ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Set.insert (Symbol i (TypeAsItemType $
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder typeKind ti) sigma) s)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder classes $ typeMap sigma
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ops = Map.foldWithKey ( \ i ts s0 ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder foldr ( \ t s1 ->
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder Set.insert (Symbol i (OpAsItemType $
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder opType t) sigma) s1) s0 $ opInfos ts)
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder types $ assumps sigma
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder in ops
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder