{- |

Module : $Header$

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 ++ ".het"

g1 = globOrLocTh src

g2 = globOrLocTh tar

case g1 of

G_theory lid1 sig1 _ sens1 _ -> case g2 of

G_theory lid2 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 ++ " ="

, prettyGTheory Nothing g1

, text "end"

, text $ "spec target_" ++ nm ++ " = source_" ++ nm

, text "then %cons"

, prettyGTheory Nothing

$ G_theory lid2 (mkExtSign diffSig) startSigId sens startThId

]