{- |

Module : ./Proofs/TriangleCons.hs

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 Static.DevGraph

import Static.DgUtils

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

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

[] -> return dg -- no outgoing thm link found

_ -> do

let bases = filter (\ ((s', _, _), _) -> s == s')

$ concatMap (\ dge@(_, tt, _) ->

map (\ x -> (x, dge))

$ filter (\ (_, _, lx) ->

getCons (dgl_type lx) == Cons

) $ inn g tt)

oThm

case bases of

[] -> return dg -- no cons link found

((_, _, cl), (_, _, tl)) : _ -> do

let changes = markCons cl tl

return $ changesDGH dg changes