module classicjava.

  accumulate classicjava_aux2, classicjava_added_syntax, store, domains.
  import list_utils.

  %% Programs

  %% ``meaning Prog Val Store'' succeeds if Val and Store are
  %% the final value and store that result from evaluating Prog
  %% in the initial store. 
  meaning (prog Decls Body) Val Store :-
    inputP (prog Decls Body) Config,
    rtc (reduces Decls) Config Config',
    outputP Config' Val Store.

  %% ``inputP C Config'' succeeds if Config is the configuration that
  %% contains C and the initial store.
  inputP (prog Decls Body) (config Body S0) :-
      initial_store S0.

  %% ``outputP Config S'' succeeds if Config is terminal and contains store S.
  outputP (config (loc L) S) (ref L) S.
  outputP (config null S)    nullref S.

  %% ``newObjectValueFor CT C O'' succeeds if O is an initial object value,
  %% with all null fields, for an object of class C (determined by CT).
  local newObjectValueFor (list declaration) -> string -> storable -> o.
  newObjectValueFor CT C (object C FMap) :-
    fieldsof CT C Fs, nullForAll Fs FMap.

  %% ``nullForAll Fs FMap'' succeeds if FMap is a finite function
  %% that maps each element of Fs to nullref.
  local nullForAll (list fielddecl) -> (finite_fun string value) -> o.
  nullForAll nil empty_f_fun.
  nullForAll (field T F::Fs) (f_fun_extend F nullref FMap) :- 
    nullForAll Fs FMap.

  %% Expressions

  %% ``meaningE CT E S V S2'' succeeds if,
  %% with the list of declarations CT,
  %% evaluating expression E in store S,
  %% produces the value V and final store S2.
  meaningE CT E S V S' :-
    rtc (reduces CT) (config E S) (config E' S'),
    outputE (config E' S') V S'.

  %% ``outputE ConfigE V'' succeeds if V is the final value of
  %% the expression configuration ConfigE.
  outputE (config (loc L) S) (ref L) S.
  outputE (config null S)    nullref S.

  %% ``value2exp V E'' succeeds if the value V is equivalent to expression E.
  local value2exp value -> expression -> o.
  value2exp (ref L) (loc L).
  value2exp nullref null.

  %% ``isTerminal E'' succeeds if the expression E is terminal.
  local isTerminal expression -> o.
  isTerminal (loc _).
  isTerminal null.

  %% ``allTerminal Es'' succeeds if each expression in Es is terminal.
  local allTerminal (list expression) -> o.
  allTerminal nil.
  allTerminal (E::Es) :- isTerminal E, allTerminal Es.

  %% ``varsFor Formals Es'' succeeds if each (formal TE N) in Formals
  %% corresponds to (var N) in the same position in Es
  local varsFor (list formaldecl) -> (list expression) -> o.
  varsFor nil nil.
  varsFor (formal _ N::Fs) ((var N)::Es) :- varsFor Fs Es.

  %% ``reduces CT Config1 Config2'' succeeds if there is a one step
  %% (expression) reduction from configuration Config1,
  %% which results in Config2.

  %% [new]
      ((newObjectValueFor CT C O), (alloc O S L S'))
 => % -----------------------------------------------
      (reduces CT (config (new C) S) (config (loc L) S')).

  %% var expressions are substituted out (they would be terminal/errors)

  %% null and loc are terminal

  %% [method-call]
       ((allTerminal Vs),
        (access S L0 (object C FMap)),
        (methodBody CT C M _ Formals Body),
        (varsFor Formals FormalNames),
        (substFor ((loc L0)::Vs) (this::FormalNames)
                 Body Body'))
  => % ----------------------------------------------------
       (reduces CT (config (mcall (loc L0) M Vs) S)
                   (config Body' S)).

  %% [method-reduce-target]
       (reduces CT (config E0 S) (config E0' S'))
  => % ----------------------------------------------------
       (reduces CT (config (mcall E0 M (Es)) S)
                   (config (mcall E0' M (Es)) S')).

  %% [method-reduce-arguments]
       ((append Vs (A::As) Es),
        (allTerminal Vs),
        (reduces CT (config A S) (config A' S')),
        (append Vs (A'::As) Es'))
  => % ----------------------------------------------------
       (reduces CT (config (mcall (loc L0) M (Es)) S)
                   (config (mcall (loc L0) M (Es')) S')).

  %% [dot]
       ((access S L (object C FMap)),
        (f_fun_apply FMap F V),
        (value2exp V E))
  => % ----------------------------------------------------
       (reduces CT (config (dot (loc L) F) S)
                   (config E S)).

  %% [dot-reduce-target]
       (reduces CT (config E S) (config E' S'))
  => % ----------------------------------------------------
       (reduces CT (config (dot E F) S)
                   (config (dot E' F) S')).

  %% [fassign]
       ((isTerminal VE),
        (access S L0 (object C FMap)),
        (value2exp V1 VE),
        (update S L0 (object C (f_fun_extend F V1 FMap)) S'))
  => % ----------------------------------------------------
       (reduces CT (config (fassign (loc L0) F VE) S)
                   (config VE S')).

  %% [fassign-reduce-target]
       (reduces CT (config E0 S) (config E0' S'))
  => % ----------------------------------------------------
       (reduces CT (config (fassign E0 F E1) S)
                   (config (fassign E0' F E1) S')).

  %% [fassign-reduce-rhs]
       (reduces CT (config E1 S) (config E1' S'))
  => % ----------------------------------------------------
       (reduces CT (config (fassign (loc L0) F E1) S)
                   (config (fassign (loc L0) F E1') S')).

  %% [cast]
       ((access S L (object C FMap)),
        (subtypeof CT C T))
  => % ----------------------------------------------------
       (reduces CT (config (cast (cn T) (loc L)) S)
                   (config (loc L) S)).

  %% [ncast]
       (reduces CT (config (cast TE null) S)
                   (config null S)).

  %% [cast-reduce]
       (reduces CT (config E S) (config E' S'))
  => % ----------------------------------------------------
       (reduces CT (config (cast TE E) S)
                   (config (cast TE E') S')).

  %% [semi-reduce-left]
       (reduces CT (config E1 S) (config E1' S'))
  => % ----------------------------------------------------
       (reduces CT (config (semi E1 E2) S)
                   (config (semi E1' E2) S')).

  %% [semi-done-left]
       (isTerminal E1)
  => % ----------------------------------------------------
       (reduces CT (config (semi E1 E2) S)
                   (config E2 S)).
end