Automatic RAM encoding selection (elaboration infrastructure)
Lax560851.RamComplexityElab · concepts/Lax560851/RamComplexityElab.lean · lax-560851
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Elaboration infrastructure
This thin frontend expands a mathematical function and two resource bounds into the encoding-explicit RAM predicate. It reuses the closed constructor registry, adding only the fixed list and product presentation combinators. Subtypes erase proofs and finite families keep their intrinsic order. No presentation instances, arbitrary field encoders, or caller-supplied agreement witnesses participate in resolution.
Natural and Boolean outputs have fixed one-word conventions. All other supported outputs use the selected structural arena. uses exactly the same input resolver as .
Concept map
Lean source view on GitHub
| 1 | import Lax560851.CertifiedDerivationElab |
| 2 | import Lax560851.RamComplexity |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Automatic RAM encoding selection (elaboration infrastructure) |
| 7 | type: elaboration infrastructure |
| 8 | --- |
| 9 | |
| 10 | This thin frontend expands a mathematical function and two resource bounds |
| 11 | into the encoding-explicit RAM predicate. It reuses the closed constructor |
| 12 | registry, adding only the fixed list and product presentation combinators. |
| 13 | Subtypes erase proofs and finite families keep their intrinsic order. |
| 14 | No presentation instances, arbitrary field encoders, or caller-supplied |
| 15 | agreement witnesses participate in resolution. |
| 16 | |
| 17 | Natural and Boolean outputs have fixed one-word conventions. All other |
| 18 | supported outputs use the selected structural arena. `inputMagnitude x` |
| 19 | uses exactly the same input resolver as `RamComputableWithin`. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax560851.RamComplexityElab |
| 23 | |
| 24 | open Lean Meta Elab Term |
| 25 | open Lax560851.StructuralPresentation Lax560851.StructuralCombinators |
| 26 | open Lax560851.CertifiedDerivation Lax560851.CertifiedDerivationElab |
| 27 | open Lax560851.RamComplexity |
| 28 | |
| 29 | universe u |
| 30 | |
| 31 | private def subtypeRaw {α : Type u} (raw : α → Raw) (p : α → Prop) |
| 32 | (x : Subtype p) : Raw := raw x.val |
| 33 | |
| 34 | private def familyRaw {n : Nat} {α : Fin n → Type u} |
| 35 | (raw : (i : Fin n) → α i → Raw) (x : (i : Fin n) → α i) : Raw := |
| 36 | Raw.fields (List.ofFn fun i => raw i (x i)) |
| 37 | |
| 38 | /-- Resolve expressions, never pretty-printed syntax or typeclass instances. -/ |
| 39 | private partial def resolveInput (type : Expr) : TermElabM Expr := do |
| 40 | let type ← instantiateMVars type |
| 41 | let type ← instantiateMVars (← whnf type) |
| 42 | if type.hasExprMVar then |
| 43 | -- Binder-local numeral/typeclass constraints may be solved only after |
| 44 | -- the surrounding declaration has finished elaborating its signature. |
| 45 | tryPostpone |
| 46 | throwError "RAM encoding selection needs a fully determined input/output type, got {type}" |
| 47 | if type.isConstOf ``Nat then |
| 48 | return mkConst ``StructuralCombinators.nat |
| 49 | if type.isAppOfArity ``List 1 then |
| 50 | return ← mkAppM ``StructuralCombinators.list #[← resolveInput type.appArg!] |
| 51 | if type.isAppOfArity ``Prod 2 then |
| 52 | let args := type.getAppArgs |
| 53 | let left ← resolveInput args[0]! |
| 54 | let right ← resolveInput args[1]! |
| 55 | return ← mkAppM ``StructuralCombinators.prod #[left, right] |
| 56 | if type.isAppOfArity ``Subtype 2 then |
| 57 | let args := type.getAppArgs |
| 58 | let base ← mkAppM ``Presentation.toRaw #[← resolveInput args[0]!] |
| 59 | let raw ← mkAppM ``subtypeRaw #[base, args[1]!] |
| 60 | return ← mkAppM ``presentationOf #[raw] |
| 61 | if let .forallE name domain body bi := type then |
| 62 | let domain ← whnf domain |
| 63 | if domain.isAppOfArity ``Fin 1 then |
| 64 | return ← withLocalDecl name bi domain fun i => do |
| 65 | let raw ← mkAppM ``Presentation.toRaw #[← resolveInput (body.instantiate1 i)] |
| 66 | let family ← mkAppM ``familyRaw #[← mkLambdaFVars #[i] raw] |
| 67 | mkAppM ``presentationOf #[family] |
| 68 | let witness ← resolveCertifiedField type |
| 69 | let raw ← mkAppM ``CertifiedFieldEncoding.toRaw #[witness] |
| 70 | mkAppM ``presentationOf #[raw] |
| 71 | |
| 72 | private def resolveOutput (type : Expr) : TermElabM Expr := do |
| 73 | let type ← whnf type |
| 74 | if type.isConstOf ``Nat then return mkConst ``natOutput |
| 75 | if type.isConstOf ``Bool then return mkConst ``boolOutput |
| 76 | let raw ← mkAppM ``Presentation.toRaw #[← resolveInput type] |
| 77 | mkAppM ``arenaOutput #[raw] |
| 78 | |
| 79 | elab "RamComputableWithin " f:term:max time:term:max words:term:max : term => do |
| 80 | let f ← elabTerm f none |
| 81 | synthesizeSyntheticMVarsNoPostponing |
| 82 | let type ← whnf (← inferType f) |
| 83 | let .forallE _ domain body _ := type |
| 84 | | throwError "RamComputableWithin expects a function" |
| 85 | if body.hasLooseBVars then |
| 86 | throwError "RamComputableWithin expects a nondependent result type; bundle dependent data into an input datatype" |
| 87 | let input ← resolveInput domain |
| 88 | let output ← resolveOutput body |
| 89 | let boundType ← mkArrow domain (mkConst ``Nat) |
| 90 | let time ← elabTermEnsuringType time (some boundType) |
| 91 | let words ← elabTermEnsuringType words (some boundType) |
| 92 | mkAppM ``RamComputableWithinUsing #[input, output, f, time, words] |
| 93 | |
| 94 | elab "inputMagnitude " x:term:max : term => do |
| 95 | let x ← elabTerm x none |
| 96 | synthesizeSyntheticMVarsNoPostponing |
| 97 | let input ← resolveInput (← inferType x) |
| 98 | mkAppM ``inputMagnitudeUsing #[input, x] |
| 99 | |
| 100 | end Lax560851.RamComplexityElab |
| 101 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments