{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
{- |
Module      :  $Header$
Description :  State data structure used by the goal management GUI.
Copyright   :  (c) Uni Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

The 'ProofState' data structure abstracts the GUI implementation details
away by allowing callback function to use it as the sole input and output.
It is also used by the CMDL interface.
-}

module Proofs.AbstractState
    ( ProverOrConsChecker (..)
    , G_prover (..)
    , G_proof_tree (..)
    , getProverName
    , getCcName
    , getCcBatch
    , coerceProver
    , G_cons_checker (..)
    , coerceConsChecker
    , ProofActions (..)
    , ProofState (..)
    , sublogicOfTheory
    , logicId
    , initialState
    , resetSelection
    , toAxioms
    , getAxioms
    , getGoals
    , recalculateSublogicAndSelectedTheory
    , markProved
    , G_theory_with_prover (..)
    , G_theory_with_cons_checker (..)
    , prepareForProving
    , prepareForConsChecking
    , isSubElemG
    , pathToComorphism
    , getAllProvers
    , getUsableProvers
    , getConsCheckers
    , getAllConsCheckers
    , lookupKnownProver
    , lookupKnownConsChecker
    , autoProofAtNode
    ) where

import qualified Data.Map as Map
import Data.Maybe
import Data.Typeable

import Control.Concurrent.MVar
import Control.Monad.Trans
import Control.Monad

import qualified Common.OrderedMap as OMap
import Common.Result as Result
import Common.ResultT
import Common.AS_Annotation
import Common.ExtSign
import Common.Utils
import Common.GraphAlgo (yen)

import Unsafe.Coerce (unsafeCoerce)

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

import Comorphisms.KnownProvers

import Static.GTheory

-- import Interfaces.DataTypes (IntState)

-- * Provers

data ProverOrConsChecker = Prover G_prover
                         | ConsChecker G_cons_checker
                         deriving (Show)

-- | provers and consistency checkers for specific logics
data G_prover =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
  deriving Typeable

instance Show G_prover where
  show = getProverName

getProverName :: G_prover -> String
getProverName (G_prover _ p) = proverName p

usable :: G_prover -> IO Bool
usable (G_prover _ p) = fmap isNothing $ proverUsable p

coerceProver ::
  ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
  , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
  , Monad m )
  => lid1 -> lid2 -> String
  -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
  -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
coerceProver = primCoerce

data G_cons_checker =
  forall lid sublogics basic_spec sentence symb_items
    symb_map_items sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items
      symb_map_items sign morphism symbol raw_symbol proof_tree
  => G_cons_checker lid
       (ConsChecker sign sentence sublogics morphism proof_tree)
  deriving (Typeable)

instance Show G_cons_checker where
 show _ = "G_cons_checker "

getCcName :: G_cons_checker -> String
getCcName (G_cons_checker _ p) = ccName p

getCcBatch :: G_cons_checker -> Bool
getCcBatch (G_cons_checker _ p) = ccBatch p

usableCC :: G_cons_checker -> IO Bool
usableCC (G_cons_checker _ p) = fmap isNothing $ ccUsable p

coerceConsChecker ::
  ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
  , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
  , Monad m )
  => lid1 -> lid2 -> String
  -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
  -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
coerceConsChecker = primCoerce


-- | provers and consistency checkers for specific logics
data G_proof_tree =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_proof_tree lid proof_tree
  deriving Typeable
instance Show G_proof_tree where
  show (G_proof_tree _ pt) = show pt

-- | Possible actions for GUI which are manipulating ProofState
data ProofActions = ProofActions {
    -- | called whenever the "Prove" button is clicked
    proveF :: ProofState
      -> IO (Result.Result ProofState),
    -- | called whenever the "More fine grained selection" button is clicked
    fineGrainedSelectionF :: ProofState
      -> IO (Result.Result ProofState),
    -- | called whenever a (de-)selection occured for updating sublogic
    recalculateSublogicF :: ProofState
      -> IO ProofState
  }

{- |
  Represents the global state of the prover GUI.
-}
data ProofState =
     ProofState
      { -- | theory name
        theoryName :: String,
        -- | Grothendieck theory
        currentTheory :: G_theory,
        -- | currently known provers
        proversMap :: KnownProversMap,
        -- | currently selected goals
        selectedGoals :: [String],
        -- | axioms to include for the proof
        includedAxioms :: [String],
        -- | theorems to include for the proof
        includedTheorems :: [String],
        -- | whether a prover is running or not
        proverRunning :: Bool,
        -- | accumulated Diagnosis during Proofs
        accDiags :: [Diagnosis],
        -- | comorphisms fitting with sublogic of this G_theory
        comorphismsToProvers :: [(G_prover, AnyComorphism)],
        -- | which prover (if any) is currently selected
        selectedProver :: Maybe String,
        -- | which consistency checker (if any) is currently selected
        selectedConsChecker :: Maybe String,
        -- | theory based on selected goals, axioms and proven theorems
        selectedTheory :: G_theory
      } deriving Show

resetSelection :: ProofState -> ProofState
resetSelection s = case currentTheory s of
  G_theory _ _ _ _ sens _ ->
    let (aMap, gMap) = OMap.partition isAxiom sens
        gs = Map.keys gMap
    in s
    { selectedGoals = Map.keys gMap
    , includedAxioms = Map.keys aMap
    , includedTheorems = gs }

toAxioms :: ProofState -> [String]
toAxioms = map (\ (k, wTh) -> if wTh then "(Th) " ++ k else k)
  . getAxioms

getAxioms :: ProofState -> [(String, Bool)]
getAxioms = getThAxioms . currentTheory

getGoals :: ProofState -> [(String, Maybe BasicProof)]
getGoals = getThGoals . currentTheory

{- |
  Creates an initial State.
-}
initialState :: String
    -> G_theory
    -> KnownProversMap
    -> ProofState
initialState thN th pm = resetSelection
       ProofState
         { theoryName = thN
         , currentTheory = th
         , proversMap = pm
         , selectedGoals = []
         , includedAxioms = []
         , includedTheorems = []
         , proverRunning = False
         , accDiags = []
         , comorphismsToProvers = []
         , selectedProver =
             let prvs = Map.keys pm
             in if null prvs
                then Nothing
                else
                    if defaultGUIProver `elem` prvs
                    then Just defaultGUIProver
                    else Nothing
         , selectedConsChecker = Nothing
         , selectedTheory = th }

logicId :: ProofState -> String
logicId s = case currentTheory s of
  G_theory lid _ _ _ _ _ -> language_name lid

sublogicOfTheory :: ProofState -> G_sublogics
sublogicOfTheory = sublogicOfTh . selectedTheory

data G_theory_with_cons_checker =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_theory_with_cons_checker lid
       (TheoryMorphism sign sentence morphism proof_tree)
       (ConsChecker sign sentence sublogics morphism proof_tree)

-- | a Grothendieck pair of prover and theory which are in the same logic
data G_theory_with_prover =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_theory_with_prover lid
       (Theory sign sentence proof_tree)
       (Prover sign sentence morphism sublogics proof_tree)

data GPlainTheory =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => GPlainTheory lid (Theory sign sentence proof_tree)

prepareForConsChecking :: ProofState
    -> (G_cons_checker, AnyComorphism)
    -> Result G_theory_with_cons_checker
prepareForConsChecking st (G_cons_checker lid4 p, co) = do
  GPlainTheory lidT th@(Theory sign'' _) <- prepareTheory st co
  incl <- subsig_inclusion lidT (empty_signature lidT) sign''
  let mor = TheoryMorphism
                    { tSource = emptyTheory lidT
                    , tTarget = th
                    , tMorphism = incl }
  p' <- coerceConsChecker lid4 lidT "" p
  return $ G_theory_with_cons_checker lidT mor p'


prepareTheory :: ProofState -> AnyComorphism -> Result GPlainTheory
prepareTheory st (Comorphism cid) = case selectedTheory st of
    G_theory lid _ (ExtSign sign _) _ sens _ -> do
        bTh' <- coerceBasicTheory lid (sourceLogic cid)
                   "Proofs.AbstractState.prepareTheory: basic theory"
                   (sign, toNamedList sens)
        (sign'', sens'') <- wrapMapTheory cid bTh'
        return . GPlainTheory (targetLogic cid) . Theory sign''
          $ toThSens sens''

{- | prepare the selected theory of the state for proving with the
given prover:

 * translation along the comorphism

 * all coercions

 * the lid is valid for the prover and the translated theory
-}
prepareForProving :: ProofState
    -> (G_prover, AnyComorphism)
    -> Result G_theory_with_prover
prepareForProving st (G_prover lid4 p, co) = do
  GPlainTheory lidT th <- prepareTheory st co
  p' <- coerceProver lid4 lidT "" p
  return $ G_theory_with_prover lidT th p'

-- | creates the currently selected theory
makeSelectedTheory :: ProofState -> G_theory
makeSelectedTheory s = case currentTheory s of
  G_theory lid syn sig si sens _ ->
    -- axiom map, goal map
    let (aMap, gMap) = OMap.partition isAxiom sens
        -- proven goals map
        pMap = OMap.filter isProvenSenStatus gMap
    in
    G_theory lid syn sig si
      (Map.unions
        [ filterMapWithList (selectedGoals s) gMap
        , filterMapWithList (includedAxioms s) aMap
        , markAsAxiom True $ filterMapWithList (includedTheorems s) pMap
        ]) startThId

{- |
  recalculation of sublogic upon (de)selection of goals, axioms and
  proven theorems
-}
recalculateSublogicAndSelectedTheory :: ProofState -> ProofState
recalculateSublogicAndSelectedTheory st = let
  sTh = makeSelectedTheory st
  sLo = sublogicOfTh sTh
  in st
    { selectedTheory = sTh
    , proversMap = shrinkKnownProvers sLo $ proversMap st }

getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers = filterM (usableCC . fst) . getAllConsCheckers

getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers = concatMap (\ cm@(Comorphism cid) ->
    map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm))
      $ cons_checkers $ targetLogic cid)

lookupKnownConsChecker :: Monad m => ProofState
    -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker st =
       let sl = sublogicOfTh (selectedTheory st)
           mt = do
                 pr_s <- selectedConsChecker st
                 ps <- Map.lookup pr_s (proversMap st)
                 return (pr_s, ps)
           matchingCC s (gp, _) = case gp of
                                  G_cons_checker _ p -> ccName p == s
           findCC (pr_n, cms) =
               case filter (matchingCC pr_n) $ getAllConsCheckers
                    $ filter (lessSublogicComor sl) cms of
                 [] -> fail ("CMDL.ProverConsistency.lookupKnownConsChecker" ++
                                 ": no consistency checker found")
                 p : _ -> return p
       in maybe ( fail ("CMDL.ProverConsistency.lookupKnownConsChecker: " ++
                      "no matching known prover")) findCC mt


lookupKnownProver :: Monad m => ProofState -> ProverKind
    -> m (G_prover, AnyComorphism)
lookupKnownProver st pk =
    let sl = sublogicOfTh (selectedTheory st)
        mt = do -- Monad Maybe
           pr_s <- selectedProver st
           ps <- Map.lookup pr_s (proversMap st)
           return (pr_s, ps)
        matchingPr s (gp, _) = case gp of
          G_prover _ p -> proverName p == s
        findProver (pr_n, cms) =
            case filter (matchingPr pr_n) $ getProvers pk sl
                 $ filter (lessSublogicComor sl) cms of
               [] -> fail "Proofs.InferBasic: no prover found"
               p : _ -> return p
    in maybe (fail "Proofs.InferBasic: no matching known prover")
             findProver mt

-- | Pairs each target prover of these comorphisms with its comorphism
getProvers :: ProverKind -> G_sublogics -> [AnyComorphism]
  -> [(G_prover, AnyComorphism)]
getProvers pk (G_sublogics lid sl) =
  foldl addProvers [] where
  addProvers acc cm = case cm of
    Comorphism cid -> let
      slid = sourceLogic cid
      tlid = targetLogic cid
      in acc ++ foldl
             (\ l p ->
                  if hasProverKind pk p
                    && language_name lid == language_name slid
                         && maybe False (flip isSubElem $ proverSublogic p)
                           (mapSublogic cid $ forceCoerceSublogic lid slid sl)
                  then (G_prover tlid p, cm) : l else l)
             [] (provers tlid)

knownProvers :: LogicGraph -> ProverKind -> Map.Map G_sublogics [G_prover]
knownProvers lg pk =
 let l = Map.elems $ logics lg
 in foldl (\ m (Logic lid) -> foldl (\ m' p ->
     let lgx = G_sublogics lid (proverSublogic p)
         p' = G_prover lid p
     in case Map.lookup lgx m' of
         Just ps -> Map.insert lgx (p' : ps) m'
         Nothing -> Map.insert lgx [p'] m') m $
     filter (hasProverKind pk)
            (provers lid)) Map.empty l

unsafeCompComorphism :: AnyComorphism -> AnyComorphism -> AnyComorphism
unsafeCompComorphism c1 c2 = case compComorphism c1 c2 of
 Result _ (Just c_new) -> c_new
 r -> propagateErrors "Proofs.AbstractState.unsafeCompComorphism" r

isSubElemG :: G_sublogics -> G_sublogics -> Bool
isSubElemG (G_sublogics lid sl) (G_sublogics lid1 sl1) =
 Logic lid == Logic lid1 &&
 isSubElem sl (Unsafe.Coerce.unsafeCoerce sl1)

pathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
                    -> AnyComorphism
pathToComorphism (path, (G_sublogics lid sub, _)) =
 case path of
  [] -> Comorphism $ mkIdComorphism lid sub
  ((G_sublogics lid1 sub1, _), c) : cs ->
   foldl unsafeCompComorphism
    (Comorphism $ mkIdComorphism lid1 sub1)
    (c : snd (unzip cs))

getUsableProvers :: ProverKind -> G_sublogics -> LogicGraph
 -> IO [(G_prover, AnyComorphism)]
getUsableProvers pk start =
  filterM (usable . fst) . getAllProvers pk start

getAllProvers :: ProverKind -> G_sublogics -> LogicGraph
 -> [(G_prover, AnyComorphism)]
getAllProvers pk start lg =
  let kp = knownProvers lg pk
      g = logicGraph2Graph lg
  in concatMap (mkComorphism kp) $
      concatMap (\ end ->
       yen 10 (start, Nothing) (\ (l, _) -> isSubElemG l end) g)
       (Map.keys kp)
 where
  mkComorphism :: Map.Map G_sublogics [t2]
   -> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
   -> [(t2, AnyComorphism)]
  mkComorphism kp path@(_, (end, _)) =
   let fullComorphism = pathToComorphism path
       cs = Map.toList $ Map.filterWithKey (\ l _ -> isSubElemG end l) kp
   in concatMap (\ x -> case x of
                        (_, ps) -> map (\ p -> (p, fullComorphism)) ps) cs

{- | the list of proof statuses is integrated into the goalMap of the state
after validation of the Disproved Statuses -}
markProved ::
  ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
                sign morphism symbol raw_symbol proof_tree )
  => AnyComorphism -> lid -> [ProofStatus proof_tree]
  -> ProofState
  -> ProofState
markProved c lid status st = st
    { currentTheory = markProvedGoalMap c lid status (currentTheory st) }

-- | mark all newly proven goals with their proof tree
markProvedGoalMap ::
    ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree )
    => AnyComorphism -> lid -> [ProofStatus proof_tree]
    -> G_theory -> G_theory
markProvedGoalMap c lid status th = case th of
  G_theory lid1 syn sig si thSens _ ->
      let updStat ps s = Just $
                s { senAttr = ThmStatus $ (c, BasicProof lid ps) : thmStatus s }
          upd pStat = OMap.update (updStat pStat) (goalName pStat)
      in G_theory lid1 syn sig si (foldl (flip upd) thSens status)
        startThId

autoProofAtNode ::
                   -- use theorems is subsequent proofs
                  Bool
                   -- Timeout Limit
                  -> Int
                   -- selected goals
                  -> [String]
                   -- selected axioms
                  -> [String]
                   -- Node selected for proving
                  -> G_theory
                   -- selected Prover and Comorphism
                  -> ( G_prover, AnyComorphism )
                   -- returns new GoalStatus for the Node
                  -> ResultT IO ((G_theory, [(String, String, String)]),
                                 (ProofState, [ProofStatus G_proof_tree]))
autoProofAtNode useTh timeout goals axioms g_th p_cm = do
      let knpr = propagateErrors "autoProofAtNode"
            $ knownProversWithKind ProveCMDLautomatic
          pf_st = initialState "" g_th knpr
          sg_st = if null goals then pf_st else pf_st
            { selectedGoals = filter (`elem` goals) $ selectedGoals pf_st }
          sa_st = if null axioms then sg_st else sg_st
            { includedAxioms = filter (`elem` axioms) $ includedAxioms sg_st }
          st = recalculateSublogicAndSelectedTheory sa_st
      -- try to prepare the theory
      if null $ selectedGoals st then fail "autoProofAtNode: no goals selected"
        else do
          (G_theory_with_prover lid1 th p) <- liftR $ prepareForProving st p_cm
          case proveCMDLautomaticBatch p of
            Nothing ->
              fail "autoProofAtNode: failed to init CMDLautomaticBatch"
            Just fn -> do
              let encapsulate_pt ps =
                   ps {proofTree = G_proof_tree lid1 $ proofTree ps}
              d <- lift $ do
                -- mVar to poll the prover for results
                answ <- newMVar (return [])
                (_, mV) <- fn useTh False answ (theoryName st)
                                       (TacticScript $ show timeout) th []
                takeMVar mV
                takeMVar answ
              case maybeResult d of
                Nothing -> fail "autoProofAtNode: proving failed"
                Just d' ->
                 return (( currentTheory $ markProved (snd p_cm) lid1 d' st
                         , map (\ ps -> ( goalName ps
                                        , show $ goalStatus ps
                                        , show $ proofTree ps)) d')
                         , (st, map encapsulate_pt d'))
