% Spinach file for the list object
% Notice that the "head" typing rules are forgotten about here since we won't
% typecheck the list module (and because we are lazy).
%
module listspi.

import typechecker, spinach.

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

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

tcheck Theta (super L poplist) Cont tcmd TC :-
	tcheck Theta none Cont dot TC.

% Private data
%
% Irrelevant here.

% Constants
%
tcheck Theta null Cont (tref poplist) TC :-
	tcheck Theta none Cont dot TC.		

% Methods
% 
% pophead
%
tcheck Theta (pophead L H) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta H nil dot nil,
	tcheck ((tp H (tref object))::Theta) none Cont dot TC.		% read

tcheck Theta (pophead L H) Cont ttest TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta H nil (tref object) nil,
	tcheck Theta none Cont dot TC.					% test

% poptail
%
tcheck Theta (poptail L T) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta T nil (tref poplist) nil,
	tcheck Theta none Cont dot TC.					% write

tcheck Theta (poptail L T) Cont ttest TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta T nil (tref poplist) nil,
	tcheck Theta none Cont dot TC.					% test

% popisnil
%
tcheck Theta (popisnil L I) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta I nil dot nil,
	tcheck ((tp I popbool)::Theta) none Cont dot TC.		% read

tcheck Theta (popisnil L I) Cont ttest TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta I nil popbool nil,
	tcheck Theta none Cont dot TC.					% test

% popbuild 
%
tcheck Theta (popbuild L H) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta H nil (tref object) nil,	
	tcheck Theta none Cont dot TC.					% write

% popappend
% 
tcheck Theta (popappend L P) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta P nil (tref poplist) nil,
	tcheck Theta none Cont dot TC.					% write

% popdelete
%
tcheck Theta (popdelete L E) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta E nil (tref object) nil,
	tcheck Theta none Cont dot TC.					% write

% popreverse
%
tcheck Theta (popreverse L) Cont tcmd TC :-
	tcheck Theta L nil (tref poplist) nil,
	tcheck Theta none Cont dot TC.					% write


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

% Construction
%
spinach Theta Mu (tref poplist) "PopList".

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

% Methods
%
% pophead
%
spinach Theta Mu (pophead L H) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu H SH,
	Java is SH ^ " = " ^ SL ^ "." ^ "pophead" ^ "(" ^ ");\n". 

spitest Theta Mu (pophead L H) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu H SH,
	Java is SL ^ "." ^ "pophead" ^ "(" ^ ")" ^ " == " ^ SH.  

% poptail
%
spinach Theta Mu (poptail L T) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu T ST,
	Java is SL ^ "." ^ "poptail" ^ "(" ^ ST ^ ");\n". 

spitest Theta Mu (poptail L T) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu T ST,
	Java is SL ^ "." ^ "poptail" ^ "(" ^ ")" ^ " == " ^ ST.

% popisnil
%
spinach Theta Mu (popisnil L I) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu I SI,
	Java is SI ^ " = " ^ SL ^ "." ^ "popisnil" ^ "(" ^ ");\n". 

spitest Theta Mu (popisnil L I) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu I SI,
	Java is SL ^ "." ^ "popisnil" ^ "(" ^ ")" ^ " == " ^ SI.

% popbuild
%
spinach Theta Mu (popbuild L H) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu H SH,
	Java is SL ^ "." ^ "popbuild" ^ "(" ^ SH ^ ");\n".

% popappend
%
spinach Theta Mu (popappend L P) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu P SP,
	Java is SL ^ "." ^ "popappend" ^ "(" ^ SP ^ ");\n".

% popdelete
%
spinach Theta Mu (popdelete L E) Java :-
	spinach Theta Mu L SL,
	spinach Theta Mu E SE,
	Java is SL ^ "." ^ "popdelete" ^ "(" ^ SE ^ ");\n".

% popreverse
%
spinach Theta Mu (popreverse L) Java :-
	spinach Theta Mu L SL,
	Java is SL ^ "." ^ "popreverse" ^ "(" ^ ");\n".