SimpleTheoremHideShift.hs revision 697e63e30aa3c309a1ef1f9357745111f8dfc5a9
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederCopyright : (c) Cui Jian, Till Mossakowski, Uni Bremen 2002-2006
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederDescription : simple version of theorem hide shift proof rule
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : ken@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable(Logic)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maedersimple version of theorem hide shift proof rule for development graphs.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Extending Development Graphs With Hiding.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Lecture Notes in Computer Science 2029, p. 269-283,
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Springer-Verlag 2001.
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder it relates to the ticket 13
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder (theoremHideShift,
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder getInComingGlobalUnprovenEdges
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder{- | to be exported function.
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder firstly it gets all the hiding definition links out of DGraph and
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder passes them to theoremHideShiftFromList which does the actual processing
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedertheoremHideShift :: LIB_NAME -> LibEnv -> LibEnv
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedertheoremHideShift ln proofStatus =
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder let dgraph = lookupDGraph ln proofStatus
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder hidingDefEdges = filter (liftE isHidingDef) $ labEdgesDG dgraph
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (newDGraph, newHistory) = mapAccumL
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder theoremHideShiftFromList dgraph hidingDefEdges
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder in mkResultProofStatus ln proofStatus newDGraph
05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder (concatMap fst newHistory, concatMap snd newHistory)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder{- | apply the theorem hide shift with a list of hiding definition links.
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder it calls the function for one hiding edge at a time and fills the history
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder if necessary.
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedertheoremHideShiftFromList :: DGraph -> LEdge DGLinkLab
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder -> (DGraph, ([DGRule], [DGChange]))
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedertheoremHideShiftFromList dgraph e = let
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (newDGraph, newChanges) = theoremHideShiftWithOneHidingDefEdge dgraph e
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder in (newDGraph, ([TheoremHideShift], concat newChanges))
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder{- | apply the rule to one hiding definition link.
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder it takes all the related global unproven edges to the given hiding edge
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder and passes them together to its auxiliary function.
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedertheoremHideShiftWithOneHidingDefEdge :: DGraph -> LEdge DGLinkLab
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder -> (DGraph, [[DGChange]])
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus LuettichtheoremHideShiftWithOneHidingDefEdge dgraph e@(_, n, _) =
4e23d551da8fb051cc4752319740ae7858ef1044Christian Maeder mapAccumL (theoremHideShiftWithOneHidingDefEdgeAux e) dgraph
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder $ getInComingGlobalUnprovenEdges dgraph n
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder{- | get all the global unproven threorem links which go into the given
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder node in the given dgraph
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedergetInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedergetInComingGlobalUnprovenEdges dgraph =
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder filter (liftE isUnprovenGlobalThm) . innDG dgraph
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder{- | it's the main function of this simplified theorem hide shift.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder it applies the rule to a list of global unproven threorem links
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder with the related hiding definition link. It contains three steps
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder fulfilling the task and is marked below.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedertheoremHideShiftWithOneHidingDefEdgeAux :: LEdge DGLinkLab -> DGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> LEdge DGLinkLab
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -> (DGraph, [DGChange])
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedertheoremHideShiftWithOneHidingDefEdgeAux hd@(hds, _, _) dgraph x@(s, t, lbl) =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (finalDGraph, newChanges ++ finalChanges)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -------- to insert an unproven global theorem link ------------
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder newMorphism = case calculateMorphismOfPath [x, hd] of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Nothing -> error
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder "SimpleTheoremHideShift.theoremHideShiftWithOneHidingDefEdgeAux"
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder newGlobalEdge = (s, hds, DGLink
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder { dgl_morphism = newMorphism
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , dgl_type = GlobalThm LeftOpen None LeftOpen
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder , dgl_origin = DGLinkProof
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder , dgl_id = defaultEdgeId})
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder ((newDGraph, newChanges), proofbasis) =
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder tryToInsertEdgeAndSelectProofBasis dgraph newGlobalEdge emptyProofBasis
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder -------- to insert a proven global theorem link ---------------
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder GlobalThm _ conservativity conservStatus = dgl_type lbl
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder provenEdge = (s, t, lbl
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder { dgl_type = GlobalThm (Proven TheoremHideShift proofbasis)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder conservativity conservStatus
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder , dgl_origin = DGLinkProof })
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder (finalDGraph, finalChanges) = updateWithChanges
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [DeleteEdge x, InsertEdge provenEdge] newDGraph
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder{- | it tries to insert the given edge into the DGraph and selects the
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder inserted edge as proof basis if possible.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedertryToInsertEdgeAndSelectProofBasis :: DGraph -> LEdge DGLinkLab -> ProofBasis
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -> ((DGraph, [DGChange]), ProofBasis)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedertryToInsertEdgeAndSelectProofBasis dgraph newEdge proofbasis =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case tryToGetEdge newEdge dgraph of
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder Just tempE -> ((dgraph, []), addEdgeId proofbasis $ getEdgeId tempE)
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder Nothing -> let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (tempDGraph, tempChanges) =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder updateWithOneChange (InsertEdge newEdge) dgraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tempPB = case tempChanges of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder [InsertEdge tempE] -> addEdgeId proofbasis $ getEdgeId tempE
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder "SimpleTheoremHideShift.tryToInsertEdgeAndSelectProofBasis"
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder in ((tempDGraph, tempChanges), tempPB)