| 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
Description
Datatypes for an intermediate OMDoc representation.
Synopsis
- data OMDoc = OMDoc String [TLElement]
- data TLElement
- data TCElement
- = TCSymbol String OMElement SymbolRole (Maybe OMElement)
- | TCNotation OMQualName String (Maybe String)
- | TCSmartNotation OMQualName Fixity Assoc Int Int
- | TCFlexibleNotation OMQualName Int [NotationComponent]
- | TCADT [OmdADT]
- | TCImport String OMCD TCMorphism
- | TCComment String
- type TCorOMElement = Either TCElement OMElement
- type TCMorphism = [(OMName, OMImage)]
- type OMImage = Either String OMElement
- data OmdADT
- = ADTSortDef String ADTType [OmdADT]
- | ADTConstr String [OmdADT]
- | ADTArg OMElement (Maybe OmdADT)
- | ADTSelector String Totality
- | ADTInsort OMQualName
- 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
OMDoc root element with libname and a list of toplevel elements
Toplevel elements for OMDoc, theory with name, meta and content, view with from, to and morphism
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 Source #
return type for sentence translation (ADT or formula)
type TCMorphism = [(OMName, OMImage)] Source #
Morphisms to specify signature mappings
type OMImage = Either String OMElement Source #
The target type of a mapping is just an alias or an assignment to a symbol
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 SymbolRole Source #
Roles of the declared symbols can be object or type
Instances
| Eq SymbolRole Source # | |
Defined in OMDoc.DataTypes | |
| Ord SymbolRole Source # | |
Defined in OMDoc.DataTypes Methods compare :: SymbolRole -> SymbolRole -> Ordering (<) :: SymbolRole -> SymbolRole -> Bool (<=) :: SymbolRole -> SymbolRole -> Bool (>) :: SymbolRole -> SymbolRole -> Bool (>=) :: SymbolRole -> SymbolRole -> Bool max :: SymbolRole -> SymbolRole -> SymbolRole min :: SymbolRole -> SymbolRole -> SymbolRole | |
| Read SymbolRole Source # | |
Defined in OMDoc.DataTypes Methods readsPrec :: Int -> ReadS SymbolRole readList :: ReadS [SymbolRole] readPrec :: ReadPrec SymbolRole readListPrec :: ReadPrec [SymbolRole] | |
| Show SymbolRole Source # | |
Defined in OMDoc.DataTypes Methods showsPrec :: Int -> SymbolRole -> ShowS show :: SymbolRole -> String showList :: [SymbolRole] -> ShowS | |
Fixity of notation patterns
Associativity of notation patterns
Constructors
| LeftAssoc | |
| RightAssoc | |
| NoneAssoc |
Type of the algebraic data type
Totality for selectors of an adt
data NotationComponent Source #
A component can be a text-component, e.g., value="["/, or an argument-component such as index="1" precedence="p1"/
Instances
Names used for OpenMath variables and symbols
data OMAttribute Source #
Attribute-name/attribute-value pair used to represent the type of a type-annotated term
Instances
| Eq OMAttribute Source # | |
Defined in OMDoc.DataTypes | |
| Ord OMAttribute Source # | |
Defined in OMDoc.DataTypes Methods compare :: OMAttribute -> OMAttribute -> Ordering (<) :: OMAttribute -> OMAttribute -> Bool (<=) :: OMAttribute -> OMAttribute -> Bool (>) :: OMAttribute -> OMAttribute -> Bool (>=) :: OMAttribute -> OMAttribute -> Bool max :: OMAttribute -> OMAttribute -> OMAttribute min :: OMAttribute -> OMAttribute -> OMAttribute | |
| Read OMAttribute Source # | |
Defined in OMDoc.DataTypes Methods readsPrec :: Int -> ReadS OMAttribute readList :: ReadS [OMAttribute] readPrec :: ReadPrec OMAttribute readListPrec :: ReadPrec [OMAttribute] | |
| Show OMAttribute Source # | |
Defined in OMDoc.DataTypes Methods showsPrec :: Int -> OMAttribute -> ShowS show :: OMAttribute -> String showList :: [OMAttribute] -> ShowS | |
| XmlRepresentable OMAttribute Source # | Helper instance for OpenMath attributes |
Defined in OMDoc.XmlInterface Methods toXml :: OMAttribute -> Content Source # fromXml :: Element -> Result (Maybe OMAttribute) Source # | |
CD contains the reference to the content dictionary and eventually the cdbase entry
Constructors
| CD [String] |
type OMQualName = (OMCD, OMName) Source #
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 Source #
Utils for Translation
Mapping of symbols and sentence names to unique ids (used in export)
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 Source #
cdFromList :: [String] -> OMCD Source #
cdToMaybeList :: OMCD -> [Maybe String] Source #
Name handling: encoding, decoding, unique names
uniqPrefix :: String Source #
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]) Source #
This invariant should hold:
(x, l) = fromJust $ nameDecode $ nameEncode x l
nameToString :: UniqName -> String Source #
Constructing/Extracting Values
tcName :: TCElement -> OMName Source #
name of the theory constitutive element, error if not TCSymbol, TCNotation, or TCImport
unqualName :: OMQualName -> OMName Source #
mkSimpleName :: String -> OMName Source #
Lookup utils for Import and Export
lookupNotation :: SigMapI a -> OMName -> String Source #
lookupNotationInMap :: Map OMName String -> OMName -> String Source #