content: {- |
  Module      :  ./CASL/RunStaticAna.hs
  Description :  make static analysis checkable by RunParsers
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2003
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  Make static analysis checkable by RunParsers
  
  -}
  
  module CASL.RunStaticAna where
  
  import Common.AnnoState
  import Common.AS_Annotation
  import Common.GlobalAnnotations
  import Common.Result
  import Common.DocUtils
  import Common.ExtSign
  
  import CASL.Parse_AS_Basic
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.StaticAna
  import CASL.SimplifySen
  import CASL.Quantification
  import CASL.AlphaConvert
  
  import qualified Data.Map as Map
  
  plainBasicSpec :: AParser st (BASIC_SPEC () () ())
  plainBasicSpec = basicSpec [] Map.empty
  
  localAnalysis :: GlobalAnnos -> BASIC_SPEC () () ()
                -> Result (BASIC_SPEC () () ())
  localAnalysis ga bs =
          let Result ds ms = basicCASLAnalysis (bs, emptySign () , ga)
          in Result ds $ case ms of
             Just (newBs, _accSig, _sents) -> Just newBs
             _ -> Nothing
  
  runAna :: GlobalAnnos -> AParser () (Result (BASIC_SPEC () () ()))
  runAna ga =
      do b <- plainBasicSpec
         return $ localAnalysis ga b
  
  localAna :: GlobalAnnos -> BASIC_SPEC () () () -> Result (Sign () ())
  localAna ga bs =
      let Result ds ms =
              basicCASLAnalysis (bs, emptySign () , ga)
          es = filter ((<= Error) . diagKind) ds
          in case ms of
             Just (_newBs, ExtSign accSig _, _sents) -> Result es $ Just accSig
             Nothing -> Result ds Nothing
  
  getSign :: GlobalAnnos -> AParser () (Result (Sign () ()))
  getSign ga =
      do b <- plainBasicSpec
         return $ localAna ga b
  
  props :: GlobalAnnos -> BASIC_SPEC () () ()
        -> Result (Sign () (), [Named (FORMULA ())])
  props ga bs =
      let Result ds ms =
              basicCASLAnalysis (bs, emptySign (), ga)
          in Result ds $ case ms of
             Just (_newBs, ExtSign accSig _, sents) -> Just (accSig,
                       map (mapNamed $ simplifySen (error "props1")
                                       (error "props2") accSig
                             . stripQuant accSig . convertFormula 1 id)
                         sents)
             Nothing -> Nothing
  
  getProps :: GlobalAnnos
           -> AParser () (Result (Sign () (), [Annoted (FORMULA ())]))
  getProps ga =
      do b <- plainBasicSpec
         return $ fmap ( \ (sign, sens) -> (sign, map fromLabelledSen sens))
                $ props ga b
  