{- |
Module      :  $Header$
Description :  xml input for Hets development graphs
Copyright   :  (c) Simon Ulbricht, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (DevGraph)

create new or extend a Development Graph in accordance with an XML input
-}

module Static.FromXml where

import Static.ComputeTheory (computeLibEnvTheories)
import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.FromXmlUtils
import Static.XGraph

import Common.LibName
import Common.Result (Result (..))
import Common.ResultT
import Common.XmlParser

import Comorphisms.LogicGraph (logicGraph)

import Control.Monad.Trans (lift)
import Control.Monad (foldM, unless)

import qualified Data.Graph.Inductive.Graph as Graph (Node)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Driver.Options
import Driver.ReadFn (findFileOfLibNameAux)

import Logic.ExtSign (ext_empty_signature)
import Logic.Grothendieck
import Logic.Logic (AnyLogic (..), cod, composeMorphisms)
import Logic.Prover (noSens)

import Text.XML.Light (Element)

-- | top-level function
readDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
readDGXml opts path = do
    Result ds res <- runResultT $ readDGXmlR opts path Map.empty
    showDiags opts ds
    return res

{- | main function; receives a FilePath and calls fromXml upon that path,
using an initial LogicGraph. -}
readDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
readDGXmlR opts path lv = do
  lift $ putIfVerbose opts 2 $ "Reading " ++ path
  xml' <- lift $ readXmlFile path
  res <- lift $ parseXml xml'
  case res of
    Right xml -> rebuiltDgXml opts lv xml
    Left err -> fail $ "failed to parse XML file: " ++ path ++ "\n" ++ err

-- | call rebuiltDG with only a LibEnv and an Xml-Element
rebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)
rebuiltDgXml opts lv xml = do
      xg <- liftR $ xGraph xml
      res <- rebuiltDG opts logicGraph xg lv
      let ln = libName xg
      return (ln, computeLibEnvTheories $ uncurry (Map.insert ln) res)

{- | reconstructs the Development Graph via a previously created XGraph-
structure. -}
rebuiltDG :: HetcatsOpts -> LogicGraph -> XGraph -> LibEnv
          -> ResultT IO (DGraph, LibEnv)
rebuiltDG opts lg (XGraph _ ga i thmLk nds body) lv = do
  (dg, lv') <- rebuiltBody body lv
  dg' <- insertThmLinks lg dg $ mkEdgeMap thmLk
  return (dg', lv') where
    rebuiltBody bd lv' = case bd of
        [] ->
          foldM (flip $ insertFirstNode opts lg)
            (emptyDG { globalAnnos = ga, getNewEdgeId = i }, lv') nds
        bs : bd' -> do
          res0 <- rebuiltBody bd' lv'
          foldM (\ dl (lKs, nd) ->
            insertStep opts lg nd lKs dl)
            res0 bs

-- | inserts a new node as well as all definition links pointing at that node
insertStep :: HetcatsOpts -> LogicGraph -> XNode -> [XLink] -> (DGraph, LibEnv)
           -> ResultT IO (DGraph, LibEnv)
insertStep opts lg xNd lks (dg, lv) = do
  mrs <- mapM (getTypeAndMorphism lg dg) lks
  G_sign lid sg sId <- getSigForXNode lg dg mrs
  let j = getNewNodeDG dg
  (gt2, dg', lv') <-
    insertNode opts lg (Just $ noSensGTheory lid sg sId) xNd j (dg, lv)
  dg'' <- foldM (insertLink lg j (signOf gt2)) dg' mrs
  return (dg'', lv')

insertLink :: LogicGraph -> Graph.Node -> G_sign -> DGraph
            -> (Graph.Node, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph
insertLink lg j gs dg (i, mr, tp, lk) = do
            lkLab <- finalizeLink lg lk mr gs tp
            return $ insEdgeAsIs (i, j, lkLab) dg

-- | inserts theorem links
insertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph
insertThmLinks lg p = foldM (\ dg (tgt, sm) -> do
  (j, gsig) <- signOfNode tgt dg
  insertTarThmLinks lg j gsig dg sm) p . Map.toList

insertTarThmLinks :: LogicGraph -> Graph.Node -> G_sign
  -> DGraph -> Map.Map String [XLink] -> ResultT IO DGraph
insertTarThmLinks lg j tgt p = foldM (\ dg (src, ls) -> do
  (i, gsig) <- signOfNode src dg
  foldM (\ dg' xLk -> do
      (mr, tp) <- getTypeAndMorphism1 lg dg gsig xLk
      insertLink lg j tgt dg' (i, mr, tp, xLk)) dg ls) p . Map.toList

{- | given a links intermediate morphism and its target nodes signature,
this function calculates the final morphism for this link -}
finalizeLink :: LogicGraph -> XLink -> GMorphism -> G_sign -> DGLinkType
             -> ResultT IO DGLinkLab
finalizeLink lg xLk mr sg tp = do
  mr' <- liftR $ case edgeTypeModInc $ lType xLk of
    HidingDef -> ginclusion lg sg (cod mr)
    _ -> do
      mr1 <- ginclusion lg (cod mr) sg
      composeMorphisms mr mr1
  return $ defDGLinkId mr' tp SeeTarget $ edgeId xLk

{- | based upon the morphisms of ingoing deflinks, calculate the initial
signature to be used for node insertion -}
getSigForXNode :: LogicGraph -> DGraph
               -> [(Graph.Node, GMorphism, DGLinkType, XLink)]
               -> ResultT IO G_sign
getSigForXNode lg dg mrs = case mrs of
    [] -> fail "insertStep: empty link list"
    (_, _, FreeOrCofreeDefLink _ _, xLk) : rt -> do
        unless (null rt)
          $ fail "unexpected non-singleton free or cofree def link"
        fmap snd $ signOfNode (source xLk) dg
    _ -> liftR $ gsigManyUnion lg $ map (\ (_, m, _, _) -> cod m) mrs

-- | gathers information for an XLink using its source nodes signature
getTypeAndMorphism :: LogicGraph -> DGraph -> XLink
                   -> ResultT IO (Graph.Node, GMorphism, DGLinkType, XLink)
getTypeAndMorphism lg dg xLk = do
  (i, sg1) <- signOfNode (source xLk) dg
  (mr', lTp) <- getTypeAndMorphism1 lg dg sg1 xLk
  return (i, mr', lTp, xLk)

getTypeAndMorphism1 :: LogicGraph -> DGraph -> G_sign -> XLink
  -> ResultT IO (GMorphism, DGLinkType)
getTypeAndMorphism1 lg dg sg1 xLk = do
    (sg2, lTp) <- getTypeAndMorAux lg dg sg1 xLk
    mr' <- liftR $ getGMorphism lg sg2 (mr_name xLk) (mapping xLk)
    return (mr', lTp)

{- depending on the type of the link, the correct DGLinkType and the signature
for the (external) morphism are extracted here -}
getTypeAndMorAux :: LogicGraph -> DGraph -> G_sign -> XLink
                 -> ResultT IO (G_sign, DGLinkType)
getTypeAndMorAux lg dg sg@(G_sign slid _ _) xLk = let
  emptySig = G_sign slid (ext_empty_signature slid) startSigId
  mkRtVAL sg' tp = return (sg', tp)
  cc = cons xLk
  in case edgeTypeModInc $ lType xLk of
    HidingDef -> mkRtVAL sg HidingDefLink
    GlobalDef -> mkRtVAL sg $ localOrGlobalDef Global cc
    HetDef -> mkRtVAL sg $ localOrGlobalDef Global cc
    LocalDef -> mkRtVAL sg $ localOrGlobalDef Local cc
    FreeOrCofreeDef fc -> do
      (sg', mNd) <- case mr_source xLk of
        Nothing -> return (emptySig, EmptyNode $ Logic slid)
        Just ms -> do
          (j, sg') <- signOfNode ms dg
          return (sg', JustNode $ NodeSig j sg')
      mkRtVAL sg' $ FreeOrCofreeDefLink fc mNd
    ThmType thTp prv _ _ -> let
      lStat = if not prv then LeftOpen
          else Proven (rule xLk) $ prBasis xLk in
      case thTp of
        HidingThm -> do
          (i', sg') <- case mr_source xLk of
            Just ms -> signOfNode ms dg
            Nothing -> fail "no morphism source declaration for HidingThmLink"
          mr' <- liftR $ ginclusion lg sg' sg
          mkRtVAL sg' $ HidingFreeOrCofreeThm Nothing i' mr' lStat
        FreeOrCofreeThm fc -> do
            (i', sg') <- case mr_source xLk of
              Just ms -> signOfNode ms dg
              Nothing -> return (-1, emptySig)
            mr' <- liftR $ ginclusion lg sg' sg
            mkRtVAL sg' $ HidingFreeOrCofreeThm (Just fc) i' mr' lStat
        GlobalOrLocalThm sc _ -> mkRtVAL sg
          $ ScopedLink sc (ThmLink lStat) $ mkConsStatus cc

{- | Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element
and the the DGraphs Global Annotations. The caller has to ensure that the
chosen nodeId is not used in dgraph. -}
insertNode :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> Graph.Node
  -> (DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)
insertNode opts lg mGt xNd n (dg, lv) = do
  (lbl, lv') <- generateNodeLab opts lg mGt xNd (dg, lv)
  return (dgn_theory lbl, insNodeDG (n, lbl) dg, lv')

{- | generate nodelab with startoff-gtheory and xnode information (a new libenv
is returned in case it was extended due to reference node insertion) -}
generateNodeLab :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode
  -> (DGraph, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)
generateNodeLab opts lg mGt xNd (dg, lv) = case xNd of
  -- Case #1: Reference Node
  XRef nm rfNd rfLb spc -> do
          (dg', lv') <- case Map.lookup (emptyLibName rfLb) lv of
            Just dg' -> return (dg', lv)
            Nothing -> loadRefLib opts rfLb lv
          (i, gt) <- case lookupUniqueNodeByName rfNd dg' of
              Just (i, lbl) -> case signOf $ dgn_theory lbl of
                G_sign lid sign sId -> return (i, noSensGTheory lid sign sId)
              Nothing -> fail $ "reference node " ++ rfNd ++ " was not found"
          (gt', _) <- parseSpecs gt nm dg spc
          let nInf = newRefInfo (emptyLibName rfLb) i
          return (newInfoNodeLab nm nInf gt', lv')
  -- Case #2: Regular Node
  XNode nm lN (hid, syb) spc cc -> do
        -- StartOff-Theory. Taken from LogicGraph for initial Nodes
        gt0 <- case mGt of
          Nothing -> fmap emptyTheory $ lookupLogic "generateNodeLab " lN lg
          Just gt -> return gt
        -- hidden symbols use a different parser
        gt1 <- if hid then parseHidden gt0 syb
                 else fmap fst $ parseSpecs gt0 nm dg syb
        (gt2, syb') <- parseSpecs gt1 nm dg spc
        -- the DGOrigin is also different for nodes with hidden symbols
        lOrig <- if hid then let
                syms = Set.difference (symsOfGsign $ signOf gt0)
                  $ symsOfGsign $ signOf gt2
                in return $ DGRestriction NoRestriction syms
          else do
            diffSig <- liftR $ homGsigDiff (signOf gt2) $ signOf gt0
            return $ DGBasicSpec Nothing diffSig syb'
        return (newInfoNodeLab nm (newConsNodeInfo lOrig cc) gt2, lv)

insertFirstNode :: HetcatsOpts -> LogicGraph -> XNode -> (DGraph, LibEnv)
  -> ResultT IO (DGraph, LibEnv)
insertFirstNode opts lg xNd p@(dg', _) = let n = getNewNodeDG dg' in do
  (_, dg, lv) <- insertNode opts lg Nothing xNd n p
  return (dg, lv)

parseHidden :: G_theory -> String -> ResultT IO G_theory
parseHidden gt s' = do
  gs <- liftR $ deleteHiddenSymbols s' $ signOf gt
  return $ case gs of
    G_sign lid sg sId -> noSensGTheory lid sg sId

parseSpecs :: G_theory -> NodeName -> DGraph -> String
           -> ResultT IO (G_theory, Set G_symbol)
parseSpecs gt' nm dg spec = let
          (response, msg) = extendByBasicSpec (globalAnnos dg) spec gt'
          in case response of
            Success gt'' _ smbs _ -> return (gt'', smbs)
            Failure _ -> fail $ "[ " ++ showName nm ++ " ]\n" ++ msg

loadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)
loadRefLib opts ln lv = do
          mPath <- lift $ findFileOfLibNameAux opts { intype = DgXml } ln
          case mPath of
            Just path -> do
              (ln', lv') <- readDGXmlR opts path lv
              return (lookupDGraph ln' lv', lv')
            _ -> fail $ "no file exists for reference library " ++ ln

-- | creates an entirely empty theory
emptyTheory :: AnyLogic -> G_theory
emptyTheory (Logic lid) =
  G_theory lid Nothing (ext_empty_signature lid) startSigId noSens startThId

{- | A Node is looked up via its name in the DGraph. Returns the nodes
signature, but only if one single node is found for the respective name.
Otherwise an error is thrown. -}
signOfNode :: String -> DGraph -> ResultT IO (Graph.Node, G_sign)
signOfNode nd dg = case lookupUniqueNodeByName nd dg of
  Nothing -> fail $ "required node [" ++ nd ++ "] was not found in DGraph!"
  Just (j, lbl) ->
    return (j, signOf (dgn_theory lbl))
