content: {- |
  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 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
  
  -}
  