Add macroDefinition cursor kind, flags param for parseTranslationUnit, and evaluateCursor

LeanLibclang/Basic.lean

@@ -44,11 +44,14 @@ opaque createIndex (excludeDeclsFromPCH : Bool)
                    (displayDiagnostics : Bool) : IO Index
 
 /-- Parse a source file into a translation unit.
-    `args` are extra command-line arguments passed to clang (e.g. `#["-std=c11"]`). -/
+    `args` are extra command-line arguments passed to clang (e.g. `#["-std=c11"]`).
+    `flags` is a bitmask of `CXTranslationUnit_Flags` values (0 = none).
+    Pass `1` for `CXTranslationUnit_DetailedPreprocessingRecord` to expose macro cursors. -/
 @[extern "lean_clang_parseTranslationUnit"]
 opaque parseTranslationUnit (idx : @& Index)
                              (filename : @& String)
-                             (args : @& Array String) : IO TranslationUnit
+                             (args : @& Array String)
+                             (flags : UInt32 := 0) : IO TranslationUnit
 
 /-- Get the root cursor of a translation unit. -/
 @[extern "lean_clang_getTranslationUnitCursor"]
@@ -113,6 +116,11 @@ opaque getCursorResultTypeSpelling (cursor : @& Cursor) : IO String
 @[extern "lean_clang_getCursorEnumConstantValue"]
 opaque getCursorEnumConstantValue (cursor : @& Cursor) : IO Int64
 
+/-- Evaluate a cursor's expression and return the integer result, or `none`
+    if the cursor is not an integer-valued macro or expression. -/
+@[extern "lean_clang_evaluateCursor"]
+opaque evaluateCursor (cursor : @& Cursor) : IO (Option Int64)
+
 /-- Get the unsigned integer value of an `enumConstantDecl` cursor. -/
 @[extern "lean_clang_getCursorEnumConstantUValue"]
 opaque getCursorEnumConstantUValue (cursor : @& Cursor) : IO UInt64

LeanLibclang/CursorKind.lean

@@ -62,6 +62,9 @@ inductive CursorKind where
   | declStmt             -- 231
   -- Translation unit
   | translationUnit      -- 350 (CXCursor_TranslationUnit = 300)
+  -- Preprocessor
+  | macroDefinition      -- 501
+  | macroExpansion       -- 502
   -- Other
   | other (raw : UInt32)
   deriving Repr, BEq, Inhabited
@@ -120,6 +123,8 @@ def ofRaw (n : UInt32) : CursorKind :=
   | 214 => .returnStmt
   | 231 => .declStmt
   | 350 => .translationUnit
+  | 501 => .macroDefinition
+  | 502 => .macroExpansion
   | n   => .other n
 
 instance : ToString CursorKind where

c/clang_shim.c

@@ -115,6 +115,7 @@ Translation unit
 lean_obj_res lean_clang_parseTranslationUnit(lean_obj_arg idx,
                                               lean_obj_arg filename,
                                               lean_obj_arg args,
+                                              uint32_t flags,
                                               lean_obj_arg world) {
     CXIndex cxIdx = (CXIndex)lean_get_external_data(idx);
     const char *fname = lean_string_cstr(filename);
@@ -131,7 +132,7 @@ lean_obj_res lean_clang_parseTranslationUnit(lean_obj_arg idx,
 
     CXTranslationUnit tu = clang_parseTranslationUnit(
         cxIdx, fname, cargs, (int)nargs, NULL, 0,
-        CXTranslationUnit_None);
+        (unsigned)flags);
 
     if (cargs) free(cargs);
 
@@ -349,3 +350,29 @@ lean_obj_res lean_clang_getCursorEnumConstantUValue(lean_obj_arg cursor,
     unsigned long long value = clang_getEnumConstantDeclUnsignedValue(c);
     return lean_io_result_mk_ok(lean_box_uint64((uint64_t)value));
 }
+
+/*
+Evaluate a cursor as an integer expression (for macro constants).
+Returns Option Int64: some(value) for CXEval_Int, none otherwise.
+*/
+
+lean_obj_res lean_clang_evaluateCursor(lean_obj_arg cursor, lean_obj_arg world) {
+    CXCursor c = lean_to_cursor(cursor);
+    CXEvalResult eval = clang_Cursor_Evaluate(c);
+    if (!eval)
+        return lean_io_result_mk_ok(lean_box(0));  // none
+
+    lean_obj_res result;
+    if (clang_EvalResult_getKind(eval) == CXEval_Int) {
+        long long val = clang_EvalResult_getAsInt(eval);
+        lean_obj_res boxed = lean_box_uint64((uint64_t)val);
+        lean_obj_res some  = lean_alloc_ctor(1, 1, 0);
+        lean_ctor_set(some, 0, boxed);
+        result = some;
+    } else {
+        result = lean_box(0);  // none
+    }
+
+    clang_EvalResult_dispose(eval);
+    return lean_io_result_mk_ok(result);
+}