% Spinach file for the unigate class % module bigatespi. import typechecker, wiresig, gatesig, bigatesig, spinach. % Extension % extends bigate gate. % Typechecker stuff %%%%%%%%%%%%%%%%%%% % Generated by: otype bigate ref wire -> ref wire -> ref wire -> aclass. % tcheck Theta bigate Cont tmod TC :- popmod (bigate InwireA InwireB Outwire) M, pi C\ tcheck ((tp C (tref bigate))::Theta) (M C) Cont tprog TC. tcheck Theta (new (bigate InwireA InwireB Outwire) P) Cont tcmd TC :- tcheck Theta InwireA nil (tref wire) nil, tcheck Theta InwireB nil (tref wire) nil, tcheck Theta Outwire nil (tref wire) nil, pi C\ tcheck ((tp C (tref bigate))::Theta) (P C) Cont tcmd TC. tcheck Theta (cons G (bigate InwireA InwireB Outwire)) Cont theadin TC :- tcheck Theta G nil (tref bigate) nil, tcheck ((tp InwireA (tref wire))::(tp InwireB (tref wire)):: (tp Outwire (tref wire))::Theta) none Cont dot TC. tcheck Theta (cons G (bigate InwireA InwireB Outwire)) Cont theadout TC :- tcheck Theta none Cont dot TC. tcheck Theta (super C (bigate InwireA InwireB Outwire)) Cont tcmd TC :- tcheck Theta InwireA nil (tref wire) nil, tcheck Theta InwireB nil (tref wire) nil, tcheck Theta Outwire nil (tref wire) nil, tcheck Theta none Cont dot TC. % Private data % tcheck Theta (ppriv bigate inwa) Cont (tref wire) TC :- tcheck Theta none Cont dot TC. tcheck Theta (ppriv bigate inwb) Cont (tref wire) TC :- tcheck Theta none Cont dot TC. % Methods % % Generated by: mtype out get_inputa ref bigate -> ref wire -> cmd. % tcheck Theta (get_inputa G W) Cont tcmd TC :- print "a", tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil dot nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % read tcheck Theta (get_inputa G W) Cont ttest TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % test tcheck Theta (get_inputa G W) Cont theadin TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (get_inputa G W) Cont theadout TC :- tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % headout % Generated by: mtype out get_inputb ref bigate -> ref wire -> cmd. % tcheck Theta (get_inputb G W) Cont tcmd TC :- print "b", tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil dot nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % read tcheck Theta (get_inputb G W) Cont ttest TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % test tcheck Theta (get_inputb G W) Cont theadin TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta none Cont dot TC. % headin tcheck Theta (get_inputb G W) Cont theadout TC :- tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % headout % Generated by: mtype in set_input ref bigate -> ref wire -> cmd. % tcheck Theta (set_inputa G W) Cont tcmd TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % write tcheck Theta (set_inputa G W) Cont theadin TC :- tcheck Theta G nil (tref bigate) nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % headin tcheck Theta (set_inputa G W) Cont theadout TC :- tcheck Theta none Cont dot TC. % headout % Generated by: mtype in set_input ref bigate -> ref wire -> cmd. % tcheck Theta (set_inputb G W) Cont tcmd TC :- tcheck Theta G nil (tref bigate) nil, tcheck Theta W nil (tref wire) nil, tcheck Theta none Cont dot TC. % write tcheck Theta (set_inputb G W) Cont theadin TC :- tcheck Theta G nil (tref bigate) nil, tcheck ((tp W (tref wire))::Theta) none Cont dot TC. % headin tcheck Theta (set_inputb G W) Cont theadout TC :- tcheck Theta none Cont dot TC. % headout % Spinacher stuff %%%%%%%%%%%%%%%%% % Generated by: otype bigate ref wire -> ref wire -> ref wire -> aclass. % spinach Theta Mu (tref bigate) "Bigate". spinach Theta Mu bigate Java :- popmod (bigate InwireA InwireB Outwire) P, extends bigate O, spinach nil nil (tref O) SO, pi C\ spinach ((tp C (tref bigate))::Theta) ((np C "this")::Mu) (P C) JP, Java is "public abstract class " ^ "Bigate" ^ " extends " ^ SO ^ "{\n" ^ JP ^ "}\n". spihead Theta Mu (cons G (bigate InwireA InwireB Outwire)) (InwireA::InwireB::Outwire::nil) Java "" :- spinach nil nil (tref wire) STW, spinach Theta Mu InwireA SInwireA, spinach Theta Mu InwireB SInwireB, spinach Theta Mu Outwire SOutwire, Java is "Bigate" ^ "(" ^ STW ^ " " ^ SInwireA ^ ", " ^ STW ^ " " ^ SInwireB ^ ", " ^ STW ^ " " ^ SOutwire ^ "){\n". spinach Theta Mu (popnew (bigate InwireA InwireB Outwire) S P) Java :- pi O\ spinach ((tp Outwire (tref bigate))::nil) ((np O S)::Mu) (P O) JP, spinach nil nil (tref bigate) JS, spinach nil nil InwireA SInwireA, spinach nil nil InwireB SInwireB, spinach nil nil Outwire SOutwire, Java is JS ^ " " ^ S ^ " = new " ^ JS ^ "(" ^ SInwireA ^ ", " ^ SInwireB ^ ", " ^ SOutwire ^ ");\n" ^ JP. spinach Theta Mu (super C (bigate InwireA InwireB Outwire)) Java :- spinach Theta Mu InwireA JIA, spinach Theta Mu InwireB JIB, spinach Theta Mu Outwire JO, Java is "super(" ^ JIA ^ ", " ^ JIB ^ ", " ^ JO ^ ");\n". % Methods % % Generated by: mtype get_inputa out ref bigate -> ref wire -> cmd. % spihead Theta Mu (get_inputa G W) nil Java Jreturn :- spinach nil nil (tref bigate) STG, Java is "public " ^ STG ^ " get_inputa" ^ "(" ^ "){\n", spinach Theta Mu W SW, Jreturn is "return " ^ SW ^ ";\n". spinach Theta Mu (get_inputa G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SW ^ "=" ^ SG ^ "." ^ "get_inputa" ^ "(" ^ ");\n". % Generated by: mtype get_inputb out ref bigate -> ref wire -> cmd. % spihead Theta Mu (get_inputb G W) nil Java Jreturn :- spinach nil nil (tref bigate) STG, Java is "public " ^ STG ^ " get_inputb" ^ "(" ^ "){\n", spinach Theta Mu W SW, Jreturn is "return " ^ SW ^ ";\n". spinach Theta Mu (get_inputb G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SW ^ "=" ^ SG ^ "." ^ "get_inputb" ^ "(" ^ ");\n". % Generated by: mtype set_inputa in ref bigate -> ref wire -> cmd. % spihead Theta Mu (set_inputa G W) (W::nil) Java "" :- spinach nil nil (tref wire) STW, spinach Theta Mu W SW, Java is "public void set_inputa" ^ "( " ^ STW ^ " " ^ SW ^ " ){\n". spinach Theta Mu (set_inputa G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SG ^ "." ^ "set_inputa" ^ "( " ^ SW ^ ");\n". % Generated by: mtype set_inputb in ref bigate -> ref wire -> cmd. % spihead Theta Mu (set_inputb G W) (W::nil) Java "" :- spinach nil nil (tref wire) STW, spinach Theta Mu W SW, Java is "public void set_inputb" ^ "( " ^ STW ^ " " ^ SW ^ " ){\n". spinach Theta Mu (set_inputb G W) Java :- spinach Theta Mu G SG, spinach Theta Mu W SW, Java is SG ^ "." ^ "set_inputb" ^ "( " ^ SW ^ ");\n".