Fixup name generation for -fmicrosoft; uppercase type names
Following our discussion, here's a proposed fix for the type names. Please let me know if this works as intended. Thanks!
I tried this out today and it doesn't seem to work for my scenario which involves external types. Consider:
module Test
module B = LowStar.Buffer
assume
val _MY_EXTERNAL_TYPE : Type0
let p_MY_EXTERNAL_TYPE = B.pointer _MY_EXTERNAL_TYPE
let test (x:p_MY_EXTERNAL_TYPE) : bool = true
Extracting this using --codegen krml and then running krml -fmicrosoft -skip-compilation out.krml` produces
/*
This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
KaRaMeL invocation: /home/nswamy/everest/karamel/krml -fmicrosoft -skip-compilation out.krml
F* version: 46cbaf03
KaRaMeL version: d6db69ab
*/
#include "Test.h"
BOOLEAN TestTest(TestMyExternalType *X)
{
return TRUE;
}
I pushed a fix. With your test file, I now get:
/*
This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
KaRaMeL invocation: krml out.krml -skip-compilation -fmicrosoft -d c-names
F* version: ce8b1957
KaRaMeL version: fb04bf2a
*/
#ifndef __Test_H
#define __Test_H
#include "krmllib.h"
typedef TEST__MY_EXTERNAL_TYPE *TEST_P_MY_EXTERNAL_TYPE;
BOOLEAN TestTest(TEST__MY_EXTERNAL_TYPE *X);
#define __Test_H_DEFINED
#endif
is this the desired behavior?
ping @nikswamy @tahina-pro ... should this be merged?
Thanks for this fix. I am merging it after offline discussion with @protz ... much appreciated!