{- |
Module      :  ./Static/DGTranslation.hs
Description :  Translation of development graphs along comorphisms
Copyright   :  Heng Jiang, Uni Bremen 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

Translation of development graphs along comorphisms
   Follows Sect. IV:4.3 of the CASL Reference Manual.
-}

module Static.DGTranslation
    ( libEnv_translation
    , dg_translation
    , getDGLogic
    ) where

import Static.GTheory
import Static.DevGraph
import Static.PrintDevGraph
import Static.ComputeTheory

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

import Common.ExtSign
import Common.LibName
import Common.Result

import qualified Data.Map as Map
import qualified Data.Set as Set

import Data.Graph.Inductive.Graph

import Control.Monad (foldM)
import qualified Control.Monad.Fail as Fail

-- | translation of a LibEnv (a map of globalcontext)
libEnv_translation :: LibEnv -> AnyComorphism -> Result LibEnv
libEnv_translation :: LibEnv -> AnyComorphism -> Result LibEnv
libEnv_translation libEnv :: LibEnv
libEnv com :: AnyComorphism
com =
  (LibEnv -> LibName -> Result LibEnv)
-> LibEnv -> [LibName] -> Result LibEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ le :: LibEnv
le ln :: LibName
ln -> do
    DGraph
dgTr <- LibEnv -> LibName -> DGraph -> AnyComorphism -> Result DGraph
dg_translation LibEnv
le LibName
ln (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv) AnyComorphism
com
    LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dgTr LibEnv
le) LibEnv
forall k a. Map k a
Map.empty ([LibName] -> Result LibEnv) -> [LibName] -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
getTopsortedLibs LibEnv
libEnv

dg_translation :: LibEnv -> LibName -> DGraph -> AnyComorphism -> Result DGraph
dg_translation :: LibEnv -> LibName -> DGraph -> AnyComorphism -> Result DGraph
dg_translation le :: LibEnv
le ln :: LibName
ln gc :: DGraph
gc acm :: AnyComorphism
acm@(Comorphism cidMor :: cid
cidMor) =
    let labNodesList :: [LNode DGNodeLab]
labNodesList = DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
gc
        labEdgesList :: [LEdge DGLinkLab]
labEdgesList = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
gc
    in String -> () -> Result DGraph -> Result DGraph
forall a b.
(GetRange a, Pretty a) =>
String -> a -> Result b -> Result b
addErrorDiag ("translation failed via: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cidMor) ()
       (Result DGraph -> Result DGraph) -> Result DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ do
        [LEdge DGLinkLab]
resOfEdges <- (LEdge DGLinkLab -> Result (LEdge DGLinkLab))
-> [LEdge DGLinkLab] -> Result [LEdge DGLinkLab]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (AnyComorphism
-> DGraph -> LEdge DGLinkLab -> Result (LEdge DGLinkLab)
updateEdges AnyComorphism
acm DGraph
gc) [LEdge DGLinkLab]
labEdgesList
        [LNode DGNodeLab]
resOfNodes <- (LNode DGNodeLab -> Result (LNode DGNodeLab))
-> [LNode DGNodeLab] -> Result [LNode DGNodeLab]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (AnyComorphism -> LNode DGNodeLab -> Result (LNode DGNodeLab)
updateNodes AnyComorphism
acm) [LNode DGNodeLab]
labNodesList
        DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le LibName
ln
          (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph
mkGraphDG [LNode DGNodeLab]
resOfNodes [LEdge DGLinkLab]
resOfEdges DGraph
emptyDG

updateEdges :: AnyComorphism -> DGraph -> LEdge DGLinkLab
  -> Result (LEdge DGLinkLab)
updateEdges :: AnyComorphism
-> DGraph -> LEdge DGLinkLab -> Result (LEdge DGLinkLab)
updateEdges (Comorphism cidMor :: cid
cidMor) gc :: DGraph
gc (s :: Node
s, t :: Node
t, lbl :: DGLinkLab
lbl) = case DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl of
  GMorphism cid' :: cid
cid' esig :: ExtSign sign1 symbol1
esig _ mor :: morphism2
mor _ ->
   if AnyComorphism -> Bool
isIdComorphism (cid -> 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 cid
cid')
   then do
     let slid :: lid1
slid = cid -> lid1
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 -> lid1
sourceLogic cid
cidMor
         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
cidMor
     ExtSign lsign :: sign1
lsign sys :: Set symbol1
sys <- lid1
-> lid1
-> String
-> ExtSign sign1 symbol1
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign (cid -> lid1
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 -> lid1
sourceLogic cid
cid') lid1
slid
       "DGTranslation.fSign" ExtSign sign1 symbol1
esig
     (lsign' :: sign2
lsign', _) <- cid -> sign1 -> Result (sign2, [Named sentence2])
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 -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
cidMor sign1
lsign
     morphism1
lMor <- lid2 -> lid1 -> String -> morphism2 -> Result morphism1
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 (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') lid1
slid "DGTranslation.fMor" morphism2
mor
     morphism2
lmorphism' <- cid -> morphism1 -> Result morphism2
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 -> morphism1 -> Result morphism2
map_morphism cid
cidMor morphism1
lMor
     LEdge DGLinkLab -> Result (LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
s, Node
t, DGLinkLab
lbl
       { dgl_morphism :: GMorphism
dgl_morphism = InclComorphism lid2 sublogics2
-> ExtSign sign2 symbol2
-> SigId
-> morphism2
-> MorId
-> GMorphism
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
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism (lid2 -> sublogics2 -> InclComorphism lid2 sublogics2
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 -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid2
tlid (sublogics2 -> InclComorphism lid2 sublogics2)
-> sublogics2 -> InclComorphism lid2 sublogics2
forall a b. (a -> b) -> a -> b
$ lid2 -> sublogics2
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 -> sublogics
top_sublogic lid2
tlid)
         (sign2 -> Set symbol2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign2
lsign' (Set symbol2 -> ExtSign sign2 symbol2)
-> Set symbol2 -> ExtSign sign2 symbol2
forall a b. (a -> b) -> a -> b
$ [Set symbol2] -> Set symbol2
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
         ([Set symbol2] -> Set symbol2) -> [Set symbol2] -> Set symbol2
forall a b. (a -> b) -> a -> b
$ (symbol1 -> Set symbol2) -> [symbol1] -> [Set symbol2]
forall a b. (a -> b) -> [a] -> [b]
map (cid -> sign1 -> symbol1 -> Set symbol2
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 -> sign1 -> symbol1 -> Set symbol2
map_symbol cid
cidMor sign1
lsign) ([symbol1] -> [Set symbol2]) -> [symbol1] -> [Set symbol2]
forall a b. (a -> b) -> a -> b
$ Set symbol1 -> [symbol1]
forall a. Set a -> [a]
Set.toList Set symbol1
sys)
         SigId
startSigId morphism2
lmorphism' MorId
startMorId })
   else String -> Result (LEdge DGLinkLab)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (LEdge DGLinkLab))
-> String -> Result (LEdge DGLinkLab)
forall a b. (a -> b) -> a -> b
$ "Link " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> Node -> DGraph -> String
showFromTo Node
s Node
t DGraph
gc String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not homogeneous."

updateNodes :: AnyComorphism -> LNode DGNodeLab -> Result (LNode DGNodeLab)
updateNodes :: AnyComorphism -> LNode DGNodeLab -> Result (LNode DGNodeLab)
updateNodes (Comorphism cidMor :: cid
cidMor) (node :: Node
node, dgNodeLab :: DGNodeLab
dgNodeLab) =
  case DGNodeLab -> G_theory
dgn_theory DGNodeLab
dgNodeLab of
    G_theory lid :: lid
lid _ esig :: ExtSign sign symbol
esig _ thSens :: ThSens sentence (AnyComorphism, BasicProof)
thSens _ -> do
      let slid :: lid1
slid = cid -> lid1
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 -> lid1
sourceLogic cid
cidMor
      ExtSign sign' :: sign1
sign' sys' :: Set symbol1
sys' <- lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid lid1
slid "DGTranslation.fTh.sign" ExtSign sign symbol
esig
      ThSens sentence1 (AnyComorphism, BasicProof)
thSens' <- lid
-> lid1
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Result (ThSens sentence1 (AnyComorphism, BasicProof))
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 :: * -> *) b.
(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, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid lid1
slid "DGTranslation.fTh.sen" ThSens sentence (AnyComorphism, BasicProof)
thSens
      (sign'' :: sign2
sign'', namedS :: [Named sentence2]
namedS) <- cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
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
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cidMor (sign1
sign', ThSens sentence1 (AnyComorphism, BasicProof) -> [Named sentence1]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence1 (AnyComorphism, BasicProof)
thSens')
      LNode DGNodeLab -> Result (LNode DGNodeLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node
node, DGNodeLab
dgNodeLab
        { dgn_nf :: Maybe Node
dgn_nf = Maybe Node
forall a. Maybe a
Nothing
        , dgn_sigma :: Maybe GMorphism
dgn_sigma = Maybe GMorphism
forall a. Maybe a
Nothing
        , dgn_theory :: G_theory
dgn_theory = lid2
-> Maybe IRI
-> ExtSign sign2 symbol2
-> SigId
-> ThSens sentence2 (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 (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
cidMor) Maybe IRI
forall a. Maybe a
Nothing
            (sign2 -> Set symbol2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign2
sign'' (Set symbol2 -> ExtSign sign2 symbol2)
-> Set symbol2 -> ExtSign sign2 symbol2
forall a b. (a -> b) -> a -> b
$ [Set symbol2] -> Set symbol2
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
            ([Set symbol2] -> Set symbol2) -> [Set symbol2] -> Set symbol2
forall a b. (a -> b) -> a -> b
$ (symbol1 -> Set symbol2) -> [symbol1] -> [Set symbol2]
forall a b. (a -> b) -> [a] -> [b]
map (cid -> sign1 -> symbol1 -> Set symbol2
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 -> sign1 -> symbol1 -> Set symbol2
map_symbol cid
cidMor sign1
sign') ([symbol1] -> [Set symbol2]) -> [symbol1] -> [Set symbol2]
forall a b. (a -> b) -> a -> b
$ Set symbol1 -> [symbol1]
forall a. Set a -> [a]
Set.toList Set symbol1
sys')
            SigId
startSigId ([Named sentence2] -> ThSens sentence2 (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
namedS) ThId
startThId })

showFromTo :: Node -> Node -> DGraph -> String
showFromTo :: Node -> Node -> DGraph -> String
showFromTo from :: Node
from to :: Node
to gc :: DGraph
gc =
    "from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> DGraph -> String
getNameOfNode Node
from DGraph
gc String -> String -> String
forall a. [a] -> [a] -> [a]
++ " to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> DGraph -> String
getNameOfNode Node
to DGraph
gc

{- | get the maximal sublogic of a graph.
 each DGraph and each node will be tested, in order to find
 the maximal sublogic of th Graph.
 All edges and nodes will be searched also in the meantime, so as to test,
 whether the GMorphism of edges is homogeneous, and the logics of nodes are
 equal. -}
getDGLogic :: LibEnv -> Result G_sublogics
getDGLogic :: LibEnv -> Result G_sublogics
getDGLogic libEnv :: LibEnv
libEnv =
    (LibName -> Result G_sublogics)
-> [LibName] -> Result [G_sublogics]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LibEnv -> LibName -> Result G_sublogics
getSublogicFromDGraph LibEnv
libEnv) (LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
libEnv)
    Result [G_sublogics]
-> ([G_sublogics] -> Result G_sublogics) -> Result G_sublogics
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [G_sublogics] -> Result G_sublogics
combineSublogics

getSublogicFromDGraph :: LibEnv -> LibName -> Result G_sublogics
getSublogicFromDGraph :: LibEnv -> LibName -> Result G_sublogics
getSublogicFromDGraph le :: LibEnv
le ln :: LibName
ln = do
    let gc :: DGraph
gc = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
        edgesList :: [LEdge DGLinkLab]
edgesList = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
gc
        nodesList :: [LNode DGNodeLab]
nodesList = DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
gc
    [G_sublogics]
slList1 <- (LEdge DGLinkLab -> Result G_sublogics)
-> [LEdge DGLinkLab] -> Result [G_sublogics]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM LEdge DGLinkLab -> Result G_sublogics
testAndGetSublogicFromEdge [LEdge DGLinkLab]
edgesList
    [G_sublogics]
slList2 <- (LNode DGNodeLab -> Result G_sublogics)
-> [LNode DGNodeLab] -> Result [G_sublogics]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (AnyLogic -> LNode DGNodeLab -> Result G_sublogics
getSubLogicsFromNodes (AnyLogic -> LNode DGNodeLab -> Result G_sublogics)
-> AnyLogic -> LNode DGNodeLab -> Result G_sublogics
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab] -> AnyLogic
getFirstLogic [LNode DGNodeLab]
nodesList)
                        [LNode DGNodeLab]
nodesList
    [G_sublogics] -> Result G_sublogics
combineSublogics ([G_sublogics] -> Result G_sublogics)
-> [G_sublogics] -> Result G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics]
slList1 [G_sublogics] -> [G_sublogics] -> [G_sublogics]
forall a. [a] -> [a] -> [a]
++ [G_sublogics]
slList2

combineSublogics :: [G_sublogics] -> Result G_sublogics
combineSublogics :: [G_sublogics] -> Result G_sublogics
combineSublogics l :: [G_sublogics]
l = case [G_sublogics]
l of
  [] -> String -> Result G_sublogics
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Static.DGTranslation.combineSublogics.empty"
  h :: G_sublogics
h : t :: [G_sublogics]
t -> case (G_sublogics -> Maybe G_sublogics -> Maybe G_sublogics)
-> Maybe G_sublogics -> [G_sublogics] -> Maybe G_sublogics
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ s :: G_sublogics
s ms :: Maybe G_sublogics
ms -> case Maybe G_sublogics
ms of
           Just u :: G_sublogics
u -> G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics G_sublogics
s G_sublogics
u
           _ -> Maybe G_sublogics
forall a. Maybe a
Nothing) (G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just G_sublogics
h) [G_sublogics]
t of
     Nothing -> String -> Result G_sublogics
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Static.DGTranslation.combineSublogics"
     Just s :: G_sublogics
s -> G_sublogics -> Result G_sublogics
forall (m :: * -> *) a. Monad m => a -> m a
return G_sublogics
s

testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Result G_sublogics
testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Result G_sublogics
testAndGetSublogicFromEdge l :: LEdge DGLinkLab
l@(_, _, lbl :: DGLinkLab
lbl) =
  case DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl of
    GMorphism cid' :: cid
cid' (ExtSign lsign :: sign1
lsign _) _ lmorphism :: morphism2
lmorphism _ -> do
      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'
      sign2
lsign' <- lid1 -> lid2 -> String -> sign1 -> Result sign2
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 -> m sign2
coercePlainSign (cid -> lid1
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 -> lid1
sourceLogic cid
cid') lid2
tlid
        (LEdge DGLinkLab -> String
showLEdge LEdge DGLinkLab
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not homogeneous.") sign1
lsign
      G_sublogics -> Result G_sublogics
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sublogics -> Result G_sublogics)
-> G_sublogics -> Result G_sublogics
forall a b. (a -> b) -> a -> b
$ lid2 -> sublogics2 -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid2
tlid (sublogics2 -> G_sublogics) -> sublogics2 -> G_sublogics
forall a b. (a -> b) -> a -> b
$ sublogics2 -> sublogics2 -> sublogics2
forall l. SemiLatticeWithTop l => l -> l -> l
lub (sign2 -> sublogics2
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic sign2
lsign' )
        (sublogics2 -> sublogics2) -> sublogics2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ morphism2 -> sublogics2
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic morphism2
lmorphism

getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab -> Result G_sublogics
getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab -> Result G_sublogics
getSubLogicsFromNodes logic :: AnyLogic
logic (_, lnode :: DGNodeLab
lnode) =
        case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lnode of
          th :: G_theory
th@(G_theory lid :: lid
lid _ _ _ _ _) ->
              if 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
lid AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== AnyLogic
logic then G_sublogics -> Result G_sublogics
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sublogics -> Result G_sublogics)
-> G_sublogics -> Result G_sublogics
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sublogics
sublogicOfTh G_theory
th
                 else String -> Result G_sublogics
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result G_sublogics) -> String -> Result G_sublogics
forall a b. (a -> b) -> a -> b
$ "the node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
lnode String -> String -> String
forall a. [a] -> [a] -> [a]
++
                               "  has a different logic \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid -> String
forall a. Show a => a -> String
show lid
lid String -> String -> String
forall a. [a] -> [a] -> [a]
++
                               "\" as the logic of Graph \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
logic String -> String -> String
forall a. [a] -> [a] -> [a]
++
                               " is not homogeneous."

getFirstLogic :: [LNode DGNodeLab] -> AnyLogic
getFirstLogic :: [LNode DGNodeLab] -> AnyLogic
getFirstLogic list :: [LNode DGNodeLab]
list = case [LNode DGNodeLab]
list of
  (_, nlab :: DGNodeLab
nlab) : _ -> case DGNodeLab -> G_theory
dgn_theory DGNodeLab
nlab of
          G_theory lid :: lid
lid _ _ _ _ _ -> 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
lid
  _ -> String -> AnyLogic
forall a. HasCallStack => String -> a
error "Static.DGTranslation.getFirstLogic"