From 64ac47d84532d92f3d6e9560913f358c6099fd5e Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 13 Aug 2026 22:01:49 -0700 Subject: [PATCH] refactor(Encoding): move the rose-tree `Data` type into the encoding layer `Data` and the `DataEncode` typeclass are machine-independent: `Data` is the rose tree the RTM operates on, but it is also the target every `DataEncode` instance encodes into, so it does not belong under `Models/RoseTreeMachine/`. Move `Models/RoseTreeMachine/Data.lean` to `Encoding/Data.lean` and `Models/RoseTreeMachine/DataEncode.lean` to `Encoding/DataEncode.lean`, and repoint the three import statements that referred to the old paths. Nothing else changes. `Encoding/Data.lean` is byte-identical to the file it replaces; `Encoding/DataEncode.lean` differs only in its own import of `Data`. Namespaces, module docs, comments and declarations are all untouched, so the `Complexity.RoseTreeMachine` namespace is preserved for now. Co-Authored-By: Claude Fable 5 --- Complexitylib/{Models/RoseTreeMachine => Encoding}/Data.lean | 0 .../{Models/RoseTreeMachine => Encoding}/DataEncode.lean | 2 +- Complexitylib/Models.lean | 4 ++-- Complexitylib/Models/RoseTreeMachine/Prog.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) rename Complexitylib/{Models/RoseTreeMachine => Encoding}/Data.lean (100%) rename Complexitylib/{Models/RoseTreeMachine => Encoding}/DataEncode.lean (98%) diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Encoding/Data.lean similarity index 100% rename from Complexitylib/Models/RoseTreeMachine/Data.lean rename to Complexitylib/Encoding/Data.lean diff --git a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean b/Complexitylib/Encoding/DataEncode.lean similarity index 98% rename from Complexitylib/Models/RoseTreeMachine/DataEncode.lean rename to Complexitylib/Encoding/DataEncode.lean index d2409157..6059428c 100644 --- a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean +++ b/Complexitylib/Encoding/DataEncode.lean @@ -5,7 +5,7 @@ Authors: Christian Reitwiessner -/ module -public import Complexitylib.Models.RoseTreeMachine.Data +public import Complexitylib.Encoding.Data public import Mathlib.Data.Nat.Bits public import Mathlib.Data.List.Basic diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean index ae8ecc48..fdb7abca 100644 --- a/Complexitylib/Models.lean +++ b/Complexitylib/Models.lean @@ -67,8 +67,8 @@ public import Complexitylib.Models.TuringMachine.UTM.ClockedUtm public import Complexitylib.Models.TuringMachine.UTM.HierarchySupport public import Complexitylib.Models.TuringMachine.UTM.Diagonal public import Complexitylib.Models.RandomAccessMachine -public import Complexitylib.Models.RoseTreeMachine.Data -public import Complexitylib.Models.RoseTreeMachine.DataEncode +public import Complexitylib.Encoding.Data +public import Complexitylib.Encoding.DataEncode public import Complexitylib.Models.RoseTreeMachine.Prog /-! diff --git a/Complexitylib/Models/RoseTreeMachine/Prog.lean b/Complexitylib/Models/RoseTreeMachine/Prog.lean index 73adbc2e..6af0b6f7 100644 --- a/Complexitylib/Models/RoseTreeMachine/Prog.lean +++ b/Complexitylib/Models/RoseTreeMachine/Prog.lean @@ -5,7 +5,7 @@ Authors: Christian Reitwiessner -/ module -public import Complexitylib.Models.RoseTreeMachine.DataEncode +public import Complexitylib.Encoding.DataEncode public import Mathlib.Order.Lattice public import Std.Tactic.BVDecide.Normalize.Prop