{-# 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 e :: TptpExpr
e) = "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]
++ ")."
show Null = ""
instance Show TptpExpr where
show :: TptpExpr -> String
show (Bin e1 :: TptpExpr
e1 op :: String
op e2 :: TptpExpr
e2) = "(" 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " 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]
++ ")"
show (Un op :: String
op e :: TptpExpr
e) = "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " 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]
++ ")"
show (Atom atom :: String
atom) = String
atom
show (Fun name :: String
name args :: [TptpExpr]
args) = String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((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]
++ ")"
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 c :: 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 str :: String
str
| "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
| "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 v :: Bool
v -> String -> TptpExpr
Atom (String -> TptpExpr) -> String -> TptpExpr
forall a b. (a -> b) -> a -> b
$ if Bool
v then "$true" else "$false"
ConstR v :: 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 _ v :: 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 _ c :: Expr
c e1 :: Expr
e1 e2 :: Expr
e2 -> TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (Expr -> TptpExpr
expr Expr
c) "=>" (Expr -> TptpExpr
expr Expr
e1))
"&" (TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (String -> TptpExpr -> TptpExpr
Un "~" (Expr -> TptpExpr
expr Expr
c)) "=>" (Expr -> TptpExpr
expr Expr
e2))
FunApp _ f :: String
f args :: [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 _ Not e :: 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 _ Neg e :: 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 _ op :: Op1
op e :: Expr
e -> String -> [TptpExpr] -> TptpExpr
Fun (Op1 -> String
showOp1 Op1
op) [Expr -> TptpExpr
expr Expr
e]
Op2 _ op :: Op2
op e1 :: Expr
e1 e2 :: Expr
e2 -> TptpExpr -> String -> TptpExpr -> TptpExpr
Bin (Expr -> TptpExpr
expr Expr
e1) (Op2 -> String
showOp2 Op2
op) (Expr -> TptpExpr
expr Expr
e2)
SVal _ f :: String
f ix :: SeqIndex
ix -> case SeqIndex
ix of
Fixed i :: 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
Var off :: 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]
++ "_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
Not -> "~"
Neg -> "-"
Abs -> "abs"
Exp -> "exp"
Sqrt -> "sqrt"
Log -> "log"
Sin -> "sin"
Tan -> "tan"
Cos -> "cos"
Asin -> "arcsin"
Atan -> "arctan"
Acos -> "arccos"
Sinh -> "sinh"
Tanh -> "tanh"
Cosh -> "cosh"
Asinh -> "arcsinh"
Atanh -> "arctanh"
Acosh -> "arccosh"
showOp2 :: Op2 -> String
showOp2 :: Op2 -> String
showOp2 = \case
Eq -> "="
Le -> "<="
Lt -> "<"
Ge -> ">="
Gt -> ">"
And -> "&"
Or -> "|"
Add -> "+"
Sub -> "-"
Mul -> "*"
Mod -> "mod"
Fdiv -> "/"
Pow -> "^"