<br><br><div class="gmail_quote">On Sat, Nov 17, 2012 at 10:48 PM, John Clements <span dir="ltr"><<a href="mailto:clements@brinckerhoff.org" target="_blank">clements@brinckerhoff.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="HOEnZb"><div class="h5"><br> On Nov 16, 2012, at 10:05 PM, Monica Tomson wrote:<br> <br> > Hi,<br> ><br> > I have an experiment for my project, basically, I need to embedded some s-expression into the code and make it run, like this,<br> ><br> > (define (test lst)<br> ><br> ><br> > (define num 1)<br> ><br> ><br> > (define l (list))<br> ><br> ><br> > `@lst) ; oh, this is not the right way to go.<br> ><br> ><br> ><br> > (define<br> > lst<br> ><br> > `( (define num2 (add1 num))<br> ><br> ><br> > (displayln num2)))<br> > I want the test function be like after test(lst) in racket code:<br> ><br> > (define (test lst)<br> ><br> ><br> > (define num 1)<br> ><br> ><br> > (define l (list))<br> ><br> ><br> > (define num2 (add1 num)<br> ><br> ><br> > (displayln num2))<br> > How can I do this in racket?<br> <br> </div></div>I'm following up to your post to include the explanation that you posted on StackOverflow:<br> <br> <br> > 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<br> > (let ([arr (array-alloc 10)])<br> > (array-set! arr 3 4))<br> ><br> > 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:<br> ><br> > I will generate something like:<br> ><br> > • At allocation site, I will need to make the following formula:<br> ><br> > (smt:declare-fun arr_z3 () IntList)<br> > (define len (make-length 10))<br> ><br> > • Then at the array set site, I will have the following assertions and to check whether the 3 less then the length*<br> ><br> > (smt:assert (< 3 (smt:eval (len arr_z3))<br> > (smt:check-sat)<br> ><br> > • 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:<br> ><br> > (smt:with-context<br> > (smt:new-context)<br> > (define len (make-length 10))<br> > (smt:assert (< 3 (smt:eval (len arr_z3))<br> > (smt:check-sat))<br> ><br> > This is the super simple example I can think of... making sense?<br> ><br> <br> <br> Ah! are you automatically generating a z3 program from a Racket program? </blockquote><div><br></div><div>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. </div> <div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.</blockquote> <div><br></div><div>I don't know how to take the expanded syntax as inputs to use Z3 Racket binding. </div><div><br></div><div>I only know S-expression can be easily added, removed etc as I want, so that's why..</div> <div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It sounds like you don't want macros here so much as you want a complete syntactic rewrite?<br></blockquote> <div><br></div><div>kind of, to generate (and manage) the formulas based on my analyzer information. </div><div><br></div><div>Oh, Btw, </div><div><br></div><div>Thanks to Mattias tip for another question, I used the define-namespace-anchor and parameterize current-namespace with namespace-anchor->namespace, then </div> <div>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! </div><div><br></div><div><div><div> (define-namespace-anchor top)</div> <div> (parameterize ((current-namespace (namespace-anchor->namespace top)))</div><div> (eval </div><div> `(smt:with-context</div><div> (smt:new-context )</div><div> (parameterize ((current-namespace (current-namespace)))</div> <div> (define len (make-length 10))</div><div> (smt:assert (</s 3 (len (list->z3-list '(42 31 24 19)))))</div><div> (check-eq? (smt:check-sat) 'sat)))))</div></div></div><div><br></div><div><br> </div><div><br></div><div><br></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <span class="HOEnZb"><font color="#888888"><br> John Clements<br> <br> <br> <br> </font></span></blockquote></div><br>