module counter.
import forumlog.

kind tm     type.
type abs    (tm -> tm) -> tm.
type app    tm -> tm -> tm.

type eval   tm -> tm -> o -> o.

cl (eval (abs M) (abs M) K o- K).
cl (eval (app M N) V K o- eval M (abs R) (eval N U (eval (R U) V K))).

type i      int -> tm.         % read contents of register
type read   tm.                % read contents of register
type inc    tm.                % add one to the register
type r      tm -> o.           % store the register's value here

cl (eval read V K     | r V     o- K | r V).
cl (eval inc  (i V) K | r (i V) o- U is (V + 1) o- (K | r (i U))).

type prog   int -> tm -> o.

prog 1 (abs x\x).
prog 2 (app (abs x\x) (abs x\x)).
prog 3 (app (abs x\inc) read).
prog 4 (app (abs x\read) inc).
prog 5 (app (app (abs x\(abs y\read)) inc) inc).


% sample queries

% prog N P, right nil nil ((r (i 4) | eval P V erase)::nil).