\section{Implementation}\label{g-imp} We now discuss a simple \prolog{} interpreter for \tgentzen. The implementation is intended to enable users to quickly develop, run, test and debug \tgentzen{} programs, thus getting a feel for the \tcc{} computation model. The emphasis in this implementation is on simplicity rather than efficiency --- several well-known techniques that have been developed in the literature on implementations of logic programming languages and problem-solving systems can be used to substantially improve performance.\footnote{For instance, one standard technique is to use partial evaluation to generate from this interpreter a compiler that inputs a source \tcc{} program and outputs \prolog{} code. This techniques was used to generate very similar compiler-based implementations of Concurrent Prolog, GHC and \Herbrand.} Separately, we are implementing the FSA compilation algorithm outlined in \cite{tcc} for bounded \tcc{} programs. Clearly that compiler, once it exists, will be the implementation of choice to use in fielding embedded, reactive \tgentzen{} programs. \subsection{The basic interpreter} First we begin with basic operation declarations for symbols that will stand for \tcc{} combinators. \begin{ccprogram} \agent :- op(1100, xfy, '::').. \agent :- op(975, fy, [next, always]).. \agent :- op(950, xfy, [ ->, ~> ]).. \agent :- op(150, xfy, ['^', '\$']).. \agent :- use\_module(library(ordsets)).. \agent :- use\_module(library(lists)).. \end{ccprogram} The interpreter keeps track of the following pieces of information: \begin{enumerate} \item The current agents not yet examined (Pool). \item The Positive Asks that have already been discharged (Susp). \item The Tells that have already been executed (Store). \item The Nexts that have already been identified (Nexts). \item The Elses that have already been identified (Elses). \item The current cycle number (Count). \item The counter for existential quantifiers (V). \end{enumerate} At each step, the next agent from the pool is examined. Obvious things are done in simple cases: a {\tt []} agent is discarded, an \abort{} agent is Prolog-failed (causing Prolog-failed termination of the entire computation), a parallel composition is repackaged, a {\tt next} agent is pushed onto the Next list, an ${\tt \leadsto}$ agent is pushed onto the Else list, a recursive procedure call is unfolded by examining the program database. The interesting cases are Hiding, (parametric) Asks and Tells. Hiding is implemented by using the counters (and the functor {\tt '\_'/2}) to generate a unique identifier; this is then bound to the \Prolog{} variable representing the quantified \tgentzen{} variable. In the case of a Tell, the argument of the tell is added to the store. At the same time, all possible instances of the Positive Asks (that have already been discharged) that match this tell are added to the pool. Symmetrically, when a new Positive Ask is being executed, all possible instantiations that reduce against tokens in the store are added to Pool. (This is discussed in more detail below.) Computation in the cycle terminates when Pool is empty. All the accumulated Elses are now examined to see if they should be rejected or retained for the next cycle. The current Suspended agents and store are thrown away. The next cycle commences. \begin{ccprogram} \agent tcc([]) :-!.. \agent tcc([A | Pool]) :- !, tcc(A, Pool, [[], a([], []), [], [], 0, 0]).. \agent tcc(A) :- tcc(A, [], [[], a([], []), [], [], 0, 0]).. \agent tcc([], [Store, \_SuspA, Elses, Next, C, \_V]) :- !, next(Elses, Store, Next, New), (New {==} [] -> format('~n\ Termination\ at\ T=~p.', [C]) ; (C1\ is\ C+1, tcc(New, [[], a([], []), [], [], C1, 0]))).. \agent tcc([A | Pool], Rest) :- tcc(A, Pool, Rest).. \agent tcc(\{(A,B)\}, Pool, State) :- !, tcc(\{A\}, [\{B\} | Pool], State).. \agent tcc(\{C\}, Pool, [Store, SuspA | Rest]) :- !, install\_tell(C, Pool, Store, SuspA, NewPool, NewStore), tcc(NewPool, [NewStore, SuspA | Rest]).. \agent tcc((E1,E2)-> A, Pool, State) :- !, tcc(E1 -> E2 -> A, Pool, State).. \agent tcc((E1 ; E2) -> A, Pool, State) :- !, tcc(E1 -> A, [E2 -> A | Pool], State).. \agent tcc(C-> A, Pool, [Store, SuspA | Rest]) :-!, install\_ask(C->A, Pool, Store, SuspA, NewPool, NewSuspA), tcc(NewPool, [Store, NewSuspA | Rest]).. \agent tcc(E ~> A, Pool, [Store, SuspA, Elses | Rest]) :- !, tcc(Pool, [Store, SuspA, [E ~> A | Elses] | Rest]).. \agent tcc(next\ A, Pool, [Store, SuspA, Elses, Nexts | Rest ]) :- !, tcc(Pool, [Store, SuspA, Elses, [A | Nexts] | Rest]).. \agent tcc(\_X\$A, Pool, State) :- !, tcc(A, Pool, State).. \agent tcc(Vars^A, Pool, [Store, SuspA, Elses, Nexts, C, V]) :- !, inst\_ex\_vars(Vars, C, V, NV), tcc(A, Pool, [Store, SuspA, Elses, Nexts, C, NV]).. \agent tcc(abort, \_Pool, \_State) :- !, fail.. \agent tcc([], Pool, State) :- !, tcc(Pool, State).. \agent tcc([A | B], Pool, State) :- !, tcc(A, [B | Pool], State).. \agent tcc(Goal, Pool, State) :- !, (Goal :: Body),!, tcc(Body, Pool, State).. \end{ccprogram} \subsection{The \Gentzen{} constraint system.} Consider now the implementation of Ask and Tell operations. \paragraph{Ask operations} A check is made for whether the Ask operation is basic (e.g., an arithmetic routine). If it is, the operation is treated as a \Prolog{} call and fails or succeeds as appropriate. There are two remaining cases. If the Ask is not parametric, then the store is checked for the match; if there is a match, the Ask is reduced. As an optimization, note that there is no need to record the Ask in Susp since multiple firings will result only in the very same body being fired multiple times. If the Ask is parametric, it is recorded in Susp (multiple firings may potentially be different because of the values bound to variables). A check is made for instantiations in the current store. The heart of the constraint system operation is this check. The \Prolog{} {\tt bagof/3} predicate is used to generate all possible matches of the Ask, and, for each match, to generate the corresponding instantiated body of the Ask. Of importance here is the ability to specify that the query in {\tt bagof} must be existentially instantiated for all the variables that occur in the Ask. (It is for this purpose that Susp actually contains the list $T$ of suspended Asks, together with the list of free variables in $T$. The call to {\tt vars/6} is used to update this list.) This allows the correct treatment of \tgentzen{} universal variables in Ask-queries (and any \tgentzen{} existential variables in the body of the query). Indeed, the \Prolog{} variables representing \tgentzen{} universal variables will never be instantiated in the course of the computation; {\tt bagof} will use those variables to create copies exactly as needed. (Note that atoms added to the store will always be \Prolog{}-ground, since existential variables are represented as \Prolog{}-ground terms.) The resulting set of agents is then added to Pool. \begin{ccprogram} \agent install\_ask(C->A, Pool, Store, a(Var, SuspA), NewPool, NewSusp) :- ask\_basic(C) -> \(NewSusp = a(Var, SuspA), \(call(C) -> NewPool = [A | Pool] ; NewPool = Pool\)\) ; \(vars(A, C, Var, VC, Vs, NewVar), \quad\(VC == [] ->{} \(member(C, Store) -> (NewPool = [A | Pool], NewSusp = a(Var, SuspA)) ; (NewPool = Pool, NewSusp = a(NewVar, [C -> A | SuspA]))\) ; \(NewSusp = a(NewVar, [C -> A | SuspA]), \(bagof(A, Vs^member(C, Store), Agents) -> NewPool=[Agents | Pool] ; NewPool = Pool\)\)\)\).. \agent ask\_basic((\_X::\_Y)).. \agent ask\_basic(\_X\ is\ \_Y).. \agent ask\_basic(\_X =:= \_Y).. \agent ask\_basic(\_X < \_Y).. \agent ask\_basic(\_X =< \_Y).. \agent ask\_basic(\_X =\= \_Y).. \agent ask\_basic(\_X >= \_Y).. \agent ask\_basic(\_X > \_Y).. \agent ask\_basic(read(\_X)).. \agent vars(A, C, Var, VC, Vs, NewVar) :- vars(A, VA), vars(C, VC), ord\_union(VA, VC, Vars1), ord\_subtract(VC, VA, Vs), ord\_union(Vars1, Var, NewVar).. \agent vars(Term, Vars) :- vars(Term, [], Vars).. \agent vars(X, V, Vars) :- var(X), !, ord\_add\_element(V, X, Vars).. \agent vars(Term, V, Vars) :- functor(Term, \_F, A), vars\_each(0, A, Term, V, Vars).. \agent vars\_each(M, N, Term, V, Vars):- M = N -> V = Vars ; ( M1\ is\ M+1, arg(M1, Term, Term\_M1), vars(Term\_M1, Var1), ord\_union(Var1, V, Var2), vars\_each(M1, N, Term, Var2, Vars)).. \end{ccprogram} \paragraph{Tells.} Tells are implemented dually to Asks. A basic Tell is simply executed; note that basic Tells allowed are such that they cannot fail. For non-basic Tells, a check is made to see if the atom being told is already in the store, in which case it can be discarded. Otherwise {\tt bagof/3} is used to generate the list of instantiated Ask agents (from Susp) that can now fire; this list is added to Pool. \begin{ccprogram} \agent install\_tell(C, Pool, Store, a(Vars, SuspA), NewPool, NewStore) :- tell\_basic(C) -> (call(C), NewStore = Store, NewPool=Pool) ; \(member(C, Store) -> (NewStore = Store, NewPool = Pool) ; \(NewStore = [C | Store], \(bagof(A, Vars^member(C->A, SuspA), Agents) -> NewPool = [Agents | Pool] ; NewPool = Pool\)\)\).. \agent tell\_basic(format(\_X, \_Y)).. \agent tell\_basic(ttyflush).. \end{ccprogram} \paragraph{Negative Asks.} When moving from one time instant to the next, the list of Negative Ask agents is examined. Those agents whose condition is {\em not} entailed are carried over; others are discarded. \begin{ccprogram} \agent next([], \_Store, Next, Next).. \agent next([C ~> A | E], Store, Next, Out) :- !, \(succeeds(C, Store) -> next(E, Store, Next, Out) ; (Out = [A | Out1], next(E, Store, Next, Out1))\).. \agent succeeds((C1, C2), Store) :- !, succeeds(C1, Store), succeeds(C2, Store).. \agent succeeds((C1 ; C2), Store) :- !, (succeeds(C1, Store); succeeds(C2, Store)).. \agent succeeds(C, Store) :- ask\_basic(C) -> call(C) ; member(C, Store).. \end{ccprogram} \input{def_combinators.tex} \paragraph{That's it!} This completes the description of the interpreter. The general combinators defined in previous sections (e.g. {\tt whenever}, {\tt watching}) can be defined as user programs (Tables~\ref{assorted-def},~\ref{clock-def}).