{-# 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 :: DGraph -> Node -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
getCFreeDefLinks dg :: DGraph
dg tgt :: Node
tgt =
  let isGlobalOrCFreeEdge :: DGLinkType -> Bool
isGlobalOrCFreeEdge = (DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isGlobalEdge ((DGLinkType -> Bool) -> DGLinkType -> Bool)
-> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isFreeEdge DGLinkType -> Bool
isCofreeEdge
      paths :: [[LEdge DGLinkLab]]
paths = ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> [a] -> [b]
map [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. [a] -> [a]
reverse ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ Node -> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. Node -> Gr a b -> [[LEdge b]]
Tree.getAllPathsTo Node
tgt
        (Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (DGLinkType -> Bool
isGlobalOrCFreeEdge (DGLinkType -> Bool)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type) (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
      myfilter :: (DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter p :: DGLinkType -> Bool
p = ([(a, b, DGLinkLab)] -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ ~((_, _, lbl :: DGLinkLab
lbl) : _) -> DGLinkType -> Bool
p (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl)
  in ((DGLinkType -> Bool) -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b.
(DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter DGLinkType -> Bool
isFreeEdge [[LEdge DGLinkLab]]
paths, (DGLinkType -> Bool) -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b.
(DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter DGLinkType -> Bool
isCofreeEdge [[LEdge DGLinkLab]]
paths)

mkFreeDefMor :: [Named sentence] -> morphism -> morphism
  -> FreeDefMorphism sentence morphism
mkFreeDefMor :: [Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor sens :: [Named sentence]
sens m1 :: morphism
m1 m2 :: morphism
m2 = FreeDefMorphism :: forall sentence morphism.
morphism
-> morphism
-> [Named sentence]
-> Bool
-> FreeDefMorphism sentence morphism
FreeDefMorphism
  { freeDefMorphism :: morphism
freeDefMorphism = morphism
m1
  , pathFromFreeDef :: morphism
pathFromFreeDef = morphism
m2
  , freeTheory :: [Named sentence]
freeTheory = [Named sentence]
sens
  , isCofree :: Bool
isCofree = Bool
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
-> LibName -> DGraph -> [LEdge DGLinkLab] -> Maybe GFreeDefMorphism
getFreeDefMorphism libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg path :: [LEdge DGLinkLab]
path = case [LEdge DGLinkLab]
path of
  [] -> [Char] -> Maybe GFreeDefMorphism
forall a. HasCallStack => [Char] -> a
error "getFreeDefMorphism"
  (s :: Node
s, t :: Node
t, l :: DGLinkLab
l) : rp :: [LEdge DGLinkLab]
rp -> do
    gmor :: GMorphism
gmor@(GMorphism cid :: cid
cid _ _ fmor :: morphism2
fmor _) <- GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l
    let tlid :: lid2
tlid = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
    G_theory lidth :: lid
lidth _ (ExtSign _sign :: sign
_sign _) _ axs :: ThSens sentence (AnyComorphism, BasicProof)
axs _ <-
      LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Node
s
    if GMorphism -> Bool
isHomogeneous GMorphism
gmor then do
        [Named sentence2]
sens <- lid
-> lid2 -> [Char] -> [Named sentence] -> Maybe [Named sentence2]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> [Named sentence1] -> m [Named sentence2]
coerceSens lid
lidth lid2
tlid "getFreeDefMorphism4" (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axs)
        case [LEdge DGLinkLab]
rp of
          [] -> do
            G_theory lid2 :: lid
lid2 _ (ExtSign sig :: sign
sig _) _ _ _ <-
                     G_theory -> Maybe G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
t
            sign2
sig2 <- lid -> lid2 -> [Char] -> sign -> Maybe sign2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> sign1 -> m sign2
coercePlainSign lid
lid2 lid2
tlid "getFreeDefMorphism2" sign
sig
            GFreeDefMorphism -> Maybe GFreeDefMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GFreeDefMorphism -> Maybe GFreeDefMorphism)
-> GFreeDefMorphism -> Maybe GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ lid2 -> FreeDefMorphism sentence2 morphism2 -> 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 =>
lid -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid2
tlid (FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism)
-> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ [Named sentence2]
-> morphism2 -> morphism2 -> FreeDefMorphism sentence2 morphism2
forall sentence morphism.
[Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor [Named sentence2]
sens morphism2
fmor (morphism2 -> FreeDefMorphism sentence2 morphism2)
-> morphism2 -> FreeDefMorphism sentence2 morphism2
forall a b. (a -> b) -> a -> b
$ sign2 -> morphism2
forall object morphism.
Category object morphism =>
object -> morphism
ide sign2
sig2
          _ -> do
            pm :: GMorphism
pm@(GMorphism cid2 :: cid
cid2 _ _ pmor :: morphism2
pmor _) <- [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
rp
            if GMorphism -> Bool
isHomogeneous GMorphism
pm then do
                morphism2
cpmor <- lid2 -> lid2 -> [Char] -> morphism2 -> Maybe morphism2
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid2) lid2
tlid
                         "getFreeDefMorphism3" morphism2
pmor
                GFreeDefMorphism -> Maybe GFreeDefMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GFreeDefMorphism -> Maybe GFreeDefMorphism)
-> GFreeDefMorphism -> Maybe GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ lid2 -> FreeDefMorphism sentence2 morphism2 -> 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 =>
lid -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid2
tlid (FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism)
-> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ [Named sentence2]
-> morphism2 -> morphism2 -> FreeDefMorphism sentence2 morphism2
forall sentence morphism.
[Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor [Named sentence2]
sens morphism2
fmor morphism2
cpmor
              else Maybe GFreeDefMorphism
forall a. Maybe a
Nothing
      else Maybe GFreeDefMorphism
forall a. Maybe a
Nothing

getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]
getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]
getCFreeDefMorphs libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg node :: Node
node = let
  (frees :: [[LEdge DGLinkLab]]
frees, cofrees :: [[LEdge DGLinkLab]]
cofrees) = DGraph -> Node -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
getCFreeDefLinks DGraph
dg Node
node
  myget :: [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget = ([LEdge DGLinkLab] -> Maybe GFreeDefMorphism)
-> [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (LibEnv
-> LibName -> DGraph -> [LEdge DGLinkLab] -> Maybe GFreeDefMorphism
getFreeDefMorphism LibEnv
libEnv LibName
ln DGraph
dg)
  mkCoFree :: GFreeDefMorphism -> GFreeDefMorphism
mkCoFree (GFreeDefMorphism lid :: lid
lid m :: FreeDefMorphism sentence morphism
m) = lid -> FreeDefMorphism sentence morphism -> 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 =>
lid -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid
lid FreeDefMorphism sentence morphism
m { isCofree :: Bool
isCofree = Bool
True }
  in [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget [[LEdge DGLinkLab]]
frees [GFreeDefMorphism] -> [GFreeDefMorphism] -> [GFreeDefMorphism]
forall a. [a] -> [a] -> [a]
++ (GFreeDefMorphism -> GFreeDefMorphism)
-> [GFreeDefMorphism] -> [GFreeDefMorphism]
forall a b. (a -> b) -> [a] -> [b]
map GFreeDefMorphism -> GFreeDefMorphism
mkCoFree ([[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget [[LEdge DGLinkLab]]
cofrees)