{- |
Module      :  $Header$
Description :  devGraph rule that calls provers for specific logics
Copyright   :  (c) J. Gerken, T. Mossakowski, K. Luettich, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

devGraph rule that calls provers for specific logics

Proof rule "basic inference" in the development graphs calculus.
   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.InferBasic
  ( basicInferenceNode
  ) where

import Static.GTheory
import Static.DevGraph
import Static.ComputeTheory

import Proofs.EdgeUtils
import Proofs.AbstractState
import Proofs.FreeDefLinks

import Common.LibName
import Common.Result
import Common.ResultT
import Common.AS_Annotation

import Logic.Logic
import Logic.Prover
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce

import Comorphisms.KnownProvers

import GUI.Utils
import GUI.ProverGUI

import Interfaces.DataTypes
import Interfaces.Utils

import Data.IORef
import Data.Graph.Inductive.Graph
import Data.Maybe

import Control.Monad.Trans

selectProver :: [(G_prover, AnyComorphism)]
             -> ResultT IO (G_prover, AnyComorphism)
selectProver ps = case ps of
  [] -> fail "No prover available"
  [p] -> return p
  _ -> do
   sel <- lift $ listBox "Choose a translation to a prover-supported logic"
     $ map (\ (aGN, cm) -> shows cm $ " (" ++ getProverName aGN ++ ")") ps
   i <- case sel of
           Just j -> return j
           _ -> fail "Proofs.Proofs: selection"
   return $ ps !! i

proveTheory :: Logic lid sublogics
              basic_spec sentence symb_items symb_map_items
              sign morphism symbol raw_symbol proof_tree
           => lid -> Prover sign sentence morphism sublogics proof_tree
           -> String -> Theory sign sentence proof_tree
           -> [FreeDefMorphism sentence morphism]
           -> IO ( [ProofStatus proof_tree]
                , [(Named sentence, ProofStatus proof_tree)])
proveTheory _ =
    fromMaybe (\ _ _ -> fail "proveGUI not implemented") . proveGUI


{- | applies basic inference to a given node. The result is a theory which is
     either a model after a consistency check or a new theory for the node
     label -}
basicInferenceNode :: LogicGraph -> LibName -> DGraph -> LNode DGNodeLab
                   -> LibEnv -> IORef IntState
                   -> IO (Result G_theory)
basicInferenceNode lg ln dGraph (node, lbl) libEnv intSt =
  runResultT $ do
    -- compute the theory (that may contain proved theorems) and its name
    thForProof <- liftR $ getGlobalTheory lbl
    let thName = shows (getLibId ln) "_" ++ getDGNodeName lbl
        freedefs = getCFreeDefMorphs libEnv ln dGraph node
    kpMap <- liftR knownProversGUI
    ResultT $ proverGUI ProofActions
      { proveF = proveKnownPMap lg intSt freedefs
      , fineGrainedSelectionF = proveFineGrainedSelect lg intSt freedefs
      , recalculateSublogicF = return . recalculateSublogicAndSelectedTheory
      } thName (hidingLabelWarning lbl) thForProof kpMap
      (getAllProvers ProveGUI (sublogicOfTh thForProof) lg)

proveKnownPMap :: LogicGraph
    -> IORef IntState
    -> [GFreeDefMorphism]
    -> ProofState -> IO (Result ProofState)
proveKnownPMap lg intSt freedefs st =
    maybe (proveFineGrainedSelect lg intSt freedefs st)
          (callProver st intSt False freedefs) $
          lookupKnownProver st ProveGUI

callProver :: ProofState
    -> IORef IntState
    -> Bool -- indicates if a translation was chosen
    -> [GFreeDefMorphism]
    -> (G_prover, AnyComorphism) -> IO (Result ProofState)
callProver st intSt trans_chosen freedefs p_cm@(_, acm) =
       runResultT $ do
        (_, exit) <- lift $ pulseBar "prepare for proving" "please wait..."
        G_theory_with_prover lid th p <- liftR $ prepareForProving st p_cm
        freedefs1 <- mapM (\ (GFreeDefMorphism fdlid fd) ->
                       coerceFreeDefMorphism fdlid lid "" fd) freedefs
        lift exit
        (ps, _) <- lift $ proveTheory lid p (theoryName st) th freedefs1
        let st' = markProved acm lid ps st
        lift $ addCommandHistoryToState intSt st'
              (if trans_chosen then Just p_cm else Nothing) ps
        return st'

proveFineGrainedSelect :: LogicGraph
    -> IORef IntState
    -> [GFreeDefMorphism]
    -> ProofState -> IO (Result ProofState)
proveFineGrainedSelect lg intSt freedefs st =
    runResultT $ do
       let sl = sublogicOfTheory st
           cmsToProvers = getAllProvers ProveGUI sl lg
       pr <- selectProver cmsToProvers
       ResultT $ callProver st { comorphismsToProvers = cmsToProvers }
                               intSt True freedefs pr
