locDecompFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList ln localThmEdges libEnv=
let dgraph = lookupDGraph ln libEnv
finalLocalThmEdges = filter (liftE isUnprovenLocalThm) localThmEdges
(nextDGraph, nextHistoryElem) =
locDecompAux libEnv ln dgraph ([],[]) finalLocalThmEdges
in mkResultProofStatus ln libEnv nextDGraph nextHistoryElem
locDecomp :: LIB_NAME -> LibEnv -> LibEnv
let dgraph = lookupDGraph ln libEnv
localThmEdges = labEdgesDG dgraph
in locDecompFromList ln localThmEdges libEnv
{- auxiliary function for locDecomp (above)
locDecompAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
-> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
locDecompAux _ _ dgraph historyElement [] = (dgraph, historyElement)
locDecompAux libEnv ln dgraph (rules,changes)
(ledge@(src, tgt, edgeLab) : list) =
if not (isIdentityEdge ledge libEnv dgraph) && nullProofBasis proofbasis
locDecompAux libEnv ln dgraph (rules, changes) list
locDecompAux libEnv ln newGraph (newRules,newChanges) list
morphism = dgl_morphism edgeLab
allPaths = getAllLocGlobPathsBetween dgraph src tgt
th = computeLocalTheory libEnv ln src
pathsWithoutEdgeItself = filter (noPath ledge) allPaths
filteredPaths = filterByTranslation th morphism pathsWithoutEdgeItself
proofbasis = selectProofBasis dgraph ledge filteredPaths
updateWithOneChange (DeleteEdge ledge) dgraph changes
LocalThm _ conservativity conservStatus = dgl_type edgeLab
DGLink {dgl_morphism = morphism,
(LocalThm (Proven (LocDecomp ledge) proofbasis)
conservativity conservStatus),
insertDGLEdge newEdge auxGraph auxChanges
--updateWithChanges [DeleteEdge ledge, InsertEdge newEdge] dgraph changes
newRules = LocDecomp ledge : rules
{- | removes all paths from the given list of paths whose morphism does
not translate the given sentence list to the same resulting sentence
list as the given morphism. -}
filterByTranslation :: Maybe G_theory -> GMorphism -> [[LEdge DGLinkLab]]
filterByTranslation maybeTh morphism paths =
Just th -> filter (isSameTranslation th morphism) paths
{- | checks if the given morphism and the morphism of the given path
translate the given sentence list to the same resulting sentence list. -}
isSameTranslation :: G_theory -> GMorphism -> [LEdge DGLinkLab] -> Bool
isSameTranslation th morphism path =
case calculateMorphismOfPath path of
maybeResult (translateG_theory morphism th) ==
maybeResult (translateG_theory morphismOfPath th)
-- ----------------------------------------------
-- ----------------------------------------------
localInferenceFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
localInferenceFromList ln localThmEdges libEnv =
let dgraph = lookupDGraph ln libEnv
finalLocalThmEdges = filter (liftE isUnprovenLocalThm) localThmEdges
(nextDGraph, nextHistoryElem) =
localInferenceAux libEnv ln dgraph ([],[]) finalLocalThmEdges
in mkResultProofStatus ln libEnv nextDGraph nextHistoryElem
localInference :: LIB_NAME -> LibEnv -> LibEnv
localInference ln libEnv =
let dgraph = lookupDGraph ln libEnv
localThmEdges = filter (liftE isUnprovenLocalThm) (labEdgesDG dgraph)
in localInferenceFromList ln localThmEdges libEnv
-- auxiliary method for localInference
localInferenceAux :: LibEnv -> LIB_NAME -> DGraph -> ([DGRule],[DGChange])
-> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))
localInferenceAux _ _ dgraph (rules, changes) [] =
(dgraph, (reverse rules, reverse changes))
localInferenceAux libEnv ln dgraph (rules, changes)
(ledge@(src,tgt,edgeLab) : list) =
case (maybeResult (computeTheory libEnv ln tgt),
maybeResult (translateG_theory morphism thSrc)) of
(Just (G_theory lidTgt _ _ sensTgt _),
Just (G_theory lidSrc _ _ sensSrc _)) ->
case maybeResult (coerceThSens lidTgt lidSrc "" sensTgt) of
Nothing -> localInferenceAux libEnv ln dgraph (rules,changes) list
-- check if all source axioms are also axioms in the target
goals' = markAsGoal goals
newTh = case (dgn_theory oldContents) of
G_theory lid sig ind sens ind' ->
case coerceThSens lidSrc lid "" goals' of
Nothing -> G_theory lid sig ind sens ind'
(sens `joinSens` goals'') 0
let (newGraph, newChanges) =
[DeleteEdge ledge, InsertEdge newEdge]
in localInferenceAux libEnv ln newGraph
(newRules,newChanges) list
let newContents = oldContents{dgn_theory = newTh}
, SetNodeLab (error "localInferenceAux")
in localInferenceAux newLibEnv ln newGraph
(newRules,newChanges) list
_ -> localInferenceAux libEnv ln dgraph (rules,changes) list
_ -> localInferenceAux libEnv ln dgraph (rules,changes) list
morphism = dgl_morphism edgeLab
maybeThSrc = computeLocalTheory libEnv ln src
LocalThm _ conservativity conservStatus = dgl_type edgeLab
-- notice that the original id from edgeLab is kept
{ dgl_morphism = morphism
, dgl_type = LocalThm (Proven (LocInference ledge) emptyProofBasis)
conservativity conservStatus
, dgl_id = dgl_id edgeLab}
newEdge = (src, tgt, newLab)
newRules = LocInference ledge : rules
oldContents = labDG dgraph tgt