Copyright | (c) Hendrik Iben Uni Bremen 2005-2007 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | hiben@informatik.uni-bremen.de |
Stability | provisional |
Portability | non-portable |
Safe Haskell | Safe |
OMDoc.OMDocInterface
Description
Model of a handpicked subset from OMDoc
- omdocDefaultNamespace :: String
- type OMDocRef = IRI
- type OMDocRefs = [OMDocRef]
- showIRI :: IRI -> String
- mkOMDocRef :: String -> Maybe OMDocRef
- mkSymbolRef :: XmlId -> OMDocRef
- mkExtSymbolRef :: XmlId -> XmlId -> OMDocRef
- type XmlId = String
- type XmlString = String
- data OMDoc = OMDoc {
- omdocId :: XmlId
- omdocTheories :: [Theory]
- omdocInclusions :: [Inclusion]
- addTheories :: OMDoc -> [Theory] -> OMDoc
- addInclusions :: OMDoc -> [Inclusion] -> OMDoc
- data Theory = Theory {
- theoryId :: XmlId
- theoryConstitutives :: [Constitutive]
- theoryPresentations :: [Presentation]
- theoryComment :: Maybe String
- showTheory :: Theory -> String
- data ImportsType
- data Imports = Imports {
- importsFrom :: OMDocRef
- importsMorphism :: Maybe Morphism
- importsId :: Maybe XmlId
- importsType :: ImportsType
- importsConservativity :: Conservativity
- data Presentation = Presentation {
- presentationForId :: XmlId
- presentationSystem :: Maybe XmlString
- presentationUses :: [Use]
- mkPresentationS :: XmlId -> XmlString -> [Use] -> Presentation
- mkPresentation :: XmlId -> [Use] -> Presentation
- addUse :: Presentation -> Use -> Presentation
- data Use = Use {}
- mkUse :: XmlString -> String -> Use
- data SymbolRole
- data Symbol = Symbol {
- symbolGeneratedFrom :: Maybe XmlId
- symbolId :: XmlId
- symbolRole :: SymbolRole
- symbolType :: Maybe Type
- mkSymbolE :: Maybe XmlId -> XmlId -> SymbolRole -> Maybe Type -> Symbol
- mkSymbol :: XmlId -> SymbolRole -> Symbol
- data Type = Type {
- typeSystem :: Maybe IRI
- typeOMDocMathObject :: OMDocMathObject
- mkType :: Maybe OMDocRef -> OMDocMathObject -> Type
- data Constitutive
- mkCAx :: Axiom -> Constitutive
- mkCDe :: Definition -> Constitutive
- mkCSy :: Symbol -> Constitutive
- mkCIm :: Imports -> Constitutive
- mkCAd :: ADT -> Constitutive
- mkCCo :: String -> Constitutive -> Constitutive
- isAxiom :: Constitutive -> Bool
- isDefinition :: Constitutive -> Bool
- isSymbol :: Constitutive -> Bool
- isImports :: Constitutive -> Bool
- isADT :: Constitutive -> Bool
- isCommented :: Constitutive -> Bool
- getIdsForPresentation :: Constitutive -> [XmlId]
- data Axiom = Axiom {}
- mkAxiom :: XmlId -> [CMP] -> [FMP] -> Axiom
- data CMP = CMP {
- cmpContent :: MText
- mkCMP :: MText -> CMP
- data FMP = FMP {
- fmpLogic :: Maybe XmlString
- fmpContent :: Either OMObject ([Assumption], [Conclusion])
- data Assumption = Assumption
- data Conclusion = Conclusion
- data Definition = Definition {
- definitionId :: XmlId
- definitionCMPs :: [CMP]
- definitionFMPs :: [FMP]
- mkDefinition :: XmlId -> [CMP] -> [FMP] -> Definition
- data ADT = ADT {
- adtId :: Maybe XmlId
- adtSortDefs :: [SortDef]
- data SortType
- = STFree
- | STGenerated
- | STLoose
- mkADT :: [SortDef] -> ADT
- mkADTEx :: Maybe XmlId -> [SortDef] -> ADT
- data SortDef = SortDef {}
- mkSortDefE :: XmlId -> SymbolRole -> SortType -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
- mkSortDef :: XmlId -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
- data Constructor = Constructor {}
- mkConstructorE :: XmlId -> SymbolRole -> [Type] -> Constructor
- mkConstructor :: XmlId -> [Type] -> Constructor
- data Insort = Insort {}
- mkInsort :: OMDocRef -> Insort
- data Recognizer = Recognizer {}
- mkRecognizer :: XmlId -> Recognizer
- data Conservativity
- data Inclusion
- = TheoryInclusion {
- inclusionFrom :: OMDocRef
- inclusionTo :: OMDocRef
- inclusionMorphism :: Maybe Morphism
- inclusionId :: Maybe XmlId
- inclusionConservativity :: Conservativity
- | AxiomInclusion {
- inclusionFrom :: OMDocRef
- inclusionTo :: OMDocRef
- inclusionMorphism :: Maybe Morphism
- inclusionId :: Maybe XmlId
- inclusionConservativity :: Conservativity
- = TheoryInclusion {
- data Morphism = Morphism {
- morphismId :: Maybe XmlId
- morphismHiding :: [XmlId]
- morphismBase :: [XmlId]
- morphismRequations :: [(MText, MText)]
- data MText
- = MTextText String
- | MTextTerm String
- | MTextPhrase String
- | MTextOM OMObject
- data OMDocMathObject
- data OMObject = OMObject OMElement
- mkOMOBJ :: OMElementClass e => e -> OMObject
- data OMSymbol = OMS {}
- mkOMS :: Maybe OMDocRef -> XmlId -> XmlId -> OMSymbol
- mkOMSE :: Maybe OMDocRef -> XmlId -> XmlId -> OMElement
- data OMInteger = OMI {
- omiInt :: Int
- mkOMI :: Int -> OMInteger
- mkOMIE :: Int -> OMElement
- data OMVariable
- class OMVariableClass a where
- mkOMVar :: Either OMSimpleVariable OMAttribution -> OMVariable
- mkOMVarE :: Either OMSimpleVariable OMAttribution -> OMElement
- data OMSimpleVariable = OMV {}
- mkOMSimpleVar :: XmlString -> OMSimpleVariable
- mkOMSimpleVarE :: XmlString -> OMElement
- mkOMVSVar :: XmlString -> OMVariable
- mkOMVSVarE :: XmlString -> OMElement
- data OMAttribution = OMATTR {}
- mkOMATTR :: OMElementClass e => OMAttributionPart -> e -> OMAttribution
- mkOMATTRE :: OMElementClass e => OMAttributionPart -> e -> OMElement
- data OMAttributionPart = OMATP {
- omatpAttribs :: [(OMSymbol, OMElement)]
- mkOMATP :: OMElementClass e => [(OMSymbol, e)] -> OMAttributionPart
- data OMBindingVariables = OMBVAR {
- ombvarVars :: [OMVariable]
- mkOMBVAR :: OMVariableClass e => [e] -> OMBindingVariables
- data OMBase64 = OMB {
- ombContent :: [Word8]
- mkOMB :: [Word8] -> OMBase64
- mkOMBE :: [Word8] -> OMElement
- mkOMBWords :: [Word8] -> OMBase64
- mkOMBWordsE :: [Word8] -> OMElement
- getOMBWords :: OMBase64 -> [Word8]
- data OMString = OMSTR {
- omstrText :: String
- mkOMSTR :: String -> OMString
- mkOMSTRE :: String -> OMElement
- data OMFloat = OMF {
- omfFloat :: Float
- mkOMF :: Float -> OMFloat
- mkOMFE :: Float -> OMElement
- data OMApply = OMA {
- omaElements :: [OMElement]
- mkOMA :: OMElementClass e => [e] -> OMApply
- mkOMAE :: OMElementClass e => [e] -> OMElement
- data OMError = OME {}
- mkOME :: OMElementClass e => OMSymbol -> [e] -> OMError
- mkOMEE :: OMElementClass e => OMSymbol -> [e] -> OMElement
- data OMReference = OMR {}
- mkOMR :: IRI -> OMReference
- mkOMRE :: IRI -> OMElement
- data OMBind = OMBIND {}
- mkOMBIND :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMBind
- mkOMBINDE :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMElement
- data OMElement
- mkOMComment :: String -> OMElement
- mkOMCommented :: OMElementClass e => String -> e -> OMElement
- class OMElementClass a where
Documentation
omdocDefaultNamespace :: String Source #
mkOMDocRef :: String -> Maybe OMDocRef Source #
mkSymbolRef :: XmlId -> OMDocRef Source #
OMDoc
Constructors
OMDoc | |
Fields
|
Constructors
Theory | |
Fields
|
Instances
Eq Theory Source # | |
Data Theory Source # | |
Ord Theory Source # | |
Show Theory Source # | |
Pretty Theory Source # | |
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # | |
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # | |
Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source # | |
showTheory :: Theory -> String Source #
data ImportsType Source #
Type (scope) of import
Instances
Data ImportsType Source # | |
Show ImportsType Source # | |
Imports (for Theory)
Constructors
Imports | |
Fields
|
data Presentation Source #
Presentation
Constructors
Presentation | |
Fields
|
Instances
Eq Presentation Source # | |
Data Presentation Source # | |
Show Presentation Source # | |
mkPresentationS :: XmlId -> XmlString -> [Use] -> Presentation Source #
mkPresentation :: XmlId -> [Use] -> Presentation Source #
addUse :: Presentation -> Use -> Presentation Source #
Use for Presentation
data SymbolRole Source #
SymbolRole for Symbol
Constructors
SRType | |
SRSort | |
SRObject | |
SRBinder | |
SRAttribution | |
SRSemanticAttribution | |
SRError |
Instances
Eq SymbolRole Source # | |
Data SymbolRole Source # | |
Ord SymbolRole Source # | |
Read SymbolRole Source # | |
Show SymbolRole Source # | |
Symbol
Constructors
Symbol | |
Fields
|
Instances
Eq Symbol Source # | |
Data Symbol Source # | |
Ord Symbol Source # | |
Show Symbol Source # | |
GetRange Symbol Source # | |
Pretty Symbol Source # | |
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # | |
Syntax OMDoc_PUN () Symbol () () Source # | |
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # | |
Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source # | |
Type
Constructors
Type | |
Fields
|
data Constitutive Source #
OMDoc Theory constitutive elements + convenience additions (ADT)
Constructors
CAx Axiom | |
CDe Definition | |
CSy Symbol | |
CIm Imports | |
CAd ADT | |
CCo | |
Fields
|
Instances
Data Constitutive Source # | |
Show Constitutive Source # | |
mkCAx :: Axiom -> Constitutive Source #
mkCDe :: Definition -> Constitutive Source #
mkCSy :: Symbol -> Constitutive Source #
mkCIm :: Imports -> Constitutive Source #
mkCAd :: ADT -> Constitutive Source #
mkCCo :: String -> Constitutive -> Constitutive Source #
isAxiom :: Constitutive -> Bool Source #
isDefinition :: Constitutive -> Bool Source #
isSymbol :: Constitutive -> Bool Source #
isImports :: Constitutive -> Bool Source #
isADT :: Constitutive -> Bool Source #
isCommented :: Constitutive -> Bool Source #
getIdsForPresentation :: Constitutive -> [XmlId] Source #
Axiom
CMP
Constructors
CMP | |
Fields
|
FMP
Constructors
FMP | |
Fields
|
data Assumption Source #
Assumption (incomplete)
Constructors
Assumption |
Instances
Data Assumption Source # | |
Show Assumption Source # | |
data Conclusion Source #
Constructors
Conclusion |
Instances
Data Conclusion Source # | |
Show Conclusion Source # | |
data Definition Source #
Definition (incomplete)
Constructors
Definition | |
Fields
|
Instances
Data Definition Source # | |
Show Definition Source # | |
mkDefinition :: XmlId -> [CMP] -> [FMP] -> Definition Source #
ADT
Constructors
ADT | |
Fields
|
Constructors
STFree | |
STGenerated | |
STLoose |
SortDef
Constructors
SortDef | |
Fields
|
mkSortDefE :: XmlId -> SymbolRole -> SortType -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef Source #
mkSortDef :: XmlId -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef Source #
data Constructor Source #
Constructor
Constructors
Constructor | |
Fields |
Instances
Data Constructor Source # | |
Show Constructor Source # | |
mkConstructorE :: XmlId -> SymbolRole -> [Type] -> Constructor Source #
mkConstructor :: XmlId -> [Type] -> Constructor Source #
Insort
data Recognizer Source #
Recognizer
Constructors
Recognizer | |
Fields |
Instances
Data Recognizer Source # | |
Show Recognizer Source # | |
mkRecognizer :: XmlId -> Recognizer Source #
data Conservativity Source #
Inclusion-Conservativity
Constructors
CNone | |
CMonomorphism | |
CDefinitional | |
CConservative |
Instances
Eq Conservativity Source # | |
Data Conservativity Source # | |
Ord Conservativity Source # | |
Read Conservativity Source # | |
Show Conservativity Source # | |
Inclusions
Constructors
TheoryInclusion | |
Fields
| |
AxiomInclusion | |
Fields
|
Instances
Eq Inclusion Source # | |
Data Inclusion Source # | |
Ord Inclusion Source # | |
Show Inclusion Source # | |
Pretty Inclusion Source # | |
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol Source # | |
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () Source # | |
Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () Source # | |
OMDoc Morphism
Constructors
Morphism | |
Fields
|
Constructors
MTextText String | |
MTextTerm String | |
MTextPhrase String | |
MTextOM OMObject |
data OMDocMathObject Source #
Instances
Eq OMDocMathObject Source # | |
Data OMDocMathObject Source # | |
Ord OMDocMathObject Source # | |
Show OMDocMathObject Source # | |
OMOBJ
mkOMOBJ :: OMElementClass e => e -> OMObject Source #
OMS
OMI
data OMVariable Source #
A Variable can be a OMV or an OMATTR
Constructors
OMVS OMSimpleVariable | |
OMVA OMAttribution |
Instances
Eq OMVariable Source # | |
Data OMVariable Source # | |
Ord OMVariable Source # | |
Show OMVariable Source # | |
OMElementClass OMVariable Source # | |
OMVariableClass OMVariable Source # | |
class OMVariableClass a where Source #
Class to use something as a Variable
Minimal complete definition
mkOMVar :: Either OMSimpleVariable OMAttribution -> OMVariable Source #
mkOMVarE :: Either OMSimpleVariable OMAttribution -> OMElement Source #
mkOMSimpleVarE :: XmlString -> OMElement Source #
mkOMVSVar :: XmlString -> OMVariable Source #
mkOMVSVarE :: XmlString -> OMElement Source #
mkOMATTR :: OMElementClass e => OMAttributionPart -> e -> OMAttribution Source #
mkOMATTRE :: OMElementClass e => OMAttributionPart -> e -> OMElement Source #
data OMAttributionPart Source #
OMATP
Constructors
OMATP | |
Fields
|
Instances
Eq OMAttributionPart Source # | |
Data OMAttributionPart Source # | |
Ord OMAttributionPart Source # | |
Show OMAttributionPart Source # | |
mkOMATP :: OMElementClass e => [(OMSymbol, e)] -> OMAttributionPart Source #
data OMBindingVariables Source #
OMBVAR
Constructors
OMBVAR | |
Fields
|
Instances
Eq OMBindingVariables Source # | |
Data OMBindingVariables Source # | |
Ord OMBindingVariables Source # | |
Show OMBindingVariables Source # | |
mkOMBVAR :: OMVariableClass e => [e] -> OMBindingVariables Source #
OMB is actually just a bytearray for storing data. [Char] representation is forced by export from Codec.Base64
Constructors
OMB | |
Fields
|
mkOMBWords :: [Word8] -> OMBase64 Source #
mkOMBWordsE :: [Word8] -> OMElement Source #
getOMBWords :: OMBase64 -> [Word8] Source #
OMSTR
OMF
OMA
Constructors
OMA | |
Fields
|
mkOMA :: OMElementClass e => [e] -> OMApply Source #
mkOMAE :: OMElementClass e => [e] -> OMElement Source #
OME
data OMReference Source #
OMR
Instances
Eq OMReference Source # | |
Data OMReference Source # | |
Ord OMReference Source # | |
Show OMReference Source # | |
OMElementClass OMReference Source # | |
mkOMR :: IRI -> OMReference Source #
OMB
Constructors
OMBIND | |
Fields |
mkOMBIND :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMBind Source #
mkOMBINDE :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMElement Source #
Elements for Open Math
mkOMComment :: String -> OMElement Source #
insert a comment into an open-math structure (use with caution...)
mkOMCommented :: OMElementClass e => String -> e -> OMElement Source #
class OMElementClass a where Source #
Class of Elements for Open Math
Minimal complete definition
Instances