TriangleCons.hs revision a77aecc59cee605ea48e33b65a627e0aa0a245e0
{- |
Module : $Header$
Description : apply triangle-cons rule for all edges in development graphs
Copyright : (c) Christian Maeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable(Logic)
-}
module Proofs.TriangleCons where
--import Logic.Grothendieck
import Static.DevGraph
import Static.History
import Common.Consistency
import Common.Result
import Common.LibName
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Graph.Inductive.Graph
import Control.Monad
import Debug.Trace
triangleConsRule :: DGRule
triangleConsRule = DGRule "TriangleCons"
triangleCons :: LibName -> LibEnv -> Result LibEnv
triangleCons ln le = do
let dg = lookupDGraph ln le
newDg <- foldM triangleConsDG dg $
filter (\ (_, _, l) -> let e = getRealDGLinkType l in
edgeTypeModInc e == GlobalDef
&& getCons (dgl_type l) == Cons
)
$ labEdgesDG dg
return $ Map.insert ln
(groupHistory dg triangleConsRule newDg) le
triangleConsDG :: DGraph -> LEdge DGLinkLab -> Result DGraph
triangleConsDG dg (s,t,l) = do
let g = dgBody dg
markCons l1 l2= let
l' = l{dgl_type = case dgl_type l of
ScopedLink a b _ ->
ScopedLink a b $
ConsStatus
Cons
Cons
$ Proven triangleConsRule $
ProofBasis $ Set.fromList $
map dgl_id [l1, l2]
dt -> dt}
in [DeleteEdge (s,t,l), InsertEdge (s,t,l')]
checkThm eType =
case eType of
ThmType (GlobalOrLocalThm _ _) _ _ _ -> True
_ -> False
oThm = filter (\ (_, _, ll) -> let e = getRealDGLinkType ll in
checkThm (edgeTypeModInc e)
) $ out g t
case oThm of
[] -> trace "1" $ return dg -- no outgoing thm link found
_ -> do
let bases = filter (\((s',_,_), _) -> s == s')
$ concatMap (\dge@(_, tt, _) ->
map (\x-> (x,dge))
$ filter (\ (_, _, lx) ->
let e = getRealDGLinkType lx in
-- edgeTypeModInc e == GlobalDef &&
getCons (dgl_type lx) == Cons
) $ inn g tt)
oThm
case bases of
[] -> trace "2" $ return dg -- no cons link found
((_, _, cl), (_, _, tl)):_ -> do
let changes = markCons cl tl
return $ changesDGH dg changes
--error "nyi"