Copyright	(c) Christian Maeder and Uni Bremen 2002-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

CASL.StaticAna

Contents

traversing all data types of the abstract syntax

Description

CASL static analysis for basic specifications

Follows Chaps. III:2 and III:3 of the CASL Reference Manual.

The static analysis takes an abstract syntax tree of a basic specification and outputs a signature and a set of formulas, while checking that - all sorts used in operation and predicate declarations have been declared - all sorts, operation and predicate symbols used in formulas have been declared - formulas type-check The formulas are returned with fully-qualified variables, operation and predicate symbols.

The static analysis functions are parameterized with functions for treating CASL extensions, that is, additional basic items, signature items and formulas.

Synopsis

Documentation

checkPlaces :: [SORT] -> Id -> [Diagnosis]

checkWithVars :: String -> Map SIMPLE_ID a -> Id -> [Diagnosis]

addOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()

addAssocOp :: OpType -> Id -> State (Sign f e) ()

updateExtInfo :: (e -> Result e) -> State (Sign f e) ()

addPred :: Annoted a -> PredType -> Id -> State (Sign f e) ()

nonConsts :: OpMap -> Set Id

opMapConsts :: OpMap -> Set Id

allOpIds :: Sign f e -> Set Id

allConstIds :: Sign f e -> Set Id

addAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos

updAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos

addAssocId :: Id -> AssocMap -> AssocMap

formulaIds :: Sign f e -> Set Id

allPredIds :: Sign f e -> Set Id

addSentences :: [Named (FORMULA f)] -> State (Sign f e) ()

traversing all data types of the abstract syntax

ana_BASIC_SPEC :: (FormExtension f, TermExtension f) => Min f e -> Ana b b s f e -> Ana s b s f e -> Mix b s f e -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)

data GenKind

Constructors

Free
Generated
Loose

Instances

Eq GenKind
Ord GenKind
Show GenKind

unionGenAx :: [GenAx] -> GenAx

anaVarForms :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> State (Sign f e) [Annoted (FORMULA f)]

anaLocalVarForms :: TermExtension f => (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f)) -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])

anaDatatypeDecls :: GenKind -> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()

ana_BASIC_ITEMS :: (FormExtension f, TermExtension f) => Min f e -> Ana b b s f e -> Ana s b s f e -> Mix b s f e -> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)

mapAn :: (a -> b) -> Annoted a -> Annoted b

type GenAx = (Set SORT, Rel SORT, Set Component)

emptyGenAx :: GenAx

toSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()

ana_SIG_ITEMS :: (FormExtension f, TermExtension f) => Min f e -> Ana s b s f e -> Mix b s f e -> GenKind -> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)

ana_Generated :: (FormExtension f, TermExtension f) => Min f e -> Ana s b s f e -> Mix b s f e -> [Annoted (SIG_ITEMS s f)] -> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])

getGenSig :: SIG_ITEMS s f -> GenAx

isConsAlt :: ALTERNATIVE -> Bool

getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx

getGenSorts :: SORT_ITEM f -> GenAx

getOps :: OP_ITEM f -> Set Component

ana_SORT_ITEM :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> SortsKind -> Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))

putVarsInEmptyMap :: [VAR_DECL] -> State (Sign f e) (Sign f e)

ana_OP_ITEM :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))

headToTypeM :: a -> (OP_TYPE -> a) -> OP_HEAD -> a

headToType :: OP_HEAD -> Maybe OP_TYPE

sortsOfArgs :: [VAR_DECL] -> [SORT]

threeVars :: SORT -> ([VAR_DECL], [TERM f])

addLeftComm :: OpType -> Bool -> Id -> Named (FORMULA f)

ana_OP_ATTR :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> OpType -> Bool -> [Id] -> OP_ATTR f -> State (Sign f e) (Maybe (OP_ATTR f))

makeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)

ana_PRED_ITEM :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> Annoted (PRED_ITEM f) -> State (Sign f e) (Annoted (PRED_ITEM f))

data Component

Constructors

Component
Fields compId :: Id compType :: OpType

Instances

Eq Component
Ord Component
Show Component
GetRange Component
Pretty Component

ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]

return list of constructors

makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]

makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)

makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)

makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]

catSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]

makeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)]) -> Maybe (Named (FORMULA f))

getAltSubsorts :: ALTERNATIVE -> [SORT]

getConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])

getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]

genSelVars :: String -> Int -> [OpType] -> [VAR_DECL]

makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)]) -> [Named (FORMULA f)]

selForms1 :: String -> (Id, OpType, [COMPONENTS]) -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])

selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]

ana_ALTERNATIVE :: SORT -> Annoted ALTERNATIVE -> State (Sign f e) (Maybe (Component, Set Component))

return the constructor and the set of total selectors

ana_COMPONENTS :: SORT -> COMPONENTS -> State (Sign f e) ([Component], [Component])

return total and partial selectors

resultToState :: (a -> Result a) -> a -> State (Sign f e) a

utility

type Ana a b s f e = Mix b s f e -> a -> State (Sign f e) a

anaForm :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f)

anaTerm :: (FormExtension f, TermExtension f) => Min f e -> Mix b s f e -> Sign f e -> Maybe SORT -> Range -> TERM f -> Result (TERM f, TERM f)

basicAnalysis

Arguments

:: (FormExtension f, TermExtension f)
=> Min f e	type analysis of f
-> Ana b b s f e	static analysis of basic item b
-> Ana s b s f e	static analysis of signature item s
-> Mix b s f e	for mixfix analysis
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])	(BS with analysed mixfix formulas for pretty printing, differences to input Sig,accumulated Sig,analysed Sentences)

basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos) -> Result (BASIC_SPEC () () (), ExtSign (Sign () ()) Symbol, [Named (FORMULA ())])

cASLsen_analysis :: (BASIC_SPEC () () (), Sign () (), FORMULA ()) -> Result (FORMULA ())

extra