% Spinach file for the notgate class
% 
module notgatespi.

import typechecker, wiresig, gatesig, unigatesig, notgatesig, spinach.

% Extension
%
extends notgate unigate.

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

% Generated by: 	otype notgate 	ref wire -> ref wire -> class.
%
tcheck Theta notgate Cont tmod TC :-
	popmod (notgate Inwire Outwire) M,
	pi C\ tcheck ((tp C (tref notgate))::Theta) (M C) Cont tprog TC.

tcheck Theta (new (notgate Inwire Outwire) P) Cont tcmd TC :-
	tcheck Theta Inwire nil (tref wire) nil,
	tcheck Theta Outwire nil (tref wire) nil,
	pi C\ tcheck ((tp C (tref notgate))::Theta) (P C) Cont tcmd TC.

tcheck Theta (cons G (notgate Inwire Outwire)) Cont theadin TC :-
	tcheck Theta G nil (tref notgate) nil,
	tcheck ((tp Inwire (tref wire))::(tp Outwire (tref wire))::Theta) none Cont dot TC.

tcheck Theta (cons G (notgate Inwire Outwire)) Cont theadout TC :-
	tcheck Theta none Cont dot TC.

tcheck Theta (super C (notgate Inwire Outwire)) Cont tcmd TC :-
	tcheck Theta Inwire nil (tref wire) nil,
	tcheck Theta Outwire nil (tref wire) nil,
	tcheck Theta none Cont dot TC.

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

% Generated by: otype notgate 	ref wire -> ref wire -> class.
%
spinach Theta Mu (tref notgate) "Notgate".

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

spihead Theta Mu (cons G (notgate Inwire Outwire)) (Inwire::Outwire::nil) Java "" :-
	spinach nil nil (tref wire) STW,
	spinach Theta Mu Inwire SInwire,
	spinach Theta Mu Outwire SOutwire,
	Java is "Notgate" ^ "(" ^ STW ^ " " ^ SInwire ^ ", " ^ STW ^ " " ^ SOutwire ^ "){\n".

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

spinach Theta Mu (super C (notgate Inwire Outwire)) Java :-
	spinach Theta Mu Inwire JI,
	spinach Theta Mu Outwire JO,
	Java is "super(" ^ JI ^ ", " ^ JO ^ ");\n".