{-# LANGUAGE GADTs      #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Safe       #-}

-- | A backend to <http://www.tptp.org/ TPTP>, enabling to produce assertions
-- and to parse the results from TPTP.
module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where

import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))
import Copilot.Theorem.IL

import Data.List

-- | Type used to represent TPTP expressions.
--
-- Although this type implements the 'SmtFormat' interface, only 'assert' is
-- actually used.
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, " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TptpExpr
e 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
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TptpExpr
e1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
op forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TptpExpr
e2 forall a. [a] -> [a] -> [a]
++ String
")"
  show (Un String
op TptpExpr
e)       = String
"(" forall a. [a] -> [a] -> [a]
++ String
op forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TptpExpr
e forall a. [a] -> [a] -> [a]
++ String
")"
  show (Atom String
atom)     = String
atom
  show (Fun String
name [TptpExpr]
args) = String
name forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [TptpExpr]
args) 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 = forall a b. a -> b -> a
const Tptp
Null
  declFun :: String -> Type -> [Type] -> Tptp
declFun  = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Tptp
Null
  assert :: Expr -> Tptp
assert Expr
c = TptpExpr -> Tptp
Ax forall a b. (a -> b) -> a -> b
$ Expr -> TptpExpr
expr Expr
c

-- | Parse a satisfiability result.
interpret :: String -> Maybe SatResult
interpret :: String -> Maybe SatResult
interpret String
str
  | String
"SZS status Unsatisfiable" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
str = forall a. a -> Maybe a
Just SatResult
Unsat
  | String
"SZS status"               forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
str = forall a. a -> Maybe a
Just SatResult
Unknown
  | Bool
otherwise                                   = forall a. Maybe a
Nothing

expr :: Expr -> TptpExpr
expr :: Expr -> TptpExpr
expr = \case
  ConstB Bool
v        -> String -> TptpExpr
Atom forall a b. (a -> b) -> a -> b
$ if Bool
v then String
"$true" else String
"$false"
  ConstR Double
v        -> String -> TptpExpr
Atom forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Double
v
  ConstI Type
_ Integer
v      -> String -> TptpExpr
Atom forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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) 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) 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 forall a b. (a -> b) -> a -> b
$ String
f forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i
                       Var Integer
off -> String -> TptpExpr
Atom forall a b. (a -> b) -> a -> b
$ String
f forall a. [a] -> [a] -> [a]
++ String
"_n" forall a. [a] -> [a] -> [a]
++ 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
"^"