{-# LANGUAGE CPP #-}
{- |
Module      :  ./Proofs/VSE.hs
Description :  Interface to send structured theories to the VSE prover
Copyright   :  (c) C. Maeder, DFKI 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

call an adaption of VSE II to hets

the prover should be attached to a node's menu (if applicable) but take the
whole library environment as in- and output like development graph rules.
-}

module Proofs.VSE where

import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.PrintDevGraph
import Static.DGTranslation
import Static.History
import Static.ComputeTheory

import Proofs.QualifyNames

import Common.AS_Annotation
import Common.ExtSign
import Common.Id
import Common.LibName
import Common.Result
import Common.ResultT
import Common.SExpr
import qualified Common.OrderedMap as OMap

import Logic.Logic
import Logic.Prover
import Logic.Comorphism
import Logic.Coerce
import Logic.Grothendieck

import VSE.Logic_VSE

import VSE.Prove
import VSE.ToSExpr
import Comorphisms.CASL2VSE
import CASL.ToSExpr
import CASL.Logic_CASL

import Data.Char
import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Graph.Inductive.Basic (elfilter, gfold)
import Data.Graph.Inductive.Graph hiding (out)

import Control.Monad.Trans

thName :: LibName -> LNode DGNodeLab -> String
thName :: LibName -> LNode DGNodeLab -> String
thName ln :: LibName
ln (n :: Node
n, lbl :: DGNodeLab
lbl) = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "/,[]: " then '-' else Char
c)
           (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ LibName -> String
libToFileName LibName
ln String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
lbl String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
n

getSubGraph :: Node -> DGraph -> DGraph
getSubGraph :: Node -> DGraph -> DGraph
getSubGraph n :: Node
n dg :: DGraph
dg =
    let g :: Gr DGNodeLab DGLinkLab
g = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
        ns :: [Node]
ns = Gr DGNodeLab DGLinkLab -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes Gr DGNodeLab DGLinkLab
g
        sns :: Set Node
sns = (Context DGNodeLab DGLinkLab -> [Node])
-> (Context DGNodeLab DGLinkLab -> Set Node -> Set Node)
-> (Maybe (Set Node) -> Set Node -> Set Node, Set Node)
-> [Node]
-> Gr DGNodeLab DGLinkLab
-> Set Node
forall (gr :: * -> * -> *) a b c d.
Graph gr =>
(Context a b -> [Node])
-> (Context a b -> c -> d)
-> (Maybe d -> c -> c, c)
-> [Node]
-> gr a b
-> c
gfold Context DGNodeLab DGLinkLab -> [Node]
forall a b. Context a b -> [Node]
pre' (\ c :: Context DGNodeLab DGLinkLab
c s :: Set Node
s -> Node -> Set Node -> Set Node
forall a. Ord a => a -> Set a -> Set a
Set.insert (Context DGNodeLab DGLinkLab -> Node
forall a b. Context a b -> Node
node' Context DGNodeLab DGLinkLab
c) Set Node
s)
          (\ m :: Maybe (Set Node)
m s :: Set Node
s -> Set Node -> Set Node -> Set Node
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Node
s (Set Node -> Set Node) -> Set Node -> Set Node
forall a b. (a -> b) -> a -> b
$ Set Node -> Maybe (Set Node) -> Set Node
forall a. a -> Maybe a -> a
fromMaybe Set Node
forall a. Set a
Set.empty Maybe (Set Node)
m, Set Node
forall a. Set a
Set.empty) [Node
n] Gr DGNodeLab DGLinkLab
g
    in [Node] -> DGraph -> DGraph
delNodesDG (Set Node -> [Node]
forall a. Set a -> [a]
Set.toList (Set Node -> [Node]) -> Set Node -> [Node]
forall a b. (a -> b) -> a -> b
$ Set Node -> Set Node -> Set Node
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([Node] -> Set Node
forall a. Ord a => [a] -> Set a
Set.fromList [Node]
ns) Set Node
sns) DGraph
dg

-- | applies basic inference to a given node and whole import tree above
proveVSE :: (LibName, Node) -> LibEnv -> IO (Result LibEnv)
proveVSE :: (LibName, Node) -> LibEnv -> IO (Result LibEnv)
proveVSE (ln :: LibName
ln, node :: Node
node) libEnv :: LibEnv
libEnv =
  ResultT IO LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO LibEnv -> IO (Result LibEnv))
-> ResultT IO LibEnv -> IO (Result LibEnv)
forall a b. (a -> b) -> a -> b
$ do
    LibEnv
qLibEnv <- Result LibEnv -> ResultT IO LibEnv
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result LibEnv -> ResultT IO LibEnv)
-> Result LibEnv -> ResultT IO LibEnv
forall a b. (a -> b) -> a -> b
$ LibEnv -> Result LibEnv
qualifyLibEnv LibEnv
libEnv
    let dg1 :: DGraph
dg1 = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
qLibEnv
        dg2 :: DGraph
dg2 = DGraph
dg1 { dgBody :: Gr DGNodeLab DGLinkLab
dgBody = (DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (DGLinkType -> Bool
isGlobalEdge (DGLinkType -> Bool)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type) (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg1 }
        dg3 :: DGraph
dg3 = Node -> DGraph -> DGraph
getSubGraph Node
node DGraph
dg2
        oLbl :: DGNodeLab
oLbl = DGraph -> Node -> DGNodeLab
labDG DGraph
dg3 Node
node
        ostr :: String
ostr = LibName -> LNode DGNodeLab -> String
thName LibName
ln (Node
node, DGNodeLab
oLbl)
    G_theory olid :: lid
olid _ _ _ _ _ <- 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
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
oLbl
    let mcm :: Maybe AnyComorphism
mcm = if CASL -> 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 CASL
CASL AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== 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
olid then AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just (CASL2VSE -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism CASL2VSE
CASL2VSE) else
             Maybe AnyComorphism
forall a. Maybe a
Nothing
    DGraph
dGraph <- Result DGraph -> ResultT IO DGraph
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result DGraph -> ResultT IO DGraph)
-> Result DGraph -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ (DGraph -> Result DGraph)
-> (AnyComorphism -> DGraph -> Result DGraph)
-> Maybe AnyComorphism
-> DGraph
-> Result DGraph
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return ((DGraph -> AnyComorphism -> Result DGraph)
-> AnyComorphism -> DGraph -> Result DGraph
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((DGraph -> AnyComorphism -> Result DGraph)
 -> AnyComorphism -> DGraph -> Result DGraph)
-> (DGraph -> AnyComorphism -> Result DGraph)
-> AnyComorphism
-> DGraph
-> Result DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> DGraph -> AnyComorphism -> Result DGraph
dg_translation LibEnv
qLibEnv LibName
ln) Maybe AnyComorphism
mcm DGraph
dg3
    let nls :: [LNode DGNodeLab]
nls = DGraph -> [LNode DGNodeLab]
topsortedNodes DGraph
dGraph
        ns :: [DGNodeLab]
ns = (LNode DGNodeLab -> DGNodeLab) -> [LNode DGNodeLab] -> [DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd [LNode DGNodeLab]
nls
    [(String, String)]
ts <- Result [(String, String)] -> ResultT IO [(String, String)]
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result [(String, String)] -> ResultT IO [(String, String)])
-> Result [(String, String)] -> ResultT IO [(String, String)]
forall a b. (a -> b) -> a -> b
$ (DGNodeLab -> Result (String, String))
-> [DGNodeLab] -> Result [(String, String)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
      (\ lbl :: DGNodeLab
lbl -> do
         let lbln :: String
lbln = DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
         G_theory lid :: lid
lid _ (ExtSign sign0 :: sign
sign0 _) _ sens0 :: ThSens sentence (AnyComorphism, BasicProof)
sens0 _ <- 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
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl
         (sign1 :: VSESign
sign1, sens1 :: [Named Sentence]
sens1) <-
           String
-> LibName
-> Result (VSESign, [Named Sentence])
-> Result (VSESign, [Named Sentence])
forall a b.
(GetRange a, Pretty a) =>
String -> a -> Result b -> Result b
addErrorDiag "failure when proving VSE nodes of" LibName
ln
           (Result (VSESign, [Named Sentence])
 -> Result (VSESign, [Named Sentence]))
-> Result (VSESign, [Named Sentence])
-> Result (VSESign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ lid
-> VSE
-> String
-> (sign, [Named sentence])
-> Result (VSESign, [Named Sentence])
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
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid VSE
VSE
             ("cannot cast untranslated node '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lbln String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'")
             (sign
sign0, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens0)
         let (sign2 :: VSESign
sign2, sens2 :: [Named Sentence]
sens2) = VSESign -> [Named Sentence] -> (VSESign, [Named Sentence])
forall f.
Sign f Procs
-> [Named Sentence] -> (Sign f Procs, [Named Sentence])
addUniformRestr VSESign
sign1 [Named Sentence]
sens1
         (String, String) -> Result (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return
           ( Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SExpr -> Doc
prettySExpr
             (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> LibName -> VSESign -> SExpr
forall f. SIMPLE_ID -> LibName -> Sign f Procs -> SExpr
qualVseSignToSExpr (String -> SIMPLE_ID
mkSimpleId String
lbln) LibName
ln VSESign
sign2
           , Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SExpr -> Doc
prettySExpr
             (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> SExpr) -> [Named Sentence] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (VSESign -> Named Sentence -> SExpr
forall f. Sign f Procs -> Named Sentence -> SExpr
namedSenToSExpr VSESign
sign2) [Named Sentence]
sens2)) [DGNodeLab]
ns
    IO LibEnv -> ResultT IO LibEnv
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO LibEnv -> ResultT IO LibEnv) -> IO LibEnv -> ResultT IO LibEnv
forall a b. (a -> b) -> a -> b
$ do
#ifdef TAR_PACKAGE
       String -> IO ()
moveVSEFiles String
ostr
#endif
       (inp :: Handle
inp, out :: Handle
out, cp :: ProcessHandle
cp) <- IO (Handle, Handle, ProcessHandle)
prepareAndCallVSE
       Handle -> String -> IO ()
sendMyMsg Handle
inp (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((LNode DGNodeLab -> String) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (LibName -> LNode DGNodeLab -> String
thName LibName
ln) [LNode DGNodeLab]
nls) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
       (LNode DGNodeLab -> IO ()) -> [LNode DGNodeLab] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ nl :: LNode DGNodeLab
nl -> do
           ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
linksP
           String
str <- LibName -> DGraph -> LNode DGNodeLab -> IO String
getLinksTo LibName
ln DGraph
dGraph LNode DGNodeLab
nl
           Handle -> String -> IO ()
sendMyMsg Handle
inp String
str) [LNode DGNodeLab]
nls
       ((String, String) -> IO ()) -> [(String, String)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (fsig :: String
fsig, _) -> do
           ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
sigP
           Handle -> String -> IO ()
sendMyMsg Handle
inp String
fsig) [(String, String)]
ts
       ((String, String) -> IO ()) -> [(String, String)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_, sens :: String
sens) -> do
           ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
lemsP
           Handle -> String -> IO ()
sendMyMsg Handle
inp String
sens) [(String, String)]
ts
       Maybe (Map String [String])
ms <- ProcessHandle -> Handle -> IO (Maybe (Map String [String]))
readFinalVSEOutput ProcessHandle
cp Handle
out
#ifdef TAR_PACKAGE
       String -> IO ()
createVSETarFile String
ostr
#endif
       case Maybe (Map String [String])
ms of
         Nothing -> LibEnv -> IO LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return LibEnv
libEnv
         Just lemMap :: Map String [String]
lemMap -> LibEnv -> IO LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> IO LibEnv) -> LibEnv -> IO LibEnv
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> LibEnv -> LibEnv)
-> LibEnv -> [LNode DGNodeLab] -> LibEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (n :: Node
n, lbl :: DGNodeLab
lbl) le :: LibEnv
le ->
                 let str :: String
str = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ LibName -> LNode DGNodeLab -> String
thName LibName
ln (Node
n, DGNodeLab
lbl)
                     lems :: Set String
lems = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ [String] -> String -> Map String [String] -> [String]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] String
str Map String [String]
lemMap
                 in if Set String -> Bool
forall a. Set a -> Bool
Set.null Set String
lems then LibEnv
le else let
                     dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
                     in case Gr DGNodeLab DGLinkLab -> Node -> Maybe DGNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg) Node
n of
                     Nothing -> LibEnv
le -- node missing in original graph
                     Just olbl :: DGNodeLab
olbl -> case DGNodeLab -> G_theory
dgn_theory DGNodeLab
olbl of
                       G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig sigId :: SigId
sigId sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> let
                         axs :: [String]
axs = ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Map k a -> [k]
Map.keys (ThSens sentence (AnyComorphism, BasicProof) -> [String])
-> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens
                         nsens :: ThSens sentence (AnyComorphism, BasicProof)
nsens = (String
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. (k -> a -> b) -> OMap k a -> OMap k b
OMap.mapWithKey (\ name :: String
name sen :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen ->
                             if Bool -> Bool
not (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) Bool -> Bool -> Bool
&& String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member
                                  ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
transString String
name) Set String
lems
                             then SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen {
                                 senAttr :: ThmStatus (AnyComorphism, BasicProof)
senAttr = [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a. [a] -> ThmStatus a
ThmStatus ([(AnyComorphism, BasicProof)]
 -> ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$
                                     (CASL2VSE -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism CASL2VSE
CASL2VSE,
                                     VSE -> ProofStatus () -> BasicProof
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 -> ProofStatus proof_tree -> BasicProof
BasicProof VSE
VSE (ProofStatus () -> BasicProof) -> ProofStatus () -> BasicProof
forall a b. (a -> b) -> a -> b
$
                                       String -> [String] -> ProofStatus ()
mkVseProofStatus String
name [String]
axs)
                                       (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a. a -> [a] -> [a]
: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen }
                             else SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) ThSens sentence (AnyComorphism, BasicProof)
sens
                         nlbl :: DGNodeLab
nlbl = DGNodeLab
olbl { dgn_theory :: G_theory
dgn_theory
                           = 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
syn ExtSign sign symbol
sig SigId
sigId ThSens sentence (AnyComorphism, BasicProof)
nsens ThId
startThId }
                         flbl :: DGNodeLab
flbl = DGNodeLab
nlbl { globalTheory :: Maybe G_theory
globalTheory
                           = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
le LibName
ln DGraph
dg (Node
n, DGNodeLab
nlbl) }
                         ndg :: DGraph
ndg = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
olbl (Node
n, DGNodeLab
flbl)
                        in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
ndg LibEnv
le) LibEnv
libEnv [LNode DGNodeLab]
nls

getLinksTo :: LibName -> DGraph -> LNode DGNodeLab -> IO String
getLinksTo :: LibName -> DGraph -> LNode DGNodeLab -> IO String
getLinksTo ln :: LibName
ln dg :: DGraph
dg (n :: Node
n, lbl :: DGNodeLab
lbl) = do
  let (ls :: [(Node, Node, DGLinkLab)]
ls, rs :: [(Node, Node, DGLinkLab)]
rs) = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)]
-> ([(Node, Node, DGLinkLab)], [(Node, Node, DGLinkLab)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ (s :: Node
s, _, el :: DGLinkLab
el) -> Node
s Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
n
           Bool -> Bool -> Bool
&& DGLinkType -> Bool
isGlobalDef (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el)
           Bool -> Bool -> Bool
&& DGEdgeType -> Bool
isInc (DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
el)) ([(Node, Node, DGLinkLab)]
 -> ([(Node, Node, DGLinkLab)], [(Node, Node, DGLinkLab)]))
-> [(Node, Node, DGLinkLab)]
-> ([(Node, Node, DGLinkLab)], [(Node, Node, DGLinkLab)])
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [(Node, Node, DGLinkLab)]
innDG DGraph
dg Node
n
  ((Node, Node, DGLinkLab) -> IO ())
-> [(Node, Node, DGLinkLab)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ e :: (Node, Node, DGLinkLab)
e -> String -> IO ()
putStrLn
        (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "ignored unsupported link (non-inclusion or theorem link):\n "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ((Node, Node, DGLinkLab) -> Doc
prettyLEdge (Node, Node, DGLinkLab)
e)) [(Node, Node, DGLinkLab)]
rs
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SExpr -> Doc
prettySExpr (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
SList
    ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ ((Node, Node, DGLinkLab) -> SExpr)
-> [(Node, Node, DGLinkLab)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, el :: DGLinkLab
el) -> let
    ltype :: DGLinkType
ltype = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el
    defl :: Bool
defl = DGLinkType -> Bool
isGlobalDef DGLinkType
ltype
    in [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$
    [ String -> SExpr
SSymbol (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ (if Bool
defl then "definition" else "theorem") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-link"
    , String -> SExpr
SSymbol (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ "edge" String -> String -> String
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
el)
    , String -> SExpr
SSymbol (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ LibName -> LNode DGNodeLab -> String
thName LibName
ln (Node
s, DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
s)
    , String -> SExpr
SSymbol (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ LibName -> LNode DGNodeLab -> String
thName LibName
ln (Node
n, DGNodeLab
lbl)
    , String -> SExpr
SSymbol "global"
    , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ String -> SExpr
SSymbol "morphism" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: GMorphism -> [SExpr]
hetMorToSSexpr (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
el)]
    [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ if Bool
defl then [] else
       [String -> SExpr
SSymbol (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ if DGLinkType -> Bool
isProven DGLinkType
ltype then "proven" else "open"]) [(Node, Node, DGLinkLab)]
ls

hetMorToSSexpr :: GMorphism -> [SExpr]
hetMorToSSexpr :: GMorphism -> [SExpr]
hetMorToSSexpr (GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _) =
  let tlid :: lid2
tlid = cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid
  in case lid2
-> VSE
-> String
-> morphism2
-> Maybe (Morphism Dlformula Procs VSEMorExt)
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 -> String -> morphism1 -> m morphism2
coerceMorphism lid2
tlid VSE
VSE "" morphism2
mor of
       Just vsemor :: Morphism Dlformula Procs VSEMorExt
vsemor -> Morphism Dlformula Procs VSEMorExt -> [SExpr]
forall f e m. Morphism f e m -> [SExpr]
morToSExprs Morphism Dlformula Procs VSEMorExt
vsemor
       Nothing -> case lid2 -> CASL -> String -> morphism2 -> Maybe (Morphism () () ())
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 -> String -> morphism1 -> m morphism2
coerceMorphism lid2
tlid CASL
CASL "" morphism2
mor of
         Just cmor :: Morphism () () ()
cmor -> Morphism () () () -> [SExpr]
forall f e m. Morphism f e m -> [SExpr]
morToSExprs Morphism () () ()
cmor
         Nothing -> []