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

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

raw symbols bridge symb items and the symbols of a signature
-}

module HasCASL.RawSym where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.ClassAna
import HasCASL.Le
import HasCASL.Merge (addUnit)
import HasCASL.PrintLe (addClassMap)
import HasCASL.VarDecl

import Common.DocUtils
import Common.Id
import Common.Result
import Common.Lib.State
import qualified Data.Map as Map

statSymbMapItems :: Env -> [SymbMapItems] -> Result RawSymbolMap
statSymbMapItems :: Env -> [SymbMapItems] -> Result RawSymbolMap
statSymbMapItems e :: Env
e sl :: [SymbMapItems]
sl = do
    [[(RawSymbol, RawSymbol)]]
rs <- (SymbMapItems -> Result [(RawSymbol, RawSymbol)])
-> [SymbMapItems] -> Result [[(RawSymbol, RawSymbol)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (SymbMapItems kind :: SymbKind
kind l :: [SymbOrMap]
l _ _)
                 -> (SymbOrMap -> Result (RawSymbol, RawSymbol))
-> [SymbOrMap] -> Result [(RawSymbol, RawSymbol)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> SymbKind -> SymbOrMap -> Result (RawSymbol, RawSymbol)
symbOrMapToRaw Env
e SymbKind
kind) [SymbOrMap]
l) [SymbMapItems]
sl
    ((RawSymbol, RawSymbol)
 -> Result RawSymbolMap -> Result RawSymbolMap)
-> Result RawSymbolMap
-> [(RawSymbol, RawSymbol)]
-> Result RawSymbolMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (r1 :: RawSymbol
r1, r2 :: RawSymbol
r2) mm :: Result RawSymbolMap
mm -> do
            RawSymbolMap
m <- Result RawSymbolMap
mm
            if RawSymbol -> RawSymbolMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member RawSymbol
r1 RawSymbolMap
m then do
                [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("duplicate mapping for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                          RawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RawSymbol
r1 "\n ignoring: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RawSymbol
r2 "")
                       (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId (Id -> Range) -> Id -> Range
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Id
rawSymName RawSymbol
r2] (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
                RawSymbolMap -> Result RawSymbolMap
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbolMap
m
              else RawSymbolMap -> Result RawSymbolMap
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbolMap -> Result RawSymbolMap)
-> RawSymbolMap -> Result RawSymbolMap
forall a b. (a -> b) -> a -> b
$ RawSymbol -> RawSymbol -> RawSymbolMap -> RawSymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert RawSymbol
r1 RawSymbol
r2 RawSymbolMap
m)
          (RawSymbolMap -> Result RawSymbolMap
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbolMap
forall k a. Map k a
Map.empty) ([(RawSymbol, RawSymbol)] -> Result RawSymbolMap)
-> [(RawSymbol, RawSymbol)] -> Result RawSymbolMap
forall a b. (a -> b) -> a -> b
$ [[(RawSymbol, RawSymbol)]] -> [(RawSymbol, RawSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(RawSymbol, RawSymbol)]]
rs

symbOrMapToRaw :: Env -> SymbKind -> SymbOrMap -> Result (RawSymbol, RawSymbol)
symbOrMapToRaw :: Env -> SymbKind -> SymbOrMap -> Result (RawSymbol, RawSymbol)
symbOrMapToRaw e :: Env
e k :: SymbKind
k (SymbOrMap s :: Symb
s mt :: Maybe Symb
mt _) = do
    RawSymbol
s1 <- Maybe Env -> SymbKind -> Symb -> Result RawSymbol
symbToRaw (Env -> Maybe Env
forall a. a -> Maybe a
Just Env
e) SymbKind
k Symb
s
    RawSymbol
s2 <- case Maybe Symb
mt of
      Nothing -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
s1
      Just t :: Symb
t -> Maybe Env -> SymbKind -> Symb -> Result RawSymbol
symbToRaw Maybe Env
forall a. Maybe a
Nothing SymbKind
k Symb
t
    (RawSymbol, RawSymbol) -> Result (RawSymbol, RawSymbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol
s1, RawSymbol
s2)

statSymbItems :: Env -> [SymbItems] -> Result [RawSymbol]
statSymbItems :: Env -> [SymbItems] -> Result [RawSymbol]
statSymbItems e :: Env
e sl :: [SymbItems]
sl = do
  [[RawSymbol]]
rs <- (SymbItems -> Result [RawSymbol])
-> [SymbItems] -> Result [[RawSymbol]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (SymbItems kind :: SymbKind
kind l :: [Symb]
l _ _)
              -> (Symb -> Result RawSymbol) -> [Symb] -> Result [RawSymbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Env -> SymbKind -> Symb -> Result RawSymbol
symbToRaw (Env -> Maybe Env
forall a. a -> Maybe a
Just Env
e) SymbKind
kind) [Symb]
l) [SymbItems]
sl
  [RawSymbol] -> Result [RawSymbol]
forall (m :: * -> *) a. Monad m => a -> m a
return ([RawSymbol] -> Result [RawSymbol])
-> [RawSymbol] -> Result [RawSymbol]
forall a b. (a -> b) -> a -> b
$ [[RawSymbol]] -> [RawSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[RawSymbol]]
rs

symbToRaw :: Maybe Env -> SymbKind -> Symb -> Result RawSymbol
symbToRaw :: Maybe Env -> SymbKind -> Symb -> Result RawSymbol
symbToRaw me :: Maybe Env
me k :: SymbKind
k (Symb idt :: Id
idt mt :: Maybe SymbType
mt _) = case Maybe SymbType
mt of
    Nothing -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ SymbKind -> Id -> RawSymbol
symbKindToRaw SymbKind
k Id
idt
    Just (SymbType sc :: TypeScheme
sc@(TypeScheme vs :: [TypeArg]
vs t :: Type
t _)) -> case Maybe Env
me of
      Nothing ->
        RawSymbol -> String -> Range -> Result RawSymbol
forall a. a -> String -> Range -> Result a
hint (SymbKind -> Id -> RawSymbol
symbKindToRaw SymbKind
k Id
idt) "ignoring target symbol qualification"
          (Range -> Result RawSymbol) -> Range -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Range
forall a. GetRange a => a -> Range
getRange TypeScheme
sc
      Just e :: Env
e ->
        let qi :: SymbolType -> RawSymbol
qi ty :: SymbolType
ty = Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbolType -> Symbol
Symbol Id
idt SymbolType
ty
            rsc :: TypeScheme
rsc = if SymbKind
k SymbKind -> SymbKind -> Bool
forall a. Eq a => a -> a -> Bool
== SymbKind
SyKpred then Range -> TypeScheme -> TypeScheme
predTypeScheme (Id -> Range
posOfId Id
idt) TypeScheme
sc else TypeScheme
sc
            r :: Result RawSymbol
r = do
              let cm :: ClassMap
cm = ClassMap -> ClassMap -> ClassMap
addClassMap ClassMap
cpoMap (Env -> ClassMap
classMap Env
e)
                  (mtysc :: Maybe TypeScheme
mtysc, rLe :: Env
rLe) = State Env (Maybe TypeScheme) -> Env -> (Maybe TypeScheme, Env)
forall s a. State s a -> s -> (a, s)
runState (TypeScheme -> State Env (Maybe TypeScheme)
anaTypeScheme TypeScheme
rsc) Env
e
                    { typeMap :: TypeMap
typeMap = ClassMap -> TypeMap -> TypeMap
addUnit ClassMap
cm (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
e
                    , classMap :: ClassMap
classMap = ClassMap
cm }
              case Maybe TypeScheme
mtysc of
                Nothing -> [Diagnosis] -> Maybe RawSymbol -> Result RawSymbol
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse
                  ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> TypeScheme -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "no function type" TypeScheme
rsc Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: Env -> [Diagnosis]
envDiags Env
rLe) Maybe RawSymbol
forall a. Maybe a
Nothing
                Just asc :: TypeScheme
asc -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ SymbolType -> RawSymbol
qi (SymbolType -> RawSymbol) -> SymbolType -> RawSymbol
forall a b. (a -> b) -> a -> b
$ TypeScheme -> SymbolType
OpAsItemType TypeScheme
asc
            rk :: Maybe RawKind
rk = if [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
vs then do
                (_, ck :: Kind
ck) <- Type -> Maybe (Variance, Kind)
convTypeToKind Type
t
                Result RawKind -> Maybe RawKind
forall a. Result a -> Maybe a
maybeResult (Result RawKind -> Maybe RawKind)
-> Result RawKind -> Maybe RawKind
forall a b. (a -> b) -> a -> b
$ Kind -> ClassMap -> Result RawKind
anaKindM Kind
ck (ClassMap -> Result RawKind) -> ClassMap -> Result RawKind
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
e
              else Maybe RawKind
forall a. Maybe a
Nothing
        in case Maybe RawKind
rk of
             Nothing -> case SymbKind
k of
               Implicit -> Result RawSymbol
r
               SyKop -> Result RawSymbol
r
               SyKpred -> Result RawSymbol
r
               _ -> String -> Type -> Result RawSymbol
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "not a valid kind" Type
t
             Just fk :: RawKind
fk -> case SymbKind
k of
               Implicit -> -- check here which symbol is in the signature
                 case Result RawSymbol -> Maybe RawSymbol
forall a. Result a -> Maybe a
maybeResult Result RawSymbol
r of
                 Just sy :: RawSymbol
sy -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
sy
                 _ -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ SymbolType -> RawSymbol
qi (SymbolType -> RawSymbol) -> SymbolType -> RawSymbol
forall a b. (a -> b) -> a -> b
$ RawKind -> SymbolType
TypeAsItemType RawKind
fk
               SyKop -> Result RawSymbol
r
               SyKpred -> Result RawSymbol
r
               SyKclass -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ SymbolType -> RawSymbol
qi (SymbolType -> RawSymbol) -> SymbolType -> RawSymbol
forall a b. (a -> b) -> a -> b
$ RawKind -> SymbolType
ClassAsItemType RawKind
fk
               _ -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ SymbolType -> RawSymbol
qi (SymbolType -> RawSymbol) -> SymbolType -> RawSymbol
forall a b. (a -> b) -> a -> b
$ RawKind -> SymbolType
TypeAsItemType RawKind
fk

matchSymb :: Symbol -> RawSymbol -> Bool
matchSymb :: Symbol -> RawSymbol -> Bool
matchSymb sy :: Symbol
sy rsy :: RawSymbol
rsy = let ty :: SymbolType
ty = Symbol -> SymbolType
symType Symbol
sy in
  Symbol -> Id
symName Symbol
sy Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== RawSymbol -> Id
rawSymName RawSymbol
rsy Bool -> Bool -> Bool
&& case RawSymbol
rsy of
    AnID _ -> Bool
True
    AKindedId k :: SymbKind
k _ -> SymbolType -> SymbKind
symbTypeToKind SymbolType
ty SymbKind -> SymbKind -> Bool
forall a. Eq a => a -> a -> Bool
== SymbKind
k
    ASymbol sy2 :: Symbol
sy2 -> Symbol
sy Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
sy2

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