[racket] How can I unsplice a list of expression into code?

On Sat, Nov 17, 2012 at 10:48 PM, John Clements
<clements at brinckerhoff.org>wrote:

>
> On Nov 16, 2012, at 10:05 PM, Monica Tomson wrote:
>
> > Hi,
> >
> > I have an experiment for my project, basically, I need to embedded some
> s-expression into the code and make it run, like this,
> >
> > (define (test lst)
> >
> >
> > (define num 1)
> >
> >
> > (define l (list))
> >
> >
> > `@lst) ; oh, this is not the right way to go.
> >
> >
> >
> > (define
> >  lst
> >
> > `( (define num2 (add1 num))
> >
> >
> > (displayln num2)))
> > I want the test function be like after test(lst) in racket code:
> >
> > (define (test lst)
> >
> >
> > (define num 1)
> >
> >
> > (define l (list))
> >
> >
> > (define num2 (add1 num)
> >
> >
> > (displayln num2))
> > How can I do this in racket?
>
> I'm following up to your post to include the explanation that you posted
> on StackOverflow:
>
>
> > Update The reason I would like to use eval or the previous questions is
> that I am using Z3 racket binding, I need to generate formulas (which uses
> racket binding APIs), and then I will fire the query at some point, that's
> when I need to evaluate those code. I have not figured out other ways to go
> in my case... One super simple example is, imagine
> > (let ([arr (array-alloc 10)])
> > (array-set! arr 3 4))
> >
> > I have some model to analyze the constructs (so I am not using racketZ3
> directly), during each analyzing point, I will map the data types in the
> program into the Z3 types, and made some assertions, like this:
> >
> > I will generate something like:
> >
> >       • At allocation site, I will need to make the following formula:
> >
> > (smt:declare-fun arr_z3 () IntList)
> > (define len (make-length 10))
> >
> >       • Then at the array set site, I will have the following assertions
> and to check whether the 3 less then the length*
> >
> > (smt:assert (< 3 (smt:eval (len arr_z3))
> > (smt:check-sat)
> >
> >       • Then finally, I will gather the formulas generated as above, and
> wrap them in the form which is able to fire Z3 binding to run the following
> gathered information as code:
> >
> > (smt:with-context
> > (smt:new-context)
> > (define len (make-length 10))
> > (smt:assert (< 3 (smt:eval (len arr_z3))
> > (smt:check-sat))
> >
> > This is the super simple example I can think of... making sense?
> >
>
>
> Ah! are you automatically generating a z3 program from a Racket program?


I am trying to generating a Z3 program from an IR I am analyzing on. the IR
is in a-normalized form, which I compiled from a subset of Python program.


> In this case, it makes perfect sense that you'd be mucking around at the
> syntactic level. In fact, if you want to do the job right, you might want
> to be taking expanded syntax as inputs, rather than s-expressions.


I don't know how to take the expanded syntax as inputs to use Z3 Racket
binding.

I only know S-expression can be easily added, removed etc as I want, so
that's why..


> It sounds like you don't want macros here so much as you want a complete
> syntactic rewrite?
>

kind of, to generate (and manage) the formulas based on my analyzer
information.

Oh, Btw,

Thanks to Mattias tip for another question, I used
the define-namespace-anchor and parameterize current-namespace
with namespace-anchor->namespace, then
I use the nested  (parameterize ((current-namespace (current-namespace)))
to get the Z3 racket binding's namespace, now it is able to prove my
previous super simple example!

  (define-namespace-anchor top)
 (parameterize ((current-namespace (namespace-anchor->namespace top)))
   (eval
   `(smt:with-context
    (smt:new-context )
    (parameterize ((current-namespace (current-namespace)))
      (define len (make-length 10))
      (smt:assert (</s 3 (len (list->z3-list '(42 31 24 19)))))
      (check-eq? (smt:check-sat) 'sat)))))







>
> John Clements
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20121117/39bc4301/attachment.html>