diff --git a/DatapathVerification/BitHeap/Basic.lean b/DatapathVerification/BitHeap/Basic.lean index d40ec64..b917dce 100644 --- a/DatapathVerification/BitHeap/Basic.lean +++ b/DatapathVerification/BitHeap/Basic.lean @@ -1,11 +1,11 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain import DatapathVerification.BitHeap.Column -import DatapathVerification.BitHeap.CompressionHelpers import DatapathVerification.BitHeap.Circuit -import DatapathVerification.BitHeap.NaiveCompression -import DatapathVerification.BitHeap.DaddaTree -import DatapathVerification.BitHeap.WallaceTree +import DatapathVerification.BitHeap.Compressors.CompressionHelpers +import DatapathVerification.BitHeap.Compressors.NaiveCompression +import DatapathVerification.BitHeap.Compressors.DaddaTree +import DatapathVerification.BitHeap.Compressors.WallaceTree import DatapathVerification.BitHeap.Examples.Examples import DatapathVerification.BitHeap.Examples.NaiveCompressionExamples import DatapathVerification.BitHeap.Examples.EvalModExamples diff --git a/DatapathVerification/BitHeap/CompressionHelpers.lean b/DatapathVerification/BitHeap/Compressors/CompressionHelpers.lean similarity index 100% rename from DatapathVerification/BitHeap/CompressionHelpers.lean rename to DatapathVerification/BitHeap/Compressors/CompressionHelpers.lean diff --git a/DatapathVerification/BitHeap/DaddaTree.lean b/DatapathVerification/BitHeap/Compressors/DaddaTree.lean similarity index 98% rename from DatapathVerification/BitHeap/DaddaTree.lean rename to DatapathVerification/BitHeap/Compressors/DaddaTree.lean index ce4b595..ed71b18 100644 --- a/DatapathVerification/BitHeap/DaddaTree.lean +++ b/DatapathVerification/BitHeap/Compressors/DaddaTree.lean @@ -19,7 +19,7 @@ following level. import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain import DatapathVerification.BitHeap.Column -import DatapathVerification.BitHeap.CompressionHelpers +import DatapathVerification.BitHeap.Compressors.CompressionHelpers import Std.Data.HashSet open BitHeap diff --git a/DatapathVerification/BitHeap/NaiveCompression.lean b/DatapathVerification/BitHeap/Compressors/NaiveCompression.lean similarity index 100% rename from DatapathVerification/BitHeap/NaiveCompression.lean rename to DatapathVerification/BitHeap/Compressors/NaiveCompression.lean diff --git a/DatapathVerification/BitHeap/WallaceTree.lean b/DatapathVerification/BitHeap/Compressors/WallaceTree.lean similarity index 98% rename from DatapathVerification/BitHeap/WallaceTree.lean rename to DatapathVerification/BitHeap/Compressors/WallaceTree.lean index b7302a1..e9e8309 100644 --- a/DatapathVerification/BitHeap/WallaceTree.lean +++ b/DatapathVerification/BitHeap/Compressors/WallaceTree.lean @@ -1,7 +1,7 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain import DatapathVerification.BitHeap.Column -import DatapathVerification.BitHeap.CompressionHelpers +import DatapathVerification.BitHeap.Compressors.CompressionHelpers import Std.Data.HashSet open BitHeap diff --git a/DatapathVerification/BitHeap/Examples/DaddaTree.lean b/DatapathVerification/BitHeap/Examples/DaddaTree.lean index 6db1ea7..41bfcde 100644 --- a/DatapathVerification/BitHeap/Examples/DaddaTree.lean +++ b/DatapathVerification/BitHeap/Examples/DaddaTree.lean @@ -1,6 +1,6 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain -import DatapathVerification.BitHeap.DaddaTree +import DatapathVerification.BitHeap.Compressors.DaddaTree import DatapathVerification.BitHeap.Examples.PartialProductGenerator namespace BitHeap diff --git a/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean b/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean index 92e2139..43cba34 100644 --- a/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean +++ b/DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean @@ -1,6 +1,6 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain -import DatapathVerification.BitHeap.NaiveCompression +import DatapathVerification.BitHeap.Compressors.NaiveCompression namespace BitHeap diff --git a/DatapathVerification/BitHeap/Examples/PartialProductGenerator.lean b/DatapathVerification/BitHeap/Examples/PartialProductGenerator.lean index 8961b36..9cca820 100644 --- a/DatapathVerification/BitHeap/Examples/PartialProductGenerator.lean +++ b/DatapathVerification/BitHeap/Examples/PartialProductGenerator.lean @@ -1,6 +1,6 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain -import DatapathVerification.BitHeap.WallaceTree +import DatapathVerification.BitHeap.Compressors.WallaceTree namespace BitHeap diff --git a/DatapathVerification/BitHeap/Examples/WallaceTree.lean b/DatapathVerification/BitHeap/Examples/WallaceTree.lean index ac0af53..411c984 100644 --- a/DatapathVerification/BitHeap/Examples/WallaceTree.lean +++ b/DatapathVerification/BitHeap/Examples/WallaceTree.lean @@ -1,6 +1,6 @@ import DatapathVerification.BitHeap.BitHeap import DatapathVerification.BitHeap.Chain -import DatapathVerification.BitHeap.WallaceTree +import DatapathVerification.BitHeap.Compressors.WallaceTree import DatapathVerification.BitHeap.Examples.PartialProductGenerator namespace BitHeap