c2ats: Translate C code into ATS

[ gpl, language, library, program ] [ Propose Tags ]

Please see README.md

[Skip to Readme]


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS]
Dependencies base (>=4.6 && <5), c2ats, containers, language-c (>=0.5.0), pretty (>=, regex-posix [details]
License GPL-3.0-only
Copyright 2016 Kiwamu Okabe
Author Kiwamu Okabe
Maintainer kiwamu@debian.or.jp
Category Language
Home page https://github.com/metasepi/c2ats#readme
Source repo head: git clone https://github.com/metasepi/c2ats
Uploaded by KiwamuOkabe at 2016-09-17T12:59:38Z
Executables c2ats
Downloads 892 total (2 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-10-27 [all 1 reports]

Readme for c2ats-

[back to package description]

c2ats - generate ATS interface from C code Build Status

What's this?

ATS is a statically typed programming language that unifies implementation with formal specification. It can powerfully capture invariant in program.

However, don't you feel frustration to use API of many C language libraries from ATS code? Don't you manually import such API into ATS code?

The c2ats is an utility to generate ATS's sats file importing from C language header, semi-automatically.


We are testing this tool on Debian GNU/Linux.


Checkout source code of the c2ats:

$ git clone https://github.com/metasepi/c2ats.git
$ cd c2ats

Then install using cabal:

$ cabal install
$ which c2ats

or install using stack:

$ stack install
$ which c2ats


Start from Hello World example. Create following fake C language header to use printf(3) function in C language:

$ vi example.h
#include <stdio.h>

Next, let the c2ats to generate ATS sats file from above header:

$ c2ats gen example.h > example.sats
$ wc -l example.sats
318 example.sats
$ grep _printf example.sats
fun fun_c2ats_printf: {l1:addr} (!ptr_v_1(char, l1) | ptr l1) -> int = "mac#printf"

The sats file has many ATS declarations generated from the C header. It includes a declaration of printf(3) which can be used as following in dats:

$ vi main.dats
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

staload "example.sats"

fun my_printf (s: string): void = {
  val p = string2ptr s
  val (pfat, fpfat | p) = $UN.ptr_vtake p
  val ret = fun_c2ats_printf (pfat | p)
  prval () = fpfat pfat

implement main0 () = {
  val s = "Hello, world!\n"
  val () = my_printf s
$ patscc main.dats
$ ./a.out
Hello, world!

Of course, above code is so messy. It's caused by assigning a bad signature to fun_c2ats_printf function. You can get better dats code, if modify sats file as following:

$ vi example.sats
fun fun_c2ats_printf: (string) -> int = "mac#printf"
$ vi main.dats
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

staload "example.sats"

implement main0 () = {
  val s = "Hello, world!\n"
  val _ = fun_c2ats_printf s
$ patscc main.dats
$ ./a.out
Hello, world!

Totally, the c2ats generates a scaffold (you may be familiar with Ruby on Rails) to build ATS application. Sometimes, it's useful to create application rapidly. However, such scaffold should be replaced with better signature until shipping your product.

The other examples are found at example directory.


GPLv3 or later.