(** Printing {!Form} formulas to TPTP format. *)

open Fol
open Printf

(* Possible Flags : 
   TimeOut [ default 5]
   PairAxioms [default on] 
   OrderAxioms [default off] 
   ArithAxioms [default off] 
   TranslationMode [default FunctionSymbols but Predicates is possible]
   ParadoxInteractive [default off]
   Spliting [default on]
   SortGuards [default off]
   Debug [default off]
*)



(** input formats of supported provers *)
let input_format = "tptp"

let tptp_var_ident s = 
  "Var_" ^ s

let tptp_const_ident s =
  "const_" ^ s

let total_proof_obligations = ref 0
let fresh_tptp_var_counter = ref 0

let fresh_uppercase_ident i = 
     incr fresh_tptp_var_counter;
     (String.capitalize i ^ "__tptp_" ^ (string_of_int !fresh_tptp_var_counter))
       
let fresh_lowercase_ident i = 
     incr fresh_tptp_var_counter;
     (String.uncapitalize i ^ "__tptp__" ^ (string_of_int !fresh_tptp_var_counter))

let fof_formula = "fof"

(** (FOL) form -> string *)
let tptp_pretty_print (f : fol_formula) : string = 

  let rec p s = "(" ^ s ^ ")" 

  and print_term : term -> string = function
    | _, `Int k -> string_of_int k
    | _, `Variable v -> tptp_var_ident v
    | _, `Constant c -> tptp_const_ident c
    | _, `Function (f, args) -> sprintf "%s(%s)" (tptp_const_ident f) (String.concat ", " (ListLabels.map ~f:print_term args))
    
  and print_bool : boool -> string = function
	       | `True -> "vrai"
	       | `False -> "~vrai"
	       | `BoolVar v -> tptp_const_ident v
	       | `NegatedBoolVar v -> "~" ^ tptp_const_ident v
	  
  and print_atom : fol_atom -> string = function
    | `Predicate (p, args) -> sprintf "%s(%s)" (tptp_const_ident p) (String.concat ", " (ListLabels.map ~f:print_term args)) 
    | `Equality (t1, t2) ->  sprintf "(%s = %s)" (print_term t1) (print_term t2)


  and tptp_pretty_print_binder b vars f =
    let v_names = String.concat ", " (List.map (fun (v,s) -> tptp_var_ident v) vars) in
    p ( b ^ " [" ^ v_names ^ "] : " ^ p (foo f))
  

  and foo : fol_formula -> string = function
    | `Forall (v, f) -> tptp_pretty_print_binder "!" v f
    | `Exists (v, f) -> tptp_pretty_print_binder "?" v f
    | #boool as b -> print_bool b
    | #fol_atom as a -> print_atom a
    | `Conjunction [] -> "vrai"
    | `Disjunction [] -> "~vrai"
    | `Conjunction fs -> p (String.concat " & " (ListLabels.map ~f:foo fs)) 
    | `Disjunction fs -> p (String.concat " | " (ListLabels.map ~f:foo fs)) 
    | `Negation f ->  (
        "~" ^ p (foo f)
      )

  in
    foo f
 

let tptp_pretty_print_hyps (hyps : fol_formula list) =
  String.concat "\n\n\n" 
    (List.map 
      (fun new_f -> sprintf "%s(%s, hypothesis, %s)." (fof_formula) (fresh_lowercase_ident "hyp") (tptp_pretty_print new_f))
      hyps
    ) 
  ^ "\n\n\nfof(hyp__vrai, hypothesis, vrai).\n"
    
let tptp_pretty_print_goal (goalname : string) (new_goal : fol_formula) =
  sprintf "%s(%s, conjecture, %s)." (fof_formula) ("goal_" ^ goalname) (tptp_pretty_print new_goal)