Fix "no #%datum syntax transformer is bound" bug when run tests in a Racket module

[chansey97]

The current codebase supports Racket, but only in REPL.

If running in a module, it will crash.

For example,

Suppose I'd like some compatible patches (for both Racket and Scheme) via include, I may write the following code:

test-check.rkt

#lang racket/base
(require racket/include)
(provide test time-test todo)
(include "test-check.scm")

clpsmt-basic-tests.rkt

#lang racket/base
(require racket/include)
(require "mk.rkt")
(require "test-check.rkt")
(include "clpsmt-basic-tests.scm")

Then you can click clpsmt-basic-tests.rkt (I use windows) to open DrRacket and Run.

But that will fail, DrRacket complains:

?: literal data is not allowed;
 no #%datum syntax transformer is bound in: 0

The root cause is that the read-model in z3-driver.rkt uses eval but no namespace passed. It can work well in REPL, but not in a module, see https://docs.racket-lang.org/guide/eval.html#%28part._namespaces%29.

This patch can fix this problem and make the above compatible patches work.

BTW, do you need these Racket compatible patches? i.e. test-check.rkt, clpsmt-basic-tests.rkt, etc. I can create a new pull-request. (I currently use these Racket compatible patches in my local codebase, because it is convenient to debug in DrRacket).

[namin]

Thanks!

We should find a way to not duplicate z3-server.rkt and z3-server.scm so much, etc. The way faster-miniKanren is setup for both rkt and scm is an example.

And yes, I'd be happy to take your rkt wrappers if you want to do a pull request.

Thanks, again!

[chansey97]

We should find a way to not duplicate z3-server.rkt and z3-server.scm so much, etc. The way faster-miniKanren is setup for both rkt and scm is an example.

Yes, I agree.

Actually, I have just made a patch for this. (But before that there are other patches to commit.)

In addition to z3, I observed that this project can also use cvc4 or yices as a SMT backend.

Current codebase is just hardcode z3 in mk.rkt.

mk.rkt

#lang racket/base
...

(include "z3-driver.rkt")

Ideally, user should be able to switch between different SMT backends.

In Scheme, it is easy (and rough):

test-code.scm

(load "z3-driver.scm") ; if you want cvc4, just replace it with (load "cv4-driver.scm") 
(load "mk.scm")

;; test code here

In Racket, we can use include or load to simulate, but it is obviously not a good solution.

We should find a way to switch SMT backends in Racket, e.g. unit-system, parameters, generics, oop, di-container, etc. (may create a new issue to discuss?)

[namin]

Why is using include or load not a good solution in Racket?

Sure, feel free to open a new issue.

Thanks.

[chansey97]

In fact, the solution I currently used is using include.

However, in general include or load is not a best practice in Racket, see https://gist.github.com/samth/3083053. Perhaps it is an exception when we want to compatible both Racket and Scheme? (Frankly, I have never written Racket code like this...) This is why I'd like to discuss.

Anyway, I will give you a pull request to review.

[namin]

It's what faster-miniKanren does, so I think it's OK.

Thanks.