ComputeTheory.hs revision 26210e52bda19c75ac6a4287d16ce9d8789b68de
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder{- |
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederModule : $Header$
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederDescription : compute the theory of a node
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederCopyright : (c) Christian Maeder and DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederMaintainer : Christian.Maeder@dfki.de
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederStability : provisional
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederPortability : non-portable(Logic)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedercompute the theory of a node
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder-}
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maedermodule Static.ComputeTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder ( computeTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , getGlobalTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , theoremsToAxioms
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeDGraphTheories
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeLibEnvTheories
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeLabelTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , updateLabelTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , markHiding
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , markFree
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder , renumberDGLink
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder ) where
002961cfb5c53204887101239d2a47c83d596585Christian Maeder
9f7cd2db42cbc88253af8034f8d1fb83e1ecd4cdChristian Maederimport Logic.Prover
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maederimport Static.GTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maederimport Static.DevGraph
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maederimport Static.DgUtils
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maederimport Static.History
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Common.LibName
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Common.Result
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederimport Data.Graph.Inductive.Graph as Graph
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maederimport Data.List (sortBy)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport qualified Data.Map as Map
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederimport Data.Ord
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder-- * nodes with incoming hiding definition links
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedernodeHasHiding :: DGraph -> Node -> Bool
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian MaedernodeHasHiding dg = labelHasHiding . labDG dg
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedernodeHasFree :: DGraph -> Node -> Bool
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaedernodeHasFree dg = labelHasFree . labDG dg
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder{- | mark all nodes if they have incoming hiding edges.
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder Assume reference nodes to other libraries being properly marked already.
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder-}
720eeee7c9d8442093c8d05bed743193eee906e0Christian MaedermarkFree :: LibEnv -> DGraph -> DGraph
720eeee7c9d8442093c8d05bed743193eee906e0Christian MaedermarkFree le dgraph =
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder foldl (\ dg (n, lbl) -> let
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder ingoingEdges = innDG dg n
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder defEdges = filter (liftE isDefEdge) ingoingEdges
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder freeDefEdges = filter (liftE isFreeEdge ) defEdges
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder in fst $ labelNodeDG (n, lbl { labelHasFree =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder if isDGRef lbl
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder then nodeHasFree (lookupDGraph (dgn_libname lbl) le)
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder $ dgn_node lbl
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder else not (null freeDefEdges) }) dg)
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder dgraph $ topsortedNodes dgraph
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaedermarkHiding :: LibEnv -> DGraph -> DGraph
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedermarkHiding le dgraph =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder foldl (\ dg (n, lbl) -> let
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder ingoingEdges = innDG dg n
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder defEdges = filter (liftE isDefEdge) ingoingEdges
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder hidingDefEdges = filter (liftE isHidingDef ) defEdges
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder next = map (\ (s, _, _) -> s) defEdges
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder in fst $ labelNodeDG (n, lbl { labelHasHiding =
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder if isDGRef lbl
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder then nodeHasHiding (lookupDGraph (dgn_libname lbl) le)
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder $ dgn_node lbl
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder else not (null hidingDefEdges) || any (nodeHasHiding dg) next }) dg)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder dgraph $ topsortedNodes dgraph
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedercomputeTheory :: LibEnv -> LibName -> Node -> Maybe G_theory
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedercomputeTheory libEnv ln = globalNodeTheory $ lookupDGraph ln libEnv
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedertheoremsToAxioms :: G_theory -> G_theory
002961cfb5c53204887101239d2a47c83d596585Christian MaedertheoremsToAxioms (G_theory lid sign ind1 sens ind2) =
002961cfb5c53204887101239d2a47c83d596585Christian Maeder G_theory lid sign ind1 (markAsAxiom True sens) ind2
002961cfb5c53204887101239d2a47c83d596585Christian Maeder
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedergetGlobalTheory :: DGNodeLab -> Result G_theory
002961cfb5c53204887101239d2a47c83d596585Christian MaedergetGlobalTheory = maybe (fail "no global theory") return . globalTheory
b7bba589fb78fe61379de93d531556c00da36cd9Christian Maeder
b7bba589fb78fe61379de93d531556c00da36cd9Christian MaederglobalNodeTheory :: DGraph -> Node -> Maybe G_theory
002961cfb5c53204887101239d2a47c83d596585Christian MaederglobalNodeTheory dg = globalTheory . labDG dg
002961cfb5c53204887101239d2a47c83d596585Christian Maeder
11c3a215d5cf043181e83929f1ce214df65cb587Christian MaedercomputeLibEnvTheories :: LibEnv -> LibEnv
9005b07df2277a9fefca6868cd00c1c39533a9fbChristian MaedercomputeLibEnvTheories le =
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder let lns = getTopsortedLibs le
9f7cd2db42cbc88253af8034f8d1fb83e1ecd4cdChristian Maeder upd le' ln = let dg0 = lookupDGraph ln le
9f7cd2db42cbc88253af8034f8d1fb83e1ecd4cdChristian Maeder dg = computeDGraphTheories le' dg0
9f7cd2db42cbc88253af8034f8d1fb83e1ecd4cdChristian Maeder in Map.insert ln dg le'
1596a4d2cc01bff500afdd3789a43ec93210e81fChristian Maeder in foldl upd Map.empty lns
1596a4d2cc01bff500afdd3789a43ec93210e81fChristian Maeder
002961cfb5c53204887101239d2a47c83d596585Christian MaedercomputeDGraphTheories :: LibEnv -> DGraph -> DGraph
429df04296fa571432f62cbfad6855e1420e0fd6Christian MaedercomputeDGraphTheories le dgraph =
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let newDg = computeDGraphTheoriesAux le dgraph
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder in groupHistory dgraph (DGRule "Compute theory") newDg
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder
fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst SchulzrecomputeNodeLabel :: LibEnv -> DGraph -> LNode DGNodeLab -> DGNodeLab
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaederrecomputeNodeLabel le dg l@(n, lbl) =
fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz case computeLabelTheory le dg l of
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder gTh@(Just th) ->
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder let (chg, lbl1) = case globalTheory lbl of
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Nothing -> (False, lbl)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Just oTh -> (True, lbl
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder { dgn_theory = invalidateProofs oTh th $ dgn_theory lbl })
14d7908303969441ba30c2748de45f20345c6b31Christian Maeder ngTh = if chg then computeLabelTheory le dg (n, lbl1) else gTh
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in case ngTh of
54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder Just nth@(G_theory _ _ _ sens _) ->
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder (if Map.null sens then markNodeConsistent "ByNoSentences" lbl1
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder else lbl1 { dgn_theory = proveLocalSens nth (dgn_theory lbl1) })
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder { globalTheory = ngTh }
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder Nothing -> lbl1
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Nothing -> lbl
54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedercomputeDGraphTheoriesAux :: LibEnv -> DGraph -> DGraph
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedercomputeDGraphTheoriesAux le dgraph =
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder foldl (\ dg l@(n, lbl) -> updatePending dg lbl
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder (n, recomputeNodeLabel le dg l))
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder dgraph $ topsortedNodes dgraph
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedercomputeLabelTheory :: LibEnv -> DGraph -> LNode DGNodeLab -> Maybe G_theory
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian MaedercomputeLabelTheory le dg (n, lbl) = let localTh = dgn_theory lbl in
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder fmap reduceTheory . maybeResult $ if isDGRef lbl then
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder case Map.lookup (dgn_libname lbl) le of
54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder Nothing -> return localTh -- do not crash here
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Just dg' -> do
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder refTh <- getGlobalTheory $ labDG dg' $ dgn_node lbl
e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst Schulz joinG_sentences refTh localTh
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz else do
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz ths <- mapM (\ (s, _, l) -> do
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder th <- let sl = labDG dg s in if isLocalDef $ dgl_type l then
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder return $ dgn_theory sl
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder else getGlobalTheory sl
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder -- translate theory and turn all imported theorems into axioms
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder translateG_theory (dgl_morphism l) $ theoremsToAxioms th)
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder $ sortBy
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder (flip $ comparing (\ (_, _, l) -> dgl_id l))
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder $ filter (liftE $ liftOr isGlobalDef isLocalDef)
$ innDG dg n
flatG_sentences localTh ths
reduceTheory :: G_theory -> G_theory
reduceTheory (G_theory lid sig ind sens _) =
G_theory lid sig ind (reduceSens sens) startThId
updateLabelTheory :: LibEnv -> DGraph -> LNode DGNodeLab -> G_theory -> DGraph
updateLabelTheory le dg (i, l) gth = let
l' = l { dgn_theory = gth }
n = (i, l' { globalTheory = computeLabelTheory le dg (i, l') })
in updatePending dg l n
updatePending :: DGraph
-> DGNodeLab -- ^ old label
-> LNode DGNodeLab -- ^ node with new label
-> DGraph
updatePending dg l n = let
dg0 = changeDGH dg $ SetNodeLab l n
dg1 = togglePending dg0 $ changedLocalTheorems dg0 n
dg2 = togglePending dg1 $ changedPendingEdges dg1
in groupHistory dg (DGRule "Node proof") dg2
renumberDGLink :: EdgeId -> EdgeId -> DGraph -> DGraph
renumberDGLink i ni dg = changesDGH dg
$ foldr (\ e@(s, t, l) -> if dgl_id l == i then
([DeleteEdge e, InsertEdge (s, t, l { dgl_id = ni })] ++)
else let pB = getProofBasis l in
if edgeInProofBasis i pB then
([ DeleteEdge e, InsertEdge (s, t, l
{ dgl_type = updThmProofBasis (dgl_type l) $ updEdgeId pB i ni })] ++)
else id) [] $ labEdgesDG dg