max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/compiler/ir/emitcpp): small hack for exporting functions as C functions instead of C++

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-16 19:26:03 -07:00
parent 2758681d78
commit 8a3522c8e5
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -125,10 +125,20 @@ do env ← getEnv;
def emitCppInitName (n : Name) : M Unit :=
toCppInitName n >>= emit
def isSimpleExportName (n : Name) : M Bool :=
do env ← getEnv;
match getExportNameFor env n with
| some (Name.mkString Name.anonymous s) => pure true
| _ => pure false
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit :=
do
let ps := decl.params;
when (ps.isEmpty && addExternForConsts) (emit "extern ");
if ps.isEmpty && addExternForConsts then
emit "extern "
else
-- Temporary hack for transitioning to C
mwhen (isSimpleExportName decl.name) (emit "extern \"C\" ");
emit (toCppType decl.resultType ++ " " ++ cppBaseName);
unless (ps.isEmpty) $ do {
emit "(";