hets/Proofs/TriangleCons.hs

	TriangleCons.hs revision c208973c890b8f993297720fd0247bc7481d4304


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
{- |
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 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

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) ->
                             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