{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./HasCASL/Le.hs
Description :  the abstract syntax for analysis and final signature instance
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

abstract syntax during static analysis
-}

module HasCASL.Le where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.AsUtils

import qualified Common.Lib.State as State
import Common.Result
import Common.Id
import Common.AS_Annotation (Named)
import Common.GlobalAnnotations
import Common.Prec

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

-- * class info

-- | store the raw kind and all superclasses of a class identifier
data ClassInfo = ClassInfo
    { rawKind :: RawKind
    , classKinds :: Set.Set Kind
    } deriving (Show, Eq, Ord, Typeable, Data)

-- | mapping class identifiers to their definition
type ClassMap = Map.Map Id ClassInfo

-- * type info

-- | data type generatedness indicator
data GenKind = Free | Generated | Loose deriving (Show, Eq, Ord, Typeable, Data)

-- | an analysed alternative with a list of (product) types
data AltDefn =
    Construct (Maybe Id) [Type] Partiality [[Selector]]
    -- only argument types
    deriving (Show, Eq, Ord, Typeable, Data)

-- | an analysed component
data Selector =
    Select (Maybe Id) Type Partiality deriving (Show, Eq, Ord, Typeable, Data)
    -- only result type

-- | a mapping of type (and disjoint class) identifiers
type IdMap = Map.Map Id Id

{- | data entries are produced from possibly mutual recursive data types. The
top-level identifiers of these types are never renamed but there renaming is
stored in the identifier map. This identifier map must never be empty (even
without renamings) because (the domain of) this map is used to store the
other (recursively dependent) top-level identifiers. -}
data DataEntry =
    DataEntry IdMap Id GenKind [TypeArg] RawKind (Set.Set AltDefn)
    deriving (Show, Eq, Ord, Typeable, Data)

-- | possible definitions for type identifiers
data TypeDefn =
    NoTypeDefn
  | PreDatatype     -- auxiliary entry for DatatypeDefn
  | DatatypeDefn DataEntry
  | AliasTypeDefn Type
    deriving (Show, Eq, Ord, Typeable, Data)

-- | for type identifiers also store the raw kind, instances and supertypes
data TypeInfo = TypeInfo
    { typeKind :: RawKind
    , otherTypeKinds :: Set.Set Kind
    , superTypes :: Set.Set Id -- only declared or direct supertypes?
    , typeDefn :: TypeDefn
    } deriving (Show, Typeable, Data)

instance Eq TypeInfo where
    a == b = compare a b == EQ

instance Ord TypeInfo where
   compare t1 t2 = compare
     (typeKind t1, otherTypeKinds t1, superTypes t1)
     (typeKind t2, otherTypeKinds t2, superTypes t2)

-- | mapping type identifiers to their definition
type TypeMap = Map.Map Id TypeInfo

-- | the minimal information for a sort
starTypeInfo :: TypeInfo
starTypeInfo = TypeInfo rStar (Set.singleton universe) Set.empty NoTypeDefn

-- | rename the type according to identifier map (for comorphisms)
mapType :: IdMap -> Type -> Type
mapType m = if Map.null m then id else
    foldType mapTypeRec
    { foldTypeName = \ t i k n -> if n /= 0 then t else
        case Map.lookup i m of
          Just j -> TypeName j k 0
          Nothing -> t }

-- * sentences

-- | data types are also special sentences because of their properties
data Sentence =
    Formula Term
  | DatatypeSen [DataEntry]
  | ProgEqSen Id TypeScheme ProgEq
    deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange Sentence where
  getRange s = case s of
    Formula t -> getRange t
    _ -> nullRange

-- * variables

-- | type variable are kept separately
data TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int
  deriving (Show, Typeable, Data)

-- | mapping type variables to their definition
type LocalTypeVars = Map.Map Id TypeVarDefn

-- | the type of a local variable
data VarDefn = VarDefn Type deriving (Show, Typeable, Data)

-- * assumptions

-- | name and scheme of a constructor
data ConstrInfo = ConstrInfo
    { constrId :: Id
    , constrType :: TypeScheme
    } deriving (Show, Eq, Ord, Typeable, Data)

-- | possible definitions of functions
data OpDefn =
    NoOpDefn OpBrand
  | ConstructData Id     -- ^ target type
  | SelectData (Set.Set ConstrInfo) Id   -- ^ constructors of source type
  | Definition OpBrand Term
    deriving (Show, Eq, Ord, Typeable, Data)

-- | scheme, attributes and definition for function identifiers
data OpInfo = OpInfo
    { opType :: TypeScheme
    , opAttrs :: Set.Set OpAttr
    , opDefn :: OpDefn
    } deriving (Show, Typeable, Data)

instance Eq OpInfo where
    o1 == o2 = compare o1 o2 == EQ

instance Ord OpInfo where
    compare = comparing opType

-- | test for constructor
isConstructor :: OpInfo -> Bool
isConstructor o = case opDefn o of
    ConstructData _ -> True
    _ -> False

-- | mapping operation identifiers to their definition
type Assumps = Map.Map Id (Set.Set OpInfo)

-- * the local environment and final signature

-- | the signature is established by the classes, types and assumptions
data Env = Env
    { classMap :: ClassMap
    , typeMap :: TypeMap
    , localTypeVars :: LocalTypeVars
    , assumps :: Assumps
    , binders :: Map.Map Id Id -- binder with associated op-id
    , localVars :: Map.Map Id VarDefn
    , sentences :: [Named Sentence]
    , declSymbs :: Set.Set Symbol
    , envDiags :: [Diagnosis]
    , preIds :: (PrecMap, Set.Set Id)
    , globAnnos :: GlobalAnnos
    , counter :: Int
    } deriving (Show, Typeable, Data)

instance Eq Env where
    a == b = compare a b == EQ

instance Ord Env where
  compare e1 e2 = compare
    (classMap e1, typeMap e1, assumps e1)
    (classMap e2, typeMap e2, assumps e2)

-- | the empty environment (fresh variables start with 1)
initialEnv :: Env
initialEnv = Env
    { classMap = Map.empty
    , typeMap = Map.empty
    , localTypeVars = Map.empty
    , assumps = Map.empty
    , binders = Map.empty
    , localVars = Map.empty
    , sentences = []
    , declSymbs = Set.empty
    , envDiags = []
    , preIds = (emptyPrecMap, Set.empty)
    , globAnnos = emptyGlobalAnnos
    , counter = 1 }

{- utils for singleton sets that could also be part of "Data.Set". These
functions rely on 'Data.Set.size' being computable in constant time and
would need to be rewritten for set implementations with a size
function that is only linear. -}

data Constrain = Kinding Type Kind
               | Subtyping Type Type
                 deriving (Show, Eq, Ord, Typeable, Data)

-- * accessing the environment

-- | add diagnostic messages
addDiags :: [Diagnosis] -> State.State Env ()
addDiags ds = do
    e <- State.get
    State.put $ e {envDiags = reverse ds ++ envDiags e}

-- | add sentences
appendSentences :: [Named Sentence] -> State.State Env ()
appendSentences fs = do
    e <- State.get
    State.put $ e {sentences = reverse fs ++ sentences e}

-- | store a class map
putClassMap :: ClassMap -> State.State Env ()
putClassMap ce = do
    e <- State.get
    State.put e { classMap = ce }

-- | store local assumptions
putLocalVars :: Map.Map Id VarDefn -> State.State Env ()
putLocalVars vs = do
    e <- State.get
    State.put e { localVars = vs }

-- | converting a result to a state computation
fromResult :: (Env -> Result a) -> State.State Env (Maybe a)
fromResult f = do
   e <- State.get
   let Result ds mr = f e
   addDiags ds
   return mr

-- | add the symbol to the state
addSymbol :: Symbol -> State.State Env ()
addSymbol sy = do
    e <- State.get
    State.put e { declSymbs = Set.insert sy $ declSymbs e }

-- | store local type variables
putLocalTypeVars :: LocalTypeVars -> State.State Env ()
putLocalTypeVars tvs = do
    e <- State.get
    State.put e { localTypeVars = tvs }

-- | store a complete type map
putTypeMap :: TypeMap -> State.State Env ()
putTypeMap tm = do
    e <- State.get
    State.put e { typeMap = tm }

-- | store assumptions
putAssumps :: Assumps -> State.State Env ()
putAssumps ops = do
    e <- State.get
    State.put e { assumps = ops }

-- | store assumptions
putBinders :: Map.Map Id Id -> State.State Env ()
putBinders bs = do
    e <- State.get
    State.put e { binders = bs }

-- | get the variable
getVar :: VarDecl -> Id
getVar (VarDecl v _ _ _) = v

-- | check uniqueness of variables
checkUniqueVars :: [VarDecl] -> State.State Env ()
checkUniqueVars = addDiags . checkUniqueness . map getVar

-- * morphisms

-- mapping qualified operation identifiers (aka renamings)
type FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

-- | keep types and class disjoint and use a single identifier map for both
data Morphism = Morphism
    { msource :: Env
    , mtarget :: Env
    , typeIdMap :: IdMap
    , classIdMap :: IdMap
    , funMap :: FunMap
    } deriving (Show, Eq, Ord, Typeable, Data)

-- | construct morphism for subsignatures
mkMorphism :: Env -> Env -> Morphism
mkMorphism e1 e2 = Morphism
    { msource = e1
    , mtarget = e2
    , typeIdMap = Map.empty
    , classIdMap = Map.empty
    , funMap = Map.empty }

isInclMor :: Morphism -> Bool
isInclMor m =
   Map.null (typeIdMap m) && Map.null (classIdMap m) && Map.null (funMap m)

-- * symbol stuff

-- | the type or kind of an identifier
data SymbolType =
    OpAsItemType TypeScheme
  | TypeAsItemType RawKind
  | ClassAsItemType RawKind
  | SuperClassSymbol Kind
  | TypeKindInstance Kind
  | SuperTypeSymbol Id
  | TypeAliasSymbol Type
  | PredAsItemType TypeScheme
    deriving (Show, Eq, Ord, Typeable, Data)

-- | symbols with their type
data Symbol =
    Symbol { symName :: Id, symType :: SymbolType }
    deriving (Show, Typeable, Data)

instance Eq Symbol where
    s1 == s2 = compare s1 s2 == EQ

instance Ord Symbol where
    compare s1 s2 = compare (symName s1, symType s1) (symName s2, symType s2)

-- | mapping symbols to symbols
type SymbolMap = Map.Map Symbol Symbol

-- | a set of symbols
type SymbolSet = Set.Set Symbol

-- | create a type symbol
idToTypeSymbol :: Id -> RawKind -> Symbol
idToTypeSymbol idt k = Symbol idt (TypeAsItemType $ nonVarRawKind k)

-- | create a class symbol
idToClassSymbol :: Id -> RawKind -> Symbol
idToClassSymbol idt k = Symbol idt (ClassAsItemType $ nonVarRawKind k)

-- | create an operation symbol
idToOpSymbol :: Id -> TypeScheme -> Symbol
idToOpSymbol idt typ = Symbol idt (OpAsItemType typ)

{- | raw symbols where the type of a qualified raw symbol can be a type scheme
and also be a kind if the symbol kind is unknown. -}
data RawSymbol =
    AnID Id
  | AKindedId SymbKind Id
  | ASymbol Symbol
    deriving (Show, Eq, Ord, Typeable, Data)

-- | mapping raw symbols to raw symbols
type RawSymbolMap = Map.Map RawSymbol RawSymbol

-- | create a raw symbol from an identifier
idToRaw :: Id -> RawSymbol
idToRaw = AnID

-- | extract the top identifer from a raw symbol
rawSymName :: RawSymbol -> Id
rawSymName r = case r of
    AnID i -> i
    AKindedId _ i -> i
    ASymbol s -> symName s

-- | convert a symbol type to a symbol kind
symbTypeToKind :: SymbolType -> SymbKind
symbTypeToKind s = case s of
    OpAsItemType _ -> SyKop
    TypeAsItemType _ -> SyKtype
    SuperTypeSymbol _ -> SyKtype
    TypeKindInstance _ -> SyKtype
    TypeAliasSymbol _ -> SyKtype
    ClassAsItemType _ -> SyKclass
    SuperClassSymbol _ -> SyKclass
    PredAsItemType _ -> SyKpred

-- | wrap a symbol as raw symbol (is 'ASymbol')
symbolToRaw :: Symbol -> RawSymbol
symbolToRaw = ASymbol

-- | create a raw symbol from a symbol kind and an identifier
symbKindToRaw :: SymbKind -> Id -> RawSymbol
symbKindToRaw sk = case sk of
    Implicit -> AnID
    _ -> AKindedId $ case sk of
        SyKpred -> SyKop
        SyKfun -> SyKop
        SyKsort -> SyKtype
        _ -> sk

getCompoundLists :: Env -> Set.Set [Id]
getCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union
    (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e
    where getCompound (Id _ cs _) = cs
