From c2ea120591e82b6826f46283e3b34696907c976f Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 22 Dec 2023 13:24:53 -0500 Subject: [PATCH] feat: indent-based C blocks for `def`/`impl` --- Alloy/C/ExternDef.lean | 7 ++++--- Alloy/C/ExternImpl.lean | 12 ++++++++---- Alloy/C/Grammar.lean | 5 ++++- Alloy/C/Syntax.lean | 17 ++++++++++++++--- Alloy/Util/Binder.lean | 2 +- examples/S/S.lean | 20 +++++++------------- tests/compile/Test/Enum.lean | 3 +-- tests/compile/Test/RawStruct.lean | 5 ++--- 8 files changed, 41 insertions(+), 30 deletions(-) diff --git a/Alloy/C/ExternDef.lean b/Alloy/C/ExternDef.lean index 507eafb..9569d98 100644 --- a/Alloy/C/ExternDef.lean +++ b/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) diff --git a/Alloy/C/ExternImpl.lean b/Alloy/C/ExternImpl.lean index 2929809..48b0734 100644 --- a/Alloy/C/ExternImpl.lean +++ b/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 _ => diff --git a/Alloy/C/Grammar.lean b/Alloy/C/Grammar.lean index 0bc15cd..957696c 100644 --- a/Alloy/C/Grammar.lean +++ b/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 /-! diff --git a/Alloy/C/Syntax.lean b/Alloy/C/Syntax.lean index 025f053..2bbb11f 100644 --- a/Alloy/C/Syntax.lean +++ b/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*}) diff --git a/Alloy/Util/Binder.lean b/Alloy/Util/Binder.lean index c98195b..509e40f 100644 --- a/Alloy/Util/Binder.lean +++ b/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 := diff --git a/examples/S/S.lean b/examples/S/S.lean index 3790e9b..ff0f953 100644 --- a/examples/S/S.lean +++ b/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); -} alloy c extern "lean_S_add_x_y" -def S.addXY (s : @& S) : UInt32 := { +def S.addXY (s : @& S) : UInt32 := return of_lean(s)->m_x + of_lean(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)->m_s); return of_lean(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)->m_y; g_s.m_s = of_lean(s)->m_s; return lean_io_result_mk_ok(lean_box(0)); -} diff --git a/tests/compile/Test/Enum.lean b/tests/compile/Test/Enum.lean index 98025fb..db61322 100644 --- a/tests/compile/Test/Enum.lean +++ b/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(x) + of_lean(y); -} def test : IO Unit := do if myAdd .a .c = 8 then diff --git a/tests/compile/Test/RawStruct.lean b/tests/compile/Test/RawStruct.lean index 3dc8ac4..9c49313 100644 --- a/tests/compile/Test/RawStruct.lean +++ b/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); -} noncomputable def RawY.n (y : RawY) := y.data.n