open Fol

let rec string_of_basesort = function
  | `I -> "`I"
  | `O -> "`O"
  | `F -> "`F"
  | `B -> "`B"
  | `Unknown -> "`Unknown"


let string_of_ident : ident -> string = fun x -> "\"" ^ x ^ "\""


let rec string_of_term : term -> string = fun (b, t) ->"(" ^ string_of_basesort b ^ ", " ^ begin match t with
  | `Int i -> "(`Int " ^ string_of_int i ^ ")"
  | `Constant i -> "(`Constant " ^ string_of_ident i ^ ")"
  | `Variable i -> "(`Variable " ^ string_of_ident i ^ ")"
  | `Function (f, l) -> List.fold_left (fun x y -> x ^ y ^ "; ") ("(`Function (" ^ string_of_ident f ^ ", [") (List.map string_of_term l) ^ "]))"
end ^ ")"


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

  | `Negation f -> "(`Negation " ^ string_of_fol_formula_generic f ^ ")"
  | `Conjunction (l) -> List.fold_left (fun x y -> x ^ y ^ ";\n") ("(`Conjunction [\n") (List.map string_of_fol_formula_generic l) ^ "])"
  | `Disjunction (l) -> List.fold_left (fun x y -> x ^ y ^ ";\n") ("(`Disjunction [\n") (List.map string_of_fol_formula_generic l) ^ "])"
  | `Exists (l, f) ->
      List.fold_left (fun x (y, b) -> x ^ "(" ^ string_of_ident y ^ ", " ^ string_of_basesort b ^ ")" ^ ";") "(`Exists ([" l ^ "], " ^ string_of_fol_formula_generic f ^ "))"
  | `Forall (l, f) ->
      List.fold_left (fun x (y, b) -> x ^ "(" ^ string_of_ident y ^ ", " ^ string_of_basesort b ^ ")" ^ ";") "(`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 ^ string_of_fol_formula y ^ ";\n") "{res_axiomes = [" r.res_axiomes
  ^ List.fold_left (fun x (y, z) -> x ^ "(" ^ string_of_ident y ^ "," ^ string_of_fol_formula z ^ ");\n") "];\n\nres_theoremes = [" r.res_theoremes ^ "]}"