content: {-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
  {- |
  Module      :  ./Proofs/FreeDefLinks.hs
  Description :  compute ingoing free definition links for provers
  Copyright   :  C. Maeder DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  compute ingoing free definition links for provers
  -}
  
  module Proofs.FreeDefLinks where
  
  import Static.GTheory
  import Static.DevGraph
  import Static.DgUtils
  import Static.ComputeTheory
  
  import Proofs.EdgeUtils
  
  import Common.ExtSign
  import Common.LibName
  import Common.AS_Annotation
  import qualified Common.Lib.Graph as Tree
  
  import Logic.Logic
  import Logic.Prover
  import Logic.Grothendieck
  import Logic.Comorphism
  import Logic.Coerce
  
  import Data.Graph.Inductive.Basic (elfilter)
  import Data.Graph.Inductive.Graph
  import Data.Maybe
  import Data.Typeable
  
  getCFreeDefLinks :: DGraph -> Node
    -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
  getCFreeDefLinks dg tgt =
    let isGlobalOrCFreeEdge = liftOr isGlobalEdge $ liftOr isFreeEdge isCofreeEdge
        paths = map reverse $ Tree.getAllPathsTo tgt
          $ elfilter (isGlobalOrCFreeEdge . dgl_type) $ dgBody dg
        myfilter p = filter ( \ ~((_, _, lbl) : _) -> p $ dgl_type lbl)
    in (myfilter isFreeEdge paths, myfilter isCofreeEdge paths)
  
  mkFreeDefMor :: [Named sentence] -> morphism -> morphism
    -> FreeDefMorphism sentence morphism
  mkFreeDefMor sens m1 m2 = FreeDefMorphism
    { freeDefMorphism = m1
    , pathFromFreeDef = m2
    , freeTheory = sens
    , isCofree = False }
  
  data GFreeDefMorphism =
    forall lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
    . Logic lid sublogics basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
    => GFreeDefMorphism lid (FreeDefMorphism sentence morphism)
    deriving Typeable
  
  getFreeDefMorphism :: LibEnv -> LibName -> DGraph -> [LEdge DGLinkLab]
    -> Maybe GFreeDefMorphism
  getFreeDefMorphism libEnv ln dg path = case path of
    [] -> error "getFreeDefMorphism"
    (s, t, l) : rp -> do
      gmor@(GMorphism cid _ _ fmor _) <- return $ dgl_morphism l
      let tlid = targetLogic cid
      G_theory lidth _ (ExtSign _sign _) _ axs _ <-
        computeTheory libEnv ln s
      if isHomogeneous gmor then do
          sens <- coerceSens lidth tlid "getFreeDefMorphism4" (toNamedList axs)
          case rp of
            [] -> do
              G_theory lid2 _ (ExtSign sig _) _ _ _ <-
                       return $ dgn_theory $ labDG dg t
              sig2 <- coercePlainSign lid2 tlid "getFreeDefMorphism2" sig
              return $ GFreeDefMorphism tlid $ mkFreeDefMor sens fmor $ ide sig2
            _ -> do
              pm@(GMorphism cid2 _ _ pmor _) <- calculateMorphismOfPath rp
              if isHomogeneous pm then do
                  cpmor <- coerceMorphism (targetLogic cid2) tlid
                           "getFreeDefMorphism3" pmor
                  return $ GFreeDefMorphism tlid $ mkFreeDefMor sens fmor cpmor
                else Nothing
        else Nothing
  
  getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]
  getCFreeDefMorphs libEnv ln dg node = let
    (frees, cofrees) = getCFreeDefLinks dg node
    myget = mapMaybe (getFreeDefMorphism libEnv ln dg)
    mkCoFree (GFreeDefMorphism lid m) = GFreeDefMorphism lid m { isCofree = True }
    in myget frees ++ map mkCoFree (myget cofrees)
  