{- |

Module : $Header$

Copyright : (c) Christian Maeder and Uni Bremen 2003

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : experimental

Portability : portable

HasCASL analysed symbols of a signature

-}

module HasCASL.Symbol where

import HasCASL.Le

import HasCASL.PrintLe()

import HasCASL.As

import HasCASL.RawSym

import Common.Id

import Common.Result

import qualified Common.Lib.Map as Map

import qualified Common.Lib.Set as Set

instance PosItem Symbol where

get_pos = get_pos . symName

checkSymbols :: SymbolSet -> SymbolSet -> Result a -> Result a

checkSymbols s1 s2 r =

let s = foldr ( \ e2 d ->

Set.filter (not . matchSymb e2 . ASymbol) d)

s1 $ Set.toList s2 in

if Set.isEmpty s then r else

Result [mkDiag Error "unknown symbols" s] Nothing

dependentSyms :: Symbol -> Env -> SymbolSet

dependentSyms sym sig =

Set.fold ( \ op se ->

if Set.member sym $ subSymsOf op then

Set.insert op se else se) Set.empty $ symOf sig

hideRelSymbol :: Symbol -> Env -> Env

hideRelSymbol sym sig =

hideSymbol sym $ Set.fold hideSymbol sig $ dependentSyms sym sig

hideSymbol :: Symbol -> Env -> Env

hideSymbol sym sig =

let i = symName sym

tm = typeMap sig

as = assumps sig in

case symType sym of

ClassAsItemType _ -> sig

TypeAsItemType _ -> sig { typeMap =

Map.delete i tm }

OpAsItemType ot ->

let OpInfos os = Map.findWithDefault (OpInfos []) i as

rs = filter (not . (== ot) . opType) os

in sig { assumps = if null rs then Map.delete i as

else Map.insert i (OpInfos rs) as }

plainHide :: SymbolSet -> Env -> Env

plainHide syms sigma =

let (opSyms, otherSyms) = Set.partition (\ sy -> case symType sy of

OpAsItemType _ -> True

_ -> False) syms

in Set.fold hideSymbol (Set.fold hideSymbol sigma otherSyms) opSyms

-- | type ids within a type

subSyms :: Env -> Type -> SymbolSet

subSyms e t = case t of

TypeName i k n ->

if n == 0 then if i == unitTypeId then Set.empty

else Set.single $ idToTypeSymbol e i k

else Set.empty

TypeAppl t1 t2 -> Set.union (subSyms e t1) (subSyms e t2)

ExpandedType _ t1 -> subSyms e t1

KindedType tk _ _ -> subSyms e tk

LazyType tl _ -> subSyms e tl

ProductType l _ -> Set.unions $ map (subSyms e) l

FunType t1 _ t2 _ -> Set.union (subSyms e t1) (subSyms e t2)

_ -> error ("subSyms: " ++ show t)

subSymsOf :: Symbol -> SymbolSet

subSymsOf sy = case symType sy of

OpAsItemType (TypeScheme _ ty _) -> subSyms (symEnv sy) ty

_ -> Set.empty

closeSymbSet :: SymbolSet -> SymbolSet

closeSymbSet s = Set.unions (s : map subSymsOf (Set.toList s))

symOf :: Env -> SymbolSet

symOf sigma =

let classes = Map.foldWithKey ( \ i ks s ->

Set.insert (idToClassSymbol sigma i $

Intersection (classKinds ks) []) s)

Set.empty $ classMap sigma

types = Map.foldWithKey ( \ i ti s ->

Set.insert (idToTypeSymbol sigma i $

typeKind ti) s)

classes $ typeMap sigma

ops = Map.foldWithKey ( \ i ts s0 ->

foldr ( \ t s1 ->

Set.insert (idToOpSymbol sigma i $

opType t) s1) s0 $ opInfos ts)

types $ assumps sigma

in ops