{- |
Module      :  $Header$
Description :  compute the normal forms of all nodes in development graphs
Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

compute normal forms
-}

module Proofs.NormalForm
    ( normalFormLibEnv
    , normalForm
    , normalFormRule
    ) where

import Logic.Logic
import Logic.Grothendieck

import Static.ComputeTheory
import Static.GTheory
import Static.DgUtils
import Static.DevGraph
import Static.History
import Static.WACocone

import Proofs.ComputeColimit

import Common.Consistency
import Common.Id
import Common.LibName
import Common.Result
import Common.Lib.Graph
import Common.Utils (nubOrd)

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import Control.Monad

normalFormRule :: DGRule
normalFormRule = DGRule "NormalForm"

-- | compute normal form for a library and imported libs
normalForm :: LibName -> LibEnv -> Result LibEnv
normalForm ln le = normalFormLNS (dependentLibs ln le) le

-- | compute norm form for all libraries
normalFormLibEnv :: LibEnv -> Result LibEnv
normalFormLibEnv le = normalFormLNS (getTopsortedLibs le) le

normalFormLNS :: [LibName] -> LibEnv -> Result LibEnv
normalFormLNS lns libEnv = foldM (\ le ln -> do
  let dg = lookupDGraph ln le
  newDg <- normalFormDG le dg
  return $ Map.insert ln
    (groupHistory dg normalFormRule newDg) le)
  libEnv lns

normalFormDG :: LibEnv -> DGraph -> Result DGraph
normalFormDG libEnv dgraph = foldM (\ dg (node, nodelab) ->
  if labelHasHiding nodelab then case dgn_nf nodelab of
    Just _ -> return dg -- already computed
    Nothing -> if isDGRef nodelab then do
        {- the normal form of the node
        is a reference to the normal form of the node it references
        careful: here not refNf, but a new Node which references refN -}
       let refLib = dgn_libname nodelab
           refNode = dgn_node nodelab
           refGraph' = lookupDGraph refLib libEnv
           refLabel = labDG refGraph' refNode
       case dgn_nf refLabel of
         Nothing -> warning dg
           (getDGNodeName refLabel ++ " (node " ++ show refNode
            ++ ") from '" ++ show (getLibId refLib)
            ++ "' without normal form") nullRange
         Just refNf -> do
           let refNodelab = labDG refGraph' refNf
               -- the label of the normal form ^
               nfNode = getNewNodeDG dg
               -- the new reference node in the old graph ^
               refLab = refNodelab
                 { dgn_name = extName "NormalForm" $ dgn_name nodelab
                 , dgn_nf = Just nfNode
                 , dgn_sigma = Just $ ide $ dgn_sign refNodelab
                 , nodeInfo = newRefInfo refLib refNf
                 , dgn_lock = Nothing }
               newLab = nodelab
                 { dgn_nf = Just nfNode,
                   dgn_sigma = dgn_sigma refLabel }
               chLab = SetNodeLab nodelab (node, newLab)
               changes = [InsertNode (nfNode, refLab), chLab]
               newGraph = changesDGH dgraph changes
           return newGraph
      else do
        let gd = insNode (node, dgn_theory nodelab) empty
            g0 = Map.fromList [(node, node)]
            (diagram, g) = computeDiagram dg [node] (gd, g0)
            fsub = finalSubcateg diagram
            Result ds res = gWeaklyAmalgamableCocone fsub
            es = map (\ d -> if isErrorDiag d then d { diagKind = Warning }
                             else d) ds
        appendDiags es
        case res of
          Nothing -> warning dg
                ("cocone failure for " ++ getDGNodeName nodelab
                 ++ " (node " ++ shows node ")") nullRange
          Just (sign, mmap) -> do
            {- we don't know that node is in fsub
            if it's not, we have to find a tip accessible from node
            and dgn_sigma = edgeLabel(node, tip); mmap (g Map.! tip) -}
            morNode <- if node `elem` nodes fsub then let
                        gn = Map.findWithDefault (error "gn") node g
                        phi = Map.findWithDefault (error "mor") gn mmap
                       in return phi else let
                          leaves = filter (\ x -> outdeg fsub x == 0) $
                                     nodes fsub
                          paths = map (\ x ->
                                       (x, propagateErrors "normalFormDG"
                                             $ dijkstra diagram node x))
                                      $ filter (\ x -> node `elem` subgraph
                                                      diagram x) leaves
                                          in
                            case paths of
                             [] -> fail "node should reach a tip"
                             (xn, xf) : _ -> comp xf $ mmap Map.! xn
            let nfNode = getNewNodeDG dg -- new node for normal form
                info = nodeInfo nodelab
                ConsStatus c cp pr = node_cons_status info
                nfLabel = newInfoNodeLab
                  (extName "NormalForm" $ dgn_name nodelab)
                  info
                  { node_origin = DGNormalForm node
                  , node_cons_status = mkConsStatus c }
                  sign
                newLab = nodelab -- the new label for node
                     { dgn_nf = Just nfNode
                     , dgn_sigma = Just morNode
                     , nodeInfo = info
                         { node_cons_status = ConsStatus None cp pr }
                     }
            -- add the nf to the label of node
                chLab = SetNodeLab nodelab (node, newLab)
            -- insert the new node and add edges from the predecessors
                insNNF = InsertNode (nfNode, nfLabel)
                makeEdge src tgt m = (src, tgt, globDefLink m DGLinkProof)
                insStrMor = map (\ (x, f) -> InsertEdge $ makeEdge x nfNode f)
                  $ nubOrd $ map (\ (x, y) -> (g Map.! x, y))
                  $ (node, morNode) : Map.toList mmap
                allChanges = insNNF : chLab : insStrMor
                newDG = changesDGH dg allChanges
            return $ changeDGH newDG $ SetNodeLab nfLabel (nfNode, nfLabel
              { globalTheory = computeLabelTheory libEnv newDG
                (nfNode, nfLabel) })
  else return dg) dgraph $ topsortedNodes dgraph -- only change relevant nodes

{- | computes the diagram associated to a node N in a development graph,
   adding common origins for multiple occurences of nodes, whenever
   needed
-}
computeDiagram :: DGraph -> [Node] -> (GDiagram, Map.Map Node Node)
               -> (GDiagram, Map.Map Node Node)
  -- as described in the paper for now
computeDiagram dgraph nodeList (gd, g) =
 case nodeList of
  [] -> (gd, g)
  _ ->
   let -- defInEdges is list of pairs (n, edges of target g(n))
       defInEdges = map (\ n -> (n, filter (\ e@(s, t, _) -> s /= t &&
                         liftE (liftOr isGlobalDef isHidingDef) e) $
                        innDG dgraph $ g Map.! n)) nodeList
       {- TO DO: no local links, and why edges with s=t are removed
       add normal form nodes
       sources of each edge must be added as new nodes -}
       nodeIds = zip (newNodes (length $ concatMap snd defInEdges) gd)
                     $ concatMap (\ (n, l) -> map (\ x -> (n, x)) l ) defInEdges
       newLNodes = zip (map fst nodeIds) $
                   map (\ (s, _, _) -> dgn_theory $ labDG dgraph s) $
                   concatMap snd defInEdges
       g0 = Map.fromList $
                     map (\ (newS, (_newT, (s, _t, _))) -> (newS, s)) nodeIds
       morphEdge (n1, (n2, (_, _, el))) =
         if isHidingDef $ dgl_type el
            then (n2, n1, (x, dgl_morphism el))
            else (n1, n2, (x, dgl_morphism el))
         where EdgeId x = dgl_id el
       newLEdges = map morphEdge nodeIds
       gd' = insEdges newLEdges $ insNodes newLNodes gd
       g' = Map.union g g0
   in computeDiagram dgraph (map fst nodeIds) (gd', g')

finalSubcateg :: GDiagram -> GDiagram
finalSubcateg graph = let
    leaves = filter (\ (n, _) -> outdeg graph n == 0) $ labNodes graph
 in buildGraph graph (map fst leaves) leaves [] $ nodes graph

subgraph :: Gr a b -> Node -> [Node]
subgraph graph node = let
   descs nList descList =
    case nList of
      [] -> descList
      _ -> let
             newDescs = concatMap (pre graph) nList
             nList' = filter (`notElem` nList) newDescs
             descList' = nubOrd $ descList ++ newDescs
           in descs nList' descList'
 in descs [node] []

buildGraph :: GDiagram -> [Node]
           -> [LNode G_theory]
           -> [LEdge (Int, GMorphism)]
           -> [Node]
           -> GDiagram
buildGraph oGraph leaves nList eList nodeList =
 case nodeList of
  [] -> mkGraph nList eList
  n : nodeList' ->
     case outdeg oGraph n of
      1 -> buildGraph oGraph leaves nList eList nodeList'
       -- the node is simply removed
      0 -> buildGraph oGraph leaves nList eList nodeList'
       -- the leaves have already been added to nList
      _ -> let
            Just l = lab oGraph n
            nList' = (n, l) : nList
            accesLeaves = filter (\ x -> n `elem` subgraph oGraph x) leaves
            eList' = map (\ x -> (n, x, (1 :: Int,
                       propagateErrors "buildGraph" $ dijkstra oGraph n x)))
                       accesLeaves
           in buildGraph oGraph leaves nList' (eList ++ eList') nodeList'
       -- branch, must add n to the nList and edges in eList
