au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Unexpected Recursion in Generated C Code #398

Open gteege opened 3 years ago

gteege commented 3 years ago

The following example code

h: all acc.  (acc -> acc, acc) -> acc
h (f, i) = f i

f1: U32 -> U32
f1 i = i+1

g: U32 -> U32
g i = h[U32](f1, i)

will cause g and h[U32] to be mutually recursive after translation to C. The reason is that g and h[U32] have the same type and thus a common dispatcher function is generated for them and invoked in the C implementation of h.

The effect is that although the C translation fully works, autocorres will fail on the generated C code, since it cannot generate a nonrecursive definition for g and h[U32]. There seems to be no easy solution for this, but at least Cogent programmers should be made aware of this case.