{- |
Module      :  $Header$
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)

-- | translation of a LibEnv (a map of globalcontext)
libEnv_translation :: LibEnv -> AnyComorphism -> Result LibEnv
libEnv_translation libEnv com =
  foldM (\ le ln -> do
    dgTr <- dg_translation le (lookupDGraph ln libEnv) com
    return $ Map.insert ln dgTr le) Map.empty $ getTopsortedLibs libEnv

dg_translation :: LibEnv -> DGraph -> AnyComorphism -> Result DGraph
dg_translation le gc acm@(Comorphism cidMor) =
    let labNodesList = labNodesDG gc
        labEdgesList = labEdgesDG gc
    in addErrorDiag ("translation failed via: " ++ language_name cidMor) ()
       $ do
        resOfEdges <- mapM (updateEdges acm gc) labEdgesList
        resOfNodes <- mapM (updateNodes acm) labNodesList
        return $ computeDGraphTheories le
          $ mkGraphDG resOfNodes resOfEdges emptyDG

updateEdges :: AnyComorphism -> DGraph -> LEdge DGLinkLab
  -> Result (LEdge DGLinkLab)
updateEdges (Comorphism cidMor) gc (s, t, lbl) = case dgl_morphism lbl of
  GMorphism cid' esig _ mor _ ->
   if isIdComorphism (Comorphism cid')
   then do
     let slid = sourceLogic cidMor
         tlid = targetLogic cidMor
     ExtSign lsign sys <- coerceSign (sourceLogic cid') slid
       "DGTranslation.fSign" esig
     (lsign', _) <- map_sign cidMor lsign
     lMor <- coerceMorphism (targetLogic cid') slid "DGTranslation.fMor" mor
     lmorphism' <- map_morphism cidMor lMor
     return (s, t, lbl
       { dgl_morphism = GMorphism (mkIdComorphism tlid $ top_sublogic tlid)
         (ExtSign lsign' $ Set.unions
         $ map (map_symbol cidMor lsign) $ Set.toList sys)
         startSigId lmorphism' startMorId })
   else fail $ "Link " ++ showFromTo s t gc ++ " is not homogeneous."

updateNodes :: AnyComorphism -> LNode DGNodeLab -> Result (LNode DGNodeLab)
updateNodes (Comorphism cidMor) (node, dgNodeLab) =
  case dgn_theory dgNodeLab of
    G_theory lid _ esig _ thSens _ -> do
      let slid = sourceLogic cidMor
      ExtSign sign' sys' <- coerceSign lid slid "DGTranslation.fTh.sign" esig
      thSens' <- coerceThSens lid slid "DGTranslation.fTh.sen" thSens
      (sign'', namedS) <- wrapMapTheory cidMor (sign', toNamedList thSens')
      return (node, dgNodeLab
        { dgn_nf = Nothing
        , dgn_sigma = Nothing
        , dgn_theory = G_theory (targetLogic cidMor) Nothing
            (ExtSign sign'' $ Set.unions
            $ map (map_symbol cidMor sign') $ Set.toList sys')
            startSigId (toThSens namedS) startThId })

showFromTo :: Node -> Node -> DGraph -> String
showFromTo from to gc =
    "from " ++ getNameOfNode from gc ++ " to " ++ getNameOfNode to 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 =
    mapM (getSublogicFromDGraph libEnv) (Map.keys libEnv)
    >>= combineSublogics

getSublogicFromDGraph :: LibEnv -> LibName -> Result G_sublogics
getSublogicFromDGraph le ln = do
    let gc = lookupDGraph ln le
        edgesList = labEdgesDG gc
        nodesList = labNodesDG gc
    slList1 <- mapM testAndGetSublogicFromEdge edgesList
    slList2 <- mapM (getSubLogicsFromNodes $ getFirstLogic nodesList)
                        nodesList
    combineSublogics $ slList1 ++ slList2

combineSublogics :: [G_sublogics] -> Result G_sublogics
combineSublogics l = case l of
  [] -> fail "Static.DGTranslation.combineSublogics.empty"
  h : t -> case foldr (\ s ms -> case ms of
           Just u -> joinSublogics s u
           _ -> Nothing) (Just h) t of
     Nothing -> fail "Static.DGTranslation.combineSublogics"
     Just s -> return s

testAndGetSublogicFromEdge :: LEdge DGLinkLab -> Result G_sublogics
testAndGetSublogicFromEdge l@(_, _, lbl) =
  case dgl_morphism lbl of
    GMorphism cid' (ExtSign lsign _) _ lmorphism _ -> do
      let tlid = targetLogic cid'
      lsign' <- coercePlainSign (sourceLogic cid') tlid
        (showLEdge l ++ " is not homogeneous.") lsign
      return $ G_sublogics tlid $ lub (minSublogic lsign' )
        $ minSublogic lmorphism

getSubLogicsFromNodes :: AnyLogic -> LNode DGNodeLab -> Result G_sublogics
getSubLogicsFromNodes logic (_, lnode) =
        case dgn_theory lnode of
          th@(G_theory lid _ _ _ _ _) ->
              if Logic lid == logic then return $ sublogicOfTh th
                 else fail $ "the node " ++ getDGNodeName lnode ++
                               "  has a different logic \"" ++ show lid ++
                               "\" as the logic of Graph \"" ++ show logic ++
                               " is not homogeneous."

getFirstLogic :: [LNode DGNodeLab] -> AnyLogic
getFirstLogic list = case list of
  (_, nlab) : _ -> case dgn_theory nlab of
          G_theory lid _ _ _ _ _ -> Logic lid
  _ -> error "Static.DGTranslation.getFirstLogic"
