{- |

Module : $Header$

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 f i = (makeNamed (if label == "" then "Ax_" ++ show i

else label) $ item f)

{ isAxiom = not isTheorem }

where

label = getRLabel f

annos = r_annos f

isImplies' = foldl (\ y x -> isImplies x || y) False annos

isImplied' = foldl (\ y x -> isImplied x || y) False annos

isTheorem = isImplies' || 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 _ f i =

return $ withName f i

-- | Extracts the axioms and the signature of a basic spec

splitSpec :: BASIC_SPEC -> Sign.Sign -> Result (Sign.Sign, [Named CMD])

splitSpec (Basic_spec specitems) sig =

do

((newsig, _), mNCmds) <- mapAccumLM anaBasicItem (sig, 0) specitems

return (newsig, catMaybes 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, i) itm =

case item itm of

Op_decl (Op_item tokens _) -> return ((addTokens sign tokens, i), Nothing)

Var_decls l -> return ((addVarDecls sign l, i), Nothing)

EP_decl l -> return ((addEPDecls sign l, i), Nothing)

EP_domdecl l -> return ((addEPDomDecls sign l, i), Nothing)

EP_defval l -> return ((addEPDefVals sign l, i), Nothing)

Axiom_item annocmd ->

do

ncmd <- analyzeFormula sign annocmd i

return ((sign, i + 1), Just ncmd)

-- | adds the specified tokens to the signature

addTokens :: Sign.Sign -> [Token] -> Sign.Sign

addTokens sign tokens = let f res itm = addToSig res itm

$ optypeFromArity 0

in foldl f sign tokens

-- | adds the specified var items to the signature

addVarDecls :: Sign.Sign -> [VAR_ITEM] -> Sign.Sign

addVarDecls = 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 = addPairsToSig addEPDeclToSig

addEPDomDecls :: Sign.Sign -> [(Token, APInt)] -> Sign.Sign

addEPDomDecls = addPairsToSig addEPDomVarDeclToSig

addEPDefVals :: Sign.Sign -> [(Token, APInt)] -> Sign.Sign

addEPDefVals = addPairsToSig addEPDefValToSig

addPairsToSig :: (Sign.Sign -> a -> b -> Sign.Sign)

-> Sign.Sign -> [(a, b)] -> Sign.Sign

addPairsToSig f = foldl g where

g s' = uncurry $ f 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 (bs, sig, _) =

do

(newSig, ncmds) <- splitSpec bs sig

let newSyms = Set.map Symbol $ opIds $ sigDiff newSig sig

return (bs, ExtSign newSig newSyms, 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

-}