(* Translation between infix expressions and reverse Polish notation (RPN) w/o using rewrite.

Sample inputs:
  '0
  ('0.('1.'0))
  (('0.('1.('0.('1.'0)))).('1.('0.('1.('0.('1.'0))))))
*)

proc MAIN(X)
  Y <= call POST(X);
  return Y;

proc POST(T)                   (* iter.postorder traversal *)
 S <= (T.nil);                 (* init stack s to tree t   *)
 from =? Y nil loop            (* list y empty at entry?   *)
  if =? (hd S) '0 then         (* stack top is leaf *)
   ('0.S) <= S;
   Y <= ('0.Y);
  else                         (* stack top is inner node  *)
   ((L.('1.R)).S) <= S;
   S <= (R.(L.S));
   Y <= ('1.Y);
  fi =? (hd Y) '0;
 until (=? S nil);             (* stack s empty at exit?   *)
return Y