6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : make static analysis checkable by RunParsers

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : Christian.Maeder@dfki.de

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : experimental

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : portable

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMake static analysis checkable by RunParsers

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule CASL.RunStaticAna where

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AnnoState

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AS_Annotation

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.GlobalAnnotations

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Result

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.DocUtils

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.ExtSign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.Parse_AS_Basic

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.AS_Basic_CASL

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.Sign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.StaticAna

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.SimplifySen

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.Quantification

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.AlphaConvert

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlocalAnalysis :: GlobalAnnos -> BASIC_SPEC () () ()

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Result (BASIC_SPEC () () ())

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlocalAnalysis ga bs =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let Result ds ms = basicCASLAnalysis (bs, emptySign () , ga)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in Result ds $ case ms of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (newBs, _accSig, _sents) -> Just newBs

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrunAna :: GlobalAnnos -> AParser () (Result (BASIC_SPEC () () ()))

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrunAna ga =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann do b <- basicSpec []

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return $ localAnalysis ga b

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlocalAna :: GlobalAnnos -> BASIC_SPEC () () () -> Result (Sign () ())

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlocalAna ga bs =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let Result ds ms =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basicCASLAnalysis (bs, emptySign () , ga)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann es = filter ((<= Error) . diagKind) ds

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in case ms of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (_newBs, ExtSign accSig _, _sents) -> Result es $ Just accSig

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Result ds Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSign :: GlobalAnnos -> AParser () (Result (Sign () ()))

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetSign ga =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann do b <- basicSpec []

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return $ localAna ga b

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannprops :: GlobalAnnos -> BASIC_SPEC () () ()

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Result (Sign () (), [Named (FORMULA ())])

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannprops ga bs =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let Result ds ms =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basicCASLAnalysis (bs, emptySign (), ga)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in Result ds $ case ms of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (_newBs, ExtSign accSig _, sents) -> Just (accSig,

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map (mapNamed $ simplifySen (error "props1")

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (error "props2") accSig

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann . stripQuant . convertFormula 1 id)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sents)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetProps :: GlobalAnnos

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> AParser () (Result (Sign () (), [Annoted (FORMULA ())]))

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetProps ga =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann do b <- basicSpec []

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return $ fmap ( \ (sign, sens) -> (sign, map fromLabelledSen sens))

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ props ga b

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann