module aux2_tests.
  accumulate test_helpers, classicjava_aux2, classicjava_added_syntax, 
             classicjava_testct.

  local substFor_test int
            -> (list expression) -> (list expression)
            -> expression -> expression -> o.
  local methodBody_test int
                -> string -> string 
                -> typeexpression -> (list formaldecl) -> expression -> o.

  %% adapters from test_helpers.
  check_exists 1 J :- substFor_test J _ _ _ _.
  check_exists 2 J :- methodBody_test J _ _ _ _ _.
  check 1 J :- substFor_test J As Fs E E', substFor As Fs E E'.
  check 2 J :- methodBody_test J C MN T Fs Body,
               example CT, methodBody CT C MN T Fs Body.

  % substFor examples
  substFor_test 1 ((loc 1)::(loc 2)::nil) ((var "x")::(var "y")::nil)
                  (fassign (var "x") "f" (var "y"))
                  (fassign (loc 1) "f" (loc 2)).
  substFor_test 2 ((loc 1)::(loc 2)::nil) (this::(var "o")::nil)
                  (mcall (dot this "elems") "add" ((var "o")::nil))
                  (mcall (dot (loc 1) "elems") "add" ((loc 2)::nil)).
  substFor_test 3 ((loc 1)::(loc 2)::nil) (this::(var "o")::nil)
                  (semi null
                   (cast (cn "Object")
                    (mcall (dot this "elems") "add" ((var "o")::nil))))
                  (semi null
                   (cast (cn "Object")
                    (mcall (dot (loc 1) "elems") "add" ((loc 2)::nil)))).


  methodBody_test 1 "Stack" "push"
                (cn "Stack")
                ((formal (cn "Object") "o")::nil) 
                (semi
                  (fassign this "elems" 
                     (mcall 
                        (mcall (new "Cons") "setHead" ((var "o")::nil))
                        "setTail" ((dot this "elems")::nil)))
                  this).
  methodBody_test 2 "ColoredStack" "push"
                (cn "Stack")
                ((formal (cn "Object") "o")::nil) 
                (semi
                  (fassign this "elems" 
                     (mcall 
                        (mcall (new "Cons") "setHead" ((var "o")::nil))
                        "setTail" ((dot this "elems")::nil)))
                  this).
  methodBody_test 3 "ColoredStack" "pop"
                (cn "Stack")
                nil
                (semi
                  (fassign this "elems" 
                     (mcall (dot this "elems") "tail" nil))
                  this).
   methodBody_test 4 "ColoredStack" "setColor"
                 (cn "ColoredStack")
                 ((formal (cn "Color") "nv")::nil)
                 (semi (fassign this "color" (var "nv"))
                      this).
end