{- |
Module      :  ./Static/FromXml.hs
Description :  xml input for Hets development graphs
Copyright   :  (c) Simon Ulbricht, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (DevGraph)

create new or extend a Development Graph in accordance with an XML input
-}

module Static.FromXml where

import Static.ComputeTheory (computeLibEnvTheories)
import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.FromXmlUtils
import Static.XGraph

import Common.LibName
import Common.Result (Result (..))
import Common.ResultT
import Common.XmlParser

import Comorphisms.LogicGraph (logicGraph)

import Control.Monad.Trans (lift)
import Control.Monad (foldM, unless)
import qualified Control.Monad.Fail as Fail

import qualified Data.Graph.Inductive.Graph as Graph (Node)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Driver.Options
import Driver.ReadFn (findFileOfLibNameAux)

import Logic.ExtSign (ext_empty_signature)
import Logic.Grothendieck
import Logic.Logic (AnyLogic (..), cod, composeMorphisms)
import Logic.Prover (noSens)

import Text.XML.Light (Element)

-- | top-level function
readDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
readDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
readDGXml opts :: HetcatsOpts
opts path :: FilePath
path = do
    Result ds :: [Diagnosis]
ds res :: Maybe (LibName, LibEnv)
res <- ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
readDGXmlR HetcatsOpts
opts FilePath
path LibEnv
forall k a. Map k a
Map.empty
    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)
res

{- | main function; receives a FilePath and calls fromXml upon that path,
using an initial LogicGraph. -}
readDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
readDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
readDGXmlR opts :: HetcatsOpts
opts path :: FilePath
path lv :: LibEnv
lv = do
  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 HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Reading " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path
  ByteString
xml' <- 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
readXmlFile FilePath
path
  Either FilePath Element
res <- IO (Either FilePath Element)
-> ResultT IO (Either FilePath Element)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Either FilePath Element)
 -> ResultT IO (Either FilePath Element))
-> IO (Either FilePath Element)
-> ResultT IO (Either FilePath Element)
forall a b. (a -> b) -> a -> b
$ ByteString -> IO (Either FilePath Element)
forall a. XmlParseable a => a -> IO (Either FilePath Element)
parseXml ByteString
xml'
  case Either FilePath Element
res of
    Right xml :: Element
xml -> HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)
rebuiltDgXml HetcatsOpts
opts LibEnv
lv Element
xml
    Left err :: FilePath
err -> FilePath -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO (LibName, LibEnv))
-> FilePath -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ "failed to parse XML file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
err

-- | call rebuiltDG with only a LibEnv and an Xml-Element
rebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)
rebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)
rebuiltDgXml opts :: HetcatsOpts
opts lv :: LibEnv
lv xml :: Element
xml = do
      XGraph
xg <- Result XGraph -> ResultT IO XGraph
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result XGraph -> ResultT IO XGraph)
-> Result XGraph -> ResultT IO XGraph
forall a b. (a -> b) -> a -> b
$ Element -> Result XGraph
xGraph Element
xml
      (DGraph, LibEnv)
res <- HetcatsOpts
-> LogicGraph -> XGraph -> LibEnv -> ResultT IO (DGraph, LibEnv)
rebuiltDG HetcatsOpts
opts LogicGraph
logicGraph XGraph
xg LibEnv
lv
      let ln :: LibName
ln = XGraph -> LibName
libName XGraph
xg
      (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln, LibEnv -> LibEnv
computeLibEnvTheories (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ (DGraph -> LibEnv -> LibEnv) -> (DGraph, LibEnv) -> LibEnv
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln) (DGraph, LibEnv)
res)

{- | reconstructs the Development Graph via a previously created XGraph-
structure. -}
rebuiltDG :: HetcatsOpts -> LogicGraph -> XGraph -> LibEnv
          -> ResultT IO (DGraph, LibEnv)
rebuiltDG :: HetcatsOpts
-> LogicGraph -> XGraph -> LibEnv -> ResultT IO (DGraph, LibEnv)
rebuiltDG opts :: HetcatsOpts
opts lg :: LogicGraph
lg (XGraph _ ga :: GlobalAnnos
ga i :: EdgeId
i thmLk :: [XLink]
thmLk nds :: [XNode]
nds body :: XTree
body) lv :: LibEnv
lv = do
  (dg :: DGraph
dg, lv' :: LibEnv
lv') <- XTree -> LibEnv -> ResultT IO (DGraph, LibEnv)
forall (t :: * -> *).
Foldable t =>
[t ([XLink], XNode)] -> LibEnv -> ResultT IO (DGraph, LibEnv)
rebuiltBody XTree
body LibEnv
lv
  DGraph
dg' <- LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph
insertThmLinks LogicGraph
lg DGraph
dg (EdgeMap -> ResultT IO DGraph) -> EdgeMap -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ [XLink] -> EdgeMap
mkEdgeMap [XLink]
thmLk
  (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', LibEnv
lv') where
    rebuiltBody :: [t ([XLink], XNode)] -> LibEnv -> ResultT IO (DGraph, LibEnv)
rebuiltBody bd :: [t ([XLink], XNode)]
bd lv' :: LibEnv
lv' = case [t ([XLink], XNode)]
bd of
        [] ->
          ((DGraph, LibEnv) -> XNode -> ResultT IO (DGraph, LibEnv))
-> (DGraph, LibEnv) -> [XNode] -> ResultT IO (DGraph, LibEnv)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((XNode -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv))
-> (DGraph, LibEnv) -> XNode -> ResultT IO (DGraph, LibEnv)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((XNode -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv))
 -> (DGraph, LibEnv) -> XNode -> ResultT IO (DGraph, LibEnv))
-> (XNode -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv))
-> (DGraph, LibEnv)
-> XNode
-> ResultT IO (DGraph, LibEnv)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> LogicGraph
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGraph, LibEnv)
insertFirstNode HetcatsOpts
opts LogicGraph
lg)
            (DGraph
emptyDG { globalAnnos :: GlobalAnnos
globalAnnos = GlobalAnnos
ga, getNewEdgeId :: EdgeId
getNewEdgeId = EdgeId
i }, LibEnv
lv') [XNode]
nds
        bs :: t ([XLink], XNode)
bs : bd' :: [t ([XLink], XNode)]
bd' -> do
          (DGraph, LibEnv)
res0 <- [t ([XLink], XNode)] -> LibEnv -> ResultT IO (DGraph, LibEnv)
rebuiltBody [t ([XLink], XNode)]
bd' LibEnv
lv'
          ((DGraph, LibEnv)
 -> ([XLink], XNode) -> ResultT IO (DGraph, LibEnv))
-> (DGraph, LibEnv)
-> t ([XLink], XNode)
-> ResultT IO (DGraph, LibEnv)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dl :: (DGraph, LibEnv)
dl (lKs :: [XLink]
lKs, nd :: XNode
nd) ->
            HetcatsOpts
-> LogicGraph
-> XNode
-> [XLink]
-> (DGraph, LibEnv)
-> ResultT IO (DGraph, LibEnv)
insertStep HetcatsOpts
opts LogicGraph
lg XNode
nd [XLink]
lKs (DGraph, LibEnv)
dl)
            (DGraph, LibEnv)
res0 t ([XLink], XNode)
bs

-- | inserts a new node as well as all definition links pointing at that node
insertStep :: HetcatsOpts -> LogicGraph -> XNode -> [XLink] -> (DGraph, LibEnv)
           -> ResultT IO (DGraph, LibEnv)
insertStep :: HetcatsOpts
-> LogicGraph
-> XNode
-> [XLink]
-> (DGraph, LibEnv)
-> ResultT IO (DGraph, LibEnv)
insertStep opts :: HetcatsOpts
opts lg :: LogicGraph
lg xNd :: XNode
xNd lks :: [XLink]
lks (dg :: DGraph
dg, lv :: LibEnv
lv) = do
  [(Int, GMorphism, DGLinkType, XLink)]
mrs <- (XLink -> ResultT IO (Int, GMorphism, DGLinkType, XLink))
-> [XLink] -> ResultT IO [(Int, GMorphism, DGLinkType, XLink)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LogicGraph
-> DGraph
-> XLink
-> ResultT IO (Int, GMorphism, DGLinkType, XLink)
getTypeAndMorphism LogicGraph
lg DGraph
dg) [XLink]
lks
  G_sign lid :: lid
lid sg :: ExtSign sign symbol
sg sId :: SigId
sId <- LogicGraph
-> DGraph
-> [(Int, GMorphism, DGLinkType, XLink)]
-> ResultT IO G_sign
getSigForXNode LogicGraph
lg DGraph
dg [(Int, GMorphism, DGLinkType, XLink)]
mrs
  let j :: Int
j = DGraph -> Int
getNewNodeDG DGraph
dg
  (gt2 :: G_theory
gt2, dg' :: DGraph
dg', lv' :: LibEnv
lv') <-
    HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> Int
-> (DGraph, LibEnv)
-> ResultT IO (G_theory, DGraph, LibEnv)
insertNode HetcatsOpts
opts LogicGraph
lg (G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> 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 -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sg SigId
sId) XNode
xNd Int
j (DGraph
dg, LibEnv
lv)
  DGraph
dg'' <- (DGraph
 -> (Int, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph)
-> DGraph
-> [(Int, GMorphism, DGLinkType, XLink)]
-> ResultT IO DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> Int
-> G_sign
-> DGraph
-> (Int, GMorphism, DGLinkType, XLink)
-> ResultT IO DGraph
insertLink LogicGraph
lg Int
j (G_theory -> G_sign
signOf G_theory
gt2)) DGraph
dg' [(Int, GMorphism, DGLinkType, XLink)]
mrs
  (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg'', LibEnv
lv')

insertLink :: LogicGraph -> Graph.Node -> G_sign -> DGraph
            -> (Graph.Node, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph
insertLink :: LogicGraph
-> Int
-> G_sign
-> DGraph
-> (Int, GMorphism, DGLinkType, XLink)
-> ResultT IO DGraph
insertLink lg :: LogicGraph
lg j :: Int
j gs :: G_sign
gs dg :: DGraph
dg (i :: Int
i, mr :: GMorphism
mr, tp :: DGLinkType
tp, lk :: XLink
lk) = do
            DGLinkLab
lkLab <- LogicGraph
-> XLink
-> GMorphism
-> G_sign
-> DGLinkType
-> ResultT IO DGLinkLab
finalizeLink LogicGraph
lg XLink
lk GMorphism
mr G_sign
gs DGLinkType
tp
            DGraph -> ResultT IO DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> ResultT IO DGraph) -> DGraph -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGraph -> DGraph
insEdgeAsIs (Int
i, Int
j, DGLinkLab
lkLab) DGraph
dg

-- | inserts theorem links
insertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph
insertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph
insertThmLinks lg :: LogicGraph
lg p :: DGraph
p = (DGraph -> (FilePath, Map FilePath [XLink]) -> ResultT IO DGraph)
-> DGraph
-> [(FilePath, Map FilePath [XLink])]
-> ResultT IO DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg :: DGraph
dg (tgt :: FilePath
tgt, sm :: Map FilePath [XLink]
sm) -> do
  (j :: Int
j, gsig :: G_sign
gsig) <- FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode FilePath
tgt DGraph
dg
  LogicGraph
-> Int
-> G_sign
-> DGraph
-> Map FilePath [XLink]
-> ResultT IO DGraph
insertTarThmLinks LogicGraph
lg Int
j G_sign
gsig DGraph
dg Map FilePath [XLink]
sm) DGraph
p ([(FilePath, Map FilePath [XLink])] -> ResultT IO DGraph)
-> (EdgeMap -> [(FilePath, Map FilePath [XLink])])
-> EdgeMap
-> ResultT IO DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeMap -> [(FilePath, Map FilePath [XLink])]
forall k a. Map k a -> [(k, a)]
Map.toList

insertTarThmLinks :: LogicGraph -> Graph.Node -> G_sign
  -> DGraph -> Map.Map String [XLink] -> ResultT IO DGraph
insertTarThmLinks :: LogicGraph
-> Int
-> G_sign
-> DGraph
-> Map FilePath [XLink]
-> ResultT IO DGraph
insertTarThmLinks lg :: LogicGraph
lg j :: Int
j tgt :: G_sign
tgt p :: DGraph
p = (DGraph -> (FilePath, [XLink]) -> ResultT IO DGraph)
-> DGraph -> [(FilePath, [XLink])] -> ResultT IO DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg :: DGraph
dg (src :: FilePath
src, ls :: [XLink]
ls) -> do
  (i :: Int
i, gsig :: G_sign
gsig) <- FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode FilePath
src DGraph
dg
  (DGraph -> XLink -> ResultT IO DGraph)
-> DGraph -> [XLink] -> ResultT IO DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg' :: DGraph
dg' xLk :: XLink
xLk -> do
      (mr :: GMorphism
mr, tp :: DGLinkType
tp) <- LogicGraph
-> DGraph -> G_sign -> XLink -> ResultT IO (GMorphism, DGLinkType)
getTypeAndMorphism1 LogicGraph
lg DGraph
dg G_sign
gsig XLink
xLk
      LogicGraph
-> Int
-> G_sign
-> DGraph
-> (Int, GMorphism, DGLinkType, XLink)
-> ResultT IO DGraph
insertLink LogicGraph
lg Int
j G_sign
tgt DGraph
dg' (Int
i, GMorphism
mr, DGLinkType
tp, XLink
xLk)) DGraph
dg [XLink]
ls) DGraph
p ([(FilePath, [XLink])] -> ResultT IO DGraph)
-> (Map FilePath [XLink] -> [(FilePath, [XLink])])
-> Map FilePath [XLink]
-> ResultT IO DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map FilePath [XLink] -> [(FilePath, [XLink])]
forall k a. Map k a -> [(k, a)]
Map.toList

{- | given a links intermediate morphism and its target nodes signature,
this function calculates the final morphism for this link -}
finalizeLink :: LogicGraph -> XLink -> GMorphism -> G_sign -> DGLinkType
             -> ResultT IO DGLinkLab
finalizeLink :: LogicGraph
-> XLink
-> GMorphism
-> G_sign
-> DGLinkType
-> ResultT IO DGLinkLab
finalizeLink lg :: LogicGraph
lg xLk :: XLink
xLk mr :: GMorphism
mr sg :: G_sign
sg tp :: DGLinkType
tp = do
  GMorphism
mr' <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc (DGEdgeType -> DGEdgeTypeModInc) -> DGEdgeType -> DGEdgeTypeModInc
forall a b. (a -> b) -> a -> b
$ XLink -> DGEdgeType
lType XLink
xLk of
    HidingDef -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
sg (GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mr)
    _ -> do
      GMorphism
mr1 <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg (GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mr) G_sign
sg
      GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
mr GMorphism
mr1
  DGLinkLab -> ResultT IO DGLinkLab
forall (m :: * -> *) a. Monad m => a -> m a
return (DGLinkLab -> ResultT IO DGLinkLab)
-> DGLinkLab -> ResultT IO DGLinkLab
forall a b. (a -> b) -> a -> b
$ GMorphism -> DGLinkType -> DGLinkOrigin -> EdgeId -> DGLinkLab
defDGLinkId GMorphism
mr' DGLinkType
tp DGLinkOrigin
SeeTarget (EdgeId -> DGLinkLab) -> EdgeId -> DGLinkLab
forall a b. (a -> b) -> a -> b
$ XLink -> EdgeId
edgeId XLink
xLk

{- | based upon the morphisms of ingoing deflinks, calculate the initial
signature to be used for node insertion -}
getSigForXNode :: LogicGraph -> DGraph
               -> [(Graph.Node, GMorphism, DGLinkType, XLink)]
               -> ResultT IO G_sign
getSigForXNode :: LogicGraph
-> DGraph
-> [(Int, GMorphism, DGLinkType, XLink)]
-> ResultT IO G_sign
getSigForXNode lg :: LogicGraph
lg dg :: DGraph
dg mrs :: [(Int, GMorphism, DGLinkType, XLink)]
mrs = case [(Int, GMorphism, DGLinkType, XLink)]
mrs of
    [] -> FilePath -> ResultT IO G_sign
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail "insertStep: empty link list"
    (_, _, FreeOrCofreeDefLink _ _, xLk :: XLink
xLk) : rt :: [(Int, GMorphism, DGLinkType, XLink)]
rt -> do
        Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Int, GMorphism, DGLinkType, XLink)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, GMorphism, DGLinkType, XLink)]
rt)
          (ResultT IO () -> ResultT IO ()) -> ResultT IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> ResultT IO ()
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail "unexpected non-singleton free or cofree def link"
        ((Int, G_sign) -> G_sign)
-> ResultT IO (Int, G_sign) -> ResultT IO G_sign
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, G_sign) -> G_sign
forall a b. (a, b) -> b
snd (ResultT IO (Int, G_sign) -> ResultT IO G_sign)
-> ResultT IO (Int, G_sign) -> ResultT IO G_sign
forall a b. (a -> b) -> a -> b
$ FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode (XLink -> FilePath
source XLink
xLk) DGraph
dg
    _ -> Result G_sign -> ResultT IO G_sign
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_sign -> ResultT IO G_sign)
-> Result G_sign -> ResultT IO G_sign
forall a b. (a -> b) -> a -> b
$ LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion LogicGraph
lg ([G_sign] -> Result G_sign) -> [G_sign] -> Result G_sign
forall a b. (a -> b) -> a -> b
$ ((Int, GMorphism, DGLinkType, XLink) -> G_sign)
-> [(Int, GMorphism, DGLinkType, XLink)] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, m :: GMorphism
m, _, _) -> GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
m) [(Int, GMorphism, DGLinkType, XLink)]
mrs

-- | gathers information for an XLink using its source nodes signature
getTypeAndMorphism :: LogicGraph -> DGraph -> XLink
                   -> ResultT IO (Graph.Node, GMorphism, DGLinkType, XLink)
getTypeAndMorphism :: LogicGraph
-> DGraph
-> XLink
-> ResultT IO (Int, GMorphism, DGLinkType, XLink)
getTypeAndMorphism lg :: LogicGraph
lg dg :: DGraph
dg xLk :: XLink
xLk = do
  (i :: Int
i, sg1 :: G_sign
sg1) <- FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode (XLink -> FilePath
source XLink
xLk) DGraph
dg
  (mr' :: GMorphism
mr', lTp :: DGLinkType
lTp) <- LogicGraph
-> DGraph -> G_sign -> XLink -> ResultT IO (GMorphism, DGLinkType)
getTypeAndMorphism1 LogicGraph
lg DGraph
dg G_sign
sg1 XLink
xLk
  (Int, GMorphism, DGLinkType, XLink)
-> ResultT IO (Int, GMorphism, DGLinkType, XLink)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, GMorphism
mr', DGLinkType
lTp, XLink
xLk)

getTypeAndMorphism1 :: LogicGraph -> DGraph -> G_sign -> XLink
  -> ResultT IO (GMorphism, DGLinkType)
getTypeAndMorphism1 :: LogicGraph
-> DGraph -> G_sign -> XLink -> ResultT IO (GMorphism, DGLinkType)
getTypeAndMorphism1 lg :: LogicGraph
lg dg :: DGraph
dg sg1 :: G_sign
sg1 xLk :: XLink
xLk = do
    (sg2 :: G_sign
sg2, lTp :: DGLinkType
lTp) <- LogicGraph
-> DGraph -> G_sign -> XLink -> ResultT IO (G_sign, DGLinkType)
getTypeAndMorAux LogicGraph
lg DGraph
dg G_sign
sg1 XLink
xLk
    GMorphism
mr' <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> FilePath -> FilePath -> Result GMorphism
getGMorphism LogicGraph
lg G_sign
sg2 (XLink -> FilePath
mr_name XLink
xLk) (XLink -> FilePath
mapping XLink
xLk)
    (GMorphism, DGLinkType) -> ResultT IO (GMorphism, DGLinkType)
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism
mr', DGLinkType
lTp)

{- depending on the type of the link, the correct DGLinkType and the signature
for the (external) morphism are extracted here -}
getTypeAndMorAux :: LogicGraph -> DGraph -> G_sign -> XLink
                 -> ResultT IO (G_sign, DGLinkType)
getTypeAndMorAux :: LogicGraph
-> DGraph -> G_sign -> XLink -> ResultT IO (G_sign, DGLinkType)
getTypeAndMorAux lg :: LogicGraph
lg dg :: DGraph
dg sg :: G_sign
sg@(G_sign slid :: lid
slid _ _) xLk :: XLink
xLk = let
  emptySig :: G_sign
emptySig = 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
slid (lid -> 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 -> ExtSign sign symbol
ext_empty_signature lid
slid) SigId
startSigId
  mkRtVAL :: a -> b -> m (a, b)
mkRtVAL sg' :: a
sg' tp :: b
tp = (a, b) -> m (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
sg', b
tp)
  cc :: Conservativity
cc = XLink -> Conservativity
cons XLink
xLk
  in case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc (DGEdgeType -> DGEdgeTypeModInc) -> DGEdgeType -> DGEdgeTypeModInc
forall a b. (a -> b) -> a -> b
$ XLink -> DGEdgeType
lType XLink
xLk of
    HidingDef -> G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg DGLinkType
HidingDefLink
    GlobalDef -> G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Global Conservativity
cc
    HetDef -> G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Global Conservativity
cc
    LocalDef -> G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Scope -> Conservativity -> DGLinkType
localOrGlobalDef Scope
Local Conservativity
cc
    FreeOrCofreeDef fc :: FreeOrCofree
fc -> do
      (sg' :: G_sign
sg', mNd :: MaybeNode
mNd) <- case XLink -> Maybe FilePath
mr_source XLink
xLk of
        Nothing -> (G_sign, MaybeNode) -> ResultT IO (G_sign, MaybeNode)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign
emptySig, AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
slid)
        Just ms :: FilePath
ms -> do
          (j :: Int
j, sg' :: G_sign
sg') <- FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode FilePath
ms DGraph
dg
          (G_sign, MaybeNode) -> ResultT IO (G_sign, MaybeNode)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign
sg', NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode) -> NodeSig -> MaybeNode
forall a b. (a -> b) -> a -> b
$ Int -> G_sign -> NodeSig
NodeSig Int
j G_sign
sg')
      G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg' (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
fc MaybeNode
mNd
    ThmType thTp :: ThmTypes
thTp prv :: Bool
prv _ _ -> let
      lStat :: ThmLinkStatus
lStat = if Bool -> Bool
not Bool
prv then ThmLinkStatus
LeftOpen
          else DGRule -> ProofBasis -> ThmLinkStatus
Proven (XLink -> DGRule
rule XLink
xLk) (ProofBasis -> ThmLinkStatus) -> ProofBasis -> ThmLinkStatus
forall a b. (a -> b) -> a -> b
$ XLink -> ProofBasis
prBasis XLink
xLk in
      case ThmTypes
thTp of
        HidingThm -> do
          (i' :: Int
i', sg' :: G_sign
sg') <- case XLink -> Maybe FilePath
mr_source XLink
xLk of
            Just ms :: FilePath
ms -> FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode FilePath
ms DGraph
dg
            Nothing -> FilePath -> ResultT IO (Int, G_sign)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail "no morphism source declaration for HidingThmLink"
          GMorphism
mr' <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
sg' G_sign
sg
          G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg' (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Maybe FreeOrCofree
-> Int -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
forall a. Maybe a
Nothing Int
i' GMorphism
mr' ThmLinkStatus
lStat
        FreeOrCofreeThm fc :: FreeOrCofree
fc -> do
            (i' :: Int
i', sg' :: G_sign
sg') <- case XLink -> Maybe FilePath
mr_source XLink
xLk of
              Just ms :: FilePath
ms -> FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode FilePath
ms DGraph
dg
              Nothing -> (Int, G_sign) -> ResultT IO (Int, G_sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (-1, G_sign
emptySig)
            GMorphism
mr' <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
sg' G_sign
sg
            G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg' (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Maybe FreeOrCofree
-> Int -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm (FreeOrCofree -> Maybe FreeOrCofree
forall a. a -> Maybe a
Just FreeOrCofree
fc) Int
i' GMorphism
mr' ThmLinkStatus
lStat
        GlobalOrLocalThm sc :: Scope
sc _ -> G_sign -> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall (m :: * -> *) a b. Monad m => a -> b -> m (a, b)
mkRtVAL G_sign
sg
          (DGLinkType -> ResultT IO (G_sign, DGLinkType))
-> DGLinkType -> ResultT IO (G_sign, DGLinkType)
forall a b. (a -> b) -> a -> b
$ Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc (ThmLinkStatus -> LinkKind
ThmLink ThmLinkStatus
lStat) (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ Conservativity -> ConsStatus
mkConsStatus Conservativity
cc

{- | Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element
and the the DGraphs Global Annotations. The caller has to ensure that the
chosen nodeId is not used in dgraph. -}
insertNode :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> Graph.Node
  -> (DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)
insertNode :: HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> Int
-> (DGraph, LibEnv)
-> ResultT IO (G_theory, DGraph, LibEnv)
insertNode opts :: HetcatsOpts
opts lg :: LogicGraph
lg mGt :: Maybe G_theory
mGt xNd :: XNode
xNd n :: Int
n (dg :: DGraph
dg, lv :: LibEnv
lv) = do
  (lbl :: DGNodeLab
lbl, lv' :: LibEnv
lv') <- HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab HetcatsOpts
opts LogicGraph
lg Maybe G_theory
mGt XNode
xNd (DGraph
dg, LibEnv
lv)
  (G_theory, DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl, LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
n, DGNodeLab
lbl) DGraph
dg, LibEnv
lv')

{- | generate nodelab with startoff-gtheory and xnode information (a new libenv
is returned in case it was extended due to reference node insertion) -}
generateNodeLab :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode
  -> (DGraph, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab :: HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab opts :: HetcatsOpts
opts lg :: LogicGraph
lg mGt :: Maybe G_theory
mGt xNd :: XNode
xNd (dg :: DGraph
dg, lv :: LibEnv
lv) = case XNode
xNd of
  -- Case #1: Reference Node
  XRef nm :: NodeName
nm rfNd :: FilePath
rfNd rfLb :: FilePath
rfLb spc :: FilePath
spc -> do
          (dg' :: DGraph
dg', lv' :: LibEnv
lv') <- case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (FilePath -> LibName
emptyLibName FilePath
rfLb) LibEnv
lv of
            Just dg' :: DGraph
dg' -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg', LibEnv
lv)
            Nothing -> HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (DGraph, LibEnv)
loadRefLib HetcatsOpts
opts FilePath
rfLb LibEnv
lv
          (i :: Int
i, gt :: G_theory
gt) <- case FilePath -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName FilePath
rfNd DGraph
dg' of
              Just (i :: Int
i, lbl :: DGNodeLab
lbl) -> case G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
                G_sign lid :: lid
lid sign :: ExtSign sign symbol
sign sId :: SigId
sId -> (Int, G_theory) -> ResultT IO (Int, G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, lid -> ExtSign sign symbol -> SigId -> 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 -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sign SigId
sId)
              Nothing -> FilePath -> ResultT IO (Int, G_theory)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO (Int, G_theory))
-> FilePath -> ResultT IO (Int, G_theory)
forall a b. (a -> b) -> a -> b
$ "reference node " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
rfNd FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " was not found"
          (gt' :: G_theory
gt', _) <- G_theory
-> NodeName
-> DGraph
-> FilePath
-> ResultT IO (G_theory, Set G_symbol)
parseSpecs G_theory
gt NodeName
nm DGraph
dg FilePath
spc
          let nInf :: DGNodeInfo
nInf = LibName -> Int -> DGNodeInfo
newRefInfo (FilePath -> LibName
emptyLibName FilePath
rfLb) Int
i
          (DGNodeLab, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
nm DGNodeInfo
nInf G_theory
gt', LibEnv
lv')
  -- Case #2: Regular Node
  XNode nm :: NodeName
nm lN :: FilePath
lN (hid :: Bool
hid, syb :: FilePath
syb) spc :: FilePath
spc cc :: Conservativity
cc -> do
        -- StartOff-Theory. Taken from LogicGraph for initial Nodes
        G_theory
gt0 <- case Maybe G_theory
mGt of
          Nothing -> (AnyLogic -> G_theory)
-> ResultT IO AnyLogic -> ResultT IO G_theory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AnyLogic -> G_theory
emptyTheory (ResultT IO AnyLogic -> ResultT IO G_theory)
-> ResultT IO AnyLogic -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> LogicGraph -> ResultT IO AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> FilePath -> LogicGraph -> m AnyLogic
lookupLogic "generateNodeLab " FilePath
lN LogicGraph
lg
          Just gt :: G_theory
gt -> G_theory -> ResultT IO G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return G_theory
gt
        -- hidden symbols use a different parser
        G_theory
gt1 <- if Bool
hid then G_theory -> FilePath -> ResultT IO G_theory
parseHidden G_theory
gt0 FilePath
syb
                 else ((G_theory, Set G_symbol) -> G_theory)
-> ResultT IO (G_theory, Set G_symbol) -> ResultT IO G_theory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (G_theory, Set G_symbol) -> G_theory
forall a b. (a, b) -> a
fst (ResultT IO (G_theory, Set G_symbol) -> ResultT IO G_theory)
-> ResultT IO (G_theory, Set G_symbol) -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ G_theory
-> NodeName
-> DGraph
-> FilePath
-> ResultT IO (G_theory, Set G_symbol)
parseSpecs G_theory
gt0 NodeName
nm DGraph
dg FilePath
syb
        (gt2 :: G_theory
gt2, syb' :: Set G_symbol
syb') <- G_theory
-> NodeName
-> DGraph
-> FilePath
-> ResultT IO (G_theory, Set G_symbol)
parseSpecs G_theory
gt1 NodeName
nm DGraph
dg FilePath
spc
        -- the DGOrigin is also different for nodes with hidden symbols
        DGOrigin
lOrig <- if Bool
hid then let
                syms :: Set G_symbol
syms = Set G_symbol -> Set G_symbol -> Set G_symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (G_sign -> Set G_symbol
symsOfGsign (G_sign -> Set G_symbol) -> G_sign -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt0)
                  (Set G_symbol -> Set G_symbol) -> Set G_symbol -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ G_sign -> Set G_symbol
symsOfGsign (G_sign -> Set G_symbol) -> G_sign -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt2
                in DGOrigin -> ResultT IO DGOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return (DGOrigin -> ResultT IO DGOrigin)
-> DGOrigin -> ResultT IO DGOrigin
forall a b. (a -> b) -> a -> b
$ MaybeRestricted -> Set G_symbol -> DGOrigin
DGRestriction MaybeRestricted
NoRestriction Set G_symbol
syms
          else do
            G_sign
diffSig <- Result G_sign -> ResultT IO G_sign
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_sign -> ResultT IO G_sign)
-> Result G_sign -> ResultT IO G_sign
forall a b. (a -> b) -> a -> b
$ G_sign -> G_sign -> Result G_sign
homGsigDiff (G_theory -> G_sign
signOf G_theory
gt2) (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt0
            DGOrigin -> ResultT IO DGOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return (DGOrigin -> ResultT IO DGOrigin)
-> DGOrigin -> ResultT IO DGOrigin
forall a b. (a -> b) -> a -> b
$ Maybe G_basic_spec -> G_sign -> Set G_symbol -> DGOrigin
DGBasicSpec Maybe G_basic_spec
forall a. Maybe a
Nothing G_sign
diffSig Set G_symbol
syb'
        (DGNodeLab, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
nm (DGOrigin -> Conservativity -> DGNodeInfo
newConsNodeInfo DGOrigin
lOrig Conservativity
cc) G_theory
gt2, LibEnv
lv)

insertFirstNode :: HetcatsOpts -> LogicGraph -> XNode -> (DGraph, LibEnv)
  -> ResultT IO (DGraph, LibEnv)
insertFirstNode :: HetcatsOpts
-> LogicGraph
-> XNode
-> (DGraph, LibEnv)
-> ResultT IO (DGraph, LibEnv)
insertFirstNode opts :: HetcatsOpts
opts lg :: LogicGraph
lg xNd :: XNode
xNd p :: (DGraph, LibEnv)
p@(dg' :: DGraph
dg', _) = let n :: Int
n = DGraph -> Int
getNewNodeDG DGraph
dg' in do
  (_, dg :: DGraph
dg, lv :: LibEnv
lv) <- HetcatsOpts
-> LogicGraph
-> Maybe G_theory
-> XNode
-> Int
-> (DGraph, LibEnv)
-> ResultT IO (G_theory, DGraph, LibEnv)
insertNode HetcatsOpts
opts LogicGraph
lg Maybe G_theory
forall a. Maybe a
Nothing XNode
xNd Int
n (DGraph, LibEnv)
p
  (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, LibEnv
lv)

parseHidden :: G_theory -> String -> ResultT IO G_theory
parseHidden :: G_theory -> FilePath -> ResultT IO G_theory
parseHidden gt :: G_theory
gt s' :: FilePath
s' = do
  G_sign
gs <- Result G_sign -> ResultT IO G_sign
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_sign -> ResultT IO G_sign)
-> Result G_sign -> ResultT IO G_sign
forall a b. (a -> b) -> a -> b
$ FilePath -> G_sign -> Result G_sign
deleteHiddenSymbols FilePath
s' (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt
  G_theory -> ResultT IO G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> ResultT IO G_theory)
-> G_theory -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ case G_sign
gs of
    G_sign lid :: lid
lid sg :: ExtSign sign symbol
sg sId :: SigId
sId -> lid -> ExtSign sign symbol -> SigId -> 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 -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sg SigId
sId

parseSpecs :: G_theory -> NodeName -> DGraph -> String
           -> ResultT IO (G_theory, Set G_symbol)
parseSpecs :: G_theory
-> NodeName
-> DGraph
-> FilePath
-> ResultT IO (G_theory, Set G_symbol)
parseSpecs gt' :: G_theory
gt' nm :: NodeName
nm dg :: DGraph
dg spec :: FilePath
spec = let
          (response :: BasicExtResponse
response, msg :: FilePath
msg) = GlobalAnnos -> FilePath -> G_theory -> (BasicExtResponse, FilePath)
extendByBasicSpec (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) FilePath
spec G_theory
gt'
          in case BasicExtResponse
response of
            Success gt'' :: G_theory
gt'' _ smbs :: Set G_symbol
smbs _ -> (G_theory, Set G_symbol) -> ResultT IO (G_theory, Set G_symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
gt'', Set G_symbol
smbs)
            Failure _ -> FilePath -> ResultT IO (G_theory, Set G_symbol)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO (G_theory, Set G_symbol))
-> FilePath -> ResultT IO (G_theory, Set G_symbol)
forall a b. (a -> b) -> a -> b
$ "[ " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ NodeName -> FilePath
showName NodeName
nm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " ]\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg

loadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)
loadRefLib :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (DGraph, LibEnv)
loadRefLib opts :: HetcatsOpts
opts ln :: FilePath
ln lv :: LibEnv
lv = do
          Maybe FilePath
mPath <- IO (Maybe FilePath) -> ResultT IO (Maybe FilePath)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe FilePath) -> ResultT IO (Maybe FilePath))
-> IO (Maybe FilePath) -> ResultT IO (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> IO (Maybe FilePath)
findFileOfLibNameAux HetcatsOpts
opts { intype :: InType
intype = InType
DgXml } FilePath
ln
          case Maybe FilePath
mPath of
            Just path :: FilePath
path -> do
              (ln' :: LibName
ln', lv' :: LibEnv
lv') <- HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
readDGXmlR HetcatsOpts
opts FilePath
path LibEnv
lv
              (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln' LibEnv
lv', LibEnv
lv')
            _ -> FilePath -> ResultT IO (DGraph, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO (DGraph, LibEnv))
-> FilePath -> ResultT IO (DGraph, LibEnv)
forall a b. (a -> b) -> a -> b
$ "no file exists for reference library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
ln

-- | creates an entirely empty theory
emptyTheory :: AnyLogic -> G_theory
emptyTheory :: AnyLogic -> G_theory
emptyTheory (Logic lid :: lid
lid) =
  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 (lid -> 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 -> ExtSign sign symbol
ext_empty_signature lid
lid) SigId
startSigId ThSens sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId

{- | A Node is looked up via its name in the DGraph. Returns the nodes
signature, but only if one single node is found for the respective name.
Otherwise an error is thrown. -}
signOfNode :: String -> DGraph -> ResultT IO (Graph.Node, G_sign)
signOfNode :: FilePath -> DGraph -> ResultT IO (Int, G_sign)
signOfNode nd :: FilePath
nd dg :: DGraph
dg = case FilePath -> DGraph -> Maybe (LNode DGNodeLab)
lookupUniqueNodeByName FilePath
nd DGraph
dg of
  Nothing -> FilePath -> ResultT IO (Int, G_sign)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO (Int, G_sign))
-> FilePath -> ResultT IO (Int, G_sign)
forall a b. (a -> b) -> a -> b
$ "required node [" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
nd FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "] was not found in DGraph!"
  Just (j :: Int
j, lbl :: DGNodeLab
lbl) ->
    (Int, G_sign) -> ResultT IO (Int, G_sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
j, G_theory -> G_sign
signOf (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl))