Figure out how to allow twelf code to control event loop

[jcreedcmu]

The goal of this issue is to allow a twelf logic program, via FFI, to call WaitNextEvent, dispatch on event->what, and then call itself again in a loop, until some user choice terminates the loop.

It would be nice if we could simply write the loop in a (logic-programming) tail-recursive style, like

...
state : type. % some internal state for the loop

output : type.
success : output.

%% We imagine this to be supplied by the %use mac/toolbox constraint domain
% event : type.
% wait-next-event : event -> type.

% This logic program could have side effects by making other FFI calls,
% creating windows, etc.
update-state-for-event : event -> state -> state -> type.
% implement 'update-state-for-event' ...

% This logic program decides whether a state ends our infinite loop or not
done : state -> bool -> type.
% implement 'done' ...

loop : state -> output -> type.
loop/continue : 
  loop S OUT
   <- done S false
   <- wait-next-event E
   <- update-state-for-event E S S'
   <- loop S' OUT.

loop/stop :
  loop S success
   <- done S true.

%query 1 1 tail-rec initial-state OUT.

However, I'm concerned that %query might still keep around enough data to reconstruct a proof term to justify its substitution, which would mean an continual leaking of memory as the predicate tail-rec iterates.

[jcreedcmu]

It seems possible (but not certain) that %fquery might help, see https://delphin.poswolsky.com/publications specifically "Factoring Report"

Chapter 8 of these notes might be relevant to understanding what's going on in twelf's compile.fun.

[jcreedcmu]

Unfortunately, %compile and %fquery don't seem to do TCO out of the box:

%use equality/integers.

x : integer -> type.

program : integer -> integer -> integer -> type.
/ : program 0 ACC ACC.
/ : program N ACC OUT <- program (N - 1) (ACC + 1) OUT.
%worlds () (program _ _ _).
%mode (program +N +ACC -M).
%compile program.
%fquery  (program 100000 0 X).

on twelf-wasm runs out of memory. However, inspecting the output, we see the functional program pretty-printed:

fun program 0 ACC = <ACC, <>>
  | program N ACC = let
                         val <OUT, <>> =  program (~1 + N) (1 + ACC)
                    in
                      <OUT, <>>
                    end

This program is not actually tail-recursive, due to the tupling around the output value OUT. Possibly a small tweak to the implementation of %compile might allow real tail-call optimization?

[jcreedcmu]

The code responsible for pretty-printing these compiled programs is here in tomegaprint.fun.

[jcreedcmu]

tomega.sig has the definition of Prg, the syntax type for compiled functional programs.