{- |

Module : $Header$

Copyright : (c) University of Cambridge, Cambridge, England

adaption (c) Till Mossakowski, Uni Bremen 2002-2005

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : maeder@tzi.de

Stability : provisional

Portability : portable

Interface for Isabelle theorem prover.

-}

{-

todo: thy files in subdir, check of legal changes in thy file

consistency check

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 where

import Logic.Prover

import Isabelle.IsaSign

import Isabelle.IsaConsts

import Isabelle.IsaPrint

import Isabelle.Translate

import Common.AS_Annotation

import Common.DefaultMorphism

import Common.ProofUtils

import qualified Common.Lib.Map as Map

import Driver.Options

import Data.Char

import Directory

import System

isabelleS :: String

isabelleS = "Isabelle"

isabelleProver :: Prover Sign Sentence ()

isabelleProver =

Prover { prover_name = isabelleS,

prover_sublogic = isabelleS,

prove = isaProve False

}

isabelleConsChecker :: ConsChecker Sign Sentence (DefaultMorphism Sign) ()

isabelleConsChecker =

Prover { prover_name = "Isabelle-refute",

prover_sublogic = isabelleS,

prove = \ thn mor -> error "isabelleConsChecker" }

prepareTheory :: Theory Sign Sentence ()

-> (Sign, [Named Sentence], [Named Sentence], Map.Map String String)

prepareTheory (Theory sig nSens) = let

oSens = toNamedList nSens

nSens' = prepareSenNames transString oSens

(disAxs, disGoals) = getAxioms nSens'

in (sig, map markSimp disAxs, map markSimp disGoals,

Map.fromList $ zip (map senName nSens') $ map senName oSens)

-- return a reverse mapping for renamed sentences

removeDepFiles :: String -> [String] -> IO ()

removeDepFiles thName = mapM_ $ removeFile . getDepsFileName thName

getDepsFileName :: String -> String -> String

getDepsFileName thName thm = thName ++ "_" ++ thm ++ ".deps"

getProofDeps :: Map.Map String String -> String -> String

-> IO (Proof_status ())

getProofDeps m thName thm = do

let file = getDepsFileName thName thm

mapN n = Map.findWithDefault n n m

strip = takeWhile (not . isSpace) . dropWhile isSpace

b <- checkInFile file

if b then do

s <- readFile file

if null s then return $ Open $ mapN thm

else let l = filter (not . null) $ map strip $ lines s

in return $ mkProved (mapN thm) $ map mapN l

else return $ Open $ mapN thm

getAllProofDeps :: Map.Map String String -> String -> [String]

-> IO([Proof_status ()])

getAllProofDeps m thName = mapM $ getProofDeps m thName

mkProved :: String -> [String] -> Proof_status ()

mkProved thm used = Proved

{ goalName = thm

, usedAxioms = used

, proverName = isabelleS

, proofTree = ()

, tacticScript = Tactic_script "unknown isabelle user input"

}

prepareThyFiles :: String -> String -> IO ()

prepareThyFiles thyFile thy = do

let origFile = thyFile ++ ".orig"

exOrig <- checkInFile origFile

exThyFile <- checkInFile thyFile

if exOrig then return () else writeFile origFile thy

if exThyFile then return () else writeFile thyFile thy

s <- readFile origFile

if s == thy then do -- orig file is up to date

thy_time <- getModificationTime thyFile

orig_time <- getModificationTime origFile

if thy_time >= orig_time then -- use the current file

return ()

else patchThyFile origFile thyFile thy

else patchThyFile origFile thyFile thy

patchThyFile :: FilePath -> FilePath -> String -> IO ()

patchThyFile origFile thyFile thy = do

let patchFile = thyFile ++ ".patch"

oldFile = thyFile ++ ".old"

diffCall = "diff -u " ++ origFile ++ " " ++ thyFile

++ " > " ++ patchFile

patchCall = "patch -u " ++ thyFile ++ " " ++ patchFile

callSystem diffCall

renameFile thyFile oldFile

writeFile origFile thy

writeFile thyFile thy

callSystem patchCall

return()

callSystem :: String -> IO ExitCode

callSystem s = putStrLn s >> system s

isaProve :: Bool -> String -> Theory Sign Sentence () -> IO([Proof_status ()])

isaProve checkCons thName th = do

let (sig, axs, ths, m) = prepareTheory th

thms = map senName ths

hlibdir <- getEnv "HETS_LIB"

let thBaseName = reverse . takeWhile (/= '/') $ reverse thName

thy = show $ printIsaTheory thBaseName hlibdir sig $ axs ++ ths

thyFile = thName ++ ".thy"

prepareThyFiles thyFile thy

removeDepFiles thName thms

isabelle <- getEnv "HETS_ISABELLE"

callSystem $ isabelle ++ " " ++ thyFile

getAllProofDeps m thName thms

markSimp :: Named Sentence -> Named Sentence

markSimp = mapNamed markSimpSen

markSimpSen :: Sentence -> Sentence

markSimpSen s = case s of

Sentence {} -> s {isSimp = isSimpRuleSen s}

_ -> s

isSimpRuleSen :: Sentence -> Bool

isSimpRuleSen sen = case sen of

RecDef {} -> False

_ -> isSimpRule $ senTerm sen

-- | test whether a formula should be put into the simpset

isSimpRule :: Term -> Bool

-- only universal quantifications

isSimpRule App { funId = Const {termName = VName { new = q }}

, argId = arg@Abs{}}

| q == exS || q == ex1S = False

| q == allS = isSimpRule (termId arg)

-- accept everything expect from abstractions

isSimpRule App {funId = arg1, argId = arg2} =

isSimpRule arg1 && isSimpRule arg2

isSimpRule MixfixApp {funId = arg1, argIds = args } =

isSimpRule arg1 && all isSimpRule args

isSimpRule Const{} = True

isSimpRule Free{} = True

isSimpRule Var{} = True

isSimpRule Bound{} = True

isSimpRule Abs{} = False

isSimpRule If{} = True

isSimpRule Case{} = True

isSimpRule Let{} = True

isSimpRule (Paren t) = isSimpRule t

isSimpRule _ = False