Better interpreter and stack printer

Ix/Aiur/Interpret.lean

@@ -35,43 +35,43 @@ 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
+      if depth == 0 then "..."
       else
         match store.getByIdx n with
         | some (vs, _) =>
             -- 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,30 @@ instance : ToString Interrupt where
           s!"  in {g}({argStr})"
         msg ++ "\nCall stack:\n" ++ String.intercalate "\n" frames
 
+/-- 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 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))
+        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
 -- ---------------------------------------------------------------------------
@@ -139,7 +163,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 +380,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 +416,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
 

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 1 10}"
       return 1
-    | .ok (output, _state) =>
+    | (.ok output, _) =>
       IO.println s!"{name}: {output}"
       pure 0

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)