OMDoc.OMDocInterface

Description

Synopsis

• 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
  • = ITLocal
  • | ITGlobal
• 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 {
  • useFormat :: XmlString
  • useValue :: String
  }
• mkUse :: XmlString -> String -> Use
• data SymbolRole
  • = SRType
  • | SRSort
  • | SRObject
  • | SRBinder
  • | SRAttribution
  • | SRSemanticAttribution
  • | SRError
• 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
  • = CAx Axiom
  • | CDe Definition
  • | CSy Symbol
  • | CIm Imports
  • | CAd ADT
  • | CCo {
    • conComCmt :: String
    • conComCon :: 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 {
  • axiomName :: XmlId
  • axiomCMPs :: [CMP]
  • axiomFMPs :: [FMP]
  }
• 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 {
  • sortDefName :: XmlId
  • sortDefRole :: SymbolRole
  • sortDefType :: SortType
  • sortDefConstructors :: [Constructor]
  • sortDefInsorts :: [Insort]
  • sortDefRecognizers :: [Recognizer]
  }
• mkSortDefE :: XmlId -> SymbolRole -> SortType -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
• mkSortDef :: XmlId -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
• data Constructor = Constructor {
  • constructorName :: XmlId
  • constructorRole :: SymbolRole
  • constructorArguments :: [Type]
  }
• mkConstructorE :: XmlId -> SymbolRole -> [Type] -> Constructor
• mkConstructor :: XmlId -> [Type] -> Constructor
• data Insort = Insort {
  • insortFor :: OMDocRef
  }
• mkInsort :: OMDocRef -> Insort
• data Recognizer = Recognizer {
  • recognizerName :: XmlId
  }
• mkRecognizer :: XmlId -> Recognizer
• data Conservativity
  • = CNone
  • | CMonomorphism
  • | CDefinitional
  • | CConservative
• 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
    }
• 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
  • = OMOMOBJ OMObject
  • | OMLegacy String
  • | OMMath String
• data OMObject = OMObject OMElement
• mkOMOBJ :: OMElementClass e => e -> OMObject
• data OMSymbol = OMS {
  • omsCDBase :: Maybe OMDocRef
  • omsCD :: XmlId
  • omsName :: XmlId
  }
• 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
  • = OMVS OMSimpleVariable
  • | OMVA OMAttribution
• class OMVariableClass a where
  • toVariable :: a -> OMVariable
  • fromVariable :: OMVariable -> Maybe a
• mkOMVar :: Either OMSimpleVariable OMAttribution -> OMVariable
• mkOMVarE :: Either OMSimpleVariable OMAttribution -> OMElement
• data OMSimpleVariable = OMV {
  • omvName :: XmlString
  }
• mkOMSimpleVar :: XmlString -> OMSimpleVariable
• mkOMSimpleVarE :: XmlString -> OMElement
• mkOMVSVar :: XmlString -> OMVariable
• mkOMVSVarE :: XmlString -> OMElement
• data OMAttribution = OMATTR {
  • omattrATP :: OMAttributionPart
  • omattrElem :: OMElement
  }
• 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 {
  • omeSymbol :: OMSymbol
  • omeExtra :: [OMElement]
  }
• mkOME :: OMElementClass e => OMSymbol -> [e] -> OMError
• mkOMEE :: OMElementClass e => OMSymbol -> [e] -> OMElement
• data OMReference = OMR {
  • omrHRef :: IRI
  }
• mkOMR :: IRI -> OMReference
• mkOMRE :: IRI -> OMElement
• data OMBind = OMBIND {
  • ombindBinder :: OMElement
  • ombindVariables :: OMBindingVariables
  • ombindExpression :: OMElement
  }
• mkOMBIND :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMBind
• mkOMBINDE :: (OMElementClass e1, OMElementClass e2) => e1 -> OMBindingVariables -> e2 -> OMElement
• data OMElement
  • = OMES OMSymbol
  • | OMEV OMSimpleVariable
  • | OMEI OMInteger
  • | OMEB OMBase64
  • | OMESTR OMString
  • | OMEF OMFloat
  • | OMEA OMApply
  • | OMEBIND OMBind
  • | OMEE OMError
  • | OMEATTR OMAttribution
  • | OMER OMReference
  • | OMEC (Maybe OMElement) String
• mkOMComment :: String -> OMElement
• mkOMCommented :: OMElementClass e => String -> e -> OMElement
• class OMElementClass a where
  • toElement :: a -> OMElement
  • fromElement :: OMElement -> Maybe a

Documentation