module classicjava_free.
  accumulate classicjava_syntax.
  import q2.

  local free_list (list expression) -> (list string) -> o.

  %% ``free E Ns'' succeeds if the list of free variables in E is Ns.
  free (var N) (N::nil).
  free (mcall E0 MN (Es)) Ns :-
       free E0 E0Ns, free_list Es EsNs, join E0Ns EsNs Ns.
  free (dot E0 F) Ns :- free E0 Ns.
  free (fassign E0 F E1) Ns :- free E0 N0s, free E1 N1s, join N0s N1s Ns.
  free (cast T E) Ns :- free E Ns.
  free (semi E1 E2) Ns :- free_list (E1::E2::nil) Ns.
  free _ nil.

  free_list nil nil.
  free_list (E1::Es) L :-
       free E1 L1, free_list Es EsNs, join L1 EsNs L.
end