{- |
Module      :  ./RelationalScheme/StaticAnalysis.hs
Description :  static analysis for Relational Schemes
Copyright   :  Dominik Luecke, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt or LIZENZ.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis for Relational Schemes
-}

module RelationalScheme.StaticAnalysis
    (
        basic_Rel_analysis
    )
    where

import RelationalScheme.AS
import RelationalScheme.Sign

import Common.AS_Annotation
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Result

import Control.Monad

import Data.Maybe
import qualified Data.Set as Set

basic_Rel_analysis :: (RSScheme, Sign, GlobalAnnos) ->
                      Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])
basic_Rel_analysis :: (RSScheme, Sign, GlobalAnnos)
-> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])
basic_Rel_analysis (spec :: RSScheme
spec, sign :: Sign
sign, _) =
    let
        sens :: [Annoted Sentence]
sens = RSScheme -> [Annoted Sentence]
getRels RSScheme
spec
        sig :: Sign
sig = RSScheme -> Sign
getSignature RSScheme
spec
    in
    do
        Sign
os <- Sign
sig Sign -> Sign -> Result Sign
forall (m :: * -> *). MonadFail m => Sign -> Sign -> m Sign
`uniteSig` Sign
sign
        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sign -> Set RSTable
tables Sign
os Set RSTable -> Set RSTable -> Bool
forall a. Eq a => a -> a -> Bool
== Set RSTable
forall a. Set a
Set.empty) (String -> Range -> Result ()
forall a. String -> Range -> Result a
fatal_error "Empty signature" Range
nullRange)
        let syms :: Set RSSymbol
syms = Sign -> Set RSSymbol
getSymbols Sign
sig
        (Annoted Sentence -> Result (Annoted Sentence))
-> [Annoted Sentence] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Annoted Sentence -> Result (Annoted Sentence)
analyse_relationship Sign
os) [Annoted Sentence]
sens
        (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])
-> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (RSScheme
spec, ExtSign :: forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign
                    {
                        plainSign :: Sign
plainSign = Sign
os
                    , nonImportedSymbols :: Set RSSymbol
nonImportedSymbols = Set RSSymbol
syms
                    },
                    (Annoted Sentence -> Named Sentence)
-> [Annoted Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Annoted Sentence -> Named Sentence
forall a. Annoted a -> Named a
makeNamedSen [Annoted Sentence]
sens)

-- ^ Function to determine the symbols of a spec
getSymbols :: RSTables -> Set.Set RSSymbol
getSymbols :: Sign -> Set RSSymbol
getSymbols inTbl :: Sign
inTbl =
        (RSTable -> Set RSSymbol -> Set RSSymbol)
-> Set RSSymbol -> Set RSTable -> Set RSSymbol
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: RSTable
x y :: Set RSSymbol
y ->
             Set RSSymbol -> Set RSSymbol -> Set RSSymbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                ((Set RSSymbol -> RSColumn -> Set RSSymbol)
-> Set RSSymbol -> [RSColumn] -> Set RSSymbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ b :: Set RSSymbol
b a :: RSColumn
a -> Id -> Id -> RSDatatype -> Bool -> RSSymbol
SColumn (RSTable -> Id
t_name RSTable
x) (RSColumn -> Id
c_name RSColumn
a) (RSColumn -> RSDatatype
c_data RSColumn
a) (RSColumn -> Bool
c_key RSColumn
a)
                        RSSymbol -> Set RSSymbol -> Set RSSymbol
forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set RSSymbol
b) Set RSSymbol
forall a. Set a
Set.empty ([RSColumn] -> Set RSSymbol) -> [RSColumn] -> Set RSSymbol
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
columns RSTable
x) (Set RSSymbol -> Set RSSymbol) -> Set RSSymbol -> Set RSSymbol
forall a b. (a -> b) -> a -> b
$
                (Id -> RSSymbol
STable (Id -> RSSymbol) -> Id -> RSSymbol
forall a b. (a -> b) -> a -> b
$ RSTable -> Id
t_name RSTable
x) RSSymbol -> Set RSSymbol -> Set RSSymbol
forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set RSSymbol
y) Set RSSymbol
forall a. Set a
Set.empty (Set RSTable -> Set RSSymbol) -> Set RSTable -> Set RSSymbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
tables Sign
inTbl

-- ^ outputs a sorted list of sorts
collectTypes :: RSTables -> [RSQualId] -> [RSDatatype]
collectTypes :: Sign -> [RSQualId] -> [RSDatatype]
collectTypes tb :: Sign
tb = (RSQualId -> RSDatatype) -> [RSQualId] -> [RSDatatype]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> RSQualId -> RSDatatype
collectType Sign
tb)

collectType :: RSTables -> RSQualId -> RSDatatype
collectType :: Sign -> RSQualId -> RSDatatype
collectType tbi :: Sign
tbi qi :: RSQualId
qi =
        let
                tb :: Set RSTable
tb = Sign -> Set RSTable
tables Sign
tbi
                (tn :: Id
tn, cn :: Id
cn) = case RSQualId
qi of
                        RSQualId i1 :: Id
i1 i2 :: Id
i2 _ -> (Id
i1, Id
i2)
                t :: RSTable
t = [RSTable] -> RSTable
forall a. [a] -> a
head ([RSTable] -> RSTable) -> [RSTable] -> RSTable
forall a b. (a -> b) -> a -> b
$ Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ (RSTable -> Bool) -> Set RSTable -> Set RSTable
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ x :: RSTable
x -> RSTable -> Id
t_name RSTable
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
tn) Set RSTable
tb
                r :: RSColumn
r = [RSColumn] -> RSColumn
forall a. [a] -> a
head ([RSColumn] -> RSColumn) -> [RSColumn] -> RSColumn
forall a b. (a -> b) -> a -> b
$ (RSColumn -> Bool) -> [RSColumn] -> [RSColumn]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: RSColumn
x -> RSColumn -> Id
c_name RSColumn
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
cn) ([RSColumn] -> [RSColumn]) -> [RSColumn] -> [RSColumn]
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
columns RSTable
t
        in
                RSColumn -> RSDatatype
c_data RSColumn
r

{-
collectNames :: RSTables -> [RSQualId] -> [Id]
collectNames tb qar =
    sort $ map (collectName tb) qar

collectName :: RSTables -> RSQualId -> Id
collectName tbi qi =
    let
        tb = tables tbi
        (tn, cn) = case qi of
                     RSQualId i1 i2 _ -> (i1,i2)
        t  = head $ Set.toList $ Set.filter (\x -> t_name x == tn) tb
        r  = head $ filter (\x -> c_name x == cn) $ columns t
    in
      c_name r
-}

analyse_relationship :: RSTables -> Annoted RSRel -> Result (Annoted RSRel)
analyse_relationship :: Sign -> Annoted Sentence -> Result (Annoted Sentence)
analyse_relationship tbi :: Sign
tbi reli :: Annoted Sentence
reli =
    let
        tb :: Set RSTable
tb = Sign -> Set RSTable
tables Sign
tbi
        rel :: Sentence
rel = Annoted Sentence -> Sentence
forall a. Annoted a -> a
item Annoted Sentence
reli
        (relDom :: [RSQualId]
relDom, relCo :: [RSQualId]
relCo, _, rn :: Range
rn) = case Sentence
rel of
            RSRel r1 :: [RSQualId]
r1 r2 :: [RSQualId]
r2 r3 :: RSRelType
r3 r4 :: Range
r4 -> ([RSQualId]
r1, [RSQualId]
r2, RSRelType
r3, Range
r4)
        (t2 :: Id
t2, _) = case [RSQualId] -> RSQualId
forall a. [a] -> a
head [RSQualId]
relCo of
            RSQualId i1 :: Id
i1 i2 :: Id
i2 _ -> (Id
i1, Id
i2)
        tf2 :: [RSTable]
tf2 = Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ (RSTable -> Bool) -> Set RSTable -> Set RSTable
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ x :: RSTable
x -> RSTable -> Id
t_name RSTable
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
t2) Set RSTable
tb
        keyz2 :: Set (Id, RSDatatype)
keyz2 = RSTable -> Set (Id, RSDatatype)
t_keys (RSTable -> Set (Id, RSDatatype))
-> RSTable -> Set (Id, RSDatatype)
forall a b. (a -> b) -> a -> b
$ [RSTable] -> RSTable
forall a. [a] -> a
head [RSTable]
tf2
        domT :: [RSDatatype]
domT = Sign -> [RSQualId] -> [RSDatatype]
collectTypes Sign
tbi [RSQualId]
relDom
        codoT :: [RSDatatype]
codoT = Sign -> [RSQualId] -> [RSDatatype]
collectTypes Sign
tbi [RSQualId]
relCo
{- domN  = collectNames tbi relDom
codoN = collectNames tbi relCo -}
    in
        do
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([RSDatatype]
domT [RSDatatype] -> [RSDatatype] -> Bool
forall a. Eq a => a -> a -> Bool
/= [RSDatatype]
codoT) (String -> Range -> Result ()
forall a. String -> Range -> Result a
fatal_error ("The types of the left and right " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                " right hand side of: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
rel String -> String -> String
forall a. [a] -> [a] -> [a]
++ " do not match") Range
rn)
{- when (domN /= codoN && length domN > 1) (fatal_error ("The names of the left and right " ++
" right hand side of: " ++ (show rel) ++ " do not match") rn) -}
            (RSQualId -> Result RSQualId) -> [RSQualId] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Range -> Set RSTable -> RSQualId -> Result RSQualId
analyse_RSQualid Range
rn Set RSTable
tb) [RSQualId]
relDom
            [(RSQualId, Maybe Id)]
k2 <- (RSQualId -> Result (RSQualId, Maybe Id))
-> [RSQualId] -> Result [(RSQualId, Maybe Id)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> Set RSTable -> RSQualId -> Result (RSQualId, Maybe Id)
analyse_RSQualidK Range
rn Set RSTable
tb) [RSQualId]
relCo
            let kl2 :: Set Id
kl2 = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> [Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Maybe Id -> Id) -> [Maybe Id] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Id -> Id
forall a. HasCallStack => Maybe a -> a
fromJust ([Maybe Id] -> [Id]) -> [Maybe Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ (Maybe Id -> Bool) -> [Maybe Id] -> [Maybe Id]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Maybe Id
x -> case Maybe Id
x of
                                 Nothing -> Bool
False
                                 _ -> Bool
True) ([Maybe Id] -> [Maybe Id]) -> [Maybe Id] -> [Maybe Id]
forall a b. (a -> b) -> a -> b
$ ((RSQualId, Maybe Id) -> Maybe Id)
-> [(RSQualId, Maybe Id)] -> [Maybe Id]
forall a b. (a -> b) -> [a] -> [b]
map (RSQualId, Maybe Id) -> Maybe Id
forall a b. (a, b) -> b
snd [(RSQualId, Maybe Id)]
k2
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set Id
kl2 Set Id -> Set Id -> Bool
forall a. Eq a => a -> a -> Bool
/= ((Id, RSDatatype) -> Id) -> Set (Id, RSDatatype) -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Id, RSDatatype) -> Id
forall a b. (a, b) -> a
fst Set (Id, RSDatatype)
keyz2) (String -> Range -> Result ()
forall a. String -> Range -> Result a
fatal_error
             ("Not all keys are used on the right hand side of: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
rel)
             Range
rn)
            Annoted Sentence -> Result (Annoted Sentence)
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted Sentence
reli

analyse_RSQualid :: Range -> Set.Set RSTable -> RSQualId -> Result RSQualId
analyse_RSQualid :: Range -> Set RSTable -> RSQualId -> Result RSQualId
analyse_RSQualid rn :: Range
rn st :: Set RSTable
st quid :: RSQualId
quid =
    let
        (tname :: Id
tname, cname :: Id
cname) = case RSQualId
quid of
            RSQualId i1 :: Id
i1 i2 :: Id
i2 _ -> (Id
i1, Id
i2)
        ft :: Set RSTable
ft = (RSTable -> Bool) -> Set RSTable -> Set RSTable
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ x :: RSTable
x -> RSTable -> Id
t_name RSTable
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
tname) Set RSTable
st
        cols :: Set Id
cols = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> [Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (RSColumn -> Id) -> [RSColumn] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map RSColumn -> Id
c_name ([RSColumn] -> [Id]) -> [RSColumn] -> [Id]
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
columns (RSTable -> [RSColumn]) -> RSTable -> [RSColumn]
forall a b. (a -> b) -> a -> b
$ [RSTable] -> RSTable
forall a. [a] -> a
head ([RSTable] -> RSTable) -> [RSTable] -> RSTable
forall a b. (a -> b) -> a -> b
$ Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList Set RSTable
ft
    in
      do
        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id
cname Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Id
cols) (String -> Range -> Result ()
forall a. String -> Range -> Result a
fatal_error (Id -> String
forall a. Show a => a -> String
show Id
cname String -> String -> String
forall a. [a] -> [a] -> [a]
++
         " is not" String -> String -> String
forall a. [a] -> [a] -> [a]
++ " defined") Range
rn)
        RSQualId -> Result RSQualId
forall (m :: * -> *) a. Monad m => a -> m a
return RSQualId
quid

analyse_RSQualidK :: Range -> Set.Set RSTable -> RSQualId -> Result (RSQualId, Maybe Id)
analyse_RSQualidK :: Range -> Set RSTable -> RSQualId -> Result (RSQualId, Maybe Id)
analyse_RSQualidK rn :: Range
rn st :: Set RSTable
st quid :: RSQualId
quid =
    let
        (tname :: Id
tname, cname :: Id
cname) = case RSQualId
quid of
            RSQualId i1 :: Id
i1 i2 :: Id
i2 _ -> (Id
i1, Id
i2)
        ft :: Set RSTable
ft = (RSTable -> Bool) -> Set RSTable -> Set RSTable
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ x :: RSTable
x -> RSTable -> Id
t_name RSTable
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
tname) Set RSTable
st
    in
            case Set RSTable -> Int
forall a. Set a -> Int
Set.size Set RSTable
ft of
            0 -> (RSQualId, Maybe Id) -> Result (RSQualId, Maybe Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (RSQualId
quid, Maybe Id
forall a. Maybe a
Nothing)
            1 -> do
                        let tid :: RSTable
tid = [RSTable] -> RSTable
forall a. [a] -> a
head ([RSTable] -> RSTable) -> [RSTable] -> RSTable
forall a b. (a -> b) -> a -> b
$ Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList Set RSTable
ft
                            keyz :: Set Id
keyz = ((Id, RSDatatype) -> Id) -> Set (Id, RSDatatype) -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Id, RSDatatype) -> Id
forall a b. (a, b) -> a
fst (Set (Id, RSDatatype) -> Set Id) -> Set (Id, RSDatatype) -> Set Id
forall a b. (a -> b) -> a -> b
$ RSTable -> Set (Id, RSDatatype)
t_keys RSTable
tid
                        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id
cname Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Id
keyz) (String -> Range -> Result ()
forall a. String -> Range -> Result a
fatal_error
                         (Id -> String
forall a. Show a => a -> String
show Id
cname String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is used " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                          "as a key, but not defined as one") Range
rn)
                        (RSQualId, Maybe Id) -> Result (RSQualId, Maybe Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (RSQualId
quid, Id -> Maybe Id
forall a. a -> Maybe a
Just Id
cname)
            _ -> String -> Range -> Result (RSQualId, Maybe Id)
forall a. String -> Range -> Result a
fatal_error ("Duplicate table name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set RSTable -> String
forall a. Show a => a -> String
show Set RSTable
ft) Range
rn