Initial commit - super basic toy Lean AST parser

.gitignore

@@ -0,0 +1 @@
+/.lake

LeanFfiExperiment.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `LeanFfiExperiment` library.
+-- Import modules here that should be built as part of the library.
+import LeanFfiExperiment.Basic

LeanFfiExperiment/Basic.lean

@@ -0,0 +1,16 @@
+def hello := "world"
+
+structure AST where
+  name: String
+  count: Nat
+
+instance : ToString AST where
+  toString (input: AST) : String :=
+  s!"\{ name: {input.name}, count: {input.count} }"
+
+
+def parseCFile (input: String): AST :=
+  {
+    name := input,
+    count := 5
+  }

Main.lean

@@ -0,0 +1,8 @@
+import LeanFfiExperiment
+
+def main : IO Unit := do
+  IO.println s!"Hello, {hello}!"
+
+  let ast := parseCFile "test.c"
+
+  IO.println s!"The AST: {ast}"

README.md

@@ -0,0 +1 @@
+# lean-ffi-experiment

lake-manifest.json

@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«lean-ffi-experiment»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lakefile.toml

@@ -0,0 +1,10 @@
+name = "lean-ffi-experiment"
+version = "0.1.0"
+defaultTargets = ["lean-ffi-experiment"]
+
+[[lean_lib]]
+name = "LeanFfiExperiment"
+
+[[lean_exe]]
+name = "lean-ffi-experiment"
+root = "Main"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0