A quick-and-dirty POC of writing C++ with alloy

Alloy/C/ExternDef.lean

@@ -92,3 +92,41 @@ scoped elab (name := externDecl) doc?:(docComment)?
   )
   let cmd ← `(alloy c section $fn:function end)
   withMacroExpansion (← getRef) cmd <| elabCommand cmd
+
+
+scoped syntax (name := leanCppExport) "extern \"C\"" : cDeclSpec
+
+scoped elab (name := externCppDecl) doc?:(docComment)?
+"alloy " &"cpp " ex:&"extern " sym?:(str)? attrs?:(Term.attributes)?
+"def " id:declId bx:binders " : " type:term " := " body:cStmt : command => do
+
+  -- Lean Definition
+  let name := (← getCurrNamespace) ++ id.raw[0].getId
+  let (symLit, extSym) :=
+    match sym? with
+    | some sym => (sym, sym.getString)
+    | none =>
+      let extSym := "_alloy_c_" ++ name.mangle
+      (Syntax.mkStrLit extSym <| SourceInfo.fromRef id, extSym)
+  let attr ← withRef ex `(Term.attrInstance| extern $symLit:str)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  let bs := bx.raw.getArgs.map (⟨.⟩)
+  let cmd ← `($[$doc?]? @[$attrs,*] opaque $id $[$bs]* : $type)
+  withMacroExpansion (← getRef) cmd <| elabCommand cmd
+
+  -- C Definition
+  let env ← getEnv
+  let some info := env.find? name
+    | throwError "failed to find Lean definition"
+  let some decl := IR.findEnvDecl env name
+    | throwError "failed to find Lean IR definition"
+  let bvs ← liftMacroM <| bs.concatMapM matchBinder
+  let id := mkIdentFrom symLit (Name.mkSimple extSym)
+  let ty ← liftMacroM <| withRef type <| expandIrResultTypeToC false decl.resultType
+  let params ← liftMacroM <| mkParams info.type bvs decl.params
+  let body := packBody body
+  let fn ← MonadRef.withRef Syntax.missing <| `(function|
+    extern "C" LEAN_EXPORT%$ex $ty:cTypeSpec $id:ident($params:params) $body:compStmt
+  )
+  let cmd ← `(alloy c section $fn:function end)
+  withMacroExpansion (← getRef) cmd <| elabCommand cmd

Alloy/C/Grammar.lean

@@ -263,6 +263,32 @@ A C [functional call][1] expression.
 -/
 syntax:1000 cExpr:1000 "(" cExpr,* ")" : cExpr
 
+/--
+
+A C++ [new][1] expression.
+
+[1]: https://en.cppreference.com/w/cpp/language/new
+
+Supports only: `new S`.
+
+TODO: Move to Cpp module, and include all new variants.
+
+-/
+syntax:1000 "new" type : cExpr
+
+/--
+
+A C++ [delete][1] expression.
+
+[1]: https://en.cppreference.com/w/cpp/language/delete
+
+Supports only: `delete (S*)ptr`.
+
+TODO: Move to Cpp module, and include all delete variants.
+
+-/
+syntax:1000 "delete" cExpr:1000 : cExpr
+
 /--
 A C [member access][1] expression.
 

examples/Cpp/Cpp.lean

@@ -0,0 +1,97 @@
+import Alloy.C
+open scoped Alloy.C
+
+/-!
+# `Cpp.lean`
+
+An adaption of Lean 4's ['foreign'][1] example for Alloy.
+
+[1]: https://github.com/leanprover/lean4/tree/b278a20ac22adcbfde11db386f2dc874d4a215ad/tests/compiler/foreign
+-/
+
+alloy c include <stdint.h> <stdlib.h> <string.h> <lean/lean.h> <string>
+
+--------------------------------------------------------------------------------
+/-! ## Definition of S                                                      -/
+--------------------------------------------------------------------------------
+
+alloy c section
+
+typedef struct {
+  uint32_t      m_x;
+  uint32_t      m_y;
+  lean_object * m_s;
+} S;
+
+static void S_finalize(void* ptr) {
+  lean_dec(((S*)ptr)->m_s);
+  delete (S*)ptr;
+}
+
+static void S_foreach(void* ptr, b_lean_obj_arg f) {
+  lean_apply_1(f, ((S*)ptr)->m_s);
+}
+
+static S g_s = {0, 0, NULL};
+
+end
+
+alloy c extern_type S => S := {
+  foreach := `S_foreach
+  finalize := `S_finalize
+}
+
+--------------------------------------------------------------------------------
+/-! ## Lean Interface                                                         -/
+--------------------------------------------------------------------------------
+
+alloy cpp extern "lean_mk_S"
+def mkS (x y : UInt32) (string : String) : S := {
+  S* s = new S;
+  s->m_x = x;
+  s->m_y = y;
+  s->m_s = string;
+  return to_lean<S>(s);
+}
+
+-- alloy c extern "lean_S_add_x_y"
+-- def S.addXY (s : @& S) : UInt32 := {
+--   return of_lean<S>(s)->m_x + of_lean<S>(s)->m_y;
+-- }
+
+alloy cpp extern "lean_S_string"
+def S.string (s : @& S) : String := {
+  lean_inc(of_lean<S>(s)->m_s);
+  return of_lean<S>(s)->m_s;
+}
+
+-- alloy c extern "lean_S_global_append"
+-- def appendToGlobalS (string : String) : BaseIO PUnit := {
+--   if (g_s.m_s == NULL) {
+--     g_s.m_s = string;
+--   } else {
+--     g_s.m_s = lean_string_append(g_s.m_s, string);
+--   }
+--   return lean_io_result_mk_ok(lean_box(0));
+-- }
+
+-- alloy c extern "lean_S_global_string"
+-- def getGlobalString : BaseIO String := {
+--   if (g_s.m_s == NULL) {
+--     g_s.m_s = lean_mk_string("");
+--   }
+--   lean_inc(g_s.m_s);
+--   return lean_io_result_mk_ok(g_s.m_s);
+-- }
+
+-- alloy c extern "lean_S_update_global"
+-- def updateGlobalS (s : @& S) : BaseIO Unit := {
+--   if (g_s.m_s != NULL) {
+--     lean_dec(g_s.m_s);
+--   }
+--   lean_inc(of_lean<S>(s)->m_s);
+--   g_s.m_x = of_lean<S>(s)->m_x;
+--   g_s.m_y = of_lean<S>(s)->m_y;
+--   g_s.m_s = of_lean<S>(s)->m_s;
+--   return lean_io_result_mk_ok(lean_box(0));
+-- }

examples/Cpp/Main.lean

@@ -1,4 +1,6 @@
-import S
+-- This file is unmodified and unused. Check Test.lean for now.
+
+import Cpp
 
 def main : IO Unit := do
   IO.println (mkS 10 20 "hello").addXY

examples/Cpp/Test.lean

@@ -1,17 +1,17 @@
-import S
+import Cpp
 
-#eval show IO _ from do
-  getGlobalString >>= IO.println
+-- #eval show IO _ from do
+--   getGlobalString >>= IO.println
 
 #eval show IO _ from do
-  IO.println (mkS 10 20 "hello").addXY
   IO.println (mkS 10 20 "hello").string
-  updateGlobalS (mkS 0 0 "")
-  appendToGlobalS "foo"
-  appendToGlobalS "bla"
-  getGlobalString >>= IO.println
-  updateGlobalS (mkS 0 0 "world")
-  getGlobalString >>= IO.println
+--   IO.println (mkS 10 20 "hello").string
+--   updateGlobalS (mkS 0 0 "")
+--   appendToGlobalS "foo"
+--   appendToGlobalS "bla"
+--   getGlobalString >>= IO.println
+--   updateGlobalS (mkS 0 0 "world")
+--   getGlobalString >>= IO.println
 
-#eval show IO _ from do
-  getGlobalString >>= IO.println
+-- #eval show IO _ from do
+--   getGlobalString >>= IO.println

examples/Cpp/lakefile.lean

@@ -1,21 +1,28 @@
 import Lake
 open Lake DSL
 
-package s {
+package Cpp where
   buildType := .debug
-}
+  precompileModules := true
+  moreLinkArgs := #[s!"-L{__dir__}/build/lib",
+    "-lstdc++"] -- "-v",  --, "-lc++", "-lc++abi", "-lunwind"] -- "-lstdc++"]
+  weakLeanArgs := #[
+    -- s!"--load-dynlib={__dir__}/build/lib/" ++ nameToSharedLib "xxx",
+  ]
 
 require alloy from ".."/".."
 
-module_data alloy.c.o : BuildJob FilePath
-lean_lib S {
+module_data alloy.cpp.o : BuildJob FilePath
+lean_lib Cpp {
   precompileModules := true
-  nativeFacets := #[Module.oFacet, `alloy.c.o]
+  nativeFacets := #[Module.oFacet, `alloy.cpp.o]
 }
 
-@[default_target]
-lean_exe s {
-  root := `Main
-}
+-- @[default_target]
+-- lean_exe alloycpp {
+--   root := `Main
+-- }
+
+-- For now, test with `lake -R build Test -v`
 
 lean_lib Test

lakefile.lean

@@ -45,3 +45,25 @@ module_facet alloy.c.o mod : FilePath := do
   let cJob ← fetch <| mod.facet `alloy.c
   let weakArgs := #["-I", (← getLeanIncludeDir).toString]
   buildO s!"{mod.name} alloy" oFile cJob weakArgs mod.leancArgs "cc"
+
+module_facet alloy.cpp mod : FilePath := do
+  let exeJob ← alloy.fetch
+  let modJob ← mod.olean.fetch
+  let cppFile := mod.irPath "alloy.cpp"
+  exeJob.bindAsync fun exeFile exeTrace => do
+  modJob.bindSync fun _ modTrace => do
+    let depTrace := exeTrace.mix modTrace
+    let trace ← buildFileUnlessUpToDate cppFile depTrace do
+      logStep s!"Generating {mod.name} alloy"
+      proc {
+        cmd := exeFile.toString
+        args := #[mod.name.toString, cppFile.toString]
+        env := #[("LEAN_PATH", (← getLeanPath).toString)]
+      }
+    return (cppFile, trace)
+
+module_facet alloy.cpp.o mod : FilePath := do
+  let oFile := mod.irPath "alloy.cpp.o"
+  let cJob ← fetch <| mod.facet `alloy.cpp
+  let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-v"]
+  buildO s!"{mod.name} alloy" oFile cJob weakArgs mod.leancArgs "clang++"