Does Cosette support using expressions in Select about cosette HOT 9 CLOSED

I think the actual question here is: do we support using expression in projection.

Currently our parser supports that, and the rosette backend supports that. The coq backend can treat "+" in the projection as an uninterpreted function, but we need to add some extra transformation in the parser to make the compilation to coq (expression in projection) work.

@xuruiyang can you provide an example of queries that you want to prove?

from cosette.

I don't have two queries for comparison for the time being. But I'm actually considering on something like the following query:

SELECT Product.unit_price * Product.num WHERE Product.unit_price > 10.

And I'm interested in writing down this in form of HoTTSQL ( more specifically, something like in your racket test files) and running it with (run query).

I guess that I need to write my own Aggregation functions to implement this projection in VALS clause, right?

from cosette.

@xuruiyang this does not looks like an aggregation function to me. you just need to define a uninterpreted function takes the type unit_price and num in coq.

from cosette.

To my understanding, only the interactive proof part (Coq) of your system can handle this kind of queries. But the automatic proof part (Rosette) can't handle such kind of queries. Am I right?

from cosette.

@xuruiyang I think both parts can handle that. Compiling cosette DSL to coq need some extra work, but not much.

from cosette.

Would you mind to give me an example of how to use the CosetteParser as well as the ToRosette parser? Since I didn't see any further instructions on how to use them (except the ones on how to run test cases), are you still developing them?

from cosette.

@xuruiyang we will update the instruction soon. Also the initial release is on the way. Stay tuned!

from cosette.

@xuruiyang I invited you to the gitter chatroom of cosette. Feel free to ask us anything on gitter, too.

from cosette.

@xuruiyang we fully support expressions in frontend and all backends now (both Coq and Rosette). We are going to release the first beta version of Cosette soon!

from cosette.