karamel icon indicating copy to clipboard operation
karamel copied to clipboard

Fixup name generation for -fmicrosoft; uppercase type names

Open msprotz opened this issue 3 years ago • 2 comments

Following our discussion, here's a proposed fix for the type names. Please let me know if this works as intended. Thanks!

msprotz avatar Mar 15 '22 17:03 msprotz

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;
}

nikswamy avatar Mar 30 '22 17:03 nikswamy

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?

msprotz avatar Apr 21 '22 17:04 msprotz

ping @nikswamy @tahina-pro ... should this be merged?

msprotz avatar Oct 13 '22 17:10 msprotz

Thanks for this fix. I am merging it after offline discussion with @protz ... much appreciated!

nikswamy avatar Feb 07 '23 23:02 nikswamy