Hets - the Heterogeneous Tool Set

Copyright(c) Kristina Sojakova DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerk.sojakova@jacobs-university.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

LF.Twelf2GR

Description

 

Documentation

type NODE = (BASE, MODULE) Source #

type SIGS = Map MODULE Sign Source #

type LIBS = Map BASE GRAPH Source #

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

data Namespace Source #

Constructors

LATIN 
HETS 

latinEnv :: String Source #

twelfEnv :: String Source #

hetsEnv :: String 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 #

aliasQN :: QName Source #

typeQN :: 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 #

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 #

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 #