% Spinach file for the gate class % module gatespi. import typechecker, wiresig, gatesig, spinach. % Extension % extends gate object. % Typechecker stuff %%%%%%%%%%%%%%%%%%% % Generated by: otype gate ref wire -> class. % tcheck Theta gate Cont tmod TC :- popmod (gate Outwire) M, pi C\ tcheck ((tp C (tref gate))::Theta) (M C) Cont tprog TC. tcheck Theta (new (gate Outwire) P) Cont tcmd TC :- tcheck Theta Outwire nil (tref wire) nil, pi C\ tcheck ((tp C (tref gate))::Theta) (P C) Cont tcmd TC. tcheck Theta (cons G (gate Outwire)) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck ((tp Outwire (tref wire))::Theta) none Cont dot TC. tcheck Theta (cons G (gate Outwire)) Cont theadout TC :- tcheck Theta none Cont dot TC. tcheck Theta (super C (gate Outwire)) Cont tcmd TC :- tcheck Theta Outwire nil (tref wire) nil, tcheck Theta none Cont dot TC. % Private data % tcheck Theta (ppriv gate outw) Cont (tref wire) TC :- tcheck Theta none Cont dot TC. % Generated by: ptype gate state ref wire. tcheck Theta (ppriv gate state) Cont popbool TC :- tcheck Theta none Cont dot TC. % Generated by: ptype gate queue boolean. % Methods % % Generated by mtype get_output out ref gate -> ref wire -> cmd. % tcheck Theta (get_output G W) Cont tcmd TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta W nil dot nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % read tcheck Theta (get_output G W) Cont ttest TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % test tcheck Theta (get_output G W) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (get_output G W) Cont theadout TC :- tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % headout % Generated by mtype set_output in ref gate -> ref wire -> cmd. % tcheck Theta (set_output G W) Cont tcmd TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % write tcheck Theta (set_output G W) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % headin tcheck Theta (set_output G W) Cont theadout TC :- tcheck Theta none Cont dot TC. % headout % Generated by mtype get_state out ref gate -> boolean -> cmd. % tcheck Theta (get_state G S) Cont tcmd TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta S nil dot nil, tcheck ((tp S popbool)::Theta) none Cont dot TC. % read tcheck Theta (get_state G S) Cont ttest TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta S nil popbool nil, tcheck Theta none Cont dot TC. % test tcheck Theta (get_state G S) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (get_state G S) Cont theadout TC :- tcheck Theta S nil popbool nil, tcheck Theta none Cont dot TC. % headout % Generated by mtype alert in ref gate -> cmd. % tcheck Theta (alert G) Cont tcmd TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta none Cont dot TC. % write tcheck Theta (alert G) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (alert G) Cont theadout TC :- tcheck Theta none Cont dot TC. % headout % Generated by: mtype computestate out ref gate -> boolean -> acmd. % tcheck Theta (computestate G S) Cont tcmd TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta S nil dot nil, tcheck ((tp S popbool)::Theta) none Cont dot TC. % read tcheck Theta (computestate G S) Cont ttest TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta S nil popbool nil, tcheck Theta none Cont dot TC. % test tcheck Theta (computestate G S) Cont theadin TC :- tcheck Theta G nil (tref gate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (computestate G S) Cont theadout TC :- tcheck Theta S nil popbool nil, tcheck Theta none Cont dot TC. % headout % Spinacher stuff %%%%%%%%%%%%%%%%% % Generated by: otype gate wire -> aclass. % spinach Theta Mu (tref gate) "Gate". spinach Theta Mu gate Java :- popmod (gate Outwire) P, extends gate O, spinach nil nil (tref O) SO, spinach nil nil (tref gate) JS, pi C\ spinach ((tp C (tref gate))::Theta) ((np C "this")::Mu) (P C) JP, Java is "public abstract class " ^ JS ^ " extends " ^ SO ^ "{\n" ^ JP ^ "}\n". spihead Theta Mu (cons G (gate W)) (W::nil) Java "" :- spinach nil nil (tref wire) STW, spinach Theta Mu W SW, spinach nil nil (tref gate) JS, Java is JS ^ "(" ^ STW ^ " " ^ SW ^ "){\n". spinach Theta Mu (popnew (gate W) S P) Java :- pi O\ spinach ((tp O (tref gate))::Theta) ((np O S)::Mu) (P O) JP, spinach nil nil (tref gate) JS, spinach nil nil W SW, Java is JS ^ " " ^ S ^ " = new " ^ JS ^ "(" ^ SW ^ ");\n" ^ JP. spinach Theta Mu (super C (gate W)) Java :- spinach Theta Mu W SW, Java is "super(" ^ SW ^ ");\n". % Methods % % Generated by: mtype get_output out ref gate -> ref wire -> cmd. % spihead Theta Mu (get_output G W) nil Java Jreturn :- spinach nil nil (tref wire) STW, Java is "public " ^ STW ^ " get_output" ^ "(" ^ "){\n", spinach Theta Mu W SW, Jreturn is "return " ^ SW ^ ";\n". spinach Theta Mu (get_output G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SW ^ "=" ^ SG ^ "." ^ "get_output" ^ "(" ^ ");". % Generated by: mtype set_output in ref gate -> ref wire -> cmd. % spihead Theta Mu (set_output G W) (W::nil) Java "" :- spinach nil nil (tref wire) STW, spinach Theta Mu W SW, Java is "public void set_output" ^ "( " ^ STW ^ " " ^ SW ^ " ){\n". spinach Theta Mu (set_output G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SG ^ "." ^ "set_output" ^ "( " ^ SW ^ ");\n". % Generated by: mtype get_state out ref gate -> boolean -> cmd. % spihead Theta Mu (get_state G S) nil Java Jreturn :- spinach nil nil popbool STS, Java is "public " ^ STS ^ " get_state" ^ "(" ^ "){\n", spinach Theta Mu S SS, Jreturn is "return " ^ SS ^ ";\n". spinach Theta Mu (get_state G S) Java :- spinach Theta Mu G SG, spinach Theta Mu S SS, Java is SS ^ "=" ^ SG ^ "." ^ "get_state" ^ "(" ^ ");". % Generated by: mtype alert in ref gate -> cmd. % spihead Theta Mu (alert G) nil Java "" :- Java is "public void alert" ^ "(" ^ "){\n". spinach Theta Mu (alert G) Java :- spinach Theta Mu G SG, Java is SG ^ "." ^ "alert" ^ "(" ^ ");\n". % Generated by: mtype computestate out ref gate -> boolean -> acmd. % spihead Theta Mu (computestate G S) nil Java Jreturn :- spinach nil nil popbool STS, tcheck Theta G nil (tref gate) nil, Java is "public abstract " ^ STS ^ " computestate" ^ "(" ^ "){\n", spinach Theta Mu S SS, Jreturn is "return " ^ SS ^ ";\n". spinach Theta Mu (computestate G S) Java :- spinach Theta Mu G SG, spinach Theta Mu S SS, Java is SS ^ "=" ^ SG ^ "." ^ "computestate" ^ "(" ^ ");\n".