d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson{- |

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonModule : $Header$

800f99741c01cfb1b9a0294688349398bc8a0271Automatic UpdaterDescription : Conversion of Twelf files to LF signatures and morphisms

dafcb997e390efa4423883dafd100c975c4095d6Mark AndrewsCopyright : (c) Kristina Sojakova, DFKI Bremen 2010

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David LawrenceLicense : GPLv2 or higher, see LICENSE.txt

ec5347e2c775f027573ce5648b910361aa926c01Automatic Updater

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonMaintainer : k.sojakova@jacobs-university.de

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonStability : experimental

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David LawrencePortability : portable

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews-}

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsmodule LF.Twelf2GR where

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsimport System.Exit

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsimport System.Process

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsimport System.Directory

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsimport System.FilePath

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport System.IO (hGetContents)

ea94d370123a5892f6c47a97f21d1b28d44bb168Tinderbox User

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport Network.URI

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport LF.Sign

eefe56c8b367d1e54361b0c55f9db9d9468a0d6aAndreas Gustafssonimport LF.Morphism

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport qualified Data.Map as Map

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport qualified Data.Set as Set

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport Common.Result

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafssonimport Common.Utils

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssonimport Common.Keywords

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrewsimport Control.Monad

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Text.XML.Light.Input

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Text.XML.Light.Types

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewsimport Text.XML.Light.Proc

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrews

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewstype NODE = (BASE,MODULE)

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewstype LINK = (BASE,MODULE,NAME)

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrews

683e751c957d8b209cc393ff603bea937f5565b0Mark Andrewstype SIGS = Map.Map MODULE Sign

d49d75f5073294d798aa500728116309398bb535Andreas Gustafssontype MORPHS = Map.Map ((MODULE,NAME),NODE,NODE) Morphism

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrewstype GRAPH = (SIGS,MORPHS)

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrewstype LIBS = Map.Map BASE GRAPH

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrewstype LIBS_EXT = ((LIBS,[BASE]),(BASE,GRAPH))

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsemptyGraph :: GRAPH

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsemptyGraph = (Map.empty,Map.empty)

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsomdocNS :: Maybe String

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsomdocNS = Just "http://omdoc.org/ns"

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsopenMathNS :: Maybe String

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsopenMathNS = Just "http://www.openmath.org/OpenMath"

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewslfBase :: String

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewslfBase = "http://cds.omdoc.org/foundations/lf/lf.omdoc"

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsmmtBase :: String

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsmmtBase = "http://cds.omdoc.org/omdoc/mmt.omdoc"

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewslfMod :: String

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonlfMod = "lf"

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonmmtMod :: String

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonmmtMod = "mmt"

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonomdocQN :: QName

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonomdocQN = QName "omdoc" omdocNS Nothing

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

d49d75f5073294d798aa500728116309398bb535Andreas GustafssontheoryQN :: QName

d49d75f5073294d798aa500728116309398bb535Andreas GustafssontheoryQN = QName "theory" omdocNS Nothing

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsviewQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsviewQN = QName "view" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsincludeQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsincludeQN = QName "include" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsstructureQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsstructureQN = QName "structure" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsconstantQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsconstantQN = QName "constant" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsaliasQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsaliasQN = QName "alias" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsnotationQN :: QName

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonnotationQN = QName "notation" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewstypeQN :: QName

d49d75f5073294d798aa500728116309398bb535Andreas GustafssontypeQN = QName "type" omdocNS Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssondefinitionQN :: QName

8f9755413f8814bbabbad40c850a81be52e05623Mark AndrewsdefinitionQN = QName "definition" omdocNS Nothing

8f9755413f8814bbabbad40c850a81be52e05623Mark Andrews

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonomobjQN :: QName

a60f32928e486c147fa66d74ba02eda74a5d1d42Mark AndrewsomobjQN = QName "OMOBJ" openMathNS Nothing

8f9755413f8814bbabbad40c850a81be52e05623Mark Andrews

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsomsQN :: QName

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan HuntomsQN = QName "OMS" openMathNS Nothing

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsomaQN :: QName

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsomaQN = QName "OMA" openMathNS Nothing

7964553eb43ab5146475841540c1c0d977e08b30Mark Andrews

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsombindQN :: QName

7964553eb43ab5146475841540c1c0d977e08b30Mark AndrewsombindQN = QName "OMBIND" openMathNS Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonombvarQN :: QName

b043b56271060295bd32f61e7b7221dd40fb60dcMark AndrewsombvarQN = QName "OMBVAR" openMathNS Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonomattrQN :: QName

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonomattrQN = QName "OMATTR" openMathNS Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonomatpQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsomatpQN = QName "OMATP" openMathNS Nothing

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan Hunt

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonomvQN :: QName

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonomvQN = QName "OMV" openMathNS Nothing

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsommorQN :: QName

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan HuntommorQN = QName "OMMOR" omdocNS Nothing

38bcbbf947f0611bcae2e127d004dab761770c64Mark Andrews

d49d75f5073294d798aa500728116309398bb535Andreas GustafssonconassQN :: QName

38bcbbf947f0611bcae2e127d004dab761770c64Mark AndrewsconassQN = QName "conass" omdocNS Nothing

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonstrassQN :: QName

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonstrassQN = QName "strass" omdocNS Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssontypeOMS :: Element

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssontypeOMS =

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Element omsQN [Attr baseQN lfBase,

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Attr moduleQN lfMod,

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson Attr nameQN "type"] [] Nothing

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas Gustafsson

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonarrowOMS :: Element

c4213ed935163b25bde9273a7c1a79a6296a0662Andreas GustafssonarrowOMS =

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Element omsQN [Attr baseQN lfBase,

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson Attr moduleQN lfMod,

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson Attr nameQN "arrow"] [] Nothing

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas GustafssonlambdaOMS :: Element

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas GustafssonlambdaOMS =

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas Gustafsson Element omsQN [Attr baseQN lfBase,

52f16aeb304bc13f6957e3ecf24c8c5b69991558Andreas Gustafsson Attr moduleQN lfMod,

7d97663b2ca5b7b057276fc9d239025da80e4756Mark Andrews Attr nameQN "lambda"] [] Nothing

7d97663b2ca5b7b057276fc9d239025da80e4756Mark Andrews

6e8a02d5d3a845ca1768e92c88bdc0a4da47f95bAndreas GustafssonpiOMS :: Element

534253444e569bf039fb6e5fc31a5e8c2e8305c0Mark AndrewspiOMS =

52f16aeb304bc13f6957e3ecf24c8c5b69991558Andreas Gustafsson Element omsQN [Attr baseQN lfBase,

8a86c12ec245eb3838f48ffbc5a01fb9b7666a60Evan Hunt Attr moduleQN lfMod,

7c87a8bf7bc525f9b3ce80e7c12928a226e37d2bMark Andrews Attr nameQN "Pi"] [] Nothing

05398561e0221fe1fef1457627a50c60bddbb022Mark Andrews

8a86c12ec245eb3838f48ffbc5a01fb9b7666a60Evan Hunt

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan HuntimpLambdaOMS :: Element

a26e1cacef2047b1048febd5e8d756060b4bddb1Evan HuntimpLambdaOMS =

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson Element omsQN [Attr baseQN lfBase,

2e286ac71f3621c11a3409f35a859488026b5fb5Mark Andrews Attr moduleQN lfMod,

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews Attr nameQN "implicit_lambda"] [] Nothing

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark AndrewsimpPiOMS :: Element

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark AndrewsimpPiOMS =

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews Element omsQN [Attr baseQN lfBase,

61d7ab455fe6c2c1be112e7f48a768b9db1f65bbMark Andrews Attr moduleQN lfMod,

2e286ac71f3621c11a3409f35a859488026b5fb5Mark Andrews Attr nameQN "implicit_Pi"] [] Nothing

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark AndrewsoftypeOMS :: Element

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark AndrewsoftypeOMS =

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews Element omsQN [Attr baseQN lfBase,

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews Attr moduleQN lfMod,

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews Attr nameQN "oftype"] [] Nothing

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark AndrewscompOMS :: Element

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark AndrewscompOMS =

c85ffa76df4b94e0c44b2924f7a7f2e875a1ea86Mark Andrews Element omsQN [Attr baseQN mmtBase,

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews Attr moduleQN mmtMod,

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews Attr nameQN "composition"] [] Nothing

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsnameQN :: QName

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsnameQN = (QName "name" Nothing Nothing)

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsmoduleQN :: QName

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsmoduleQN = (QName "module" Nothing Nothing)

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsbaseQN :: QName

3d2ce18535b3d2d828bd40aec7f4686519f305feMark AndrewsbaseQN = (QName "base" Nothing Nothing)

3d2ce18535b3d2d828bd40aec7f4686519f305feMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewsfromQN :: QName

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewsfromQN = (QName "from" Nothing Nothing)

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewstoQN :: QName

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewstoQN = (QName "to" Nothing Nothing)

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewsomdocE :: String

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewsomdocE = "omdoc"

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewstwelfE :: String

4347f7ac1286aaa114935823c3cd59151de0166bMark AndrewstwelfE = "elf"

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews-- path to the Twelf folder must be set in the environment variable TWELF_LIB

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewstwelf :: String

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewstwelf = "check-some"

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsoptions :: [String]

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrewsoptions = ["-omdoc"]

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews

4347f7ac1286aaa114935823c3cd59151de0166bMark Andrews------------------------------------------------------------------------------

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson------------------------------------------------------------------------------

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson-- HELPER FUNCTIONS

d49d75f5073294d798aa500728116309398bb535Andreas Gustafsson

1090574e9153ad41c403f812d9b6cef0334e828eMark AndrewsgetFromAttr :: Element -> String

d49d75f5073294d798aa500728116309398bb535Andreas GustafssongetFromAttr e =

case findAttr fromQN e of

Nothing -> error "Element is missing a \"from\" attribute."

Just a -> a

getToAttr :: Element -> String

getToAttr e =

case findAttr toQN e of

Nothing -> error "Element is missing a \"to\" attribute."

Just a -> a

getNameAttr :: Element -> String

getNameAttr e =

case findAttr nameQN e of

Nothing -> error $ "Element is missing a name." ++ (show e)

Just n -> n

getModuleAttr :: Element -> Maybe String

getModuleAttr e = findAttr moduleQN e

getBaseAttr :: Element -> Maybe String

getBaseAttr e = findAttr baseQN e

-- compares two OMS elements

eqOMS :: Element -> Element -> Bool

eqOMS e1 e2 =

if (elName e1 /= omsQN || elName e2 /= omsQN) then False else

and [ getNameAttr e1 == getNameAttr e2

, getModuleAttr e1 == getModuleAttr e2

, getBaseAttr e1 == getBaseAttr e2]

toLibName :: FilePath -> FilePath

toLibName fp = dropExtension fp

fromLibName :: FilePath -> FilePath

fromLibName fp = addExtension fp twelfE

toOMDoc :: FilePath -> FilePath

toOMDoc fp = replaceExtension fp omdocE

fromOMDoc :: FilePath -> FilePath

fromOMDoc fp = replaceExtension fp twelfE

-- resolves the first file path wrt to the second

resolve :: FilePath -> FilePath -> FilePath

resolve fp1 fp2 =

case parseURIReference fp1 of

Nothing -> er

Just uri1 -> do

case parseURIReference fp2 of

Nothing -> er

Just uri2 -> do

case relativeTo uri1 uri2 of

Nothing -> er

Just f -> show f

where er = error "Invalid file name."

-- resolves the file path wrt to the current directory

resolveToCur :: FilePath -> IO FilePath

resolveToCur fp = do

dir <- getCurrentDirectory

return $ resolve fp (dir ++ "/")

{- returns the referenced base and module resolved w.r.t.

the second argument -}

parseRef :: String -> String -> NODE

parseRef ref base =

case splitBy '?' ref of

[br,m] -> let b = fromOMDoc $ resolve br base

in (b,m)

_ -> error "Invalid reference."

-- retrieves the base, module, and name attributes

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

getBMN e (base,modul) =

let n = case findAttr nameQN e of

Nothing -> ""

Just n' -> n'

m = case getModuleAttr e of

Nothing -> modul

Just m' -> m'

b = case getBaseAttr e of

Nothing -> base

Just b' -> fromOMDoc $ resolve b' base

in (b,m,n)

{- parses the referenced file if needed and imports all signatures

and morphisms from it -}

addFromFile :: FilePath -> LIBS_EXT -> IO LIBS_EXT

addFromFile fp libs@(lb@(l,_),(b,gr)) = do

let file = toLibName fp

if (file == b || Map.member file l)

then return libs

else do lb' <- twelf2GR fp 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 :: FilePath -> IO LIBS

twelf2SigMor fp = do

(libs,_) <- twelf2GR 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 :: FilePath -> (LIBS,[BASE]) -> IO (LIBS,[BASE])

twelf2GR fp lb = do

file <- resolveToCur fp

runTwelf file

le@((libs,bs),(b,gr)) <- buildGraph 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 <- getEnvDef "TWELF_LIB" ""

if null twelfdir

then error "environment variable TWELF_LIB is not set"

else do

(_, 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

ExitSuccess -> return ()

------------------------------------------------------------------------------

------------------------------------------------------------------------------

-- CONSTRUCTING SIGNATURES AND MORPHISMS

-- builds the LF signature and morphism graph

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

buildGraph file lb = do

xml <- readFile $ toOMDoc file

let elems = onlyElems $ parseXML xml

let elems1 = filter (\ e -> elName e == omdocQN) elems

case elems1 of

[root] -> do

foldM (\ libs e ->

let n = elName e

in if (n == theoryQN) then addSign e libs else

if (n == viewQN) then addView e libs else

return libs

)

(lb,(toLibName file,emptyGraph))

$ elChildren root

_ -> fail "Not an OMDoc file."

-- transforms a theory element into a signature and adds it to the graph

addSign :: Element -> LIBS_EXT -> IO LIBS_EXT

addSign e libs@(_,(base,_)) = do

let sig = Sign base (getNameAttr e) []

(libs1,sig1) <-

foldM (\ ls el ->

let n = elName el

in if (n == includeQN) then addIncl el ls else

if (n == structureQN) then addStruct el ls else

if (n == constantQN) then addConst 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 :: Element -> LIBS_EXT -> IO LIBS_EXT

addView e libs@(_,(file,_)) = do

let name = getNameAttr e

let from = getFromAttr e

let to = getToAttr e

let (b1,m1) = parseRef from file

let (b2,m2) = parseRef to file

libs1 <- addFromFile b1 libs

libs2 <- addFromFile b2 libs1

let srcSig = lookupSig (toLibName b1,m1) libs2

let tarSig = lookupSig (toLibName b2,m2) libs2

(morph,libs3) <- getViewMorph name srcSig tarSig (elChildren e) libs2

let libs4 = addMorphToGraph morph libs3

return libs4

{- constructs the view morphism -}

getViewMorph :: String -> Sign -> Sign -> [Element] -> LIBS_EXT ->

IO (Morphism,LIBS_EXT)

getViewMorph name srcSig tarSig els libs@(_,(file,_)) = do

let b1 = sigBase srcSig

let m1 = sigModule srcSig

let b2 = sigBase tarSig

let m2 = sigModule tarSig

(symmap,libs1) <- constructMap els (b1,m1) (b2,m2) libs

let morph = Morphism file name "" srcSig tarSig Postulated symmap

return (morph,libs1)

------------------------------------------------------------------------------

------------------------------------------------------------------------------

-- CONSTRUCTING CONSTANTS

-- adds a constant declaration to the signature

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

addConst e (libs,sig) = do

let ref@(b,m) = (sigBase sig, sigModule sig)

let sym = Symbol b m $ getNameAttr e

let typ = case findChildren typeQN e of

[t] -> type2exp t ref

_ -> error "Constant element must have a unique type child."

let val = case findChildren definitionQN e of

[] -> Nothing

[v] -> Just $ definition2exp v ref

_ -> error $ "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 :: Element -> NODE -> EXP

type2exp e ref =

case findChildren omobjQN e of

[omobj] -> omobj2exp omobj ref

_ -> error "Type element must have a unique OMOBJ child."

{- converts a definition element to an expression

second argument is used for resolving symbol references -}

definition2exp :: Element -> NODE -> EXP

definition2exp e ref =

case findChildren omobjQN e of

[omobj] -> omobj2exp omobj ref

_ -> error "Definition element must have a unique OMOBJ child."

-- converts an OMOBJ element to an expression

omobj2exp :: Element -> NODE -> EXP

omobj2exp e ref =

case elChildren e of

[el] -> omel2exp el ref

_ -> error "OMOBJ element must have a unique child."

-- converts an Open Math element to an expression

omel2exp :: Element -> NODE -> EXP

omel2exp e ref =

let name = elName e

in if (name == omsQN) then oms2exp e ref else

if (name == omaQN) then oma2exp e ref else

if (name == ombindQN) then ombind2exp e ref else

if (name == omvQN) then omv2exp e ref else

error $ "Only OMA, OMS, and OMBIND elements correspond " ++

"to an expression."

-- converts an OMS element to an expression

oms2exp :: Element -> NODE -> EXP

oms2exp e ref =

if (eqOMS e typeOMS) then Type else

let (b,m,n) = getBMN e ref

in Const $ Symbol (toLibName b) m n

-- converts an OMA element to an expression

oma2exp :: Element -> NODE -> EXP

oma2exp e ref =

case elChildren e of

[] -> error "OMA element must have at least one child."

(f:as) ->

let as1 = map (\ a -> omel2exp a ref) as

in if (eqOMS f arrowOMS)

then case as1 of

[] -> error $ "The -> constructor must be applied" ++

" to at least one argument."

_ -> Func (init as1) (last as1)

else let f1 = omel2exp f ref

in Appl f1 as1

-- converts an OMBIND element to an expression

ombind2exp :: Element -> NODE -> EXP

ombind2exp e ref =

case elChildren e of

[f,d,b] ->

if (elName d /= ombvarQN)

then error "The second child of OMBIND must be OMBVAR."

else let d1 = ombvar2decls d ref

b1 = omel2exp b ref

in if (eqOMS f lambdaOMS) then Lamb d1 b1 else

if (eqOMS f piOMS) then Pi d1 b1 else

{- so far implicit binders are treated

as explicit -}

if (eqOMS f impLambdaOMS) then Lamb d1 b1 else

if (eqOMS f impPiOMS) then Pi d1 b1 else

error $ "The first child of OMBIND " ++

"must be be Pi or Lambda."

_ -> error "OMBIND element must have exactly 3 children."

-- converts an OMBVAR element to a list of declaration

ombvar2decls :: Element -> NODE -> CONTEXT

ombvar2decls e ref =

let attrs = findChildren omattrQN e

in map (\ a -> omattr2vardecl a ref) attrs

-- converts an OMATTR element to a variable declaration

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

omattr2vardecl e ref =

case findChildren omatpQN e of

[omatp] ->

case findChildren omvQN e of

[omv] -> (getNameAttr omv, omatp2exp omatp ref)

_ -> error "OMATTR element must have a unique OMV child."

_ -> error "OMATTR element must have a unique OMATP child."

-- converts an OMATP element to an expression

omatp2exp :: Element -> NODE -> EXP

omatp2exp e ref =

case elChildren e of

[c1,c2] ->

if (eqOMS c1 oftypeOMS)

then omel2exp c2 ref

else error $ "The first child of OMATP " ++

"must be the \"oftype\" symbol."

_ -> error "OMATP element must have exactly two children."

-- converts an OMV element to an expression

omv2exp :: Element -> NODE -> EXP

omv2exp e _ = Var $ getNameAttr e

------------------------------------------------------------------------------

------------------------------------------------------------------------------

-- CONSTRUCTING INCLUSIONS

{- adds declarations arising from an inclusion to the signature

adds the inclusion to the morphism map -}

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

addIncl e (libs@(_,(file,_)),sig) = do

let from = getFromAttr e

let (b,m) = parseRef from file

libs1 <- addFromFile b libs

let srcSig = lookupSig (toLibName 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 :: Element -> (LIBS_EXT,Sign) -> IO (LIBS_EXT,Sign)

addStruct e (libs@(_,(file,_)),sig) = do

let name = getNameAttr e

let from = getFromAttr e

let (b,m) = parseRef from file

libs1 <- addFromFile b libs

let srcSig = lookupSig (toLibName b,m) libs1

(tarSig,morph,libs2) <- processStruct 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 :: String -> Sign -> Sign -> [Element] -> LIBS_EXT ->

IO (Sign,Morphism,LIBS_EXT)

processStruct 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 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 = case translate morph t of

Just t1'-> t1'

Nothing -> error $

"Structure could not be formed. " ++ name

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 :: [Element] -> NODE -> NODE -> LIBS_EXT ->

IO (Map.Map Symbol EXP, LIBS_EXT)

constructMap els src tar libs = do

foldM (\ ml el ->

let n = elName el

in if (n == conassQN) then conass2map el ml src tar else

if (n == includeQN) then incl2map el ml src tar else

if (n == strassQN) then strass2map el ml src tar else

return ml

) (Map.empty,libs) els

-- converts the constant assignment into a map

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

IO (Map.Map Symbol EXP, LIBS_EXT)

conass2map e (mapp,libs) src tar = do

let (b,m,n) = getBMN e src

case findChildren omobjQN e of

[omobj] -> do let expr = omobj2exp omobj tar

let map1 = Map.insert (Symbol b m n) expr mapp

return (map1,libs)

_ -> error "Constant assignment element must have a unique OMOBJ child."

-- converts the included morphism into a map

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

IO (Map.Map Symbol EXP, LIBS_EXT)

incl2map e (mapp,libs) _ tar =

case findChildren ommorQN e of

[ommor] -> do (mor,libs1) <- ommor2mor ommor tar libs

let map1 = Map.union mapp $ symMap mor

return (map1,libs1)

_ -> error "Include element must have a unique OMMOR child."

-- converts the structure assignment into a map

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

IO (Map.Map Symbol EXP, LIBS_EXT)

strass2map e (mapp,libs) src tar = do

let (b,m,n) = getBMN e src

case findChildren ommorQN e of

[ommor] -> do (mor1,libs1) <- retrieveMorph (toLibName b,m,n) libs

(mor2,libs2) <- ommor2mor ommor tar libs1

let map1 = Map.union mapp $ combineMorphs mor1 mor2

return (map1,libs2)

_ -> error "Structure assignment element must have a unique OMMOR child."

-- converts an OMMOR element to a morphism

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

ommor2mor e ref libs =

case elChildren e of

[el] -> omel2mor el ref libs

_ -> error "OMMOR element must have a unique child."

-- converts an Open Math element to a morphism

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

omel2mor e ref libs =

let name = elName e

in if (name == omsQN) then oms2mor e ref libs else

if (name == omaQN) then oma2mor e ref libs else

error "Only OMA and OMS elements correspond to a morphism."

-- converts an OMS element to a morphism

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

oms2mor e ref libs = do

let (b,m,n) = getBMN e ref

retrieveMorph (toLibName b,m,n) libs

-- converts an OMA element to a morphism

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

oma2mor e ref libs = do

case elChildren e of

[c,m1,m2] -> do

if (eqOMS c compOMS)

then do (mor1,libs1) <- omel2mor m1 ref libs

(mor2,libs2) <- omel2mor 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 error "The first child of OMA in OMMOR must be composition."

_ -> error "OMA in OMMOR must have exactly three children."

-- retrieves a morphism by the link name

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

retrieveMorph (b,m,n) libs = retrieveMorphH b m (splitBy '/' n) libs

retrieveMorphH :: BASE -> MODULE -> [NAME] -> LIBS_EXT ->

IO (Morphism,LIBS_EXT)

retrieveMorphH b m ns libs = do

libs1 <- addFromFile (fromLibName b) libs

case ns of

[] -> error "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 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