A toy translator C to ATS

Table of contents

• TL;DR
• Why difficult to make real products in ATS language?
• Why is c2ats not useful?
• Let’s start to create new translator C to ATS
• How to install
• Some examples
  • while loop in C
  • for loop in C
  • the others
• Next?
• Acknowledgements

TL;DR

We can translate a simple for and while loop in C language into a recursive function in ATS language, using the idiomaticca tool.

Why difficult to make real products in ATS language?

We believe ATS language is a better choice than C language. Because it can:

• prove simple invariant,
• safely use pointer,
• support some rich types such as tuple,
• support template,

But there are following barriers to make real products in ATS:

1. Hard to learn ATS language.
2. Hard to reuse existing programs and libraries written in C.

Why is c2ats not useful?

We have already create c2ats to fix above barriers. But people should write own ATS code side of existing C code, because the c2ats only translate C function signature into ATS. It can’t translate C function body.

Please imagine that someone tries to translate a file system driver using c2ats:

1. Choose target files to be translated.
2. Translate headers included by the target files into ATS using c2ats.
3. Manually re-write the target files by ATS

Undoubtedly, the step 3 requires more man-hours, and is sometimes unrealistic.

Let’s start to create new translator C to ATS

If so, how about translate both function signature and function body into ATS? The translator may fix:

• the barrier 1, because programmer learn ATS with codes translated from their C code,
• the barrier 2, because manually re-writing is not needed.

Of course, we know it seems like a crazy attempt. Let’s try to create a toy translator C to ATS. We call it idiomaticca.

How to install

$ git clone https://github.com/metasepi/idiomaticca.git -b v0.1.0.0
$ cd idiomaticca
$ make install
$ which idiomaticca
/home/YourName/.local/bin/idiomaticca

Some examples

while loop in C

$ vi loop_while.c

int fib(int n) {
	int f0 = 0, f1 = 1;

	while (n-- > 0) {
		int tmp = f1;
		f1 = f0 + f1;
		f0 = tmp;
	}

	return f0;
}

int main() {
	return fib(10);
}

$ gcc loop_while.c
$ ./a.out
$ echo $?
55
$ idiomaticca trans loop_while.c > loop_while.dats
$ cat loop_while.dats

#include "share/atspre_staload.hats"

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

fun fib(n : int) : int =
 let
 var n: int = n
 in
 let
 var f0: int = 0
 var f1: int = 1
 
 fun loop_while(f0 : int, f1 : int, n : int) : (int, int, int) =
 let
 var f0: int = f0
 var f1: int = f1
 var n: int = n
 in
 if n > 0 then
 let
 val () = n := n - 1
 var tmp: int = f1
 val () = f1 := f0 + f1
 val () = f0 := tmp
 in
 loop_while(f0, f1, n)
 end
 else
 (f0, f1, n)
 end
 
 val (i9a_f0, i9a_f1, i9a_n) = loop_while(f0, f1, n)
 val () = f0 := i9a_f0
 val () = f1 := i9a_f1
 val () = n := i9a_n
 in
 f0
 end
 end

implement main () =
 fib(10)

$ patscc loop_while.dats
$ ./a.out
$ echo $?
55

for loop in C

$ vi loop_for.c

int sum(int n) {
	int i, sum = 0;

	for (i = 1; i <= n; i++) {
		sum = sum + i;
	}

	return sum;
}

int main() {
	return sum(5);
}

$ gcc loop_for.c
$ ./a.out
$ echo $?
15
$ idiomaticca trans loop_for.c > loop_for.dats
$ cat loop_for.dats

#include "share/atspre_staload.hats"

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

fun sum(n : int) : int =
 let
 var n: int = n
 in
 let
 var i: int
 var sum: int = 0

 fun loop_for(i : int, n : int, sum : int) : (int, int, int) =
 let
 var i: int = i
 var n: int = n
 var sum: int = sum
 in
 if i <= n then
 let
 val () = sum := sum + i
 val () = i := i + 1
 in
 loop_for(i, n, sum)
 end
 else
 (i, n, sum)
 end

 val () = i := 1
 val (i9a_i, i9a_n, i9a_sum) = loop_for(i, n, sum)
 val () = i := i9a_i
 val () = n := i9a_n
 val () = sum := i9a_sum
 in
 sum
 end
 end

implement main () =
 sum(5)

$ patscc loop_for.dats
$ ./a.out
$ echo $?
15

the others

Please see regress tests.

Next?

• Support break, continue, and goto. (Should use some kind of CFG?)
• Support pointers using at-view.
• Support C headers using .sats files.
• Use val instead of var.
• Simplify ATS code. Example: reduce multiple let.
• Support ATS3.
• And more...

Acknowledgements

• This translator is inspired by Jamey Sharp’s Corrode translator.
• This translator is using Vanessa McHale’s language-ats library.

Please enable JavaScript to view the comments powered by Disqus. blog comments powered by Disqus