{- |
Module      :  ./Proofs/Automatic.hs
Description :  automatic proofs in the development graph calculus
Copyright   :  (c) Jorina F. Gerken, Mossakowski, Luettich, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

automatic proofs in development graphs.
   Follows Sect. IV:4.4 of the CASL Reference Manual.
-}

{-
   References:

   T. Mossakowski, S. Autexier and D. Hutter:
   Extending Development Graphs With Hiding.
   H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
   Lecture Notes in Computer Science 2029, p. 269-283,
   Springer-Verlag 2001.

-}

module Proofs.Automatic (automatic, automaticFromList) where

import Proofs.Global
import Proofs.Local
import Proofs.HideTheoremShift
import Proofs.TheoremHideShift

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.LibName
import qualified Common.Lib.SizedList as SizedList

import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.Graph.Inductive.Graph
import Common.Result

automaticFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticFromList ln :: LibName
ln ls :: [LEdge DGLinkLab]
ls libEnv :: LibEnv
libEnv =
  let x :: LibEnv
x = LibName -> LibEnv -> [LEdge DGLinkLab] -> LibEnv
automaticRecursiveFromList LibName
ln LibEnv
libEnv [LEdge DGLinkLab]
ls
      y :: LibEnv
y = LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
localInferenceFromList LibName
ln [LEdge DGLinkLab]
ls LibEnv
x
  in LibEnv
y

noChange :: LibEnv -> LibEnv -> Bool
noChange :: LibEnv -> LibEnv -> Bool
noChange oldLib :: LibEnv
oldLib newLib :: LibEnv
newLib = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ Map LibName Bool -> [Bool]
forall k a. Map k a -> [a]
Map.elems (Map LibName Bool -> [Bool]) -> Map LibName Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ (DGraph -> DGraph -> Bool) -> LibEnv -> LibEnv -> Map LibName Bool
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith
  (\ a :: DGraph
a b :: DGraph
b -> SizedList HistElem -> Bool
forall a. SizedList a -> Bool
SizedList.null (SizedList HistElem -> Bool)
-> ((SizedList HistElem, SizedList HistElem) -> SizedList HistElem)
-> (SizedList HistElem, SizedList HistElem)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SizedList HistElem, SizedList HistElem) -> SizedList HistElem
forall a b. (a, b) -> b
snd ((SizedList HistElem, SizedList HistElem) -> Bool)
-> (SizedList HistElem, SizedList HistElem) -> Bool
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph -> (SizedList HistElem, SizedList HistElem)
splitHistory DGraph
a DGraph
b) LibEnv
oldLib LibEnv
newLib

automaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab]
                           -> LibEnv
automaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab] -> LibEnv
automaticRecursiveFromList ln :: LibName
ln proofstatus :: LibEnv
proofstatus ls :: [LEdge DGLinkLab]
ls =
  let auxProofstatus :: LibEnv
auxProofstatus = LibName
-> [LEdge DGLinkLab]
-> LibEnv
-> [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
-> LibEnv
automaticApplyRulesToGoals LibName
ln [LEdge DGLinkLab]
ls LibEnv
proofstatus
                                                  [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
rulesWithGoals
  in if LibEnv -> LibEnv -> Bool
noChange LibEnv
proofstatus LibEnv
auxProofstatus then LibEnv
auxProofstatus
     else LibName -> LibEnv -> [LEdge DGLinkLab] -> LibEnv
automaticRecursiveFromList LibName
ln LibEnv
auxProofstatus [LEdge DGLinkLab]
ls

{- | automatically applies all rules to the library
   denoted by the library name of the given proofstatus -}
automatic :: LibName -> LibEnv -> LibEnv
automatic :: LibName -> LibEnv -> LibEnv
automatic ln :: LibName
ln le :: LibEnv
le = let nLib :: LibEnv
nLib = LibName -> LibEnv -> LibEnv
localInference LibName
ln (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ Int -> LibName -> LibEnv -> LibEnv
automaticRecursive 49 LibName
ln LibEnv
le in
  (DGraph -> DGraph -> DGraph) -> LibEnv -> LibEnv -> LibEnv
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (\ odg :: DGraph
odg ndg :: DGraph
ndg ->
      DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
odg (String -> DGRule
DGRule "automatic") DGraph
ndg) LibEnv
le LibEnv
nLib

-- | applies the rules recursively until no further changes can be made
automaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
automaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
automaticRecursive count :: Int
count ln :: LibName
ln proofstatus :: LibEnv
proofstatus =
  let auxProofstatus :: LibEnv
auxProofstatus = LibName -> LibEnv -> LibEnv
automaticApplyRules LibName
ln LibEnv
proofstatus
  in if LibEnv -> LibEnv -> Bool
noChange LibEnv
proofstatus LibEnv
auxProofstatus Bool -> Bool -> Bool
|| Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then LibEnv
auxProofstatus
     else Int -> LibName -> LibEnv -> LibEnv
automaticRecursive (Int
count Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) LibName
ln LibEnv
auxProofstatus

wrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
wrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
wrapTheoremHideShift ln :: LibName
ln libEnv :: LibEnv
libEnv = LibEnv -> Maybe LibEnv -> LibEnv
forall a. a -> Maybe a -> a
fromMaybe LibEnv
libEnv
 (Result LibEnv -> Maybe LibEnv
forall a. Result a -> Maybe a
maybeResult (Result LibEnv -> Maybe LibEnv) -> Result LibEnv -> Maybe LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> Result LibEnv
theoremHideShift LibName
ln LibEnv
libEnv)

-- | list of rules to use
rules :: [LibName -> LibEnv -> LibEnv]
rules :: [LibName -> LibEnv -> LibEnv]
rules =
    [ LibName -> LibEnv -> LibEnv
automaticHideTheoremShift
    , LibName -> LibEnv -> LibEnv
globDecomp
    , LibName -> LibEnv -> LibEnv
wrapTheoremHideShift
    ]

rulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
rulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
rulesWithGoals =
            [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
automaticHideTheoremShiftFromList
            , LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
locDecompFromList
            , LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globDecompFromList
            , LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
globSubsumeFromList
            ]

automaticApplyRulesToGoals :: LibName -> [LEdge DGLinkLab] -> LibEnv ->
                 [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv] -> LibEnv
automaticApplyRulesToGoals :: LibName
-> [LEdge DGLinkLab]
-> LibEnv
-> [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
-> LibEnv
automaticApplyRulesToGoals ln :: LibName
ln ls :: [LEdge DGLinkLab]
ls libEnv :: LibEnv
libEnv ll :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
ll =
 case [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
ll of
     [] -> LibEnv
libEnv
     f :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
f : l :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
l -> let nwLibEnv :: LibEnv
nwLibEnv = LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
f LibName
ln [LEdge DGLinkLab]
ls LibEnv
libEnv
                  dgraph :: DGraph
dgraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
nwLibEnv
                  updateList :: [LEdge DGLinkLab]
updateList = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter
                                (\ (_, _, lp :: DGLinkLab
lp) ->
                                   case DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus
                                         (DGLinkType -> Maybe ThmLinkStatus)
-> DGLinkType -> Maybe ThmLinkStatus
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lp of
                                    Just LeftOpen -> Bool
True
                                    _ -> Bool
False) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph
           in LibName
-> [LEdge DGLinkLab]
-> LibEnv
-> [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
-> LibEnv
automaticApplyRulesToGoals LibName
ln [LEdge DGLinkLab]
updateList LibEnv
nwLibEnv [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
l

{- | sequentially applies all rules to the given proofstatus,
   ie to the library denoted by the library name of the proofstatus -}
automaticApplyRules :: LibName -> LibEnv -> LibEnv
automaticApplyRules :: LibName -> LibEnv -> LibEnv
automaticApplyRules ln :: LibName
ln = ((LibEnv -> LibEnv) -> (LibEnv -> LibEnv) -> LibEnv -> LibEnv)
-> (LibEnv -> LibEnv) -> [LibEnv -> LibEnv] -> LibEnv -> LibEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (LibEnv -> LibEnv) -> (LibEnv -> LibEnv) -> LibEnv -> LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) LibEnv -> LibEnv
forall a. a -> a
id ([LibEnv -> LibEnv] -> LibEnv -> LibEnv)
-> [LibEnv -> LibEnv] -> LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ ((LibName -> LibEnv -> LibEnv) -> LibEnv -> LibEnv)
-> [LibName -> LibEnv -> LibEnv] -> [LibEnv -> LibEnv]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: LibName -> LibEnv -> LibEnv
f -> LibName -> LibEnv -> LibEnv
f LibName
ln) [LibName -> LibEnv -> LibEnv]
rules