search

Ptival / PeaCoq

PeaCoq is a pretty Coq, isn't it?
http://goto.ucsd.edu/peacoq
MIT License
106 stars 10 forks source link

Serialization of Coq's types. #44

Open ejgallego opened 5 years ago

ejgallego commented 5 years ago

This is just a suggestion, but IMHO it would make sense to implement a small Coq program that given an OCaml type [for example, constr_expr , the Coq's AST] would generate the corresponding .ts file, including constructors from sexp.

IMHO that should save a lot of time; but maybe you are using already some other automatic method.

Ptival commented 5 years ago

I agree. I wrote them manually because I had to get things going fast and dirty, but it's neither pleasant nor manageable.

Now that OCaml has ppx extensions, I wonder how hard it'd be to have it use this mechanism to do it? Or do you have any technical suggestion on how to achieve this? I'd love to generate those automatically.

ejgallego commented 5 years ago

It should be "fairly easy", I am a bit busy right now but I would start from already existing projects that do similar things; basically you do a traversal on the AST and that is.

I am interesting doing this for both Python and TS, so keep me posted if you start something, if I do I'll ping you here too.

ejgallego commented 5 years ago

Actually ppx is not even needed, we just a program that uses compiler-libs. Then, the basic scheme is very simple IMO:

let ast = Parse.interface foo in 
let typ_list = Ast_iterator that build the right type list in
output (convert typ_list)
Ptival commented 5 years ago

I can look into it, I just graduated so I have a lot of free time for about a month.

On Thu, Dec 6, 2018, 19:40 Emilio Jesús Gallego Arias < notifications@github.com> wrote:

Actually ppx is not even needed, we just a program that uses compiler-libs. Then, the basic scheme is very simple IMO:

let ast = Parse.interface foo in let typ_list = Ast_iterator that build the right type list in

output (convert typ_list)

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/Ptival/PeaCoq/issues/44#issuecomment-445112906, or mute the thread https://github.com/notifications/unsubscribe-auth/AAdNjiVNrW4ctexELHDe-CXrtIu0n7Tzks5u2eMbgaJpZM4ZHq7v .

ejgallego commented 5 years ago

Hey congrats @Ptival !! I guess you'll have way better things to do than to hack OCaml.

Anyways I actually wrote already a very small shim, find it here at https://github.com/ejgallego/ocaml-ts