e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder{- |

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederModule : $Header$

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederDescription : test driver for static analysis

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : Christian.Maeder@dfki.de

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : experimental

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : portable

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederparse and call static analysis

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-}

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maedermodule HasCASL.RunStaticAna where

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport HasCASL.Le

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport HasCASL.As

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport HasCASL.AsToLe(anaBasicSpec)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport HasCASL.ParseItem(basicSpec)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport HasCASL.ProgEq

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport HasCASL.SimplifyTerm

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport HasCASL.Builtin

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.Lib.State

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.Doc

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.DocUtils

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.RunParsers

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.AS_Annotation

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.GlobalAnnotations

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport Common.AnnoState

cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederbParser :: GlobalAnnos -> AParser () (BasicSpec, Env)

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederbParser ga = do b <- basicSpec

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ runState (anaBasicSpec ga b) initialEnv

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskianaParser :: StringParser

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskianaParser ga = do (a, e) <- bParser ga

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let ne = e { sentences = map

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (mapNamed $ simplifySentence e) $ sentences e }

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return . show . useGlobalAnnos (addBuiltins ga)

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder $ pretty a $+$ pretty ne

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitype SenParser = GlobalAnnos -> AParser () [Named Sentence]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersenParser :: SenParser

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersenParser = fmap (reverse . sentences . snd) . bParser

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedertransParser :: SenParser

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedertransParser = fmap ( ( \ e -> map (mapNamed (translateSen e)) $ reverse $

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sentences e) . snd) . bParser

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederprintSen :: SenParser -> StringParser

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiprintSen p ga = fmap (show . useGlobalAnnos (addBuiltins ga) .

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski vcat . map (pretty . fromLabelledSen)) $ p ga

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski