Rebrand to ImpLab and split debugger into DAP/Widget

.vscode/launch.json

@@ -2,15 +2,15 @@
   "version": "0.2.0",
   "configurations": [
     {
-      "name": "Toy DAP (auto-export ProgramInfo)",
+      "name": "ImpLab Toy DAP (auto-export ProgramInfo)",
       "type": "lean-toy-dap",
       "request": "launch",
       "source": "${workspaceFolder}/examples/Main.lean",
       "stopOnEntry": true,
-      "preLaunchTask": "Generate Toy DAP ProgramInfo"
+      "preLaunchTask": "Generate ImpLab ProgramInfo"
     },
     {
-      "name": "Toy DAP (sample ProgramInfo fallback)",
+      "name": "ImpLab Toy DAP (sample ProgramInfo fallback)",
       "type": "lean-toy-dap",
       "request": "launch",
       "source": "${file}",

.vscode/tasks.json

@@ -2,14 +2,14 @@
   "version": "2.0.0",
   "tasks": [
     {
-      "label": "Generate Toy DAP ProgramInfo",
+      "label": "Generate ImpLab ProgramInfo",
       "type": "process",
       "command": "lake",
       "args": [
         "exe",
         "dap-export",
         "--decl",
-        "Dap.Lang.Examples.mainProgram",
+        "ImpLab.Lang.Examples.mainProgram",
         "--out",
         ".dap/programInfo.generated.json"
       ],

AGENTS.md

@@ -1,16 +1,15 @@
 # AGENTS
 
 ## Scope and priorities
-- Educational Lean 4 toy language + debugger.
+- Educational Lean 4 playground for language modeling and debugger experimentation.
 - Optimize for clarity and maintainability, not performance.
 - Avoid compatibility shims during refactors; prefer direct clean structure.
 
 ## Main surfaces
-- Runtime: `Dap/Lang/*.lean`
-- Debugger source of truth: `Dap/Debugger/Core.lean`
-- Session semantics: `Dap/Debugger/Session.lean`
-- Lean RPC transport: `Dap/Widget/Server.lean`
-- StdIO DAP transport: `Dap/DAP/Stdio.lean` + `app/ToyDap.lean`
+- Language runtime and semantics: `ImpLab/Lang/*.lean`
+- Debugger subsystem: `ImpLab/Debugger/*`
+- Executables: `app/`
+- Tests: `Test/`
 - VS Code client: `client/`
 
 ## Build/test commands
@@ -20,28 +19,14 @@
 - `lake exe dap-export --help`
 - `cd client && npm run compile`
 
-## Architecture guardrails
-- Put new debugger behavior in `Dap/Debugger/Core.lean` first, then wire transports.
-- Keep transport files as adapters only; avoid protocol/state duplication.
-- Treat `ProgramInfo` as canonical across launch/debug/export flows.
-- `Program` remains function-only (`functions : Array FuncDef`) with required `main`.
-- Keep source mapping coherent (function + statement line <-> source line).
-
-## Language and API conventions
-- `dap%[...]` is the only DSL elaborator and must produce `ProgramInfo`.
-- `dap%[...]` accepts functions only and must include `main()` (zero params).
+## Global conventions
+- `imp%[...]` is the only DSL elaborator and must produce `ProgramInfo`.
+- `imp%[...]` accepts functions only and must include `main()` (zero params).
 - Keep `mainProgram` as default fixture entrypoint in `examples/Main.lean`.
 - Prefer `initialize` over `builtin_initialize` in project code.
-- Preserve stable DAP JSON payload shapes.
-
-## Testing split
-- Core behavior tests: `Dap/Debugger/Core.lean` APIs.
-- Transport tests: framing/serialization + request-to-core wiring.
-- DAP sanity tests: lifecycle ordering + at least one breakpoint hit path.
 
-## Review checklist
-- Is behavior duplicated in `Server.lean`/`Stdio.lean` that belongs in core?
-- Any hardcoded entrypoint/decl list that should be generalized?
-- Any duplicated decode/source-mapping logic that can drift?
-- Are stack/breakpoint lines mapped correctly for all functions via `ProgramInfo`?
-- Are lifecycle events ordered correctly (`initialized`, `stopped`, `continued`, `terminated`)?
+## Subsystem-local instructions
+- Debugger-specific rules and review checklist live in:
+  - `ImpLab/Debugger/AGENTS.md`
+- Debugger active work tracking lives in:
+  - `docs/debugger-roadmap.md`

ImpLab.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import ImpLab.Lang.Ast
+import ImpLab.Lang.Dsl
+import ImpLab.Lang.Eval
+import ImpLab.Lang.History
+import ImpLab.Lang.Trace
+import ImpLab.Debugger.Session
+import ImpLab.Debugger.Core
+import ImpLab.Debugger.DAP.Resolve
+import ImpLab.Debugger.DAP.Launch
+import ImpLab.Debugger.DAP.Export
+import ImpLab.Debugger.DAP.Capabilities
+import ImpLab.Debugger.Widget.Types
+import ImpLab.Debugger.Widget.UI
+import ImpLab.Debugger.Widget.Server
+import examples.Main

ImpLab/Debugger/AGENTS.md

@@ -0,0 +1,30 @@
+# Debugger AGENTS
+
+## Scope
+Applies to work under `ImpLab/Debugger/*`, `app/ToyDap.lean`, `app/ExportMain.lean`, and debugger-focused tests.
+Active debugger backlog and priorities are tracked in `docs/debugger-roadmap.md`.
+
+## Source of truth
+- Debugger behavior: `ImpLab/Debugger/Core.lean`
+- Session semantics: `ImpLab/Debugger/Session.lean`
+- DAP transport: `ImpLab/Debugger/DAP/Stdio.lean`
+- Widget transport: `ImpLab/Debugger/Widget/Server.lean`
+
+## Rules
+- Put new debugger behavior in `Core.lean` first, then wire transports.
+- Keep transport files as adapters only; avoid protocol/state duplication.
+- Treat `ProgramInfo` as canonical across launch/debug/export flows.
+- Keep source mapping coherent (function + statement line <-> source line).
+- Preserve stable DAP JSON payload shapes.
+
+## Testing split
+- Core behavior tests: `Test/Core.lean`.
+- Transport tests: `Test/Transport.lean`.
+- DAP sanity must include lifecycle ordering and at least one breakpoint hit path.
+
+## Review checklist
+- Is behavior duplicated in `Widget/Server.lean` or `DAP/Stdio.lean` that belongs in core?
+- Any hardcoded entrypoint/decl list that should be generalized?
+- Any duplicated decode/source-mapping logic that can drift?
+- Are stack and breakpoint lines mapped correctly for all functions via `ProgramInfo`?
+- Are lifecycle events ordered correctly (`initialized`, `stopped`, `continued`, `terminated`)?

Dap/Debugger/Core.lean → ImpLab/Debugger/Core.lean

@@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
-import Dap.Debugger.Session
+import ImpLab.Debugger.Session
 
 open Lean
 
-namespace Dap
+namespace ImpLab
 
 inductive SessionStatus where
   | stopped
@@ -322,4 +322,4 @@ def disconnect (store : SessionStore) (sessionId : Nat) : SessionStore × Bool :
 def inspectSession (store : SessionStore) (sessionId : Nat) : Except String SessionData :=
   getSessionData store sessionId
 
-end Dap
+end ImpLab

Dap/DAP/Capabilities.lean → ImpLab/Debugger/DAP/Capabilities.lean

@@ -8,7 +8,7 @@ import Lean
 
 open Lean
 
-namespace Dap
+namespace ImpLab
 
 structure DapCapabilities where
   supportsConfigurationDoneRequest : Bool := true
@@ -19,4 +19,4 @@ structure DapCapabilities where
 def dapCapabilities : DapCapabilities :=
   {}
 
-end Dap
+end ImpLab

Dap/DAP/Export.lean → ImpLab/Debugger/DAP/Export.lean

@@ -5,13 +5,13 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
-import Dap.Lang.Ast
-import Dap.DAP.Resolve
+import ImpLab.Lang.Ast
+import ImpLab.Debugger.DAP.Resolve
 import examples.Main
 
 open Lean
 
-namespace Dap.Export
+namespace ImpLab.Export
 
 structure CliOptions where
   decl : String := "mainProgram"
@@ -24,13 +24,13 @@ def usage : String := String.intercalate "\n"
     "",
     "Export a DAP payload from a Lean declaration.",
     "",
-    "--decl must point to a Dap.ProgramInfo declaration.",
+    "--decl must point to a ImpLab.ProgramInfo declaration.",
     "",
     "Default: --decl mainProgram",
     "Name resolution for unqualified names tries:",
     "  1) <name>",
     "  2) Main.<name>",
-    "  3) Dap.Lang.Examples.<name>" ]
+    "  3) ImpLab.Lang.Examples.<name>" ]
 
 private def parseArgs : CliOptions → List String → Except String CliOptions
   | opts, [] =>
@@ -55,28 +55,28 @@ private def normalizeDeclName (raw : String) : String :=
 
 private unsafe def evalProgramInfo
     (env : Environment) (opts : Options) (decl : Name) : Except String ProgramInfo := do
-  match env.evalConstCheck ProgramInfo opts ``Dap.ProgramInfo decl with
+  match env.evalConstCheck ProgramInfo opts ``ImpLab.ProgramInfo decl with
   | .ok info =>
     info.validate
   | .error infoErr =>
-    throw s!"Declaration '{decl}' is not Dap.ProgramInfo.\nProgramInfo error: {infoErr}"
+    throw s!"Declaration '{decl}' is not ImpLab.ProgramInfo.\nProgramInfo error: {infoErr}"
 
 private def loadProgramInfoFromDecl (rawDecl : String) : IO ProgramInfo := do
   let sysroot ← Lean.findSysroot
   Lean.initSearchPath sysroot [System.FilePath.mk ".lake/build/lib/lean"]
   let declName ←
-    match Dap.parseDeclName? rawDecl with
+    match ImpLab.parseDeclName? rawDecl with
     | some n => pure n
     | none => throw <| IO.userError s!"Invalid declaration name '{rawDecl}'"
-  let env ← Dap.importProjectEnv
+  let env ← ImpLab.importProjectEnv
   let opts : Options := {}
-  let candidates := Dap.candidateDeclNames declName (moduleName? := some `Main)
-  let resolved? := Dap.resolveFirstDecl? env candidates
+  let candidates := ImpLab.candidateDeclNames declName (moduleName? := some `Main)
+  let resolved? := ImpLab.resolveFirstDecl? env candidates
   let resolved ←
     match resolved? with
     | some n => pure n
     | none =>
-      let attempted := Dap.renderCandidateDecls candidates
+      let attempted := ImpLab.renderCandidateDecls candidates
       throw <| IO.userError s!"Could not resolve declaration '{rawDecl}'. Tried: {attempted}"
   match unsafe evalProgramInfo env opts resolved with
   | .ok info => pure info
@@ -107,4 +107,4 @@ def run (args : List String) : IO Unit := do
   writeJsonFile opts.out content
   IO.println s!"Wrote {opts.out} from {normalizeDeclName opts.decl}"
 
-end Dap.Export
+end ImpLab.Export

Dap/DAP/Launch.lean → ImpLab/Debugger/DAP/Launch.lean

@@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
-import Dap.Lang.Ast
+import ImpLab.Lang.Ast
 
 open Lean
 
-namespace Dap
+namespace ImpLab
 
 def decodeProgramInfoJson (json : Json) : Except String ProgramInfo :=
   match (fromJson? json : Except String ProgramInfo) with
@@ -18,4 +18,4 @@ def decodeProgramInfoJson (json : Json) : Except String ProgramInfo :=
   | .error err =>
     throw s!"Invalid 'programInfo' payload: {err}"
 
-end Dap
+end ImpLab

Dap/DAP/Resolve.lean → ImpLab/Debugger/DAP/Resolve.lean

@@ -8,7 +8,7 @@ import Lean
 
 open Lean
 
-namespace Dap
+namespace ImpLab
 
 def parseDeclName? (raw : String) : Option Name :=
   let parts := raw.trimAscii.toString.splitOn "." |>.filter (· != "")
@@ -42,7 +42,7 @@ def candidateDeclNames
       | none =>
         names
     if includeExamples then
-      pushIfMissing names (`Dap.Lang.Examples ++ decl)
+      pushIfMissing names (`ImpLab.Lang.Examples ++ decl)
     else
       names
   else
@@ -56,7 +56,7 @@ def renderCandidateDecls (candidates : Array Name) : String :=
 
 def importProjectEnv : IO Environment := do
   let candidates : Array (Array Name) :=
-    #[#[`Main, `Dap], #[`Main], #[`Dap]]
+    #[#[`Main, `ImpLab], #[`Main], #[`ImpLab]]
   let rec go (idx : Nat) : IO Environment := do
     if h : idx < candidates.size then
       let modules := candidates[idx]
@@ -66,7 +66,7 @@ def importProjectEnv : IO Environment := do
       catch _ =>
         go (idx + 1)
     else
-      throw <| IO.userError "Could not import project modules (`Main` or `Dap`) to resolve declaration"
+      throw <| IO.userError "Could not import project modules (`Main` or `ImpLab`) to resolve declaration"
   go 0
 
-end Dap
+end ImpLab