hets/OMDoc/OMDocInterface.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./OMDoc/OMDocInterface.hs
Description :  Handpicked model of OMDoc subset
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

Model of a handpicked subset from OMDoc
-}
module OMDoc.OMDocInterface where

import qualified Common.IRI as IRI

import Data.Char
import Data.Data

import qualified Data.Word as Word

import Common.Doc
import Common.DocUtils
import Common.Id

omdocDefaultNamespace :: String
omdocDefaultNamespace = "http://www.mathweb.org/omdoc"

-- | OMDocRef is anyIRI
type OMDocRef = IRI.IRI

-- | OMDocRefs modelled as a list
type OMDocRefs = [OMDocRef]

showIRI :: IRI.IRI -> String
showIRI = IRI.iriToStringUnsecure

-- Try to parse an IRI
mkOMDocRef :: String -> Maybe OMDocRef
mkOMDocRef = IRI.parseIRIReference

mkSymbolRef :: XmlId -> OMDocRef
mkSymbolRef xid =
  case IRI.parseIRIReference ('#' : xid) of
    Nothing -> error ("Invalid Symbol-Id! (" ++ xid ++ ")")
    (Just u) -> u

mkExtSymbolRef :: XmlId -> XmlId -> OMDocRef
mkExtSymbolRef xcd xid =
  case IRI.parseIRIReference (xcd ++ "#" ++ xid) of
    Nothing -> error "Invalid Reference!"
    (Just u) -> u

-- OMDoc

-- | used for ids
type XmlId = String
-- | used for names, pcdata
type XmlString = String

-- | OMDoc
data OMDoc =
  OMDoc
    {
        omdocId :: XmlId
      , omdocTheories :: [Theory]
      , omdocInclusions :: [Inclusion]
    }
    deriving (Show, Typeable, Data)

addTheories :: OMDoc -> [Theory] -> OMDoc
addTheories omdoc theories =
  omdoc
    {
      omdocTheories = omdocTheories omdoc ++ theories
    }

addInclusions :: OMDoc -> [Inclusion] -> OMDoc
addInclusions omdoc inclusions =
  omdoc
    {
      omdocInclusions = omdocInclusions omdoc ++ inclusions
    }

-- Theory
data Theory =
  Theory
    {
        theoryId :: XmlId
      , theoryConstitutives :: [Constitutive]
      , theoryPresentations :: [Presentation]
      , theoryComment :: Maybe String
    }
    deriving (Show, Typeable, Data)

instance Pretty Theory where
  pretty t = text $
    show (theoryId t)
    ++
      case theoryComment t of
        Nothing -> ""
        (Just c) -> ": " ++ show c

instance Eq Theory where
  t1 == t2 = theoryId t1 == theoryId t2

instance Ord Theory where
  t1 `compare` t2 = theoryId t1 `compare` theoryId t2

-- debug
showTheory :: Theory -> String
showTheory t = show (t { theoryPresentations = [] })

-- | Type (scope) of import
data ImportsType = ITLocal | ITGlobal
  deriving (Show, Typeable, Data)

-- | Imports (for Theory)
data Imports =
  Imports
    {
        importsFrom :: OMDocRef
      , importsMorphism :: Maybe Morphism
      , importsId :: Maybe XmlId
      , importsType :: ImportsType
      , importsConservativity :: Conservativity
    }
    deriving (Show, Typeable, Data)

-- | Presentation
data Presentation =
  Presentation
    {
        presentationForId :: XmlId
      , presentationSystem :: Maybe XmlString
      , presentationUses :: [Use]
    }
    deriving (Show, Eq, Typeable, Data)

mkPresentationS :: XmlId -> XmlString -> [Use] -> Presentation
mkPresentationS forid presSystem = Presentation forid (Just presSystem)

mkPresentation :: XmlId -> [Use] -> Presentation
mkPresentation forid = Presentation forid Nothing

addUse :: Presentation -> Use -> Presentation
addUse pres use = pres { presentationUses = presentationUses pres ++ [use] }

-- | Use for Presentation
data Use =
  Use
    {
        useFormat :: XmlString
      , useValue :: String
    }
    deriving (Show, Eq, Typeable, Data)

mkUse :: XmlString -> String -> Use
mkUse = Use

-- | SymbolRole for Symbol
data SymbolRole =
    SRType
  | SRSort
  | SRObject
  | SRBinder
  | SRAttribution
  | SRSemanticAttribution
  | SRError
  deriving (Eq, Ord, Typeable, Data)

instance Show SymbolRole where
  show SRType = "type"
  show SRSort = "sort"
  show SRObject = "object"
  show SRBinder = "binder"
  show SRAttribution = "attribution"
  show SRSemanticAttribution = "semantic-attribution"
  show SRError = "error"

instance Read SymbolRole where
  readsPrec _ s =
    case map toLower s of
      "type" -> [(SRType, [])]
      "sort" -> [(SRSort, [])]
      "object" -> [(SRObject, [])]
      "binder" -> [(SRBinder, [])]
      "attribution" -> [(SRAttribution, [])]
      "semantic-attribution" -> [(SRSemanticAttribution, [])]
      "error" -> [(SRError, [])]
      _ -> []

-- | Symbol
data Symbol =
  Symbol
    {
        symbolGeneratedFrom :: Maybe XmlId
      , symbolId :: XmlId
      , symbolRole :: SymbolRole
      , symbolType :: Maybe Type
    }
    deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange Symbol

instance Pretty Symbol where
  pretty s =
   text $ show s

mkSymbolE :: Maybe XmlId -> XmlId -> SymbolRole -> Maybe Type -> Symbol
mkSymbolE = Symbol

mkSymbol :: XmlId -> SymbolRole -> Symbol
mkSymbol xid sr = mkSymbolE Nothing xid sr Nothing

-- | Type
data Type =
  Type
    {
        typeSystem :: Maybe IRI.IRI
      , typeOMDocMathObject :: OMDocMathObject
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkType :: Maybe OMDocRef -> OMDocMathObject -> Type
mkType = Type

{- |
  OMDoc Theory constitutive elements + convenience additions (ADT)
-}
data Constitutive =
    CAx Axiom
  | CDe Definition
  | CSy Symbol
  | CIm Imports
  | CAd ADT
  | CCo { conComCmt :: String, conComCon :: Constitutive }
  deriving (Show, Typeable, Data)

mkCAx :: Axiom -> Constitutive
mkCAx = CAx
mkCDe :: Definition -> Constitutive
mkCDe = CDe
mkCSy :: Symbol -> Constitutive
mkCSy = CSy
mkCIm :: Imports -> Constitutive
mkCIm = CIm
mkCAd :: ADT -> Constitutive
mkCAd = CAd
mkCCo :: String -> Constitutive -> Constitutive
mkCCo = CCo

isAxiom :: Constitutive -> Bool
isAxiom (CAx {}) = True
isAxiom _ = False

isDefinition :: Constitutive -> Bool
isDefinition (CDe {}) = True
isDefinition _ = False

isSymbol :: Constitutive -> Bool
isSymbol (CSy {}) = True
isSymbol _ = False

isImports :: Constitutive -> Bool
isImports (CIm {}) = True
isImports _ = False

isADT :: Constitutive -> Bool
isADT (CAd {}) = True
isADT _ = False

isCommented :: Constitutive -> Bool
isCommented (CCo {}) = True
isCommented _ = False

getIdsForPresentation :: Constitutive -> [XmlId]
getIdsForPresentation (CAx a) = [axiomName a]
getIdsForPresentation (CDe _) = []
getIdsForPresentation (CSy s) = [symbolId s]
getIdsForPresentation (CIm _) = []
getIdsForPresentation (CAd a) = map sortDefName (adtSortDefs a)
getIdsForPresentation (CCo {}) = []

-- | Axiom
data Axiom =
  Axiom
    {
        axiomName :: XmlId
      , axiomCMPs :: [CMP]
      , axiomFMPs :: [FMP]
    }
    deriving (Show, Typeable, Data)

mkAxiom :: XmlId -> [CMP] -> [FMP] -> Axiom
mkAxiom = Axiom

-- | CMP
data CMP =
  CMP
    {
      cmpContent :: MText
    }
  deriving (Show, Typeable, Data)

mkCMP :: MText -> CMP
mkCMP = CMP

-- | FMP
data FMP =
  FMP
    {
        fmpLogic :: Maybe XmlString
      , fmpContent :: Either OMObject ([Assumption], [Conclusion])
    }
  deriving (Show, Typeable, Data)

-- | Assumption (incomplete)
data Assumption = Assumption
  deriving (Show, Typeable, Data)

data Conclusion = Conclusion
  deriving (Show, Typeable, Data)

-- | Definition (incomplete)
data Definition =
  Definition
    {
        definitionId :: XmlId
      , definitionCMPs :: [CMP]
      , definitionFMPs :: [FMP]
    }
  deriving (Show, Typeable, Data)

mkDefinition :: XmlId -> [CMP] -> [FMP] -> Definition
mkDefinition = Definition

-- | ADT
data ADT =
  ADT
    {
        adtId :: Maybe XmlId
      , adtSortDefs :: [SortDef]
    }
  deriving (Show, Typeable, Data)

data SortType = STFree | STGenerated | STLoose deriving (Typeable, Data)

mkADT :: [SortDef] -> ADT
mkADT = ADT Nothing

mkADTEx :: Maybe XmlId -> [SortDef] -> ADT
mkADTEx = ADT

instance Show SortType where
  show STFree = "free"
  show STGenerated = "generated"
  show STLoose = "loose"

instance Read SortType where
  readsPrec _ s
   | s == "free" = [(STFree, "")]
   | s == "generated" = [(STGenerated, "")]
   | s == "loose" = [(STLoose, "")]
   | otherwise = []

-- | SortDef
data SortDef =
  SortDef
    {
        sortDefName :: XmlId
      , sortDefRole :: SymbolRole
      , sortDefType :: SortType
      , sortDefConstructors :: [Constructor]
      , sortDefInsorts :: [Insort]
      , sortDefRecognizers :: [Recognizer]
    }
  deriving (Show, Typeable, Data)

mkSortDefE :: XmlId -> SymbolRole -> SortType -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
mkSortDefE = SortDef

mkSortDef :: XmlId -> [Constructor] -> [Insort] -> [Recognizer] -> SortDef
mkSortDef xid = mkSortDefE xid SRSort STFree

-- | Constructor
data Constructor =
  Constructor
    {
        constructorName :: XmlId
      , constructorRole :: SymbolRole
      , constructorArguments :: [Type]
    }
  deriving (Show, Typeable, Data)

mkConstructorE :: XmlId -> SymbolRole -> [Type] -> Constructor
mkConstructorE = Constructor

mkConstructor :: XmlId -> [Type] -> Constructor
mkConstructor xid = Constructor xid SRObject

-- | Insort
data Insort =
  Insort
    {
      insortFor :: OMDocRef
    }
  deriving (Show, Typeable, Data)

mkInsort :: OMDocRef -> Insort
mkInsort = Insort

-- | Recognizer
data Recognizer =
  Recognizer
    {
      recognizerName :: XmlId
    }
  deriving (Show, Typeable, Data)

mkRecognizer :: XmlId -> Recognizer
mkRecognizer = Recognizer

-- | Inclusion-Conservativity
data Conservativity = CNone | CMonomorphism | CDefinitional | CConservative
  deriving (Eq, Ord, Typeable, Data)

instance Show Conservativity where
  show CNone = "none"
  show CMonomorphism = "monomorphism"
  show CDefinitional = "definitional"
  show CConservative = "conservative"

instance Read Conservativity where
  readsPrec _ s =
    case s of
      "monomorphism" -> [(CMonomorphism, "")]
      "definitional" -> [(CDefinitional, "")]
      "conservative" -> [(CConservative, "")]
      "none" -> [(CNone, "")]
      _ -> []

-- | Inclusions
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
      }
  deriving (Show, Eq, Ord, Typeable, Data)

instance Pretty Inclusion where
  pretty = text . show

-- | OMDoc Morphism
data Morphism =
  Morphism
    {
        morphismId :: Maybe XmlId
      , morphismHiding :: [XmlId]
      , morphismBase :: [XmlId]
      , morphismRequations :: [ ( MText, MText ) ]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

instance Pretty Morphism where
  pretty m = text $ show m

-- Mathematical Text (incomplete)
data MText = MTextText String | MTextTerm String | MTextPhrase String | MTextOM OMObject
  deriving (Show, Eq, Ord, Typeable, Data)

-- OMDoc Mathematical Object
data OMDocMathObject = OMOMOBJ OMObject | OMLegacy String | OMMath String
  deriving (Show, Eq, Ord, Typeable, Data)

-- | OMOBJ
data OMObject = OMObject OMElement
  deriving (Show, Eq, Ord, Typeable, Data)

mkOMOBJ :: OMElementClass e => e -> OMObject
mkOMOBJ e = OMObject (toElement e)

-- | OMS
data OMSymbol =
  OMS
    {
        omsCDBase :: Maybe OMDocRef
      , omsCD :: XmlId
      , omsName :: XmlId
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMS :: Maybe OMDocRef -> XmlId -> XmlId -> OMSymbol
mkOMS = OMS

mkOMSE :: Maybe OMDocRef -> XmlId -> XmlId -> OMElement
mkOMSE mref xcd xid = toElement $ mkOMS mref xcd xid

-- | OMI
data OMInteger =
  OMI
    {
      omiInt :: Int
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMI :: Int -> OMInteger
mkOMI = OMI

mkOMIE :: Int -> OMElement
mkOMIE i = toElement $ mkOMI i

-- | A Variable can be a OMV or an OMATTR
data OMVariable = OMVS OMSimpleVariable | OMVA OMAttribution
    deriving (Show, Eq, Ord, Typeable, Data)

-- | Class to use something as a Variable
class OMVariableClass a where
  toVariable :: a -> OMVariable
  fromVariable :: OMVariable -> Maybe a

instance OMVariableClass OMVariable where
  toVariable = id
  fromVariable = Just . id

instance OMVariableClass OMSimpleVariable where
  toVariable = OMVS
  fromVariable (OMVS x) = Just x
  fromVariable _ = Nothing

mkOMVar :: Either OMSimpleVariable OMAttribution -> OMVariable
mkOMVar (Left oms) = OMVS oms
mkOMVar (Right omattr) = OMVA omattr

mkOMVarE :: Either OMSimpleVariable OMAttribution -> OMElement
mkOMVarE v = toElement $ mkOMVar v

-- | OMV
data OMSimpleVariable =
  OMV
    {
      omvName :: XmlString
    }
    deriving (Show, Eq, Ord, Typeable, Data)


mkOMSimpleVar :: XmlString -> OMSimpleVariable
mkOMSimpleVar = OMV

mkOMSimpleVarE :: XmlString -> OMElement
mkOMSimpleVarE xid = toElement $ mkOMSimpleVar xid

mkOMVSVar :: XmlString -> OMVariable
mkOMVSVar = OMVS . mkOMSimpleVar

mkOMVSVarE :: XmlString -> OMElement
mkOMVSVarE xid = toElement $ OMVS $ mkOMSimpleVar xid

-- | OMATTR
data OMAttribution =
  OMATTR
    {
        omattrATP :: OMAttributionPart
      , omattrElem :: OMElement
    }
    deriving (Show, Eq, Ord, Typeable, Data)

instance OMVariableClass OMAttribution where
  toVariable = OMVA
  fromVariable (OMVA x) = Just x
  fromVariable _ = Nothing

mkOMATTR :: OMElementClass e => OMAttributionPart -> e -> OMAttribution
mkOMATTR omatp ome = OMATTR { omattrATP = omatp , omattrElem = toElement ome }

mkOMATTRE :: OMElementClass e => OMAttributionPart -> e -> OMElement
mkOMATTRE omatp ome = toElement $ mkOMATTR omatp ome

-- | OMATP
data OMAttributionPart =
  OMATP
    {
      omatpAttribs :: [(OMSymbol, OMElement)]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMATP :: OMElementClass e => [(OMSymbol, e)] -> OMAttributionPart
mkOMATP = OMATP . map (\ (s, e) -> (s, toElement e))

-- | OMBVAR
data OMBindingVariables =
  OMBVAR
    {
      ombvarVars :: [OMVariable]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMBVAR :: OMVariableClass e => [e] -> OMBindingVariables
mkOMBVAR = OMBVAR . map toVariable

{- |
  OMB is actually just a bytearray for storing data.
  [Char] representation is forced by export from Codec.Base64
-}
data OMBase64 =
  OMB
    {
      -- decoded Content
      ombContent :: [Word.Word8]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMB :: [Word.Word8] -> OMBase64
mkOMB = OMB

mkOMBE :: [Word.Word8] -> OMElement
mkOMBE = toElement . mkOMB

mkOMBWords :: [Word.Word8] -> OMBase64
mkOMBWords = OMB

mkOMBWordsE :: [Word.Word8] -> OMElement
mkOMBWordsE = toElement . mkOMBWords

getOMBWords :: OMBase64 -> [Word.Word8]
getOMBWords = ombContent

-- | OMSTR
data OMString =
  OMSTR
    {
      omstrText :: String
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMSTR :: String -> OMString
mkOMSTR = OMSTR

mkOMSTRE :: String -> OMElement
mkOMSTRE = toElement . mkOMSTR

-- | OMF
data OMFloat =
  OMF
    {
      omfFloat :: Float
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMF :: Float -> OMFloat
mkOMF = OMF

mkOMFE :: Float -> OMElement
mkOMFE = toElement . mkOMF

-- | OMA
data OMApply =
  OMA
    {
      omaElements :: [OMElement]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMA :: OMElementClass e => [e] -> OMApply
mkOMA [] = error "Empty list of elements for OMA!"
mkOMA l = OMA (map toElement l)

mkOMAE :: OMElementClass e => [e] -> OMElement
mkOMAE = toElement . mkOMA

-- | OME
data OMError =
  OME
    {
        omeSymbol :: OMSymbol
      , omeExtra :: [OMElement]
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOME :: OMElementClass e => OMSymbol -> [e] -> OMError
mkOME _ [] = error "Empty list of elements for OME!"
mkOME s e = OME s (map toElement e)

mkOMEE :: OMElementClass e => OMSymbol -> [e] -> OMElement
mkOMEE s e = toElement $ mkOME s e

-- | OMR
data OMReference =
  OMR
    {
      omrHRef :: IRI.IRI
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMR :: IRI.IRI -> OMReference
mkOMR = OMR

mkOMRE :: IRI.IRI -> OMElement
mkOMRE = toElement . mkOMR

-- | OMB
data OMBind =
  OMBIND
    {
        ombindBinder :: OMElement
      , ombindVariables :: OMBindingVariables
      , ombindExpression :: OMElement
    }
    deriving (Show, Eq, Ord, Typeable, Data)

mkOMBIND :: (OMElementClass e1, OMElementClass e2)
  => e1 -> OMBindingVariables -> e2 -> OMBind
mkOMBIND binder bvars expr =
  OMBIND
    {
        ombindBinder = toElement binder
     , ombindVariables = bvars
      , ombindExpression = toElement expr
    }

mkOMBINDE :: (OMElementClass e1, OMElementClass e2)
  => e1 -> OMBindingVariables -> e2 -> OMElement
mkOMBINDE binder vars expr = toElement $ mkOMBIND binder vars expr

-- | Elements for Open Math
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
  deriving (Show, Eq, Ord, Typeable, Data)

-- | insert a comment into an open-math structure (use with caution...)
mkOMComment :: String -> OMElement
mkOMComment = OMEC Nothing

mkOMCommented :: OMElementClass e => String -> e -> OMElement
mkOMCommented cmt e = OMEC (Just (toElement e)) cmt

-- | Class of Elements for Open Math
class OMElementClass a where
  toElement :: a -> OMElement
  fromElement :: OMElement -> Maybe a

instance OMElementClass OMSymbol where
  toElement = OMES
  fromElement (OMES oms) = Just oms
  fromElement _ = Nothing

instance OMElementClass OMInteger where
  toElement = OMEI
  fromElement (OMEI x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMVariable where
  toElement (OMVS omv) = OMEV omv
  toElement (OMVA omattr) = OMEATTR omattr
  fromElement (OMEV omv) = Just (OMVS omv)
  fromElement (OMEATTR omattr) = Just (OMVA omattr)
  fromElement _ = Nothing

instance OMElementClass OMSimpleVariable where
  toElement = OMEV
  fromElement (OMEV omv) = Just omv
  fromElement _ = Nothing

instance OMElementClass OMAttribution where
  toElement = OMEATTR
  fromElement (OMEATTR x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMBase64 where
  toElement = OMEB
  fromElement (OMEB x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMString where
  toElement = OMESTR
  fromElement (OMESTR x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMFloat where
  toElement = OMEF
  fromElement (OMEF x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMApply where
  toElement = OMEA
  fromElement (OMEA x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMError where
  toElement = OMEE
  fromElement (OMEE x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMReference where
  toElement = OMER
  fromElement (OMER x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMBind where
  toElement = OMEBIND
  fromElement (OMEBIND x) = Just x
  fromElement _ = Nothing

instance OMElementClass OMElement where
  toElement = id
  fromElement = Just . id