Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone




Static Analysis for EnCL


Basic Analysis Functions

withName :: Annoted CMD -> Int -> Named CMD

generates a named formula

analyzeFormula :: Sign -> Annoted CMD -> Int -> Result (Named CMD)

takes a signature and a formula and a number. It analyzes the formula and returns a formula with diagnosis

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

Extracts the axioms and the signature of a basic spec

anaBasicItem :: (Sign, Int) -> Annoted BASIC_ITEM -> Result ((Sign, Int), Maybe (Named CMD))

Add a single basic item to the signature. EP_defvals cannot be added if the corresponding EP_decl is not yet defined.

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

adds the specified tokens to the signature

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

adds the specified var items to the signature

addPairsToSig :: (Sign -> a -> b -> Sign) -> Sign -> [(a, b)] -> Sign

basicCSLAnalysis :: (BASIC_SPEC, Sign, a) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])

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