Documentation

type NODE = (BASE, MODULE)

type LINK = (BASE, MODULE, NAME)

type SIGS = Map MODULE Sign

type MORPHS = Map ((MODULE, NAME), NODE, NODE) Morphism

type GRAPH = (SIGS, MORPHS)

type LIBS = Map BASE GRAPH

type LIBS_EXT = ((LIBS, [BASE]), (BASE, GRAPH))

data Namespace

latinEnv :: String

twelfEnv :: String

hetsEnv :: String

emptyGraph :: GRAPH

omdocNS :: Maybe String

openMathNS :: Maybe String

lfBase :: String

mmtBase :: String

lfMod :: String

mmtMod :: String

omdocQN :: QName

theoryQN :: QName

viewQN :: QName

includeQN :: QName

structureQN :: QName

constantQN :: QName

aliasQN :: QName

notationQN :: QName

typeQN :: QName

definitionQN :: QName

omobjQN :: QName

omsQN :: QName

omaQN :: QName

ombindQN :: QName

ombvarQN :: QName

omattrQN :: QName

omatpQN :: QName

omvQN :: QName

ommorQN :: QName

conassQN :: QName

strassQN :: QName

typeOMS :: Element

arrowOMS :: Element

lambdaOMS :: Element

piOMS :: Element

impLambdaOMS :: Element

impPiOMS :: Element

oftypeOMS :: Element

compOMS :: Element

nameQN :: QName

moduleQN :: QName

baseQN :: QName

fromQN :: QName

toQN :: QName

omdocE :: String

twelfE :: String

twelf :: String

options :: [String]

getFromAttr :: Element -> String

getToAttr :: Element -> String

getNameAttr :: Element -> String

getModuleAttr :: Element -> Maybe String

getBaseAttr :: Element -> Maybe String

eqOMS :: Element -> Element -> Bool

toOMDoc :: FilePath -> FilePath

toTwelf :: FilePath -> FilePath

getEnv :: Namespace -> String

getEnvVar :: String -> IO String

resolve :: FilePath -> FilePath -> FilePath

relativize :: FilePath -> FilePath -> FilePath

toAbsoluteURI :: FilePath -> IO FilePath

toRelativeURI :: FilePath -> IO FilePath

toLibName :: Namespace -> FilePath -> IO BASE

fromLibName :: Namespace -> BASE -> IO FilePath

parseRef :: Namespace -> String -> String -> IO NODE

getBMN :: Namespace -> Element -> NODE -> IO (BASE, MODULE, NAME)

addFromFile :: Namespace -> FilePath -> LIBS_EXT -> IO LIBS_EXT

lookupSig :: NODE -> LIBS_EXT -> Sign

lookupMorph :: LINK -> LIBS_EXT -> Morphism

addSigToGraph :: Sign -> LIBS_EXT -> LIBS_EXT

addMorphToGraph :: Morphism -> LIBS_EXT -> LIBS_EXT

computeTargets :: GRAPH -> LIBS_EXT -> GRAPH

twelf2SigMor :: Namespace -> FilePath -> IO LIBS

twelf2GR :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO (LIBS, [BASE])

runTwelf :: FilePath -> IO ()

buildGraph :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO LIBS_EXT

addSign :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT

addView :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT

getViewMorph :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

addConst :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)

type2exp :: Namespace -> Element -> NODE -> IO EXP

definition2exp :: Namespace -> Element -> NODE -> IO EXP

omobj2exp :: Namespace -> Element -> NODE -> IO EXP

omel2exp :: Namespace -> Element -> NODE -> IO EXP

oms2exp :: Namespace -> Element -> NODE -> IO EXP

oma2exp :: Namespace -> Element -> NODE -> IO EXP

ombind2exp :: Namespace -> Element -> NODE -> IO EXP

ombvar2decls :: Namespace -> Element -> NODE -> IO CONTEXT

omattr2vardecl :: Namespace -> Element -> NODE -> IO (VAR, EXP)

omatp2exp :: Namespace -> Element -> NODE -> IO EXP

omv2exp :: Namespace -> Element -> NODE -> IO EXP

addIncl :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)

addInclSyms :: Sign -> Sign -> Sign

getInclMorph :: Sign -> Sign -> Morphism

addStruct :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)

processStruct :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT -> IO (Sign, Morphism, LIBS_EXT)

constructMap :: Namespace -> [Element] -> NODE -> NODE -> LIBS_EXT -> IO (Map Symbol EXP, LIBS_EXT)

conass2map :: Namespace -> Element -> (Map Symbol EXP, LIBS_EXT) -> NODE -> NODE -> IO (Map Symbol EXP, LIBS_EXT)

incl2map :: Namespace -> Element -> (Map Symbol EXP, LIBS_EXT) -> NODE -> NODE -> IO (Map Symbol EXP, LIBS_EXT)

strass2map :: Namespace -> Element -> (Map Symbol EXP, LIBS_EXT) -> NODE -> NODE -> IO (Map Symbol EXP, LIBS_EXT)

ommor2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

omel2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

oms2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

oma2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

retrieveMorph :: Namespace -> LINK -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

retrieveMorphH :: Namespace -> BASE -> MODULE -> [NAME] -> LIBS_EXT -> IO (Morphism, LIBS_EXT)

combineMorphs :: Morphism -> Morphism -> Map Symbol EXP