{-# LANGUAGE GADTs, LambdaCase #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
import Copilot.Theorem.IL
import Data.List
data Tptp = Ax TptpExpr | Null
data TptpExpr = Bin TptpExpr String TptpExpr | Un String TptpExpr
| Atom String | Fun String [TptpExpr]
instance Show Tptp where
show :: Tptp -> String
show (Ax TptpExpr
e) = String
"fof(formula, axiom, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TptpExpr -> String
forall a. Show a => a -> String
show TptpExpr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")."
show Tptp
Null = String
""
instance Show TptpExpr where
show :: TptpExpr -> String
show (Bin TptpExpr
e1 String
op TptpExpr
e2) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TptpExpr -> String
forall a. Show a => a -> String
show TptpExpr
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TptpExpr -> String
forall a. Show a => a -> String
show TptpExpr
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Un String
op TptpExpr
e) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TptpExpr -> String
forall a. Show a => a -> String
show TptpExpr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Atom String
atom) = String
atom
show (Fun String
name [TptpExpr]
args) = String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((TptpExpr -> String) -> [TptpExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TptpExpr -> String
forall a. Show a => a -> String
show [TptpExpr]
args) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
instance SmtFormat Tptp where
push :: Tptp
push = Tptp
Null
pop :: Tptp
pop = Tptp
Null
checkSat :: Tptp
checkSat = Tptp
Null
setLogic :: String -> Tptp
setLogic = Tptp -> String -> Tptp
forall a b. a -> b -> a
const Tptp
Null
declFun :: String -> Type -> [Type] -> Tptp
declFun = (Type -> [Type] -> Tptp) -> String -> Type -> [Type] -> Tptp
forall a b. a -> b -> a
const ((Type -> [Type] -> Tptp) -> String -> Type -> [Type] -> Tptp)
-> (Type -> [Type] -> Tptp) -> String -> Type -> [Type] -> Tptp
forall a b. (a -> b) -> a -> b
$ ([Type] -> Tptp) -> Type -> [Type] -> Tptp
forall a b. a -> b -> a
const (([Type] -> Tptp) -> Type -> [Type] -> Tptp)
-> ([Type] -> Tptp) -> Type -> [Type] -> Tptp
forall a b. (a -> b) -> a -> b
$ Tptp -> [Type] -> Tptp
forall a b. a -> b -> a
const Tptp
Null
assert :: Expr -> Tptp
assert Expr
c = TptpExpr -> Tptp
Ax (TptpExpr -> Tptp) -> TptpExpr -> Tptp
forall a b. (a -> b) -> a -> b
$ Expr -> TptpExpr
expr Expr
c
interpret :: String -> Maybe SatResult
interpret :: String -> Maybe SatResult
interpret String
str
| String
"SZS status Unsatisfiable" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
str = SatResult -> Maybe SatResult
forall a. a -> Maybe a
Just SatResult
Unsat
| String
"SZS status" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
str = SatResult -> Maybe SatResult
forall a. a -> Maybe a
Just SatResult
Unknown
| Bool
otherwise = Maybe SatResult
forall a. Maybe a
Nothing
expr :: Expr -> TptpExpr
expr :: Expr -> TptpExpr
expr = \case
ConstB Bool
v -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ if Bool
v then String
"$true" else String
"$false"
ConstR Double
v -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ Double -> String
forall a. Show a => a -> String
show Double
v
ConstI Type
_ Integer
v -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
v
Ite Type
_ Expr
c Expr
e1 Expr
e2 -> TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (Expr -> TptpExpr
expr Expr
c) String
"=>" (Expr -> TptpExpr
expr Expr
e1))
String
"&" (TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (String -> TptpExpr -> TptpExpr
Un String
"~" (Expr -> TptpExpr
expr Expr
c)) String
"=>" (Expr -> TptpExpr
expr Expr
e2))
FunApp Type
_ String
f [Expr]
args -> String -> [TptpExpr] -> TptpExpr
Fun String
f ([TptpExpr] -> TptpExpr) -> [TptpExpr] -> TptpExpr
forall a b. (a -> b) -> a -> b
$ (Expr -> TptpExpr) -> [Expr] -> [TptpExpr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> TptpExpr
expr [Expr]
args
Op1 Type
_ Op1
Not Expr
e -> String -> TptpExpr -> TptpExpr
Un (Op1 -> String
showOp1 Op1
Not) (TptpExpr -> TptpExpr) -> TptpExpr -> TptpExpr
forall a b. (a -> b) -> a -> b
$ Expr -> TptpExpr
expr Expr
e
Op1 Type
_ Op1
Neg Expr
e -> String -> TptpExpr -> TptpExpr
Un (Op1 -> String
showOp1 Op1
Neg) (TptpExpr -> TptpExpr) -> TptpExpr -> TptpExpr
forall a b. (a -> b) -> a -> b
$ Expr -> TptpExpr
expr Expr
e
Op1 Type
_ Op1
op Expr
e -> String -> [TptpExpr] -> TptpExpr
Fun (Op1 -> String
showOp1 Op1
op) [Expr -> TptpExpr
expr Expr
e]
Op2 Type
_ Op2
op Expr
e1 Expr
e2 -> TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (Expr -> TptpExpr
expr Expr
e1) (Op2 -> String
showOp2 Op2
op) (Expr -> TptpExpr
expr Expr
e2)
SVal Type
_ String
f SeqIndex
ix -> case SeqIndex
ix of
Fixed Integer
i -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
Var Integer
off -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
off
showOp1 :: Op1 -> String
showOp1 :: Op1 -> String
showOp1 = \case
Op1
Not -> String
"~"
Op1
Neg -> String
"-"
Op1
Abs -> String
"abs"
Op1
Exp -> String
"exp"
Op1
Sqrt -> String
"sqrt"
Op1
Log -> String
"log"
Op1
Sin -> String
"sin"
Op1
Tan -> String
"tan"
Op1
Cos -> String
"cos"
Op1
Asin -> String
"arcsin"
Op1
Atan -> String
"arctan"
Op1
Acos -> String
"arccos"
Op1
Sinh -> String
"sinh"
Op1
Tanh -> String
"tanh"
Op1
Cosh -> String
"cosh"
Op1
Asinh -> String
"arcsinh"
Op1
Atanh -> String
"arctanh"
Op1
Acosh -> String
"arccosh"
showOp2 :: Op2 -> String
showOp2 :: Op2 -> String
showOp2 = \case
Op2
Eq -> String
"="
Op2
Le -> String
"<="
Op2
Lt -> String
"<"
Op2
Ge -> String
">="
Op2
Gt -> String
">"
Op2
And -> String
"&"
Op2
Or -> String
"|"
Op2
Add -> String
"+"
Op2
Sub -> String
"-"
Op2
Mul -> String
"*"
Op2
Mod -> String
"mod"
Op2
Fdiv -> String
"/"
Op2
Pow -> String
"^"