{- |

Module : $Header$

Description : Utilities for CspCASLProver related to Isabelle

Copyright : (c) Liam O'Reilly and Markus Roggenbach,

Swansea University 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : csliam@swansea.ac.uk

Stability : provisional

Portability : portable

Utilities for CspCASLProver related to Isabelle. The functions here

typically manipulate Isabelle signatures.

-}

module CspCASLProver.IsabelleUtils

( addConst

, addDef

, addInstanceOf

, addLemmasCollection

, addPrimRec

, addTheoremWithProof

, updateDomainTab

, writeIsaTheory

) where

import Common.AS_Annotation (makeNamed, Named, SenAttr (..))

import Common.ProofUtils (prepareSenNames)

import Comorphisms.CFOL2IsabelleHOL (IsaTheory)

-- import CspCASLProver.Consts

import qualified Data.Map as Map

import Isabelle.IsaParse (parseTheory)

import Isabelle.IsaPrint (getAxioms, printIsaTheory)

import Isabelle.IsaSign (DomainEntry, IsaProof (..), mkCond, mkSen

, Sentence (..), Sign (..), Sort

, Term (..), Typ (..))

import Isabelle.IsaConsts (mkVName)

import Isabelle.Translate (transString)

import Logic.Prover (Theory (..), toNamedList)

import Text.ParserCombinators.Parsec (parse)

-- | Add a single constant to the signature of an Isabelle theory

addConst :: String -> Typ -> IsaTheory -> IsaTheory

addConst cName cType isaTh =

let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

isaTh_sign_ConstTab = constTab isaTh_sign

isaTh_sign_ConstTabUpdated =

Map.insert (mkVName cName) cType isaTh_sign_ConstTab

isaTh_sign_updated = isaTh_sign {

constTab = isaTh_sign_ConstTabUpdated

}

in (isaTh_sign_updated, isaTh_sen)

-- | Function to add a def command to an Isabelle theory

addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory

addDef name lhs rhs isaTh =

let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

sen = ConstDef (IsaEq lhs rhs)

namedSen = makeNamed name sen

in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Function to add an instance of command to an Isabelle theory. The

sort parameters here are basically strings. -}

addInstanceOf :: String -> [Sort] -> Sort -> [(String, Term)] -> IsaProof ->

IsaTheory -> IsaTheory

addInstanceOf name args res defs prf isaTh =

let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

sen = Instance name args res defs prf

namedSen = makeNamed name sen

in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Add a lemmas sentence (definition) that allow us to group large collections

of lemmas in to a single lemma. This cuts down on the repreated addition of

lemmas in the proofs. -}

addLemmasCollection :: String -> [String] -> IsaTheory -> IsaTheory

addLemmasCollection lemmaname lemmas isaTh =

if null lemmas

then isaTh

else let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

-- Make a named lemmas sentence

namedSen = (makeNamed lemmaname (Lemmas lemmaname lemmas))

{isAxiom = False}

in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Add a constant with a primrec defintion to the sentences of an Isabelle

theory. Parameters: constant name, type, primrec defintions and isabelle

theory to be added to. -}

addPrimRec :: String -> Typ -> [Term] -> IsaTheory -> IsaTheory

addPrimRec cName cType terms isaTh =

let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

primRecDef = RecDef {

keyword = Nothing, constName = mkVName cName,

constType = Just cType, primRecSenTerms = terms}

namedPrimRecDef = (makeNamed "BUG_what_does_this_word_do?" primRecDef) {

isAxiom = False,

isDef = True}

in (isaTh_sign, isaTh_sen ++ [namedPrimRecDef])

-- | Add a theorem with proof to an Isabelle theory

addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory ->

IsaTheory

addTheoremWithProof name conds concl proof' isaTh =

let isaTh_sign = fst isaTh

isaTh_sen = snd isaTh

sen = if null conds

then ((mkSen concl) {thmProof = Just proof'})

else ((mkCond conds concl) {thmProof = Just proof'})

namedSen = (makeNamed name sen) {isAxiom = False}

in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Prepare a theory for writing it out to a file. This function is based off

the function Isabelle.IsaProve.prepareTheory. The difference being that

this function does not mark axioms nor theorms as to be added to the

simplifier in Isabelle. -}

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, disAxs, disGoals,

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

-- | Add a DomainEntry to the domain tab of an Isabelle signature.

updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory

updateDomainTab domEnt (isaSign, isaSens) =

let oldDomTab = domainTab isaSign

isaSignUpdated = isaSign {domainTab = oldDomTab ++ [[domEnt]]}

in (isaSignUpdated, isaSens)

{- | Write out an Isabelle Theory. The theory should just run through

in Isabelle without any user interactions. This is based heavily

off Isabelle.IsaProve.isaProve -}

writeIsaTheory :: String -> Theory Sign Sentence () -> IO ()

writeIsaTheory thName th = do

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

-- thms = map senAttr ths

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

{- useaxs = filter (\ s ->

sentence s /= mkSen true && (isDef s ||

isSuffixOf "def" (senAttr s))) axs

defaultProof = Just $ IsaProof

(if null useaxs then [] else [Using $ map senAttr useaxs])

By Auto -}

thy = shows (printIsaTheory thBaseName sig $ axs ++ ths) "\n"

thyFile = thBaseName ++ ".thy"

-- Check if the Isabelle theory is a valid Isabelle theory

case parse parseTheory thyFile thy of

Right _ -> do

{- prepareThyFiles (ho, bo) thyFile thy

removeDepFiles thBaseName thms

isabelle <- getEnvDef "HETS_ISABELLE" "Isabelle"

callSystem $ isabelle ++ " " ++ thyFile

ok <- checkFinalThyFile (ho, bo) thyFile

if ok then getAllProofDeps m thBaseName thms

else return [] -}

writeFile thyFile thy

return ()

{- The Isabelle theory is not a valid theory (according to Hets)

as it cannot be parsed. -}

Left err -> do

print err

putStrLn $ "Sorry, a generated theory cannot be parsed, see: "

++ thyFile

writeFile thyFile thy

putStrLn "Aborting Isabelle proof attempt"

return ()