Documentation

type NODE = (BASE, MODULE) Source #

type LINK = (BASE, MODULE, NAME) Source #

type SIGS = Map MODULE Sign Source #

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

type GRAPH = (SIGS, MORPHS) Source #

type LIBS = Map BASE GRAPH Source #

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

data Namespace Source #

latinEnv :: String Source #

twelfEnv :: String Source #

hetsEnv :: String Source #

emptyGraph :: GRAPH Source #

omdocNS :: Maybe String Source #

openMathNS :: Maybe String Source #

lfBase :: String Source #

mmtBase :: String Source #

lfMod :: String Source #

mmtMod :: String Source #

omdocQN :: QName Source #

theoryQN :: QName Source #

viewQN :: QName Source #

includeQN :: QName Source #

structureQN :: QName Source #

constantQN :: QName Source #

aliasQN :: QName Source #

notationQN :: QName Source #

typeQN :: QName Source #

definitionQN :: QName Source #

omobjQN :: QName Source #

omsQN :: QName Source #

omaQN :: QName Source #

ombindQN :: QName Source #

ombvarQN :: QName Source #

omattrQN :: QName Source #

omatpQN :: QName Source #

omvQN :: QName Source #

ommorQN :: QName Source #

conassQN :: QName Source #

strassQN :: QName Source #

typeOMS :: Element Source #

arrowOMS :: Element Source #

lambdaOMS :: Element Source #

piOMS :: Element Source #

impLambdaOMS :: Element Source #

impPiOMS :: Element Source #

oftypeOMS :: Element Source #

compOMS :: Element Source #

nameQN :: QName Source #

moduleQN :: QName Source #

baseQN :: QName Source #

fromQN :: QName Source #

toQN :: QName Source #

omdocE :: String Source #

twelfE :: String Source #

twelf :: String Source #

options :: [String] Source #

getFromAttr :: Element -> String Source #

getToAttr :: Element -> String Source #

getNameAttr :: Element -> String Source #

getModuleAttr :: Element -> Maybe String Source #

getBaseAttr :: Element -> Maybe String Source #

eqOMS :: Element -> Element -> Bool Source #

toOMDoc :: FilePath -> FilePath Source #

toTwelf :: FilePath -> FilePath Source #

getEnv :: Namespace -> String Source #

getEnvVar :: String -> IO String Source #

resolve :: FilePath -> FilePath -> FilePath Source #

relativize :: FilePath -> FilePath -> FilePath Source #

toAbsoluteURI :: FilePath -> IO FilePath Source #

toRelativeURI :: FilePath -> IO FilePath Source #

toLibName :: Namespace -> FilePath -> IO BASE Source #

fromLibName :: Namespace -> BASE -> IO FilePath Source #

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

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

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

lookupSig :: NODE -> LIBS_EXT -> Sign Source #

lookupMorph :: LINK -> LIBS_EXT -> Morphism Source #

addSigToGraph :: Sign -> LIBS_EXT -> LIBS_EXT Source #

addMorphToGraph :: Morphism -> LIBS_EXT -> LIBS_EXT Source #

computeTargets :: GRAPH -> LIBS_EXT -> GRAPH Source #

twelf2SigMor :: Namespace -> FilePath -> IO LIBS Source #

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

runTwelf :: FilePath -> IO () Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

addInclSyms :: Sign -> Sign -> Sign Source #

getInclMorph :: Sign -> Sign -> Morphism Source #

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

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

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

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

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

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

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

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

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

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

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

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

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