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

{-# LANGUAGE GADTs, 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 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

-- | Parse a satisfiability result.
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   -> "^"

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