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

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