You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The current C89 backend (#671) is semantics-preserving and quite fast (as fast as native OCaml without GC allocations) thanks to @AltGr. However, the code it generates is not very idiomatic and might be difficult to adopt by people that really want a C they can read and modify (https://jonathan.protzenko.fr/2019/01/04/behind-the-scenes.html). Thus, we might want to relax semantics-preservation (slightly) in favor of generating C code that looks like man-made. This could be done in an alternative C89 backend that I would qualify as "idiomatic". The gist of the idiomatic backend is that it should use builtin types and avoid boxing at all costs.
To achieve this objective, the following changes are needed from the current C89 backend :
stop using GMP and model integers as long long int and decimals as double ;
minimize closure lifting by matching collection operations early and turning them into for loops ;
layout structs and enums in a flat fashion (no boxing)
pipe Scalc to one of the intermediate representations of https://github.com/FStarLang/karamel/, and apply Karamel's optimization passes and pretty-printing capabilities (thanks @protz !).
The text was updated successfully, but these errors were encountered:
The current C89 backend (#671) is semantics-preserving and quite fast (as fast as native OCaml without GC allocations) thanks to @AltGr. However, the code it generates is not very idiomatic and might be difficult to adopt by people that really want a C they can read and modify (https://jonathan.protzenko.fr/2019/01/04/behind-the-scenes.html). Thus, we might want to relax semantics-preservation (slightly) in favor of generating C code that looks like man-made. This could be done in an alternative C89 backend that I would qualify as "idiomatic". The gist of the idiomatic backend is that it should use builtin types and avoid boxing at all costs.
To achieve this objective, the following changes are needed from the current C89 backend :
long long int
and decimals asdouble
;for
loops ;The text was updated successfully, but these errors were encountered: