(** 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 prover_type = E | Vampire


(** input formats of supported provers *)
let input_format = function 
  | Vampire | E -> "tptp"

let replace_dot_with_uscore =
  Str.global_replace (Str.regexp_string ".") "_"

let tptp_var_ident s = 
  String.capitalize (replace_dot_with_uscore s)


let tptp_const_ident s =
  String.uncapitalize (replace_dot_with_uscore 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 = function
  | E | Vampire -> "fof"

let rec split_form : fol_formula -> fol_formula list = function
  | `Conjunction fs -> List.concat (ListLabels.map ~f:split_form fs)
  | `Forall (v, `Conjunction fs) -> split_form (`Conjunction (ListLabels.map ~f:(fun f ->  `Forall (v, f)) fs))
  | `Forall (v, `Forall (v', f)) -> split_form (`Forall (v@v', f))
  | f -> [f]

(** (FOL) form -> string *)
let tptp_pretty_print (tptp_var : prover_type) (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 : prover_type -> boool -> string = function
    | Vampire -> (function
		    | `True -> "true"
		    | `False -> "false"
		    | `BoolVar v -> tptp_const_ident v
		    | `NegatedBoolVar v -> "~" ^ tptp_const_ident v
		 )
   
    | E ->  (function
	       | `True -> "$true"
	       | `False -> "$false"
	       | `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) -> (match tptp_var with 
			       | _ -> 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 tptp_var b
    | #fol_atom as a -> print_atom a
    | `Conjunction fs -> p (String.concat " & " (ListLabels.map ~f:foo fs)) 
    | `Disjunction fs -> p (String.concat " | " (ListLabels.map ~f:foo fs)) 
    | `Negation f ->  (match tptp_var with  	  
    			 | Vampire -> p ( foo f ^ " => false" )
			 | _ -> "~" ^ p (foo f)
		      )

  in
    foo f
 

let tptp_pretty_print_sequent (tptp_var : prover_type) (hyps : fol_formula list) (new_goal : fol_formula) =
  let goal_string = sprintf "%s(goal, conjecture, %s)." (fof_formula tptp_var) (tptp_pretty_print tptp_var new_goal)
  in 
  let hyps_string = 
    String.concat "\n\n\n" 
      (List.map 
	 (fun new_f -> sprintf "%s(%s, hypothesis, %s)." (fof_formula tptp_var) (fresh_lowercase_ident "hyp") (tptp_pretty_print tptp_var new_f))
	 hyps
      ) 
  in
    hyps_string ^ "\n\n\n\n" ^ goal_string

let total_proof_obligations = ref 0
let successfull_proof_obligations = ref 0


let interpret_result (chn : in_channel) : prover_type -> bool = function
  | Vampire ->
      (let result = input_line chn in
	match String.sub result 0 16 with
	  | "Satisfiabi" -> false
	  | "Refutation found" -> true
	  | "Refutation not f" -> false
	  | _ ->  (printf "Hey ! The prover failed while saying : %s\n" result); false
      )  
  | E -> (try
	    let line1 = input_line chn in
	    let result = input_line chn in
	      match (try String.sub result 0 14 with Invalid_argument _ -> "") with
		| "# Proof found!" -> true
		| "# No proof fou" -> false
		| _ -> (printf "Hey ! The prover failed while saying : %s\n" line1); false
	  with
	    | _ -> failwith "something went wrong..."
      )


	
let invocation_string (p:prover_type) : string = 
    match p with
      | Vampire -> "vampire8 "
      | E -> "eprover --tptp3-in -s -xAuto -tAuto --print-statistics "


let mkeq ~p l r = match p with
     | E 
     | Vampire -> sprintf "(%s=%s)" l r

let convert_input (prover : prover_type) (tptp_in_file : string) : string =
  let in_format = input_format prover in
  if in_format = "tptp" then tptp_in_file else failwith "convert_input: unimplemented"

(** {6 title} [decide_sq toto tutu titi] ca fait blabla *)

let decide_sq  (result : Fol.resultat) (thname : Fol.ident) ~(prover : prover_type) : bool =

  let vc_tptp_in = (sprintf "vc.tptp.%d.in" !total_proof_obligations) in
  let vc_out = (sprintf "vc.tptp.%d.out" !total_proof_obligations) in 

  let hyps = result.res_axiomes
  and subgoal = List.assoc thname result.res_theoremes
  in
 
  incr total_proof_obligations ; 
  let chn = open_out vc_tptp_in in
  output_string chn (tptp_pretty_print_sequent prover hyps subgoal);
  
  close_out chn; 
  flush_all ();
  
  let now = Unix.gettimeofday () in
  
  let vc_in = convert_input prover vc_tptp_in in
  let redirection = 
    " &> " ^ vc_out in
  ignore (Sys.command (invocation_string prover ^ " " ^ vc_in ^ redirection)) ;
  let delta =  Unix.gettimeofday () -. now in
  if delta > 1.0 then (printf "\nthe Prover has run for %f seconds\n" delta);
  let chn = open_in vc_out in
  let res = interpret_result chn prover in
  close_in chn;
  res

      
    (* the ACTUAL main code is here *)