I am looking to write a DSL in Rosette with the goal of synthesizing a function. The DSL is based off a very small subset of Haskell, and is strongly typed. I therefore want to make sure that anything that Rosette generates is well-typed.
One way I could consider going about this is writing a "is-well-typed-code" function (that's something I've already done in Julia, which I'm porting from), and then assert that it must hold true of the synthesized function. However, I do not see with define-synthax and synthesize how to view the code both as a syntactic object (i.e., an S-expr that can have any function applied to it) and as a semantic function when synthesizing.
I could also imagine using a cond inside the define-synthax module over all possible types of the arguments (this is a finite set for this small DSL), and defining the possible forms separately for each type. However, including conds inside define-synthax does not seem to be possible.
Any ideas?
Thanks!