open Fol

let string_of_ident : ident -> string = fun x -> x

let rec string_of_term : term -> string = fun (_, t) -> match t with
  | `Int i -> string_of_int i
  | `Constant i | `Variable i -> i
  | `Function (f, l) -> List.fold_left (fun x y -> x ^ " " ^ y) ("(" ^ f) (List.map string_of_term l) ^ ")"

let rec string_of_fol_formula_generic = function 
  | `True -> "True"
  | `False -> "False"
  | `BoolVar i -> i
  | `NegatedBoolVar i -> "(" ^ i ^ " -> False)"
  | `Predicate (f, l) -> "(" ^ f ^ List.fold_left (fun x y -> x ^ " " ^ y ^ " ") "" (List.map string_of_term l) ^ ")"
  | `Equality (a, b) -> "(" ^ string_of_term a ^ " = " ^ string_of_term b ^ ")"

  | `Negation f -> "(" ^ string_of_fol_formula_generic f ^ " -> False)"
  | `Conjunction [] -> "True"
  | `Disjunction [] -> "False"
  | `Conjunction (a::l) -> List.fold_left (fun x y -> x ^ " /\\ " ^ y) ("(" ^ string_of_fol_formula_generic a) (List.map string_of_fol_formula_generic l) ^ ")"
  | `Disjunction (a::l) -> List.fold_left (fun x y -> x ^ " \\/ " ^ y) ("(" ^ string_of_fol_formula_generic a) (List.map string_of_fol_formula_generic l) ^ ")"
  | `Exists (l, f) ->
      List.fold_left (fun x (y, _) -> x ^ " " ^ y) "(exists" l ^ ", " ^ string_of_fol_formula_generic f ^ ")"
  | `Forall (l, f) ->
      List.fold_left (fun x (y, _) -> x ^ " " ^ y) "(forall" l ^ ", " ^ string_of_fol_formula_generic f ^ ")"

let string_of_fol_formula : fol_formula -> string = string_of_fol_formula_generic
let string_of_boool : boool -> string = string_of_fol_formula_generic
let string_of_fol_atom : fol_atom -> string = string_of_fol_formula_generic

let string_of_resultat (r: resultat) : string =
  List.fold_left (fun x y -> x ^ " /\\ \n" ^ string_of_fol_formula y) "Axiom ax : True " r.res_axiomes 
  ^ List.fold_left (fun x (y, z) -> x ^ "Definition " ^ y ^ " :=" ^ string_of_fol_formula z ^ ".\n") ".\n\n" r.res_theoremes