Skip to content

Aiur inlined function calls (@fn(args)) + blake3 G-function cleanup #500

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 2 commits into from
Jul 20, 2026
Merged

Aiur inlined function calls (@fn(args)) + blake3 G-function cleanup #500

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8f6ee6f
Aiur: inlined function calls (`@fn(args)`)
arthurpaulino Jul 13, 2026
afb4497
Aiur blake3: extract G-function word-ops into @-inlined helpers
arthurpaulino Jul 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 24 additions & 21 deletions Ix/Aiur/Compiler.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ def Bytecode.Toplevel.needsCircuit (t : Bytecode.Toplevel) : Array Bool := Id.ru

/-- Full compilation pipeline. -/
def Source.Toplevel.compile (t : Source.Toplevel) : Except String CompiledToplevel := do
let t ← t.inlineCalls
let typedDecls ← t.checkAndSimplify.mapError toString
let concDecls ← typedDecls.concretize.mapError toString
let (bytecodeRaw, preNameMap) ← concDecls.toBytecode
Expand All @@ -129,13 +130,14 @@ def Source.Toplevel.compile (t : Source.Toplevel) : Except String CompiledToplev
`needsCircuit`, the field-setter `mapIdx`, the name-map `fold`, and the
terminating `pure` — are all total). -/
theorem Source.Toplevel.compile_ok_of_stages
{t : Source.Toplevel} {typedDecls concDecls bytecodeRaw preNameMap}
(hts : t.checkAndSimplify = .ok typedDecls)
{t inlined : Source.Toplevel} {typedDecls concDecls bytecodeRaw preNameMap}
(hinline : t.inlineCalls = .ok inlined)
(hts : inlined.checkAndSimplify = .ok typedDecls)
(hconc : typedDecls.concretize = .ok concDecls)
(hbc : concDecls.toBytecode = .ok (bytecodeRaw, preNameMap)) :
∃ ct, t.compile = .ok ct := by
simp only [Source.Toplevel.compile, hts, hconc, hbc, Except.mapError, bind,
Except.bind, pure, Except.pure]
simp only [Source.Toplevel.compile, hinline, hts, hconc, hbc, Except.mapError,
bind, Except.bind, pure, Except.pure]
exact ⟨_, rfl⟩

/-- Inverse of `compile_ok_of_stages`: unpack a successful `compile` into
Expand All @@ -144,27 +146,28 @@ lemmas through the composition. -/
theorem Source.Toplevel.compile_stages_of_ok
{t : Source.Toplevel} {ct : CompiledToplevel}
(_hct : t.compile = .ok ct) :
∃ typedDecls concDecls bytecodeRaw preNameMap,
t.checkAndSimplify = .ok typedDecls ∧
∃ inlined typedDecls concDecls bytecodeRaw preNameMap,
t.inlineCalls = .ok inlined ∧
inlined.checkAndSimplify = .ok typedDecls ∧
typedDecls.concretize = .ok concDecls ∧
concDecls.toBytecode = .ok (bytecodeRaw, preNameMap) := by
-- Case on each stage result; `mapError` on `.ok` is definitionally `.ok`.
cases hts : t.checkAndSimplify with
| error e => simp [Source.Toplevel.compile, hts, bind, Except.bind, Except.mapError] at _hct
| ok typedDecls =>
cases hconc : typedDecls.concretize with
| error e =>
simp [Source.Toplevel.compile, hts, hconc, bind, Except.bind, Except.mapError] at _hct
| ok concDecls =>
cases hbc : concDecls.toBytecode with
cases hinline : t.inlineCalls with
| error e => simp [Source.Toplevel.compile, hinline, bind, Except.bind] at _hct
| ok inlined =>
cases hts : inlined.checkAndSimplify with
| error e => simp [Source.Toplevel.compile, hinline, hts, bind, Except.bind, Except.mapError] at _hct
| ok typedDecls =>
cases hconc : typedDecls.concretize with
| error e =>
simp [Source.Toplevel.compile, hts, hconc, hbc, bind, Except.bind, Except.mapError] at _hct
| ok bc =>
obtain ⟨bytecodeRaw, preNameMap⟩ := bc
-- `checkAndSimplify`/`concretize` are unfolded; `toBytecode` is not
-- (private module), so the first two equalities reduce to `rfl` but
-- the third still mentions `concDecls.toBytecode` — supply `hbc`.
exact ⟨typedDecls, concDecls, bytecodeRaw, preNameMap, rfl, hconc, hbc⟩
simp [Source.Toplevel.compile, hinline, hts, hconc, bind, Except.bind, Except.mapError] at _hct
| ok concDecls =>
cases hbc : concDecls.toBytecode with
| error e =>
simp [Source.Toplevel.compile, hinline, hts, hconc, hbc, bind, Except.bind, Except.mapError] at _hct
| ok bc =>
obtain ⟨bytecodeRaw, preNameMap⟩ := bc
exact ⟨inlined, typedDecls, concDecls, bytecodeRaw, preNameMap, rfl, hts, hconc, hbc⟩

-- Compile post-conditions moved to `Proofs/StructCompatible.lean`.

Expand Down
9 changes: 8 additions & 1 deletion Ix/Aiur/Compiler/Check.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -622,7 +622,14 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
match typOpt with
| some (typ, escapes) => pure (Typed.Term.match typ escapes term' branches')
| none => throw .emptyMatch
| .app func args u => do
| .app func args mode => do
-- `.inlined` is eliminated by `Toplevel.inlineCalls` before checking;
-- reaching it here means the pass was skipped. Downstream stages carry
-- only the unconstrained flag.
let u : Bool ← match mode with
| .normal => pure false
| .unconstrained => pure true
| .inlined => throw (.cannotApply func)
let ctx ← read
-- Local function lookup (only for unqualified names); returns
-- `some (.ok …)` on hit, `some (.error …)` on wrong-type local, `none` to
Expand Down
30 changes: 20 additions & 10 deletions Ix/Aiur/Meta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,10 @@ syntax ("." noWs)? ident "(" ")" :
syntax ("." noWs)? ident "(" aiur_trm (", " aiur_trm)* ")" : aiur_trm
syntax "#" noWs ("." noWs)? ident "(" ")" : aiur_trm
syntax "#" noWs ("." noWs)? ident "(" aiur_trm (", " aiur_trm)* ")" : aiur_trm
-- Inlined call: `@fn(args)` splices `fn`'s body into the caller at compile
-- time (no separate circuit). Callee must not be inline-recursive.
syntax "@" noWs ("." noWs)? ident "(" ")" : aiur_trm
syntax "@" noWs ("." noWs)? ident "(" aiur_trm (", " aiur_trm)* ")" : aiur_trm
syntax ident "‹" aiur_typ (", " aiur_typ)* "›" "(" ")" : aiur_trm
syntax ident "‹" aiur_typ (", " aiur_typ)* "›" "(" aiur_trm
(", " aiur_trm)* ")" : aiur_trm
Expand Down Expand Up @@ -266,16 +270,22 @@ partial def elabTrm : ElabStxCat `aiur_trm
| .str .anonymous _ => pure ()
| _ => logWarningAt f "empty parentheses are not needed; use the name without parentheses"
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| $[.]?$f:ident ($a:aiur_trm $[, $as:aiur_trm]*)) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| #$[.]?$f:ident()) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, toExpr true]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.unconstrained]
| `(aiur_trm| #$[.]?$f:ident($a:aiur_trm $[, $as:aiur_trm]*)) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, toExpr true]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.unconstrained]
| `(aiur_trm| @$[.]?$f:ident()) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.inlined]
| `(aiur_trm| @$[.]?$f:ident($a:aiur_trm $[, $as:aiur_trm]*)) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.inlined]
| `(aiur_trm| $a:aiur_trm + $b:aiur_trm) => do
mkAppM ``Source.Term.add #[← elabTrm a, ← elabTrm b]
| `(aiur_trm| $a:aiur_trm - $b:aiur_trm) => do
Expand Down Expand Up @@ -355,29 +365,29 @@ partial def elabTrm : ElabStxCat `aiur_trm
-- Template function calls: explicit type args are dropped (inferred)
| `(aiur_trm| $f:ident‹$_:aiur_typ $[, $_:aiur_typ]*›()) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| $f:ident‹$_:aiur_typ $[, $_:aiur_typ]*›
($a:aiur_trm $[, $as:aiur_trm]*)) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| #$f:ident‹$_:aiur_typ $[, $_:aiur_typ]*›()) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, toExpr true]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.unconstrained]
| `(aiur_trm| #$f:ident‹$_:aiur_typ $[, $_:aiur_typ]*›
($a:aiur_trm $[, $as:aiur_trm]*)) => do
let g ← mkAppM ``Global.mk #[toExpr f.getId]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, toExpr true]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.unconstrained]
-- Template constructor calls
| `(aiur_trm| $tmpl:ident‹$_:aiur_typ $[, $_:aiur_typ]*›.$ctor:ident()) => do
logWarningAt ctor "empty parentheses are not needed; use the name without parentheses"
let name := tmpl.getId ++ ctor.getId
let g ← mkAppM ``Global.mk #[toExpr name]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabEmptyList ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| $tmpl:ident‹$_:aiur_typ $[, $_:aiur_typ]*›.$ctor:ident
($a:aiur_trm $[, $as:aiur_trm]*)) => do
let name := tmpl.getId ++ ctor.getId
let g ← mkAppM ``Global.mk #[toExpr name]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, toExpr false]
mkAppM ``Source.Term.app #[g, ← elabList a as elabTrm ``Source.Term, mkConst ``Source.CallMode.normal]
| `(aiur_trm| fold($i .. $j, $init, |$acc, @$v| $body)) => do
let i := i.getNat
let j := j.getNat
Expand Down
Loading