content: {- |
  Module      :  ./Proofs/Freeness.hs
  Description :  normalization of freeness
  Copyright   :  (c) Mihai Codescu, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Mihai.Codescu@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  compute normal forms
  -}
  
  module Proofs.Freeness
      ( freeness
      ) where
  
  import Logic.Logic
  import Logic.Grothendieck
  import Logic.Coerce
  import Logic.Comorphism
  import Logic.Prover (toNamedList, toThSens)
  import Logic.ExtSign
  
  import Static.ComputeTheory
  import Static.GTheory
  import Static.DevGraph
  import Static.DgUtils
  import Static.History
  
  import Common.ExtSign
  import Common.LibName
  import Common.Result
  
  import Data.Graph.Inductive.Graph as Graph
  import qualified Data.Map as Map
  import Control.Monad
  
  import Data.List (nub)
  import Data.Maybe (fromMaybe)
  import Common.Lib.Graph
  
  freenessRule :: DGRule
  freenessRule = DGRule "Freeness"
  
  freeness :: LibName -> LibEnv -> Result LibEnv
  freeness ln le = do
    let dg = lookupDGraph ln le
    newDg <- freenessDG le ln dg
    return $ Map.insert ln
      (groupHistory dg freenessRule newDg) le
  
  freenessDG :: LibEnv -> LibName -> DGraph -> Result DGraph
  freenessDG le ln dgraph = foldM (handleEdge le ln) dgraph $ labEdgesDG dgraph
  
  handleEdge :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> Result DGraph
  handleEdge libEnv ln dg edge@(m, n, x) =
      case dgl_type x of
       FreeOrCofreeDefLink _ _ -> do
        let phi = dgl_morphism x
            mlab = labDG dg m
            gth = fromMaybe (dgn_theory $ labDG dg m) $ globalTheory mlab
        case gth of
         G_theory lid syn sig _ sen _ ->
          case phi of
           GMorphism cid _ _ mor1 _ -> do
            mor <- coerceMorphism (targetLogic cid) lid "free" mor1
            let res = quotient_term_algebra lid mor $ toNamedList sen
            case maybeResult res of
             Just (sigK, axK) -> do
                 -- success in logic lid
              let thK = G_theory lid syn (makeExtSign lid sigK)
                               startSigId (toThSens axK) startThId
              incl <- subsig_inclusion lid (plainSign sig) sigK
              let inclM = gEmbed $ mkG_morphism lid incl
        {- remove x
        add nodes
        k  with signature = sigK, sentences axK
        global def link from m to k, labeled with inclusion
        hiding def link from k to n, labeled with inclusion
                m' = getNewNodeDG dg -- new node -}
                  nodelab = labDG dg m
                  info = nodeInfo nodelab
                  ConsStatus c _ _ = node_cons_status info
                  k = getNewNodeDG dg
                  labelK = newInfoNodeLab
                     (extName "Freeness" $ dgn_name nodelab)
                     info
                     { node_origin = DGNormalForm m
                    , node_cons_status = mkConsStatus c }
                    thK
                  insK = InsertNode (k, labelK)
                  insE = [ InsertEdge (m, k, globDefLink inclM DGLinkProof)
                         , InsertEdge (k, n, defDGLink inclM HidingDefLink
                                        DGLinkProof)]
                  del = DeleteEdge edge
                  allChanges = del : insK : insE
                  newDG = changesDGH dg allChanges
                  labelN = labDG dg n
                  succs = map (\ y -> (y, labDG dg y)) $ descs (dgBody dg) n
                  labCh = [SetNodeLab labelK (k, labelK
                            { globalTheory = computeLabelTheory libEnv ln newDG
                                 (k, labelK) }),
                           SetNodeLab labelN (n, labelN
                            { globalTheory = computeLabelTheory libEnv ln newDG
                                 (n, labelN)
                              , labelHasHiding = True })
                           ] ++
                           map (\ (y, ly) -> SetNodeLab ly
                                           (y, ly {labelHasHiding = True})) succs
              return $ changesDGH newDG labCh
             _ -> return dg
                {- do
                -- failed in logic lid, look for comorphism and translate
                -- then recursive call
                let look = lookupQTA_in_LG $ language_name lid
                case maybeResult look of
                Nothing -> return dg
                -- can't translate to a logic where qta is implemented
                Just com -> do
                (m', dgM) <- translateFree libEnv dg edge com
                foldM (handleEdge libEnv) dgM $ out (dgBody dgM) m' -}
       _ -> return dg
  
  descs :: Gr a b -> Node -> [Node]
  descs graph node = let
     d nList descList =
      case nList of
        [] -> descList
        _ -> let
               newDescs = concatMap (suc graph) nList
               nList' = filter (\ x -> not $ (x `elem` nList) ||
                                            (x `elem` descList))
                        newDescs
               descList' = nub $ descList ++ newDescs
             in d nList' descList'
   in d [node] []
  
  
  {- translateFree :: LibEnv -> DGraph -> LEdge DGLinkLab -> AnyComorphism ->
  Result (Node, DGraph)
  translateFree le dg edge@(m,n,x) com = do
  (m', dg') <- translateNode le dg m (dgn_theory $ labDG dg m) com
  (n', dg'') <- translateNode le dg' n (dgn_theory $ labDG dg n) com
  dg''' <- translateEdge dg'' edge (dgl_morphism x) com m' n'
  return (m', dg''') -}
  
  {- translateEdge :: DGraph -> LEdge DGLinkLab -> GMorphism -> AnyComorphism ->
  Node -> Node -> Result DGraph
  translateEdge dg _edge (GMorphism cid _sig _i1 mor1 _i2)
  (Comorphism cid') m n = do
  let
  lidS = sourceLogic cid'
  lidT = targetLogic cid'
  mor2 <- coerceMorphism (targetLogic cid) lidS "" mor1
  mor3 <- map_morphism cid' mor2
  let
  gm = gEmbed $ mkG_morphism lidT mor3
  --del = DeleteEdge edge
  edge' = defDGLink gm
  (FreeOrCofreeDefLink Free $ EmptyNode $ Logic lidT)  DGLinkProof
  ins = InsertEdge (m, n, edge')
  return $ changesDGH dg  [ins] -}
  
  {- translateNode :: LibEnv -> DGraph -> Node -> G_theory -> AnyComorphism ->
  Result (Node, DGraph)
  translateNode libEnv dg n s@(G_theory lid sig _ _ _) com@(Comorphism cid) = do
  let
  m' = getNewNodeDG dg -- new node
  nodelab = labDG dg n
  info = nodeInfo nodelab
  ConsStatus cs _ _ = node_cons_status info
  lidS = sourceLogic cid
  lidT = targetLogic cid
  sig' <- coerceSign lid lidS "" sig
  (sig'',sen'') <- wrapMapTheory cid (plainSign sig', [])
  let
  gth = G_theory lidT (mkExtSign sig'') startSigId
  (toThSens sen'') startThId
  labelM' = newInfoNodeLab
  (extName "Freeness" $ dgn_name nodelab)
  info
  { node_origin = DGNormalForm n
  , node_cons_status = mkConsStatus cs }
  gth
  insM' = InsertNode (m', labelM')
  gMor <- gEmbedComorphism com (signOf s)
  let insE = InsertEdge (n,m', globDefLink gMor DGLinkProof)
  changeLabel = SetNodeLab nodelab
  (n, nodelab{dgn_freenf = Just m', dgn_phi = Just gMor})
  newDG = changesDGH dg [insM', insE, changeLabel]
  return $ (m', changeDGH newDG $ SetNodeLab labelM' (m', labelM'
  { globalTheory = computeLabelTheory libEnv newDG
  (m', labelM') })) -}
  
  {- thmFreeShift :: DGRule
  thmFreeShift = DGRule "TheoremFreeShift" -}
  
  {- ----------------------------------------------
  Theorem free shift and  auxiliaries
  moves theorem links to nodes with incoming free dfn links
  to their freeness normal form (must be computed before)
  --------------------------------------------- -}
  
  {- theoremFreeShift :: LibName -> LibEnv -> Result LibEnv
  theoremFreeShift ln  = return .
  Map.adjust (\ dg -> theoremFreeShiftAux (labNodesDG dg) dg) ln -}
  
  {- -- | assume that the normal forms a commputed already.
  -- return Nothing if nothing changed
  theoremFreeShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
  theoremFreeShiftAux  ns dg = let
  nodesWFree = map fst $ filter
  (\ (_, lbl) -> labelHasFree lbl && isJust (dgn_freenf lbl)
  && isJust (dgn_phi lbl)) ns
  -- all nodes with incoming hiding links
  -- all the theorem links entering these nodes
  -- have to replaced by theorem links with the same origin
  -- but pointing to the normal form of the former target node
  ingoingEdges = concatMap (getInComingGlobalUnprovenEdges dg) nodesWFree
  in foldl theoremFreeShiftForEdge
  dg ingoingEdges -}
  
  {- theoremFreeShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
  theoremFreeShiftForEdge dg edge@(source, target, edgeLab) =
  case maybeResult $ theoremFreeShiftForEdgeAux dg edge of
  Nothing -> error "theoremFreeShiftForEdgeAux"
  Just (dg', pbasis) -> let
  provenEdge = (source, target, edgeLab
  { dgl_type = setProof (Proven thmFreeShift pbasis) $ dgl_type edgeLab
  , dgl_origin = DGLinkProof
  , dgl_id = defaultEdgeId })
  in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge -}
  
  {- theoremFreeShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
  -> Result (DGraph, ProofBasis)
  theoremFreeShiftForEdgeAux dg (sn, tn, llab) = do
  let tlab = labDG dg tn
  Just nfNode = dgn_freenf tlab
  phi = dgl_morphism llab
  Just muN = dgn_phi tlab
  let cmor1  = composeMorphisms phi muN
  case maybeResult cmor1 of
  Nothing -> error "composition"
  Just cmor -> do
  let newEdge =(sn, nfNode, defDGLink cmor globalThm DGLinkProof)
  case tryToGetEdge newEdge dg of
  Nothing -> let
  newGraph = changeDGH dg $ InsertEdge newEdge
  finalEdge = case getLastChange newGraph of
  InsertEdge final_e -> final_e
  _ -> error "Proofs.Global.globDecompForOneEdgeAux"
  in return
  (newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
  Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e) -}
  
  {- theoremFreeShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
  -> Result LibEnv
  theoremFreeShiftFromList ln ls =
  return . Map.adjust (theoremFreeShiftAux ls) ln -}
  