Copyright	(c) Dominik Dietrich, DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	dominik.dietrich@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred

CSL.Sign

Description

Types and functions for EnCL logic signatures

Synopsis

Documentation

data Sign

Datatype for EnCL Signatures Signatures are just sets of Tokens for the operators

Constructors

Sign (Map Token OpType) (Map Token (Maybe APInt)) (Map Token EPDecl)

Instances

Eq Sign
Data Sign
Ord Sign
Show Sign
ShATermConvertible Sign
Pretty Sign
Typeable * Sign
Category Sign Morphism	Instance of Category for CSL logic
Sentences CSL CMD Sign Morphism Symbol	Instance of Sentences for reduce logic
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for reduce logic
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]	Instance of Logic for reduce logc

opIds :: Sign -> Set Id

data OpType

Constructors

OpType
Fields opArity :: Int

Instances

Eq OpType
Data OpType
Ord OpType
Show OpType
ShATermConvertible OpType
Typeable * OpType

pretty :: Pretty a => a -> Doc

isLegalSignature :: Sign -> Bool

determines whether a signature is valid. all sets are ok, so glued to true

addToSig :: Sign -> Token -> OpType -> Sign

Basic function to extend a given signature by adding an item (id) to it

unite :: Sign -> Sign -> Sign

Union of signatures

emptySig :: Sign

The empty signature, use this one to create new signatures

isSubSigOf :: Sign -> Sign -> Bool

Determines if sig1 is subsignature of sig2

sigDiff :: Sign -> Sign -> Sign

difference of Signatures

sigUnion :: Sign -> Sign -> Result Sign

union of Signatures or do I have to care about more things here?

lookupSym :: Sign -> Id -> Bool

checks whether a Id is declared in the signature

optypeFromArity :: Int -> OpType

addEPDefValToSig :: Sign -> Token -> APInt -> Sign

addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign

Adds an extended parameter declaration for a given domain and eventually implicitly defined EP domain vars, e.g., for 'I = [0, n]' n is implicitly added

addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign