Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder and Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.StaticAna

Contents

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

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

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

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

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

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

allOpIds :: Sign f e -> Set Id Source #

allConstIds :: Sign f e -> Set Id Source #

formulaIds :: Sign f e -> Set Id Source #

allPredIds :: Sign f e -> Set Id Source #

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

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) Source #

data GenKind Source #

Constructors

Free 
Generated 
Loose 

Instances

Eq GenKind Source # 

Methods

(==) :: GenKind -> GenKind -> Bool

(/=) :: GenKind -> GenKind -> Bool

Ord GenKind Source # 

Methods

compare :: GenKind -> GenKind -> Ordering

(<) :: GenKind -> GenKind -> Bool

(<=) :: GenKind -> GenKind -> Bool

(>) :: GenKind -> GenKind -> Bool

(>=) :: GenKind -> GenKind -> Bool

max :: GenKind -> GenKind -> GenKind

min :: GenKind -> GenKind -> GenKind

Show GenKind Source # 

Methods

showsPrec :: Int -> GenKind -> ShowS

show :: GenKind -> String

showList :: [GenKind] -> ShowS

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)] Source #

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)]) Source #

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) Source #

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

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

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

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) Source #

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)]) Source #

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)) Source #

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

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

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)) Source #

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

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)) Source #

data Component Source #

Constructors

Component 

Fields

Instances

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

return list of constructors

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

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

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

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

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

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

return the constructor and the set of total selectors

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

return total and partial selectors

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

utility

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

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

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) Source #

basicAnalysis Source #

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 ())]) Source #

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

extra