let gcd a b =
let rec gcdloop ((pl, ql, gcd) as acc) (al, bl) =
match al, bl with
| [], [] ->
acc
| [], bl ->
(bl @ pl , ql, gcd)
| al, [] ->
(pl, al @ ql, gcd)
| a :: al', b :: bl' ->
let (x, n) = destruct a
and (y, m) = destruct b in
let res = Term.cmp x y in
if res = 0 then
let acc' =
if n = m then
(pl, ql, mk_expt n x :: gcd)
else if n < m then
(mk_expt (m - n) x :: pl, ql, mk_expt n x :: gcd)
else
(pl, mk_expt (n - m) x :: ql, mk_expt m x :: gcd)
in
gcdloop acc' (al', bl')
else if res > 0 then
let x_pow_n = mk_expt n x in
gcdloop (x_pow_n :: pl, ql, x_pow_n :: gcd) (al', bl)
else
let y_pow_m = mk_expt m y in
gcdloop (y_pow_m :: pl, ql, y_pow_m :: gcd) (al, bl')
in
let (pl, ql, gcd) = gcdloop ([], [], []) (to_list a, to_list b) in
(mk_multl pl, mk_multl ql, mk_multl gcd)