module classicjava_aux.
  accumulate classicjava_syntax, q2, rtc.

  local fielddecls (list fielddecl) -> (list fielddecl) -> o.
  local fieldsof_helper (list declaration)
                        -> (list declaration) -> string -> (list fielddecl) -> o.

  %% "direct_subclass CT Sub Sup" succeeds if in the class table CT,
  %% Sub is a direct subclass of Sup.
  direct_subclass ((class Sub Sup _ _)::Cs) Sub Sup :- !.
  direct_subclass (_::Cs) Sub Sup :- direct_subclass Cs Sub Sup.

  %% "subtypeof CT Sub Sup" succeeds if in the class table CT,
  %% Sub is either Sup or a direct or indirect subclass of Sup.
  subtypeof CT Sub Sup :- rtc (direct_subclass CT) Sub Sup.

  %% "fieldsof CT C Fs" succeeds if C has the fielddecls Fs in CT.
  fieldsof CT "Object" nil.
  fieldsof CT C L :- fieldsof_helper CT CT C L.

  %% fieldsof_helper is used so that subtypeof
  %% can get the entire class table to work with.
  fieldsof_helper _ nil _ nil.
  fieldsof_helper CT ((class C0 _ F0s _)::CLASSES) C L :-
     subtypeof CT C C0, !,
     fielddecls F0s L0,
     fieldsof_helper CT CLASSES C Ls,
     join L0 Ls L.
  fieldsof_helper CT ((class C0 _ F0s _)::CLASSES) C L :-
     fieldsof_helper CT CLASSES C L.

  %% "fielddecls Ds Fs" succeeds if Fs is the list of field decls from Ds.
  fielddecls nil nil.
  fielddecls (F::FDs) (F::Fs) :- fielddecls FDs Fs.
end