module classicjava_aux2.
  accumulate classicjava_aux.

  %% ``substFor As Fs E1 E2'' succeeds if E2 is the result of substituting
  %% each actual expression in A for the corresponding formal in Fs,
  %% throughout E1, yielding E2.
  substFor nil nil E E.
  substFor (A::As) (F::Fs) E E' :-
     subst A F E E'',
     substFor As Fs E'' E'.

  local subst expression -> expression -> expression -> expression -> o.

  subst A F F A.
  subst A F (mcall E0 MN (Es)) (mcall E0' MN (Es')) :-
       subst A F E0 E0', substForAll A F Es Es'.
  subst A F (dot E0 FN) (dot E0' FN) :-
       subst A F E0 E0'.
  subst A F (fassign E0 FN E1) (fassign E0' FN E1') :-
       subst A F E0 E0', subst A F E1 E1'.
  subst A F (cast TE E) (cast TE E') :-
       subst A F E E'.
  subst A F (semi E1 E2) (semi E1' E2') :-
       subst A F E1 E1', subst A F E2 E2'.
  subst A F E E.

  local substForAll expression -> expression 
        -> (list expression) -> (list expression) -> o.

  substForAll A F nil nil.
  substForAll A F (E1::E1s) (E2::E2s) :-
     subst A F E1 E2,
     substForAll A F E1s E2s.


  methodBody CT C MN T Fs Body :-
     methodBodySearch CT CT C MN T Fs Body.

  local methodBodySearch (list declaration) -> (list declaration)
        -> string -> string 
        -> typeexpression -> (list formaldecl) -> expression -> o.
  methodBodySearch CT ((class C _ _ Ms)::CLs) C MN T Fs Body :-
     methodFromList Ms MN T Fs Body, !.
  methodBodySearch CT (_::CLs) C MN T Fs Body :-
     methodBodySearch CT CLs C MN T Fs Body.
  methodBodySearch CT nil C MN T Fs Body :-
     direct_subclass CT C Super,
     methodBodySearch CT CT Super MN T Fs Body.

  local methodFromList (list methoddecl) -> string
                    -> typeexpression -> (list formaldecl) -> expression -> o.
  methodFromList ((meth T MN (Fs) Body)::Meths) MN T Fs Body :-
     !.
  methodFromList (_::Meths) MN T Fs Body :-
     methodFromList Meths MN T Fs Body.

end