{- |
Module      :  ./CspCASLProver/IsabelleUtils.hs
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 :: String -> Typ -> IsaTheory -> IsaTheory
addConst cName :: String
cName cType :: Typ
cType isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        isaTh_sign_ConstTab :: ConstTab
isaTh_sign_ConstTab = Sign -> ConstTab
constTab Sign
isaTh_sign
        isaTh_sign_ConstTabUpdated :: ConstTab
isaTh_sign_ConstTabUpdated =
            VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> VName
mkVName String
cName) Typ
cType ConstTab
isaTh_sign_ConstTab
        isaTh_sign_updated :: Sign
isaTh_sign_updated = Sign
isaTh_sign {
                               constTab :: ConstTab
constTab = ConstTab
isaTh_sign_ConstTabUpdated
                             }
    in (Sign
isaTh_sign_updated, [Named Sentence]
isaTh_sen)

-- | Function to add a def command to an Isabelle theory
addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory
addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory
addDef name :: String
name lhs :: Term
lhs rhs :: Term
rhs isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        sen :: Sentence
sen = Term -> Sentence
ConstDef (Term -> Term -> Term
IsaEq Term
lhs Term
rhs)
        namedSen :: Named Sentence
namedSen = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
name Sentence
sen
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
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 :: String
-> [Sort]
-> Sort
-> [(String, Term)]
-> IsaProof
-> IsaTheory
-> IsaTheory
addInstanceOf name :: String
name args :: [Sort]
args res :: Sort
res defs :: [(String, Term)]
defs prf :: IsaProof
prf isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        sen :: Sentence
sen = String
-> [Sort] -> Sort -> [(String, Term)] -> IsaProof -> Sentence
Instance String
name [Sort]
args Sort
res [(String, Term)]
defs IsaProof
prf
        namedSen :: Named Sentence
namedSen = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
name Sentence
sen
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
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 :: String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection lemmaname :: String
lemmaname lemmas :: [String]
lemmas isaTh :: IsaTheory
isaTh =
    if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
lemmas
    then IsaTheory
isaTh
    else let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
             isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
             -- Make a named lemmas sentence
             namedSen :: Named Sentence
namedSen = (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
lemmaname (String -> [String] -> Sentence
Lemmas String
lemmaname [String]
lemmas))
                        {isAxiom :: Bool
isAxiom = Bool
False}
         in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
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 :: String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec cName :: String
cName cType :: Typ
cType terms :: [Term]
terms isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        primRecDef :: Sentence
primRecDef = RecDef :: Maybe String -> VName -> Maybe Typ -> [Term] -> Sentence
RecDef {
          keyword :: Maybe String
keyword = Maybe String
forall a. Maybe a
Nothing, constName :: VName
constName = String -> VName
mkVName String
cName,
          constType :: Maybe Typ
constType = Typ -> Maybe Typ
forall a. a -> Maybe a
Just Typ
cType, primRecSenTerms :: [Term]
primRecSenTerms = [Term]
terms}
        namedPrimRecDef :: Named Sentence
namedPrimRecDef = (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "BUG_what_does_this_word_do?" Sentence
primRecDef) {
          isAxiom :: Bool
isAxiom = Bool
False,
          isDef :: Bool
isDef = Bool
True}
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
namedPrimRecDef])

-- | Add a theorem with proof to an Isabelle theory
addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory ->
                      IsaTheory
addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof name :: String
name conds :: [Term]
conds concl :: Term
concl proof' :: IsaProof
proof' isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        sen :: Sentence
sen = if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
conds
              then ((Term -> Sentence
mkSen Term
concl) {thmProof :: Maybe IsaProof
thmProof = IsaProof -> Maybe IsaProof
forall a. a -> Maybe a
Just IsaProof
proof'})
              else (([Term] -> Term -> Sentence
mkCond [Term]
conds Term
concl) {thmProof :: Maybe IsaProof
thmProof = IsaProof -> Maybe IsaProof
forall a. a -> Maybe a
Just IsaProof
proof'})
        namedSen :: Named Sentence
namedSen = (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
name Sentence
sen) {isAxiom :: Bool
isAxiom = Bool
False}
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
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 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' = (String -> String) -> [Named Sentence] -> [Named Sentence]
forall a. (String -> String) -> [Named a] -> [Named a]
prepareSenNames String -> String
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]
disAxs, [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)

-- | Add a DomainEntry to the domain tab of an Isabelle signature.
updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab domEnt :: DomainEntry
domEnt (isaSign :: Sign
isaSign, isaSens :: [Named Sentence]
isaSens) =
    let oldDomTab :: DomainTab
oldDomTab = Sign -> DomainTab
domainTab Sign
isaSign
        isaSignUpdated :: Sign
isaSignUpdated = Sign
isaSign {domainTab :: DomainTab
domainTab = DomainTab
oldDomTab DomainTab -> DomainTab -> DomainTab
forall a. [a] -> [a] -> [a]
++ [[DomainEntry
domEnt]]}
    in (Sign
isaSignUpdated, [Named Sentence]
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 :: String -> Theory Sign Sentence () -> IO ()
writeIsaTheory thName :: String
thName th :: Theory Sign Sentence ()
th = do
  let (sig :: Sign
sig, axs :: [Named Sentence]
axs, ths :: [Named Sentence]
ths, _) = Theory Sign Sentence ()
-> (Sign, [Named Sentence], [Named Sentence], Map String String)
prepareTheory Theory Sign Sentence ()
th
      -- thms = map senAttr ths
      thBaseName :: String
thBaseName = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '/') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
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 :: String
thy = Doc -> String -> String
forall a. Show a => a -> String -> String
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]
ths) "\n"
      thyFile :: String
thyFile = String
thBaseName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".thy"
  -- Check if the Isabelle theory is a valid Isabelle theory
  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 _ -> 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 [] -}
      String -> String -> IO ()
writeFile String
thyFile String
thy
      () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    {- The Isabelle theory is not a valid theory (according to Hets)
    as it cannot be parsed. -}
    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, a generated theory cannot be parsed, see: "
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thyFile
      String -> String -> IO ()
writeFile String
thyFile String
thy
      String -> IO ()
putStrLn "Aborting Isabelle proof attempt"
      () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()