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

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 qualified Data.Map as Map
import Data.Graph.Inductive.Graph
import Data.Maybe (isJust)

type ListSelector m a = [a] -> m (Maybe a)
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 :: * -> *).
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
forall a. (a -> Bool) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
labEdgesDG DGraph
dgraph
in LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticHideTheoremShiftFromList LibName
ls LibEnv
libEnv

automaticHideTheoremShiftFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv
-> LibEnv
automaticHideTheoremShiftFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticHideTheoremShiftFromList ln :: LibName
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 :: * -> *).
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
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
hidingThmEdges proofStatus :: LibEnv
proofStatus = do
let dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
proofStatus
forall a. (a -> Bool) -> [a] -> [a]
hidingThmEdges
DGraph
nextDGraph <- (DGraph -> LEdge DGLinkLab -> m DGraph)
-> DGraph -> [LEdge DGLinkLab] -> m DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(b -> a -> m b) -> b -> t a -> m b
foldM
(ProofBaseSelector m -> DGraph -> LEdge DGLinkLab -> m DGraph
forall (m :: * -> *).
ProofBaseSelector m -> DGraph -> LEdge DGLinkLab -> m DGraph
hideTheoremShiftAux ProofBaseSelector m
proofBaseSel) DGraph
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 = DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
in ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
forall (m :: * -> *).
ProofBaseSelector m
-> LibName -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
hideTheoremShiftFromList ProofBaseSelector m
proofBaseSel LibName
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
ledge =
proofbasis <- DGraph
forall (m :: * -> *).
DGraph
findProofBaseForHideTheoremShift DGraph
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
proofbasis
then DGraph
dgraph
else
let (auxDGraph :: DGraph
auxDGraph, finalProofBasis :: ProofBasis
finalProofBasis) =
((DGraph, ProofBasis) -> LEdge DGLinkLab -> (DGraph, ProofBasis))
-> (DGraph, ProofBasis)
-> (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
proofbasis
makeProvenHidingThmEdge ProofBasis
ledge
newDGraph2 :: DGraph
newDGraph2 = DGraph -> DGChange -> DGraph
changeDGH DGraph
auxDGraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
ledge
newDGraph :: DGraph
newDGraph = LEdge DGLinkLab -> DGraph -> DGraph
newEdge DGraph
newDGraph2
newRules :: DGRule
newRules = EdgeId -> DGRule
hideThmShiftRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
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
edge =
edge DGraph
dgraph of
e -> (DGraph
dgraph, ProofBasis -> EdgeId -> ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
e)
Nothing -> let
tempDGraph :: DGraph
tempDGraph = DGraph -> DGChange -> DGraph
changeDGH DGraph
dgraph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
edge
-- checks if the edge is actually inserted
tempProofBasis :: ProofBasis
tempProofBasis = case DGraph -> DGChange
getLastChange DGraph
tempDGraph of
tempE ->
ProofBasis -> EdgeId -> ProofBasis
proofbasis (EdgeId -> ProofBasis) -> EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
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 proofBasisEdges :: ProofBasis
ledge@(src :: Node
src, tgt :: Node
edgeLab) =
(Node
src, Node
edgeLab
setProof (DGRule -> ProofBasis -> ThmLinkStatus
Proven (EdgeId -> DGRule
hideThmShiftRule (EdgeId -> DGRule) -> EdgeId -> DGRule
forall a b. (a -> b) -> a -> b
ledge)
ProofBasis
proofBasisEdges)
forall a b. (a -> b) -> a -> b
edgeLab

-- | selects a proof basis for 'hide theorem shift' if there is one
-> ProofBaseSelector m -> m [LEdge DGLinkLab]
findProofBaseForHideTheoremShift :: DGraph
findProofBaseForHideTheoremShift dgraph :: DGraph
ledge@(src :: Node
src, tgt :: Node
lb)) proofBaseSel :: ProofBaseSelector m
proofBaseSel = do
let dgraph2 :: DGraph
dgraph2 = LEdge DGLinkLab -> DGraph -> DGraph
ledge DGraph
dgraph
pathsFromSrc = DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom DGraph
dgraph2 Node
src
pathsFromTgt = DGraph -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom DGraph
dgraph2 Node
tgt
pathsFromTgt
HidingFreeOrCofreeThm Nothing _ hidingMorphism :: GMorphism
lb
morphism :: GMorphism
lb
pathPairsFilteredByMorphism :: [PathTuple]
pathPairsFilteredByMorphism
-> GMorphism -> GMorphism -> [PathTuple]
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
forall (m :: * -> *) a. Monad m => a -> m a
forall a b. (a -> b) -> a -> b
\$ case Maybe PathTuple
pb of
Nothing -> []
forall a b. (a -> b) -> [a] -> [b]
sndPath]

-- | advoiding duplicate to be selected proofbasis.
filterPairsByGlobalProveStatus :: [PathTuple] -> [PathTuple]
filterPairsByGlobalProveStatus = (PathTuple -> Bool) -> [PathTuple] -> [PathTuple]
forall a. (a -> Bool) -> [a] -> [a]
filter PathTuple -> Bool
bothAreProven where
bothAreProven :: PathTuple -> Bool
pb2) = [LEdge DGLinkLab] -> Bool
pb1 Bool -> Bool -> Bool
pb2
allAreProven :: [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
forall a b. (a -> b) -> a -> b
l Bool -> Bool -> Bool
l)

{- removes all pairs from the given list whose second path does not have a
conservativity greater than or equal to Cons -}
filterPairsByConservativityOfSecondPath
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)
forall a b. (a -> b) -> [a] -> [b]
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
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\' -}
-> String
prettyPrintPathTuple :: DGraph -> PathTuple -> String
prettyPrintPathTuple dgraph :: DGraph
p2) =
DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath DGraph
p1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintPath DGraph
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
edge : path :: [LEdge DGLinkLab]
path) =
DGraph -> LEdge DGLinkLab -> String
prettyPrintSourceNode DGraph
edge String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath DGraph
path
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
end
where
end :: String
path of
[] -> DGraph -> LEdge DGLinkLab -> String
prettyPrintTargetNode DGraph
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
path =
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGraph -> [LEdge DGLinkLab] -> String
prettyPrintNodesOfPath DGraph
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 -}
path =
case ([LEdge DGLinkLab] -> Maybe GMorphism
path) of
(Just morphism :: GMorphism
morphism, (s :: Node
s, _, _) : _) ->
let (_, t :: Node
forall a. [a] -> a
path
in (Node
s, Node
_ -> 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 [] _ = []
selectPathPairs _ [] = []
paths2 =
forall a. [a] -> a
forall a. [a] -> a
p2) ] ) | [LEdge DGLinkLab]
paths1]

where
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. -}
-> GMorphism -> GMorphism
-> GMorphism -> GMorphism -> [PathTuple]
filterPairsByResultingMorphisms [] _ _ = []
pairs) morph1 :: GMorphism
morph1 morph2 :: GMorphism
morph2 =
forall a b. (a, b) -> a
suitingPaths]
[PathTuple] -> [PathTuple] -> [PathTuple]
forall a. [a] -> [a] -> [a]
-> GMorphism -> GMorphism -> [PathTuple]
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
forall a b. (a, b) -> a
pair))
suitingPaths = if Maybe GMorphism -> Bool
forall a. Maybe a -> Bool
isJust Maybe GMorphism
compMorph1 then
forall a b. (a, b) -> b
pair,
Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
compMaybeMorphisms (GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just GMorphism
morph2)
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
```