{- |
Module : ./LF/Twelf2GR.hs
Description : Conversion of Twelf files to LF signatures and morphisms
Copyright : (c) Kristina Sojakova, DFKI Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : k.sojakova@jacobs-university.de
Stability : experimental
Portability : portable
-}
module LF.Twelf2GR where
import System.Exit
import System.Process
import System.Directory
import System.FilePath
import System.IO (hGetContents)
import LF.Sign
import LF.Morphism
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe (fromMaybe)
import Common.IRI
import Common.Result
import Common.Utils
import Common.Keywords
import Control.Monad
import Text.XML.Light.Input
import Text.XML.Light.Types
import Text.XML.Light.Proc
type NODE = (BASE, MODULE)
type LINK = (BASE, MODULE, NAME)
type SIGS = Map.Map MODULE Sign
type MORPHS = Map.Map ((MODULE, NAME), NODE, NODE) Morphism
type GRAPH = (SIGS, MORPHS)
type LIBS = Map.Map BASE GRAPH
type LIBS_EXT = ((LIBS, [BASE]), (BASE, GRAPH))
data Namespace = LATIN | HETS
latinEnv :: String
latinEnv = "LATIN_LIB"
twelfEnv :: String
twelfEnv = "TWELF_LIB"
hetsEnv :: String
hetsEnv = "HETS_HOME"
emptyGraph :: GRAPH
omdocNS :: Maybe String
omdocNS = Just "http://omdoc.org/ns"
openMathNS :: Maybe String
openMathNS = Just "http://www.openmath.org/OpenMath"
lfBase :: String
lfBase = "http://cds.omdoc.org/foundations/lf/lf.omdoc"
mmtBase :: String
mmtBase = "http://cds.omdoc.org/omdoc/mmt.omdoc"
lfMod :: String
lfMod = "lf"
mmtMod :: String
mmtMod = "mmt"
omdocQN :: QName
omdocQN = QName "omdoc" omdocNS Nothing
theoryQN :: QName
theoryQN = QName "theory" omdocNS Nothing
viewQN :: QName
viewQN = QName "view" omdocNS Nothing
includeQN :: QName
includeQN = QName "include" omdocNS Nothing
structureQN :: QName
structureQN = QName "structure" omdocNS Nothing
constantQN :: QName
constantQN = QName "constant" omdocNS Nothing
aliasQN :: QName
aliasQN = QName "alias" omdocNS Nothing
notationQN :: QName
notationQN = QName "notation" omdocNS Nothing
typeQN :: QName
typeQN = QName "type" omdocNS Nothing
definitionQN :: QName
definitionQN = QName "definition" omdocNS Nothing
omobjQN :: QName
omobjQN = QName "OMOBJ" openMathNS Nothing
omsQN :: QName
omsQN = QName "OMS" openMathNS Nothing
omaQN :: QName
omaQN = QName "OMA" openMathNS Nothing
ombindQN :: QName
ombindQN = QName "OMBIND" openMathNS Nothing
ombvarQN :: QName
ombvarQN = QName "OMBVAR" openMathNS Nothing
omattrQN :: QName
omattrQN = QName "OMATTR" openMathNS Nothing
omatpQN :: QName
omatpQN = QName "OMATP" openMathNS Nothing
omvQN :: QName
omvQN = QName "OMV" openMathNS Nothing
ommorQN :: QName
ommorQN = QName "OMMOR" omdocNS Nothing
conassQN :: QName
conassQN = QName "conass" omdocNS Nothing
strassQN :: QName
strassQN = QName "strass" omdocNS Nothing
typeOMS :: Element
typeOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "type"] [] Nothing
arrowOMS :: Element
arrowOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "arrow"] [] Nothing
lambdaOMS :: Element
lambdaOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "lambda"] [] Nothing
piOMS :: Element
piOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "Pi"] [] Nothing
impLambdaOMS :: Element
impLambdaOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "implicit_lambda"] [] Nothing
impPiOMS :: Element
impPiOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "implicit_Pi"] [] Nothing
oftypeOMS :: Element
oftypeOMS =
Element omsQN [Attr baseQN lfBase,
Attr moduleQN lfMod,
Attr nameQN "oftype"] [] Nothing
compOMS :: Element
compOMS =
Element omsQN [Attr baseQN mmtBase,
Attr moduleQN mmtMod,
Attr nameQN "composition"] [] Nothing
nameQN :: QName
nameQN = QName "name" Nothing Nothing
moduleQN :: QName
moduleQN = QName "module" Nothing Nothing
baseQN :: QName
baseQN = QName "base" Nothing Nothing
fromQN :: QName
fromQN = QName "from" Nothing Nothing
toQN :: QName
toQN = QName "to" Nothing Nothing
omdocE :: String
omdocE = "omdoc"
twelfE :: String
twelfE = "elf"
-- path to the Twelf folder must be set in the environment variable TWELF_LIB
twelf :: String
twelf = "check-some"
options :: [String]
options = ["-omdoc"]
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
HELPER FUNCTIONS -}
getFromAttr :: Element -> String
getFromAttr e = fromMaybe (error "Element is missing a \"from\" attribute.") $
findAttr fromQN e
getToAttr :: Element -> String
getToAttr e = fromMaybe (error "Element is missing a \"to\" attribute.") $
findAttr toQN e
getNameAttr :: Element -> String
getNameAttr e = fromMaybe (error $ "Element is missing a name." ++ show e) $
findAttr nameQN e
getModuleAttr :: Element -> Maybe String
getModuleAttr = findAttr moduleQN
getBaseAttr :: Element -> Maybe String
getBaseAttr = findAttr baseQN
-- compares two OMS elements
eqOMS :: Element -> Element -> Bool
eqOMS e1 e2 = not $ elName e1 /= omsQN || elName e2 /= omsQN
{- and [ getNameAttr e1 == getNameAttr e2
, getModuleAttr e1 == getModuleAttr e2
, getBaseAttr e1 == getBaseAttr e2] -}
toOMDoc :: FilePath -> FilePath
toOMDoc fp = replaceExtension fp omdocE
toTwelf :: FilePath -> FilePath
toTwelf fp = replaceExtension fp twelfE
getEnv :: Namespace -> String
getEnv ns =
case ns of
LATIN -> latinEnv
HETS -> hetsEnv
getEnvVar :: String -> IO String
getEnvVar var = do
val <- getEnvDef var ""
if null val
then error $ "environment variable " ++ var ++ " is not set."
else return val
-- resolves the first file path wrt to the second
resolve :: FilePath -> FilePath -> FilePath
resolve fp1 fp2 =
case parseIRIReference fp1 of
Nothing -> er
Just uri1 ->
case parseIRIReference fp2 of
Nothing -> er
Just uri2 ->
case relativeTo uri1 uri2 of
Nothing -> er
Just f -> show f
where er = error "Invalid file name."
-- relativizes the first file path wrt to the second
relativize :: FilePath -> FilePath -> FilePath
relativize fp1 fp2 =
case parseIRIReference fp1 of
Nothing -> er
Just uri1 ->
case parseIRIReference fp2 of
Nothing -> er
Just uri2 -> show $ relativeFrom uri1 uri2
where er = error "Invalid file name."
-- resolves the file path wrt to the current directory
toAbsoluteURI :: FilePath -> IO FilePath
toAbsoluteURI fp = do
dir <- getCurrentDirectory
return $ resolve fp $ dir ++ "/"
-- relativizes an absolute file path wrt to the current directory
toRelativeURI :: FilePath -> IO FilePath
toRelativeURI fp = do
dir <- getCurrentDirectory
return $ relativize fp $ dir ++ "/"
{- converts a filepath to a library name, i.e.
relativizes w.r.t. the LATIN_HOME env variable -}
toLibName :: Namespace -> FilePath -> IO BASE
toLibName ns fp = do
file <- toAbsoluteURI fp
dir <- getEnvVar $ getEnv ns
return $ relativize file $ dir ++ "/"
{- converts a library name to a filepath, i.e.
resolves w.r.t. the LATIN_HOME env variable -}
fromLibName :: Namespace -> BASE -> IO FilePath
fromLibName ns lname = do
dir <- getEnvVar $ getEnv ns
return $ resolve lname $ dir ++ "/"
{- returns the referenced base and module resolved w.r.t.
the second argument -}
parseRef :: Namespace -> String -> String -> IO NODE
parseRef ns ref base = do
file <- fromLibName ns base
case splitBy '?' ref of
[br, m] -> do let b = toTwelf $ resolve br file
lname <- toLibName ns b
return (lname, m)
_ -> fail "Invalid reference."
{- retrieves the base, module, and name attributes resolved w.r.t.
the second argument -}
getBMN :: Namespace -> Element -> NODE -> IO (BASE, MODULE, NAME)
getBMN ns e (base, modul) = do
file <- fromLibName ns base
let n = fromMaybe "" $ findAttr nameQN e
let m = fromMaybe modul $ getModuleAttr e
let b = fromMaybe file $ getBaseAttr e
lname <- toLibName ns b
return (lname, m, n)
{- parses the referenced file if needed and imports all signatures
and morphisms from it -}
addFromFile :: Namespace -> FilePath -> LIBS_EXT -> IO LIBS_EXT
addFromFile ns lname libs@(lb@(l, _), (b, gr)) =
if lname == b || Map.member lname l
then return libs
else do file <- fromLibName ns lname
lb' <- twelf2GR ns file lb
return (lb', (b, gr))
-- finds the signature by base and module
lookupSig :: NODE -> LIBS_EXT -> Sign
lookupSig (b, m) ((libs, _), (base, (sigs, _))) =
let sigs1 = if b == base then sigs else
fst $ Map.findWithDefault er b libs
in Map.findWithDefault er m sigs1
where er = error "Signature cannot be found."
-- finds the morphism by base, module, and name
lookupMorph :: LINK -> LIBS_EXT -> Morphism
lookupMorph (b, m, n) ((libs, _), (base, (_, morphs))) =
let morphs1 = if b == base then morphs else
snd $ Map.findWithDefault er b libs
morphs2 = Map.filterWithKey (\ (l, _, _) _ -> l == (m, n)) morphs1
in case Map.toList morphs2 of
[(_, morph)] -> morph
_ -> er
where er = error "Morphism cannot be found."
-- adds the signature to the signature collection
addSigToGraph :: Sign -> LIBS_EXT -> LIBS_EXT
addSigToGraph sig (lb, (b, (sigs, morphs))) =
let sigs1 = Map.insert (sigModule sig) sig sigs
in (lb, (b, (sigs1, morphs)))
-- adds the morphism to the morphism collection
addMorphToGraph :: Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph m (lb, (b, (sigs, morphs))) =
let sig1 = source m
sig2 = target m
l = (morphModule m, morphName m)
s = (sigBase sig1, sigModule sig1)
t = (sigBase sig2, sigModule sig2)
morphs1 = Map.insert (l, s, t) m morphs
in (lb, (b, (sigs, morphs1)))
-- computes the correct targets of morphisms
computeTargets :: GRAPH -> LIBS_EXT -> GRAPH
computeTargets (sigs, morphs) libs =
let morphs2 = Map.foldWithKey
(\ k@((_, _), _, t) morph morphs1 ->
let morph1 = morph { target = lookupSig t libs }
in Map.insert k morph1 morphs1
) Map.empty morphs
in (sigs, morphs2)
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING THE LIBRARY OF LF SIGNATURES AND MORPHISMS -}
-- analyzes the given Twelf file and returns LF signatures and morphisms
twelf2SigMor :: Namespace -> FilePath -> IO LIBS
twelf2SigMor ns fp = do
(libs, _) <- twelf2GR ns fp (Map.empty, [])
return libs
{- updates the graph libraries by adding specs from the Twelf file;
the list of library names stores the order in which they were added,
which is needed later for the construction of DGraphs -}
twelf2GR :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO (LIBS, [BASE])
twelf2GR ns fp lb = do
file <- toAbsoluteURI fp
runTwelf file
le@((libs, bs), (b, gr)) <- buildGraph ns file lb
let gr' = computeTargets gr le
let libs' = Map.insert b gr' libs
let bs' = bs ++ [b]
return (libs', bs')
-- runs twelf to create an omdoc file
runTwelf :: FilePath -> IO ()
runTwelf file = do
let dir = dropFileName file
twelfdir <- getEnvVar twelfEnv
(_, out, err, pr) <-
runInteractiveProcess (concat [twelfdir, "/" , twelf])
(options ++ [dir, file])
Nothing
Nothing
exitCode <- waitForProcess pr
outH <- hGetContents out
errH <- hGetContents err
case exitCode of
ExitFailure i -> do
putStrLn (outH ++ errH)
error $ "Calling Twelf failed with exitCode: " ++ show i ++
" on file " ++ file ++ "dir: " ++ dir ++ "twelfdir: " ++ twelfdir
ExitSuccess -> return ()
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING SIGNATURES AND MORPHISMS -}
-- builds the LF signature and morphism graph
buildGraph :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO LIBS_EXT
buildGraph ns file lb = do
xml <- readFile $ toOMDoc file
lname <- toLibName ns file
let elems = onlyElems $ parseXML xml
let elems1 = filter (\ e -> elName e == omdocQN) elems
case elems1 of
[root] ->
foldM (\ libs e ->
let n = elName e
in if n == theoryQN then addSign ns e libs else
if n == viewQN then addView ns e libs else
return libs
)
(lb, (lname, emptyGraph))
$ elChildren root
_ -> fail "Not an OMDoc file."
-- transforms a theory element into a signature and adds it to the graph
addSign :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addSign ns e libs@(_, (lname, _)) = do
let sig = Sign lname (getNameAttr e) []
(libs1, sig1) <-
foldM (\ ls el ->
let n = elName el
in if n == includeQN then addIncl ns el ls else
if n == structureQN then addStruct ns el ls else
if n == constantQN then addConst ns el ls else
return ls
)
(libs, sig)
$ elChildren e
return $ addSigToGraph sig1 libs1
-- transforms a view element into a view and adds it to the graph
addView :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addView ns e libs@(_, (lname, _)) = do
let name = getNameAttr e
let from = getFromAttr e
let to = getToAttr e
(b1, m1) <- parseRef ns from lname
(b2, m2) <- parseRef ns to lname
libs1 <- addFromFile ns b1 libs
libs2 <- addFromFile ns b2 libs1
let srcSig = lookupSig (b1, m1) libs2
let tarSig = lookupSig (b2, m2) libs2
(morph, libs3) <- getViewMorph ns name srcSig tarSig (elChildren e) libs2
let libs4 = addMorphToGraph morph libs3
return libs4
-- constructs the view morphism
getViewMorph :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT ->
IO (Morphism, LIBS_EXT)
getViewMorph ns name srcSig tarSig els libs@(_, (lname, _)) = do
let b1 = sigBase srcSig
let m1 = sigModule srcSig
let b2 = sigBase tarSig
let m2 = sigModule tarSig
(symmap, libs1) <- constructMap ns els (b1, m1) (b2, m2) libs
let morph = Morphism lname name "" srcSig tarSig Postulated symmap
return (morph, libs1)
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING CONSTANTS -}
-- adds a constant declaration to the signature
addConst :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addConst ns e (libs, sig) = do
let ref@(b, m) = (sigBase sig, sigModule sig)
let sym = Symbol b m $ getNameAttr e
typ <- case findChildren typeQN e of
[t] -> type2exp ns t ref
_ -> fail "Constant element must have a unique type child."
val <- case findChildren definitionQN e of
[] -> return Nothing
[v] -> fmap Just $ definition2exp ns v ref
_ -> fail $ "Constant element must have at most " ++
"one definition child."
let sig1 = addDef (Def sym typ val) sig
return (libs, sig1)
{- converts a type element to an expression
second argument is used for resolving symbol references -}
type2exp :: Namespace -> Element -> NODE -> IO EXP
type2exp ns e ref =
case findChildren omobjQN e of
[omobj] -> omobj2exp ns omobj ref
_ -> fail "Type element must have a unique OMOBJ child."
{- converts a definition element to an expression
second argument is used for resolving symbol references -}
definition2exp :: Namespace -> Element -> NODE -> IO EXP
definition2exp ns e ref =
case findChildren omobjQN e of
[omobj] -> omobj2exp ns omobj ref
_ -> fail "Definition element must have a unique OMOBJ child."
-- converts an OMOBJ element to an expression
omobj2exp :: Namespace -> Element -> NODE -> IO EXP
omobj2exp ns e ref =
case elChildren e of
[el] -> omel2exp ns el ref
_ -> fail "OMOBJ element must have a unique child."
-- converts an Open Math element to an expression
omel2exp :: Namespace -> Element -> NODE -> IO EXP
omel2exp ns e ref =
let name = elName e
in if name == omsQN then oms2exp ns e ref else
if name == omaQN then oma2exp ns e ref else
if name == ombindQN then ombind2exp ns e ref else
if name == omvQN then omv2exp ns e ref else
fail $ "Only OMA, OMS, and OMBIND elements correspond " ++
"to an expression."
-- converts an OMS element to an expression
oms2exp :: Namespace -> Element -> NODE -> IO EXP
oms2exp ns e ref =
if eqOMS e typeOMS then return Type else do
(b, m, n) <- getBMN ns e ref
return $ Const $ Symbol b m n
-- converts an OMA element to an expression
oma2exp :: Namespace -> Element -> NODE -> IO EXP
oma2exp ns e ref =
case elChildren e of
[] -> fail "OMA element must have at least one child."
(f : as) -> do
as1 <- mapM (\ a -> omel2exp ns a ref) as
if eqOMS f arrowOMS
then case as1 of
[] -> fail $ "The -> constructor must be applied" ++
" to at least one argument."
_ -> return $ Func (init as1) (last as1)
else do f1 <- omel2exp ns f ref
return $ Appl f1 as1
-- converts an OMBIND element to an expression
ombind2exp :: Namespace -> Element -> NODE -> IO EXP
ombind2exp ns e ref =
case elChildren e of
[f, d, b] ->
if elName d /= ombvarQN
then fail "The second child of OMBIND must be OMBVAR."
else do d1 <- ombvar2decls ns d ref
b1 <- omel2exp ns b ref
if eqOMS f lambdaOMS then return $ Lamb d1 b1 else
if eqOMS f piOMS then return $ Pi d1 b1 else
{- so far implicit binders are treated
as explicit -}
if eqOMS f impLambdaOMS then return $ Lamb d1 b1 else
if eqOMS f impPiOMS then return $ Pi d1 b1 else
fail "The first child of OMBIND must be be Pi or Lambda."
_ -> fail "OMBIND element must have exactly 3 children."
-- converts an OMBVAR element to a list of declaration
ombvar2decls :: Namespace -> Element -> NODE -> IO CONTEXT
ombvar2decls ns e ref =
mapM (\ a -> omattr2vardecl ns a ref) $ findChildren omattrQN e
-- converts an OMATTR element to a variable declaration
omattr2vardecl :: Namespace -> Element -> NODE -> IO (VAR, EXP)
omattr2vardecl ns e ref =
case findChildren omatpQN e of
[omatp] -> do
val <- omatp2exp ns omatp ref
case findChildren omvQN e of
[omv] -> return (getNameAttr omv, val)
_ -> fail "OMATTR element must have a unique OMV child."
_ -> fail "OMATTR element must have a unique OMATP child."
-- converts an OMATP element to an expression
omatp2exp :: Namespace -> Element -> NODE -> IO EXP
omatp2exp ns e ref =
case elChildren e of
[c1, c2] ->
if eqOMS c1 oftypeOMS
then omel2exp ns c2 ref
else fail $ "The first child of OMATP " ++
"must be the \"oftype\" symbol."
_ -> fail "OMATP element must have exactly two children."
-- converts an OMV element to an expression
omv2exp :: Namespace -> Element -> NODE -> IO EXP
omv2exp _ e _ = return $ Var $ getNameAttr e
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING INCLUSIONS -}
{- adds declarations arising from an inclusion to the signature
adds the inclusion to the morphism map -}
addIncl :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addIncl ns e (libs@(_, (lname, _)), sig) = do
let from = getFromAttr e
(b, m) <- parseRef ns from lname
libs1 <- addFromFile ns b libs
let srcSig = lookupSig (b, m) libs1
let tarSig = addInclSyms srcSig sig
let morph = getInclMorph srcSig tarSig
let libs2 = addMorphToGraph morph libs1
return (libs2, tarSig)
-- adds included definitions to the signature
addInclSyms :: Sign -> Sign -> Sign
addInclSyms (Sign _ _ ds) sig =
let syms = getSymbols sig
in foldl (\ sig1 d ->
if Set.member (getSym d) syms
then sig1
else addDef d sig1
) sig ds
-- constructs the inclusion morphism
getInclMorph :: Sign -> Sign -> Morphism
getInclMorph sig1 sig2 =
Morphism (sigBase sig2) (sigModule sig2) "" sig1 sig2 Definitional Map.empty
{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING STRUCTURES -}
{- adds declarations arising from a structure to the signature
adds the structure to the morphism map -}
addStruct :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addStruct ns e (libs@(_, (lname, _)), sig) = do
let name = getNameAttr e
let from = getFromAttr e
(b, m) <- parseRef ns from lname
libs1 <- addFromFile ns b libs
let srcSig = lookupSig (b, m) libs1
(tarSig, morph, libs2) <- processStruct ns name srcSig sig (elChildren e) libs1
let libs3 = addMorphToGraph morph libs2
return (libs3, tarSig)
{- adds the definitions imported by a structure to the signature and
constructs the structure morphism -}
processStruct :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT ->
IO (Sign, Morphism, LIBS_EXT)
processStruct ns name srcSig tarSig els libs = do
let b1 = sigBase srcSig
let m1 = sigModule srcSig
let b2 = sigBase tarSig
let m2 = sigModule tarSig
let prefix = name ++ structDelimS
let rel sym = Symbol b2 m2 $ prefix ++ symName sym
(symmap, libs1) <- constructMap ns els (b1, m1) (b2, m2) libs
let Sign _ _ ds = srcSig
let morph_init =
Morphism b2 m2 name (Sign b1 m1 []) tarSig Definitional Map.empty
let (sig2, morph2) =
foldl (\ (sig, morph) (Def s t v) ->
let local = isLocalSym s srcSig
defined = isDefinedSym s srcSig
sig1 = if not local then sig else
let s1 = rel s
t1 = fromMaybe (error $
"Structure could not be formed. " ++ name) $
translate morph t
v1 = case v of
Just v1' -> translate morph v1'
Nothing -> Map.lookup s symmap
in addDef (Def s1 t1 v1) sig
morph1 = let source1 = addDef (Def s t v) $ source morph
e = if local
then Const $ rel s
else Map.findWithDefault (Const s)
s symmap
map1 = if defined
then symMap morph
else Map.insert s e $ symMap morph
in morph { source = source1
, target = sig1
, symMap = map1 }
in (sig1, canForm morph1)
) (tarSig, morph_init) ds
return (sig2, morph2, libs1)
-- constructs the translation part of the structure
constructMap :: Namespace -> [Element] -> NODE -> NODE -> LIBS_EXT ->
IO (Map.Map Symbol EXP, LIBS_EXT)
constructMap ns els src tar libs =
foldM (\ ml el ->
let n = elName el
in if n == conassQN then conass2map ns el ml src tar else
if n == includeQN then incl2map ns el ml src tar else
if n == strassQN then strass2map ns el ml src tar else
return ml
) (Map.empty, libs) els
-- converts the constant assignment into a map
conass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
conass2map ns e (mapp, libs) src tar = do
(b, m, n) <- getBMN ns e src
case findChildren omobjQN e of
[omobj] -> do expr <- omobj2exp ns omobj tar
let map1 = Map.insert (Symbol b m n) expr mapp
return (map1, libs)
_ -> fail "Constant assignment element must have a unique OMOBJ child."
-- converts the included morphism into a map
incl2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
incl2map ns e (mapp, libs) _ tar =
case findChildren ommorQN e of
[ommor] -> do (mor, libs1) <- ommor2mor ns ommor tar libs
let map1 = Map.union mapp $ symMap mor
return (map1, libs1)
_ -> fail "Include element must have a unique OMMOR child."
-- converts the structure assignment into a map
strass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
strass2map ns e (mapp, libs) src tar = do
(b, m, n) <- getBMN ns e src
case findChildren ommorQN e of
[ommor] -> do (mor1, libs1) <- retrieveMorph ns (b, m, n) libs
(mor2, libs2) <- ommor2mor ns ommor tar libs1
let map1 = Map.union mapp $ combineMorphs mor1 mor2
return (map1, libs2)
_ -> fail "Structure assignment element must have a unique OMMOR child."
-- converts an OMMOR element to a morphism
ommor2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
ommor2mor ns e ref libs =
case elChildren e of
[el] -> omel2mor ns el ref libs
_ -> fail "OMMOR element must have a unique child."
-- converts an Open Math element to a morphism
omel2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
omel2mor ns e ref libs =
let name = elName e
in if name == omsQN then oms2mor ns e ref libs else
if name == omaQN then oma2mor ns e ref libs else
fail "Only OMA and OMS elements correspond to a morphism."
-- converts an OMS element to a morphism
oms2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
oms2mor ns e ref libs = do
(b, m, n) <- getBMN ns e ref
retrieveMorph ns (b, m, n) libs
-- converts an OMA element to a morphism
oma2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
oma2mor ns e ref libs =
case elChildren e of
[c, m1, m2] ->
if eqOMS c compOMS
then do (mor1, libs1) <- omel2mor ns m1 ref libs
(mor2, libs2) <- omel2mor ns m2 ref libs1
let morR = compMorph (mor1 { target = source mor2 }) mor2
let mor = case morR of
Result _ (Just mor') -> mor'
_ -> error "Morphism cannot be retrieved."
return (mor, libs2)
else fail "The first child of OMA in OMMOR must be composition."
_ -> fail "OMA in OMMOR must have exactly three children."
-- retrieves a morphism by the link name
retrieveMorph :: Namespace -> LINK -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
retrieveMorph ns (b, m, n) = retrieveMorphH ns b m (splitBy '/' n)
retrieveMorphH :: Namespace -> BASE -> MODULE -> [NAME] -> LIBS_EXT ->
IO (Morphism, LIBS_EXT)
retrieveMorphH ns b m names libs = do
libs1 <- addFromFile ns b libs
case names of
[] -> fail "Empty morphism name."
[n] -> do
let mor = lookupMorph (b, m, n) libs1
return (mor, libs1)
(n1 : n2) -> do
let mor1 = lookupMorph (b, m, n1) libs1
let sig = source mor1
let b1 = sigBase sig
let m1 = sigModule sig
(mor2, libs2) <- retrieveMorphH ns b1 m1 n2 libs1
let morR = compMorph (mor2 { target = sig }) mor1
let mor = case morR of
Result _ (Just mor') -> mor'
_ -> error "Morphism cannot be retrieved."
return (mor, libs2)
-- combines two morphisms according to the structure assignment
combineMorphs :: Morphism -> Morphism -> Map.Map Symbol EXP
combineMorphs mor1 mor2 =
let local = getLocalSyms $ source mor1
declared = getDeclaredSyms $ source mor1
er = error "Morphisms cannot be combined."
in Set.fold ( \ s ->
let s1 = case mapSymbol s mor1 of
Just (Const s1') -> s1'
_ -> er
e1 = case mapSymbol s mor2 of
Just e1' -> e1'
_ -> er
in Map.insert s1 e1
) Map.empty $ Set.intersection local declared