/* 
 * RAM simulator in CHR(chr)
 * Author: Seiji OGAWA, 2011-03-31
 * 
 * Examples are taken from:
 *   http://dtai.cs.kuleuven.be/CHR/examples.shtml
 *
 * If you'd like to change parameter N, 
 * please change the 1st argument of query: start("N").
 *
 */

:- use_module(library(chr)).
:- chr_option(optimize, full).
:- chr_constraint mem(+dense_int,+int), prog(+dense_int,+int,+any,+int), prog_counter(+dense_int), 
    init(+int), time(+float), start(+int), i(+int,+int),
    make_mem(+int), make_pc(+int).
%:- chr_constraint mem(+,+), prog(+,+,+,+), prog_counter(+).
%:- chr_constraint mem/2, prog/4, prog_counter/1, init/1, time/1, start/1, i/2, make_mem/1.
%:- chr_trace.


start(S) <=>
  cputime(X),
  init(S),
  cputime(Y),
  Z is Y-X,
  time(Z).

init(S) <=>
  S1 is S-1,
  make_mem(30),
	mem(1,1), 
	mem(2,S), 
	mem(3,0),
  prog(1,2, add(1), 3),
  prog(2,3, sub(1), 2),
  prog(3,1, cjump(2), 4),
  prog_counter(1).

make_mem(M) <=> M > 3 | M1 is M-1, make_mem(M1), mem(M,0), prog(M, M1, halt, 0).

%prog_counter(0), mem(1,_), mem(2,_), mem(3,_), i(S, I) <=> 
%  I > 0 | I1 is I-1, i(S, I1), prog_counter(1), mem(1,1), mem(2,S), mem(3,0).

%mem(A,_) \ mem(A,_) <=> true.

% add value of register B to register A
prog(L,L1,add(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
     Z is X+Y, mem(A,Z), prog_counter(L1).
% subtract value of register B from register A
prog(L,L1,sub(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
    Z is X-Y, mem(A,Z), prog_counter(L1).
% multiply register A with value of register B
%prog(L,L1,mult(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
%    Z is X*Y, mem(A,Z), prog_counter(L1).
% divide register A by value of register B
%prog(L,L1,div(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
%    Z is X//Y, mem(A,Z), prog_counter(L1).


% put the value in register B in register A
%prog(L,L1,move(B),A), mem(B,X) \ mem(A,_), prog_counter(L) <=> 
%    mem(A,X), prog_counter(L1).
% put the value in register <value in register B> in register A
%prog(L,L1,i_move(B),A), mem(B,C), mem(C,X) \ mem(A,_), prog_counter(L) <=> 
%    mem(A,X), prog_counter(L1).
% put the value in register B in register <value in register A>
%prog(L,L1,move_i(B),A), mem(B,X), mem(A,C) \ mem(C,_), prog_counter(L) <=> 
%    mem(C,X), prog_counter(L1).

%i_move_i(B), A : i_move(B), 0
%	  	  move_i(0), A

% put the value B in register A        -> redundant if consts are in init mem
%prog(L,L1,const(B),A) \ mem(A,_), prog_counter(L) <=> 
%    mem(A,B), prog_counter(L1).
%prog(L,L1,clr,A) \ mem(A,X), prog_counter(L) <=>   % same as const(0)
%    mem(A,0), prog_counter(L1).


% unconditional jump to label A
%prog(L,L1,Instr,A) \ prog_counter(L) <=> Instr == jump |
%    prog_counter(A).
% jump to label A if register R is zero, otherwise continue
prog(L,L1,cjump(R),A), mem(R,X) \ prog_counter(L) <=> X == 0 |
    prog_counter(A).
prog(L,L1,cjump(R),A), mem(R,X) \ prog_counter(L) <=> X =\= 0 |
    prog_counter(L1).

% halt
% prog(L,L1,Instr,_) \ prog_counter(L) <=> Instr == halt | true.
prog(L,L1,Instr,_) \ prog_counter(L) <=> Instr == halt | prog_counter(0).

% invalid instruction
% prog_counter(L) <=> true.

%:- constraints 	initmem(+natural).
%
%initmem(N) <=> N =:= 0 | mem(0,0).
%initmem(N) <=> N>0 | mem(N,0), N1 is N-1, initmem(N1).