{- |
Module      :  ./Static/ConsInclusions.hs
Description :  dump conservative inclusion links
Copyright   :  (c) C. Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via imports)

-}
module Static.ConsInclusions (dumpConsInclusions) where

import Static.DevGraph
import Static.DgUtils
import Static.GTheory

import Driver.Options
import Driver.WriteFn

import Logic.Coerce
import Logic.Grothendieck
import Logic.Logic

import Common.Consistency
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.Result
import qualified Common.OrderedMap as OMap

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Set as Set

dumpConsInclusions :: HetcatsOpts -> DGraph -> IO ()
dumpConsInclusions :: HetcatsOpts -> DGraph -> IO ()
dumpConsInclusions opts :: HetcatsOpts
opts dg :: DGraph
dg =
  (LEdge DGLinkLab -> IO ()) -> [LEdge DGLinkLab] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HetcatsOpts -> DGraph -> LEdge DGLinkLab -> IO ()
dumpConsIncl HetcatsOpts
opts DGraph
dg)
  ([LEdge DGLinkLab] -> IO ()) -> [LEdge DGLinkLab] -> IO ()
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> let e :: DGEdgeType
e = DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
l in
               DGEdgeType -> Bool
isInc DGEdgeType
e Bool -> Bool -> Bool
&& DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
forall a. Eq a => a -> a -> Bool
== DGEdgeTypeModInc
GlobalDef
           Bool -> Bool -> Bool
&& DGLinkType -> Conservativity
getCons (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l) Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
Cons
           )
  ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg

dumpConsIncl :: HetcatsOpts -> DGraph -> LEdge DGLinkLab -> IO ()
dumpConsIncl :: HetcatsOpts -> DGraph -> LEdge DGLinkLab -> IO ()
dumpConsIncl opts :: HetcatsOpts
opts dg :: DGraph
dg (s :: Node
s, t :: Node
t, l :: DGLinkLab
l) = do
   let src :: DGNodeLab
src = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
s
       tar :: DGNodeLab
tar = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
t
       ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg
       nm :: String
nm = EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
l)
       file :: String
file = "ConsIncl_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".dol"
       g1 :: G_theory
g1 = DGNodeLab -> G_theory
globOrLocTh DGNodeLab
src
       g2 :: G_theory
g2 = DGNodeLab -> G_theory
globOrLocTh DGNodeLab
tar
   case G_theory
g1 of
     G_theory lid1 :: lid
lid1 _ sig1 :: ExtSign sign symbol
sig1 _ sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _ -> case G_theory
g2 of
       G_theory lid2 :: lid
lid2 syn :: Maybe IRI
syn sig2 :: ExtSign sign symbol
sig2 _ sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 _ -> do
           ExtSign sign symbol
insig <- lid
-> lid -> String -> ExtSign sign symbol -> IO (ExtSign sign symbol)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid1 lid
lid2 "dumpConsIncl1" ExtSign sign symbol
sig1
           ThSens sentence (AnyComorphism, BasicProof)
inSens <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (ThSens sentence (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
lid1 lid
lid2 "dumpConsIncl2" ThSens sentence (AnyComorphism, BasicProof)
sens1
           let pSig2 :: sign
pSig2 = ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sig2
               diffSig :: sign
diffSig = String -> Result sign -> sign
forall a. String -> Result a -> a
propagateErrors "dumpConsIncl3"
                  (Result sign -> sign) -> Result sign -> sign
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signatureDiff lid
lid2 sign
pSig2 (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
insig)
               inSensSet :: Set (SenStatus sentence (AnyComorphism, BasicProof))
inSensSet = [SenStatus sentence (AnyComorphism, BasicProof)]
-> Set (SenStatus sentence (AnyComorphism, BasicProof))
forall a. Ord a => [a] -> Set a
Set.fromList ([SenStatus sentence (AnyComorphism, BasicProof)]
 -> Set (SenStatus sentence (AnyComorphism, BasicProof)))
-> [SenStatus sentence (AnyComorphism, BasicProof)]
-> Set (SenStatus sentence (AnyComorphism, BasicProof))
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [SenStatus sentence (AnyComorphism, BasicProof)]
forall k a. Ord k => OMap k a -> [a]
OMap.elems ThSens sentence (AnyComorphism, BasicProof)
inSens
               sens :: ThSens sentence (AnyComorphism, BasicProof)
sens = (SenStatus sentence (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 (SenStatus sentence (AnyComorphism, BasicProof)
-> Set (SenStatus sentence (AnyComorphism, BasicProof)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (SenStatus sentence (AnyComorphism, BasicProof))
inSensSet) ThSens sentence (AnyComorphism, BasicProof)
sens2
           HetcatsOpts -> String -> String -> IO ()
writeVerbFile HetcatsOpts
opts String
file
             (String -> IO ()) -> String -> IO ()
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
$ GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
             [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "spec source_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ="
             , G_theory -> Doc
forall a. Pretty a => a -> Doc
pretty G_theory
g1
             , String -> Doc
text "end\n"
             , String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "spec target_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = source_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
             , String -> Doc
text "then %cons"
             , G_theory -> Doc
forall a. Pretty a => a -> Doc
pretty
               (G_theory -> Doc) -> G_theory -> Doc
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid2 Maybe IRI
syn (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
diffSig) SigId
startSigId ThSens sentence (AnyComorphism, BasicProof)
sens ThId
startThId
             ]