{- |
Module      :  ./LF/Twelf2GR.hs
Description :  Conversion of Twelf files to LF signatures and morphisms
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module LF.Twelf2GR where

import System.Exit
import System.Process
import System.Directory
import System.FilePath
import System.IO (hGetContents)


import LF.Sign
import LF.Morphism

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe (fromMaybe)

import Common.IRI
import Common.Result
import Common.Utils
import Common.Keywords

import Control.Monad
import 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"

-- path to the Twelf folder must be set in the environment variable TWELF_LIB
twelf :: String
twelf :: String
twelf = "check-some"

options :: [String]
options :: [String]
options = ["-omdoc"]

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
HELPER FUNCTIONS -}

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

-- compares two OMS elements
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
{- and [ getNameAttr e1 == getNameAttr e2
, getModuleAttr e1 == getModuleAttr e2
, getBaseAttr e1 == getBaseAttr e2] -}

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

-- resolves the first file path wrt to the second
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."

-- relativizes the first file path wrt to the second
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."

-- resolves the file path wrt to the current directory
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]
++ "/"

-- relativizes an absolute file path wrt to the current directory
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]
++ "/"

{- converts a filepath to a library name, i.e.
   relativizes w.r.t. the LATIN_HOME env variable -}
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]
++ "/"

{- converts a library name to a filepath, i.e.
   resolves w.r.t. the LATIN_HOME env variable -}
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]
++ "/"

{- returns the referenced base and module resolved w.r.t.
   the second argument -}
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."

{- retrieves the base, module, and name attributes resolved w.r.t.
   the second argument -}
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)

{- parses the referenced file if needed and imports all signatures
   and morphisms from it -}
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))

-- finds the signature by base and module
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."

-- finds the morphism by base, module, and name
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."

-- adds the signature to the signature collection
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)))

-- adds the morphism to the morphism collection
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)))

-- computes the correct targets of morphisms
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)

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING THE LIBRARY OF LF SIGNATURES AND MORPHISMS -}

-- analyzes the given Twelf file and returns LF signatures and morphisms
twelf2SigMor :: Namespace -> FilePath -> IO LIBS
twelf2SigMor :: 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

{- updates the graph libraries by adding specs from the Twelf file;
   the list of library names stores the order in which they were added,
   which is needed later for the construction of DGraphs -}
twelf2GR :: Namespace -> FilePath -> (LIBS, [BASE]) -> IO (LIBS, [BASE])
twelf2GR :: 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')

-- runs twelf to create an omdoc file
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 ()

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING SIGNATURES AND MORPHISMS -}

-- builds the LF signature and morphism graph
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."

-- transforms a theory element into a signature and adds it to the graph
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

-- transforms a view element into a view and adds it to the graph
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

-- constructs the view morphism
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)

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING CONSTANTS -}

-- adds a constant declaration to the signature
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)

{- converts a type element to an expression
   second argument is used for resolving symbol references -}
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."

{- converts a definition element to an expression
   second argument is used for resolving symbol references -}
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."

-- converts an OMOBJ element to an expression
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."

-- converts an Open Math element to an expression
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."

-- converts an OMS element 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

-- converts an OMA element to an expression
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

-- converts an OMBIND element to an expression
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
                 {- so far implicit binders are treated
                    as explicit -}
                   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."

-- converts an OMBVAR element to a list of declaration
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

-- converts an OMATTR element to a variable declaration
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."

-- converts an OMATP element to an expression
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."

-- converts an OMV element to an expression
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

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING INCLUSIONS -}

{- adds declarations arising from an inclusion to the signature
   adds the inclusion to the morphism map -}
addIncl :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addIncl :: 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)

-- adds included definitions to the signature
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

-- constructs the inclusion morphism
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

{- ----------------------------------------------------------------------------
----------------------------------------------------------------------------
CONSTRUCTING STRUCTURES -}

{- adds declarations arising from a structure to the signature
   adds the structure to the morphism map -}
addStruct :: Namespace -> Element -> (LIBS_EXT, Sign) -> IO (LIBS_EXT, Sign)
addStruct :: 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)

{- adds the definitions imported by a structure to the signature and
   constructs the structure morphism -}
processStruct :: Namespace -> String -> Sign -> Sign -> [Element] -> LIBS_EXT ->
                 IO (Sign, Morphism, LIBS_EXT)
processStruct :: 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)

  -- constructs the translation part of the structure
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

-- converts the constant assignment into a map
conass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
              NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
conass2map :: 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."

-- converts the included morphism into a map
incl2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
            NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
incl2map :: 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."

-- converts the structure assignment into a map
strass2map :: Namespace -> Element -> (Map.Map Symbol EXP, LIBS_EXT) ->
              NODE -> NODE -> IO (Map.Map Symbol EXP, LIBS_EXT)
strass2map :: 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."

-- converts an OMMOR element to a morphism
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."

-- converts an Open Math element to a morphism
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."

-- converts an OMS element 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

-- converts an OMA element to a morphism
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."

-- retrieves a morphism by the link name
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)

-- combines two morphisms according to the structure assignment
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