{- |
Module      :  ./CSL/ReduceProve.hs
Description :  interface to Reduce CAS
Copyright   :  (c) Dominik Dietrich, DFKI Bremen, 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Dominik.Dietrich@dfki.de
Stability   :  provisional
Portability :  portable

Interface for Reduce CAS system.
-}

module CSL.ReduceProve where

import Common.AS_Annotation

import Data.List

import Logic.Prover

import CSL.AS_BASIC_CSL
import CSL.Morphism
import CSL.Reduce_Interface
import CSL.Sign

-- as mkProverTemplate, but with additionally functionality to export lemmas
mkProverTemplateWithLemmaExport :: String -> sublogics
  -> (String -> theory -> [FreeDefMorphism sentence morphism]
      -> IO ( [ProofStatus proof_tree]
            , [(Named sentence, ProofStatus proof_tree)]))
  -> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplateWithLemmaExport :: String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO
         ([ProofStatus proof_tree],
          [(Named sentence, ProofStatus proof_tree)]))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplateWithLemmaExport str :: String
str sl :: sublogics
sl fct :: String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
fct = Prover :: forall theory sentence morphism sublogics proof_tree.
String
-> IO (Maybe String)
-> sublogics
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
Prover
    { proverName :: String
proverName = String
str
    , proverUsable :: IO (Maybe String)
proverUsable = (Either String String -> Maybe String)
-> IO (Either String String) -> IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Maybe String)
-> (String -> Maybe String) -> Either String String -> Maybe String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe String -> String -> Maybe String
forall a b. a -> b -> a
const Maybe String
forall a. Maybe a
Nothing) String -> Maybe String
forall a. a -> Maybe a
Just) IO (Either String String)
lookupRedShellCmd
    , proverSublogic :: sublogics
proverSublogic = sublogics
sl
    , proveGUI :: Maybe
  (String
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO
        ([ProofStatus proof_tree],
         [(Named sentence, ProofStatus proof_tree)]))
proveGUI = (String
 -> theory
 -> [FreeDefMorphism sentence morphism]
 -> IO
      ([ProofStatus proof_tree],
       [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
forall a. a -> Maybe a
Just ((String
  -> theory
  -> [FreeDefMorphism sentence morphism]
  -> IO
       ([ProofStatus proof_tree],
        [(Named sentence, ProofStatus proof_tree)]))
 -> Maybe
      (String
       -> theory
       -> [FreeDefMorphism sentence morphism]
       -> IO
            ([ProofStatus proof_tree],
             [(Named sentence, ProofStatus proof_tree)])))
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO
         ([ProofStatus proof_tree],
          [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
forall a b. (a -> b) -> a -> b
$ \ s :: String
s t :: theory
t fs :: [FreeDefMorphism sentence morphism]
fs -> String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
fct String
s theory
t [FreeDefMorphism sentence morphism]
fs
    , proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus proof_tree])
   -> String
   -> TacticScript
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus proof_tree])
   -> String
   -> TacticScript
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO (ThreadId, MVar ()))
forall a. Maybe a
Nothing }

-- | the prover
reduceProver :: Prover Sign CMD Morphism () [EXPRESSION]
reduceProver :: Prover Sign CMD Morphism () [EXPRESSION]
reduceProver = String
-> ()
-> (String
    -> Theory Sign CMD [EXPRESSION]
    -> [FreeDefMorphism CMD Morphism]
    -> IO
         ([ProofStatus [EXPRESSION]],
          [(Named CMD, ProofStatus [EXPRESSION])]))
-> Prover Sign CMD Morphism () [EXPRESSION]
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO
         ([ProofStatus proof_tree],
          [(Named sentence, ProofStatus proof_tree)]))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplateWithLemmaExport String
reduceS () String
-> Theory Sign CMD [EXPRESSION]
-> [FreeDefMorphism CMD Morphism]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
String
-> Theory Sign CMD [EXPRESSION]
-> a
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
reduceProve

-- | splits a list of named sentences into axioms and sentences to be proven
getAxioms :: [Named CMD] -> ([Named CMD], [Named CMD])
getAxioms :: [Named CMD] -> ([Named CMD], [Named CMD])
getAxioms = (Named CMD -> Bool) -> [Named CMD] -> ([Named CMD], [Named CMD])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Named CMD -> Bool
isReduceAxiom

-- | checks whether a named sentence is a reduce axiom
isReduceAxiom :: Named CMD -> Bool
isReduceAxiom :: Named CMD -> Bool
isReduceAxiom s :: Named CMD
s = case Named CMD -> CMD
forall s a. SenAttr s a -> s
sentence Named CMD
s of
                    Cmd {} -> Named CMD -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named CMD
s
                    _ -> Bool
False -- TODO: implement


{- | takes a theory name and a theory as input, starts the prover
  and returns a list of ProofStatus. -}
reduceProve :: String -> Theory Sign CMD [EXPRESSION] -> a
  -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
reduceProve :: String
-> Theory Sign CMD [EXPRESSION]
-> a
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
reduceProve _ (Theory _ senMap :: ThSens CMD (ProofStatus [EXPRESSION])
senMap) _freedefs :: a
_freedefs =
    let
        namedCmds :: [Named CMD]
namedCmds = ThSens CMD (ProofStatus [EXPRESSION]) -> [Named CMD]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens CMD (ProofStatus [EXPRESSION])
senMap
        (_, namedGoals :: [Named CMD]
namedGoals) = [Named CMD] -> ([Named CMD], [Named CMD])
getAxioms [Named CMD]
namedCmds
    in [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
processCmds [Named CMD]
namedGoals

-- | connect to CAS, stepwise process the cmds
processCmds :: [Named CMD]
  -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
processCmds :: [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
processCmds cmds :: [Named CMD]
cmds = do
  String -> IO ()
putStr "Connecting CAS.."
  Either String String
sc <- IO (Either String String)
lookupRedShellCmd
  case Either String String
sc of
    Right reducecmd :: String
reducecmd ->
        do
          String -> IO ()
putStrLn "failed"
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Could not find reduce under " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reducecmd
          ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    Left reducecmd :: String
reducecmd ->
        do
          (inpt :: Handle
inpt, out :: Handle
out, _, pid :: ProcessHandle
pid) <- String -> IO (Handle, Handle, Handle, ProcessHandle)
connectCAS String
reducecmd
          ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
proofinfos <- (Handle, Handle, ProcessHandle)
-> [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
processCmdsIntern (Handle
inpt, Handle
out, ProcessHandle
pid) [Named CMD]
cmds
          (Handle, Handle, ProcessHandle) -> IO ()
forall a. Session a => a -> IO ()
disconnectCAS (Handle
inpt, Handle
out, ProcessHandle
pid)
          ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
proofinfos


-- | internal function to process commands over an existing connection
processCmdsIntern :: Session a => a -> [Named CMD]
  -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
processCmdsIntern :: a
-> [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
processCmdsIntern _ [] = ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
processCmdsIntern sess :: a
sess (x :: Named CMD
x : xs :: [Named CMD]
xs) = do
  (prooftree :: ProofStatus [EXPRESSION]
prooftree, newlemmas :: [(Named CMD, ProofStatus [EXPRESSION])]
newlemmas) <- a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> Named CMD
-> IO
     (ProofStatus [EXPRESSION], [(Named CMD, ProofStatus [EXPRESSION])])
procCmd a
sess Named CMD
x
  (prooftrees :: [ProofStatus [EXPRESSION]]
prooftrees, newlemmas2 :: [(Named CMD, ProofStatus [EXPRESSION])]
newlemmas2) <- a
-> [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall a.
Session a =>
a
-> [Named CMD]
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
processCmdsIntern a
sess [Named CMD]
xs
  ([ProofStatus [EXPRESSION]],
 [(Named CMD, ProofStatus [EXPRESSION])])
-> IO
     ([ProofStatus [EXPRESSION]],
      [(Named CMD, ProofStatus [EXPRESSION])])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus [EXPRESSION]
prooftree ProofStatus [EXPRESSION]
-> [ProofStatus [EXPRESSION]] -> [ProofStatus [EXPRESSION]]
forall a. a -> [a] -> [a]
: [ProofStatus [EXPRESSION]]
prooftrees, [(Named CMD, ProofStatus [EXPRESSION])]
newlemmas [(Named CMD, ProofStatus [EXPRESSION])]
-> [(Named CMD, ProofStatus [EXPRESSION])]
-> [(Named CMD, ProofStatus [EXPRESSION])]
forall a. [a] -> [a] -> [a]
++ [(Named CMD, ProofStatus [EXPRESSION])]
newlemmas2)