Natural_deduction : FML_main.string_of

let rec string_of_fml_rec (embedded: bool) (fml : t_fml) : string =
        match fml with
        | PredApp (p, term_list) -> (
                match is_infix_pred p, term_list with
                |true, [a;b] -> String.concat "" [string_of_term a;" ";string_of_pred p;" ";string_of_term b]
                |false,[] -> string_of_pred p
                |_, _ -> String.concat "" [string_of_pred p;string_of_term_list term_list]
        )
        | BinopApp (binop, fml1, fml2) -> (
                match embedded with
                |true -> String.concat "" ["("; string_of_fml_rec true fml1; " "; string_of_binop binop;" "; string_of_fml_rec true fml2;")"]
                |false -> String.concat "" [string_of_fml_rec true fml1; " "; string_of_binop binop; " "; string_of_fml_rec true fml2]
        )
        | UnopApp (unop, fml) -> String.concat "" [string_of_unop unop; string_of_fml_rec true fml]
        | QuantApp (quant, var,fml) -> String.concat "" [string_of_quant quant; string_of_var var; " "; string_of_fml_rec true fml]

and string_of_binop (binop : t_binop) : string =
        match binop with 
        |Binop s -> s

and string_of_unop (unop : t_unop) : string =
        match unop with 
        |Unop s -> s

and string_of_quant (quant : t_quant) : string =
        match quant with 
        |Quant s -> s

and string_of_pred (p : t_pred) : string =
        match p with
        |Pred s -> s

and string_of_var (var : t_var) : string =
        match var with
        |Var v -> v

and string_of_term_list (term_list : t_term list) : string =
        String.concat "" ["(";String.concat "," (List.map string_of_term term_list);")"]

and string_of_term_rec (embedded : bool) (term : t_term) : string =
        match term with
        | Atom var -> string_of_var var
        | FuncApp (Func f, term_list) ->
                match is_infix_func f, term_list with
                |true, [a;b] -> (
                        match embedded with
                        |true -> String.concat "" ["(";string_of_term_rec true a;" ";f;" ";string_of_term_rec true b;")"]
                        |false -> String.concat "" [string_of_term_rec true a;" ";f;" ";string_of_term_rec true b]
                )
                |false, [] -> f
                |false, [a] -> (
                        match is_postfix_func f with
                        |true -> String.concat "" [string_of_term_rec true a;f]
                        |false -> String.concat "" [f;"(";string_of_term a;")"]
                )
                |_, _ -> String.concat "" [f;string_of_term_list term_list]

and is_infix_pred (p : t_pred) : bool =
        match string_of_pred p with
        |"=" | "<" | ">" |"≤" | "\\leq" | "≥" | "\\geq" 
        | "∈" | "\\in" | "⊂" | "\\subset" | "⊆" | "\\subseteq" -> true
        |_ -> false

and is_infix_func (f : string) : bool =
        match f with
        |"+"|"×"|"*"|"-"|"^"|"·" -> true
        |_ -> false

and is_postfix_func (f : string) : bool =
        match f with
        |"\'" | "⁰" | "¹" | "²" | "³" | "⁴" | "⁵" | "⁶" | "⁷" | "⁸" | "⁹" -> true
        |_ -> false

and string_of_fml (fml : t_fml) : string =
        string_of_fml_rec false fml

and string_of_term (term : t_term) : string =
        string_of_term_rec false term