From bb002a4d92ef1e65197866ec17a15aadca659270 Mon Sep 17 00:00:00 2001 From: imiel Date: Sun, 19 Apr 2026 14:22:34 +0000 Subject: [PATCH] Rehydrate binder names during quoting so diagnostics stop hemorrhaging raw de bruijn indices --- BidirTT/Pretty.lean | 97 ++++++++++++++++++++++++++++++++++----------- Tests.lean | 27 ++++++++++++- 2 files changed, 100 insertions(+), 24 deletions(-) diff --git a/BidirTT/Pretty.lean b/BidirTT/Pretty.lean index 7425644..74596ab 100644 --- a/BidirTT/Pretty.lean +++ b/BidirTT/Pretty.lean @@ -3,33 +3,84 @@ import BidirTT.Syntax namespace BidirTT mutual - partial def prettyTm : Tm → String - | .var i => s!"#{i}" - | .lam t => s!"(fun => {prettyTm t})" - | .app t u => s!"({prettyTm t} {prettyTm u})" - | .pi a b => s!"(Pi {prettyTm a} -> {prettyTm b})" - | .sig a b => s!"(Sigma {prettyTm a} * {prettyTm b})" - | .pair t u => s!"({prettyTm t}, {prettyTm u})" - | .fst t => s!"({prettyTm t}.1)" - | .snd t => s!"({prettyTm t}.2)" - | .nat => "Nat" - | .zero => "zero" - | .succ t => s!"(succ {prettyTm t})" + partial def prettyTmWith (names : List Name) (nextFresh : Nat) : Tm → String × Nat + | .var i => + match names[i]? with + | some name => (name, nextFresh) + | none => (s!"#{i}", nextFresh) + | .lam t => + let x := s!"x{nextFresh}" + let (body, nextFresh) := prettyTmWith (x :: names) (nextFresh + 1) t + (s!"(fun {x} => {body})", nextFresh) + | .app t u => + let (pt, nextFresh) := prettyTmWith names nextFresh t + let (pu, nextFresh) := prettyTmWith names nextFresh u + (s!"({pt} {pu})", nextFresh) + | .pi a b => + let x := s!"x{nextFresh}" + let (pa, nextFresh) := prettyTmWith names (nextFresh + 1) a + let (pb, nextFresh) := prettyTmWith (x :: names) nextFresh b + (s!"(Pi ({x} : {pa}) -> {pb})", nextFresh) + | .sig a b => + let x := s!"x{nextFresh}" + let (pa, nextFresh) := prettyTmWith names (nextFresh + 1) a + let (pb, nextFresh) := prettyTmWith (x :: names) nextFresh b + (s!"(Sigma ({x} : {pa}) * {pb})", nextFresh) + | .pair t u => + let (pt, nextFresh) := prettyTmWith names nextFresh t + let (pu, nextFresh) := prettyTmWith names nextFresh u + (s!"({pt}, {pu})", nextFresh) + | .fst t => + let (pt, nextFresh) := prettyTmWith names nextFresh t + (s!"({pt}.1)", nextFresh) + | .snd t => + let (pt, nextFresh) := prettyTmWith names nextFresh t + (s!"({pt}.2)", nextFresh) + | .nat => ("Nat", nextFresh) + | .zero => ("zero", nextFresh) + | .succ t => + let (pt, nextFresh) := prettyTmWith names nextFresh t + (s!"(succ {pt})", nextFresh) | .natElim m z s n => - s!"(natElim {prettyTm m} {prettyTm z} {prettyTm s} {prettyTm n})" - | .unit => "Unit" - | .triv => "tt" + let (pm, nextFresh) := prettyTmWith names nextFresh m + let (pz, nextFresh) := prettyTmWith names nextFresh z + let (ps, nextFresh) := prettyTmWith names nextFresh s + let (pn, nextFresh) := prettyTmWith names nextFresh n + (s!"(natElim {pm} {pz} {ps} {pn})", nextFresh) + | .unit => ("Unit", nextFresh) + | .triv => ("tt", nextFresh) | .unitElim m t u => - s!"(unitElim {prettyTm m} {prettyTm t} {prettyTm u})" - | .empty => "Empty" + let (pm, nextFresh) := prettyTmWith names nextFresh m + let (pt, nextFresh) := prettyTmWith names nextFresh t + let (pu, nextFresh) := prettyTmWith names nextFresh u + (s!"(unitElim {pm} {pt} {pu})", nextFresh) + | .empty => ("Empty", nextFresh) | .emptyElim m e => - s!"(emptyElim {prettyTm m} {prettyTm e})" - | .id a t u => s!"(Id {prettyTm a} {prettyTm t} {prettyTm u})" - | .refl => "refl" + let (pm, nextFresh) := prettyTmWith names nextFresh m + let (pe, nextFresh) := prettyTmWith names nextFresh e + (s!"(emptyElim {pm} {pe})", nextFresh) + | .id a t u => + let (pa, nextFresh) := prettyTmWith names nextFresh a + let (pt, nextFresh) := prettyTmWith names nextFresh t + let (pu, nextFresh) := prettyTmWith names nextFresh u + (s!"(Id {pa} {pt} {pu})", nextFresh) + | .refl => ("refl", nextFresh) | .idElim m r y p => - s!"(idElim {prettyTm m} {prettyTm r} {prettyTm y} {prettyTm p})" - | .univ i => s!"U{i}" - | .letE a t u => s!"(let : {prettyTm a} := {prettyTm t}; {prettyTm u})" + let (pm, nextFresh) := prettyTmWith names nextFresh m + let (pr, nextFresh) := prettyTmWith names nextFresh r + let (py, nextFresh) := prettyTmWith names nextFresh y + let (pp, nextFresh) := prettyTmWith names nextFresh p + (s!"(idElim {pm} {pr} {py} {pp})", nextFresh) + | .univ i => (s!"U{i}", nextFresh) + | .letE a t u => + let x := s!"x{nextFresh}" + let (pa, nextFresh) := prettyTmWith names (nextFresh + 1) a + let (pt, nextFresh) := prettyTmWith names nextFresh t + let (pu, nextFresh) := prettyTmWith (x :: names) nextFresh u + (s!"(let {x} : {pa} := {pt}; {pu})", nextFresh) end +def prettyTm (tm : Tm) : String := + (prettyTmWith [] 0 tm).fst + end BidirTT diff --git a/Tests.lean b/Tests.lean index 848b803..1ab4541 100644 --- a/Tests.lean +++ b/Tests.lean @@ -148,10 +148,35 @@ def runInternalSafetyChecks : IO Bool := do IO.println "FAIL malformed core terms are rejected safely" pure false +def runPrettyPrinterChecks : IO Bool := do + match checkTop Examples.idAnn with + | .ok (tm, ty) => + match renderType ty with + | Except.ok qty => + let termText := BidirTT.prettyTm tm + let typeText := BidirTT.prettyTm qty + let ok := + containsText termText "fun x0 =>" && + containsText typeText "Pi (x0 : U0)" && + !containsText typeText "#" + if ok then + IO.println "PASS pretty printer rehydrates binder names" + pure true + else + IO.println s!"FAIL pretty printer rehydrates binder names (term: {termText}, type: {typeText})" + pure false + | Except.error err => + IO.println s!"FAIL pretty printer rehydrates binder names (could not quote type: {err})" + pure false + | .error err => + IO.println s!"FAIL pretty printer rehydrates binder names (could not elaborate fixture: {err})" + pure false + def main : IO UInt32 := do let results ← cases.mapM runCase let safetyOk ← runInternalSafetyChecks - let allResults := results ++ [safetyOk] + let prettyOk ← runPrettyPrinterChecks + let allResults := results ++ [safetyOk, prettyOk] let failed := allResults.countP (· == false) if failed == 0 then IO.println s!"\n{allResults.length} passed, 0 failed"