From 6d13857b43364f938d14a27dba3f97583bb1d6c3 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Wed, 29 Jul 2026 15:51:00 +0000 Subject: [PATCH 1/2] Extract constant array and slice literals as single data-carrying builtins An n-element array literal previously extracted to n nested letIns feeding mkArray, so every tactic pass over the goal was linear in n and steps' per-statement machinery made proofs about large arrays super-quadratic (256 elements: ~2 minutes and 5GB; 512: stack overflow). The nesting also made extracted files above ~256 elements fail to elaborate at default recursion limits. All-literal #_mkArray/#_mkVector calls now elaborate to one callBuiltin of Builtin.mkValArray/mkValVector, with the element values hoisted into an auxiliary List definition (chunked appends keep nesting bounded at any size). Goals about a table then contain a single shallow constant, so proof cost is independent of the array length: a 1024-element table spec now costs ~1s instead of failing outright. Arrays with any non-constant element keep the existing path. --- Lampe/Lampe/Builtin/Array.lean | 24 ++++++++++ Lampe/Lampe/Builtin/Vector.lean | 10 ++++ Lampe/Lampe/Syntax/Elab.lean | 85 ++++++++++++++++++++++++++++++++- Lampe/Lampe/Tactic/Steps.lean | 14 ++++++ Lampe/Lampe/Tp.lean | 18 +++++++ 5 files changed, 150 insertions(+), 1 deletion(-) diff --git a/Lampe/Lampe/Builtin/Array.lean b/Lampe/Lampe/Builtin/Array.lean index c0107622..d3857fd7 100644 --- a/Lampe/Lampe/Builtin/Array.lean +++ b/Lampe/Lampe/Builtin/Array.lean @@ -91,6 +91,30 @@ def mkRepeatedArray := newGenericTotalPureBuiltin (fun (len, tp) => ⟨[tp], (.array tp len)⟩) (fun (num, _) h![val] => List.Vector.replicate num.toNat val) +/-- +Interprets a list of element values as an array of length `n`, truncating or zero-padding as +needed. The length proof is the generic `List.takeD_length`, so no per-instance proof obligation +arises when constructing concrete arrays this way. +-/ +def valArray {p : Prime} (tp : Tp) (n : U 32) (vals : List (Tp.denote p tp)) : + Tp.denote p (.array tp n) := + ⟨vals.takeD n.toNat (Tp.zero p tp), List.takeD_length _ _ _⟩ + +/-- +Defines the builtin constructor for arrays whose elements are all compile-time constants. + +The element values are carried by the builtin itself as a (prime-generic) denoted list, rather +than as per-element expressions. The Lampe elaborator emits this builtin — with `vals` referencing +a hoisted auxiliary definition — for array literals all of whose elements are numeric literals. +This keeps both the extracted term and every proof goal mentioning the array shallow (a single +constant), in contrast to the general `mkArray` path which `letIn`-binds each element and so +produces terms whose depth grows with the array length. +-/ +def mkValArray (arrTp : Tp) (vals : (p : Prime) → List (Tp.denote p arrTp.arrayElem)) := + newGenericTotalPureBuiltin + (fun (_ : Unit) => ⟨[], .array arrTp.arrayElem arrTp.arraySize⟩) + (fun _ h![] => valArray arrTp.arrayElem arrTp.arraySize (vals _)) + /-- Defines the indexing of a array `l : Array tp n` with `i : U 32` We make the following assumptions: diff --git a/Lampe/Lampe/Builtin/Vector.lean b/Lampe/Lampe/Builtin/Vector.lean index 9aa9811f..f3178e7d 100644 --- a/Lampe/Lampe/Builtin/Vector.lean +++ b/Lampe/Lampe/Builtin/Vector.lean @@ -30,6 +30,16 @@ def mkRepeatedVector := newGenericTotalPureBuiltin (fun (a : Tp)=> ⟨[Tp.u 32, a], (.vector a)⟩) (fun _ h![n, val] => List.replicate n.toNat val) +/-- +Defines the builtin constructor for vectors (slices) whose elements are all compile-time +constants. The element values are carried by the builtin itself as a (prime-generic) denoted +list; see `Builtin.mkValArray` for the rationale. +-/ +def mkValVector (tp : Tp) (vals : (p : Prime) → List (Tp.denote p tp)) := + newGenericTotalPureBuiltin + (fun (_ : Unit) => ⟨[], .vector tp⟩) + (fun _ h![] => vals _) + /-- Defines the indexing of a vector `l : List tp` with `i : U 32` We make the following assumptions: diff --git a/Lampe/Lampe/Syntax/Elab.lean b/Lampe/Lampe/Syntax/Elab.lean index ae0334e0..ed4637ea 100644 --- a/Lampe/Lampe/Syntax/Elab.lean +++ b/Lampe/Lampe/Syntax/Elab.lean @@ -11,18 +11,101 @@ open Lean Elab -- DSL: TERMS ------------------------------------------------------------------------------------- +/-- +Views `stx` as a compile-time-constant element of an array literal, returning a term for its +denoted value (the surrounding list ascription supplies the expected type). Returns `none` for +anything that is not a numeric or boolean literal. +-/ +private partial def litArrayElem (stx : TSyntax `noir_expr) : + Elab.Command.CommandElabM (Option (TSyntax `term)) := do + match stx with + | `(noir_expr|($e:noir_expr)) => litArrayElem e + | `(noir_expr|$n:num : $_) => return some (←`($n)) + | `(noir_expr|-$n:num : $_) => return some (←`((-$n))) + | `(noir_expr|#_true) => return some (←`(true)) + | `(noir_expr|#_false) => return some (←`(false)) + | _ => return none + +/-- Applies `f` to every node of `stx` top-down, replacing a node (without descending into the +replacement) whenever `f` returns `some`. -/ +private partial def replaceSyntaxTopDownM [Monad m] (f : Syntax → m (Option Syntax)) + (stx : Syntax) : m Syntax := do + match ← f stx with + | some new => return new + | none => match stx with + | .node info kind args => return .node info kind (← args.mapM (replaceSyntaxTopDownM f)) + | s => return s + +/-- +Rewrites every `#_ mkArray` / `#_ mkVector` call in `stx` whose arguments are all compile-time +constants into a single `Builtin.mkValArray` / `Builtin.mkValVector` call (via the `splice!` +escape hatch), hoisting the element values into an auxiliary definition named +`«#lits»`. + +The general `mkArray` path `letIn`-binds every element, so an `n`-element literal produces a term +(and, later, proof goals) of depth `O(n)`; every recursive traversal of such a term — during +elaboration, `simp`, or unification — then needs recursion depth and time proportional to `n`, +which makes large array literals unusably slow. After this rewrite the extracted body and all +goals about it contain only the (shallow) auxiliary constant, so their cost is independent of the +array size. The auxiliary definition elaborates the deep list literal exactly once. + +Arrays with any non-constant element (e.g. a function call) are left on the general path. +-/ +private def hoistLiteralArrays (baseName : Name) (stx : Syntax) : + Elab.Command.CommandElabM Syntax := do + let counter ← IO.mkRef (0 : Nat) + let pId := mkIdent `p + let rewrite (node : Syntax) : Elab.Command.CommandElabM (Option Syntax) := do + let tnode : TSyntax `noir_expr := ⟨node⟩ + match tnode with + | `(noir_expr|(#_ $nm:ident returning $tp)( $args,* )) => do + let isArray := nm.getId == `mkArray + unless isArray || nm.getId == `mkVector do return none + if args.getElems.isEmpty then return none + let elems ← args.getElems.mapM litArrayElem + let some elems := elems.mapM id | return none + let arrTp ← MonadDSL.run (makeNoirType tp) + -- Emit the element list in chunks joined by `++` so that the nesting depth of the + -- elaborated term stays bounded regardless of the array length. + let chunkSize := 256 + let mut chunks : Array (Array (TSyntax `term)) := #[] + let mut i := 0 + while i < elems.size do + chunks := chunks.push (elems.extract i (min (i + chunkSize) elems.size)) + i := i + chunkSize + let mut body ← `([$(chunks.back!),*]) + for c in chunks.pop.reverse do + body ← `([$c,*] ++ $body) + let idx ← counter.modifyGet fun i => (i, i + 1) + let auxId := mkIdent <| Name.mkSimple s!"{baseName.getString!}#lits{idx}" + let elemTp ← if isArray then `(Tp.arrayElem $arrTp) else `(Tp.vectorElem $arrTp) + Elab.Command.elabCommand <| ← + `(def $auxId ($pId : Prime) : List (Tp.denote $pId $elemTp) := $body) + let repl ← if isArray then + `(noir_expr| + splice!( Expr.callBuiltin [] $arrTp (Builtin.mkValArray $arrTp $auxId) h![] )) + else + `(noir_expr| + splice!( Expr.callBuiltin [] $arrTp (Builtin.mkValVector $elemTp $auxId) h![] )) + return some repl.raw + | _ => return none + replaceSyntaxTopDownM rewrite stx + /-- Elaborates a function definition written in the Noir eDSL. -/ elab d:noir_depr? "noir_def" decl:noir_fn_def : command => do + let baseName ← makeNoirIdent decl.raw[0] + let decl : TSyntax `noir_fn_def := ⟨← hoistLiteralArrays baseName.getId decl.raw⟩ let (name, decl) ← makeFnDecl decl let decl ← match (←parseDeprecatedMessage d) with | some msg => `( - @[deprecated $name $(Syntax.mkStrLit msg) (since := "")] + @[deprecated $name $(Syntax.mkStrLit msg) (since := "")] def $name : FunctionDecl := $decl) | none => `(def $name : FunctionDecl := $decl) Elab.Command.elabCommand decl /-- Elaborates a trait implementation written in the Noir eDSL. -/ elab "noir_trait_impl[" defName:ident "]" impl:noir_trait_impl : command => do + let impl : TSyntax `noir_trait_impl := ⟨← hoistLiteralArrays defName.getId impl.raw⟩ let (name, impl) ← makeTraitImpl impl let decl ← `(def $defName : String × TraitImpl := ($(Syntax.mkStrLit name.getId.toString), $impl)) Elab.Command.elabCommand decl diff --git a/Lampe/Lampe/Tactic/Steps.lean b/Lampe/Lampe/Tactic/Steps.lean index 8cd1584e..ed1ba6e9 100644 --- a/Lampe/Lampe/Tactic/Steps.lean +++ b/Lampe/Lampe/Tactic/Steps.lean @@ -158,6 +158,13 @@ def getClosingTerm (val : Lean.Expr) : TacticM (Option (TSyntax `term)) := withT return some (←``(genericTotalPureBuiltin_intro Builtin.mkArray (a := (List.length $argTypes, _)) rfl)) | ``Lampe.Builtin.mkRepeatedArray => return some (←``(genericTotalPureBuiltin_intro Builtin.mkRepeatedArray (a := (_, _)) rfl)) + | ``Lampe.Builtin.mkValArray => + let some arrTp := builtin.getAppArgs[0]? | throwError "malformed mkValArray" + let some vals := builtin.getAppArgs[1]? | throwError "malformed mkValArray" + let arrTp ← arrTp.toSyntax + let vals ← vals.toSyntax + return some + (←``(genericTotalPureBuiltin_intro (Builtin.mkValArray $arrTp $vals) (a := ()) rfl)) | ``Lampe.Builtin.arrayIndex => return some (←``(arrayIndex_intro)) | ``Lampe.Builtin.arrayLen => let some argTps := val.getAppArgs[1]? | throwError "malformed arrayLen" @@ -176,6 +183,13 @@ def getClosingTerm (val : Lean.Expr) : TacticM (Option (TSyntax `term)) := withT return some (←``(genericTotalPureBuiltin_intro Builtin.mkVector (a := (List.length $argTypes, _)) rfl)) | ``Lampe.Builtin.mkRepeatedVector => return some (←``(genericTotalPureBuiltin_intro Builtin.mkRepeatedVector (a := _) rfl)) + | ``Lampe.Builtin.mkValVector => + let some tp := builtin.getAppArgs[0]? | throwError "malformed mkValVector" + let some vals := builtin.getAppArgs[1]? | throwError "malformed mkValVector" + let tp ← tp.toSyntax + let vals ← vals.toSyntax + return some + (←``(genericTotalPureBuiltin_intro (Builtin.mkValVector $tp $vals) (a := ()) rfl)) | ``Lampe.Builtin.vectorPushBack => return some (←``(genericTotalPureBuiltin_intro Builtin.vectorPushBack rfl)) | ``Lampe.Builtin.vectorPushFront => return some (←``(genericTotalPureBuiltin_intro Builtin.vectorPushFront rfl)) | ``Lampe.Builtin.vectorIndex => return some (←``(vectorIndex_intro)) diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean index 95a067ae..adfe9c5e 100644 --- a/Lampe/Lampe/Tp.lean +++ b/Lampe/Lampe/Tp.lean @@ -281,6 +281,24 @@ match tp with end +/-- The element type of an array type (or `.unit` for non-array types). -/ +@[reducible] +def Tp.arrayElem : Tp → Tp + | .array tp _ => tp + | _ => .unit + +/-- The length of an array type (or `0` for non-array types). -/ +@[reducible] +def Tp.arraySize : Tp → U 32 + | .array _ n => n + | _ => 0 + +/-- The element type of a vector (slice) type (or `.unit` for non-vector types). -/ +@[reducible] +def Tp.vectorElem : Tp → Tp + | .vector tp => tp + | _ => .unit + /-- Index into a `Tp.denoteArgs` tuple by `Member` witness. -/ @[reducible] def Tp.denoteArgs.getByMember : {tps : List Tp} → Tp.denoteArgs p tps → Member tp tps → Tp.denote p tp From 5f11447afceedbca6e671494870afa6330d3b581 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Wed, 29 Jul 2026 16:50:16 +0000 Subject: [PATCH 2/2] Document the fast array-literal machinery step by step Add inline explanations to each piece of the mkValArray/mkValVector pipeline: the length-proof construction in valArray, the shape of the data-carrying builtins, the reducible Tp projections and their role in unification, the literal-hoisting rewrite in the elaborator, and the closing terms emitted by the steps tactic. --- Lampe/Lampe/Builtin/Array.lean | 36 +++++++++++++++++++++++++++++---- Lampe/Lampe/Builtin/Vector.lean | 5 ++++- Lampe/Lampe/Syntax/Elab.lean | 32 +++++++++++++++++++++++++---- Lampe/Lampe/Tactic/Steps.lean | 12 +++++++++++ Lampe/Lampe/Tp.lean | 12 ++++++++++- 5 files changed, 87 insertions(+), 10 deletions(-) diff --git a/Lampe/Lampe/Builtin/Array.lean b/Lampe/Lampe/Builtin/Array.lean index d3857fd7..c2c6c862 100644 --- a/Lampe/Lampe/Builtin/Array.lean +++ b/Lampe/Lampe/Builtin/Array.lean @@ -93,12 +93,21 @@ def mkRepeatedArray := newGenericTotalPureBuiltin /-- Interprets a list of element values as an array of length `n`, truncating or zero-padding as -needed. The length proof is the generic `List.takeD_length`, so no per-instance proof obligation -arises when constructing concrete arrays this way. +needed. An array denotes as a `List.Vector`, i.e. a list *paired with a proof* that its length +is `n`; both components are built below so that they are independent of the concrete elements. -/ def valArray {p : Prime} (tp : Tp) (n : U 32) (vals : List (Tp.denote p tp)) : Tp.denote p (.array tp n) := - ⟨vals.takeD n.toNat (Tp.zero p tp), List.takeD_length _ _ _⟩ + ⟨-- Reshape the input to exactly `n` elements: keep the first `n`, pad with the type's zero + -- value if `vals` is too short. The elaborator always supplies a list of exactly the right + -- length, so this is the identity in practice; it exists so the result is length-correct + -- *by construction* for any input. + vals.takeD n.toNat (Tp.zero p tp), + -- The generic lemma `(l.takeD n d).length = n`. Because `takeD` guarantees the length for + -- *any* list, this discharges the vector's length side-condition without ever inspecting + -- the elements — checking a 10'000-element literal costs the same as a 1-element one, + -- unlike proving `[a, b, c, …].length = n` by `rfl`/`decide`, which walks the whole list. + List.takeD_length _ _ _⟩ /-- Defines the builtin constructor for arrays whose elements are all compile-time constants. @@ -110,9 +119,28 @@ This keeps both the extracted term and every proof goal mentioning the array sha constant), in contrast to the general `mkArray` path which `letIn`-binds each element and so produces terms whose depth grows with the array length. -/ -def mkValArray (arrTp : Tp) (vals : (p : Prime) → List (Tp.denote p arrTp.arrayElem)) := +def mkValArray + (arrTp : Tp) + -- `vals` is a *function of the prime* rather than a plain list, because element values live + -- in `Tp.denote p _`, which depends on `p` — e.g. `Field` elements are integers modulo `p`. + -- The builtin must work at every prime, so the hoisted definition abstracts over it. + (vals : (p : Prime) → List (Tp.denote p arrTp.arrayElem)) := newGenericTotalPureBuiltin + -- The generic-argument type is `Unit` (unlike `mkArray`, which is indexed by element count + -- and type): the builtin is fully determined by its parameters `arrTp`/`vals`, so proof + -- automation always instantiates it with `a := ()`. The signature takes *no runtime + -- arguments* (`[]`) — the elements are data inside the builtin — so stepping over a call + -- produces no per-element subgoals. The output type is recovered from the whole array type + -- via the projections `arrayElem`/`arraySize` rather than taking element type and length + -- as separate parameters: the elaborator can pass the one type annotation it already has, + -- and because the projections are `@[reducible]`, `(.array tp n).arrayElem`/`.arraySize` + -- unify with `tp`/`n` when the closing lemma from `Tactic/Steps.lean` — stated at the + -- projected type — is matched against a goal stated at the original array type. (fun (_ : Unit) => ⟨[], .array arrTp.arrayElem arrTp.arraySize⟩) + -- Evaluation: `h![]` matches the empty `HList` of runtime arguments, and the result is + -- `valArray … (vals p)` (the prime is implicit from context), whose length side-condition + -- is discharged generically (see `valArray`) — no proof obligation about the concrete + -- elements ever arises. (fun _ h![] => valArray arrTp.arrayElem arrTp.arraySize (vals _)) /-- diff --git a/Lampe/Lampe/Builtin/Vector.lean b/Lampe/Lampe/Builtin/Vector.lean index f3178e7d..afc4e716 100644 --- a/Lampe/Lampe/Builtin/Vector.lean +++ b/Lampe/Lampe/Builtin/Vector.lean @@ -33,11 +33,14 @@ def mkRepeatedVector := newGenericTotalPureBuiltin /-- Defines the builtin constructor for vectors (slices) whose elements are all compile-time constants. The element values are carried by the builtin itself as a (prime-generic) denoted -list; see `Builtin.mkValArray` for the rationale. +list; see `Builtin.mkValArray` for a step-by-step account of the construction. -/ def mkValVector (tp : Tp) (vals : (p : Prime) → List (Tp.denote p tp)) := newGenericTotalPureBuiltin (fun (_ : Unit) => ⟨[], .vector tp⟩) + -- Simpler than the array case: a vector denotes as a bare `List` with no length invariant, + -- so `vals p` is already a value of the output type and is returned directly — no `takeD` + -- reshaping and no length lemma are needed. (fun _ h![] => vals _) /-- diff --git a/Lampe/Lampe/Syntax/Elab.lean b/Lampe/Lampe/Syntax/Elab.lean index ed4637ea..b433e915 100644 --- a/Lampe/Lampe/Syntax/Elab.lean +++ b/Lampe/Lampe/Syntax/Elab.lean @@ -13,8 +13,13 @@ open Lean Elab /-- Views `stx` as a compile-time-constant element of an array literal, returning a term for its -denoted value (the surrounding list ascription supplies the expected type). Returns `none` for -anything that is not a numeric or boolean literal. +denoted value. Returns `none` for anything that is not a numeric or boolean literal. + +Note that the element's own Noir-level type ascription (`$n : $_`) is dropped: the returned +term is a bare Lean numeral (or `Bool` literal), which later elaborates against the expected +element type `Tp.denote p tp` imposed by the hoisted definition's type ascription — via that +type's `OfNat` (resp. `Neg`) instance. Dropping the ascription is sound because extraction +always ascribes every element with the array's element type. -/ private partial def litArrayElem (stx : TSyntax `noir_expr) : Elab.Command.CommandElabM (Option (TSyntax `term)) := do @@ -61,12 +66,23 @@ private def hoistLiteralArrays (baseName : Name) (stx : Syntax) : | `(noir_expr|(#_ $nm:ident returning $tp)( $args,* )) => do let isArray := nm.getId == `mkArray unless isArray || nm.getId == `mkVector do return none + -- Empty literals stay on the general path: they are already cheap, and there would be + -- nothing to hoist. if args.getElems.isEmpty then return none + -- All-or-nothing: view every element as a compile-time constant; if any element is not + -- one (`mapM id` folds `Array (Option _)` into `Option (Array _)`), leave the whole + -- literal on the general `mkArray`/`mkVector` path. let elems ← args.getElems.mapM litArrayElem let some elems := elems.mapM id | return none + -- Elaborate the surface type annotation into a `Tp` term; it becomes the builtin's + -- parameter and, projected via `Tp.arrayElem`/`Tp.vectorElem`, the element type of the + -- hoisted list. let arrTp ← MonadDSL.run (makeNoirType tp) - -- Emit the element list in chunks joined by `++` so that the nesting depth of the - -- elaborated term stays bounded regardless of the array length. + -- A `[…]` literal expands to a right-nested chain of `List.cons`, so a single literal of + -- all `n` elements would make the elaborator recurse to depth `n` (overflowing its stack + -- for large `n`). Emitting the elements as 256-element `[…]` chunks joined by `++` caps + -- the depth contributed by any one literal at 256, leaving only the far shallower + -- (`n / 256`-deep) `++` spine. let chunkSize := 256 let mut chunks : Array (Array (TSyntax `term)) := #[] let mut i := 0 @@ -77,10 +93,18 @@ private def hoistLiteralArrays (baseName : Name) (stx : Syntax) : for c in chunks.pop.reverse do body ← `([$c,*] ++ $body) let idx ← counter.modifyGet fun i => (i, i + 1) + -- `#` cannot appear in Noir identifiers, so the auxiliary name can never collide with an + -- extracted definition. let auxId := mkIdent <| Name.mkSimple s!"{baseName.getString!}#lits{idx}" let elemTp ← if isArray then `(Tp.arrayElem $arrTp) else `(Tp.vectorElem $arrTp) + -- Elaborate the auxiliary definition immediately, as its own command: the deep element + -- list is type-checked exactly once, here, and every later mention of the array — in the + -- extracted body and in proof goals — is just this constant. Elab.Command.elabCommand <| ← `(def $auxId ($pId : Prime) : List (Tp.denote $pId $elemTp) := $body) + -- Replace the literal with a raw `Expr.callBuiltin` via the `splice!` escape hatch + -- (bypassing the surface grammar, which has no syntax for data-carrying builtins). The + -- call takes no argument expressions — the elements travel inside the builtin. let repl ← if isArray then `(noir_expr| splice!( Expr.callBuiltin [] $arrTp (Builtin.mkValArray $arrTp $auxId) h![] )) diff --git a/Lampe/Lampe/Tactic/Steps.lean b/Lampe/Lampe/Tactic/Steps.lean index ed1ba6e9..99ee5ef3 100644 --- a/Lampe/Lampe/Tactic/Steps.lean +++ b/Lampe/Lampe/Tactic/Steps.lean @@ -159,10 +159,20 @@ def getClosingTerm (val : Lean.Expr) : TacticM (Option (TSyntax `term)) := withT | ``Lampe.Builtin.mkRepeatedArray => return some (←``(genericTotalPureBuiltin_intro Builtin.mkRepeatedArray (a := (_, _)) rfl)) | ``Lampe.Builtin.mkValArray => + -- `mkValArray` is a parameterized builtin, so the goal mentions it fully applied as + -- `Builtin.mkValArray arrTp vals`. Pull those two arguments out of the goal's + -- builtin expression… let some arrTp := builtin.getAppArgs[0]? | throwError "malformed mkValArray" let some vals := builtin.getAppArgs[1]? | throwError "malformed mkValArray" + -- …reify them back into syntax… let arrTp ← arrTp.toSyntax let vals ← vals.toSyntax + -- …and re-apply them inside the closing term, so that the intro lemma's hypothesis + -- `b = newGenericTotalPureBuiltin sgn desc` unfolds `mkValArray` one step and closes + -- by `rfl`, inferring `sgn`/`desc` from that equation. The generic argument is `()` + -- since `mkValArray` carries all its data in its parameters. The resulting + -- postcondition is `v = Builtin.valArray _ _ (vals p)` — a single shallow constant, + -- regardless of how many elements the literal has. return some (←``(genericTotalPureBuiltin_intro (Builtin.mkValArray $arrTp $vals) (a := ()) rfl)) | ``Lampe.Builtin.arrayIndex => return some (←``(arrayIndex_intro)) @@ -184,6 +194,8 @@ def getClosingTerm (val : Lean.Expr) : TacticM (Option (TSyntax `term)) := withT | ``Lampe.Builtin.mkRepeatedVector => return some (←``(genericTotalPureBuiltin_intro Builtin.mkRepeatedVector (a := _) rfl)) | ``Lampe.Builtin.mkValVector => + -- Same shape as the `mkValArray` case above, with the element type in place of the + -- whole array type. let some tp := builtin.getAppArgs[0]? | throwError "malformed mkValVector" let some vals := builtin.getAppArgs[1]? | throwError "malformed mkValVector" let tp ← tp.toSyntax diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean index adfe9c5e..3d111a70 100644 --- a/Lampe/Lampe/Tp.lean +++ b/Lampe/Lampe/Tp.lean @@ -281,7 +281,17 @@ match tp with end -/-- The element type of an array type (or `.unit` for non-array types). -/ +/-- +The element type of an array type (or `.unit` for non-array types). + +This and the projections below exist so that `Builtin.mkValArray`/`mkValVector` can state their +signatures in terms of the *whole* array/vector type they are given. They are `@[reducible]` so +that e.g. `(Tp.array tp n).arrayElem` reduces to `tp` during unification — the Hoare triple +produced for a `mkValArray` call (see `Tactic/Steps.lean`) is stated at the projected type +`.array arrTp.arrayElem arrTp.arraySize`, and must unify with goals stated at the original +array type. The `.unit`/`0` fallbacks for non-matching types are never reached by the +elaborator; they just make the projections total. +-/ @[reducible] def Tp.arrayElem : Tp → Tp | .array tp _ => tp