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 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)
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)
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])
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])
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
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])
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])
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])
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)
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)
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
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
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"
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
String -> String -> IO ()
writeFile String
thyFile String
thy
() -> IO ()
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, 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 ()