feat: indent-based C blocks for def/impl

Alloy/C/ExternDef.lean

@@ -25,13 +25,14 @@ alloy c section LEAN_EXPORT uint32_t alloy_foo(uint32_t x) {...}
 -/
 scoped syntax (name := externDecl)
 (docComment)? (Term.attributes)? (visibility)? «unsafe»?
-"alloy " &"c " "extern " (str)? "def " declId binders " : " term " := " cStmt
+"alloy " &"c " "extern " (str)?
+"def " declId binders " : " term " := " withPosition(many1Indent(stmtLike))
 : command
 
 elab_rules : command
 | `(externDecl| $[$doc?]? $[$attrs?]? $[$vis?]? $[unsafe%$uTk?]?
-  alloy c extern%$exTk $[$sym?]? def $id $bs* : $ty := $body) => do
+  alloy c extern%$exTk $[$sym?]? def $id $bs* : $ty := $stmts*) => do
   let cmd ← `($[$doc?]? $[$attrs?]? $[$vis?]? noncomputable $[unsafe%$uTk?]? opaque $id $[$bs]* : $ty)
   withMacroExpansion (← getRef) cmd <| elabCommand cmd
   let bvs ← liftMacroM <| bs.concatMapM matchBinder
-  elabExternImpl exTk sym? ⟨id.raw[0]⟩ bvs ty (packBody body)
+  elabExternImpl exTk sym? ⟨id.raw[0]⟩ bvs ty (packBody stmts)

Alloy/C/ExternImpl.lean

@@ -110,11 +110,15 @@ attribute [extern "alloy_foo"] foo
 alloy c section LEAN_EXPORT uint32_t alloy_foo(uint32_t x) {...}
 ```
 -/
-scoped elab (name := externImpl)
-"alloy " &"c " exTk:&"extern " sym?:(str)?
-&"impl " id:ident bs:Term.binderIdent* " := " body:cStmt : command => do
+scoped syntax (name := externImpl)
+"alloy " &"c " &"extern " (str)?
+&"impl " ident Term.binderIdent* " := " withPosition(many1Indent(stmtLike))
+: command
+
+elab_rules : command
+| `(alloy c extern%$exTk $(sym?)? impl $id $bs* := $stmts*) => do
   let bvs := bs.map fun id => {ref := id, id, type := mkHoleFrom .missing}
-  elabExternImpl exTk sym? id bvs .missing (packBody body)
+  elabExternImpl exTk sym? id bvs .missing (packBody stmts)
 
 @[unused_variables_ignore_fn]
 def ignoreExternImpl : Linter.IgnoreFunction := fun _ stack _ =>

Alloy/C/Grammar.lean

@@ -825,12 +825,15 @@ attribute [cStmt_parser] returnStmt
 ### Compound Statements
 -/
 
+/-- Syntax which can be used in the place of a statement in a `compound-statement`. -/
+syntax stmtLike := lineComment <|> blockComment <|> atomic(declaration) <|> cStmt
+
 /--
 A [`compound-statement`][1] of the C grammar.
 
 [1]: https://en.cppreference.com/w/c/language/statements#Compound_statements
 -/
-syntax compStmt := "{" (lineComment <|> blockComment <|> atomic(declaration) <|> cStmt)* "}"
+syntax compStmt := "{" stmtLike* "}"
 attribute [cStmt_parser] compStmt
 
 /-!

Alloy/C/Syntax.lean

@@ -52,6 +52,7 @@ abbrev AggrSig := TSyntax ``aggrSig
 abbrev Enumerator := TSyntax ``enumerator
 abbrev EnumSig := TSyntax ``enumSig
 abbrev Declaration := TSyntax ``declaration
+abbrev StmtLike := TSyntax ``stmtLike
 abbrev CompStmt := TSyntax ``compStmt
 abbrev ConstExpr := TSyntax ``constExpr
 
@@ -132,6 +133,12 @@ instance : Coe StorageClassSpec DeclSpec where
 instance : Coe FunSpec DeclSpec where
   coe x := Unhygienic.run `(cDeclSpec| $x:cFunSpec)
 
+instance : Coe Stmt StmtLike where
+  coe x := Unhygienic.run `(stmtLike| $x:cStmt)
+
+instance : Coe Declaration StmtLike where
+  coe x := Unhygienic.run `(stmtLike| $x:declaration)
+
 instance : Coe CompStmt Stmt where
   coe x := Unhygienic.run `(cStmt| $x:compStmt)
 
@@ -151,6 +158,10 @@ instance : Coe PPCmd Cmd where
 ## Other Helpers
 -/
 
-def packBody : Stmt → CompStmt
-| `(cStmt| $x:compStmt) => x
-| stmt => Unhygienic.run `(compStmt| {$stmt:cStmt})
+def packBody (stmts : Array StmtLike) : CompStmt :=
+  if h : 0 < stmts.size then
+    match stmts[0] with
+    | `(stmtLike| $x:compStmt) => x
+    | _ => Unhygienic.run `(compStmt| {$stmts*})
+  else
+    Unhygienic.run `(compStmt| {$stmts*})

Alloy/Util/Binder.lean

@@ -13,7 +13,7 @@ namespace Alloy
 -- Adapted from the private utilities in `Lean.Elab.Binders`
 
 abbrev Hole := TSyntax ``Term.hole
-abbrev BinderIdent := TSyntax ``Term.binderIdent
+abbrev BinderIdent := TSyntax [identKind, ``Term.hole]
 abbrev BinderModifier := TSyntax [``Term.binderTactic, ``Term.binderDefault]
 
 @[inline] def mkHoleFrom (ref : Syntax) (canonical := false) : Hole :=

examples/S/S.lean

@@ -46,46 +46,41 @@ alloy c opaque_extern_type S => S := {
 --------------------------------------------------------------------------------
 
 alloy c extern "lean_mk_S"
-def mkS (x y : UInt32) (string : String) : S := {
-  S* s = malloc(sizeof(S));
+def mkS (x y : UInt32) (string : String) : S :=
+  S* s = (S*)malloc(sizeof(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 := {
+def S.addXY (s : @& S) : UInt32 :=
   return of_lean<S>(s)->m_x + of_lean<S>(s)->m_y;
-}
 
 alloy c extern "lean_S_string"
-def S.string (s : @& 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 := {
+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 := {
+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 := {
+def updateGlobalS (s : @& S) : BaseIO Unit :=
   if (g_s.m_s != NULL) {
     lean_dec(g_s.m_s);
   }
@@ -94,4 +89,3 @@ def updateGlobalS (s : @& S) : BaseIO Unit := {
   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));
-}

tests/compile/Test/Enum.lean

@@ -12,9 +12,8 @@ alloy c enum
   | c => 7
   deriving Inhabited
 
-alloy c extern def myAdd (x y : MyNum) : UInt32 := {
+alloy c extern def myAdd (x y : MyNum) : UInt32 :=
   return of_lean<MyNum>(x) + of_lean<MyNum>(y);
-}
 
 def test : IO Unit := do
   if myAdd .a .c = 8 then

tests/compile/Test/RawStruct.lean

@@ -32,12 +32,11 @@ alloy c extern_type RawY => Y := {
   finalize := `Y_finalize
 }
 
-alloy c extern impl RawY.mk data := {
-  Y* rawY = malloc(sizeof(Y));
+alloy c extern impl RawY.mk data :=
+  Y* rawY = (Y*)malloc(sizeof(Y));
   rawY->n = lean_ctor_get_uint32(data, 0);
   rawY->m = lean_ctor_get_uint32(data, sizeof(uint32_t));
   return to_lean<RawY>(rawY);
-}
 
 noncomputable def RawY.n (y : RawY) := y.data.n