(** 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]
*)


type enumeration = {
  enum_fonctions : ident list;
  enum_predicats : ident list;
}

let enum_vide = {
  enum_fonctions = [];
  enum_predicats = [];
}

let rec enum_terme
    (en : enumeration)
    (_, t : term)
    : enumeration = match t with
      | `Constant i when not (List.mem i en.enum_fonctions)
 ->
          {en with enum_fonctions = ("const__" ^ i)::en.enum_fonctions}
      | `Function (i, tl) ->
          let en2 =
            if List.mem i en.enum_fonctions
            then en
            else {en with enum_fonctions = ("fun__" ^ i)::en.enum_fonctions}
          in List.fold_left enum_terme en2 tl
      | _ -> en

let rec enum_formule
    (en : enumeration)
    : fol_formula -> enumeration = function
      | `Equality (t1, t2) ->
          enum_terme (enum_terme en t1) t2
      | `Predicate (i, tl) ->
          let en2 =
            if List.mem i en.enum_predicats
            then en
            else {en with enum_predicats = ("pred__" ^ i)::en.enum_predicats}
          in List.fold_left enum_terme en2 tl
      | `Conjunction l | `Disjunction l -> List.fold_left enum_formule en l
      | `Forall (_, f) | `Exists (_, f) | `Negation f -> enum_formule en f
      | _ -> en


let rec string_of_term
    (_, t : term)
    : string = match t with

      | `Int i -> string_of_int i
      | `Constant i -> "const__" ^ i
      | `Variable i -> "var__" ^ i
      | `Function (i, tl) -> "fun__" ^ i ^ "(" ^ String.concat "," (List.map string_of_term tl) ^ ")"

let rec string_of_formula : fol_formula -> string = function
  | `True -> "true"
  | `False -> "false"
  | `BoolVar i -> "var__" ^ i
  | `NegatedBoolVar i -> "not(var__" ^ i ^ ")"
  | `Predicate (i, tl) -> "pred__" ^ i ^ "(" ^ String.concat "," (List.map string_of_term tl) ^ ")"
  | `Equality (t1, t2) -> "equal(" ^ string_of_term t1 ^ "," ^ string_of_term t2 ^ ")"
  | `Conjunction [] -> "true"
  | `Conjunction [f] | `Disjunction [f] | `Exists ([], f) | `Forall ([], f) ->
      string_of_formula f
  | `Conjunction l -> "and(" ^ String.concat "," (List.map string_of_formula l) ^ ")"
  | `Disjunction [] -> "false"
  | `Disjunction l -> "or(" ^ String.concat "," (List.map string_of_formula l) ^ ")"
  | `Negation f -> "not(" ^ string_of_formula f ^ ")"
  | `Exists (l, f) ->
      "exists([" ^ String.concat "," (List.map (fun (s, _) -> "var__" ^ s) l) ^ "]," ^ string_of_formula f ^ ")"
  | `Forall (l, f) ->
      "forall([" ^ String.concat "," (List.map (fun (s, _) -> "var__" ^ s) l) ^ "]," ^ string_of_formula f ^ ")"


let string_of_resultat res =
  let nom = match res.res_theoremes with
    | [] -> "untitled"
    | (n, _)::_ -> n
  in
  let en = List.fold_left enum_formule enum_vide res.res_axiomes in
  "begin_problem(" ^ nom ^ ").\n" ^
    "list_of_descriptions.\n" ^
    "name( {*" ^ nom ^ " *} ).\n" ^
    "author( {* Alloy to SPASS *} ).\n" ^
    "status(unknown).\n" ^
    "description( {* This SPASS theory has been automatically generated from an Alloy specification. *} ).\n" ^
    "end_of_list.\n" ^
    "list_of_symbols.\n" ^
    begin if en.enum_fonctions <> [] then
      "functions[" ^ String.concat "," en.enum_fonctions ^ "].\n"
    else "" end ^
    begin if en.enum_predicats <> [] then
      "predicates[" ^ String.concat "," en.enum_predicats ^ "].\n"
    else "" end ^
    "end_of_list.\n" ^
    "list_of_formulae(axioms).\n" ^
    List.fold_left (fun s f -> s ^ "formula(" ^ string_of_formula f ^ ").\n") "" res.res_axiomes ^
    "end_of_list.\n" ^
    "list_of_formulae(conjectures).\n" ^
    List.fold_left (fun s (n, f) -> s ^ "formula(" ^ string_of_formula f ^ "," ^ n ^ ").\n") "" res.res_theoremes ^
    "end_of_list.\n" ^
    "end_problem.\n"

let process_result res =
   let hyp = 
    let en = List.fold_left enum_formule enum_vide res.res_axiomes in
      "author( {* Alloy to SPASS *} ).\n" ^
      "status(unknown).\n" ^
      "description( {* This SPASS theory has been automatically generated from an Alloy specification. *} ).\n" ^
      "end_of_list.\n" ^
      "list_of_symbols.\n" ^
      begin if en.enum_fonctions <> [] then
        "functions[" ^ String.concat "," en.enum_fonctions ^ "].\n"
      else "" end ^
      begin if en.enum_predicats <> [] then
        "predicates[" ^ String.concat "," en.enum_predicats ^ "].\n"
      else "" end ^
      "end_of_list.\n" ^
      "list_of_formulae(axioms).\n" ^
      List.fold_left (fun s f -> s ^ "formula(" ^ string_of_formula f ^ ").\n") "" res.res_axiomes ^
      "end_of_list.\n" ^
      "list_of_formulae(conjectures).\n"
  in
   List.iter (fun (nom, f) -> begin
     let ch = open_out (nom ^ ".spass") in
     output_string ch (
       "begin_problem(" ^ nom ^ ").\n" ^
         "list_of_descriptions.\n" ^
         "name( {*" ^ nom ^ " *} ).\n" ^
         hyp ^
         "formula(" ^ string_of_formula f ^ "," ^ nom ^ ").\n" ^
         "end_of_list.\n" ^
         "list_of_settings(SPASS).\n" ^
         "{*\n" ^
         "\n" ^
         "set_flag(DocProof,1).\n" ^
         "set_flag(FPDFGProof,1).\n" ^
         "*}\n" ^
         "end_of_list.\n" ^
         "end_problem.\n"
     );
     close_out ch;
   end
   ) res.res_theoremes