{- |
Module      :  ./Isabelle/IsaProve.hs
Description :  interface to the Isabelle theorem prover
Copyright   :  (c) University of Cambridge, Cambridge, England
               adaption (c) Till Mossakowski, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Interface for Isabelle theorem prover.
  Interface between Isabelle and Hets:
   Hets writes Isabelle .thy file and starts Isabelle
   User extends .thy file with proofs
   User finishes Isabelle
   Hets reads in created *.deps files
-}

module Isabelle.IsaProve
  ( isabelleConsChecker
  , isabelleBatchProver
  , isabelleProver
  , IsaEditor (..)
  , isaProve
  ) where

import Logic.Prover
import Isabelle.IsaSign
import Isabelle.IsaConsts
import Isabelle.IsaPrint
import Isabelle.IsaParse
import Isabelle.Translate
import Isabelle.MarkSimp

import Common.AS_Annotation
import Common.DocUtils
import Common.DefaultMorphism
import Common.ProofUtils
import Common.Result
import Common.Utils (getEnvDef, executeProcess)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Text.ParserCombinators.Parsec

import Control.Monad
import Control.Concurrent
import Control.Exception (finally)

import Data.Char
import Data.List (isSuffixOf)
import Data.Time (midnight)

import System.Directory
import System.Exit
import System.Process

isabelleS :: String
isabelleS :: String
isabelleS = "Isabelle"

data IsaEditor = Emacs | JEdit

instance Show IsaEditor where
  show :: IsaEditor -> String
show e :: IsaEditor
e = case IsaEditor
e of
    Emacs -> "emacs"
    JEdit -> "jedit"

isabelleProcessS :: String
isabelleProcessS :: String
isabelleProcessS = "isabelle_process"

openIsaProofStatus :: String -> ProofStatus ()
openIsaProofStatus :: String -> ProofStatus ()
openIsaProofStatus n :: String
n = String -> String -> () -> ProofStatus ()
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
n String
isabelleS ()

isabelleProver :: IsaEditor -> Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleProver :: IsaEditor -> Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleProver e :: IsaEditor
e = String
-> String
-> ()
-> (String
    -> Theory Sign Sentence ()
    -> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
    -> IO [ProofStatus ()])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ()])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ()
    -> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence (DefaultMorphism Sign) () ()
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver "isabelle" (String
isabelleS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ IsaEditor -> String
forall a. Show a => a -> String
show IsaEditor
e) ()
  (IsaEditor
-> String
-> Theory Sign Sentence ()
-> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
-> IO [ProofStatus ()]
forall a.
IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProve IsaEditor
e) Bool
-> Bool
-> MVar (Result [ProofStatus ()])
-> String
-> TacticScript
-> Theory Sign Sentence ()
-> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
-> IO (ThreadId, MVar ())
forall a.
Bool
-> Bool
-> MVar (Result [ProofStatus ()])
-> String
-> TacticScript
-> Theory Sign Sentence ()
-> a
-> IO (ThreadId, MVar ())
isaBatchProve

isabelleBatchProver :: Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleBatchProver :: Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleBatchProver = String
-> String
-> ()
-> (String
    -> Theory Sign Sentence ()
    -> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
    -> IO [ProofStatus ()])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ()])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ()
    -> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence (DefaultMorphism Sign) () ()
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver String
isabelleProcessS String
isabelleProcessS ()
  (Maybe IsaEditor
-> String
-> Theory Sign Sentence ()
-> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
-> IO [ProofStatus ()]
forall a.
Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProveAux Maybe IsaEditor
forall a. Maybe a
Nothing) Bool
-> Bool
-> MVar (Result [ProofStatus ()])
-> String
-> TacticScript
-> Theory Sign Sentence ()
-> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
-> IO (ThreadId, MVar ())
forall a.
Bool
-> Bool
-> MVar (Result [ProofStatus ()])
-> String
-> TacticScript
-> Theory Sign Sentence ()
-> a
-> IO (ThreadId, MVar ())
isaBatchProve

isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
isabelleConsChecker =
  (String
-> String
-> ()
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
    -> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
    -> IO (CCStatus ()))
-> ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
forall sublogics sign sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
mkUsableConsChecker "isabelle" "Isabelle-refute" () String
-> TacticScript
-> TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
-> [FreeDefMorphism Sentence (DefaultMorphism Sign)]
-> IO (CCStatus ())
forall b a.
String
-> b
-> TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
-> a
-> IO (CCStatus ())
consCheck)
  { ccBatch :: Bool
ccBatch = Bool
False
  , ccNeedsTimer :: Bool
ccNeedsTimer = Bool
False }

-- | the name of the inconsistent lemma for consistency checks
inconsistentS :: String
inconsistentS :: String
inconsistentS = "inconsistent"

metaToTerm :: MetaTerm -> Term
metaToTerm :: MetaTerm -> Term
metaToTerm mt :: MetaTerm
mt = case MetaTerm
mt of
  Term t :: Term
t -> Term
t
  Conditional ts :: [Term]
ts t :: Term
t -> case [Term]
ts of
    [] -> Term
t
    _ -> Term -> Term -> Term
binImpl ((Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
binConj [Term]
ts) Term
t

consCheck :: String -> b
  -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) () -> a
  -> IO (CCStatus ())
consCheck :: String
-> b
-> TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
-> a
-> IO (CCStatus ())
consCheck thName :: String
thName _tac :: b
_tac tm :: TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
tm freedefs :: a
freedefs = case TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
-> Theory Sign Sentence ()
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tTarget TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()
tm of
    Theory sig :: Sign
sig nSens :: ThSens Sentence (ProofStatus ())
nSens -> do
      let (axs :: [Named Sentence]
axs, _) = [Named Sentence] -> ([Named Sentence], [Named Sentence])
getAxioms ([Named Sentence] -> ([Named Sentence], [Named Sentence]))
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a b. (a -> b) -> a -> b
$ ThSens Sentence (ProofStatus ()) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ())
nSens
      [ProofStatus ()]
l <- IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
forall a.
IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProve IsaEditor
JEdit (String
thName String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_c")
           (Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
sig
               (ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ())
-> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall a b. (a -> b) -> a -> b
$ ThSens Sentence (ProofStatus ())
-> ThSens Sentence (ProofStatus ())
forall a b. Ord a => ThSens a b -> ThSens a b
markAsGoal (ThSens Sentence (ProofStatus ())
 -> ThSens Sentence (ProofStatus ()))
-> ThSens Sentence (ProofStatus ())
-> ThSens Sentence (ProofStatus ())
forall a b. (a -> b) -> a -> b
$ [Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens ([Named Sentence] -> ThSens Sentence (ProofStatus ()))
-> [Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. (a -> b) -> a -> b
$ if [Named Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named Sentence]
axs then [] else
                   [ String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
inconsistentS (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkRefuteSen (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
termAppl Term
notOp
                     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
binConj
                     ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Term) -> [Named Sentence] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (MetaTerm -> Term
metaToTerm (MetaTerm -> Term)
-> (Named Sentence -> MetaTerm) -> Named Sentence -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> MetaTerm
metaTerm (Sentence -> MetaTerm)
-> (Named Sentence -> Sentence) -> Named Sentence -> MetaTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
axs ])
           a
freedefs
      CCStatus () -> IO (CCStatus ())
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus () -> IO (CCStatus ()))
-> CCStatus () -> IO (CCStatus ())
forall a b. (a -> b) -> a -> b
$ () -> TimeOfDay -> Maybe Bool -> CCStatus ()
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus () TimeOfDay
midnight (Maybe Bool -> CCStatus ()) -> Maybe Bool -> CCStatus ()
forall a b. (a -> b) -> a -> b
$ case (ProofStatus () -> Bool) -> [ProofStatus ()] -> [ProofStatus ()]
forall a. (a -> Bool) -> [a] -> [a]
filter ProofStatus () -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat [ProofStatus ()]
l of
        [_] -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -- inconsistency was proven
        _ -> Maybe Bool
forall a. Maybe a
Nothing -- consistency cannot be recorded automatically

prepareTheory :: Theory Sign Sentence ()
    -> (Sign, [Named Sentence], [Named Sentence], Map.Map String String)
prepareTheory :: Theory Sign Sentence ()
-> (Sign, [Named Sentence], [Named Sentence], Map String String)
prepareTheory (Theory sig :: Sign
sig nSens :: ThSens Sentence (ProofStatus ())
nSens) = let
    oSens :: [Named Sentence]
oSens = ThSens Sentence (ProofStatus ()) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ())
nSens
    nSens' :: [Named Sentence]
nSens' = ShowS -> [Named Sentence] -> [Named Sentence]
forall a. ShowS -> [Named a] -> [Named a]
prepareSenNames ShowS
transString [Named Sentence]
oSens
    (disAxs :: [Named Sentence]
disAxs, disGoals :: [Named Sentence]
disGoals) = [Named Sentence] -> ([Named Sentence], [Named Sentence])
getAxioms [Named Sentence]
nSens'
    in (Sign
sig, (Named Sentence -> Named Sentence)
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Named Sentence
markSimp [Named Sentence]
disAxs, (Named Sentence -> Named Sentence)
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Named Sentence
markThSimp [Named Sentence]
disGoals,
       [(String, String)] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, String)] -> Map String String)
-> [(String, String)] -> Map String String
forall a b. (a -> b) -> a -> b
$ [String] -> [String] -> [(String, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr [Named Sentence]
nSens') ([String] -> [(String, String)]) -> [String] -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr [Named Sentence]
oSens)
-- return a reverse mapping for renamed sentences

removeDepFiles :: String -> [String] -> IO ()
removeDepFiles :: String -> [String] -> IO ()
removeDepFiles thName :: String
thName = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> IO ()) -> [String] -> IO ())
-> (String -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ \ thm :: String
thm -> do
  let depFile :: String
depFile = String -> ShowS
getDepsFileName String
thName String
thm
  Bool
ex <- String -> IO Bool
doesFileExist String
depFile
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ex (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
depFile

getDepsFileName :: String -> String -> String
getDepsFileName :: String -> ShowS
getDepsFileName thName :: String
thName thm :: String
thm = String
thName String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thm String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".deps"

getProofDeps :: Map.Map String String -> String -> String
             -> IO (ProofStatus ())
getProofDeps :: Map String String -> String -> String -> IO (ProofStatus ())
getProofDeps m :: Map String String
m thName :: String
thName thm :: String
thm = do
    let file :: String
file = String -> ShowS
getDepsFileName String
thName String
thm
        mapN :: ShowS
mapN n :: String
n = String -> String -> Map String String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault String
n String
n Map String String
m
        strip :: ShowS
strip = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
    Bool
b <- String -> IO Bool
doesFileExist String
file
    if Bool
b then do
        String
s <- String -> IO String
readFile String
file
        ProofStatus () -> IO (ProofStatus ())
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus () -> IO (ProofStatus ()))
-> ProofStatus () -> IO (ProofStatus ())
forall a b. (a -> b) -> a -> b
$ String -> [String] -> ProofStatus ()
mkProved (ShowS
mapN String
thm) ([String] -> ProofStatus ()) -> [String] -> ProofStatus ()
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
mapN ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
               Set String -> [String]
forall a. Set a -> [a]
Set.toList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> Set String -> Set String
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$
               [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
strip ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
s
      else ProofStatus () -> IO (ProofStatus ())
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStatus () -> IO (ProofStatus ()))
-> ProofStatus () -> IO (ProofStatus ())
forall a b. (a -> b) -> a -> b
$ String -> ProofStatus ()
openIsaProofStatus (String -> ProofStatus ()) -> String -> ProofStatus ()
forall a b. (a -> b) -> a -> b
$ ShowS
mapN String
thm

getAllProofDeps :: Map.Map String String -> String -> [String]
                -> IO [ProofStatus ()]
getAllProofDeps :: Map String String -> String -> [String] -> IO [ProofStatus ()]
getAllProofDeps m :: Map String String
m = (String -> IO (ProofStatus ())) -> [String] -> IO [ProofStatus ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> IO (ProofStatus ()))
 -> [String] -> IO [ProofStatus ()])
-> (String -> String -> IO (ProofStatus ()))
-> String
-> [String]
-> IO [ProofStatus ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String String -> String -> String -> IO (ProofStatus ())
getProofDeps Map String String
m

checkFinalThyFile :: (TheoryHead, Body) -> String -> IO Bool
checkFinalThyFile :: (TheoryHead, Body) -> String -> IO Bool
checkFinalThyFile (ho :: TheoryHead
ho, bo :: Body
bo) thyFile :: String
thyFile = do
  String
s <- String -> IO String
readFile String
thyFile
  case Parsec String () (TheoryHead, Body)
-> String -> String -> Either ParseError (TheoryHead, Body)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (TheoryHead, Body)
parseTheory String
thyFile String
s of
    Right (hb :: TheoryHead
hb, b :: Body
b) -> do
            let ds :: [Diagnosis]
ds = Body -> Body -> [Diagnosis]
compatibleBodies Body
bo Body
b
            (Diagnosis -> IO ()) -> [Diagnosis] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ d :: Diagnosis
d -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagnosis -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Diagnosis
d "") ([Diagnosis] -> IO ()) -> [Diagnosis] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ Body -> [Diagnosis]
warnSimpAttr Body
b
            if TheoryHead
hb TheoryHead -> TheoryHead -> Bool
forall a. Eq a => a -> a -> Bool
/= TheoryHead
ho then do
                  String -> IO ()
putStrLn "illegal change of theory header"
                  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
              else Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds
    Left err :: ParseError
err -> ParseError -> IO ()
forall a. Show a => a -> IO ()
print ParseError
err IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

mkProved :: String -> [String] -> ProofStatus ()
mkProved :: String -> [String] -> ProofStatus ()
mkProved thm :: String
thm used :: [String]
used = (String -> ProofStatus ()
openIsaProofStatus String
thm)
    { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
    , usedAxioms :: [String]
usedAxioms = [String]
used
    , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript "unknown isabelle user input" }

prepareThyFiles :: (TheoryHead, Body) -> String -> String -> IO ()
prepareThyFiles :: (TheoryHead, Body) -> String -> String -> IO ()
prepareThyFiles ast :: (TheoryHead, Body)
ast thyFile :: String
thyFile thy :: String
thy = do
    let origFile :: String
origFile = String
thyFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".orig"
    Bool
exOrig <- String -> IO Bool
doesFileExist String
origFile
    Bool
exThyFile <- String -> IO Bool
doesFileExist String
thyFile
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exOrig (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
origFile String
thy
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exThyFile (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
thyFile String
thy
    UTCTime
thy_time <- String -> IO UTCTime
getModificationTime String
thyFile
    UTCTime
orig_time <- String -> IO UTCTime
getModificationTime String
origFile
    String
s <- String -> IO String
readFile String
origFile
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UTCTime
thy_time UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
orig_time Bool -> Bool -> Bool
&& String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
thy)
      (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ (TheoryHead, Body) -> String -> String -> String -> IO ()
patchThyFile (TheoryHead, Body)
ast String
origFile String
thyFile String
thy

patchThyFile :: (TheoryHead, Body) -> FilePath -> FilePath -> String -> IO ()
patchThyFile :: (TheoryHead, Body) -> String -> String -> String -> IO ()
patchThyFile (ho :: TheoryHead
ho, bo :: Body
bo) origFile :: String
origFile thyFile :: String
thyFile thy :: String
thy = do
  let patchFile :: String
patchFile = String
thyFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".patch"
      oldFile :: String
oldFile = String
thyFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".old"
      diffCall :: String
diffCall = "diff -u " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
origFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thyFile
                 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " > " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
patchFile
      patchCall :: String
patchCall = "patch -bfu " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thyFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
patchFile
  String -> IO ExitCode
callSystem String
diffCall
  String -> String -> IO ()
renameFile String
thyFile String
oldFile
  String -> IO ()
removeFile String
origFile
  String -> String -> IO ()
writeFile String
origFile String
thy
  String -> String -> IO ()
writeFile String
thyFile String
thy
  String -> IO ExitCode
callSystem String
patchCall
  String
s <- String -> IO String
readFile String
thyFile
  case Parsec String () (TheoryHead, Body)
-> String -> String -> Either ParseError (TheoryHead, Body)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (TheoryHead, Body)
parseTheory String
thyFile String
s of
    Right (hb :: TheoryHead
hb, b :: Body
b) -> do
            let ds :: [Diagnosis]
ds = Body -> Body -> [Diagnosis]
compatibleBodies Body
bo Body
b
                h :: Bool
h = TheoryHead
hb TheoryHead -> TheoryHead -> Bool
forall a. Eq a => a -> a -> Bool
== TheoryHead
ho
            (Diagnosis -> IO ()) -> [Diagnosis] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ d :: Diagnosis
d -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagnosis -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Diagnosis
d "") [Diagnosis]
ds
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
h (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn "theory header is corrupt"
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
h Bool -> Bool -> Bool
&& [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
revertThyFile String
thyFile String
thy
    Left err :: ParseError
err -> do
      ParseError -> IO ()
forall a. Show a => a -> IO ()
print ParseError
err
      String -> String -> IO ()
revertThyFile String
thyFile String
thy

revertThyFile :: String -> String -> IO ()
revertThyFile :: String -> String -> IO ()
revertThyFile thyFile :: String
thyFile thy :: String
thy = do
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "replacing corrupt file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
thyFile
    String -> IO ()
removeFile String
thyFile
    String -> String -> IO ()
writeFile String
thyFile String
thy

callSystem :: String -> IO ExitCode
callSystem :: String -> IO ExitCode
callSystem s :: String
s = String -> IO ()
putStrLn String
s IO () -> IO ExitCode -> IO ExitCode
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ExitCode
system String
s

isaProve :: IsaEditor -> String -> Theory Sign Sentence () -> a
  -> IO [ProofStatus ()]
isaProve :: IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProve = Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
forall a.
Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProveAux (Maybe IsaEditor
 -> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()])
-> (IsaEditor -> Maybe IsaEditor)
-> IsaEditor
-> String
-> Theory Sign Sentence ()
-> a
-> IO [ProofStatus ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsaEditor -> Maybe IsaEditor
forall a. a -> Maybe a
Just

isaProveAux :: Maybe IsaEditor -> String -> Theory Sign Sentence () -> a
  -> IO [ProofStatus ()]
isaProveAux :: Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProveAux meditor :: Maybe IsaEditor
meditor thName :: String
thName th :: Theory Sign Sentence ()
th _freedefs :: a
_freedefs = do
  let (sig :: Sign
sig, axs :: [Named Sentence]
axs, ths :: [Named Sentence]
ths, m :: Map String String
m) = Theory Sign Sentence ()
-> (Sign, [Named Sentence], [Named Sentence], Map String String)
prepareTheory Theory Sign Sentence ()
th
      thms :: [String]
thms = (Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr [Named Sentence]
ths
      thBaseName :: String
thBaseName = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '/') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
thName
      useaxs :: [Named Sentence]
useaxs = (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ s :: Named Sentence
s ->
            Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s Sentence -> Sentence -> Bool
forall a. Eq a => a -> a -> Bool
/= Term -> Sentence
mkSen Term
true Bool -> Bool -> Bool
&& (Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isDef Named Sentence
s Bool -> Bool -> Bool
||
               String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "def" (Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
s))) [Named Sentence]
axs
      defaultProof :: Maybe IsaProof
defaultProof = IsaProof -> Maybe IsaProof
forall a. a -> Maybe a
Just (IsaProof -> Maybe IsaProof) -> IsaProof -> Maybe IsaProof
forall a b. (a -> b) -> a -> b
$ [ProofCommand] -> ProofEnd -> IsaProof
IsaProof
        (if [Named Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named Sentence]
useaxs then [] else [[String] -> ProofCommand
Using ([String] -> ProofCommand) -> [String] -> ProofCommand
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr [Named Sentence]
useaxs])
        (ProofEnd -> IsaProof) -> ProofEnd -> IsaProof
forall a b. (a -> b) -> a -> b
$ ProofMethod -> ProofEnd
By ProofMethod
Auto
      thy :: String
thy = Doc -> ShowS
forall a. Show a => a -> ShowS
shows (String -> Sign -> [Named Sentence] -> Doc
printIsaTheory String
thBaseName Sign
sig
        ([Named Sentence] -> Doc) -> [Named Sentence] -> Doc
forall a b. (a -> b) -> a -> b
$ [Named Sentence]
axs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ (Named Sentence -> Named Sentence)
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((Sentence -> Sentence) -> Named Sentence -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((Sentence -> Sentence) -> Named Sentence -> Named Sentence)
-> (Sentence -> Sentence) -> Named Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ \ t :: Sentence
t -> case Sentence
t of
           Sentence { thmProof :: Sentence -> Maybe IsaProof
thmProof = Maybe IsaProof
Nothing } -> Sentence
t { thmProof :: Maybe IsaProof
thmProof = Maybe IsaProof
defaultProof }
           _ -> Sentence
t) [Named Sentence]
ths)
        "\n"
      thyFile :: String
thyFile = String
thBaseName String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".thy"
  case Parsec String () (TheoryHead, Body)
-> String -> String -> Either ParseError (TheoryHead, Body)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () (TheoryHead, Body)
parseTheory String
thyFile String
thy of
    Right (ho :: TheoryHead
ho, bo :: Body
bo) -> do
      (TheoryHead, Body) -> String -> String -> IO ()
prepareThyFiles (TheoryHead
ho, Body
bo) String
thyFile String
thy
      String -> [String] -> IO ()
removeDepFiles String
thBaseName [String]
thms
      case Maybe IsaEditor
meditor of
        Nothing -> do
          (ex :: ExitCode
ex, out :: String
out, err :: String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
isabelleProcessS []
            (String -> IO (ExitCode, String, String))
-> String -> IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ " use_thy \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thBaseName String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\";"
          String -> IO ()
putStrLn String
out
          case ExitCode
ex of
            ExitSuccess -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            _ -> String -> IO ()
putStrLn String
err
          ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode
ex
        Just editor :: IsaEditor
editor -> do
          String
isabelle <- String -> String -> IO String
getEnvDef "HETS_ISABELLE" (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "isabelle " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IsaEditor -> String
forall a. Show a => a -> String
show IsaEditor
editor
          String -> IO ExitCode
callSystem (String -> IO ExitCode) -> String -> IO ExitCode
forall a b. (a -> b) -> a -> b
$ String
isabelle String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thyFile
      Bool
ok <- (TheoryHead, Body) -> String -> IO Bool
checkFinalThyFile (TheoryHead
ho, Body
bo) String
thyFile
      if Bool
ok then Map String String -> String -> [String] -> IO [ProofStatus ()]
getAllProofDeps Map String String
m String
thBaseName [String]
thms
          else [ProofStatus ()] -> IO [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Left err :: ParseError
err -> do
      ParseError -> IO ()
forall a. Show a => a -> IO ()
print ParseError
err
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Sorry, generated theory cannot be parsed, see: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
thyFile
      String -> String -> IO ()
writeFile String
thyFile String
thy
      String -> IO ()
putStrLn "aborting Isabelle proof attempt"
      [ProofStatus ()] -> IO [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return []

isaBatchProve :: Bool -- 1.
                 -> Bool -- 2.
                 -> MVar (Result [ProofStatus ()]) -- 3.
                 -> String -- 4.
                 -> TacticScript  -- 5.
                 -> Theory Sign Sentence ()  -- 6.
                 -> a
                 -> IO (ThreadId, MVar ())
isaBatchProve :: Bool
-> Bool
-> MVar (Result [ProofStatus ()])
-> String
-> TacticScript
-> Theory Sign Sentence ()
-> a
-> IO (ThreadId, MVar ())
isaBatchProve _incl :: Bool
_incl _save :: Bool
_save resMVar :: MVar (Result [ProofStatus ()])
resMVar thName :: String
thName _tac :: TacticScript
_tac th :: Theory Sign Sentence ()
th freedefs :: a
freedefs = do
    MVar ()
mvar <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
    ThreadId
threadID <- IO () -> IO ThreadId
forkIO (do
        [ProofStatus ()]
ps <- Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
forall a.
Maybe IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProveAux Maybe IsaEditor
forall a. Maybe a
Nothing String
thName Theory Sign Sentence ()
th a
freedefs
        Result [ProofStatus ()]
_ <- MVar (Result [ProofStatus ()])
-> Result [ProofStatus ()] -> IO (Result [ProofStatus ()])
forall a. MVar a -> a -> IO a
swapMVar MVar (Result [ProofStatus ()])
resMVar (Result [ProofStatus ()] -> IO (Result [ProofStatus ()]))
-> Result [ProofStatus ()] -> IO (Result [ProofStatus ()])
forall a b. (a -> b) -> a -> b
$ [ProofStatus ()] -> Result [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return [ProofStatus ()]
ps
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO a
`finally` MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
mvar ())
    (ThreadId, MVar ()) -> IO (ThreadId, MVar ())
forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
threadID, MVar ()
mvar)