let rec compare_terms x y =
if term_equal x y then
0
else
match x, y with
(* var first *)
| Var u, Var v ->
Var.compare u v
| Var _, _ ->
-1
| _, Var _ ->
1
(* const second *)
| Const a, Const b ->
Symbol.compare a b
| Const _, _ ->
-1
| _, Const _ ->
1
(* function term last *)
| Func func1, Func func2 ->
let cmp =
Symbol.compare func1.symbol func2.symbol
in
if cmp <> 0 then
cmp
else
let rec compare_terms' index =
if index >= Array.length func1.subterms then
0
else
let cmp' =
compare_terms func1.subterms.(index) func2.subterms.(index)
in
if cmp' <> 0 then
cmp'
else
compare_terms' (index + 1)
in
compare_terms' 0