ComputeTheory.hs revision 26210e52bda19c75ac6a4287d16ce9d8789b68de
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 MaederMaintainer : Christian.Maeder@dfki.de
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederStability : provisional
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederPortability : non-portable(Logic)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedercompute the theory of a node
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder ( computeTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , getGlobalTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , theoremsToAxioms
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeDGraphTheories
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeLibEnvTheories
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , computeLabelTheory
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , updateLabelTheory
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder , renumberDGLink
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport qualified Data.Map as Map
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder-- * nodes with incoming hiding definition links
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedernodeHasHiding :: DGraph -> Node -> Bool
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian MaedernodeHasHiding dg = labelHasHiding . labDG dg
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedernodeHasFree :: DGraph -> Node -> Bool
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaedernodeHasFree dg = labelHasFree . labDG dg
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder{- | mark all nodes if they have incoming hiding edges.
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder Assume reference nodes to other libraries being properly marked already.
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
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 MaedercomputeTheory :: LibEnv -> LibName -> Node -> Maybe G_theory
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedercomputeTheory libEnv ln = globalNodeTheory $ lookupDGraph ln libEnv
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
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedergetGlobalTheory :: DGNodeLab -> Result G_theory
002961cfb5c53204887101239d2a47c83d596585Christian MaedergetGlobalTheory = maybe (fail "no global theory") return . globalTheory
b7bba589fb78fe61379de93d531556c00da36cd9Christian MaederglobalNodeTheory :: DGraph -> Node -> Maybe G_theory
002961cfb5c53204887101239d2a47c83d596585Christian MaederglobalNodeTheory dg = globalTheory . labDG dg
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
1596a4d2cc01bff500afdd3789a43ec93210e81fChristian Maeder in foldl upd Map.empty lns
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
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
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
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 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 (flip $ comparing (\ (_, _, l) -> dgl_id l))
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder $ filter (liftE $ liftOr isGlobalDef isLocalDef)