{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards
  , StandaloneDeriving
  , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
  , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
  , RankNTypes
  #-}
{-# OPTIONS -Wall #-}
module Codec.TPTP.Export(toTPTP',ToTPTP(..),isLowerWord) where

import Codec.TPTP.Base
import Control.Monad.Identity
import Data.Ratio

-- | Convenient wrapper for 'toTPTP'
toTPTP' :: forall a. (ToTPTP a) => a -> String
toTPTP' :: forall a. ToTPTP a => a -> String
toTPTP' = ((String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"") ((String -> String) -> String)
-> (a -> String -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP

s :: String -> String -> String
s :: String -> String -> String
s = String -> String -> String
showString

comma :: String -> String
comma :: String -> String
comma = String -> String -> String
s String
","

commaSepMap :: forall a.
               (a -> String -> String) -> [a] -> String -> String
commaSepMap :: forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap a -> String -> String
_ [] = String -> String -> String
s String
""
commaSepMap a -> String -> String
f (a
y:[a]
ys) = a -> String -> String
f a
y (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (String -> String) -> String -> String)
-> (String -> String) -> [a] -> String -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x String -> String
xs -> String -> String
comma (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String -> String
f a
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
xs) String -> String
forall a. a -> a
id [a]
ys




class ToTPTP a where
    -- | Convert to TPTP
    toTPTP :: a -> ShowS

instance ToTPTP [TPTP_Input] where
    toTPTP :: [TPTP_Input] -> String -> String
toTPTP = (TPTP_Input -> (String -> String) -> String -> String)
-> (String -> String) -> [TPTP_Input] -> String -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\TPTP_Input
x String -> String
xs -> TPTP_Input -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP TPTP_Input
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"\n" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
xs) String -> String
forall a. a -> a
id

instance ToTPTP TPTP_Input where
    toTPTP :: TPTP_Input -> String -> String
toTPTP AFormula{F Identity
AtomicWord
Role
Annotations
name :: AtomicWord
role :: Role
formula :: F Identity
annotations :: Annotations
name :: forall (c :: * -> *). TPTP_Input_ c -> AtomicWord
role :: forall (c :: * -> *). TPTP_Input_ c -> Role
formula :: forall (c :: * -> *). TPTP_Input_ c -> F c
annotations :: forall (c :: * -> *). TPTP_Input_ c -> Annotations
..} =
        String -> String -> String
s String
"fof(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
name (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
comma (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Role -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP Role
role (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
comma (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          F Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP F Identity
formula (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotations -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP Annotations
annotations (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")."

    toTPTP (Comment String
x) =
        String -> String -> String
s String
x -- % included in x

    toTPTP (Include String
x [AtomicWord]
sel) = String -> String -> String
s String
"include" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString (String -> String
tptpSQuote String
x) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.

                             case [AtomicWord]
sel of { [] -> String -> String
forall a. a -> a
id; [AtomicWord]
_ -> String -> String -> String
s String
",[" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AtomicWord -> String -> String)
-> [AtomicWord] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [AtomicWord]
sel (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"]" } (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.


                             String -> String -> String
s String
")."


instance ToTPTP Role where
    toTPTP :: Role -> String -> String
toTPTP (Role String
x) = String -> String -> String
s String
x

instance ToTPTP Quant where
    toTPTP :: Quant -> String -> String
toTPTP Quant
All = String -> String -> String
s String
"!"
    toTPTP Quant
Exists = String -> String -> String
s String
"?"

instance ToTPTP InfixPred where
    toTPTP :: InfixPred -> String -> String
toTPTP InfixPred
x = case InfixPred
x of
        InfixPred
(:=:)  -> String -> String -> String
s String
"="
        InfixPred
(:!=:) -> String -> String -> String
s String
"!="

instance ToTPTP BinOp where
    toTPTP :: BinOp -> String -> String
toTPTP BinOp
x = case BinOp
x of
        BinOp
(:<=>:) -> String -> String -> String
s String
"<=>"
        BinOp
(:=>:)  -> String -> String -> String
s String
"=>"
        BinOp
(:<=:)  -> String -> String -> String
s String
"<="
        BinOp
(:&:)   -> String -> String -> String
s String
"&"
        BinOp
(:|:)   -> String -> String -> String
s String
"|"
        BinOp
(:~&:)  -> String -> String -> String
s String
"~&"
        BinOp
(:~|:)  -> String -> String -> String
s String
"~|"
        BinOp
(:<~>:) -> String -> String -> String
s String
"<~>"

instance (ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) where
    toTPTP :: Formula0 t f -> String -> String
toTPTP Formula0 t f
formu =
      let
        result :: String -> String
result =
           case Formula0 t f
formu of
               Quant Quant
q [V]
vars f
f    ->
                   let par :: Bool
par = Bool
True in

                   Quant -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP Quant
q
                      (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" ["
                      (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V -> String -> String) -> [V] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap V -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [V]
vars
                      (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"] : "
                      (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> (String -> String) -> String -> String
showParen Bool
par (f -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP f
f)

               PredApp AtomicWord
p [] -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
p
               PredApp AtomicWord
p [t]
args -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
p (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> String -> String) -> [t] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap t -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [t]
args (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"
               (:~:) f
f -> String -> String -> String
s String
"~ " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> (String -> String) -> String -> String
showParen Bool
True (f -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP f
f)

               BinOp f
x BinOp
op f
y -> Bool -> (String -> String) -> String -> String
showParen Bool
True ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
                   (f -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP f
x) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinOp -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP BinOp
op (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP f
y)

               InfixPred t
x InfixPred
op t
y -> Bool -> (String -> String) -> String -> String
showParen Bool
True ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
                   (t -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP t
x) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InfixPred -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP InfixPred
op (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP t
y)
      in
        String -> String
result

instance ToTPTP t => ToTPTP (Term0 t) where
    toTPTP :: Term0 t -> String -> String
toTPTP Term0 t
term =

             case Term0 t
term of
               Var V
x -> V -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP V
x
               NumberLitTerm Rational
d -> Rational -> String -> String
showsRational Rational
d
               DistinctObjectTerm String
x -> String -> String -> String
showString (String -> String
tptpQuote String
x)
               FunApp AtomicWord
f [] -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
f
               FunApp AtomicWord
f [t]
args -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
f (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> String -> String) -> [t] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap t -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [t]
args (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"


deriving instance (ToTPTP a) => (ToTPTP (Identity a))
deriving instance ToTPTP Formula
deriving instance ToTPTP Term


instance ToTPTP Annotations where
    toTPTP :: Annotations -> String -> String
toTPTP Annotations
NoAnnotations = String -> String -> String
s String
""
    toTPTP (Annotations GTerm
a UsefulInfo
b) = String -> String -> String
s String
"," (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GTerm -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP GTerm
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsefulInfo -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP UsefulInfo
b

instance ToTPTP UsefulInfo where
    toTPTP :: UsefulInfo -> String -> String
toTPTP UsefulInfo
NoUsefulInfo = String -> String -> String
s String
""
    toTPTP (UsefulInfo [GTerm]
xs) = String -> String -> String
s String
"," (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"[" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GTerm -> String -> String) -> [GTerm] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap GTerm -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [GTerm]
xs (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"]"

instance ToTPTP GTerm where
    toTPTP :: GTerm -> String -> String
toTPTP GTerm
gt = case GTerm
gt of
                  GTerm GData
x -> GData -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP GData
x
                  ColonSep GData
x GTerm
y -> GData -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP GData
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
":" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GTerm -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP GTerm
y
                  GList [GTerm]
xs -> String -> String -> String
s String
"[" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GTerm -> String -> String) -> [GTerm] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap GTerm -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [GTerm]
xs (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"]"

instance ToTPTP AtomicWord where
    toTPTP :: AtomicWord -> String -> String
toTPTP (AtomicWord String
x) = String -> String -> String
s (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ if String -> Bool
isLowerWord String
x then String
x else String -> String
tptpSQuote String
x

instance ToTPTP GData where
 toTPTP :: GData -> String -> String
toTPTP GData
gd = case GData
gd of
   GWord AtomicWord
x -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
x
   GApp AtomicWord
x [GTerm]
args -> AtomicWord -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP AtomicWord
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GTerm -> String -> String) -> [GTerm] -> String -> String
forall a. (a -> String -> String) -> [a] -> String -> String
commaSepMap GTerm -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP [GTerm]
args (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"
   GVar V
x -> V -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP V
x
   GNumber Rational
x -> Rational -> String -> String
showsRational Rational
x
   GDistinctObject String
x -> String -> String -> String
showString (String -> String
tptpQuote String
x)
   GFormulaData str :: String
str@String
"$cnf" F Identity
formu -> String -> String -> String
s String
str (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F Identity -> String -> String
cnfToTPTP F Identity
formu (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"
     where
       cnfToTPTP :: Formula -> ShowS
       cnfToTPTP :: F Identity -> String -> String
cnfToTPTP (F (Identity (BinOp F Identity
l BinOp
(:|:) F Identity
r))) = F Identity -> String -> String
cnfToTPTP F Identity
l (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" | " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F Identity -> String -> String
cnfToTPTP F Identity
r
       cnfToTPTP (F (Identity ((:~:) x :: F Identity
x@(F (Identity (PredApp AtomicWord
_ [T Identity]
_)))))) = String -> String -> String
s String
"~ " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP F Identity
x
       cnfToTPTP x :: F Identity
x@(F (Identity (PredApp AtomicWord
_ [T Identity]
_))) = F Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP F Identity
x
       -- We do not call toTPTP directly on the formula in InfixPred case, because parenthesis should not be printed.
       cnfToTPTP (F (Identity (InfixPred T Identity
x1 InfixPred
(:!=:) T Identity
x2))) = T Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP T Identity
x1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
" != " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP T Identity
x2
       cnfToTPTP F Identity
x = String -> String -> String
forall a. HasCallStack => String -> a
error (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ F Identity -> String
forall a. Show a => a -> String
show F Identity
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a literal"

   GFormulaData String
str F Identity
formu -> String -> String -> String
s String
str (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP F Identity
formu (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"
   GFormulaTerm String
str T Identity
term -> String -> String -> String
s String
str (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
"(" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T Identity -> String -> String
forall a. ToTPTP a => a -> String -> String
toTPTP T Identity
term (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
s String
")"

tptpQuote :: [Char] -> [Char]
tptpQuote :: String -> String
tptpQuote String
x = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
go String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
    where
      go :: Char -> String
go Char
'\\' = String
"\\\\"
      go Char
'"'  = String
"\\\""
      go Char
c = [Char
c]

tptpSQuote :: [Char] -> [Char]
tptpSQuote :: String -> String
tptpSQuote String
x = String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
go String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
    where
      go :: Char -> String
go Char
'\\' = String
"\\\\"
      go Char
'\''  = String
"\\'"
      go Char
c = [Char
c]



isBetween :: forall a. (Ord a) => a -> a -> a -> Bool
isBetween :: forall a. Ord a => a -> a -> a -> Bool
isBetween a
a a
x a
b = a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b

isReallyAlnum :: Char -> Bool
isReallyAlnum :: Char -> Bool
isReallyAlnum Char
x = Char -> Char -> Char -> Bool
forall a. Ord a => a -> a -> a -> Bool
isBetween Char
'a' Char
x Char
'z' Bool -> Bool -> Bool
|| Char -> Char -> Char -> Bool
forall a. Ord a => a -> a -> a -> Bool
isBetween Char
'A' Char
x Char
'Z' Bool -> Bool -> Bool
|| Char -> Char -> Char -> Bool
forall a. Ord a => a -> a -> a -> Bool
isBetween Char
'0' Char
x Char
'9' Bool -> Bool -> Bool
|| Char
xChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'_'

isLowerWord :: [Char] -> Bool
isLowerWord :: String -> Bool
isLowerWord String
str = case String
str of
                               (Char
x:String
xs) | Char -> Char -> Char -> Bool
forall a. Ord a => a -> a -> a -> Bool
isBetween Char
'a' Char
x Char
'z' Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isReallyAlnum String
xs -> Bool
True
                               String
_ -> Bool
False

instance ToTPTP V where
    toTPTP :: V -> String -> String
toTPTP (V String
x) = String -> String -> String
s String
x


showsRational :: Rational -> ShowS
showsRational :: Rational -> String -> String
showsRational Rational
q = Integer -> String -> String
forall a. Show a => a -> String -> String
shows (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
q) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'/' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String -> String
forall a. Show a => a -> String -> String
shows (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
q)