% $Id$
% Added indirect locations as an in-class exercise.
module while_indirect.

  accumulate while.

  %% Auxilliary semantic relations

  %% ``access0 S L V'' succeeds if the last value stored in S at,
  %% location L was V, and otherwise if there was no value stored at L,
  %% returns 0.
  local access0      (store int) -> int -> int -> o.
  access0 S L SV :- access S L SV, !.
  access0 S L 0.

  %% [assign-indirect]
      (meaningE EL S L S')
 => % ------------------------------------------------------------------
      (reducesC (configC (assign (indirect EL) E) S)
                (configC (assign (loc L) E) S')).

  %% [deref-indirect-loc]
      (access0 S L V)
 => % -----------------------------------------------
      (reducesE (configE (deref (indirect (num L))) S)
                (configE (num V) S)).

  %% [deref-indirect]
      (reducesE (configE EL S) (configE EL' S'))
 => % -----------------------------------------------
      (reducesE (configE (deref (indirect EL)) S)
                (configE (deref (indirect EL')) S')).