{- |
Module      :  ./HasCASL/Symbol.hs
Description :  symbol analysis
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.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.AsUtils
import HasCASL.Builtin
import HasCASL.RawSym

import Common.Id
import Common.Result

import qualified Data.Map as Map
import qualified Data.Set as Set

instance GetRange Symbol where
    getRange :: Symbol -> Range
getRange = Id -> Range
forall a. GetRange a => a -> Range
getRange (Id -> Range) -> (Symbol -> Id) -> Symbol -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Id
symName

checkSymbols :: SymbolSet -> SymbolSet -> Result a -> Result a
checkSymbols :: SymbolSet -> SymbolSet -> Result a -> Result a
checkSymbols s1 :: SymbolSet
s1 s2 :: SymbolSet
s2 r :: Result a
r =
    let s :: SymbolSet
s = (Symbol -> SymbolSet -> SymbolSet)
-> SymbolSet -> [Symbol] -> SymbolSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ e2 :: Symbol
e2 ->
                 (Symbol -> Bool) -> SymbolSet -> SymbolSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> RawSymbol -> Bool
matchSymb Symbol
e2 (RawSymbol -> Bool) -> (Symbol -> RawSymbol) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> RawSymbol
ASymbol))
                  SymbolSet
s1 ([Symbol] -> SymbolSet) -> [Symbol] -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet -> [Symbol]
forall a. Set a -> [a]
Set.toList SymbolSet
s2 in
    if SymbolSet -> Bool
forall a. Set a -> Bool
Set.null SymbolSet
s then Result a
r else
       [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SymbolSet -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown HasCASL symbols" SymbolSet
s] Maybe a
forall a. Maybe a
Nothing

dependentSyms :: Symbol -> Env -> SymbolSet
dependentSyms :: Symbol -> Env -> SymbolSet
dependentSyms sym :: Symbol
sym =
    (Symbol -> SymbolSet -> SymbolSet)
-> SymbolSet -> SymbolSet -> SymbolSet
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ op :: Symbol
op se :: SymbolSet
se ->
               if Symbol -> SymbolSet -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
sym (SymbolSet -> Bool) -> SymbolSet -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbolSet
subSymsOf Symbol
op then
               Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
op SymbolSet
se else SymbolSet
se) SymbolSet
forall a. Set a
Set.empty (SymbolSet -> SymbolSet) -> (Env -> SymbolSet) -> Env -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SymbolSet] -> SymbolSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([SymbolSet] -> SymbolSet)
-> (Env -> [SymbolSet]) -> Env -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> [SymbolSet]
symOf

hideRelSymbol :: Symbol -> Env -> Env
hideRelSymbol :: Symbol -> Env -> Env
hideRelSymbol sym :: Symbol
sym sig :: Env
sig =
    Symbol -> Env -> Env
hideSymbol Symbol
sym (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ (Symbol -> Env -> Env) -> Env -> SymbolSet -> Env
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Env -> Env
hideSymbol Env
sig (SymbolSet -> Env) -> SymbolSet -> Env
forall a b. (a -> b) -> a -> b
$ Symbol -> Env -> SymbolSet
dependentSyms Symbol
sym Env
sig


hideSymbol :: Symbol -> Env -> Env
hideSymbol :: Symbol -> Env -> Env
hideSymbol sym :: Symbol
sym sig :: Env
sig =
    let i :: Id
i = Symbol -> Id
symName Symbol
sym
        cm :: ClassMap
cm = Env -> ClassMap
classMap Env
sig
        tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
sig
        as :: Assumps
as = Env -> Assumps
assumps Env
sig in
    case Symbol -> SymbolType
symType Symbol
sym of
    ClassAsItemType _ -> Env
sig
      { classMap :: ClassMap
classMap = (ClassInfo -> ClassInfo) -> ClassMap -> ClassMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
        (\ ci :: ClassInfo
ci -> ClassInfo
ci { classKinds :: Set Kind
classKinds = (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
                      (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Id
i (Set Id -> Bool) -> (Kind -> Set Id) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Set Id
idsOfKind) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
ci })
        (ClassMap -> ClassMap) -> ClassMap -> ClassMap
forall a b. (a -> b) -> a -> b
$ Id -> ClassMap -> ClassMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i ClassMap
cm
      , typeMap :: TypeMap
typeMap = (TypeInfo -> TypeInfo) -> TypeMap -> TypeMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
        (\ ti :: TypeInfo
ti -> TypeInfo
ti { otherTypeKinds :: Set Kind
otherTypeKinds = (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
                      (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Id
i (Set Id -> Bool) -> (Kind -> Set Id) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Set Id
idsOfKind) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti })
        TypeMap
tm }
    TypeAsItemType _ -> Env
sig
      { typeMap :: TypeMap
typeMap = (TypeInfo -> TypeInfo) -> TypeMap -> TypeMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
        (\ ti :: TypeInfo
ti -> TypeInfo
ti { superTypes :: Set Id
superTypes = Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.delete Id
i (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti })
        (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
$ Id -> TypeMap -> TypeMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i TypeMap
tm }
    OpAsItemType ot :: TypeScheme
ot ->
        let os :: Set OpInfo
os = Set OpInfo -> Id -> Assumps -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty Id
i Assumps
as
            rs :: Set OpInfo
rs = (OpInfo -> Bool) -> Set OpInfo -> Set OpInfo
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeScheme
ot) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType) Set OpInfo
os
        in Env
sig { assumps :: Assumps
assumps = if Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null Set OpInfo
rs then Id -> Assumps -> Assumps
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i Assumps
as
                          else Id -> Set OpInfo -> Assumps -> Assumps
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Set OpInfo
rs Assumps
as }
    _ -> Env
sig

idsOfKind :: Kind -> Set.Set Id
idsOfKind :: Kind -> Set Id
idsOfKind kd :: Kind
kd = case Kind
kd of
  ClassKind i :: Id
i -> Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i
  FunKind _ k1 :: Kind
k1 k2 :: Kind
k2 _ -> Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Kind -> Set Id
idsOfKind Kind
k1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Kind -> Set Id
idsOfKind Kind
k2

plainHide :: SymbolSet -> Env -> Env
plainHide :: SymbolSet -> Env -> Env
plainHide syms :: SymbolSet
syms sigma :: Env
sigma =
    let (opSyms :: SymbolSet
opSyms, otherSyms :: SymbolSet
otherSyms) = (Symbol -> Bool) -> SymbolSet -> (SymbolSet, SymbolSet)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (\ sy :: Symbol
sy -> case Symbol -> SymbolType
symType Symbol
sy of
                                              OpAsItemType _ -> Bool
True
                                              _ -> Bool
False) SymbolSet
syms
    in (Symbol -> Env -> Env) -> Env -> SymbolSet -> Env
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Env -> Env
hideSymbol ((Symbol -> Env -> Env) -> Env -> SymbolSet -> Env
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Env -> Env
hideSymbol Env
sigma SymbolSet
otherSyms) SymbolSet
opSyms

-- | type ids within a type
subSyms :: Type -> SymbolSet
subSyms :: Type -> SymbolSet
subSyms t :: Type
t = case Type
t of
           TypeName i :: Id
i k :: RawKind
k n :: Int
n ->
               if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId Bool -> Bool -> Bool
|| Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId Bool -> Bool -> Bool
||
                 Id -> Bool
isArrow Id
i Bool -> Bool -> Bool
|| Id -> Bool
isProductId Id
i then SymbolSet
forall a. Set a
Set.empty
                  else Symbol -> SymbolSet
forall a. a -> Set a
Set.singleton (Symbol -> SymbolSet) -> Symbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToTypeSymbol Id
i RawKind
k
               else SymbolSet
forall a. Set a
Set.empty
           TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> SymbolSet -> SymbolSet -> SymbolSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Type -> SymbolSet
subSyms Type
t1) (Type -> SymbolSet
subSyms Type
t2)
           ExpandedType _ t1 :: Type
t1 -> Type -> SymbolSet
subSyms Type
t1
           KindedType tk :: Type
tk _ _ -> Type -> SymbolSet
subSyms Type
tk
           TypeAbs _ b :: Type
b _ -> Type -> SymbolSet
subSyms Type
b
           _ -> String -> SymbolSet
forall a. HasCallStack => String -> a
error ("subSyms: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t)

subSymsOf :: Symbol -> SymbolSet
subSymsOf :: Symbol -> SymbolSet
subSymsOf sy :: Symbol
sy = case Symbol -> SymbolType
symType Symbol
sy of
     OpAsItemType (TypeScheme _ ty :: Type
ty _) -> Type -> SymbolSet
subSyms Type
ty
     _ -> SymbolSet
forall a. Set a
Set.empty

closeSymbSet :: SymbolSet -> SymbolSet
closeSymbSet :: SymbolSet -> SymbolSet
closeSymbSet s :: SymbolSet
s = [SymbolSet] -> SymbolSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (SymbolSet
s SymbolSet -> [SymbolSet] -> [SymbolSet]
forall a. a -> [a] -> [a]
: (Symbol -> SymbolSet) -> [Symbol] -> [SymbolSet]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> SymbolSet
subSymsOf (SymbolSet -> [Symbol]
forall a. Set a -> [a]
Set.toList SymbolSet
s))

opSymOf :: Env -> SymbolSet
opSymOf :: Env -> SymbolSet
opSymOf sigma :: Env
sigma = (Id -> Set OpInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> Assumps -> SymbolSet
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ts :: Set OpInfo
ts s :: SymbolSet
s ->
                      if Id -> Assumps -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i Assumps
bOps then SymbolSet
s else
                      (OpInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> Set OpInfo -> SymbolSet
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> SymbolSet -> SymbolSet)
-> (OpInfo -> Symbol) -> OpInfo -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TypeScheme -> Symbol
idToOpSymbol Id
i (TypeScheme -> Symbol)
-> (OpInfo -> TypeScheme) -> OpInfo -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType)
                         SymbolSet
s Set OpInfo
ts)
              SymbolSet
forall a. Set a
Set.empty (Assumps -> SymbolSet) -> Assumps -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
sigma

symOf :: Env -> [SymbolSet]
symOf :: Env -> [SymbolSet]
symOf sigma :: Env
sigma =
    let classes :: SymbolSet
classes = (Id -> ClassInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> ClassMap -> SymbolSet
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ->
                          Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> SymbolSet -> SymbolSet)
-> (ClassInfo -> Symbol) -> ClassInfo -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> RawKind -> Symbol
idToClassSymbol Id
i (RawKind -> Symbol)
-> (ClassInfo -> RawKind) -> ClassInfo -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassInfo -> RawKind
rawKind)
                  SymbolSet
forall a. Set a
Set.empty (ClassMap -> SymbolSet) -> ClassMap -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
sigma
        types :: SymbolSet
types = (Id -> TypeInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> TypeMap -> SymbolSet
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ti :: TypeInfo
ti ->
                        if Id -> TypeMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i TypeMap
bTypes then SymbolSet -> SymbolSet
forall a. a -> a
id else
                        Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> SymbolSet -> SymbolSet)
-> Symbol -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToTypeSymbol Id
i (RawKind -> Symbol) -> RawKind -> Symbol
forall a b. (a -> b) -> a -> b
$ TypeInfo -> RawKind
typeKind TypeInfo
ti)
                SymbolSet
forall a. Set a
Set.empty (TypeMap -> SymbolSet) -> TypeMap -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
sigma
        ops :: SymbolSet
ops = (Id -> Set OpInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> Assumps -> SymbolSet
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ts :: Set OpInfo
ts s :: SymbolSet
s ->
                      if Id -> Assumps -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i Assumps
bOps then SymbolSet
s else
                      (OpInfo -> SymbolSet -> SymbolSet)
-> SymbolSet -> Set OpInfo -> SymbolSet
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Symbol -> SymbolSet -> SymbolSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> SymbolSet -> SymbolSet)
-> (OpInfo -> Symbol) -> OpInfo -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TypeScheme -> Symbol
idToOpSymbol Id
i (TypeScheme -> Symbol)
-> (OpInfo -> TypeScheme) -> OpInfo -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType)
                         SymbolSet
s Set OpInfo
ts)
              SymbolSet
forall a. Set a
Set.empty (Assumps -> SymbolSet) -> Assumps -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
sigma
        in [SymbolSet
classes, SymbolSet
types, SymbolSet
ops]