#657 wrongly mangles enum values under bundles #674
Description
Consider the following two F* modules:
module Base
type test = | Foo | Bar
let f (x: Base.test) : Tot bool = Base.Foo? x
module Derived
let g (x: bool) : Tot bool = Base.f Base.Foo = xThen, after verifying and extracting them to .krml, I run Karamel to extract them to C with:
krml Base.krml Derived.krml -bundle Derived=Base -skip-linking
As expected, Karamel produces one single C file, Derived.c.
But then, the C compiler cannot compile it, and produces the following error:
./Derived.c: In function ‘uu___is_Foo’:
./Derived.c:19:10: error: ‘Base_Foo’ undeclared (first use in this function)
19 | case Base_Foo:
| ^~~~~~~~
./Derived.c:19:10: note: each undeclared identifier is reported only once for each function it appears in
At top level:
cc1: note: unrecognized command-line option ‘-Wno-unknown-warning-option’ may have been intended to silence earlier diagnostics
Warning 3: run_or_warn: the following command failed:
cc -I /home/tahina/everest/karamel/krmllib/dist/minimal -I /home/tahina/everest/karamel/krmllib -I /home/tahina/everest/karamel/include -I . -Wall -Werror -Wno-unknown-warning-option -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./Derived.c -o ./Derived.o
Warning 3 is fatal, exiting.
Here is the beginning of the contents of Derived.c as produced by Karamel:
#include "Derived.h"
#define Foo 0
#define Bar 1
typedef uint8_t test;
static bool uu___is_Foo(test projectee)
{
switch (projectee)
{
case Base_Foo:
{
return true;
}
default:
{
return false;
}
}
}
// ...Karamel produces unmangled Foo and Bar constructors, but them the corresponding destructor is_Foo expects mangled constructors, which is wrong.
I reproduced this bug with Karamel b6df0cc (latest master as of today) and 46bbe26 (merging #657).
With Karamel d94f846 (just before merging #657), Karamel generates a destructor expecting an unmangled constructor, as expected.