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 qualified Control.Monad.Fail as Fail
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 :: String
latinEnv = "LATIN_LIB"
twelfEnv :: String
twelfEnv :: String
twelfEnv = "TWELF_LIB"
hetsEnv :: String
hetsEnv :: String
hetsEnv = "HETS_HOME"
emptyGraph :: GRAPH
emptyGraph :: GRAPH
emptyGraph = (Map String Sign
forall k a. Map k a
Map.empty, Map ((String, String), (String, String), (String, String)) Morphism
forall k a. Map k a
Map.empty)
omdocNS :: Maybe String
omdocNS :: Maybe String
omdocNS = String -> Maybe String
forall a. a -> Maybe a
Just "http://omdoc.org/ns"
openMathNS :: Maybe String
openMathNS :: Maybe String
openMathNS = String -> Maybe String
forall a. a -> Maybe a
Just "http://www.openmath.org/OpenMath"
lfBase :: String
lfBase :: String
lfBase = "http://cds.omdoc.org/foundations/lf/lf.omdoc"
mmtBase :: String
mmtBase :: String
mmtBase = "http://cds.omdoc.org/omdoc/mmt.omdoc"
lfMod :: String
lfMod :: String
lfMod = "lf"
mmtMod :: String
mmtMod :: String
mmtMod = "mmt"
omdocQN :: QName
omdocQN :: QName
omdocQN = String -> Maybe String -> Maybe String -> QName
QName "omdoc" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
theoryQN :: QName
theoryQN :: QName
theoryQN = String -> Maybe String -> Maybe String -> QName
QName "theory" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
viewQN :: QName
viewQN :: QName
viewQN = String -> Maybe String -> Maybe String -> QName
QName "view" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
includeQN :: QName
includeQN :: QName
includeQN = String -> Maybe String -> Maybe String -> QName
QName "include" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
structureQN :: QName
structureQN :: QName
structureQN = String -> Maybe String -> Maybe String -> QName
QName "structure" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
constantQN :: QName
constantQN :: QName
constantQN = String -> Maybe String -> Maybe String -> QName
QName "constant" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
aliasQN :: QName
aliasQN :: QName
aliasQN = String -> Maybe String -> Maybe String -> QName
QName "alias" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
notationQN :: QName
notationQN :: QName
notationQN = String -> Maybe String -> Maybe String -> QName
QName "notation" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
typeQN :: QName
typeQN :: QName
typeQN = String -> Maybe String -> Maybe String -> QName
QName "type" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
definitionQN :: QName
definitionQN :: QName
definitionQN = String -> Maybe String -> Maybe String -> QName
QName "definition" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
omobjQN :: QName
omobjQN :: QName
omobjQN = String -> Maybe String -> Maybe String -> QName
QName "OMOBJ" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
omsQN :: QName
omsQN :: QName
omsQN = String -> Maybe String -> Maybe String -> QName
QName "OMS" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
omaQN :: QName
omaQN :: QName
omaQN = String -> Maybe String -> Maybe String -> QName
QName "OMA" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
ombindQN :: QName
ombindQN :: QName
ombindQN = String -> Maybe String -> Maybe String -> QName
QName "OMBIND" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
ombvarQN :: QName
ombvarQN :: QName
ombvarQN = String -> Maybe String -> Maybe String -> QName
QName "OMBVAR" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
omattrQN :: QName
omattrQN :: QName
omattrQN = String -> Maybe String -> Maybe String -> QName
QName "OMATTR" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
omatpQN :: QName
omatpQN :: QName
omatpQN = String -> Maybe String -> Maybe String -> QName
QName "OMATP" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
omvQN :: QName
omvQN :: QName
omvQN = String -> Maybe String -> Maybe String -> QName
QName "OMV" Maybe String
openMathNS Maybe String
forall a. Maybe a
Nothing
ommorQN :: QName
ommorQN :: QName
ommorQN = String -> Maybe String -> Maybe String -> QName
QName "OMMOR" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
conassQN :: QName
conassQN :: QName
conassQN = String -> Maybe String -> Maybe String -> QName
QName "conass" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
strassQN :: QName
strassQN :: QName
strassQN = String -> Maybe String -> Maybe String -> QName
QName "strass" Maybe String
omdocNS Maybe String
forall a. Maybe a
Nothing
typeOMS :: Element
typeOMS :: Element
typeOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "type"] [] Maybe Line
forall a. Maybe a
Nothing
arrowOMS :: Element
arrowOMS :: Element
arrowOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "arrow"] [] Maybe Line
forall a. Maybe a
Nothing
lambdaOMS :: Element
lambdaOMS :: Element
lambdaOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "lambda"] [] Maybe Line
forall a. Maybe a
Nothing
piOMS :: Element
piOMS :: Element
piOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "Pi"] [] Maybe Line
forall a. Maybe a
Nothing
impLambdaOMS :: Element
impLambdaOMS :: Element
impLambdaOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "implicit_lambda"] [] Maybe Line
forall a. Maybe a
Nothing
impPiOMS :: Element
impPiOMS :: Element
impPiOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "implicit_Pi"] [] Maybe Line
forall a. Maybe a
Nothing
oftypeOMS :: Element
oftypeOMS :: Element
oftypeOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
lfBase,
QName -> String -> Attr
Attr QName
moduleQN String
lfMod,
QName -> String -> Attr
Attr QName
nameQN "oftype"] [] Maybe Line
forall a. Maybe a
Nothing
compOMS :: Element
compOMS :: Element
compOMS =
QName -> [Attr] -> [Content] -> Maybe Line -> Element
Element QName
omsQN [QName -> String -> Attr
Attr QName
baseQN String
mmtBase,
QName -> String -> Attr
Attr QName
moduleQN String
mmtMod,
QName -> String -> Attr
Attr QName
nameQN "composition"] [] Maybe Line
forall a. Maybe a
Nothing
nameQN :: QName
nameQN :: QName
nameQN = String -> Maybe String -> Maybe String -> QName
QName "name" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
moduleQN :: QName
moduleQN :: QName
moduleQN = String -> Maybe String -> Maybe String -> QName
QName "module" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
baseQN :: QName
baseQN :: QName
baseQN = String -> Maybe String -> Maybe String -> QName
QName "base" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
fromQN :: QName
fromQN :: QName
fromQN = String -> Maybe String -> Maybe String -> QName
QName "from" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
toQN :: QName
toQN :: QName
toQN = String -> Maybe String -> Maybe String -> QName
QName "to" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
omdocE :: String
omdocE :: String
omdocE = "omdoc"
twelfE :: String
twelfE :: String
twelfE = "elf"
twelf :: String
twelf :: String
twelf = "check-some"
options :: [String]
options :: [String]
options = ["-omdoc"]
getFromAttr :: Element -> String
getFromAttr :: Element -> String
getFromAttr e :: Element
e = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (String -> String
forall a. HasCallStack => String -> a
error "Element is missing a \"from\" attribute.") (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$
QName -> Element -> Maybe String
findAttr QName
fromQN Element
e
getToAttr :: Element -> String
getToAttr :: Element -> String
getToAttr e :: Element
e = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (String -> String
forall a. HasCallStack => String -> a
error "Element is missing a \"to\" attribute.") (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$
QName -> Element -> Maybe String
findAttr QName
toQN Element
e
getNameAttr :: Element -> String
getNameAttr :: Element -> String
getNameAttr e :: Element
e = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "Element is missing a name." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Element -> String
forall a. Show a => a -> String
show Element
e) (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$
QName -> Element -> Maybe String
findAttr QName
nameQN Element
e
getModuleAttr :: Element -> Maybe String
getModuleAttr :: Element -> Maybe String
getModuleAttr = QName -> Element -> Maybe String
findAttr QName
moduleQN
getBaseAttr :: Element -> Maybe String
getBaseAttr :: Element -> Maybe String
getBaseAttr = QName -> Element -> Maybe String
findAttr QName
baseQN
eqOMS :: Element -> Element -> Bool
eqOMS :: Element -> Element -> Bool
eqOMS e1 :: Element
e1 e2 :: Element
e2 = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Element -> QName
elName Element
e1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
omsQN Bool -> Bool -> Bool
|| Element -> QName
elName Element
e2 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
omsQN
toOMDoc :: FilePath -> FilePath
toOMDoc :: String -> String
toOMDoc fp :: String
fp = String -> String -> String
replaceExtension String
fp String
omdocE
toTwelf :: FilePath -> FilePath
toTwelf :: String -> String
toTwelf fp :: String
fp = String -> String -> String
replaceExtension String
fp String
twelfE
getEnv :: Namespace -> String
getEnv :: Namespace -> String
getEnv ns :: Namespace
ns =
case Namespace
ns of
LATIN -> String
latinEnv
HETS -> String
hetsEnv
getEnvVar :: String -> IO String
getEnvVar :: String -> IO String
getEnvVar var :: String
var = do
String
val <- String -> String -> IO String
getEnvDef String
var ""
if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
val
then String -> IO String
forall a. HasCallStack => String -> a
error (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "environment variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not set."
else String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
val
resolve :: FilePath -> FilePath -> FilePath
resolve :: String -> String -> String
resolve fp1 :: String
fp1 fp2 :: String
fp2 =
case String -> Maybe IRI
parseIRIReference String
fp1 of
Nothing -> String
forall a. a
er
Just uri1 :: IRI
uri1 ->
case String -> Maybe IRI
parseIRIReference String
fp2 of
Nothing -> String
forall a. a
er
Just uri2 :: IRI
uri2 ->
case IRI -> IRI -> Maybe IRI
relativeTo IRI
uri1 IRI
uri2 of
Nothing -> String
forall a. a
er
Just f :: IRI
f -> IRI -> String
forall a. Show a => a -> String
show IRI
f
where er :: a
er = String -> a
forall a. HasCallStack => String -> a
error "Invalid file name."
relativize :: FilePath -> FilePath -> FilePath
relativize :: String -> String -> String
relativize fp1 :: String
fp1 fp2 :: String
fp2 =
case String -> Maybe IRI
parseIRIReference String
fp1 of
Nothing -> String
forall a. a
er
Just uri1 :: IRI
uri1 ->
case String -> Maybe IRI
parseIRIReference String
fp2 of
Nothing -> String
forall a. a
er
Just uri2 :: IRI
uri2 -> IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ IRI -> IRI -> IRI
relativeFrom IRI
uri1 IRI
uri2
where er :: a
er = String -> a
forall a. HasCallStack => String -> a
error "Invalid file name."
toAbsoluteURI :: FilePath -> IO FilePath
toAbsoluteURI :: String -> IO String
toAbsoluteURI fp :: String
fp = do
String
dir <- IO String
getCurrentDirectory
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
resolve String
fp (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/"
toRelativeURI :: FilePath -> IO FilePath
toRelativeURI :: String -> IO String
toRelativeURI fp :: String
fp = do
String
dir <- IO String
getCurrentDirectory
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
relativize String
fp (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/"
toLibName :: Namespace -> FilePath -> IO BASE
toLibName :: Namespace -> String -> IO String
toLibName ns :: Namespace
ns fp :: String
fp = do
String
file <- String -> IO String
toAbsoluteURI String
fp
String
dir <- String -> IO String
getEnvVar (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Namespace -> String
getEnv Namespace
ns
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
relativize String
file (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/"
fromLibName :: Namespace -> BASE -> IO FilePath
fromLibName :: Namespace -> String -> IO String
fromLibName ns :: Namespace
ns lname :: String
lname = do
String
dir <- String -> IO String
getEnvVar (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Namespace -> String
getEnv Namespace
ns
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
resolve String
lname (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/"
parseRef :: Namespace -> String -> String -> IO NODE
parseRef :: Namespace -> String -> String -> IO (String, String)
parseRef ns :: Namespace
ns ref :: String
ref base :: String
base = do
String
file <- Namespace -> String -> IO String
fromLibName Namespace
ns String
base
case Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitBy '?' String
ref of
[br :: String
br, m :: String
m] -> do let b :: String
b = String -> String
toTwelf (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
resolve String
br String
file
String
lname <- Namespace -> String -> IO String
toLibName Namespace
ns String
b
(String, String) -> IO (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
lname, String
m)
_ -> String -> IO (String, String)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Invalid reference."
getBMN :: Namespace -> Element -> NODE -> IO (BASE, MODULE, NAME)
getBMN :: Namespace
-> Element -> (String, String) -> IO (String, String, String)
getBMN ns :: Namespace
ns e :: Element
e (base :: String
base, modul :: String
modul) = do
String
file <- Namespace -> String -> IO String
fromLibName Namespace
ns String
base
let n :: String
n = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ QName -> Element -> Maybe String
findAttr QName
nameQN Element
e
let m :: String
m = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
modul (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ Element -> Maybe String
getModuleAttr Element
e
let b :: String
b = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
file (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ Element -> Maybe String
getBaseAttr Element
e
String
lname <- Namespace -> String -> IO String
toLibName Namespace
ns String
b
(String, String, String) -> IO (String, String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
lname, String
m, String
n)
addFromFile :: Namespace -> FilePath -> LIBS_EXT -> IO LIBS_EXT
addFromFile :: Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile ns :: Namespace
ns lname :: String
lname libs :: LIBS_EXT
libs@(lb :: (LIBS, [String])
lb@(l :: LIBS
l, _), (b :: String
b, gr :: GRAPH
gr)) =
if String
lname String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b Bool -> Bool -> Bool
|| String -> LIBS -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
lname LIBS
l
then LIBS_EXT -> IO LIBS_EXT
forall (m :: * -> *) a. Monad m => a -> m a
return LIBS_EXT
libs
else do String
file <- Namespace -> String -> IO String
fromLibName Namespace
ns String
lname
(LIBS, [String])
lb' <- Namespace -> String -> (LIBS, [String]) -> IO (LIBS, [String])
twelf2GR Namespace
ns String
file (LIBS, [String])
lb
LIBS_EXT -> IO LIBS_EXT
forall (m :: * -> *) a. Monad m => a -> m a
return ((LIBS, [String])
lb', (String
b, GRAPH
gr))
lookupSig :: NODE -> LIBS_EXT -> Sign
lookupSig :: (String, String) -> LIBS_EXT -> Sign
lookupSig (b :: String
b, m :: String
m) ((libs :: LIBS
libs, _), (base :: String
base, (sigs :: Map String Sign
sigs, _))) =
let sigs1 :: Map String Sign
sigs1 = if String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
base then Map String Sign
sigs else
GRAPH -> Map String Sign
forall a b. (a, b) -> a
fst (GRAPH -> Map String Sign) -> GRAPH -> Map String Sign
forall a b. (a -> b) -> a -> b
$ GRAPH -> String -> LIBS -> GRAPH
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault GRAPH
forall a. a
er String
b LIBS
libs
in Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
forall a. a
er String
m Map String Sign
sigs1
where er :: a
er = String -> a
forall a. HasCallStack => String -> a
error "Signature cannot be found."
lookupMorph :: LINK -> LIBS_EXT -> Morphism
lookupMorph :: (String, String, String) -> LIBS_EXT -> Morphism
lookupMorph (b :: String
b, m :: String
m, n :: String
n) ((libs :: LIBS
libs, _), (base :: String
base, (_, morphs :: Map ((String, String), (String, String), (String, String)) Morphism
morphs))) =
let morphs1 :: Map ((String, String), (String, String), (String, String)) Morphism
morphs1 = if String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
base then Map ((String, String), (String, String), (String, String)) Morphism
morphs else
GRAPH
-> Map
((String, String), (String, String), (String, String)) Morphism
forall a b. (a, b) -> b
snd (GRAPH
-> Map
((String, String), (String, String), (String, String)) Morphism)
-> GRAPH
-> Map
((String, String), (String, String), (String, String)) Morphism
forall a b. (a -> b) -> a -> b
$ GRAPH -> String -> LIBS -> GRAPH
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault GRAPH
forall a. a
er String
b LIBS
libs
morphs2 :: Map ((String, String), (String, String), (String, String)) Morphism
morphs2 = (((String, String), (String, String), (String, String))
-> Morphism -> Bool)
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ (l :: (String, String)
l, _, _) _ -> (String, String)
l (String, String) -> (String, String) -> Bool
forall a. Eq a => a -> a -> Bool
== (String
m, String
n)) Map ((String, String), (String, String), (String, String)) Morphism
morphs1
in case Map ((String, String), (String, String), (String, String)) Morphism
-> [(((String, String), (String, String), (String, String)),
Morphism)]
forall k a. Map k a -> [(k, a)]
Map.toList Map ((String, String), (String, String), (String, String)) Morphism
morphs2 of
[(_, morph :: Morphism
morph)] -> Morphism
morph
_ -> Morphism
forall a. a
er
where er :: a
er = String -> a
forall a. HasCallStack => String -> a
error "Morphism cannot be found."
addSigToGraph :: Sign -> LIBS_EXT -> LIBS_EXT
addSigToGraph :: Sign -> LIBS_EXT -> LIBS_EXT
addSigToGraph sig :: Sign
sig (lb :: (LIBS, [String])
lb, (b :: String
b, (sigs :: Map String Sign
sigs, morphs :: Map ((String, String), (String, String), (String, String)) Morphism
morphs))) =
let sigs1 :: Map String Sign
sigs1 = String -> Sign -> Map String Sign -> Map String Sign
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Sign -> String
sigModule Sign
sig) Sign
sig Map String Sign
sigs
in ((LIBS, [String])
lb, (String
b, (Map String Sign
sigs1, Map ((String, String), (String, String), (String, String)) Morphism
morphs)))
addMorphToGraph :: Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph :: Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph m :: Morphism
m (lb :: (LIBS, [String])
lb, (b :: String
b, (sigs :: Map String Sign
sigs, morphs :: Map ((String, String), (String, String), (String, String)) Morphism
morphs))) =
let sig1 :: Sign
sig1 = Morphism -> Sign
source Morphism
m
sig2 :: Sign
sig2 = Morphism -> Sign
target Morphism
m
l :: (String, String)
l = (Morphism -> String
morphModule Morphism
m, Morphism -> String
morphName Morphism
m)
s :: (String, String)
s = (Sign -> String
sigBase Sign
sig1, Sign -> String
sigModule Sign
sig1)
t :: (String, String)
t = (Sign -> String
sigBase Sign
sig2, Sign -> String
sigModule Sign
sig2)
morphs1 :: Map ((String, String), (String, String), (String, String)) Morphism
morphs1 = ((String, String), (String, String), (String, String))
-> Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((String, String)
l, (String, String)
s, (String, String)
t) Morphism
m Map ((String, String), (String, String), (String, String)) Morphism
morphs
in ((LIBS, [String])
lb, (String
b, (Map String Sign
sigs, Map ((String, String), (String, String), (String, String)) Morphism
morphs1)))
computeTargets :: GRAPH -> LIBS_EXT -> GRAPH
computeTargets :: GRAPH -> LIBS_EXT -> GRAPH
computeTargets (sigs :: Map String Sign
sigs, morphs :: Map ((String, String), (String, String), (String, String)) Morphism
morphs) libs :: LIBS_EXT
libs =
let morphs2 :: Map ((String, String), (String, String), (String, String)) Morphism
morphs2 = (((String, String), (String, String), (String, String))
-> Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism)
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
(\ k :: ((String, String), (String, String), (String, String))
k@((_, _), _, t :: (String, String)
t) morph :: Morphism
morph morphs1 :: Map ((String, String), (String, String), (String, String)) Morphism
morphs1 ->
let morph1 :: Morphism
morph1 = Morphism
morph { target :: Sign
target = (String, String) -> LIBS_EXT -> Sign
lookupSig (String, String)
t LIBS_EXT
libs }
in ((String, String), (String, String), (String, String))
-> Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
-> Map
((String, String), (String, String), (String, String)) Morphism
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((String, String), (String, String), (String, String))
k Morphism
morph1 Map ((String, String), (String, String), (String, String)) Morphism
morphs1
) Map ((String, String), (String, String), (String, String)) Morphism
forall k a. Map k a
Map.empty Map ((String, String), (String, String), (String, String)) Morphism
morphs
in (Map String Sign
sigs, Map ((String, String), (String, String), (String, String)) Morphism
morphs2)
twelf2SigMor :: Namespace -> FilePath -> IO LIBS
twelf2SigMor :: Namespace -> String -> IO LIBS
twelf2SigMor ns :: Namespace
ns fp :: String
fp = do
(libs :: LIBS
libs, _) <- Namespace -> String -> (LIBS, [String]) -> IO (LIBS, [String])
twelf2GR Namespace
ns String
fp (LIBS
forall k a. Map k a
Map.empty, [])
LIBS -> IO LIBS
forall (m :: * -> *) a. Monad m => a -> m a
return LIBS
libs
twelf2GR :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO (LIBS, [BASE])
twelf2GR :: Namespace -> String -> (LIBS, [String]) -> IO (LIBS, [String])
twelf2GR ns :: Namespace
ns fp :: String
fp lb :: (LIBS, [String])
lb = do
String
file <- String -> IO String
toAbsoluteURI String
fp
String -> IO ()
runTwelf String
file
le :: LIBS_EXT
le@((libs :: LIBS
libs, bs :: [String]
bs), (b :: String
b, gr :: GRAPH
gr)) <- Namespace -> String -> (LIBS, [String]) -> IO LIBS_EXT
buildGraph Namespace
ns String
file (LIBS, [String])
lb
let gr' :: GRAPH
gr' = GRAPH -> LIBS_EXT -> GRAPH
computeTargets GRAPH
gr LIBS_EXT
le
let libs' :: LIBS
libs' = String -> GRAPH -> LIBS -> LIBS
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
b GRAPH
gr' LIBS
libs
let bs' :: [String]
bs' = [String]
bs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
b]
(LIBS, [String]) -> IO (LIBS, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS
libs', [String]
bs')
runTwelf :: FilePath -> IO ()
runTwelf :: String -> IO ()
runTwelf file :: String
file = do
let dir :: String
dir = String -> String
dropFileName String
file
String
twelfdir <- String -> IO String
getEnvVar String
twelfEnv
(_, out :: Handle
out, err :: Handle
err, pr :: ProcessHandle
pr) <-
String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
twelfdir, "/" , String
twelf])
([String]
options [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
dir, String
file])
Maybe String
forall a. Maybe a
Nothing
Maybe [(String, String)]
forall a. Maybe a
Nothing
ExitCode
exitCode <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pr
String
outH <- Handle -> IO String
hGetContents Handle
out
String
errH <- Handle -> IO String
hGetContents Handle
err
case ExitCode
exitCode of
ExitFailure i :: Int
i -> do
String -> IO ()
putStrLn (String
outH String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errH)
String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Calling Twelf failed with exitCode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++
" on file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "dir: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "twelfdir: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
twelfdir
ExitSuccess -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
buildGraph :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO LIBS_EXT
buildGraph :: Namespace -> String -> (LIBS, [String]) -> IO LIBS_EXT
buildGraph ns :: Namespace
ns file :: String
file lb :: (LIBS, [String])
lb = do
String
xml <- String -> IO String
readFile (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String
toOMDoc String
file
String
lname <- Namespace -> String -> IO String
toLibName Namespace
ns String
file
let elems :: [Element]
elems = [Content] -> [Element]
onlyElems ([Content] -> [Element]) -> [Content] -> [Element]
forall a b. (a -> b) -> a -> b
$ String -> [Content]
forall s. XmlSource s => s -> [Content]
parseXML String
xml
let elems1 :: [Element]
elems1 = (Element -> Bool) -> [Element] -> [Element]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ e :: Element
e -> Element -> QName
elName Element
e QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omdocQN) [Element]
elems
case [Element]
elems1 of
[root :: Element
root] ->
(LIBS_EXT -> Element -> IO LIBS_EXT)
-> LIBS_EXT -> [Element] -> IO LIBS_EXT
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ libs :: LIBS_EXT
libs e :: Element
e ->
let n :: QName
n = Element -> QName
elName Element
e
in if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
theoryQN then Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addSign Namespace
ns Element
e LIBS_EXT
libs else
if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
viewQN then Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addView Namespace
ns Element
e LIBS_EXT
libs else
LIBS_EXT -> IO LIBS_EXT
forall (m :: * -> *) a. Monad m => a -> m a
return LIBS_EXT
libs
)
((LIBS, [String])
lb, (String
lname, GRAPH
emptyGraph))
([Element] -> IO LIBS_EXT) -> [Element] -> IO LIBS_EXT
forall a b. (a -> b) -> a -> b
$ Element -> [Element]
elChildren Element
root
_ -> String -> IO LIBS_EXT
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Not an OMDoc file."
addSign :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addSign :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addSign ns :: Namespace
ns e :: Element
e libs :: LIBS_EXT
libs@(_, (lname :: String
lname, _)) = do
let sig :: Sign
sig = String -> String -> [DEF] -> Sign
Sign String
lname (Element -> String
getNameAttr Element
e) []
(libs1 :: LIBS_EXT
libs1, sig1 :: Sign
sig1) <-
((LIBS_EXT, Sign) -> Element -> IO (LIBS_EXT, Sign))
-> (LIBS_EXT, Sign) -> [Element] -> IO (LIBS_EXT, Sign)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ ls :: (LIBS_EXT, Sign)
ls el :: Element
el ->
let n :: QName
n = Element -> QName
elName Element
el
in if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
includeQN then Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addIncl Namespace
ns Element
el (LIBS_EXT, Sign)
ls else
if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
structureQN then Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addStruct Namespace
ns Element
el (LIBS_EXT, Sign)
ls else
if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
constantQN then Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addConst Namespace
ns Element
el (LIBS_EXT, Sign)
ls else
(LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS_EXT, Sign)
ls
)
(LIBS_EXT
libs, Sign
sig)
([Element] -> IO (LIBS_EXT, Sign))
-> [Element] -> IO (LIBS_EXT, Sign)
forall a b. (a -> b) -> a -> b
$ Element -> [Element]
elChildren Element
e
LIBS_EXT -> IO LIBS_EXT
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS_EXT -> IO LIBS_EXT) -> LIBS_EXT -> IO LIBS_EXT
forall a b. (a -> b) -> a -> b
$ Sign -> LIBS_EXT -> LIBS_EXT
addSigToGraph Sign
sig1 LIBS_EXT
libs1
addView :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addView :: Namespace -> Element -> LIBS_EXT -> IO LIBS_EXT
addView ns :: Namespace
ns e :: Element
e libs :: LIBS_EXT
libs@(_, (lname :: String
lname, _)) = do
let name :: String
name = Element -> String
getNameAttr Element
e
let from :: String
from = Element -> String
getFromAttr Element
e
let to :: String
to = Element -> String
getToAttr Element
e
(b1 :: String
b1, m1 :: String
m1) <- Namespace -> String -> String -> IO (String, String)
parseRef Namespace
ns String
from String
lname
(b2 :: String
b2, m2 :: String
m2) <- Namespace -> String -> String -> IO (String, String)
parseRef Namespace
ns String
to String
lname
LIBS_EXT
libs1 <- Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile Namespace
ns String
b1 LIBS_EXT
libs
LIBS_EXT
libs2 <- Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile Namespace
ns String
b2 LIBS_EXT
libs1
let srcSig :: Sign
srcSig = (String, String) -> LIBS_EXT -> Sign
lookupSig (String
b1, String
m1) LIBS_EXT
libs2
let tarSig :: Sign
tarSig = (String, String) -> LIBS_EXT -> Sign
lookupSig (String
b2, String
m2) LIBS_EXT
libs2
(morph :: Morphism
morph, libs3 :: LIBS_EXT
libs3) <- Namespace
-> String
-> Sign
-> Sign
-> [Element]
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
getViewMorph Namespace
ns String
name Sign
srcSig Sign
tarSig (Element -> [Element]
elChildren Element
e) LIBS_EXT
libs2
let libs4 :: LIBS_EXT
libs4 = Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph Morphism
morph LIBS_EXT
libs3
LIBS_EXT -> IO LIBS_EXT
forall (m :: * -> *) a. Monad m => a -> m a
return LIBS_EXT
libs4
getViewMorph :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT ->
IO (Morphism, LIBS_EXT)
getViewMorph :: Namespace
-> String
-> Sign
-> Sign
-> [Element]
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
getViewMorph ns :: Namespace
ns name :: String
name srcSig :: Sign
srcSig tarSig :: Sign
tarSig els :: [Element]
els libs :: LIBS_EXT
libs@(_, (lname :: String
lname, _)) = do
let b1 :: String
b1 = Sign -> String
sigBase Sign
srcSig
let m1 :: String
m1 = Sign -> String
sigModule Sign
srcSig
let b2 :: String
b2 = Sign -> String
sigBase Sign
tarSig
let m2 :: String
m2 = Sign -> String
sigModule Sign
tarSig
(symmap :: Map Symbol EXP
symmap, libs1 :: LIBS_EXT
libs1) <- Namespace
-> [Element]
-> (String, String)
-> (String, String)
-> LIBS_EXT
-> IO (Map Symbol EXP, LIBS_EXT)
constructMap Namespace
ns [Element]
els (String
b1, String
m1) (String
b2, String
m2) LIBS_EXT
libs
let morph :: Morphism
morph = String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
lname String
name "" Sign
srcSig Sign
tarSig MorphType
Postulated Map Symbol EXP
symmap
(Morphism, LIBS_EXT) -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism
morph, LIBS_EXT
libs1)
addConst :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addConst :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addConst ns :: Namespace
ns e :: Element
e (libs :: LIBS_EXT
libs, sig :: Sign
sig) = do
let ref :: (String, String)
ref@(b :: String
b, m :: String
m) = (Sign -> String
sigBase Sign
sig, Sign -> String
sigModule Sign
sig)
let sym :: Symbol
sym = String -> String -> String -> Symbol
Symbol String
b String
m (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ Element -> String
getNameAttr Element
e
EXP
typ <- case QName -> Element -> [Element]
findChildren QName
typeQN Element
e of
[t :: Element
t] -> Namespace -> Element -> (String, String) -> IO EXP
type2exp Namespace
ns Element
t (String, String)
ref
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Constant element must have a unique type child."
Maybe EXP
val <- case QName -> Element -> [Element]
findChildren QName
definitionQN Element
e of
[] -> Maybe EXP -> IO (Maybe EXP)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe EXP
forall a. Maybe a
Nothing
[v :: Element
v] -> (EXP -> Maybe EXP) -> IO EXP -> IO (Maybe EXP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EXP -> Maybe EXP
forall a. a -> Maybe a
Just (IO EXP -> IO (Maybe EXP)) -> IO EXP -> IO (Maybe EXP)
forall a b. (a -> b) -> a -> b
$ Namespace -> Element -> (String, String) -> IO EXP
definition2exp Namespace
ns Element
v (String, String)
ref
_ -> String -> IO (Maybe EXP)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO (Maybe EXP)) -> String -> IO (Maybe EXP)
forall a b. (a -> b) -> a -> b
$ "Constant element must have at most " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"one definition child."
let sig1 :: Sign
sig1 = DEF -> Sign -> Sign
addDef (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
sym EXP
typ Maybe EXP
val) Sign
sig
(LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS_EXT
libs, Sign
sig1)
type2exp :: Namespace -> Element -> NODE -> IO EXP
type2exp :: Namespace -> Element -> (String, String) -> IO EXP
type2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case QName -> Element -> [Element]
findChildren QName
omobjQN Element
e of
[omobj :: Element
omobj] -> Namespace -> Element -> (String, String) -> IO EXP
omobj2exp Namespace
ns Element
omobj (String, String)
ref
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Type element must have a unique OMOBJ child."
definition2exp :: Namespace -> Element -> NODE -> IO EXP
definition2exp :: Namespace -> Element -> (String, String) -> IO EXP
definition2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case QName -> Element -> [Element]
findChildren QName
omobjQN Element
e of
[omobj :: Element
omobj] -> Namespace -> Element -> (String, String) -> IO EXP
omobj2exp Namespace
ns Element
omobj (String, String)
ref
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Definition element must have a unique OMOBJ child."
omobj2exp :: Namespace -> Element -> NODE -> IO EXP
omobj2exp :: Namespace -> Element -> (String, String) -> IO EXP
omobj2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case Element -> [Element]
elChildren Element
e of
[el :: Element
el] -> Namespace -> Element -> (String, String) -> IO EXP
omel2exp Namespace
ns Element
el (String, String)
ref
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMOBJ element must have a unique child."
omel2exp :: Namespace -> Element -> NODE -> IO EXP
omel2exp :: Namespace -> Element -> (String, String) -> IO EXP
omel2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
let name :: QName
name = Element -> QName
elName Element
e
in if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omsQN then Namespace -> Element -> (String, String) -> IO EXP
oms2exp Namespace
ns Element
e (String, String)
ref else
if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omaQN then Namespace -> Element -> (String, String) -> IO EXP
oma2exp Namespace
ns Element
e (String, String)
ref else
if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
ombindQN then Namespace -> Element -> (String, String) -> IO EXP
ombind2exp Namespace
ns Element
e (String, String)
ref else
if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omvQN then Namespace -> Element -> (String, String) -> IO EXP
omv2exp Namespace
ns Element
e (String, String)
ref else
String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO EXP) -> String -> IO EXP
forall a b. (a -> b) -> a -> b
$ "Only OMA, OMS, and OMBIND elements correspond " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"to an expression."
oms2exp :: Namespace -> Element -> NODE -> IO EXP
oms2exp :: Namespace -> Element -> (String, String) -> IO EXP
oms2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
if Element -> Element -> Bool
eqOMS Element
e Element
typeOMS then EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return EXP
Type else do
(b :: String
b, m :: String
m, n :: String
n) <- Namespace
-> Element -> (String, String) -> IO (String, String, String)
getBMN Namespace
ns Element
e (String, String)
ref
EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP
Const (Symbol -> EXP) -> Symbol -> EXP
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> Symbol
Symbol String
b String
m String
n
oma2exp :: Namespace -> Element -> NODE -> IO EXP
oma2exp :: Namespace -> Element -> (String, String) -> IO EXP
oma2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case Element -> [Element]
elChildren Element
e of
[] -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMA element must have at least one child."
(f :: Element
f : as :: [Element]
as) -> do
[EXP]
as1 <- (Element -> IO EXP) -> [Element] -> IO [EXP]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ a :: Element
a -> Namespace -> Element -> (String, String) -> IO EXP
omel2exp Namespace
ns Element
a (String, String)
ref) [Element]
as
if Element -> Element -> Bool
eqOMS Element
f Element
arrowOMS
then case [EXP]
as1 of
[] -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO EXP) -> String -> IO EXP
forall a b. (a -> b) -> a -> b
$ "The -> constructor must be applied" String -> String -> String
forall a. [a] -> [a] -> [a]
++
" to at least one argument."
_ -> EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> EXP -> EXP
Func ([EXP] -> [EXP]
forall a. [a] -> [a]
init [EXP]
as1) ([EXP] -> EXP
forall a. [a] -> a
last [EXP]
as1)
else do EXP
f1 <- Namespace -> Element -> (String, String) -> IO EXP
omel2exp Namespace
ns Element
f (String, String)
ref
EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ EXP -> [EXP] -> EXP
Appl EXP
f1 [EXP]
as1
ombind2exp :: Namespace -> Element -> NODE -> IO EXP
ombind2exp :: Namespace -> Element -> (String, String) -> IO EXP
ombind2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case Element -> [Element]
elChildren Element
e of
[f :: Element
f, d :: Element
d, b :: Element
b] ->
if Element -> QName
elName Element
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
ombvarQN
then String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "The second child of OMBIND must be OMBVAR."
else do CONTEXT
d1 <- Namespace -> Element -> (String, String) -> IO CONTEXT
ombvar2decls Namespace
ns Element
d (String, String)
ref
EXP
b1 <- Namespace -> Element -> (String, String) -> IO EXP
omel2exp Namespace
ns Element
b (String, String)
ref
if Element -> Element -> Bool
eqOMS Element
f Element
lambdaOMS then EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Lamb CONTEXT
d1 EXP
b1 else
if Element -> Element -> Bool
eqOMS Element
f Element
piOMS then EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Pi CONTEXT
d1 EXP
b1 else
if Element -> Element -> Bool
eqOMS Element
f Element
impLambdaOMS then EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Lamb CONTEXT
d1 EXP
b1 else
if Element -> Element -> Bool
eqOMS Element
f Element
impPiOMS then EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Pi CONTEXT
d1 EXP
b1 else
String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "The first child of OMBIND must be be Pi or Lambda."
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMBIND element must have exactly 3 children."
ombvar2decls :: Namespace -> Element -> NODE -> IO CONTEXT
ombvar2decls :: Namespace -> Element -> (String, String) -> IO CONTEXT
ombvar2decls ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
(Element -> IO (String, EXP)) -> [Element] -> IO CONTEXT
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ a :: Element
a -> Namespace -> Element -> (String, String) -> IO (String, EXP)
omattr2vardecl Namespace
ns Element
a (String, String)
ref) ([Element] -> IO CONTEXT) -> [Element] -> IO CONTEXT
forall a b. (a -> b) -> a -> b
$ QName -> Element -> [Element]
findChildren QName
omattrQN Element
e
omattr2vardecl :: Namespace -> Element -> NODE -> IO (VAR, EXP)
omattr2vardecl :: Namespace -> Element -> (String, String) -> IO (String, EXP)
omattr2vardecl ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case QName -> Element -> [Element]
findChildren QName
omatpQN Element
e of
[omatp :: Element
omatp] -> do
EXP
val <- Namespace -> Element -> (String, String) -> IO EXP
omatp2exp Namespace
ns Element
omatp (String, String)
ref
case QName -> Element -> [Element]
findChildren QName
omvQN Element
e of
[omv :: Element
omv] -> (String, EXP) -> IO (String, EXP)
forall (m :: * -> *) a. Monad m => a -> m a
return (Element -> String
getNameAttr Element
omv, EXP
val)
_ -> String -> IO (String, EXP)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMATTR element must have a unique OMV child."
_ -> String -> IO (String, EXP)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMATTR element must have a unique OMATP child."
omatp2exp :: Namespace -> Element -> NODE -> IO EXP
omatp2exp :: Namespace -> Element -> (String, String) -> IO EXP
omatp2exp ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref =
case Element -> [Element]
elChildren Element
e of
[c1 :: Element
c1, c2 :: Element
c2] ->
if Element -> Element -> Bool
eqOMS Element
c1 Element
oftypeOMS
then Namespace -> Element -> (String, String) -> IO EXP
omel2exp Namespace
ns Element
c2 (String, String)
ref
else String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO EXP) -> String -> IO EXP
forall a b. (a -> b) -> a -> b
$ "The first child of OMATP " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"must be the \"oftype\" symbol."
_ -> String -> IO EXP
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMATP element must have exactly two children."
omv2exp :: Namespace -> Element -> NODE -> IO EXP
omv2exp :: Namespace -> Element -> (String, String) -> IO EXP
omv2exp _ e :: Element
e _ = EXP -> IO EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> IO EXP) -> EXP -> IO EXP
forall a b. (a -> b) -> a -> b
$ String -> EXP
Var (String -> EXP) -> String -> EXP
forall a b. (a -> b) -> a -> b
$ Element -> String
getNameAttr Element
e
addIncl :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addIncl :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addIncl ns :: Namespace
ns e :: Element
e (libs :: LIBS_EXT
libs@(_, (lname :: String
lname, _)), sig :: Sign
sig) = do
let from :: String
from = Element -> String
getFromAttr Element
e
(b :: String
b, m :: String
m) <- Namespace -> String -> String -> IO (String, String)
parseRef Namespace
ns String
from String
lname
LIBS_EXT
libs1 <- Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile Namespace
ns String
b LIBS_EXT
libs
let srcSig :: Sign
srcSig = (String, String) -> LIBS_EXT -> Sign
lookupSig (String
b, String
m) LIBS_EXT
libs1
let tarSig :: Sign
tarSig = Sign -> Sign -> Sign
addInclSyms Sign
srcSig Sign
sig
let morph :: Morphism
morph = Sign -> Sign -> Morphism
getInclMorph Sign
srcSig Sign
tarSig
let libs2 :: LIBS_EXT
libs2 = Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph Morphism
morph LIBS_EXT
libs1
(LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS_EXT
libs2, Sign
tarSig)
addInclSyms :: Sign -> Sign -> Sign
addInclSyms :: Sign -> Sign -> Sign
addInclSyms (Sign _ _ ds :: [DEF]
ds) sig :: Sign
sig =
let syms :: Set Symbol
syms = Sign -> Set Symbol
getSymbols Sign
sig
in (Sign -> DEF -> Sign) -> Sign -> [DEF] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ sig1 :: Sign
sig1 d :: DEF
d ->
if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (DEF -> Symbol
getSym DEF
d) Set Symbol
syms
then Sign
sig1
else DEF -> Sign -> Sign
addDef DEF
d Sign
sig1
) Sign
sig [DEF]
ds
getInclMorph :: Sign -> Sign -> Morphism
getInclMorph :: Sign -> Sign -> Morphism
getInclMorph sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism (Sign -> String
sigBase Sign
sig2) (Sign -> String
sigModule Sign
sig2) "" Sign
sig1 Sign
sig2 MorphType
Definitional Map Symbol EXP
forall k a. Map k a
Map.empty
addStruct :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addStruct :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addStruct ns :: Namespace
ns e :: Element
e (libs :: LIBS_EXT
libs@(_, (lname :: String
lname, _)), sig :: Sign
sig) = do
let name :: String
name = Element -> String
getNameAttr Element
e
let from :: String
from = Element -> String
getFromAttr Element
e
(b :: String
b, m :: String
m) <- Namespace -> String -> String -> IO (String, String)
parseRef Namespace
ns String
from String
lname
LIBS_EXT
libs1 <- Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile Namespace
ns String
b LIBS_EXT
libs
let srcSig :: Sign
srcSig = (String, String) -> LIBS_EXT -> Sign
lookupSig (String
b, String
m) LIBS_EXT
libs1
(tarSig :: Sign
tarSig, morph :: Morphism
morph, libs2 :: LIBS_EXT
libs2) <- Namespace
-> String
-> Sign
-> Sign
-> [Element]
-> LIBS_EXT
-> IO (Sign, Morphism, LIBS_EXT)
processStruct Namespace
ns String
name Sign
srcSig Sign
sig (Element -> [Element]
elChildren Element
e) LIBS_EXT
libs1
let libs3 :: LIBS_EXT
libs3 = Morphism -> LIBS_EXT -> LIBS_EXT
addMorphToGraph Morphism
morph LIBS_EXT
libs2
(LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIBS_EXT
libs3, Sign
tarSig)
processStruct :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT ->
IO (Sign, Morphism, LIBS_EXT)
processStruct :: Namespace
-> String
-> Sign
-> Sign
-> [Element]
-> LIBS_EXT
-> IO (Sign, Morphism, LIBS_EXT)
processStruct ns :: Namespace
ns name :: String
name srcSig :: Sign
srcSig tarSig :: Sign
tarSig els :: [Element]
els libs :: LIBS_EXT
libs = do
let b1 :: String
b1 = Sign -> String
sigBase Sign
srcSig
let m1 :: String
m1 = Sign -> String
sigModule Sign
srcSig
let b2 :: String
b2 = Sign -> String
sigBase Sign
tarSig
let m2 :: String
m2 = Sign -> String
sigModule Sign
tarSig
let prefix :: String
prefix = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
structDelimS
let rel :: Symbol -> Symbol
rel sym :: Symbol
sym = String -> String -> String -> Symbol
Symbol String
b2 String
m2 (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
symName Symbol
sym
(symmap :: Map Symbol EXP
symmap, libs1 :: LIBS_EXT
libs1) <- Namespace
-> [Element]
-> (String, String)
-> (String, String)
-> LIBS_EXT
-> IO (Map Symbol EXP, LIBS_EXT)
constructMap Namespace
ns [Element]
els (String
b1, String
m1) (String
b2, String
m2) LIBS_EXT
libs
let Sign _ _ ds :: [DEF]
ds = Sign
srcSig
let morph_init :: Morphism
morph_init =
String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
b2 String
m2 String
name (String -> String -> [DEF] -> Sign
Sign String
b1 String
m1 []) Sign
tarSig MorphType
Definitional Map Symbol EXP
forall k a. Map k a
Map.empty
let (sig2 :: Sign
sig2, morph2 :: Morphism
morph2) =
((Sign, Morphism) -> DEF -> (Sign, Morphism))
-> (Sign, Morphism) -> [DEF] -> (Sign, Morphism)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (sig :: Sign
sig, morph :: Morphism
morph) (Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) ->
let local :: Bool
local = Symbol -> Sign -> Bool
isLocalSym Symbol
s Sign
srcSig
defined :: Bool
defined = Symbol -> Sign -> Bool
isDefinedSym Symbol
s Sign
srcSig
sig1 :: Sign
sig1 = if Bool -> Bool
not Bool
local then Sign
sig else
let s1 :: Symbol
s1 = Symbol -> Symbol
rel Symbol
s
t1 :: EXP
t1 = EXP -> Maybe EXP -> EXP
forall a. a -> Maybe a -> a
fromMaybe (String -> EXP
forall a. HasCallStack => String -> a
error (String -> EXP) -> String -> EXP
forall a b. (a -> b) -> a -> b
$
"Structure could not be formed. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name) (Maybe EXP -> EXP) -> Maybe EXP -> EXP
forall a b. (a -> b) -> a -> b
$
Morphism -> EXP -> Maybe EXP
translate Morphism
morph EXP
t
v1 :: Maybe EXP
v1 = case Maybe EXP
v of
Just v1' :: EXP
v1' -> Morphism -> EXP -> Maybe EXP
translate Morphism
morph EXP
v1'
Nothing -> Symbol -> Map Symbol EXP -> Maybe EXP
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s Map Symbol EXP
symmap
in DEF -> Sign -> Sign
addDef (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
s1 EXP
t1 Maybe EXP
v1) Sign
sig
morph1 :: Morphism
morph1 = let source1 :: Sign
source1 = DEF -> Sign -> Sign
addDef (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
s EXP
t Maybe EXP
v) (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
morph
e :: EXP
e = if Bool
local
then Symbol -> EXP
Const (Symbol -> EXP) -> Symbol -> EXP
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
rel Symbol
s
else EXP -> Symbol -> Map Symbol EXP -> EXP
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Symbol -> EXP
Const Symbol
s)
Symbol
s Map Symbol EXP
symmap
map1 :: Map Symbol EXP
map1 = if Bool
defined
then Morphism -> Map Symbol EXP
symMap Morphism
morph
else Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
s EXP
e (Map Symbol EXP -> Map Symbol EXP)
-> Map Symbol EXP -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Symbol EXP
symMap Morphism
morph
in Morphism
morph { source :: Sign
source = Sign
source1
, target :: Sign
target = Sign
sig1
, symMap :: Map Symbol EXP
symMap = Map Symbol EXP
map1 }
in (Sign
sig1, Morphism -> Morphism
canForm Morphism
morph1)
) (Sign
tarSig, Morphism
morph_init) [DEF]
ds
(Sign, Morphism, LIBS_EXT) -> IO (Sign, Morphism, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig2, Morphism
morph2, LIBS_EXT
libs1)
constructMap :: Namespace -> [Element] -> NODE -> NODE -> LIBS_EXT ->
IO (Map.Map Symbol EXP, LIBS_EXT)
constructMap :: Namespace
-> [Element]
-> (String, String)
-> (String, String)
-> LIBS_EXT
-> IO (Map Symbol EXP, LIBS_EXT)
constructMap ns :: Namespace
ns els :: [Element]
els src :: (String, String)
src tar :: (String, String)
tar libs :: LIBS_EXT
libs =
((Map Symbol EXP, LIBS_EXT)
-> Element -> IO (Map Symbol EXP, LIBS_EXT))
-> (Map Symbol EXP, LIBS_EXT)
-> [Element]
-> IO (Map Symbol EXP, LIBS_EXT)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ ml :: (Map Symbol EXP, LIBS_EXT)
ml el :: Element
el ->
let n :: QName
n = Element -> QName
elName Element
el
in if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
conassQN then Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
conass2map Namespace
ns Element
el (Map Symbol EXP, LIBS_EXT)
ml (String, String)
src (String, String)
tar else
if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
includeQN then Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
incl2map Namespace
ns Element
el (Map Symbol EXP, LIBS_EXT)
ml (String, String)
src (String, String)
tar else
if QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
strassQN then Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
strass2map Namespace
ns Element
el (Map Symbol EXP, LIBS_EXT)
ml (String, String)
src (String, String)
tar else
(Map Symbol EXP, LIBS_EXT) -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol EXP, LIBS_EXT)
ml
) (Map Symbol EXP
forall k a. Map k a
Map.empty, LIBS_EXT
libs) [Element]
els
conass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
conass2map :: Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
conass2map ns :: Namespace
ns e :: Element
e (mapp :: Map Symbol EXP
mapp, libs :: LIBS_EXT
libs) src :: (String, String)
src tar :: (String, String)
tar = do
(b :: String
b, m :: String
m, n :: String
n) <- Namespace
-> Element -> (String, String) -> IO (String, String, String)
getBMN Namespace
ns Element
e (String, String)
src
case QName -> Element -> [Element]
findChildren QName
omobjQN Element
e of
[omobj :: Element
omobj] -> do EXP
expr <- Namespace -> Element -> (String, String) -> IO EXP
omobj2exp Namespace
ns Element
omobj (String, String)
tar
let map1 :: Map Symbol EXP
map1 = Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> String -> String -> Symbol
Symbol String
b String
m String
n) EXP
expr Map Symbol EXP
mapp
(Map Symbol EXP, LIBS_EXT) -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol EXP
map1, LIBS_EXT
libs)
_ -> String -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Constant assignment element must have a unique OMOBJ child."
incl2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
incl2map :: Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
incl2map ns :: Namespace
ns e :: Element
e (mapp :: Map Symbol EXP
mapp, libs :: LIBS_EXT
libs) _ tar :: (String, String)
tar =
case QName -> Element -> [Element]
findChildren QName
ommorQN Element
e of
[ommor :: Element
ommor] -> do (mor :: Morphism
mor, libs1 :: LIBS_EXT
libs1) <- Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
ommor2mor Namespace
ns Element
ommor (String, String)
tar LIBS_EXT
libs
let map1 :: Map Symbol EXP
map1 = Map Symbol EXP -> Map Symbol EXP -> Map Symbol EXP
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Symbol EXP
mapp (Map Symbol EXP -> Map Symbol EXP)
-> Map Symbol EXP -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Symbol EXP
symMap Morphism
mor
(Map Symbol EXP, LIBS_EXT) -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol EXP
map1, LIBS_EXT
libs1)
_ -> String -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Include element must have a unique OMMOR child."
strass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
strass2map :: Namespace
-> Element
-> (Map Symbol EXP, LIBS_EXT)
-> (String, String)
-> (String, String)
-> IO (Map Symbol EXP, LIBS_EXT)
strass2map ns :: Namespace
ns e :: Element
e (mapp :: Map Symbol EXP
mapp, libs :: LIBS_EXT
libs) src :: (String, String)
src tar :: (String, String)
tar = do
(b :: String
b, m :: String
m, n :: String
n) <- Namespace
-> Element -> (String, String) -> IO (String, String, String)
getBMN Namespace
ns Element
e (String, String)
src
case QName -> Element -> [Element]
findChildren QName
ommorQN Element
e of
[ommor :: Element
ommor] -> do (mor1 :: Morphism
mor1, libs1 :: LIBS_EXT
libs1) <- Namespace
-> (String, String, String) -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
retrieveMorph Namespace
ns (String
b, String
m, String
n) LIBS_EXT
libs
(mor2 :: Morphism
mor2, libs2 :: LIBS_EXT
libs2) <- Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
ommor2mor Namespace
ns Element
ommor (String, String)
tar LIBS_EXT
libs1
let map1 :: Map Symbol EXP
map1 = Map Symbol EXP -> Map Symbol EXP -> Map Symbol EXP
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Symbol EXP
mapp (Map Symbol EXP -> Map Symbol EXP)
-> Map Symbol EXP -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism -> Map Symbol EXP
combineMorphs Morphism
mor1 Morphism
mor2
(Map Symbol EXP, LIBS_EXT) -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol EXP
map1, LIBS_EXT
libs2)
_ -> String -> IO (Map Symbol EXP, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Structure assignment element must have a unique OMMOR child."
ommor2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
ommor2mor :: Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
ommor2mor ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref libs :: LIBS_EXT
libs =
case Element -> [Element]
elChildren Element
e of
[el :: Element
el] -> Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
omel2mor Namespace
ns Element
el (String, String)
ref LIBS_EXT
libs
_ -> String -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMMOR element must have a unique child."
omel2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
omel2mor :: Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
omel2mor ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref libs :: LIBS_EXT
libs =
let name :: QName
name = Element -> QName
elName Element
e
in if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omsQN then Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
oms2mor Namespace
ns Element
e (String, String)
ref LIBS_EXT
libs else
if QName
name QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
omaQN then Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
oma2mor Namespace
ns Element
e (String, String)
ref LIBS_EXT
libs else
String -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Only OMA and OMS elements correspond to a morphism."
oms2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
oms2mor :: Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
oms2mor ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref libs :: LIBS_EXT
libs = do
(b :: String
b, m :: String
m, n :: String
n) <- Namespace
-> Element -> (String, String) -> IO (String, String, String)
getBMN Namespace
ns Element
e (String, String)
ref
Namespace
-> (String, String, String) -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
retrieveMorph Namespace
ns (String
b, String
m, String
n) LIBS_EXT
libs
oma2mor :: Namespace -> Element -> NODE -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
oma2mor :: Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
oma2mor ns :: Namespace
ns e :: Element
e ref :: (String, String)
ref libs :: LIBS_EXT
libs =
case Element -> [Element]
elChildren Element
e of
[c :: Element
c, m1 :: Element
m1, m2 :: Element
m2] ->
if Element -> Element -> Bool
eqOMS Element
c Element
compOMS
then do (mor1 :: Morphism
mor1, libs1 :: LIBS_EXT
libs1) <- Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
omel2mor Namespace
ns Element
m1 (String, String)
ref LIBS_EXT
libs
(mor2 :: Morphism
mor2, libs2 :: LIBS_EXT
libs2) <- Namespace
-> Element
-> (String, String)
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
omel2mor Namespace
ns Element
m2 (String, String)
ref LIBS_EXT
libs1
let morR :: Result Morphism
morR = Morphism -> Morphism -> Result Morphism
compMorph (Morphism
mor1 { target :: Sign
target = Morphism -> Sign
source Morphism
mor2 }) Morphism
mor2
let mor :: Morphism
mor = case Result Morphism
morR of
Result _ (Just mor' :: Morphism
mor') -> Morphism
mor'
_ -> String -> Morphism
forall a. HasCallStack => String -> a
error "Morphism cannot be retrieved."
(Morphism, LIBS_EXT) -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism
mor, LIBS_EXT
libs2)
else String -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "The first child of OMA in OMMOR must be composition."
_ -> String -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMA in OMMOR must have exactly three children."
retrieveMorph :: Namespace -> LINK -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
retrieveMorph :: Namespace
-> (String, String, String) -> LIBS_EXT -> IO (Morphism, LIBS_EXT)
retrieveMorph ns :: Namespace
ns (b :: String
b, m :: String
m, n :: String
n) = Namespace
-> String
-> String
-> [String]
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
retrieveMorphH Namespace
ns String
b String
m (Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitBy '/' String
n)
retrieveMorphH :: Namespace -> BASE -> MODULE -> [NAME] -> LIBS_EXT ->
IO (Morphism, LIBS_EXT)
retrieveMorphH :: Namespace
-> String
-> String
-> [String]
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
retrieveMorphH ns :: Namespace
ns b :: String
b m :: String
m names :: [String]
names libs :: LIBS_EXT
libs = do
LIBS_EXT
libs1 <- Namespace -> String -> LIBS_EXT -> IO LIBS_EXT
addFromFile Namespace
ns String
b LIBS_EXT
libs
case [String]
names of
[] -> String -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Empty morphism name."
[n :: String
n] -> do
let mor :: Morphism
mor = (String, String, String) -> LIBS_EXT -> Morphism
lookupMorph (String
b, String
m, String
n) LIBS_EXT
libs1
(Morphism, LIBS_EXT) -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism
mor, LIBS_EXT
libs1)
(n1 :: String
n1 : n2 :: [String]
n2) -> do
let mor1 :: Morphism
mor1 = (String, String, String) -> LIBS_EXT -> Morphism
lookupMorph (String
b, String
m, String
n1) LIBS_EXT
libs1
let sig :: Sign
sig = Morphism -> Sign
source Morphism
mor1
let b1 :: String
b1 = Sign -> String
sigBase Sign
sig
let m1 :: String
m1 = Sign -> String
sigModule Sign
sig
(mor2 :: Morphism
mor2, libs2 :: LIBS_EXT
libs2) <- Namespace
-> String
-> String
-> [String]
-> LIBS_EXT
-> IO (Morphism, LIBS_EXT)
retrieveMorphH Namespace
ns String
b1 String
m1 [String]
n2 LIBS_EXT
libs1
let morR :: Result Morphism
morR = Morphism -> Morphism -> Result Morphism
compMorph (Morphism
mor2 { target :: Sign
target = Sign
sig }) Morphism
mor1
let mor :: Morphism
mor = case Result Morphism
morR of
Result _ (Just mor' :: Morphism
mor') -> Morphism
mor'
_ -> String -> Morphism
forall a. HasCallStack => String -> a
error "Morphism cannot be retrieved."
(Morphism, LIBS_EXT) -> IO (Morphism, LIBS_EXT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism
mor, LIBS_EXT
libs2)
combineMorphs :: Morphism -> Morphism -> Map.Map Symbol EXP
combineMorphs :: Morphism -> Morphism -> Map Symbol EXP
combineMorphs mor1 :: Morphism
mor1 mor2 :: Morphism
mor2 =
let local :: Set Symbol
local = Sign -> Set Symbol
getLocalSyms (Sign -> Set Symbol) -> Sign -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
mor1
declared :: Set Symbol
declared = Sign -> Set Symbol
getDeclaredSyms (Sign -> Set Symbol) -> Sign -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
mor1
er :: a
er = String -> a
forall a. HasCallStack => String -> a
error "Morphisms cannot be combined."
in (Symbol -> Map Symbol EXP -> Map Symbol EXP)
-> Map Symbol EXP -> Set Symbol -> Map Symbol EXP
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ s :: Symbol
s ->
let s1 :: Symbol
s1 = case Symbol -> Morphism -> Maybe EXP
mapSymbol Symbol
s Morphism
mor1 of
Just (Const s1' :: Symbol
s1') -> Symbol
s1'
_ -> Symbol
forall a. a
er
e1 :: EXP
e1 = case Symbol -> Morphism -> Maybe EXP
mapSymbol Symbol
s Morphism
mor2 of
Just e1' :: EXP
e1' -> EXP
e1'
_ -> EXP
forall a. a
er
in Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
s1 EXP
e1
) Map Symbol EXP
forall k a. Map k a
Map.empty (Set Symbol -> Map Symbol EXP) -> Set Symbol -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Symbol
local Set Symbol
declared