--------------------------------------------------------------------------------

{-# 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
"^"

--------------------------------------------------------------------------------