let rec term_to_string ?(pretty:bool = true) (term: term) : string =
match term with
| Var var ->
Var.to_string var
| Const const ->
if Symbol.is_fd_element const then
"'" ^ Symbol.to_string ~pretty:pretty const
else
Symbol.to_string ~pretty:pretty const
| Func func when Array.length func.subterms = 0 ->
let const = func.symbol in
if Symbol.is_fd_element const then
"'" ^ Symbol.to_string ~pretty:pretty const
else
Symbol.to_string ~pretty:pretty const
| Func func ->
if pretty && Symbol.equal Symbol.equality func.symbol then begin
"(" ^ term_to_string ~pretty:pretty func.subterms.(0)
^ " = "
^ term_to_string ~pretty:pretty func.subterms.(1) ^ ")"
end
else if pretty
&&
Symbol.is_fd_relation func.symbol
then begin
let constant, subterms =
match Array.to_list func.subterms with
| []
| _ :: [] ->
failwith ("Term.term_to_string: fd relation of arity < 2: " ^ Symbol.to_string func.symbol);
| head :: tail ->
head, tail
in
let index =
if is_term_var constant then
"r_" ^ string_of_int (Symbol.arity func.symbol - 1)
else
"r_" ^ Symbol.to_string ~pretty:pretty (top_symbol_term constant)
in
index
^ "("
^ String.concat ", " (List.map (term_to_string ~pretty:pretty) subterms)
^ ")"
end
else begin
Symbol.to_string ~pretty:pretty func.symbol
^ "("
^ String.concat ", " (List.map (term_to_string ~pretty:pretty) (Array.to_list func.subterms))
^ ")"
end