I see.
I would suggest a slight different approach.
Basically, I think that every struct in C should be first mapped to an
abstract type.
Let us take the inode as an example.
absvtype inode_ptr(l:addr) = ptr(l)
For each field in inode, you can generate a get function and a set function.
For instance, imagine that the following functions are generated:
fun inode_get_i_gid{l:agz} (x: !inode_ptr(l)): gid(*type*)
fun inode_set_i_gid{l:agz} (x: !inode_ptr(l), v: gid): void
overload .i_gid with inode_get_i_gid
overload .i_gid with inode_set_i_gid
fun inode_get_i_e2fs_gid{l:agz} (x: !inode_ptr(l)): gid(*type*)
fun inode_set_i_e2fs_gid{l:agz} (x: !inode_ptr(l), v: gid): void
overload .i_gid with inode_get_i_e2fs_gid
overload .i_gid with inode_set_i_e2fs_gid
Then you can write code like:
x.i_gid(x.i_e2fs_gid()) // for x->i_gid = x.i_e2fs_gid
At the beginning, please don't try to do too much. Once you have gathered
enough experience, you can start to generate functions with more informative
types. As always, please try to find a good naming scheme to name the
generated
functions.
Also, there is no need to start with C syntax. You can (and probably
should) start
with some syntax of your design and then later find a way to translate C
syntax into
your designed syntax. I call this doing-things-in-stages. Trying to do a
complex thing
in one step usually ends up with a failure and some frustration.
On Mon, Aug 22, 2016 at 12:52 AM, Kiwamu Okabe <[email protected]> wrote:
> Hi Hongwei,
>
> On Mon, Aug 22, 2016 at 1:24 PM, gmhwxi <[email protected]> wrote:
> > As I see it, compiling C into ATS is very meaningful but also very
> > challenging. At this point, it is still unclear to me what your primary
> > objective is for compiling C into ATS. It would definitely help if you
> > could present some (potential) use cases.
>
> In the past, I create a tool translating Haskell into C, such like c2ats:
>
> https://github.com/ajhc/struct2hs
>
> With the tool, I can partly rewrite NetBSD kernel:
>
> https://github.com/metasepi/netbsd-arafura-s1/tree/
> arafura-s1/metasepi/sys/hssrc
>
> The Haskell code imports many C language interface, translated by
> struct2hs tool:
>
> Today, I would like to rewrite NetBSD kernel using ATS language with
> same method.
> I think the method will be like following:
>
> $1. Choose a .c file in NetBSD kernel to rewrite.
> Let's choose
> https://github.com/IIJ-NetBSD/netbsd-src/blob/master/sys/
> ufs/ext2fs/ext2fs_vfsops.c.
> $2. Translate C interface into ATS .sats file using c2ats tool,
> semi-automatically.
> It should make many many .sats files in output directory.
> $3. Create ext2fs_vfsops.dats file include ext2fs_vfsops.c with "%{"
> declaration and staload .sats files created by $2.
> And check the ext2fs_vfsops.dats file is ready to be compiled.
> $4. Rewrite a function in ext2fs_vfsops.dats file using some types in
> .sats files.
> $5. Do refactoring the ATS function. Sometimes I'll rewrite typedef in
> .sats with dataview.
> $6. ...
>
> I would like to choose a method to rewrite C code with ATS,
> ***incrementally***.
>
> Best regards,
> --
> Kiwamu Okabe at METASEPI DESIGN
>
> --
> You received this message because you are subscribed to the Google Groups
> "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To post to this group, send email to [email protected].
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit https://groups.google.com/d/
> msgid/ats-lang-users/CAEvX6d%3DZ8zVncN43c8rNrCBb%
> 3D9qPDxLBxhzZzEJ%2BsdZbnTTRwg%40mail.gmail.com.
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpM97-i%3DjKdx8BUzY%3DoxCAaSshtTziXBH1%2BsRyPZFM4BQ%40mail.gmail.com.