| 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 |
OMDoc.DataTypes
Contents
Description
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
Constructors
| 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
Constructors
| 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 Fixity
Fixity 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
Instances
| 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
Constructors
| OMS OMQualName | Symbol |
| OMV OMName | Simple variable |
| OMATTT OMElement OMAttribute | Attributed element needed for type annotations of elements |
| OMA [OMElement] | Application to a list of arguments, first argument is usually the functionhead |
| OMBIND OMElement [OMElement] OMElement | Bindersymbol, bound vars, body |
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)
Constructors
| SigMapI | |
Fields
| |
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.
Arguments
| :: String | the kind of the encoding, may not contain colons |
| -> [String] | the values to encode |
| -> String |
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