module queuespi.

import queuesig, cellsig, spinach.

% Typechecker stuff
%%%%%%%%%%%%%%%%%%%% 

% Extension
%
extends queue object.

% otype queue class.
%
tcheck Theta queue Cont tmod TC :-
	popmod queue M,
	pi C\ tcheck ((tp C (tref queue))::Theta) (M C) Cont tprog TC.

tcheck Theta (new queue P) Cont tcmd TC :-
	pi C\ tcheck ((tp C (tref queue))::Theta) (P C) Cont tcmd TC.

tcheck Theta (cons C queue) Cont theadin TC :-
	tcheck Theta C nil (tref queue) nil,
	tcheck Theta none Cont dot TC.

tcheck Theta (cons C queue) Cont theadout TC :-
	tcheck Theta none Cont dot TC.

tcheck Theta (super C queue) Cont tcmd TC :-
	tcheck Theta none Cont dot TC.

% Private data
%
tcheck Theta (ppriv queue hd) Cont (tref cell) TC :-
	tcheck Theta none Cont dot TC.			% ptype hd queue (ref cell)

% No constants here
%

% Methods
%
% mtype set_head	in 	ref queue -> ref cell -> cmd.
%
tcheck Theta (set_head Q C) Cont tcmd TC :- 
	tcheck Theta Q nil (tref queue) nil,
	tcheck Theta C nil (tref cell) nil,
	tcheck Theta none Cont dot TC.				% write	

tcheck Theta (set_head Q C) Cont theadin TC :-
	tcheck Theta Q nil (tref queue) nil,
	tcheck ((tp C (tref cell))::Theta) none Cont dot TC.	% headin

tcheck Theta (set_head Q C) Cont theadout TC :-
	tcheck Theta none Cont dot TC.				% headout
 
% mtype enqueue		in 	ref queue -> ref object -> cmd.
%
tcheck Theta (enqueue C O) Cont tcmd TC :- 
	tcheck Theta C nil (tref queue) nil,
	tcheck Theta O nil (tref object) nil,
	tcheck Theta none Cont dot TC.				% write	

tcheck Theta (enqueue C O) Cont theadin TC :-
	tcheck Theta C nil (tref queue) nil,
	tcheck ((tp O (tref object))::Theta) none Cont dot TC.	% headin

tcheck Theta (enqueue C O) Cont theadout TC :-
	tcheck Theta none Cont dot TC.				% headout

% mtype dequeue		out 	ref queue -> ref object -> cmd.
%
tcheck Theta (dequeue C O) Cont tcmd TC :-
	tcheck Theta C nil (tref queue) nil,
	tcheck Theta O nil dot nil,
	tcheck ((tp O (tref object))::Theta) none Cont dot TC.	% read

tcheck Theta (dequeue C O) Cont ttest TC :- 
	tcheck Theta C nil (tref queue) nil,
	tcheck Theta O nil (tref object) nil,
	tcheck Theta none Cont dot TC.				% test

tcheck Theta (dequeue C O) Cont theadin TC :-
	tcheck Theta C nil (tref queue) nil,
	tcheck Theta none Cont dot TC.				% headin

tcheck Theta (dequeue C O) Cont theadout TC :-
	tcheck Theta O nil (tref object) nil,
	tcheck Theta none Cont dot TC.				% headout


% Spinacher stuff
%%%%%%%%%%%%%%%%%

% otype queue class. 
%
spinach Theta Mu (tref queue) "Queue".

spinach Theta Mu queue Java :-
	popmod queue P,
	extends queue O,
	spinach nil nil (tref O) SO,
	pi C\ spinach ((tp C (tref queue))::Theta) ((np C "this")::Mu) (P C) JP,
	Java is "public class " ^ "Queue" ^ " extends " ^ SO ^ "{\n" ^ JP ^ "}\n".

spihead Theta Mu (cons W (queue)) nil Java "" :-
	Java is "Queue(){\n".

spinach Theta Mu (popnew queue S P) Java :-
	pi O\ spinach ((tp O (tref queue))::Theta) ((np O S)::Mu) (P O) JP,
	spinach nil nil (tref queue) JS,
	Java is JS ^ " " ^ S ^ " = new " ^ JS ^ "();\n" ^ JP.	

spinach Theta Mu (super C (queue)) Java :-
	Java is "super(" ^ ");\n".

% mtype set_head	in 	ref queue -> ref cell -> cmd.
%
spihead Theta Mu (set_head Q C) (C::nil) Java "" :-
	spinach nil nil (tref cell) STC,
	spinach Theta Mu C SC,
	Java is "public void set_head( " ^ STC ^ " " ^ SC ^ " ){\n".

spinach Theta Mu (set_head Q C) Java :-
	spinach Theta Mu Q SQ,
	spinach Theta Mu C SC,
	Java is SQ ^ ".set_head(" ^ SC ^ ");\n".

% mtype enqueue		in 	ref queue -> ref object -> cmd.
%
spihead Theta Mu (enqueue C O) (O::nil) Java "" :-
	spinach nil nil (tref object) STO,
	spinach Theta Mu O SO,
	Java is "public void enqueue( " ^ STO ^ " " ^ SO ^ " ){\n".

spinach Theta Mu (enqueue C O) Java :-
	spinach Theta Mu C SC,
	spinach Theta Mu O SO,
	Java is SC ^ ".enqueue(" ^ SO ^ ");\n". 

% mtype dequeue		out 	ref queue -> ref object -> cmd.
%
spihead Theta Mu (dequeue C O) nil Java Jreturn :-
	spinach nil nil (tref object) STO,
	Java is "public " ^ STO  ^" dequeue(){\n",
	spinach Theta Mu O SO, 
	Jreturn is "return " ^ SO ^ ";\n".

spinach Theta Mu (dequeue C O) Java :-
	spinach Theta Mu C SC,
	spinach Theta Mu O SO,
	Java is SO ^ "=" ^ SC ^ ".dequeue();". 	

spitest Theta Mu (dequeue C O) Java :-
	spinach Theta Mu C SC,
	spinach Theta Mu O SO,
	Java is SO ^ "==" ^ SC ^ ".dequeue()".