From ef45be735f44f894132bec4222b59abdf7b08e07 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sat, 16 May 2026 14:20:43 -0300 Subject: [PATCH 1/2] Better interpreter and stack printer --- Ix/Aiur/Interpret.lean | 58 ++++++++++++++++++++++++++---------------- Kernel.lean | 6 ++--- Tests/Aiur/Common.lean | 4 +-- 3 files changed, 41 insertions(+), 27 deletions(-) diff --git a/Ix/Aiur/Interpret.lean b/Ix/Aiur/Interpret.lean index 45b788f5..95fbe563 100644 --- a/Ix/Aiur/Interpret.lean +++ b/Ix/Aiur/Interpret.lean @@ -35,32 +35,32 @@ private partial def natToHexGo (n : Nat) (acc : String) : String := private def natToHex (n : Nat) : String := if n == 0 then "0" else natToHexGo n "" -partial def ppValue : Value → String +partial def Value.pp : Value → String | .unit => "()" | .field g => toString g.val.toNat - | .tuple vs => "(" ++ String.intercalate ", " (vs.toList.map ppValue) ++ ")" - | .array vs => "[" ++ String.intercalate ", " (vs.toList.map ppValue) ++ "]" + | .tuple vs => "(" ++ String.intercalate ", " (vs.toList.map Value.pp) ++ ")" + | .array vs => "[" ++ String.intercalate ", " (vs.toList.map Value.pp) ++ "]" | .ctor g args => let name := g.toName.toString if args.isEmpty then name - else name ++ "(" ++ String.intercalate ", " (args.toList.map ppValue) ++ ")" + else name ++ "(" ++ String.intercalate ", " (args.toList.map Value.pp) ++ ")" | .fn g => "fn(" ++ g.toName.toString ++ ")" | .pointer _ n => "&0x" ++ natToHex n -instance : ToString Value := ⟨ppValue⟩ +instance : ToString Value := ⟨Value.pp⟩ /-- Pretty-print a `Value` while auto-dereferencing pointers up to `depth` levels. Used by the `dbg!` interpreter helper so users see structured content like `App(Const(3, []), BVar(0))` instead of opaque `&0x123`. -/ -partial def ppValueDeref (store : Store) (depth : Nat) : Value → String +partial def Value.ppDeref (store : Store) (depth : Nat) : Value → String | .unit => "()" | .field g => toString g.val.toNat - | .tuple vs => "(" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store depth)) ++ ")" - | .array vs => "[" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store depth)) ++ "]" + | .tuple vs => "(" ++ String.intercalate ", " (vs.toList.map (Value.ppDeref store depth)) ++ ")" + | .array vs => "[" ++ String.intercalate ", " (vs.toList.map (Value.ppDeref store depth)) ++ "]" | .ctor g args => let name := g.toName.toString if args.isEmpty then name - else name ++ "(" ++ String.intercalate ", " (args.toList.map (ppValueDeref store depth)) ++ ")" + else name ++ "(" ++ String.intercalate ", " (args.toList.map (Value.ppDeref store depth)) ++ ")" | .fn g => "fn(" ++ g.toName.toString ++ ")" | .pointer _ n => if depth == 0 then "&0x" ++ natToHex n @@ -70,8 +70,8 @@ partial def ppValueDeref (store : Store) (depth : Nat) : Value → String -- Stored value is `Array Value`; for tagged enums it's -- typically `[ctor]` or `[tag, fields...]`. Recurse on each. match vs.toList with - | [v] => ppValueDeref store (depth - 1) v - | _ => "[" ++ String.intercalate ", " (vs.toList.map (ppValueDeref store (depth - 1))) ++ "]" + | [v] => Value.ppDeref store (depth - 1) v + | _ => "[" ++ String.intercalate ", " (vs.toList.map (Value.ppDeref store (depth - 1))) ++ "]" | none => "&0x" ++ natToHex n ++ "(unbound)" -- --------------------------------------------------------------------------- @@ -130,6 +130,17 @@ instance : ToString Interrupt where s!" in {g}({argStr})" msg ++ "\nCall stack:\n" ++ String.intercalate "\n" frames +/-- Pretty-print an `Interrupt`, auto-dereferencing pointer values in +the call stack (and the unexpected-return value) up to `depth` levels. -/ +def Interrupt.ppDeref (store : Store) (depth : Nat) : Interrupt → String + | .ret v => s!"unexpected return: {Value.ppDeref store depth v}" + | .error msg [] => msg + | .error msg stack => + let frames := stack.map fun (g, args) => + let argStr := String.intercalate ", " (args.map (Value.ppDeref store depth)) + s!" in {g}({argStr})" + msg ++ "\nCall stack:\n" ++ String.intercalate "\n" frames + -- --------------------------------------------------------------------------- -- Interpreter monad -- --------------------------------------------------------------------------- @@ -139,7 +150,7 @@ structure InterpState where ioBuffer : IOBuffer callCache : Std.HashMap (Global × List Value) Value := {} -abbrev InterpM := StateT InterpState (Except Interrupt) +abbrev InterpM := ExceptT Interrupt (StateM InterpState) private def throwErr (msg : String) : InterpM α := throw (.error msg []) @@ -356,7 +367,7 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu | some t => let v ← interp decls bindings t let store ← getStore - dbg_trace s!"{label}: {ppValueDeref store 16 v}" + dbg_trace s!"{label}: {Value.ppDeref store 16 v}" interp decls bindings cont | .ioGetInfo key => do let keyGs ← expectFieldArray (← interp decls bindings key) @@ -392,15 +403,18 @@ end def runFunction (decls : Decls) (funcName : Global) (inputs : List Value) (ioBuffer : IOBuffer := default) : - Except Interrupt (Value × InterpState) := do - let f ← match decls.getByKey funcName with - | some (.function f) => pure f - | _ => throw (.error s!"Function not found: {funcName}" []) - if inputs.length != f.inputs.length then - throw (.error s!"runFunction: arity mismatch for {funcName}: \ - expected {f.inputs.length}, got {inputs.length}" []) - let bindings := f.inputs.map (·.1) |>.zip inputs - StateT.run (interp decls bindings f.body) { ioBuffer } + Except Interrupt Value × InterpState := + let init : InterpState := { ioBuffer } + match decls.getByKey funcName with + | some (.function f) => + if inputs.length != f.inputs.length then + (.error (.error s!"runFunction: arity mismatch for {funcName}: \ + expected {f.inputs.length}, got {inputs.length}" []), init) + else + let bindings := f.inputs.map (·.1) |>.zip inputs + StateT.run (ExceptT.run (interp decls bindings f.body)) init + | _ => + (.error (.error s!"Function not found: {funcName}" []), init) end Aiur diff --git a/Kernel.lean b/Kernel.lean index 9e1855a1..70ef00bb 100644 --- a/Kernel.lean +++ b/Kernel.lean @@ -73,9 +73,9 @@ where | _ => IO.eprintln s!"{name}: function not found in decls"; return 1 let inputs := Aiur.unflattenInputs decls testCase.input inputTypes match Aiur.runFunction decls funcName inputs testCase.inputIOBuffer with - | .error e => - IO.eprintln s!"{name}: interpreter error:\n{e}" + | (.error e, s) => + IO.eprintln s!"{name}: interpreter error:\n{e.ppDeref s.store 16}" return 1 - | .ok (output, _state) => + | (.ok output, _) => IO.println s!"{name}: {output}" pure 0 diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index 85c10b67..5535d89c 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -66,9 +66,9 @@ def AiurTestEnv.interpTest (env : AiurTestEnv) (testCase : AiurTestCase) let inputs := Aiur.unflattenInputs env.decls testCase.input inputTypes let funcIdx g := env.compiled.getFuncIdx g.toName match Aiur.runFunction env.decls funcName inputs testCase.inputIOBuffer with - | .error e => + | (.error e, _) => test s!"Interpret succeeds for {label}: {e}" false - | .ok (output, state) => + | (.ok output, state) => let flat := Aiur.flattenValue env.decls funcIdx output let interpOutputTest := test s!"Interpret output matches for {label}" (flat == execOutput) From aa71aee69794aa72015b7fa3fc079459b4b9c75f Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sun, 17 May 2026 12:11:37 -0300 Subject: [PATCH 2/2] Stack limit and deref limit --- Ix/Aiur/Interpret.lean | 27 ++++++++++++++++++++------- Kernel.lean | 2 +- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/Ix/Aiur/Interpret.lean b/Ix/Aiur/Interpret.lean index 95fbe563..6f6e7726 100644 --- a/Ix/Aiur/Interpret.lean +++ b/Ix/Aiur/Interpret.lean @@ -63,7 +63,7 @@ partial def Value.ppDeref (store : Store) (depth : Nat) : Value → String else name ++ "(" ++ String.intercalate ", " (args.toList.map (Value.ppDeref store depth)) ++ ")" | .fn g => "fn(" ++ g.toName.toString ++ ")" | .pointer _ n => - if depth == 0 then "&0x" ++ natToHex n + if depth == 0 then "..." else match store.getByIdx n with | some (vs, _) => @@ -130,16 +130,29 @@ instance : ToString Interrupt where s!" in {g}({argStr})" msg ++ "\nCall stack:\n" ++ String.intercalate "\n" frames -/-- Pretty-print an `Interrupt`, auto-dereferencing pointer values in -the call stack (and the unexpected-return value) up to `depth` levels. -/ -def Interrupt.ppDeref (store : Store) (depth : Nat) : Interrupt → String +/-- Pretty-print an `Interrupt`, auto-dereferencing pointer values up to +`depth` pointer-follows, and showing at most `stackLimit` call-stack frames +(starting from the innermost). -/ +def Interrupt.ppDeref (store : Store) (depth : Nat) (stackLimit : Nat) : + Interrupt → String | .ret v => s!"unexpected return: {Value.ppDeref store depth v}" | .error msg [] => msg | .error msg stack => - let frames := stack.map fun (g, args) => + let total := stack.length + let shown := stack.take stackLimit + let rule := String.ofList (List.replicate 80 '─') + let frames := shown.zipIdx.map fun ((g, args), i) => let argStr := String.intercalate ", " (args.map (Value.ppDeref store depth)) - s!" in {g}({argStr})" - msg ++ "\nCall stack:\n" ++ String.intercalate "\n" frames + let header := s!"─── #{i} " ++ g.toName.toString ++ " " + let pad := String.ofList (List.replicate (max 1 (80 - header.length)) '─') + header ++ pad ++ s!"\n {g}({argStr})" + let trailer := if total > stackLimit + then s!"\n... ({total - stackLimit} more frame(s) elided)" + else "" + msg ++ s!"\nCall stack ({total} frames, #0 = innermost):\n" + ++ String.intercalate "\n" frames + ++ trailer + ++ "\n" ++ rule -- --------------------------------------------------------------------------- -- Interpreter monad diff --git a/Kernel.lean b/Kernel.lean index 70ef00bb..54fe8019 100644 --- a/Kernel.lean +++ b/Kernel.lean @@ -74,7 +74,7 @@ where let inputs := Aiur.unflattenInputs decls testCase.input inputTypes match Aiur.runFunction decls funcName inputs testCase.inputIOBuffer with | (.error e, s) => - IO.eprintln s!"{name}: interpreter error:\n{e.ppDeref s.store 16}" + IO.eprintln s!"{name}: interpreter error:\n{e.ppDeref s.store 1 10}" return 1 | (.ok output, _) => IO.println s!"{name}: {output}"