Add z3 repl

Julien LepillerThu Jan 23 21:51:25+0100 2020

c2c8c87

Add z3 repl

README.md

101101 
Of course, we pass Z3 actual s-expressions, so we can use all the quote-unquote
102102 
magick we are used to!
103103 
104+
Interactive Z3 Session
105+
----------------------
106+
107+
To start an interactive Z3 session through the Guile REPL, use this command:
108+
109+
```scheme
110+
,use (z3) ; use guile-z3
111+
,z3 ; start a Z3 repl!
112+
```
113+
104114 
Quick Reference
105115 
---------------
106116 
build-aux/guile.am unknown status 1
1+
GOBJECTS = $(SOURCES:%.scm=%.go)
2+
3+
nobase_mod_DATA = $(SOURCES) $(NOCOMP_SOURCES)
4+
nobase_go_DATA = $(GOBJECTS)
5+
6+
# Make sure source files are installed first, so that the mtime of
7+
# installed compiled files is greater than that of installed source
8+
# files.  See
9+
# <http://lists.gnu.org/archive/html/guile-devel/2010-07/msg00125.html>
10+
# for details.
11+
guile_install_go_files = install-nobase_goDATA
12+
$(guile_install_go_files): install-nobase_modDATA
13+
14+
CLEANFILES = $(GOBJECTS)
15+
EXTRA_DIST = $(SOURCES) $(NOCOMP_SOURCES)
16+
GUILE_WARNINGS = -Wunbound-variable -Warity-mismatch -Wformat
17+
SUFFIXES = .scm .go
18+
.scm.go:
19+
	$(AM_V_GEN)$(top_builddir)/env $(GUILE_TOOLS) compile $(GUILE_TARGET) $(GUILE_WARNINGS) -o "$@" "$<"
z3.scm.in
2828 
  #:use-module (system foreign)
2929 
  #:use-module (rnrs bytevectors)
3030 
  #:use-module (srfi srfi-9)
31+
  #:use-module (system base language)
32+
  #:use-module (system repl command)
33+
  #:use-module (system repl common)
34+
  #:use-module (system repl repl)
3135 
  #:export (z3-eval
3236 
            run-with-z3))
3337 
…
8488 
      (lambda ()
8589 
        (z3-del-context ctx)
8690 
        (z3-del-config conf)))))
91+
92+
(define-meta-command ((z3 exp) repl)
93+
  "Run exp in custom repl."
94+
  (run-with-z3
95+
    (lambda (context)
96+
      (let* ((scheme (lookup-language 'scheme))
97+
             (new (make-repl
98+
                   (make-language #:name "z3"
99+
                                  #:title "z3"
100+
                                  #:reader (language-reader scheme)
101+
                                  #:evaluator (lambda (exp env)
102+
                                                (z3-eval context (list exp)))
103+
                                  #:printer (language-printer scheme)
104+
                                  #:make-default-environment
105+
                                  (language-make-default-environment scheme)))))
106+
        (repl-option-set! new 'interp #t)
107+
        (run-repl new)))))