% $Id: while.mod,v 1.5 2004/10/18 03:37:42 leavens Exp leavens $
module while.

  accumulate while_syntax, store, rtc.
  import debug_write.

  %% 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.

  %% ``ap O N1 N2 Ans'' succeeds if Ans is the result
  %% of evaluating the mathematical expression N1 O N2.
  local ap operator -> int -> int -> int -> o.

  (ap add N1 N2 Ans) :- Ans is N1 + N2.
  (ap sub N1 N2 Ans) :- Ans is N1 - N2.
  (ap mult N1 N2 Ans) :- Ans is N1 * N2.


  %% Programs

  %% ``meaningC Prog Store'' succeeds if Store is the final store that results
  %% from evaluating Prog in the initial store.
  meaningC Prog Store :-
    inputC Prog Config,
    rtc reducesC Config Config',
    outputC Config' Store.

  %% ``inputC C Config'' succeeds if Config is the configuration that
  %% contains C and the intial store.
  inputC C (configC C S0) :-
      initial_store S0.

  %% ``outputC Config S'' succeeds if Config is terminal and contains store S.
  outputC (configC skip S) S.

  %% Commands

  %% ``reducesC Config1 Config2'' succeeds if there is a one step
  %% command reduction from configuration Config1 which results in Config2.

  %% [exp-cmd]
      (meaningE E S V S')
 => % ------------------------------------------------------
      (reducesC (configC (exp E) S) (configC skip S')).

  %% skip configurations are terminal

  %% [assign]
      ((meaningE E S V S'), (update S' I V S''))
 => % ------------------------------------------------------------------
      (reducesC (configC (assign (loc I) E) S) (configC skip S'')).

  %% [semi1]
      (reducesC (configC C1 S) (configC C1' S'))
 => % -------------------------------------------------------------------
      (reducesC (configC (semi C1 C2) S) (configC (semi C1' C2) S')).

  %% [semi2]
      (reducesC (configC (semi skip C2) S) (configC C2 S)).

  %% [if-false]
      (meaningE E S 0 S')
 => % ----------------------------------------------------------
      (reducesC (configC (if E C1 C2) S) (configC C2 S')).

  %% [if-true]
      ((meaningE E S V S'), not(V = 0))
 => % ---------------------------------------------------------
      (reducesC (configC (if E C1 C2) S) (configC C1 S')).

  %% [while-false]
      (meaningE E S 0 S')
 => % -----------------------------------------------------------
      (reducesC (configC (while E C) S) (configC skip S')).

  %% [while-true]
      ((meaningE E S V S'), not(V = 0))
 => % -----------------------------------------------------------
      (reducesC (configC (while E C) S)
                (configC (semi C (while E C)) S')).

  %% Expressions

  %% ``meaningE E S V S2'' succeeds if V is the value and S2 the final store
  %% that results from evaluating expression E in store S.
  meaningE E S V S' :-
    rtc reducesE (configE E S) (configE E' S'),
    outputE (configE E' S') V.

  %% ``outputE ConfigE V'' succeeds if V is the final value of
  %% the expression configuration ConfigE.
  outputE (configE (num I) S) I.

  %% ``reducesE ConfigE1 ConfigE2'' succeeds if there is a one step
  %% expression reduction from configuration ConfigE1,
  %% which results in ConfigE2.

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

  %% num is terminal

  %% [op-apply]
       (ap Oper V1 V2 N)
  => % ----------------------------------------------------
       (reducesE (configE (op Oper (num V1) (num V2)) S)
                 (configE (num N) S)).

  %% [op-left]
       (reducesE (configE E1 S) (configE E1' S'))
  => % --------------------------------------------------
       (reducesE (configE (op Oper E1 E2) S)
                 (configE (op Oper E1' E2) S')).
  
  %% [op-right]
       (reducesE (configE E2 S) (configE E2' S'))
  => % --------------------------------------------------
       (reducesE (configE (op Oper (num V1) E2) S)
                 (configE (op Oper (num V1) E2') S')).