/*

	?-com([upm,up]).
	?-tokio test.

		Thu Sep  4 22:22:41 GMT+9:00 1986
	*/

:- static([
	memory(_), g_addr, d_addr, g_cell, d_cell, g_mem, d_mem,
	length, stack_ln(_), stack_ga(_), stack_da(_),
	stack_depth, return_code, run, d_bus, g_bus]).


init:- 	
	*length <= (*memory(*g_addr)..data - 1,int,0),
	*d_addr <= (*d_addr..data + 2,int,*d_addr..map),
	*g_addr <= (*g_addr..data + 2,int,*g_addr..map),
	*stack_depth <= 0,
	*run <= 1
    &&  loop_unif.
	
loop_unif:- 
	if *length..data > 0
		then fetch_unif1
		else if *stack_depth = 0
			then (*return_code <= (0,int,0), *run <= 0  && idle)
			else   *length <= *stack_ln(*stack_depth - 1),
			       *g_addr <= *stack_ga(*stack_depth - 1),
			       *d_addr <= *stack_da(*stack_depth - 1),
			       *stack_depth <= *stack_depth - 1 
			   &&  fetch_unif1.
				   
fetch_unif1:-
	 fetch_unif0g, 
	 fetch_unif0d &&
	 *length <= (*length..data - 1,int,0),
	 *g_addr <= (*g_addr..data + 1,int, *g_addr..map),
	 *d_addr <= (*d_addr..data + 1,int, *d_addr..map) &&
	 fetch_unif2.

fetch_unif0g:-
	 fetch(*g_addr,*g_cell,*g_bus), *g_mem <= *g_addr  && 
	 if *g_cell..tag = var
		then fetch_unif1g.

fetch_unif1g:-
	 fetch(*g_cell,*g_cell,*g_bus), *g_mem <= *g_cell  && 
	 if *g_cell..tag = var
		then fetch_unif1g.

fetch_unif0d:-
	 fetch(*d_addr,*d_cell,*d_bus), *d_mem <= *d_addr  &&
	 if *d_cell..tag = var
		then fetch_unif1d.
	
fetch_unif1d:-
	 fetch(*d_cell,*d_cell,*d_bus), *d_mem <= *d_cell  && 
	 if *d_cell..tag = var
		then fetch_unif1d.
	
fetch_unif2:-
	if *g_mem = *d_mem then loop_unif 
	else {
	      G = *g_cell..tag, D = *d_cell..tag, {
	      if (G=undef,D=undef) then
		(store(*g_mem,*d_mem, *g_bus) && loop_unif)
	      else if (G=undef,D\=undef) then
		(store(*g_mem,*d_cell,*g_bus) && loop_unif)
	      else if (G\=undef,D=undef) then
		(store(*d_mem,*g_cell,*d_bus) && loop_unif)
	      else if (G=list,D=list) then
		(if *length..data > 0 
		    then ((*stack_depth <= *stack_depth + 1,
			   S<-- *stack_depth,
			   *stack_ga(S) <= *g_addr,
			   *stack_da(S) <= *d_addr,
			   *stack_ln(S) <= *length,
			   *length <= (2,int,g),
			   *g_addr <= *g_cell,
			   *d_addr <= *d_cell) && fetch_unif1)
		    else loop_unif)
	      else if (*g_cell..tag \= *d_cell..tag ; 
		     *g_cell..data \= *d_cell..data) then
		 ((*return_code <= fail, *run <= 0) && idle)
	      else loop_unif }}.


idle:- if *run = 1 
		then (true && init).


test:-
	*memory((0,_,g)) := (4,int,g), 	% length
	*memory((1,_,g)) := (append,atom,g),	%  append
	*memory((2,_,g)) := (100,list,g),
	*memory((3,_,g)) := (200,list,g),
	*memory((4,_,g)) := (300,var,g),
	*memory((5,_,g)) := (2,int,g),
	*memory((6,_,g)) := (print,atom,g),	% print
	*memory((7,_,g)) := (400,var,g),
	*memory((8,_,g)) := (0,int,g),	% length = 0
	*memory((100,_,g)) := (a,atom,g),
	*memory((101,_,g)) := (102,list,g),
	*memory((102,_,g)) := (b,atom,g),
	*memory((103,_,g)) := ([],atom,g),
	*memory((200,_,g)) := (c,atom,g),
	*memory((201,_,g)) := (102,list,g),
	*memory((202,_,g)) := (d,atom,g),
	*memory((203,_,g)) := ([],atom,g),
	*memory((300,_,g)) := (0,undef,g),
	*memory((400,_,g)) := (0,undef,g),
	*memory((0,_,d)) := (5,int,d),
	*memory((1,_,d)) := (append,atom,d),	% append([H|X],Y,[H|Z])
	*memory((2,_,d)) := (200,list,d),
	*memory((3,_,d)) := (300,var,d),
	*memory((4,_,d)) := (400,list,d),
	*memory((5,_,d)) := (5,int,d),
	*memory((6,_,d)) := (append,atom,d),   % append([],X,X)
	*memory((7,_,d)) := ([],atom,d),
	*memory((8,_,d)) := (100,var,d),
	*memory((9,_,d)) := (100,var,d),
	*memory((100,_,d)) := (0,undef,d),
	*memory((200,_,d)) := (500,var,d),    % [H|X]
	*memory((201,_,d)) := (600,var,d),  
	*memory((300,_,d)) := (0,undef,d),	% Y
	*memory((400,_,d)) := (700,list,d),	% [H|Z]
	*memory((500,_,d)) := (0,undef,d),	% H
	*memory((600,_,d)) := (0,undef,d),	% X
	*memory((700,_,d)) := (500,var,d),	% H
	*memory((701,_,d)) := (800,var,d),	% Z
	*memory((800,_,d)) := (0,undef,d),	% Z
	*g_addr := (0,int,g),
	*d_addr := (0,int,d),
	*return_code := (0,undef,0),
	*length := (0,int,0),
	*g_mem := (0,int,g),
	*d_mem := (0,int,d),
	*g_cell := (0,int,g),
	*d_cell := (0,int,d),
	*run := 0,
	*d_bus := free, *g_bus := free,
	*stack_depth := 0 &&
	init,
	# (Write = (*g_addr, *d_addr, *return_code, *run, *length, 
		 *g_mem, *d_mem, *g_cell, *d_cell, *stack_depth, 
		 *g_bus, *d_bus), write(Write) ).