content: {- |
  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 ln ls libEnv =
    let x = automaticRecursiveFromList ln libEnv ls
        y = localInferenceFromList ln ls x
    in y
  
  noChange :: LibEnv -> LibEnv -> Bool
  noChange oldLib newLib = and $ Map.elems $ Map.intersectionWith
    (\ a b -> SizedList.null . snd $ splitHistory a b) oldLib newLib
  
  automaticRecursiveFromList :: LibName -> LibEnv -> [LEdge DGLinkLab]
                             -> LibEnv
  automaticRecursiveFromList ln proofstatus ls =
    let auxProofstatus = automaticApplyRulesToGoals ln ls proofstatus
                                                    rulesWithGoals
    in if noChange proofstatus auxProofstatus then auxProofstatus
       else automaticRecursiveFromList ln auxProofstatus ls
  
  {- | automatically applies all rules to the library
     denoted by the library name of the given proofstatus -}
  automatic :: LibName -> LibEnv -> LibEnv
  automatic ln le = let nLib = localInference ln $ automaticRecursive 49 ln le in
    Map.intersectionWith (\ odg ndg ->
        groupHistory odg (DGRule "automatic") ndg) le nLib
  
  -- | applies the rules recursively until no further changes can be made
  automaticRecursive :: Int -> LibName -> LibEnv -> LibEnv
  automaticRecursive count ln proofstatus =
    let auxProofstatus = automaticApplyRules ln proofstatus
    in if noChange proofstatus auxProofstatus || count < 1 then auxProofstatus
       else automaticRecursive (count - 1) ln auxProofstatus
  
  wrapTheoremHideShift :: LibName -> LibEnv -> LibEnv
  wrapTheoremHideShift ln libEnv = fromMaybe libEnv
   (maybeResult $ theoremHideShift ln libEnv)
  
  -- | list of rules to use
  rules :: [LibName -> LibEnv -> LibEnv]
  rules =
      [ automaticHideTheoremShift
      , globDecomp
      , wrapTheoremHideShift
      ]
  
  rulesWithGoals :: [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv]
  rulesWithGoals =
              [automaticHideTheoremShiftFromList
              , locDecompFromList
              , globDecompFromList
              , globSubsumeFromList
              ]
  
  automaticApplyRulesToGoals :: LibName -> [LEdge DGLinkLab] -> LibEnv ->
                   [LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv] -> LibEnv
  automaticApplyRulesToGoals ln ls libEnv ll =
   case ll of
       [] -> libEnv
       f : l -> let nwLibEnv = f ln ls libEnv
                    dgraph = lookupDGraph ln nwLibEnv
                    updateList = filter
                                  (\ (_, _, lp) ->
                                     case thmLinkStatus
                                           $ dgl_type lp of
                                      Just LeftOpen -> True
                                      _ -> False) $ labEdgesDG dgraph
             in automaticApplyRulesToGoals ln updateList nwLibEnv 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 ln = foldl (.) id $ map (\ f -> f ln) rules
  