|
|
|---|
|
|
|
|---|
Connects ACL2 and the outside world.
The ACL2 Bridge is a general mechanism for allowing other programming languages, which may be much better than Lisp for certain tasks like developing graphical user interfaces, to interact with ACL2. It extends ACL2 with a server that can accept connections from client programs and run commands on their behalf. The basic picture is:
_____________ _______________________ | | | | | ACL2 [bridge]--------------| client program | | | socket | java, c, perl, ... | |_____________| |_______________________|
On the ACL2 side, the bridge is a simple listen/accept style server that waits for new clients. When a client connects, it creates a new worker thread to handle the client's requests. The worker thread presents the client with a kind of read-eval-print loop.
The client then sends commands. Basically each command says what s-expression to evaluate, and also indicates how the reply should be encoded. For instance, you can tell the bridge to return raw s-expressions, or you can tell it to use json-encoding to make the output easy to parse in some other programming languages. Other options may be added in the future.
The worker thread executes the command. As it runs, it may send messages to the client. These messages contain output that has been printed to standard output, the return value or error conditions, and a ready indicator that says when the worker is ready for more input. The messages are tagged with types so that the client can tell what kind of output it's receiving.
Some things are missing. There's currently no support for Lisp functions
that want to read from standard input after they've been invoked. For
instance, there's not really any way to interact with break loops,