e1e8390280254f7f0580d701e583f670643d4f3fnilgun{- |

e1e8390280254f7f0580d701e583f670643d4f3fnilgunModule : $Header$

e1e8390280254f7f0580d701e583f670643d4f3fnilgunDescription : Conversion of Twelf files to LF signatures and morphisms

e1e8390280254f7f0580d701e583f670643d4f3fnilgunCopyright : (c) Kristina Sojakova, DFKI Bremen 2010

e1e8390280254f7f0580d701e583f670643d4f3fnilgunLicense : GPLv2 or higher, see LICENSE.txt

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunMaintainer : k.sojakova@jacobs-university.de

e1e8390280254f7f0580d701e583f670643d4f3fnilgunStability : experimental

e1e8390280254f7f0580d701e583f670643d4f3fnilgunPortability : portable

e1e8390280254f7f0580d701e583f670643d4f3fnilgun-}

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule LF.Twelf2GR where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport System.Exit

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport System.Process

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport System.Directory

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport System.FilePath

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport System.IO (hGetContents)

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Network.URI

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport LF.Sign

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport LF.Morphism

3f08db06526d6901aa08c110b5bc7dde6bc39905nd

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport qualified Data.Map as Map

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport qualified Data.Set as Set

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Common.Result

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Common.Utils

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Common.Keywords

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Control.Monad

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Text.XML.Light.Input

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Text.XML.Light.Types

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport Text.XML.Light.Proc

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype NODE = (BASE,MODULE)

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype LINK = (BASE,MODULE,NAME)

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype SIGS = Map.Map MODULE Sign

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype MORPHS = Map.Map ((MODULE,NAME),NODE,NODE) Morphism

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype GRAPH = (SIGS,MORPHS)

e1e8390280254f7f0580d701e583f670643d4f3fnilguntype LIBS = Map.Map BASE GRAPH

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

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunemptyGraph :: GRAPH

e1e8390280254f7f0580d701e583f670643d4f3fnilgunemptyGraph = (Map.empty,Map.empty)

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomdocNS :: Maybe String

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomdocNS = Just "http://omdoc.org/ns"

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunopenMathNS :: Maybe String

e1e8390280254f7f0580d701e583f670643d4f3fnilgunopenMathNS = Just "http://www.openmath.org/OpenMath"

2704de98885368683621b01c8f8f4e4b01557611takashi

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlfBase :: String

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlfBase = "http://cds.omdoc.org/foundations/lf/lf.omdoc"

b9f522ae1c0ed2bf3fc4444245bf28b2e2449a65nd

e1e8390280254f7f0580d701e583f670643d4f3fnilgunmmtBase :: String

c38e2a97e43fc69b22f6b03c6d2f60e3bd705f89sfmmtBase = "http://cds.omdoc.org/omdoc/mmt.omdoc"

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlfMod :: String

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlfMod = "lf"

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunmmtMod :: String

e1e8390280254f7f0580d701e583f670643d4f3fnilgunmmtMod = "mmt"

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomdocQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomdocQN = QName "omdoc" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilguntheoryQN :: QName

2704de98885368683621b01c8f8f4e4b01557611takashitheoryQN = QName "theory" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunviewQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunviewQN = QName "view" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunincludeQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunincludeQN = QName "include" omdocNS Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunstructureQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunstructureQN = QName "structure" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunconstantQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunconstantQN = QName "constant" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunaliasQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunaliasQN = QName "alias" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunnotationQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunnotationQN = QName "notation" omdocNS Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilguntypeQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilguntypeQN = QName "type" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgundefinitionQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgundefinitionQN = QName "definition" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunomobjQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomobjQN = QName "OMOBJ" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomsQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomsQN = QName "OMS" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunomaQN :: QName

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunomaQN = QName "OMA" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunombindQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunombindQN = QName "OMBIND" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunombvarQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunombvarQN = QName "OMBVAR" openMathNS Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomattrQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomattrQN = QName "OMATTR" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomatpQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomatpQN = QName "OMATP" openMathNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomvQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunomvQN = QName "OMV" openMathNS Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunommorQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunommorQN = QName "OMMOR" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunconassQN :: QName

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunconassQN = QName "conass" omdocNS Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunstrassQN :: QName

e1e8390280254f7f0580d701e583f670643d4f3fnilgunstrassQN = QName "strass" omdocNS Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilguntypeOMS :: Element

e1e8390280254f7f0580d701e583f670643d4f3fnilguntypeOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN lfBase,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr moduleQN lfMod,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr nameQN "type"] [] Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunarrowOMS :: Element

e1e8390280254f7f0580d701e583f670643d4f3fnilgunarrowOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN lfBase,

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Attr moduleQN lfMod,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr nameQN "arrow"] [] Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlambdaOMS :: Element

e1e8390280254f7f0580d701e583f670643d4f3fnilgunlambdaOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN lfBase,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr moduleQN lfMod,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr nameQN "lambda"] [] Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunpiOMS :: Element

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunpiOMS =

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Element omsQN [Attr baseQN lfBase,

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Attr moduleQN lfMod,

2704de98885368683621b01c8f8f4e4b01557611takashi Attr nameQN "Pi"] [] Nothing

2704de98885368683621b01c8f8f4e4b01557611takashi

2704de98885368683621b01c8f8f4e4b01557611takashi

2704de98885368683621b01c8f8f4e4b01557611takashiimpLambdaOMS :: Element

2704de98885368683621b01c8f8f4e4b01557611takashiimpLambdaOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN lfBase,

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Attr moduleQN lfMod,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr nameQN "implicit_lambda"] [] Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunimpPiOMS :: Element

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunimpPiOMS =

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Element omsQN [Attr baseQN lfBase,

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Attr moduleQN lfMod,

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun Attr nameQN "implicit_Pi"] [] Nothing

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgun

e0cfea1f5d38eeaa8fdf7c197c3c1eb31148e191nilgunoftypeOMS :: Element

e1e8390280254f7f0580d701e583f670643d4f3fnilgunoftypeOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN lfBase,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr moduleQN lfMod,

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Attr nameQN "oftype"] [] Nothing

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

e1e8390280254f7f0580d701e583f670643d4f3fnilguncompOMS :: Element

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungcompOMS =

e1e8390280254f7f0580d701e583f670643d4f3fnilgun Element omsQN [Attr baseQN mmtBase,

5effc8b39fae5cd169d17f342bfc265705840014rbowen Attr moduleQN mmtMod,

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Attr nameQN "composition"] [] Nothing

2c9e74eac9f72c14535dd65a520e4de2e664d9cdhumbedooh

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowennameQN :: QName

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowennameQN = (QName "name" Nothing Nothing)

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

e1e8390280254f7f0580d701e583f670643d4f3fnilgunmoduleQN :: 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 =

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]

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 (fp == b || Map.member fp 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,(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 (b1,m1) libs2

let tarSig = lookupSig (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 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 (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 (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 (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 (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 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