{-# LANGUAGE ExistentialQuantification #-}
{- |
Module      :  ./OMDoc/Import.hs
Description :  Transforms an OMDoc file into a development graph
Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Ewaryst.Schulz@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

Given an OMDoc file, a Library Environment is constructed from it by
following all library links.

The import requires the following interface functions to be instantiated
for each logic

Signature Category:
ide, cod

Sentences:
symmap_of

StaticAnalysis:
id_to_raw, symbol_to_raw, induced_from_morphism, induced_from_to_morphism
, signature_union, empty_signature, add_symb_to_sign

Logic:
omdoc_metatheory, omdocToSym, omdocToSen

These functions have default implementations which are sufficient
in many cases:
addOMadtToTheory, addOmdocToTheory


-}

module OMDoc.Import where

import Common.Result
import Common.ResultT
import Common.ExtSign
import Common.Id
import Common.IRI
import Common.LibName
import Common.Utils
import Common.XmlParser (readXmlFile)

import Driver.ReadFn (libNameToFile)
import Driver.Options (rmSuffix, HetcatsOpts, putIfVerbose, showDiags)

import Logic.Logic
    ( AnyLogic (Logic)
    , Logic ( omdoc_metatheory, omdocToSym, omdocToSen, addOMadtToTheory
           , addOmdocToTheory)
    , Category (ide, cod)
    , StaticAnalysis ( induced_from_morphism, induced_from_to_morphism
                    , signature_union, empty_signature, add_symb_to_sign
                    , symbol_to_raw, id_to_raw )
    , Sentences (symmap_of) )
import Logic.ExtSign
import Logic.Coerce
import Logic.Prover
import Logic.Grothendieck

import Comorphisms.LogicList
import Comorphisms.LogicGraph

import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.AnalysisStructured
import Static.ComputeTheory

import OMDoc.DataTypes
import OMDoc.XmlInterface (xmlIn)

import System.Directory

import Data.Graph.Inductive.Graph (LNode, Node)
import Data.Maybe
import Data.List
import qualified Data.Map as Map
import Control.Monad
import Control.Monad.Trans

-- * Import Environment Interface

{- | There are three important maps for each theory:
 1. OMName -> symbol, the NameSymbolMap stores for each OMDoc name the
                      translated hets symbol
 2. OMName -> String, the NameMap stores the notation information of the
                      OMDoc names, identity mappings are NOT stored here!
 3. SigMapI symbol, this signature map is just a container to store map 1 and 2
-}
type NameSymbolMap = G_mapofsymbol OMName

-- | The keys of libMap consist of the filepaths without suffix!
data ImpEnv =
    ImpEnv {
      ImpEnv -> Map FilePath (LibName, DGraph)
libMap :: Map.Map FilePath (LibName, DGraph)
    , ImpEnv -> Map (LibName, FilePath) NameSymbolMap
nsymbMap :: Map.Map (LibName, String) NameSymbolMap
    , ImpEnv -> HetcatsOpts
hetsOptions :: HetcatsOpts
    }

initialEnv :: HetcatsOpts -> ImpEnv
initialEnv :: HetcatsOpts -> ImpEnv
initialEnv opts :: HetcatsOpts
opts = ImpEnv :: Map FilePath (LibName, DGraph)
-> Map (LibName, FilePath) NameSymbolMap -> HetcatsOpts -> ImpEnv
ImpEnv { libMap :: Map FilePath (LibName, DGraph)
libMap = Map FilePath (LibName, DGraph)
forall k a. Map k a
Map.empty
                         , nsymbMap :: Map (LibName, FilePath) NameSymbolMap
nsymbMap = Map (LibName, FilePath) NameSymbolMap
forall k a. Map k a
Map.empty
                         , hetsOptions :: HetcatsOpts
hetsOptions = HetcatsOpts
opts }

getLibEnv :: ImpEnv -> LibEnv
getLibEnv :: ImpEnv -> LibEnv
getLibEnv e :: ImpEnv
e = LibEnv -> LibEnv
computeLibEnvTheories (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$
              [(LibName, DGraph)] -> LibEnv
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(LibName, DGraph)] -> LibEnv) -> [(LibName, DGraph)] -> LibEnv
forall a b. (a -> b) -> a -> b
$ Map FilePath (LibName, DGraph) -> [(LibName, DGraph)]
forall k a. Map k a -> [a]
Map.elems (Map FilePath (LibName, DGraph) -> [(LibName, DGraph)])
-> Map FilePath (LibName, DGraph) -> [(LibName, DGraph)]
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map FilePath (LibName, DGraph)
libMap ImpEnv
e

addDGToEnv :: ImpEnv -> LibName -> DGraph -> ImpEnv
addDGToEnv :: ImpEnv -> LibName -> DGraph -> ImpEnv
addDGToEnv e :: ImpEnv
e ln :: LibName
ln dg :: DGraph
dg =
    ImpEnv
e { libMap :: Map FilePath (LibName, DGraph)
libMap = FilePath
-> (LibName, DGraph)
-> Map FilePath (LibName, DGraph)
-> Map FilePath (LibName, DGraph)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName -> FilePath
libNameToFile LibName
ln) (LibName
ln, DGraph
dg) (Map FilePath (LibName, DGraph) -> Map FilePath (LibName, DGraph))
-> Map FilePath (LibName, DGraph) -> Map FilePath (LibName, DGraph)
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map FilePath (LibName, DGraph)
libMap ImpEnv
e }

addNSMapToEnv :: ImpEnv -> LibName -> String -> NameSymbolMap -> ImpEnv
addNSMapToEnv :: ImpEnv -> LibName -> FilePath -> NameSymbolMap -> ImpEnv
addNSMapToEnv e :: ImpEnv
e ln :: LibName
ln nm :: FilePath
nm nsm :: NameSymbolMap
nsm =
    ImpEnv
e { nsymbMap :: Map (LibName, FilePath) NameSymbolMap
nsymbMap = (LibName, FilePath)
-> NameSymbolMap
-> Map (LibName, FilePath) NameSymbolMap
-> Map (LibName, FilePath) NameSymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName
ln, FilePath
nm) NameSymbolMap
nsm (Map (LibName, FilePath) NameSymbolMap
 -> Map (LibName, FilePath) NameSymbolMap)
-> Map (LibName, FilePath) NameSymbolMap
-> Map (LibName, FilePath) NameSymbolMap
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map (LibName, FilePath) NameSymbolMap
nsymbMap ImpEnv
e }

lookupLib :: ImpEnv -> IRI -> Maybe (LibName, DGraph)
lookupLib :: ImpEnv -> IRI -> Maybe (LibName, DGraph)
lookupLib e :: ImpEnv
e u :: IRI
u = FilePath
-> Map FilePath (LibName, DGraph) -> Maybe (LibName, DGraph)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (FilePath -> FilePath
rmSuffix (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Id -> FilePath
forall a. Show a => a -> FilePath
show (Id -> FilePath) -> Id -> FilePath
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
u) (Map FilePath (LibName, DGraph) -> Maybe (LibName, DGraph))
-> Map FilePath (LibName, DGraph) -> Maybe (LibName, DGraph)
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map FilePath (LibName, DGraph)
libMap ImpEnv
e


lookupNode :: ImpEnv -> CurrentLib -> IriCD
           -> Maybe ( LibName -- the origin libname of the theory
                    , LNode DGNodeLab -- the (eventually reference) node
                    )
lookupNode :: ImpEnv
-> (LibName, DGraph) -> IriCD -> Maybe (LibName, LNode DGNodeLab)
lookupNode e :: ImpEnv
e (ln :: LibName
ln, dg :: DGraph
dg) ucd :: IriCD
ucd =
    let mn :: FilePath
mn = IriCD -> FilePath
getModule IriCD
ucd in
    if IriCD -> LibName -> Bool
cdInLib IriCD
ucd LibName
ln then
        case FilePath -> DGraph -> [LNode DGNodeLab]
filterLocalNodesByName FilePath
mn DGraph
dg of
          [] -> FilePath -> Maybe (LibName, LNode DGNodeLab)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Maybe (LibName, LNode DGNodeLab))
-> FilePath -> Maybe (LibName, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ "lookupNode: Node not found: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
mn
          lnode :: LNode DGNodeLab
lnode : _ -> (LibName, LNode DGNodeLab) -> Maybe (LibName, LNode DGNodeLab)
forall a. a -> Maybe a
Just (LibName
ln, LNode DGNodeLab
lnode)
    else case ImpEnv -> IRI -> Maybe (LibName, DGraph)
lookupLib ImpEnv
e (IRI -> Maybe (LibName, DGraph)) -> IRI -> Maybe (LibName, DGraph)
forall a b. (a -> b) -> a -> b
$ Maybe IRI -> IRI
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ IriCD -> Maybe IRI
getIri IriCD
ucd of
           Nothing -> Maybe (LibName, LNode DGNodeLab)
forall a. Maybe a
Nothing
           Just (ln' :: LibName
ln', dg' :: DGraph
dg') ->
               case FilePath -> LibName -> DGraph -> [LNode DGNodeLab]
filterRefNodesByName FilePath
mn LibName
ln' DGraph
dg of
                 lnode :: LNode DGNodeLab
lnode : _ -> (LibName, LNode DGNodeLab) -> Maybe (LibName, LNode DGNodeLab)
forall a. a -> Maybe a
Just (LibName
ln', LNode DGNodeLab
lnode)
                 [] -> [(LibName, LNode DGNodeLab)] -> Maybe (LibName, LNode DGNodeLab)
forall a. [a] -> Maybe a
listToMaybe
                   ([(LibName, LNode DGNodeLab)] -> Maybe (LibName, LNode DGNodeLab))
-> [(LibName, LNode DGNodeLab)] -> Maybe (LibName, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> (LibName, LNode DGNodeLab))
-> [LNode DGNodeLab] -> [(LibName, LNode DGNodeLab)]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: LNode DGNodeLab
n -> (LibName
ln', LNode DGNodeLab
n)) ([LNode DGNodeLab] -> [(LibName, LNode DGNodeLab)])
-> [LNode DGNodeLab] -> [(LibName, LNode DGNodeLab)]
forall a b. (a -> b) -> a -> b
$ FilePath -> DGraph -> [LNode DGNodeLab]
filterLocalNodesByName FilePath
mn DGraph
dg'

lookupNSMap :: ImpEnv -> LibName -> Maybe LibName -> String -> NameSymbolMap
lookupNSMap :: ImpEnv -> LibName -> Maybe LibName -> FilePath -> NameSymbolMap
lookupNSMap e :: ImpEnv
e ln :: LibName
ln mLn :: Maybe LibName
mLn nm :: FilePath
nm =
    let ln' :: LibName
ln' = LibName -> Maybe LibName -> LibName
forall a. a -> Maybe a -> a
fromMaybe LibName
ln Maybe LibName
mLn
        mf :: (LibName, FilePath) -> Map (LibName, FilePath) a -> a
mf = a -> (LibName, FilePath) -> Map (LibName, FilePath) a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
             (a -> (LibName, FilePath) -> Map (LibName, FilePath) a -> a)
-> a -> (LibName, FilePath) -> Map (LibName, FilePath) a -> a
forall a b. (a -> b) -> a -> b
$ FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "lookupNSMap: lookup failed for "
                              , (LibName, FilePath) -> FilePath
forall a. Show a => a -> FilePath
show (LibName
ln', FilePath
nm), "\n", Maybe LibName -> FilePath
forall a. Show a => a -> FilePath
show Maybe LibName
mLn, "\n"
                              , Map (LibName, FilePath) NameSymbolMap -> FilePath
forall a. Show a => a -> FilePath
show (Map (LibName, FilePath) NameSymbolMap -> FilePath)
-> Map (LibName, FilePath) NameSymbolMap -> FilePath
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map (LibName, FilePath) NameSymbolMap
nsymbMap ImpEnv
e ]
    in (LibName, FilePath)
-> Map (LibName, FilePath) NameSymbolMap -> NameSymbolMap
forall a. (LibName, FilePath) -> Map (LibName, FilePath) a -> a
mf (LibName
ln', FilePath
nm) (Map (LibName, FilePath) NameSymbolMap -> NameSymbolMap)
-> Map (LibName, FilePath) NameSymbolMap -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ ImpEnv -> Map (LibName, FilePath) NameSymbolMap
nsymbMap ImpEnv
e


rPutIfVerbose :: ImpEnv -> Int -> String -> ResultT IO ()
rPutIfVerbose :: ImpEnv -> Int -> FilePath -> ResultT IO ()
rPutIfVerbose e :: ImpEnv
e n :: Int
n s :: FilePath
s = IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose (ImpEnv -> HetcatsOpts
hetsOptions ImpEnv
e) Int
n FilePath
s

rPut :: ImpEnv -> String -> ResultT IO ()
rPut :: ImpEnv -> FilePath -> ResultT IO ()
rPut e :: ImpEnv
e = ImpEnv -> Int -> FilePath -> ResultT IO ()
rPutIfVerbose ImpEnv
e 1

rPut2 :: ImpEnv -> String -> ResultT IO ()
rPut2 :: ImpEnv -> FilePath -> ResultT IO ()
rPut2 e :: ImpEnv
e = ImpEnv -> Int -> FilePath -> ResultT IO ()
rPutIfVerbose ImpEnv
e 2

-- * IRI Functions

readFromURL :: (FilePath -> IO a) -> IRI -> IO a
readFromURL :: (FilePath -> IO a) -> IRI -> IO a
readFromURL f :: FilePath -> IO a
f u :: IRI
u = if IRI -> Bool
isFileIRI IRI
u then FilePath -> IO a
f (FilePath -> IO a) -> FilePath -> IO a
forall a b. (a -> b) -> a -> b
$ Id -> FilePath
forall a. Show a => a -> FilePath
show (Id -> FilePath) -> Id -> FilePath
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
u
                  else FilePath -> IO a
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO a) -> FilePath -> IO a
forall a b. (a -> b) -> a -> b
$ "readFromURL: Unsupported IRI-scheme "
                           FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
iriScheme IRI
u

toIRI :: String -> IRI
toIRI :: FilePath -> IRI
toIRI s :: FilePath
s = case FilePath -> Maybe IRI
parseIRIReference FilePath
s of
            Just u :: IRI
u -> IRI
u
            _ -> FilePath -> IRI
forall a. HasCallStack => FilePath -> a
error (FilePath -> IRI) -> FilePath -> IRI
forall a b. (a -> b) -> a -> b
$ "toIRI: can't parse as iri " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s

libNameFromURL :: String -> IRI -> LibName
libNameFromURL :: FilePath -> IRI -> LibName
libNameFromURL s :: FilePath
s u :: IRI
u = FilePath -> LibName -> LibName
setFilePath (Id -> FilePath
forall a. Show a => a -> FilePath
show (Id -> FilePath) -> Id -> FilePath
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
u) (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ FilePath -> LibName
emptyLibName FilePath
s

-- | Compute an absolute IRI for a supplied IRI relative to the given filepath.
resolveIRI :: IRI -> FilePath -> IRI
resolveIRI :: IRI -> FilePath -> IRI
resolveIRI u :: IRI
u fp :: FilePath
fp = IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> IRI
forall a. HasCallStack => FilePath -> a
error (FilePath -> IRI) -> FilePath -> IRI
forall a b. (a -> b) -> a -> b
$ "toIRI: can't resolve iri " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
u)
                  (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ IRI -> IRI -> Maybe IRI
relativeTo IRI
u (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> IRI
toIRI FilePath
fp

-- | Is the scheme of the iri empty or file?
isFileIRI :: IRI -> Bool
isFileIRI :: IRI -> Bool
isFileIRI u :: IRI
u = FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (IRI -> FilePath
iriScheme IRI
u) ["", "file:"]


type IriCD = (Maybe IRI, String)

showIriCD :: IriCD -> String
showIriCD :: IriCD -> FilePath
showIriCD (mIri :: Maybe IRI
mIri, s :: FilePath
s) = case Maybe IRI
mIri of
                        Just u :: IRI
u -> IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
u FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s
                        _ -> FilePath
s

getIri :: IriCD -> Maybe IRI
getIri :: IriCD -> Maybe IRI
getIri = IriCD -> Maybe IRI
forall a b. (a, b) -> a
fst

getModule :: IriCD -> String
getModule :: IriCD -> FilePath
getModule = IriCD -> FilePath
forall a b. (a, b) -> b
snd


-- | Compute an absolute IRI for a supplied CD relative to the given LibName
toIriCD :: OMCD -> LibName -> IriCD
toIriCD :: OMCD -> LibName -> IriCD
toIriCD cd :: OMCD
cd ln :: LibName
ln =
    let [base :: FilePath
base, m :: FilePath
m] = OMCD -> [FilePath]
cdToList OMCD
cd
        fp :: FilePath
fp = LibName -> FilePath
getFilePath LibName
ln
        mU :: Maybe IRI
mU = if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
base then Maybe IRI
forall a. Maybe a
Nothing
             else IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ IRI -> FilePath -> IRI
resolveIRI (FilePath -> IRI
toIRI FilePath
base) FilePath
fp
    in (Maybe IRI
mU, FilePath
m)

getLogicFromMeta :: Maybe OMCD -> AnyLogic
getLogicFromMeta :: Maybe OMCD -> AnyLogic
getLogicFromMeta mCD :: Maybe OMCD
mCD =
    let p :: AnyLogic -> Bool
p (Logic lid :: lid
lid) = case lid -> Maybe OMCD
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Maybe OMCD
omdoc_metatheory lid
lid of
                          Just cd' :: OMCD
cd' -> Maybe OMCD -> OMCD
forall a. HasCallStack => Maybe a -> a
fromJust Maybe OMCD
mCD OMCD -> OMCD -> Bool
forall a. Eq a => a -> a -> Bool
== OMCD
cd'
                          _ -> Bool
False
    in if Maybe OMCD -> Bool
forall a. Maybe a -> Bool
isNothing Maybe OMCD
mCD then AnyLogic
defaultLogic else
           case (AnyLogic -> Bool) -> [AnyLogic] -> Maybe AnyLogic
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find AnyLogic -> Bool
p [AnyLogic]
logicList of
             Just al :: AnyLogic
al -> AnyLogic
al
             _ -> AnyLogic
defaultLogic

cdInLib :: IriCD -> LibName -> Bool
cdInLib :: IriCD -> LibName -> Bool
cdInLib ucd :: IriCD
ucd ln :: LibName
ln = case IriCD -> Maybe IRI
getIri IriCD
ucd of
                   Nothing -> Bool
True
                   Just url :: IRI
url -> IRI -> Bool
isFileIRI IRI
url Bool -> Bool -> Bool
&& LibName -> FilePath
getFilePath LibName
ln FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== (Id -> FilePath
forall a. Show a => a -> FilePath
show (Id -> FilePath) -> Id -> FilePath
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
url)


-- * Main translation functions

-- | Translates an OMDoc file to a LibEnv
anaOMDocFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaOMDocFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaOMDocFile opts :: HetcatsOpts
opts fp :: FilePath
fp = do
  FilePath
dir <- IO FilePath
getCurrentDirectory
  HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Importing OMDoc file " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fp
  Result ds :: [Diagnosis]
ds mEnvLn :: Maybe (ImpEnv, LibName, DGraph)
mEnvLn <- ResultT IO (ImpEnv, LibName, DGraph)
-> IO (Result (ImpEnv, LibName, DGraph))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (ImpEnv, LibName, DGraph)
 -> IO (Result (ImpEnv, LibName, DGraph)))
-> ResultT IO (ImpEnv, LibName, DGraph)
-> IO (Result (ImpEnv, LibName, DGraph))
forall a b. (a -> b) -> a -> b
$ ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
importLib (HetcatsOpts -> ImpEnv
initialEnv HetcatsOpts
opts)
                      (IRI -> ResultT IO (ImpEnv, LibName, DGraph))
-> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
forall a b. (a -> b) -> a -> b
$ IRI -> FilePath -> IRI
resolveIRI (FilePath -> IRI
toIRI FilePath
fp) (FilePath -> IRI) -> FilePath -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath
dir FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/"
  HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
  Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ ((ImpEnv, LibName, DGraph) -> (LibName, LibEnv))
-> Maybe (ImpEnv, LibName, DGraph) -> Maybe (LibName, LibEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (env :: ImpEnv
env, ln :: LibName
ln, _) -> (LibName
ln, ImpEnv -> LibEnv
getLibEnv ImpEnv
env)) Maybe (ImpEnv, LibName, DGraph)
mEnvLn


-- * OMDoc traversal

{- | If the lib is not already in the environment, the OMDoc file and
the closure of its imports is added to the environment. -}
importLib :: ImpEnv -- ^ The import environment
          -> IRI -- ^ The url of the OMDoc file
          -> ResultT IO (ImpEnv, LibName, DGraph)
importLib :: ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
importLib e :: ImpEnv
e u :: IRI
u =
    case ImpEnv -> IRI -> Maybe (LibName, DGraph)
lookupLib ImpEnv
e IRI
u of
      Just (ln :: LibName
ln, dg :: DGraph
dg) -> (ImpEnv, LibName, DGraph) -> ResultT IO (ImpEnv, LibName, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e, LibName
ln, DGraph
dg)
      _ -> ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
readLib ImpEnv
e IRI
u

-- | The OMDoc file and the closure of its imports is added to the environment.
readLib :: ImpEnv -- ^ The import environment
        -> IRI -- ^ The url of the OMDoc file
        -> ResultT IO (ImpEnv, LibName, DGraph)
readLib :: ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
readLib e :: ImpEnv
e u :: IRI
u = do
  ImpEnv -> FilePath -> ResultT IO ()
rPut ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Downloading " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
u FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " ..."
  ByteString
xmlString <- IO ByteString -> ResultT IO ByteString
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO ByteString -> ResultT IO ByteString)
-> IO ByteString -> ResultT IO ByteString
forall a b. (a -> b) -> a -> b
$ (FilePath -> IO ByteString) -> IRI -> IO ByteString
forall a. (FilePath -> IO a) -> IRI -> IO a
readFromURL FilePath -> IO ByteString
readXmlFile IRI
u
  OMDoc n :: FilePath
n l :: [TLElement]
l <- IO (Result OMDoc) -> ResultT IO OMDoc
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result OMDoc) -> ResultT IO OMDoc)
-> IO (Result OMDoc) -> ResultT IO OMDoc
forall a b. (a -> b) -> a -> b
$ ByteString -> IO (Result OMDoc)
forall a. XmlParseable a => a -> IO (Result OMDoc)
xmlIn ByteString
xmlString
  {- the name of the omdoc is used as the libname, no relationship between the
  libname and the filepath! -}
  let ln :: LibName
ln = FilePath -> IRI -> LibName
libNameFromURL FilePath
n IRI
u
  ImpEnv -> FilePath -> ResultT IO ()
rPut ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Importing library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
ln
  (e' :: ImpEnv
e', dg :: DGraph
dg) <- ((ImpEnv, DGraph) -> TLElement -> ResultT IO (ImpEnv, DGraph))
-> (ImpEnv, DGraph) -> [TLElement] -> ResultT IO (ImpEnv, DGraph)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LibName
-> (ImpEnv, DGraph) -> TLElement -> ResultT IO (ImpEnv, DGraph)
addTLToDGraph LibName
ln) (ImpEnv
e, DGraph
emptyDG) [TLElement]
l
  ImpEnv -> FilePath -> ResultT IO ()
rPut ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "... loaded " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
u
  (ImpEnv, LibName, DGraph) -> ResultT IO (ImpEnv, LibName, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv -> LibName -> DGraph -> ImpEnv
addDGToEnv ImpEnv
e' LibName
ln DGraph
dg, LibName
ln, DGraph
dg)

-- | Adds the Theory in the OMCD and the containing lib to the environment
importTheory :: ImpEnv -- ^ The import environment
             -> CurrentLib -- ^ The current lib
             -> OMCD -- ^ The cd which points to the Theory
             -> ResultT IO ( ImpEnv -- the updated environment
                           , LibName -- the origin libname of the theory
                           , DGraph -- the updated devgraph of the current lib
                           , LNode DGNodeLab -- the corresponding node
                           )
importTheory :: ImpEnv
-> (LibName, DGraph)
-> OMCD
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
importTheory e :: ImpEnv
e (ln :: LibName
ln, dg :: DGraph
dg) cd :: OMCD
cd = do
  let ucd :: IriCD
ucd = OMCD -> LibName -> IriCD
toIriCD OMCD
cd LibName
ln
  ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Looking up theory " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IriCD -> FilePath
showIriCD IriCD
ucd FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " ..."
  case ImpEnv
-> (LibName, DGraph) -> IriCD -> Maybe (LibName, LNode DGNodeLab)
lookupNode ImpEnv
e (LibName
ln, DGraph
dg) IriCD
ucd of
    Just (ln' :: LibName
ln', nd :: LNode DGNodeLab
nd)
        | LibName
ln LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln' ->
            do
              ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e "... found local node."
              (ImpEnv, LibName, DGraph, LNode DGNodeLab)
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e, LibName
ln, DGraph
dg, LNode DGNodeLab
nd)
        | DGNodeLab -> Bool
isDGRef (DGNodeLab -> Bool) -> DGNodeLab -> Bool
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd LNode DGNodeLab
nd ->
            do
              ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e "... found already referenced node."
              (ImpEnv, LibName, DGraph, LNode DGNodeLab)
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e, LibName
ln', DGraph
dg, LNode DGNodeLab
nd)
        | Bool
otherwise ->
            do
              ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e "... found node, referencing it ..."
              let (lnode :: LNode DGNodeLab
lnode, dg' :: DGraph
dg') = LNode DGNodeLab -> LibName -> DGraph -> (LNode DGNodeLab, DGraph)
addNodeAsRefToDG LNode DGNodeLab
nd LibName
ln' DGraph
dg
              ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e "... done"
              (ImpEnv, LibName, DGraph, LNode DGNodeLab)
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e, LibName
ln', DGraph
dg', LNode DGNodeLab
lnode)
    -- if lookupNode finds nothing implies that ln is not the current libname!
    _ -> do
      let u :: IRI
u = Maybe IRI -> IRI
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ IriCD -> Maybe IRI
getIri IriCD
ucd
      ImpEnv -> FilePath -> ResultT IO ()
rPut2 ImpEnv
e "... node not found, reading lib."
      (e' :: ImpEnv
e', ln' :: LibName
ln', refDg :: DGraph
refDg) <- ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
readLib ImpEnv
e IRI
u
      case FilePath -> DGraph -> [LNode DGNodeLab]
filterLocalNodesByName (IriCD -> FilePath
getModule IriCD
ucd) DGraph
refDg of
        -- don't add the node to the refDG but to the original DG!
        nd :: LNode DGNodeLab
nd : _ -> let (lnode :: LNode DGNodeLab
lnode, dg' :: DGraph
dg') = LNode DGNodeLab -> LibName -> DGraph -> (LNode DGNodeLab, DGraph)
addNodeAsRefToDG LNode DGNodeLab
nd LibName
ln' DGraph
dg
                   in (ImpEnv, LibName, DGraph, LNode DGNodeLab)
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e', LibName
ln', DGraph
dg', LNode DGNodeLab
lnode)
        [] -> FilePath -> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall a. HasCallStack => FilePath -> a
error (FilePath -> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab))
-> FilePath
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
forall a b. (a -> b) -> a -> b
$ "importTheory: couldn't find node: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OMCD -> FilePath
forall a. Show a => a -> FilePath
show OMCD
cd


-- | Adds a view or theory to the DG, the ImpEnv may also be modified.
addTLToDGraph :: LibName -> (ImpEnv, DGraph) -> TLElement
              -> ResultT IO (ImpEnv, DGraph)
-- adding a theory to the DG
addTLToDGraph :: LibName
-> (ImpEnv, DGraph) -> TLElement -> ResultT IO (ImpEnv, DGraph)
addTLToDGraph ln :: LibName
ln (e :: ImpEnv
e, dg :: DGraph
dg) (TLTheory n :: FilePath
n mCD :: Maybe OMCD
mCD l :: [TCElement]
l) = do

  ImpEnv -> FilePath -> ResultT IO ()
rPut ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Importing theory " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
n

  let clf :: TCClassification
clf = [TCElement] -> TCClassification
classifyTCs [TCElement]
l

  {- I. Lookup all imports (= follow and create them first),
  and insert DGNodeRefs if neccessary. -}
  ((e' :: ImpEnv
e', dg' :: DGraph
dg'), iIL :: [ImportInfo LinkNode]
iIL) <- LibName
-> (ImpEnv, DGraph)
-> [ImportInfo OMCD]
-> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
followImports LibName
ln (ImpEnv
e, DGraph
dg) ([ImportInfo OMCD]
 -> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode]))
-> [ImportInfo OMCD]
-> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
forall a b. (a -> b) -> a -> b
$ TCClassification -> [ImportInfo OMCD]
importInfo TCClassification
clf

  -- II. Compute morphisms and update initial sig and name symbol map stepwise.
  ((nsmap :: NameSymbolMap
nsmap, gSig :: G_sign
gSig), iIWL :: [LinkInfo]
iIWL) <-
      ImpEnv
-> LibName
-> Map OMName FilePath
-> (NameSymbolMap, G_sign)
-> [ImportInfo LinkNode]
-> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])
computeMorphisms ImpEnv
e' LibName
ln (TCClassification -> Map OMName FilePath
notations TCClassification
clf)
                           (AnyLogic -> (NameSymbolMap, G_sign)
initialSig (AnyLogic -> (NameSymbolMap, G_sign))
-> AnyLogic -> (NameSymbolMap, G_sign)
forall a b. (a -> b) -> a -> b
$ Maybe OMCD -> AnyLogic
getLogicFromMeta Maybe OMCD
mCD) [ImportInfo LinkNode]
iIL

  -- III. Compute local signature
  (nsmap' :: NameSymbolMap
nsmap', gSig' :: G_sign
gSig') <- Result (NameSymbolMap, G_sign)
-> ResultT IO (NameSymbolMap, G_sign)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (NameSymbolMap, G_sign)
 -> ResultT IO (NameSymbolMap, G_sign))
-> Result (NameSymbolMap, G_sign)
-> ResultT IO (NameSymbolMap, G_sign)
forall a b. (a -> b) -> a -> b
$ TCClassification
-> NameSymbolMap -> G_sign -> Result (NameSymbolMap, G_sign)
localSig TCClassification
clf NameSymbolMap
nsmap G_sign
gSig

  -- IV. Add the sentences to the Node.
  G_theory
gThy <- Result G_theory -> ResultT IO G_theory
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_theory -> ResultT IO G_theory)
-> Result G_theory -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ TCClassification -> NameSymbolMap -> G_sign -> Result G_theory
addSentences TCClassification
clf NameSymbolMap
nsmap' G_sign
gSig'

  -- V. Complete the morphisms with final signature
  [LinkInfo]
iIWL' <- Result [LinkInfo] -> ResultT IO [LinkInfo]
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result [LinkInfo] -> ResultT IO [LinkInfo])
-> Result [LinkInfo] -> ResultT IO [LinkInfo]
forall a b. (a -> b) -> a -> b
$ G_sign -> [LinkInfo] -> Result [LinkInfo]
completeMorphisms (G_theory -> G_sign
signOf G_theory
gThy) [LinkInfo]
iIWL

  -- VI. Add the Node to the DGraph.
  let ((nd :: Int
nd, _), dg'' :: DGraph
dg'') = DGraph -> FilePath -> G_theory -> (LNode DGNodeLab, DGraph)
addNodeToDG DGraph
dg' FilePath
n G_theory
gThy
      -- VII. Create links from the morphisms.
      dg''' :: DGraph
dg''' = Int -> DGraph -> [LinkInfo] -> DGraph
addLinksToDG Int
nd DGraph
dg'' [LinkInfo]
iIWL'
      -- add the new name symbol map to the environment
      e'' :: ImpEnv
e'' = ImpEnv -> LibName -> FilePath -> NameSymbolMap -> ImpEnv
addNSMapToEnv ImpEnv
e' LibName
ln FilePath
n NameSymbolMap
nsmap'

  (ImpEnv, DGraph) -> ResultT IO (ImpEnv, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e'', DGraph
dg''')


addTLToDGraph ln :: LibName
ln (e :: ImpEnv
e, dg :: DGraph
dg) (TLView n :: FilePath
n from :: OMCD
from to :: OMCD
to mMor :: TCMorphism
mMor) = do

  ImpEnv -> FilePath -> ResultT IO ()
rPut ImpEnv
e (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Importing view " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
n

  {- follow the source and target of the view and insert DGNodeRefs
  if neccessary.
  use followTheory for from and to. -}
  ((e' :: ImpEnv
e', dg' :: DGraph
dg'), [lkNdFrom :: LinkNode
lkNdFrom, lkNdTo :: LinkNode
lkNdTo]) <- LibName
-> (ImpEnv, DGraph)
-> [OMCD]
-> ResultT IO ((ImpEnv, DGraph), [LinkNode])
followTheories LibName
ln (ImpEnv
e, DGraph
dg) [OMCD
from, OMCD
to]
  LinkInfo
lkInf <- ImpEnv
-> LibName
-> ImportInfo (LinkNode, LinkNode)
-> ResultT IO LinkInfo
computeViewMorphism ImpEnv
e' LibName
ln (ImportInfo (LinkNode, LinkNode) -> ResultT IO LinkInfo)
-> ImportInfo (LinkNode, LinkNode) -> ResultT IO LinkInfo
forall a b. (a -> b) -> a -> b
$ (LinkNode, LinkNode)
-> FilePath -> TCMorphism -> ImportInfo (LinkNode, LinkNode)
forall a. a -> FilePath -> TCMorphism -> ImportInfo a
ImportInfo (LinkNode
lkNdFrom, LinkNode
lkNdTo) FilePath
n TCMorphism
mMor
  let dg'' :: DGraph
dg'' = Int -> DGraph -> LinkInfo -> DGraph
addLinkToDG
             {- this error should never occur as the linkinfo contains
             a to-node.
             The error is used here as a "don't care element" of type Node -}
             (FilePath -> Int
forall a. HasCallStack => FilePath -> a
error "addTLToDGraph: TLView - Default node not available")
             DGraph
dg' LinkInfo
lkInf
  (ImpEnv, DGraph) -> ResultT IO (ImpEnv, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (ImpEnv
e', DGraph
dg'')


-- ** Utils to compute DGNodes from OMDoc Theories

{-
 the morphisms are incomplete because the target signature
 wasn't complete at the time of morphism computation.
 we complete the morphisms by composing them with signature inclusions
 to the complete target signature
-}
completeMorphisms :: G_sign -- ^ the complete target signature
                  -> [LinkInfo] -- ^ the incomplete morphisms
                  -> Result [LinkInfo]
completeMorphisms :: G_sign -> [LinkInfo] -> Result [LinkInfo]
completeMorphisms gsig :: G_sign
gsig = (LinkInfo -> Result LinkInfo) -> [LinkInfo] -> Result [LinkInfo]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR ((GMorphism -> Result GMorphism) -> LinkInfo -> Result LinkInfo
forall (m :: * -> *).
Monad m =>
(GMorphism -> m GMorphism) -> LinkInfo -> m LinkInfo
fmapLI ((GMorphism -> Result GMorphism) -> LinkInfo -> Result LinkInfo)
-> (GMorphism -> Result GMorphism) -> LinkInfo -> Result LinkInfo
forall a b. (a -> b) -> a -> b
$ GMorphism -> GMorphism -> Result GMorphism
completeMorphism (GMorphism -> GMorphism -> Result GMorphism)
-> GMorphism -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide G_sign
gsig)

completeMorphism :: GMorphism -- ^ the target signature id morphism
                 -> GMorphism -- ^ the incomplete morphism
                 -> Result GMorphism
completeMorphism :: GMorphism -> GMorphism -> Result GMorphism
completeMorphism idT :: GMorphism
idT gmorph :: GMorphism
gmorph = LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion LogicGraph
logicGraph GMorphism
gmorph GMorphism
idT


computeMorphisms :: ImpEnv -> LibName
                 -> Map.Map OMName String -- ^ Notations
                 -> (NameSymbolMap, G_sign)
                 -> [ImportInfo LinkNode]
                 -> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])
computeMorphisms :: ImpEnv
-> LibName
-> Map OMName FilePath
-> (NameSymbolMap, G_sign)
-> [ImportInfo LinkNode]
-> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])
computeMorphisms e :: ImpEnv
e ln :: LibName
ln nots :: Map OMName FilePath
nots = ((NameSymbolMap, G_sign)
 -> ImportInfo LinkNode
 -> ResultT IO ((NameSymbolMap, G_sign), LinkInfo))
-> (NameSymbolMap, G_sign)
-> [ImportInfo LinkNode]
-> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (ImpEnv
-> LibName
-> Map OMName FilePath
-> (NameSymbolMap, G_sign)
-> ImportInfo LinkNode
-> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)
computeMorphism ImpEnv
e LibName
ln Map OMName FilePath
nots)

{- | Computes the morphism for an import link and updates the signature
and the name symbol map with the imported symbols -}
computeMorphism :: ImpEnv -- ^ The import environment for lookup purposes
                -> LibName -- ^ Current libname
                -> Map.Map OMName String -- ^ Notations of target signature
                -> (NameSymbolMap, G_sign) {- ^ OMDoc symbol to Hets symbol map
                                           and target signature -}
                -> ImportInfo LinkNode -- ^ source label with OMDoc morphism
                -> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)
computeMorphism :: ImpEnv
-> LibName
-> Map OMName FilePath
-> (NameSymbolMap, G_sign)
-> ImportInfo LinkNode
-> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)
computeMorphism e :: ImpEnv
e ln :: LibName
ln nots :: Map OMName FilePath
nots (nsmap :: NameSymbolMap
nsmap, tGSig :: G_sign
tGSig) (ImportInfo (mLn :: Maybe LibName
mLn, (from :: Int
from, lbl :: DGNodeLab
lbl)) n :: FilePath
n morph :: TCMorphism
morph)
    = case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
        G_theory sLid :: lid
sLid _ (ExtSign sSig :: sign
sSig _) _ _ _ ->
            case G_sign
tGSig of
              G_sign tLid :: lid
tLid (ExtSign tSig :: sign
tSig _) sigId :: SigId
sigId ->
                  do
                    let sourceNSMap :: NameSymbolMap
sourceNSMap = ImpEnv -> LibName -> Maybe LibName -> FilePath -> NameSymbolMap
lookupNSMap ImpEnv
e LibName
ln Maybe LibName
mLn (FilePath -> NameSymbolMap) -> FilePath -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> FilePath
getDGNodeName DGNodeLab
lbl
                    {- 1. build the morphism
                    compute first the symbol-map -}
                    [(symbol, Either (OMName, raw_symbol) symbol)]
symMap <- Maybe (Map OMName FilePath)
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
Maybe (Map OMName FilePath)
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
computeSymbolMap (Map OMName FilePath -> Maybe (Map OMName FilePath)
forall a. a -> Maybe a
Just Map OMName FilePath
nots) NameSymbolMap
sourceNSMap NameSymbolMap
nsmap
                              TCMorphism
morph lid
tLid
                    let
                        f :: symbol -> raw_symbol
f = lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
tLid
                        g :: Either (a, p) symbol -> p
g (Left (_, rs :: p
rs)) = p
rs
                        g (Right s :: symbol
s) = lid -> symbol -> p
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
tLid symbol
s
                        rsMap :: Map raw_symbol raw_symbol
rsMap = [(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol)
-> [(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol
forall a b. (a -> b) -> a -> b
$ ((symbol, Either (OMName, raw_symbol) symbol)
 -> (raw_symbol, raw_symbol))
-> [(symbol, Either (OMName, raw_symbol) symbol)]
-> [(raw_symbol, raw_symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: symbol
x, y :: Either (OMName, raw_symbol) symbol
y) -> (symbol -> raw_symbol
f symbol
x, Either (OMName, raw_symbol) symbol -> raw_symbol
forall basic_spec sentence symb_items symb_map_items sign morphism
       symbol p a.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  p =>
Either (a, p) symbol -> p
g Either (OMName, raw_symbol) symbol
y) )
                                [(symbol, Either (OMName, raw_symbol) symbol)]
symMap
                    -- REMARK: Logic-homogeneous environment assumed
                    sign
sSig' <- lid -> lid -> FilePath -> sign -> ResultT IO sign
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> sign1 -> m sign2
coercePlainSign lid
sLid lid
tLid "computeMorphism" sign
sSig
                    morphism
mor <- Result morphism -> ResultT IO morphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result morphism -> ResultT IO morphism)
-> Result morphism -> ResultT IO morphism
forall a b. (a -> b) -> a -> b
$ lid -> Map raw_symbol raw_symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_morphism lid
tLid Map raw_symbol raw_symbol
rsMap sign
sSig'
                    {- 2. build the GMorphism and update the signature
                    and the name symbol map -}
                    sign
newSig <- Result sign -> ResultT IO sign
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result sign -> ResultT IO sign) -> Result sign -> ResultT IO sign
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union lid
tLid sign
tSig (sign -> Result sign) -> sign -> Result sign
forall a b. (a -> b) -> a -> b
$ morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
mor
                    let gMor :: GMorphism
gMor = G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
tLid morphism
mor
                        newGSig :: G_sign
newGSig = lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
tLid (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
tLid sign
newSig) SigId
sigId
                        {- function for filtering the raw symbols in the
                        nsmap update -}
                        h :: (a, Either (b, b) b) -> Maybe (a, b)
h (s :: a
s, Left (n' :: b
n', _)) = (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
s, b
n')
                        h (_, Right _) = Maybe (a, b)
forall a. Maybe a
Nothing
                        nsmap' :: NameSymbolMap
nsmap' = lid
-> morphism -> NameSymbolMap -> [(symbol, OMName)] -> NameSymbolMap
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> morphism -> NameSymbolMap -> [(symbol, OMName)] -> NameSymbolMap
updateSymbolMap lid
tLid morphism
mor NameSymbolMap
nsmap
                                 ([(symbol, OMName)] -> NameSymbolMap)
-> [(symbol, OMName)] -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ ((symbol, Either (OMName, raw_symbol) symbol)
 -> Maybe (symbol, OMName))
-> [(symbol, Either (OMName, raw_symbol) symbol)]
-> [(symbol, OMName)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (symbol, Either (OMName, raw_symbol) symbol)
-> Maybe (symbol, OMName)
forall a b b b. (a, Either (b, b) b) -> Maybe (a, b)
h [(symbol, Either (OMName, raw_symbol) symbol)]
symMap
                    ((NameSymbolMap, G_sign), LinkInfo)
-> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return ( (NameSymbolMap
nsmap', G_sign
newGSig)
                           , (GMorphism
gMor, DGLinkType
globalDef, FilePath -> DGLinkOrigin
mkLinkOrigin FilePath
n, Int
from, Maybe Int
forall a. Maybe a
Nothing))

-- | Computes the morphism for a view
computeViewMorphism :: ImpEnv -- ^ The import environment for lookup purposes
                    -> LibName -- ^ Current libname
                    -> ImportInfo (LinkNode, LinkNode)
                    -- ^ OMDoc morphism with source and target node
                    -> ResultT IO LinkInfo
computeViewMorphism :: ImpEnv
-> LibName
-> ImportInfo (LinkNode, LinkNode)
-> ResultT IO LinkInfo
computeViewMorphism e :: ImpEnv
e ln :: LibName
ln (ImportInfo ( (mSLn :: Maybe LibName
mSLn, (from :: Int
from, lblS :: DGNodeLab
lblS))
                                     , (mTLn :: Maybe LibName
mTLn, (to :: Int
to, lblT :: DGNodeLab
lblT))) n :: FilePath
n morph :: TCMorphism
morph)
    = case (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lblS, DGNodeLab -> G_theory
dgn_theory DGNodeLab
lblT) of
        (G_theory sLid :: lid
sLid _ eSSig :: ExtSign sign symbol
eSSig _ _ _, G_theory tLid :: lid
tLid _ eTSig :: ExtSign sign symbol
eTSig _ _ _) ->
            do
              let nsmapS :: NameSymbolMap
nsmapS = ImpEnv -> LibName -> Maybe LibName -> FilePath -> NameSymbolMap
lookupNSMap ImpEnv
e LibName
ln Maybe LibName
mSLn (FilePath -> NameSymbolMap) -> FilePath -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> FilePath
getDGNodeName DGNodeLab
lblS
                  nsmapT :: NameSymbolMap
nsmapT = ImpEnv -> LibName -> Maybe LibName -> FilePath -> NameSymbolMap
lookupNSMap ImpEnv
e LibName
ln Maybe LibName
mTLn (FilePath -> NameSymbolMap) -> FilePath -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> FilePath
getDGNodeName DGNodeLab
lblT
              {- 1. build the morphism
              compute first the symbol-map -}
              [(symbol, Either (OMName, raw_symbol) symbol)]
symMap <- Maybe (Map OMName FilePath)
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
Maybe (Map OMName FilePath)
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
computeSymbolMap Maybe (Map OMName FilePath)
forall a. Maybe a
Nothing NameSymbolMap
nsmapS NameSymbolMap
nsmapT TCMorphism
morph lid
tLid
              let f :: symbol -> raw_symbol
f = lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
tLid
                  {- this can't occur as we do not provide a notation map
                  to computeSymbolMap -}
                  g :: Either a symbol -> p
g (Left _) = FilePath -> p
forall a. HasCallStack => FilePath -> a
error "computeViewMorphism: impossible case"
                  g (Right s :: symbol
s) = lid -> symbol -> p
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
tLid symbol
s
                  rsMap :: Map raw_symbol raw_symbol
rsMap = [(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                          ([(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol)
-> [(raw_symbol, raw_symbol)] -> Map raw_symbol raw_symbol
forall a b. (a -> b) -> a -> b
$ ((symbol, Either (OMName, raw_symbol) symbol)
 -> (raw_symbol, raw_symbol))
-> [(symbol, Either (OMName, raw_symbol) symbol)]
-> [(raw_symbol, raw_symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: symbol
x, y :: Either (OMName, raw_symbol) symbol
y) -> (symbol -> raw_symbol
f symbol
x, Either (OMName, raw_symbol) symbol -> raw_symbol
forall basic_spec sentence symb_items symb_map_items sign morphism
       symbol p a.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  p =>
Either a symbol -> p
g Either (OMName, raw_symbol) symbol
y) ) [(symbol, Either (OMName, raw_symbol) symbol)]
symMap
              -- REMARK: Logic-homogeneous environment assumed
              ExtSign sign symbol
eSSig' <- lid
-> lid
-> FilePath
-> ExtSign sign symbol
-> ResultT IO (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
sLid lid
tLid "computeViewMorphism" ExtSign sign symbol
eSSig
              morphism
mor <- Result morphism -> ResultT IO morphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result morphism -> ResultT IO morphism)
-> Result morphism -> ResultT IO morphism
forall a b. (a -> b) -> a -> b
$ lid
-> Map raw_symbol raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
induced_from_to_morphism lid
tLid Map raw_symbol raw_symbol
rsMap ExtSign sign symbol
eSSig' ExtSign sign symbol
eTSig
              -- 2. build the GMorphism
              let gMor :: GMorphism
gMor = G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
tLid morphism
mor
              LinkInfo -> ResultT IO LinkInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism
gMor, DGLinkType
globalThm, FilePath -> DGLinkOrigin
mkLinkOrigin FilePath
n, Int
from, Int -> Maybe Int
forall a. a -> Maybe a
Just Int
to)


mkLinkOrigin :: String -> DGLinkOrigin
mkLinkOrigin :: FilePath -> DGLinkOrigin
mkLinkOrigin s :: FilePath
s = IRI -> DGLinkOrigin
DGLinkMorph (IRI -> DGLinkOrigin) -> IRI -> DGLinkOrigin
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
mkSimpleId FilePath
s

{- | For each entry (s, n) in l we enter the mapping (n, m(s))
to the name symbol map -}
updateSymbolMap :: forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
        lid -> morphism -- ^ a signature morphism m
            -> NameSymbolMap
            -> [(symbol, OMName)] -- ^ a list l of symbol to OMName mappings
            -> NameSymbolMap
updateSymbolMap :: lid
-> morphism -> NameSymbolMap -> [(symbol, OMName)] -> NameSymbolMap
updateSymbolMap lid :: lid
lid mor :: morphism
mor nsmap :: NameSymbolMap
nsmap l :: [(symbol, OMName)]
l =
    case NameSymbolMap
nsmap of
      G_mapofsymbol lid' :: lid
lid' sm :: Map OMName symbol
sm ->
          let f :: Map k a -> (a, k) -> Map k a
f nsm :: Map k a
nsm (s :: a
s, n :: k
n) = k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
n (a -> a
forall sentence sign a.
Sentences lid sentence sign morphism a =>
a -> a
g a
s) Map k a
nsm -- fold function
              g :: a -> a
g s :: a
s = a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                    (FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$ "updateSymbolMap: symbol not found " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
s)
                    a
s (Map a a -> a) -> Map a a -> a
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> Map a a
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid
lid morphism
mor
              sm' :: Map OMName symbol
sm' = lid -> lid -> Map OMName symbol -> Map OMName symbol
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
lid' lid
lid Map OMName symbol
sm
          in lid -> Map OMName symbol -> NameSymbolMap
forall a lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map a symbol -> G_mapofsymbol a
G_mapofsymbol lid
lid (Map OMName symbol -> NameSymbolMap)
-> Map OMName symbol -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ (Map OMName symbol -> (symbol, OMName) -> Map OMName symbol)
-> Map OMName symbol -> [(symbol, OMName)] -> Map OMName symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map OMName symbol -> (symbol, OMName) -> Map OMName symbol
forall sentence sign a k.
(Sentences lid sentence sign morphism a, Ord k) =>
Map k a -> (a, k) -> Map k a
f Map OMName symbol
sm' [(symbol, OMName)]
l

{- | Computes a symbol map for the given TCMorphism. The symbols are looked
   up in the provided maps. For each symbol not found in the target map we
   return a OMName, raw symbol pair in order to insert the missing entries
   in the target name symbol map later. If notations are not present, all
   lookup failures end up in errors.
-}
computeSymbolMap :: forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
        Maybe (Map.Map OMName String) -- ^ Notations for missing symbols in map
            -> NameSymbolMap -> NameSymbolMap -> TCMorphism -> lid
            -> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
computeSymbolMap :: Maybe (Map OMName FilePath)
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
computeSymbolMap mNots :: Maybe (Map OMName FilePath)
mNots nsmapS :: NameSymbolMap
nsmapS nsmapT :: NameSymbolMap
nsmapT morph :: TCMorphism
morph lid :: lid
lid =
  case (NameSymbolMap
nsmapS, NameSymbolMap
nsmapT) of
    (G_mapofsymbol sLid :: lid
sLid sm :: Map OMName symbol
sm, G_mapofsymbol tLid :: lid
tLid tm :: Map OMName symbol
tm) ->
        do
          -- REMARK: Logic-homogeneous environment assumed
          let sNSMap :: Map OMName symbol
sNSMap = lid -> lid -> Map OMName symbol -> Map OMName symbol
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
sLid lid
lid Map OMName symbol
sm
              tNSMap :: Map OMName symbol
tNSMap = lid -> lid -> Map OMName symbol -> Map OMName symbol
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
tLid lid
lid Map OMName symbol
tm
              mf :: FilePath -> k -> Map k a -> a
mf msg :: FilePath
msg = a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                       (a -> k -> Map k a -> a) -> a -> k -> Map k a -> a
forall a b. (a -> b) -> a -> b
$ FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$ "computeSymbolMap: lookup failed for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg
              -- function for notation lookup
              g :: OMName -> FilePath
g = Map OMName FilePath -> OMName -> FilePath
lookupNotationInMap
                  (Map OMName FilePath -> OMName -> FilePath)
-> Map OMName FilePath -> OMName -> FilePath
forall a b. (a -> b) -> a -> b
$ Map OMName FilePath
-> Maybe (Map OMName FilePath) -> Map OMName FilePath
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> Map OMName FilePath
forall a. HasCallStack => FilePath -> a
error "computeSymbolMap: no notations") Maybe (Map OMName FilePath)
mNots
              -- function for map
              f :: (OMName, Either FilePath OMElement)
-> (symbol, Either (OMName, b) symbol)
f (omn :: OMName
omn, omimg :: Either FilePath OMElement
omimg) =
                  let tSymName :: OMName
tSymName = case Either FilePath OMElement
omimg of
                                   Left s -> FilePath -> OMName
mkSimpleName FilePath
s
                                   Right (OMS qn) -> OMQualName -> OMName
unqualName OMQualName
qn
                                   _ -> FilePath -> OMName
forall a. HasCallStack => FilePath -> a
error (FilePath -> OMName) -> FilePath -> OMName
forall a b. (a -> b) -> a -> b
$ "computeSymbolMap: Nonsymbol "
                                        FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "element mapped"
                  in ( FilePath -> OMName -> Map OMName symbol -> symbol
forall k a. Ord k => FilePath -> k -> Map k a -> a
mf (OMName -> FilePath
forall a. Show a => a -> FilePath
show OMName
omn) OMName
omn Map OMName symbol
sNSMap
                     , case OMName -> Map OMName symbol -> Maybe symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OMName
tSymName Map OMName symbol
tNSMap of
                         Just ts :: symbol
ts -> symbol -> Either (OMName, b) symbol
forall a b. b -> Either a b
Right symbol
ts
                         _ -> (OMName, b) -> Either (OMName, b) symbol
forall a b. a -> Either a b
Left (OMName
tSymName, lid -> Id -> b
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Id -> raw_symbol
id_to_raw lid
lid (Id -> b) -> Id -> b
forall a b. (a -> b) -> a -> b
$ FilePath -> Id
nameToId
                                                (FilePath -> Id) -> FilePath -> Id
forall a b. (a -> b) -> a -> b
$ OMName -> FilePath
g OMName
tSymName))
          [(symbol, Either (OMName, raw_symbol) symbol)]
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(symbol, Either (OMName, raw_symbol) symbol)]
 -> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)])
-> [(symbol, Either (OMName, raw_symbol) symbol)]
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
forall a b. (a -> b) -> a -> b
$ ((OMName, Either FilePath OMElement)
 -> (symbol, Either (OMName, raw_symbol) symbol))
-> TCMorphism -> [(symbol, Either (OMName, raw_symbol) symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (OMName, Either FilePath OMElement)
-> (symbol, Either (OMName, raw_symbol) symbol)
forall basic_spec sentence symb_items symb_map_items sign morphism
       symbol b.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  b =>
(OMName, Either FilePath OMElement)
-> (symbol, Either (OMName, b) symbol)
f TCMorphism
morph


followImports :: LibName -> (ImpEnv, DGraph) -> [ImportInfo OMCD]
              -> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
followImports :: LibName
-> (ImpEnv, DGraph)
-> [ImportInfo OMCD]
-> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
followImports ln :: LibName
ln = (ImportInfo OMCD -> ImportInfo LinkNode -> ImportInfo LinkNode)
-> ((ImpEnv, DGraph)
    -> ImportInfo OMCD
    -> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode))
-> (ImpEnv, DGraph)
-> [ImportInfo OMCD]
-> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
forall (m :: * -> *) a b c acc.
Monad m =>
(a -> b -> c)
-> (acc -> a -> m (acc, b)) -> acc -> [a] -> m (acc, [c])
mapAccumLCM (((ImportInfo OMCD, ImportInfo LinkNode) -> ImportInfo LinkNode)
-> ImportInfo OMCD -> ImportInfo LinkNode -> ImportInfo LinkNode
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ImportInfo OMCD, ImportInfo LinkNode) -> ImportInfo LinkNode
forall a b. (a, b) -> b
snd) (LibName
-> (ImpEnv, DGraph)
-> ImportInfo OMCD
-> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)
followImport LibName
ln)

{- | Ensures that the theory for the given OMCD is available in the environment.
See also 'followTheory' -}
followImport :: LibName -> (ImpEnv, DGraph) -> ImportInfo OMCD
             -> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)
followImport :: LibName
-> (ImpEnv, DGraph)
-> ImportInfo OMCD
-> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)
followImport ln :: LibName
ln x :: (ImpEnv, DGraph)
x iInfo :: ImportInfo OMCD
iInfo = do
  (x' :: (ImpEnv, DGraph)
x', linknode :: LinkNode
linknode) <- LibName
-> (ImpEnv, DGraph)
-> OMCD
-> ResultT IO ((ImpEnv, DGraph), LinkNode)
followTheory LibName
ln (ImpEnv, DGraph)
x (OMCD -> ResultT IO ((ImpEnv, DGraph), LinkNode))
-> OMCD -> ResultT IO ((ImpEnv, DGraph), LinkNode)
forall a b. (a -> b) -> a -> b
$ ImportInfo OMCD -> OMCD
forall a. ImportInfo a -> a
iInfoVal ImportInfo OMCD
iInfo
  ((ImpEnv, DGraph), ImportInfo LinkNode)
-> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ImpEnv, DGraph)
x', (OMCD -> LinkNode) -> ImportInfo OMCD -> ImportInfo LinkNode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LinkNode -> OMCD -> LinkNode
forall a b. a -> b -> a
const LinkNode
linknode) ImportInfo OMCD
iInfo)


followTheories :: LibName -> (ImpEnv, DGraph) -> [OMCD]
               -> ResultT IO ((ImpEnv, DGraph), [LinkNode])
followTheories :: LibName
-> (ImpEnv, DGraph)
-> [OMCD]
-> ResultT IO ((ImpEnv, DGraph), [LinkNode])
followTheories ln :: LibName
ln = (OMCD -> LinkNode -> LinkNode)
-> ((ImpEnv, DGraph)
    -> OMCD -> ResultT IO ((ImpEnv, DGraph), LinkNode))
-> (ImpEnv, DGraph)
-> [OMCD]
-> ResultT IO ((ImpEnv, DGraph), [LinkNode])
forall (m :: * -> *) a b c acc.
Monad m =>
(a -> b -> c)
-> (acc -> a -> m (acc, b)) -> acc -> [a] -> m (acc, [c])
mapAccumLCM (((OMCD, LinkNode) -> LinkNode) -> OMCD -> LinkNode -> LinkNode
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (OMCD, LinkNode) -> LinkNode
forall a b. (a, b) -> b
snd) (LibName
-> (ImpEnv, DGraph)
-> OMCD
-> ResultT IO ((ImpEnv, DGraph), LinkNode)
followTheory LibName
ln)

{- | We lookup the theory referenced by the cd in the environment
and add it if neccessary to the environment. -}
followTheory :: LibName -> (ImpEnv, DGraph) -> OMCD
             -> ResultT IO ((ImpEnv, DGraph), LinkNode)
followTheory :: LibName
-> (ImpEnv, DGraph)
-> OMCD
-> ResultT IO ((ImpEnv, DGraph), LinkNode)
followTheory ln :: LibName
ln (e :: ImpEnv
e, dg :: DGraph
dg) cd :: OMCD
cd = do
  (e' :: ImpEnv
e', ln' :: LibName
ln', dg' :: DGraph
dg', lnode :: LNode DGNodeLab
lnode) <- ImpEnv
-> (LibName, DGraph)
-> OMCD
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
importTheory ImpEnv
e (LibName
ln, DGraph
dg) OMCD
cd
  let mLn :: Maybe LibName
mLn = if LibName
ln LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln' then Maybe LibName
forall a. Maybe a
Nothing else LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
ln'
  ((ImpEnv, DGraph), LinkNode)
-> ResultT IO ((ImpEnv, DGraph), LinkNode)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ImpEnv
e', DGraph
dg'), (Maybe LibName
mLn, LNode DGNodeLab
lnode))


-- * Development Graph and LibEnv interface


{- | returns a function compatible with mapAccumLM for TCElement processing.
Used in localSig. -}
sigmapAccumFun :: (Monad m, Show a) => (SigMapI a -> TCElement -> String -> m a)
               -> SigMapI a -> TCElement -> m (SigMapI a, a)
sigmapAccumFun :: (SigMapI a -> TCElement -> FilePath -> m a)
-> SigMapI a -> TCElement -> m (SigMapI a, a)
sigmapAccumFun f :: SigMapI a -> TCElement -> FilePath -> m a
f smi :: SigMapI a
smi s :: TCElement
s = do
  let n :: OMName
n = TCElement -> OMName
tcName TCElement
s
      hetsname :: FilePath
hetsname = SigMapI a -> OMName -> FilePath
forall a. SigMapI a -> OMName -> FilePath
lookupNotation SigMapI a
smi OMName
n
  a
s' <- SigMapI a -> TCElement -> FilePath -> m a
f SigMapI a
smi TCElement
s FilePath
hetsname
  let smi' :: SigMapI a
smi' = SigMapI a
smi { sigMapISymbs :: Map OMName a
sigMapISymbs = OMName -> a -> Map OMName a -> Map OMName a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert OMName
n a
s' (Map OMName a -> Map OMName a) -> Map OMName a -> Map OMName a
forall a b. (a -> b) -> a -> b
$ SigMapI a -> Map OMName a
forall a. SigMapI a -> Map OMName a
sigMapISymbs SigMapI a
smi }
  (SigMapI a, a) -> m (SigMapI a, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SigMapI a
smi', a
s')


-- | Builds an initial signature and a name map of the given logic.
initialSig :: AnyLogic -> (NameSymbolMap, G_sign)
initialSig :: AnyLogic -> (NameSymbolMap, G_sign)
initialSig lg :: AnyLogic
lg =
    case AnyLogic
lg of
      Logic lid :: lid
lid ->
          ( lid -> Map OMName symbol -> NameSymbolMap
forall a lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map a symbol -> G_mapofsymbol a
G_mapofsymbol lid
lid Map OMName symbol
forall k a. Map k a
Map.empty
          , lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
lid (sign -> ExtSign sign symbol) -> sign -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid) SigId
startSigId)

-- | Adds the local signature to the given signature and name symbol map
localSig :: TCClassification -> NameSymbolMap -> G_sign
         -> Result (NameSymbolMap, G_sign)
localSig :: TCClassification
-> NameSymbolMap -> G_sign -> Result (NameSymbolMap, G_sign)
localSig clf :: TCClassification
clf nsmap :: NameSymbolMap
nsmap gSig :: G_sign
gSig =
    case (G_sign
gSig, NameSymbolMap
nsmap) of
      (G_sign lid :: lid
lid _ _, G_mapofsymbol lid' :: lid
lid' sm :: Map OMName symbol
sm) ->
          do
            let smi :: SigMapI symbol
smi = Map OMName symbol -> Map OMName FilePath -> SigMapI symbol
forall a. Map OMName a -> Map OMName FilePath -> SigMapI a
SigMapI (lid -> lid -> Map OMName symbol -> Map OMName symbol
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
lid' lid
lid Map OMName symbol
sm) (Map OMName FilePath -> SigMapI symbol)
-> Map OMName FilePath -> SigMapI symbol
forall a b. (a -> b) -> a -> b
$ TCClassification -> Map OMName FilePath
notations TCClassification
clf
            {- accumulates symbol mappings in the symbMap in SigMapI
            while creating symbols from OMDoc symbols -}
            (sm' :: SigMapI symbol
sm', symbs :: [symbol]
symbs) <- (SigMapI symbol -> TCElement -> Result (SigMapI symbol, symbol))
-> SigMapI symbol
-> [TCElement]
-> Result (SigMapI symbol, [symbol])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM ((SigMapI symbol -> TCElement -> FilePath -> Result symbol)
-> SigMapI symbol -> TCElement -> Result (SigMapI symbol, symbol)
forall (m :: * -> *) a.
(Monad m, Show a) =>
(SigMapI a -> TCElement -> FilePath -> m a)
-> SigMapI a -> TCElement -> m (SigMapI a, a)
sigmapAccumFun ((SigMapI symbol -> TCElement -> FilePath -> Result symbol)
 -> SigMapI symbol -> TCElement -> Result (SigMapI symbol, symbol))
-> (SigMapI symbol -> TCElement -> FilePath -> Result symbol)
-> SigMapI symbol
-> TCElement
-> Result (SigMapI symbol, symbol)
forall a b. (a -> b) -> a -> b
$ lid -> SigMapI symbol -> TCElement -> FilePath -> Result symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> SigMapI symbol -> TCElement -> FilePath -> Result symbol
omdocToSym lid
lid) SigMapI symbol
smi
                           ([TCElement] -> Result (SigMapI symbol, [symbol]))
-> [TCElement] -> Result (SigMapI symbol, [symbol])
forall a b. (a -> b) -> a -> b
$ TCClassification -> [TCElement]
sigElems TCClassification
clf
            -- adding the symbols to the empty signature
            sign
sig <- (sign -> symbol -> Result sign) -> sign -> [symbol] -> Result sign
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (lid -> sign -> symbol -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> symbol -> Result sign
add_symb_to_sign lid
lid) (lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid) [symbol]
symbs
            let locGSig :: G_sign
locGSig = lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
lid sign
sig) SigId
startSigId
            -- combining the local and the given signature
            G_sign
gSig' <- LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion LogicGraph
logicGraph Bool
True G_sign
gSig G_sign
locGSig
            (NameSymbolMap, G_sign) -> Result (NameSymbolMap, G_sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> Map OMName symbol -> NameSymbolMap
forall a lid sublogics basic_spec sentence symb_items
       symb_map_items sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map a symbol -> G_mapofsymbol a
G_mapofsymbol lid
lid (Map OMName symbol -> NameSymbolMap)
-> Map OMName symbol -> NameSymbolMap
forall a b. (a -> b) -> a -> b
$ SigMapI symbol -> Map OMName symbol
forall a. SigMapI a -> Map OMName a
sigMapISymbs SigMapI symbol
sm', G_sign
gSig')


-- | Adds sentences and logic dependent signature elements to the given sig
addSentences :: TCClassification -> NameSymbolMap -> G_sign -> Result G_theory
addSentences :: TCClassification -> NameSymbolMap -> G_sign -> Result G_theory
addSentences clf :: TCClassification
clf nsmap :: NameSymbolMap
nsmap gsig :: G_sign
gsig =
    case (NameSymbolMap
nsmap, G_sign
gsig) of
      (G_mapofsymbol lidM :: lid
lidM sm :: Map OMName symbol
sm, G_sign lid :: lid
lid (ExtSign sig :: sign
sig _) ind1 :: SigId
ind1) ->
          do
            let sigm :: SigMapI symbol
sigm = Map OMName symbol -> Map OMName FilePath -> SigMapI symbol
forall a. Map OMName a -> Map OMName FilePath -> SigMapI a
SigMapI (lid -> lid -> Map OMName symbol -> Map OMName symbol
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
lidM lid
lid Map OMName symbol
sm)
                    (Map OMName FilePath -> SigMapI symbol)
-> Map OMName FilePath -> SigMapI symbol
forall a b. (a -> b) -> a -> b
$ TCClassification -> Map OMName FilePath
notations TCClassification
clf
            -- 1. translate sentences
            [Maybe (Named sentence)]
mSens <- (TCElement -> Result (Maybe (Named sentence)))
-> [TCElement] -> Result [Maybe (Named sentence)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ tc :: TCElement
tc -> lid
-> SigMapI symbol
-> TCElement
-> FilePath
-> Result (Maybe (Named sentence))
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SigMapI symbol
-> TCElement
-> FilePath
-> Result (Maybe (Named sentence))
omdocToSen lid
lid SigMapI symbol
sigm TCElement
tc
                       (FilePath -> Result (Maybe (Named sentence)))
-> FilePath -> Result (Maybe (Named sentence))
forall a b. (a -> b) -> a -> b
$ SigMapI symbol -> OMName -> FilePath
forall a. SigMapI a -> OMName -> FilePath
lookupNotation SigMapI symbol
sigm (OMName -> FilePath) -> OMName -> FilePath
forall a b. (a -> b) -> a -> b
$ TCElement -> OMName
tcName TCElement
tc) ([TCElement] -> Result [Maybe (Named sentence)])
-> [TCElement] -> Result [Maybe (Named sentence)]
forall a b. (a -> b) -> a -> b
$ TCClassification -> [TCElement]
sentences TCClassification
clf

            -- 2. translate adts
            (sig' :: sign
sig', sens' :: [Named sentence]
sens') <- lid
-> SigMapI symbol
-> (sign, [Named sentence])
-> [[OmdADT]]
-> Result (sign, [Named sentence])
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SigMapI symbol
-> (sign, [Named sentence])
-> [[OmdADT]]
-> Result (sign, [Named sentence])
addOMadtToTheory lid
lid SigMapI symbol
sigm (sign
sig, [Maybe (Named sentence)] -> [Named sentence]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Named sentence)]
mSens)
                             ([[OmdADT]] -> Result (sign, [Named sentence]))
-> [[OmdADT]] -> Result (sign, [Named sentence])
forall a b. (a -> b) -> a -> b
$ TCClassification -> [[OmdADT]]
adts TCClassification
clf

            {- 3. translate rest of theory
            (all the sentences or just those which returned Nothing?) -}
            (sig'' :: sign
sig'', sens'' :: [Named sentence]
sens'') <- lid
-> SigMapI symbol
-> (sign, [Named sentence])
-> [TCElement]
-> Result (sign, [Named sentence])
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SigMapI symbol
-> (sign, [Named sentence])
-> [TCElement]
-> Result (sign, [Named sentence])
addOmdocToTheory lid
lid SigMapI symbol
sigm (sign
sig', [Named sentence]
sens')
                               ([TCElement] -> Result (sign, [Named sentence]))
-> [TCElement] -> Result (sign, [Named sentence])
forall a b. (a -> b) -> a -> b
$ TCClassification -> [TCElement]
sentences TCClassification
clf

            G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
forall a. Maybe a
Nothing (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig'') SigId
ind1
                       ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
sens'') ThId
startThId


-- | Adds Edges from the LinkInfo list to the development graph.
addLinksToDG :: Node -> DGraph -> [LinkInfo] -> DGraph
addLinksToDG :: Int -> DGraph -> [LinkInfo] -> DGraph
addLinksToDG nd :: Int
nd = (DGraph -> LinkInfo -> DGraph) -> DGraph -> [LinkInfo] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Int -> DGraph -> LinkInfo -> DGraph
addLinkToDG Int
nd)

-- | Adds Edge from the LinkInfo to the development graph.
addLinkToDG :: Node -> DGraph -> LinkInfo -> DGraph
addLinkToDG :: Int -> DGraph -> LinkInfo -> DGraph
addLinkToDG to :: Int
to dg :: DGraph
dg (gMor :: GMorphism
gMor, lt :: DGLinkType
lt, lo :: DGLinkOrigin
lo, from :: Int
from, mTo :: Maybe Int
mTo) =
    DGraph
-> GMorphism -> DGLinkType -> DGLinkOrigin -> Int -> Int -> DGraph
insLink DGraph
dg GMorphism
gMor DGLinkType
lt DGLinkOrigin
lo Int
from (Int -> DGraph) -> Int -> DGraph
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
to Maybe Int
mTo


-- | Adds a Node from the given 'G_theory' to the development graph.
addNodeToDG :: DGraph -> String -> G_theory -> (LNode DGNodeLab, DGraph)
addNodeToDG :: DGraph -> FilePath -> G_theory -> (LNode DGNodeLab, DGraph)
addNodeToDG dg :: DGraph
dg n :: FilePath
n gth :: G_theory
gth =
    let nd :: Int
nd = DGraph -> Int
getNewNodeDG DGraph
dg
        ndName :: NodeName
ndName = FilePath -> NodeName
parseNodeName FilePath
n
        ndInfo :: DGNodeInfo
ndInfo = DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGBasic
        newNode :: LNode DGNodeLab
newNode = (Int
nd, NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
ndName DGNodeInfo
ndInfo G_theory
gth)
    in (LNode DGNodeLab
newNode, LNode DGNodeLab -> DGraph -> DGraph
insNodeDG LNode DGNodeLab
newNode DGraph
dg)


addNodeAsRefToDG :: LNode DGNodeLab -> LibName -> DGraph
                 -> (LNode DGNodeLab, DGraph)
addNodeAsRefToDG :: LNode DGNodeLab -> LibName -> DGraph -> (LNode DGNodeLab, DGraph)
addNodeAsRefToDG (nd :: Int
nd, lbl :: DGNodeLab
lbl) ln :: LibName
ln dg :: DGraph
dg =
    let info :: DGNodeInfo
info = LibName -> Int -> DGNodeInfo
newRefInfo LibName
ln Int
nd
        refNodeM :: Maybe Int
refNodeM = DGNodeInfo -> DGraph -> Maybe Int
lookupInAllRefNodesDG DGNodeInfo
info DGraph
dg
        nd' :: Int
nd' = DGraph -> Int
getNewNodeDG DGraph
dg
        lnode :: LNode DGNodeLab
lnode = (Int
nd', DGNodeLab
lbl { nodeInfo :: DGNodeInfo
nodeInfo = DGNodeInfo
info })
        dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG LNode DGNodeLab
lnode DGraph
dg
     in case Maybe Int
refNodeM of
         Just refNode :: Int
refNode -> ((Int
refNode, DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
refNode), DGraph
dg)
         _ -> (LNode DGNodeLab
lnode, DGraph
dg1)


-- * Theory-utils

type CurrentLib = (LibName, DGraph)

type LinkNode = (Maybe LibName, LNode DGNodeLab)

type LinkInfo = (GMorphism, DGLinkType, DGLinkOrigin, Node, Maybe Node)

data ImportInfo a = ImportInfo a String TCMorphism deriving Int -> ImportInfo a -> FilePath -> FilePath
[ImportInfo a] -> FilePath -> FilePath
ImportInfo a -> FilePath
(Int -> ImportInfo a -> FilePath -> FilePath)
-> (ImportInfo a -> FilePath)
-> ([ImportInfo a] -> FilePath -> FilePath)
-> Show (ImportInfo a)
forall a. Show a => Int -> ImportInfo a -> FilePath -> FilePath
forall a. Show a => [ImportInfo a] -> FilePath -> FilePath
forall a. Show a => ImportInfo a -> FilePath
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [ImportInfo a] -> FilePath -> FilePath
$cshowList :: forall a. Show a => [ImportInfo a] -> FilePath -> FilePath
show :: ImportInfo a -> FilePath
$cshow :: forall a. Show a => ImportInfo a -> FilePath
showsPrec :: Int -> ImportInfo a -> FilePath -> FilePath
$cshowsPrec :: forall a. Show a => Int -> ImportInfo a -> FilePath -> FilePath
Show

iInfoVal :: ImportInfo a -> a
iInfoVal :: ImportInfo a -> a
iInfoVal (ImportInfo x :: a
x _ _) = a
x

instance Functor ImportInfo where
  fmap :: (a -> b) -> ImportInfo a -> ImportInfo b
fmap f :: a -> b
f (ImportInfo x :: a
x y :: FilePath
y z :: TCMorphism
z) = b -> FilePath -> TCMorphism -> ImportInfo b
forall a. a -> FilePath -> TCMorphism -> ImportInfo a
ImportInfo (a -> b
f a
x) FilePath
y TCMorphism
z

fmapLI :: Monad m => (GMorphism -> m GMorphism) -> LinkInfo -> m LinkInfo
fmapLI :: (GMorphism -> m GMorphism) -> LinkInfo -> m LinkInfo
fmapLI f :: GMorphism -> m GMorphism
f (gm :: GMorphism
gm, x :: DGLinkType
x, y :: DGLinkOrigin
y, z :: Int
z, t :: Maybe Int
t) = do
  GMorphism
gm' <- GMorphism -> m GMorphism
f GMorphism
gm
  LinkInfo -> m LinkInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism
gm', DGLinkType
x, DGLinkOrigin
y, Int
z, Maybe Int
t)

data TCClassification = TCClf {
      TCClassification -> [ImportInfo OMCD]
importInfo :: [ImportInfo OMCD] -- ^ Import-info
    , TCClassification -> [TCElement]
sigElems :: [TCElement] -- ^ Signature symbols
    , TCClassification -> [TCElement]
sentences :: [TCElement] -- ^ Theory sentences
    , TCClassification -> [[OmdADT]]
adts :: [[OmdADT]] -- ^ ADTs
    , TCClassification -> Map OMName FilePath
notations :: Map.Map OMName String -- ^ Notations
    }


emptyClassification :: TCClassification
emptyClassification :: TCClassification
emptyClassification = [ImportInfo OMCD]
-> [TCElement]
-> [TCElement]
-> [[OmdADT]]
-> Map OMName FilePath
-> TCClassification
TCClf [] [] [] [] Map OMName FilePath
forall k a. Map k a
Map.empty

classifyTCs :: [TCElement] -> TCClassification
classifyTCs :: [TCElement] -> TCClassification
classifyTCs = (TCElement -> TCClassification -> TCClassification)
-> TCClassification -> [TCElement] -> TCClassification
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TCElement -> TCClassification -> TCClassification
classifyTC TCClassification
emptyClassification

classifyTC :: TCElement -> TCClassification -> TCClassification
classifyTC :: TCElement -> TCClassification -> TCClassification
classifyTC tc :: TCElement
tc clf :: TCClassification
clf =
    case TCElement
tc of
      TCSymbol _ _ sr :: SymbolRole
sr _
          | SymbolRole -> [SymbolRole] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SymbolRole
sr [SymbolRole
Obj, SymbolRole
Typ] -> TCClassification
clf { sigElems :: [TCElement]
sigElems = TCElement
tc TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
: TCClassification -> [TCElement]
sigElems TCClassification
clf }
          | Bool
otherwise -> TCClassification
clf { sentences :: [TCElement]
sentences = TCElement
tc TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
: TCClassification -> [TCElement]
sentences TCClassification
clf }
      TCNotation (cd :: OMCD
cd, omn :: OMName
omn) n :: FilePath
n (Just "hets") ->
          if OMCD -> Bool
cdIsEmpty OMCD
cd then
              TCClassification
clf { notations :: Map OMName FilePath
notations = OMName -> FilePath -> Map OMName FilePath -> Map OMName FilePath
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert OMName
omn FilePath
n (Map OMName FilePath -> Map OMName FilePath)
-> Map OMName FilePath -> Map OMName FilePath
forall a b. (a -> b) -> a -> b
$ TCClassification -> Map OMName FilePath
notations TCClassification
clf }
          else TCClassification
clf
      TCADT l :: [OmdADT]
l -> TCClassification
clf { adts :: [[OmdADT]]
adts = [OmdADT]
l [OmdADT] -> [[OmdADT]] -> [[OmdADT]]
forall a. a -> [a] -> [a]
: TCClassification -> [[OmdADT]]
adts TCClassification
clf }
      TCImport n :: FilePath
n from :: OMCD
from morph :: TCMorphism
morph ->
          TCClassification
clf { importInfo :: [ImportInfo OMCD]
importInfo = OMCD -> FilePath -> TCMorphism -> ImportInfo OMCD
forall a. a -> FilePath -> TCMorphism -> ImportInfo a
ImportInfo OMCD
from FilePath
n TCMorphism
morph ImportInfo OMCD -> [ImportInfo OMCD] -> [ImportInfo OMCD]
forall a. a -> [a] -> [a]
: TCClassification -> [ImportInfo OMCD]
importInfo TCClassification
clf }
      TCComment _ -> TCClassification
clf
      TCSmartNotation {} -> FilePath -> TCClassification
forall a. HasCallStack => FilePath -> a
error "classifyTC: unexpected SmartNotation"
      TCFlexibleNotation {} ->
          FilePath -> TCClassification
forall a. HasCallStack => FilePath -> a
error "classifyTC: unexpected FlexibleNotation"
      -- just for the case TCNotation with a style different from hets
      _ -> TCClassification
clf