Copyright | (c) Ewaryst Schulz, DFKI 2008 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Ewaryst.Schulz@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Datatypes for an intermediate OMDoc representation.
- data OMDoc = OMDoc String [TLElement]
- data TLElement
- data TCElement
- type TCorOMElement = Either TCElement OMElement
- type TCMorphism = [(OMName, OMImage)]
- type OMImage = Either String OMElement
- data OmdADT
- data SymbolRole
- data Fixity
- data Assoc
- data ADTType
- data Totality
- data NotationComponent
- data OMName = OMName {}
- data OMAttribute = OMAttr OMElement OMElement
- data OMCD = CD [String]
- type OMQualName = (OMCD, OMName)
- data OMElement
- nameToId :: String -> Id
- nameToToken :: String -> Token
- type UniqName = (String, Int)
- type NameMap a = Map a UniqName
- data SigMap a = SigMap (NameMap a) (NameMap String)
- data SigMapI a = SigMapI {
- sigMapISymbs :: Map OMName a
- sigMapINotations :: Map OMName String
- sigMapSymbs :: SigMap a -> NameMap a
- cdFromList :: [String] -> OMCD
- cdIsEmpty :: OMCD -> Bool
- cdToList :: OMCD -> [String]
- cdToMaybeList :: OMCD -> [Maybe String]
- uniqPrefix :: String
- nameEncode :: String -> [String] -> String
- nameDecode :: String -> Maybe (String, [String])
- nameToString :: UniqName -> String
- tcName :: TCElement -> OMName
- unqualName :: OMQualName -> OMName
- emptyCD :: OMCD
- omName :: UniqName -> OMName
- mkSimpleName :: String -> OMName
- mkSimpleQualName :: UniqName -> OMQualName
- simpleOMS :: UniqName -> OMElement
- lookupNotation :: SigMapI a -> OMName -> String
- lookupNotationInMap :: Map OMName String -> OMName -> String
Documentation
data OMDoc
OMDoc root element with libname and a list of toplevel elements
data TLElement
Toplevel elements for OMDoc, theory with name, meta and content, view with from, to and morphism
data TCElement
Theory constitutive elements for OMDoc
TCSymbol String OMElement SymbolRole (Maybe OMElement) | Symbol to represent sorts, constants, predicate symbols, etc. |
TCNotation OMQualName String (Maybe String) | A notation for the given symbol with an optional style |
TCSmartNotation OMQualName Fixity Assoc Int Int | A smart notation for the given symbol with fixity, associativity, precedence and the number of implicit arguments |
TCFlexibleNotation OMQualName Int [NotationComponent] | A smart notation for the given symbol, the argument- and text-components have to alternate in the component list |
TCADT [OmdADT] | Algebraic Data Type represents free/generated types |
TCImport String OMCD TCMorphism | Import statements for referencing other theories |
TCComment String | A comment, only for development purposes |
type TCorOMElement = Either TCElement OMElement
return type for sentence translation (ADT or formula)
type TCMorphism = [(OMName, OMImage)]
Morphisms to specify signature mappings
type OMImage = Either String OMElement
The target type of a mapping is just an alias or an assignment to a symbol
data OmdADT
The flattened structure of an Algebraic Data Type
ADTSortDef String ADTType [OmdADT] | A single sort given by name, type and a list of constructors |
ADTConstr String [OmdADT] | A constructor given by its name and a list of arguments |
ADTArg OMElement (Maybe OmdADT) | An argument with type and evtually a selector |
ADTSelector String Totality | The selector has a name and is total (Yes) or partial (No) |
ADTInsort OMQualName | Insort elements point to other sortdefs and inherit their structure |
data SymbolRole
Roles of the declared symbols can be object or type
data Fixity
Fixity of notation patterns
data Assoc
Associativity of notation patterns
data ADTType
Type of the algebraic data type
data Totality
Totality for selectors of an adt
data NotationComponent
A component can be a text-component, e.g., value="["/, or an argument-component such as index="1" precedence="p1"/
data OMName
Names used for OpenMath variables and symbols
data OMAttribute
Attribute-name/attribute-value pair used to represent the type of a type-annotated term
Eq OMAttribute | |
Ord OMAttribute | |
Read OMAttribute | |
Show OMAttribute | |
XmlRepresentable OMAttribute | Helper instance for OpenMath attributes |
data OMCD
CD contains the reference to the content dictionary and eventually the cdbase entry
type OMQualName = (OMCD, OMName)
data OMElement
Elements for Open Math
Hets Utils
nameToToken :: String -> Token
Utils for Translation
data SigMap a
Mapping of symbols and sentence names to unique ids (used in export)
data SigMapI a
Mapping of OMDoc names to hets strings, for signature creation, and strings to symbols, for lookup in terms (used in import)
SigMapI | |
|
sigMapSymbs :: SigMap a -> NameMap a
cdFromList :: [String] -> OMCD
cdToMaybeList :: OMCD -> [Maybe String]
Name handling: encoding, decoding, unique names
uniqPrefix :: String
The closing paren + percent can be used neither in ordinary Hets-names nor in sentence names hence it is used here for encodings.
Special name encoding in order to be able to recognize these names while reading.
nameDecode :: String -> Maybe (String, [String])
This invariant should hold:
(x, l) = fromJust $ nameDecode $ nameEncode x l
nameToString :: UniqName -> String
Constructing/Extracting Values
name of the theory constitutive element, error if not TCSymbol, TCNotation, or TCImport
unqualName :: OMQualName -> OMName
mkSimpleName :: String -> OMName
Lookup utils for Import and Export
lookupNotation :: SigMapI a -> OMName -> String