Serialization of Coq's types.

[ejgallego]

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]

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]

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]

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]

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 < ***@***.***> 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 <#44 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdNjiVNrW4ctexELHDe-CXrtIu0n7Tzks5u2eMbgaJpZM4ZHq7v> .

[ejgallego]

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