{- |
Module      :  ./Proofs/HideTheoremShift.hs
Description :  hide theorem shift proof rule for development graphs
Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

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

hide theorem shift proof rule for development graphs
   Follows Sect. IV:4.4 of the CASL Reference Manual.
-}

{-
   References:

   T. Mossakowski, S. Autexier and D. Hutter:
   Extending Development Graphs With Hiding.
   H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
   Lecture Notes in Computer Science 2029, p. 269-283,
   Springer-Verlag 2001.
-}

module Proofs.HideTheoremShift
    ( interactiveHideTheoremShift
    , automaticHideTheoremShift
    , automaticHideTheoremShiftFromList
    ) where

import Comorphisms.LogicGraph

import GUI.Utils

import Logic.Grothendieck

import Proofs.EdgeUtils

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.Consistency
import Common.LibName
import Common.Result

import Control.Monad.Identity
import qualified Data.Map as Map
import Data.Graph.Inductive.Graph
import Data.Maybe (isJust)

type ListSelector m a = [a] -> m (Maybe a)
type PathTuple = ([LEdge DGLinkLab], [LEdge DGLinkLab])
type ProofBaseSelector m = DGraph -> ListSelector m PathTuple

hideThmShiftRule :: EdgeId -> DGRule
hideThmShiftRule :: EdgeId -> DGRule
hideThmShiftRule = String -> EdgeId -> DGRule
DGRuleWithEdge "HideTheoremShift"

interactiveHideTheoremShift :: LibName -> LibEnv -> IO LibEnv
interactiveHideTheoremShift :: LibName -> LibEnv -> IO LibEnv
interactiveHideTheoremShift =
    ProofBaseSelector IO -> LibName -> LibEnv -> IO LibEnv
forall (m :: * -> *).
Monad m =>
ProofBaseSelector m -> LibName -> LibEnv -> m LibEnv
hideTheoremShift ProofBaseSelector IO
hideTheoremShift_selectProofBase

automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
automaticHideTheoremShift ln :: LibName
ln libEnv :: LibEnv
libEnv =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
        ls :: [LEdge DGLinkLab]
ls = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isUnprovenHidingThm) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticHideTheoremShiftFromList LibName
ln [LEdge DGLinkLab]
ls LibEnv
libEnv

automaticHideTheoremShiftFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv
                                  -> LibEnv
automaticHideTheoremShiftFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticHideTheoremShiftFromList ln :: LibName
ln ls :: [LEdge DGLinkLab]
ls = Identity LibEnv -> LibEnv
forall a. Identity a -> a
runIdentity (Identity LibEnv -> LibEnv)
-> (LibEnv -> Identity LibEnv) -> LibEnv -> LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofBaseSelector Identity
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> Identity LibEnv
forall (m :: * -> *).
Monad m =>
ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
hideTheoremShiftFromList
      (([PathTuple] -> Identity (Maybe PathTuple))
-> ProofBaseSelector Identity
forall a b. a -> b -> a
const (([PathTuple] -> Identity (Maybe PathTuple))
 -> ProofBaseSelector Identity)
-> ([PathTuple] -> Identity (Maybe PathTuple))
-> ProofBaseSelector Identity
forall a b. (a -> b) -> a -> b
$ \ l :: [PathTuple]
l -> Maybe PathTuple -> Identity (Maybe PathTuple)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PathTuple -> Identity (Maybe PathTuple))
-> Maybe PathTuple -> Identity (Maybe PathTuple)
forall a b. (a -> b) -> a -> b
$ case [PathTuple]
l of
                      [a :: PathTuple
a] -> PathTuple -> Maybe PathTuple
forall a. a -> Maybe a
Just PathTuple
a -- maybe take the first one always ?
                      _ -> Maybe PathTuple
forall a. Maybe a
Nothing) LibName
ln [LEdge DGLinkLab]
ls

hideTheoremShiftFromList :: Monad m => ProofBaseSelector m -> LibName
                     -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
hideTheoremShiftFromList :: ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
hideTheoremShiftFromList proofBaseSel :: ProofBaseSelector m
proofBaseSel ln :: LibName
ln hidingThmEdges :: [LEdge DGLinkLab]
hidingThmEdges proofStatus :: LibEnv
proofStatus = do
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
        finalHidingThmEdges :: [LEdge DGLinkLab]
finalHidingThmEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isUnprovenHidingThm) [LEdge DGLinkLab]
hidingThmEdges
    DGraph
nextDGraph <- (DGraph -> LEdge DGLinkLab -> m DGraph)
-> DGraph -> [LEdge DGLinkLab] -> m DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
       (ProofBaseSelector m -> DGraph -> LEdge DGLinkLab -> m DGraph
forall (m :: * -> *).
Monad m =>
ProofBaseSelector m -> DGraph -> LEdge DGLinkLab -> m DGraph
hideTheoremShiftAux ProofBaseSelector m
proofBaseSel) DGraph
dgraph [LEdge DGLinkLab]
finalHidingThmEdges
    LibEnv -> m LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> m LibEnv) -> LibEnv -> m LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
nextDGraph LibEnv
proofStatus

hideTheoremShift :: Monad m => ProofBaseSelector m -> LibName
                 -> LibEnv -> m LibEnv
hideTheoremShift :: ProofBaseSelector m -> LibName -> LibEnv -> m LibEnv
hideTheoremShift proofBaseSel :: ProofBaseSelector m
proofBaseSel ln :: LibName
ln proofStatus :: LibEnv
proofStatus =
    let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
        hidingThmEdges :: [LEdge DGLinkLab]
hidingThmEdges = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
    in ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
forall (m :: * -> *).
Monad m =>
ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
hideTheoremShiftFromList ProofBaseSelector m
proofBaseSel LibName
ln [LEdge DGLinkLab]
hidingThmEdges LibEnv
proofStatus

{- | auxiliary method for hideTheoremShift.
     it contains three steps: inserting of the proof basis, deleting of the
     current edge and inserting of the new proven edge.
-}
hideTheoremShiftAux :: Monad m => ProofBaseSelector m -> DGraph
                    -> LEdge DGLinkLab -> m DGraph
hideTheoremShiftAux :: ProofBaseSelector m -> DGraph -> LEdge DGLinkLab -> m DGraph
hideTheoremShiftAux proofBaseSel :: ProofBaseSelector m
proofBaseSel dgraph :: DGraph
dgraph ledge :: LEdge DGLinkLab
ledge =
  do [LEdge DGLinkLab]
proofbasis <- DGraph
-> LEdge DGLinkLab -> ProofBaseSelector m -> m [LEdge DGLinkLab]
forall (m :: * -> *).
Monad m =>
DGraph
-> LEdge DGLinkLab -> ProofBaseSelector m -> m [LEdge DGLinkLab]
findProofBaseForHideTheoremShift DGraph
dgraph LEdge DGLinkLab
ledge ProofBaseSelector m
proofBaseSel
     DGraph -> m DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> m DGraph) -> DGraph -> m DGraph
forall a b. (a -> b) -> a -> b
$ if [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LEdge DGLinkLab]
proofbasis
      then DGraph
dgraph
       else
         let (auxDGraph :: DGraph
auxDGraph, finalProofBasis :: ProofBasis
finalProofBasis) =
                 ((DGraph, ProofBasis) -> LEdge DGLinkLab -> (DGraph, ProofBasis))
-> (DGraph, ProofBasis)
-> [LEdge DGLinkLab]
-> (DGraph, ProofBasis)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (DGraph, ProofBasis) -> LEdge DGLinkLab -> (DGraph, ProofBasis)
insertNewEdges (DGraph
dgraph, ProofBasis
emptyProofBasis) [LEdge DGLinkLab]
proofbasis
             newEdge :: LEdge DGLinkLab
newEdge = ProofBasis -> LEdge DGLinkLab -> LEdge DGLinkLab
makeProvenHidingThmEdge ProofBasis
finalProofBasis LEdge DGLinkLab
ledge
             newDGraph2 :: DGraph
newDGraph2 = DGraph -> DGChange -> DGraph
changeDGH DGraph
auxDGraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
ledge
             newDGraph :: DGraph
newDGraph = LEdge DGLinkLab -> DGraph -> DGraph
insertDGLEdge LEdge DGLinkLab
newEdge DGraph
newDGraph2
             newRules :: DGRule
newRules = EdgeId -> DGRule
hideThmShiftRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
ledge
         in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph DGRule
newRules DGraph
newDGraph

{- | inserts the given edges into the development graph and adds a
     corresponding entry to the changes, while getting the proofbasis.
     Notice that EdgeId is enough to represent an edge and can therefore
     be used as proof basis.
-}
insertNewEdges :: (DGraph, ProofBasis) -> LEdge DGLinkLab
               -> (DGraph, ProofBasis)
insertNewEdges :: (DGraph, ProofBasis) -> LEdge DGLinkLab -> (DGraph, ProofBasis)
insertNewEdges (dgraph :: DGraph
dgraph, proofbasis :: ProofBasis
proofbasis) edge :: LEdge DGLinkLab
edge =
  case LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
tryToGetEdge LEdge DGLinkLab
edge DGraph
dgraph of
       Just e :: LEdge DGLinkLab
e -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
e)
       Nothing -> let
                  tempDGraph :: DGraph
tempDGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
edge
                  -- checks if the edge is actually inserted
                  tempProofBasis :: ProofBasis
tempProofBasis = case DGraph -> DGChange
getLastChange DGraph
tempDGraph of
                    InsertEdge tempE :: LEdge DGLinkLab
tempE ->
                        ProofBasis -> EdgeId -> ProofBasis
addEdgeId ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
tempE
                    _ -> String -> ProofBasis
forall a. HasCallStack => String -> a
error ("Proofs" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                ".HideTheoremShift" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                ".insertNewEdges")
                  in (DGraph
tempDGraph, ProofBasis
tempProofBasis)

{- | creates a new proven HidingThm edge from the given
     HidingThm edge using the edge list as the proofbasis
-}
makeProvenHidingThmEdge :: ProofBasis -> LEdge DGLinkLab -> LEdge DGLinkLab
makeProvenHidingThmEdge :: ProofBasis -> LEdge DGLinkLab -> LEdge DGLinkLab
makeProvenHidingThmEdge proofBasisEdges :: ProofBasis
proofBasisEdges ledge :: LEdge DGLinkLab
ledge@(src :: Node
src, tgt :: Node
tgt, edgeLab :: DGLinkLab
edgeLab) =
  (Node
src, Node
tgt, DGLinkLab
edgeLab
       { dgl_type :: DGLinkType
dgl_type = ThmLinkStatus -> DGLinkType -> DGLinkType
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven (EdgeId -> DGRule
hideThmShiftRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> EdgeId
getEdgeId LEdge DGLinkLab
ledge)
                              ProofBasis
proofBasisEdges)
           (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
edgeLab
       , dgl_origin :: DGLinkOrigin
dgl_origin = DGLinkOrigin
DGLinkProof })

-- | selects a proof basis for 'hide theorem shift' if there is one
findProofBaseForHideTheoremShift :: Monad m => DGraph -> LEdge DGLinkLab
                                 -> ProofBaseSelector m -> m [LEdge DGLinkLab]
findProofBaseForHideTheoremShift :: DGraph
-> LEdge DGLinkLab -> ProofBaseSelector m -> m [LEdge DGLinkLab]
findProofBaseForHideTheoremShift dgraph :: DGraph
dgraph (ledge :: LEdge DGLinkLab
ledge@(src :: Node
src, tgt :: Node
tgt, lb :: DGLinkLab
lb)) proofBaseSel :: ProofBaseSelector m
proofBaseSel = do
  let dgraph2 :: DGraph
dgraph2 = LEdge DGLinkLab -> DGraph -> DGraph
delLEdgeDG LEdge DGLinkLab
ledge DGraph
dgraph
      pathsFromSrc :: [[LEdge DGLinkLab]]
pathsFromSrc = DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom DGraph
dgraph2 Node
src
      pathsFromTgt :: [[LEdge DGLinkLab]]
pathsFromTgt = DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom DGraph
dgraph2 Node
tgt
      possiblePathPairs :: [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
possiblePathPairs = [[LEdge DGLinkLab]]
-> [[LEdge DGLinkLab]]
-> [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
selectPathPairs [[LEdge DGLinkLab]]
pathsFromSrc [[LEdge DGLinkLab]]
pathsFromTgt
      HidingFreeOrCofreeThm Nothing _ hidingMorphism :: GMorphism
hidingMorphism _ = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lb
      morphism :: GMorphism
morphism = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lb
      pathPairsFilteredByMorphism :: [PathTuple]
pathPairsFilteredByMorphism
        = [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
-> GMorphism -> GMorphism -> [PathTuple]
filterPairsByResultingMorphisms [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
possiblePathPairs
          GMorphism
hidingMorphism GMorphism
morphism
      pathPairsFilteredByConservativity :: [PathTuple]
pathPairsFilteredByConservativity
        = [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [PathTuple]
pathPairsFilteredByMorphism
      -- advoiding duplicate to be selected proofbasis.
      pathPairsFilteredByProveStatus :: [PathTuple]
pathPairsFilteredByProveStatus
        = [PathTuple] -> [PathTuple]
filterPairsByGlobalProveStatus [PathTuple]
pathPairsFilteredByConservativity
  Maybe PathTuple
pb <- ProofBaseSelector m
proofBaseSel DGraph
dgraph [PathTuple]
pathPairsFilteredByProveStatus
  [LEdge DGLinkLab] -> m [LEdge DGLinkLab]
forall (m :: * -> *) a. Monad m => a -> m a
return ([LEdge DGLinkLab] -> m [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> m [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ case Maybe PathTuple
pb of
          Nothing -> []
          Just (fstPath :: [LEdge DGLinkLab]
fstPath, sndPath :: [LEdge DGLinkLab]
sndPath) -> ([LEdge DGLinkLab] -> LEdge DGLinkLab)
-> [[LEdge DGLinkLab]] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map [LEdge DGLinkLab] -> LEdge DGLinkLab
createEdgeForPath [[LEdge DGLinkLab]
fstPath, [LEdge DGLinkLab]
sndPath]

-- | advoiding duplicate to be selected proofbasis.
filterPairsByGlobalProveStatus :: [([LEdge DGLinkLab], [LEdge DGLinkLab])]
                               -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
filterPairsByGlobalProveStatus :: [PathTuple] -> [PathTuple]
filterPairsByGlobalProveStatus = (PathTuple -> Bool) -> [PathTuple] -> [PathTuple]
forall a. (a -> Bool) -> [a] -> [a]
filter PathTuple -> Bool
bothAreProven where
  bothAreProven :: PathTuple -> Bool
bothAreProven (pb1 :: [LEdge DGLinkLab]
pb1, pb2 :: [LEdge DGLinkLab]
pb2) = [LEdge DGLinkLab] -> Bool
allAreProven [LEdge DGLinkLab]
pb1 Bool -> Bool -> Bool
&& [LEdge DGLinkLab] -> Bool
allAreProven [LEdge DGLinkLab]
pb2
  allAreProven :: [LEdge DGLinkLab] -> Bool
allAreProven = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool)
-> (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE (\ l :: DGLinkType
l -> DGLinkType -> Bool
isProven DGLinkType
l Bool -> Bool -> Bool
&& DGLinkType -> Bool
isGlobalEdge DGLinkType
l)

{- removes all pairs from the given list whose second path does not have a
   conservativity greater than or equal to Cons -}
filterPairsByConservativityOfSecondPath
    :: [([LEdge DGLinkLab], [LEdge DGLinkLab])]
    -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
filterPairsByConservativityOfSecondPath :: [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [] = []
filterPairsByConservativityOfSecondPath (([], _) : list :: [PathTuple]
list) =
  [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [PathTuple]
list
filterPairsByConservativityOfSecondPath ((_, []) : list :: [PathTuple]
list) =
  [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [PathTuple]
list
filterPairsByConservativityOfSecondPath (pair :: PathTuple
pair : list :: [PathTuple]
list) =
  if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Conservativity
cons Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
>= Conservativity
Cons | Conservativity
cons <- (LEdge DGLinkLab -> Conservativity)
-> [LEdge DGLinkLab] -> [Conservativity]
forall a b. (a -> b) -> [a] -> [b]
map LEdge DGLinkLab -> Conservativity
getConservativity (PathTuple -> [LEdge DGLinkLab]
forall a b. (a, b) -> b
snd PathTuple
pair)]
   then PathTuple
pair PathTuple -> [PathTuple] -> [PathTuple]
forall a. a -> [a] -> [a]
: [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [PathTuple]
list
    else [PathTuple] -> [PathTuple]
filterPairsByConservativityOfSecondPath [PathTuple]
list

{- | selects a proofBasis (i.e. a path tuple) from the list of possible ones:
     If there is exaclty one proofBasis in the list, this is returned.
     If there are more than one and the method is called in automatic mode
     Nothing is returned.
     In non-automatic mode the user is asked to select a proofBasis via
     listBox, then the selected one will be returned.
-}
hideTheoremShift_selectProofBase
    :: DGraph -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
    -> IO (Maybe ([LEdge DGLinkLab], [LEdge DGLinkLab]))
hideTheoremShift_selectProofBase :: ProofBaseSelector IO
hideTheoremShift_selectProofBase dgraph :: DGraph
dgraph basisList :: [PathTuple]
basisList =
  case [PathTuple]
basisList of
    [] -> Maybe PathTuple -> IO (Maybe PathTuple)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PathTuple
forall a. Maybe a
Nothing
    [basis :: PathTuple
basis] -> Maybe PathTuple -> IO (Maybe PathTuple)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PathTuple -> IO (Maybe PathTuple))
-> Maybe PathTuple -> IO (Maybe PathTuple)
forall a b. (a -> b) -> a -> b
$ PathTuple -> Maybe PathTuple
forall a. a -> Maybe a
Just PathTuple
basis
    _ -> do
         Maybe Node
sel <- String -> [String] -> IO (Maybe Node)
listBox
                       "Choose a path tuple as the proof basis"
                       ((PathTuple -> String) -> [PathTuple] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (DGraph -> PathTuple -> String
prettyPrintPathTuple DGraph
dgraph) [PathTuple]
basisList)
         case Maybe Node
sel of
             Just j :: Node
j -> Maybe PathTuple -> IO (Maybe PathTuple)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PathTuple -> IO (Maybe PathTuple))
-> Maybe PathTuple -> IO (Maybe PathTuple)
forall a b. (a -> b) -> a -> b
$ PathTuple -> Maybe PathTuple
forall a. a -> Maybe a
Just ([PathTuple]
basisList [PathTuple] -> Node -> PathTuple
forall a. [a] -> Node -> a
!! Node
j)
             _ -> Maybe PathTuple -> IO (Maybe PathTuple)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PathTuple
forall a. Maybe a
Nothing

{- returns a string representation of the given paths: for each path a
   tuple of the names of its nodes is shown, the two are combined by
   an \'and\' -}
prettyPrintPathTuple :: DGraph -> ([LEdge DGLinkLab], [LEdge DGLinkLab])
                     -> String
prettyPrintPathTuple :: DGraph -> PathTuple -> String
prettyPrintPathTuple dgraph :: DGraph
dgraph (p1 :: [LEdge DGLinkLab]
p1, p2 :: [LEdge DGLinkLab]
p2) =
  DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath DGraph
dgraph [LEdge DGLinkLab]
p1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath DGraph
dgraph [LEdge DGLinkLab]
p2

-- returns the names of the nodes of the path, separated by commas
prettyPrintNodesOfPath :: DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath :: DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath _ [] = ""
prettyPrintNodesOfPath dgraph :: DGraph
dgraph (edge :: LEdge DGLinkLab
edge : path :: [LEdge DGLinkLab]
path) =
  DGraph -> LEdge DGLinkLab -> String
prettyPrintSourceNode DGraph
dgraph LEdge DGLinkLab
edge String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", "
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath DGraph
dgraph [LEdge DGLinkLab]
path
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
end
  where
    end :: String
end = case [LEdge DGLinkLab]
path of
            [] -> DGraph -> LEdge DGLinkLab -> String
prettyPrintTargetNode DGraph
dgraph LEdge DGLinkLab
edge
            _ -> ""

-- returns a string reprentation of the path: showing a tuple of its nodes
prettyPrintPath :: DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath :: DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath _ [] = "<empty path>"
prettyPrintPath dgraph :: DGraph
dgraph path :: [LEdge DGLinkLab]
path =
  "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath DGraph
dgraph [LEdge DGLinkLab]
path String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

-- returns the name of the source node of the given edge
prettyPrintSourceNode :: DGraph -> LEdge DGLinkLab -> String
prettyPrintSourceNode :: DGraph -> LEdge DGLinkLab -> String
prettyPrintSourceNode dgraph :: DGraph
dgraph (src :: Node
src, _, _) =
   DGNodeLab -> String
getDGNodeName (DGNodeLab -> String) -> DGNodeLab -> String
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
src

-- returns the name of the target node of the given edge
prettyPrintTargetNode :: DGraph -> LEdge DGLinkLab -> String
prettyPrintTargetNode :: DGraph -> LEdge DGLinkLab -> String
prettyPrintTargetNode dgraph :: DGraph
dgraph (_, tgt :: Node
tgt, _) =
   DGNodeLab -> String
getDGNodeName (DGNodeLab -> String) -> DGNodeLab -> String
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dgraph Node
tgt

{- creates a unproven global thm edge for the given path, i.e. with
the same source and target nodes and the same morphism as the path -}
createEdgeForPath :: [LEdge DGLinkLab] -> LEdge DGLinkLab
createEdgeForPath :: [LEdge DGLinkLab] -> LEdge DGLinkLab
createEdgeForPath path :: [LEdge DGLinkLab]
path =
  case ([LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path, [LEdge DGLinkLab]
path) of
    (Just morphism :: GMorphism
morphism, (s :: Node
s, _, _) : _) ->
        let (_, t :: Node
t, _) = [LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
last [LEdge DGLinkLab]
path
        in (Node
s, Node
t, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
morphism DGLinkType
globalThm DGLinkOrigin
DGLinkProof)
    _ -> String -> LEdge DGLinkLab
forall a. HasCallStack => String -> a
error "createEdgeForPath"

{- returns a list of path pairs, as shorthand the pairs are not
returned as path-path tuples but as path-<list of path> tuples. Every
path in the list is a pair of the single path.  The path pairs are
selected by having the same target node. -}
selectPathPairs :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
                -> [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
selectPathPairs :: [[LEdge DGLinkLab]]
-> [[LEdge DGLinkLab]]
-> [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
selectPathPairs [] _ = []
selectPathPairs _ [] = []
selectPathPairs paths1 :: [[LEdge DGLinkLab]]
paths1 paths2 :: [[LEdge DGLinkLab]]
paths2 =
  [([LEdge DGLinkLab]
p1, [[LEdge DGLinkLab]
p2 | [LEdge DGLinkLab]
p2 <- [[LEdge DGLinkLab]]
paths2, LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
haveSameTgt ([LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
last [LEdge DGLinkLab]
p1) ([LEdge DGLinkLab] -> LEdge DGLinkLab
forall a. [a] -> a
last [LEdge DGLinkLab]
p2) ] ) | [LEdge DGLinkLab]
p1 <- [[LEdge DGLinkLab]]
paths1]

  where
    haveSameTgt :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
    haveSameTgt :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
haveSameTgt (_, tgt1 :: Node
tgt1, _) (_, tgt2 :: Node
tgt2, _) = Node
tgt1 Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
tgt2

{- returns a list of path pairs by keeping those pairs, whose first
path composed with the first given morphism and whose second path
composed with the second given morphism result in the same morphism,
and dropping all other pairs. -}
filterPairsByResultingMorphisms :: [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
                                -> GMorphism -> GMorphism
                                -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
filterPairsByResultingMorphisms :: [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
-> GMorphism -> GMorphism -> [PathTuple]
filterPairsByResultingMorphisms [] _ _ = []
filterPairsByResultingMorphisms (pair :: ([LEdge DGLinkLab], [[LEdge DGLinkLab]])
pair : pairs :: [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
pairs) morph1 :: GMorphism
morph1 morph2 :: GMorphism
morph2 =
  [(([LEdge DGLinkLab], [[LEdge DGLinkLab]]) -> [LEdge DGLinkLab]
forall a b. (a, b) -> a
fst ([LEdge DGLinkLab], [[LEdge DGLinkLab]])
pair, [LEdge DGLinkLab]
path) | [LEdge DGLinkLab]
path <- [[LEdge DGLinkLab]]
suitingPaths]
          [PathTuple] -> [PathTuple] -> [PathTuple]
forall a. [a] -> [a] -> [a]
++ [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
-> GMorphism -> GMorphism -> [PathTuple]
filterPairsByResultingMorphisms [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
pairs GMorphism
morph1 GMorphism
morph2
  where
    compMorph1 :: Maybe GMorphism
compMorph1
        = Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
compMaybeMorphisms (GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morph1) ([LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath (([LEdge DGLinkLab], [[LEdge DGLinkLab]]) -> [LEdge DGLinkLab]
forall a b. (a, b) -> a
fst ([LEdge DGLinkLab], [[LEdge DGLinkLab]])
pair))
    suitingPaths :: [[LEdge DGLinkLab]]
    suitingPaths :: [[LEdge DGLinkLab]]
suitingPaths = if Maybe GMorphism -> Bool
forall a. Maybe a -> Bool
isJust Maybe GMorphism
compMorph1 then
                      [[LEdge DGLinkLab]
path | [LEdge DGLinkLab]
path <- ([LEdge DGLinkLab], [[LEdge DGLinkLab]]) -> [[LEdge DGLinkLab]]
forall a b. (a, b) -> b
snd ([LEdge DGLinkLab], [[LEdge DGLinkLab]])
pair,
                       Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
compMaybeMorphisms (GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morph2)
                                          ([LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
path)
                       Maybe GMorphism -> Maybe GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe GMorphism
compMorph1]
                    else []

{- if the given maybe morphisms are both not Nothing,
   this method composes their GMorphisms -
   returns Nothing otherwise -}
compMaybeMorphisms :: Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
compMaybeMorphisms :: Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
compMaybeMorphisms morph1 :: Maybe GMorphism
morph1 morph2 :: Maybe GMorphism
morph2 =
  case (Maybe GMorphism
morph1, Maybe GMorphism
morph2) of
    (Just m1 :: GMorphism
m1, Just m2 :: GMorphism
m2) -> Result GMorphism -> Maybe GMorphism
forall a. Result a -> Maybe a
resultToMaybe (Result GMorphism -> Maybe GMorphism)
-> Result GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion LogicGraph
logicGraph GMorphism
m1 GMorphism
m2
       -- This should be compInclusion, but this would need the logic graph
    _ -> Maybe GMorphism
forall a. Maybe a
Nothing