\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}).

