module PropaFP.Translators.MetiTarski where

import MixedTypesNumPrelude

import PropaFP.Expression

-- import Data.List
import Data.Ratio
import Data.Char (toUpper)
import PropaFP.VarMap
import Data.List (intercalate)

formulaToTPTP :: F -> Integer -> String
formulaToTPTP :: F -> Integer -> String
formulaToTPTP (FConn Conn
op F
f1 F
f2) Integer
numTabs = 
  case Conn
op of
    Conn
And     -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"&"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Conn
Or      -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Conn
Impl    -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"=>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToTPTP (FComp Comp
op E
e1 E
e2) Integer
numTabs =
  case Comp
op of
    Comp
Ge -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Gt -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Le -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"<=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Lt -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"<"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Eq -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"="  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToTPTP (FNot F
f) Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"~(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToTPTP F
FTrue Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(0 = 0)"
formulaToTPTP F
FFalse Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(0 = 1)"

expressionToTPTP :: E -> String
expressionToTPTP :: E -> String
expressionToTPTP (EBinOp BinOp
op E
e1 E
e2) =
  case BinOp
op of
    BinOp
Add -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Sub -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mul -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Div -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Min -> String
"(min(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
    BinOp
Max -> String
"(max(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
    BinOp
Pow -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mod -> String -> String
forall a. HasCallStack => String -> a
error String
"Modulo is not supported in tptp"
expressionToTPTP (EUnOp UnOp
op E
e) =
  case UnOp
op of
    UnOp
Sqrt -> String
"(sqrt(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
    UnOp
Negate -> String
"(-1 * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Abs -> String
"(abs(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
    UnOp
Sin -> String
"(sin(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
    UnOp
Cos -> String
"(cos(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
expressionToTPTP (RoundToInteger RoundingMode
m E
e) = 
  case RoundingMode
m of
    RoundingMode
RNE -> String
"round(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String -> String
forall a. HasCallStack => String -> a
error String
"Round Towards Ceiling not supported in TPTP" -- "ceiling(" ++ expressionToTPTP e ++ ")"
    RoundingMode
RTN -> String
"floor(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String -> String
forall a. HasCallStack => String -> a
error String
"Round Towards Zero not supported in TPTP"
    RoundingMode
RNA -> String -> String
forall a. HasCallStack => String -> a
error String
"Round Nearest Away not supported in TPTP"
expressionToTPTP (PowI E
e Integer
i) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToTPTP (Var String
e) = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
e
expressionToTPTP (Lit Rational
e) = 
  case Rational -> Integer
forall a. Ratio a -> a
denominator Rational
e of
    Integer
1 -> Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
e)
    Integer
_ ->
      String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
e) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
e) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToTPTP E
Pi = String
"pi"
expressionToTPTP (Float RoundingMode
_ E
_)   = String
"MetiTarski translator does not support Floats"
expressionToTPTP (Float32 RoundingMode
_ E
_) = String
"MetiTarski translator does not support Floats"
expressionToTPTP (Float64 RoundingMode
_ E
_) = String
"MetiTarski translator does not support Floats"

formulaAndVarMapToMetiTarski :: F -> TypedVarMap -> String
formulaAndVarMapToMetiTarski :: F -> TypedVarMap -> String
formulaAndVarMapToMetiTarski F
f TypedVarMap
typedVarMap =
  String
"fof(vc,conjecture," String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
  case TypedVarMap
typedVarMap of
    []  -> String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f Integer
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n)."
    TypedVarMap
_   -> String
"\n\t! [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((TypedVarInterval -> String) -> TypedVarMap -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(TypedVar (String
v,(Rational, Rational)
_) VarType
_) -> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
v) TypedVarMap
typedVarMap) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] : (" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
variablesAsString TypedVarMap
typedVarMap String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t) =>" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToTPTP F
f Integer
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t))" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n)."
  where
    variablesAsString :: TypedVarMap -> String
variablesAsString [] = String
""
    variablesAsString ((TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
_) : TypedVarMap
typedVarIntervals) =
      let 
        varNameUpper :: String
varNameUpper = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
varName
        leftBoundString :: String
leftBoundString = Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
leftBound) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
leftBound)
        rightBoundString :: String
rightBoundString = Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
rightBound) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
rightBound)
      in
        String
"\n\t\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
leftBoundString String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varNameUpper String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" & " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varNameUpper String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rightBoundString String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if TypedVarMap -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null TypedVarMap
typedVarIntervals then String
"" else String
" &" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
variablesAsString TypedVarMap
typedVarIntervals)

disjunctionExpressionsToSMT :: [E] -> String
disjunctionExpressionsToSMT :: [E] -> String
disjunctionExpressionsToSMT []        = String
""
disjunctionExpressionsToSMT [E
e]       = E -> String
expressionToTPTP E
e
disjunctionExpressionsToSMT (E
e : [E]
es)  = String
"(max " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ [E] -> String
disjunctionExpressionsToSMT [E]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

cnfExpressionsToSMT :: [[E]] -> String
cnfExpressionsToSMT :: [[E]] -> String
cnfExpressionsToSMT []        = String
""
cnfExpressionsToSMT [[E]
e]       = [E] -> String
disjunctionExpressionsToSMT [E]
e
cnfExpressionsToSMT ([E]
e : [[E]]
es)  = String
"(min " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [E] -> String
disjunctionExpressionsToSMT [E]
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ [[E]] -> String
cnfExpressionsToSMT [[E]]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

disjunctionExpressionsToTptp :: [ESafe] -> String
disjunctionExpressionsToTptp :: [ESafe] -> String
disjunctionExpressionsToTptp []        = String
""
disjunctionExpressionsToTptp [ESafe
eSafe]       = 
  case ESafe
eSafe of
    EStrict E
e    -> String
"\n\t\t\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" > 0.0"
    ENonStrict E
e -> String
"\n\t\t\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToTPTP E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" >= 0.0"
disjunctionExpressionsToTptp (ESafe
e : [ESafe]
es)  = [ESafe] -> String
disjunctionExpressionsToTptp [ESafe
e] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t\t\t|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ESafe] -> String
disjunctionExpressionsToTptp [ESafe]
es

cnfExpressionsToTptp :: [[ESafe]] -> String
cnfExpressionsToTptp :: [[ESafe]] -> String
cnfExpressionsToTptp []        = String
""
cnfExpressionsToTptp [[ESafe]
e]       = String
"\n\t\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ESafe] -> String
disjunctionExpressionsToTptp [ESafe]
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t\t)"
cnfExpressionsToTptp ([ESafe]
e : [[ESafe]]
es)  = String
"\n\t\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ESafe] -> String
disjunctionExpressionsToTptp [ESafe]
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t\t)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t\t&" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [[ESafe]] -> String
cnfExpressionsToTptp [[ESafe]]
es

cnfExpressionAndDomainsToMetiTarski :: [[ESafe]] -> [(String, (Rational, Rational))] -> String
cnfExpressionAndDomainsToMetiTarski :: [[ESafe]] -> [(String, (Rational, Rational))] -> String
cnfExpressionAndDomainsToMetiTarski [[ESafe]]
cnf [(String, (Rational, Rational))]
realDomains =
  String
"fof(vc,conjecture, " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"\n\t! [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (((String, (Rational, Rational)) -> String)
-> [(String, (Rational, Rational))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
v,(Rational, Rational)
_) -> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
v) [(String, (Rational, Rational))]
realDomains) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] : " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  case [(String, (Rational, Rational))]
realDomains of
    [] ->       
      [[ESafe]] -> String
cnfExpressionsToTptp [[ESafe]]
cnf String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"\n\t))."
    [(String, (Rational, Rational))]
_ ->
      String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
       String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n\t& " (((String, (Rational, Rational)) -> String)
-> [(String, (Rational, Rational))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
x',(Rational
l,Rational
u)) -> let x :: String
x = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
x' in Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" & " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
u) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
u)) [(String, (Rational, Rational))]
realDomains) String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"\n\t) =>" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [[ESafe]] -> String
cnfExpressionsToTptp [[ESafe]]
cnf String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"\n\t)" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"\n\t))."

runMetiTarskiTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> IO ()
runMetiTarskiTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> IO ()
runMetiTarskiTranslatorCNFWithVarMap [[ESafe]]
cnf [(String, (Rational, Rational))]
realVarMap =
  do
  String -> IO ()
putStrLn String
"Running Haskell to dReal translator for Expressions"
  String -> IO ()
putStr String
"Enter target file name: "
  String
fileName <- IO String
getLine
  String -> String -> IO ()
writeFile String
fileName (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [[ESafe]] -> [(String, (Rational, Rational))] -> String
cnfExpressionAndDomainsToMetiTarski [[ESafe]]
cnf [(String, (Rational, Rational))]
realVarMap