content: {- |
  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 opts dg =
    mapM_ (dumpConsIncl opts dg)
    $ filter (\ (_, _, l) -> let e = getRealDGLinkType l in
                 isInc e && edgeTypeModInc e == GlobalDef
             && getCons (dgl_type l) == Cons
             )
    $ labEdgesDG dg
  
  dumpConsIncl :: HetcatsOpts -> DGraph -> LEdge DGLinkLab -> IO ()
  dumpConsIncl opts dg (s, t, l) = do
     let src = labDG dg s
         tar = labDG dg t
         ga = globalAnnos dg
         nm = showEdgeId (dgl_id l)
         file = "ConsIncl_" ++ nm ++ ".dol"
         g1 = globOrLocTh src
         g2 = globOrLocTh tar
     case g1 of
       G_theory lid1 _ sig1 _ sens1 _ -> case g2 of
         G_theory lid2 syn sig2 _ sens2 _ -> do
             insig <- coerceSign lid1 lid2 "dumpConsIncl1" sig1
             inSens <- coerceThSens lid1 lid2 "dumpConsIncl2" sens1
             let pSig2 = plainSign sig2
                 diffSig = propagateErrors "dumpConsIncl3"
                    $ signatureDiff lid2 pSig2 (plainSign insig)
                 inSensSet = Set.fromList $ OMap.elems inSens
                 sens = OMap.filter (`Set.notMember` inSensSet) sens2
             writeVerbFile opts file
               $ show $ useGlobalAnnos ga $ vcat
               [ text $ "spec source_" ++ nm ++ " ="
               , pretty g1
               , text "end\n"
               , text $ "spec target_" ++ nm ++ " = source_" ++ nm
               , text "then %cons"
               , pretty
                 $ G_theory lid2 syn (mkExtSign diffSig) startSigId sens startThId
               ]
  