{- |
Module      :  ./CSL/Analysis.hs
Description :  Static Analysis for EnCL
Copyright   :  (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Ewaryst.Schulz@dfki.de
Stability   :  experimental
Portability :  portable

Static Analysis for EnCL
-}


module CSL.Analysis where

import Common.ExtSign
import Common.AS_Annotation
import Common.Id
import Common.Result
-- import Common.ResultT
import Common.Utils (mapAccumLM)

import CSL.AS_BASIC_CSL
import CSL.Symbol
-- import CSL.Fold
import CSL.Sign as Sign


-- import Control.Monad.State

-- import qualified Data.Map as Map
import qualified Data.Set as Set
-- import Data.List
import Data.Maybe

-- * Basic Analysis Functions


-- | generates a named formula
withName :: Annoted CMD -> Int -> Named CMD
withName :: Annoted CMD -> Int -> Named CMD
withName f :: Annoted CMD
f i :: Int
i = ([Char] -> CMD -> Named CMD
forall a s. a -> s -> SenAttr s a
makeNamed (if [Char]
label [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== "" then "Ax_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
                                   else [Char]
label) (CMD -> Named CMD) -> CMD -> Named CMD
forall a b. (a -> b) -> a -> b
$ Annoted CMD -> CMD
forall a. Annoted a -> a
item Annoted CMD
f)
               { isAxiom :: Bool
isAxiom = Bool -> Bool
not Bool
isTheorem }
    where
      label :: [Char]
label = Annoted CMD -> [Char]
forall a. Annoted a -> [Char]
getRLabel Annoted CMD
f
      annos :: [Annotation]
annos = Annoted CMD -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted CMD
f
      isImplies' :: Bool
isImplies' = (Bool -> Annotation -> Bool) -> Bool -> [Annotation] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ y :: Bool
y x :: Annotation
x -> Annotation -> Bool
isImplies Annotation
x Bool -> Bool -> Bool
|| Bool
y) Bool
False [Annotation]
annos
      isImplied' :: Bool
isImplied' = (Bool -> Annotation -> Bool) -> Bool -> [Annotation] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ y :: Bool
y x :: Annotation
x -> Annotation -> Bool
isImplied Annotation
x Bool -> Bool -> Bool
|| Bool
y) Bool
False [Annotation]
annos
      isTheorem :: Bool
isTheorem = Bool
isImplies' Bool -> Bool -> Bool
|| Bool
isImplied'


{- | takes a signature and a formula and a number.
It analyzes the formula and returns a formula with diagnosis -}
analyzeFormula :: Sign.Sign -> Annoted CMD -> Int -> Result (Named CMD)
analyzeFormula :: Sign -> Annoted CMD -> Int -> Result (Named CMD)
analyzeFormula _ f :: Annoted CMD
f i :: Int
i =
    Named CMD -> Result (Named CMD)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CMD -> Result (Named CMD))
-> Named CMD -> Result (Named CMD)
forall a b. (a -> b) -> a -> b
$ Annoted CMD -> Int -> Named CMD
withName Annoted CMD
f Int
i


-- | Extracts the axioms and the signature of a basic spec
splitSpec :: BASIC_SPEC -> Sign.Sign -> Result (Sign.Sign, [Named CMD])
splitSpec :: BASIC_SPEC -> Sign -> Result (Sign, [Named CMD])
splitSpec (Basic_spec specitems :: [Annoted BASIC_ITEM]
specitems) sig :: Sign
sig =
    do
      ((newsig :: Sign
newsig, _), mNCmds :: [Maybe (Named CMD)]
mNCmds) <- ((Sign, Int)
 -> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD)))
-> (Sign, Int)
-> [Annoted BASIC_ITEM]
-> Result ((Sign, Int), [Maybe (Named CMD)])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (Sign, Int)
-> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD))
anaBasicItem (Sign
sig, 0) [Annoted BASIC_ITEM]
specitems
      (Sign, [Named CMD]) -> Result (Sign, [Named CMD])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
newsig, [Maybe (Named CMD)] -> [Named CMD]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Named CMD)]
mNCmds)

{- | Add a single basic item to the signature. EP_defvals cannot be added if
   the corresponding EP_decl is not yet defined.
-}
anaBasicItem :: (Sign.Sign, Int) -> Annoted BASIC_ITEM
             -> Result ((Sign.Sign, Int), Maybe (Named CMD))
anaBasicItem :: (Sign, Int)
-> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD))
anaBasicItem (sign :: Sign
sign, i :: Int
i) itm :: Annoted BASIC_ITEM
itm =
    case Annoted BASIC_ITEM -> BASIC_ITEM
forall a. Annoted a -> a
item Annoted BASIC_ITEM
itm of
      Op_decl (Op_item tokens :: [Token]
tokens _) -> ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign -> [Token] -> Sign
addTokens Sign
sign [Token]
tokens, Int
i), Maybe (Named CMD)
forall a. Maybe a
Nothing)
      Var_decls l :: [VAR_ITEM]
l -> ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign -> [VAR_ITEM] -> Sign
addVarDecls Sign
sign [VAR_ITEM]
l, Int
i), Maybe (Named CMD)
forall a. Maybe a
Nothing)
      EP_decl l :: [(Token, EPDomain)]
l -> ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign -> [(Token, EPDomain)] -> Sign
addEPDecls Sign
sign [(Token, EPDomain)]
l, Int
i), Maybe (Named CMD)
forall a. Maybe a
Nothing)
      EP_domdecl l :: [(Token, APInt)]
l -> ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign -> [(Token, APInt)] -> Sign
addEPDomDecls Sign
sign [(Token, APInt)]
l, Int
i), Maybe (Named CMD)
forall a. Maybe a
Nothing)
      EP_defval l :: [(Token, APInt)]
l -> ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign -> [(Token, APInt)] -> Sign
addEPDefVals Sign
sign [(Token, APInt)]
l, Int
i), Maybe (Named CMD)
forall a. Maybe a
Nothing)
      Axiom_item annocmd :: Annoted CMD
annocmd ->
          do
            Named CMD
ncmd <- Sign -> Annoted CMD -> Int -> Result (Named CMD)
analyzeFormula Sign
sign Annoted CMD
annocmd Int
i
            ((Sign, Int), Maybe (Named CMD))
-> Result ((Sign, Int), Maybe (Named CMD))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign
sign, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1), Named CMD -> Maybe (Named CMD)
forall a. a -> Maybe a
Just Named CMD
ncmd)

-- | adds the specified tokens to the signature
addTokens :: Sign.Sign -> [Token] -> Sign.Sign
addTokens :: Sign -> [Token] -> Sign
addTokens sign :: Sign
sign tokens :: [Token]
tokens = let f :: Sign -> Token -> Sign
f res :: Sign
res itm :: Token
itm = Sign -> Token -> OpType -> Sign
addToSig Sign
res Token
itm
                                        (OpType -> Sign) -> OpType -> Sign
forall a b. (a -> b) -> a -> b
$ Int -> OpType
optypeFromArity 0
                        in (Sign -> Token -> Sign) -> Sign -> [Token] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign -> Token -> Sign
f Sign
sign [Token]
tokens


-- | adds the specified var items to the signature
addVarDecls :: Sign.Sign -> [VAR_ITEM] -> Sign.Sign
addVarDecls :: Sign -> [VAR_ITEM] -> Sign
addVarDecls = Sign -> [VAR_ITEM] -> Sign
forall a b. a -> b -> a
const
{-
addVarDecls sign vitems = foldl f sign vitems where
    f res (Var_item toks dom _) = addVarItem res toks dom
-}
addEPDecls :: Sign.Sign -> [(Token, EPDomain)] -> Sign.Sign
addEPDecls :: Sign -> [(Token, EPDomain)] -> Sign
addEPDecls = (Sign -> Token -> EPDomain -> Sign)
-> Sign -> [(Token, EPDomain)] -> Sign
forall a b. (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
addPairsToSig Sign -> Token -> EPDomain -> Sign
addEPDeclToSig

addEPDomDecls :: Sign.Sign -> [(Token, APInt)] -> Sign.Sign
addEPDomDecls :: Sign -> [(Token, APInt)] -> Sign
addEPDomDecls = (Sign -> Token -> APInt -> Sign)
-> Sign -> [(Token, APInt)] -> Sign
forall a b. (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
addPairsToSig Sign -> Token -> APInt -> Sign
addEPDomVarDeclToSig

addEPDefVals :: Sign.Sign -> [(Token, APInt)] -> Sign.Sign
addEPDefVals :: Sign -> [(Token, APInt)] -> Sign
addEPDefVals = (Sign -> Token -> APInt -> Sign)
-> Sign -> [(Token, APInt)] -> Sign
forall a b. (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
addPairsToSig Sign -> Token -> APInt -> Sign
addEPDefValToSig

addPairsToSig :: (Sign.Sign -> a -> b -> Sign.Sign)
              -> Sign.Sign -> [(a, b)] -> Sign.Sign
addPairsToSig :: (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign
addPairsToSig f :: Sign -> a -> b -> Sign
f = (Sign -> (a, b) -> Sign) -> Sign -> [(a, b)] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign -> (a, b) -> Sign
g where
                      g :: Sign -> (a, b) -> Sign
g s' :: Sign
s' = (a -> b -> Sign) -> (a, b) -> Sign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((a -> b -> Sign) -> (a, b) -> Sign)
-> (a -> b -> Sign) -> (a, b) -> Sign
forall a b. (a -> b) -> a -> b
$ Sign -> a -> b -> Sign
f Sign
s'


{- | stepwise extends an initially empty signature by the basic spec bs.
 The resulting spec contains analyzed axioms in it. The result contains:
 (1) the basic spec
 (2) the new signature + the added symbols
 (3) sentences of the spec
-}
basicCSLAnalysis :: (BASIC_SPEC, Sign, a)
                 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
basicCSLAnalysis :: (BASIC_SPEC, Sign, a)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
basicCSLAnalysis (bs :: BASIC_SPEC
bs, sig :: Sign
sig, _) =
    do
      (newSig :: Sign
newSig, ncmds :: [Named CMD]
ncmds) <- BASIC_SPEC -> Sign -> Result (Sign, [Named CMD])
splitSpec BASIC_SPEC
bs Sign
sig
      let newSyms :: Set Symbol
newSyms = (Id -> Symbol) -> Set Id -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Symbol
Symbol (Set Id -> Set Symbol) -> Set Id -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
opIds (Sign -> Set Id) -> Sign -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
sigDiff Sign
newSig Sign
sig
      (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC
bs, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
newSig Set Symbol
newSyms, [Named CMD]
ncmds)


{-
-- * Alternative Basic Analysis

data AnaEnv = AnaEnv
                 { aVarDecls :: Map.Map Token Domain
                 , aEPConsts :: Map.Map Token EP_const
                 , aEPDecls :: Map.Map Token EP_item
                 , aCommands :: Map.Map Int (Named CMD)
                 , aCounter :: Int
                 }


emptyAnaEnv :: AnaEnv
emptyAnaEnv = AnaEnv
              { aVarDecls = Map.empty
              , aEPConsts = Map.empty
              , aEPDecls = Map.empty
              , aCommands = Map.empty
              , aCounter = 0
              }


tTT :: CMD -> CMD
tTT c = foldCMD myrec c where
    myrec = passAllRecord { foldVar = \ _ _ -> Var $ mkSimpleId "X" }

type Analysis a = ResultT (State AnaEnv) a

-- data VAR_ITEM = Var_item [Id.Token] Domain Id.Range
anaVarDecl :: VAR_ITEM -> Analysis ()
anaVarDecl (Var_item l dom rg) = error ""

{- data EPComponent = EPDomain Id.Token EPDomain |
                      EPDefault Id.Token APInt |
                      EPConst Id.Token APInt -}
anaEPComp :: EPComponent -> Analysis ()
anaEPComp (EPDomain n dom) = addEPDomain n dom
anaEPComp (EPDefault n i) = addEPDefault n i
anaEPComp (EPConst n i) = addEPConst n i


anaAxiom :: Annoted CMD -> Analysis ()
anaAxiom = error ""

anaBasicItem' :: Annoted BASIC_ITEM -> Analysis ()
anaBasicItem' itm =
    case item itm of
      Op_decl _ -> return ()
      Var_decls l -> mapM_ anaVarDecl l
      EP_components l -> mapM_ anaEPComp l
      Axiom_item annocmd -> anaAxiom annocmd

-}