chore: Switch to module system

Benchmarks/Compile/CompileFLT.lean

@@ -1,2 +1 @@
 import FLT
-

Ix.lean

@@ -1,14 +1,15 @@
 -- This module serves as the root of the `Ix` library.
 -- Import modules here that should be built as part of the library.
-import Ix.Environment
-import Ix.CanonM
-import Ix.Ixon
-import Ix.Sharing
-import Ix.Meta
-import Ix.GraphM
-import Ix.CondenseM
-import Ix.CompileM
-import Ix.DecompileM
-import Ix.Claim
-import Ix.Commit
-import Ix.Benchmark.Bench
+module
+public import Ix.Environment
+public import Ix.CanonM
+public import Ix.Ixon
+public import Ix.Sharing
+public import Ix.Meta
+public import Ix.GraphM
+public import Ix.CondenseM
+public import Ix.CompileM
+public import Ix.DecompileM
+public import Ix.Claim
+public import Ix.Commit
+public import Ix.Benchmark.Bench

Ix/Address.lean

@@ -1,7 +1,10 @@
-import Lean
-import Ix.ByteArray
-import Ix.Common
-import Blake3
+module
+public import Lean.ToExpr
+public import Ix.ByteArray
+public import Ix.Common
+public import Blake3
+
+public section
 
 deriving instance Lean.ToExpr for ByteArray
 deriving instance Repr for ByteArray
@@ -117,3 +120,4 @@ def Address.fromUniqueName (name: Lean.Name) : Option Address :=
   | .str (.str (.str .anonymous "Ix") "_#") s => Address.fromString s
   | _ => .none
 
+end

Ix/Aiur/Bytecode.lean

@@ -1,4 +1,7 @@
-import Ix.Aiur.Goldilocks
+module
+public import Ix.Aiur.Goldilocks
+
+public section
 
 namespace Aiur
 
@@ -76,3 +79,5 @@ structure Toplevel where
 end Bytecode
 
 end Aiur
+
+end

Ix/Aiur/Check.lean

@@ -1,5 +1,8 @@
-import Ix.Aiur.Term
-import Std.Data.HashSet
+module
+public import Ix.Aiur.Term
+public import Std.Data.HashSet
+
+public section
 
 namespace Aiur
 
@@ -473,3 +476,5 @@ def checkFunction (function : Function) : CheckM TypedFunction := do
   pure ⟨function.name, function.inputs, function.output, body, function.unconstrained⟩
 
 end Aiur
+
+end

Ix/Aiur/Compile.lean

@@ -1,7 +1,10 @@
-import Std.Data.HashMap
-import Lean.Data.RBTree
-import Ix.Aiur.Term
-import Ix.Aiur.Bytecode
+module
+public import Std.Data.HashMap
+public import Lean.Data.RBTree
+public import Ix.Aiur.Term
+public import Ix.Aiur.Bytecode
+
+public section
 
 namespace Aiur
 
@@ -643,3 +646,5 @@ def TypedDecls.compile (decls : TypedDecls) : Except String Bytecode.Toplevel :=
   pure ⟨functions, memSizes.toArray⟩
 
 end Aiur
+
+end

Ix/Aiur/Goldilocks.lean

@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Aiur
 
 abbrev gSize : UInt64 := 1 - 2 ^ 32
@@ -19,3 +23,5 @@ instance : OfNat G n := ⟨G.ofNat n⟩
   ⟨u64, h⟩
 
 end Aiur
+
+end

Ix/Aiur/Match.lean

@@ -1,5 +1,8 @@
-import Ix.Aiur.Term
-import Ix.SmallMap
+module
+public import Ix.Aiur.Term
+public import Ix.SmallMap
+
+public section
 
 namespace Aiur
 
@@ -236,3 +239,5 @@ partial def decisionToTerm : Decision → Option Term
 end
 
 end Aiur
+
+end

Ix/Aiur/Meta.lean

@@ -1,5 +1,9 @@
-import Lean
-import Ix.Aiur.Term
+module
+public import Lean.Elab
+public import Lean.Elab.Term.TermElabM
+public import Ix.Aiur.Term
+
+public meta section
 
 namespace Aiur
 
@@ -492,3 +496,5 @@ def elabToplevel : ElabStxCat `toplevel
 elab "⟦" t:toplevel "⟧" : term => elabToplevel t
 
 end Aiur
+
+end

Ix/Aiur/Protocol.lean

@@ -1,5 +1,8 @@
-import Ix.Aiur.Bytecode
-import Std.Data.HashMap
+module
+public import Ix.Aiur.Bytecode
+public import Std.Data.HashMap
+
+public section
 
 namespace Aiur
 
@@ -76,3 +79,5 @@ def buildClaim (funIdx : Bytecode.FunIdx) (input output : Array G) :=
   #[functionChannel, .ofNat funIdx] ++ input ++ output
 
 end Aiur
+
+end

Ix/Aiur/Simple.lean

@@ -1,5 +1,8 @@
-import Ix.Aiur.Match
-import Ix.Aiur.Check
+module
+public import Ix.Aiur.Match
+public import Ix.Aiur.Check
+
+public section
 
 namespace Aiur
 
@@ -47,3 +50,5 @@ def Toplevel.checkAndSimplify (toplevel : Toplevel) : Except CheckError TypedDec
       pure $ typedDecls.insert name (.function f)
 
 end Aiur
+
+end

Ix/Aiur/Term.lean

@@ -1,6 +1,9 @@
-import Std.Data.HashSet.Basic
-import Ix.Aiur.Goldilocks
-import Ix.IndexMap
+module
+public import Std.Data.HashSet.Basic
+public import Ix.Aiur.Goldilocks
+public import Ix.IndexMap
+
+public section
 
 namespace Aiur
 
@@ -272,3 +275,5 @@ partial def DataType.size (dt : DataType) (decls : TypedDecls)
 end
 
 end Aiur
+
+end

Ix/Benchmark/Bench.lean

@@ -1,11 +1,14 @@
-import Ix.Address
-import Ix.Meta
-import Ix.Cronos
-import Ix.Address
-import Batteries
+module
+public import Ix.Address
+public import Ix.Meta
+public import Ix.Cronos
+public import Ix.Address
+public import Batteries
 
-import Ix.Benchmark.Serde
-import Ix.Benchmark.Tukey
+public import Ix.Benchmark.Serde
+public import Ix.Benchmark.Tukey
+
+public section
 
 open Batteries (RBMap)
 
@@ -329,7 +332,7 @@ def getColumnWidths (report : Array BenchReport) : ColumnWidths :=
 
 -- Centers a string with padded whitespace given the total width
 def padWhitespace (input : String) (width : Nat) : String :=
-  let padWidth := width - input.length 
+  let padWidth := width - input.length
   let leftPad := padWidth / 2
   let rightPad := padWidth - leftPad
   String.ofList (List.replicate leftPad ' ') ++ input ++ (String.ofList (List.replicate rightPad ' '))
@@ -449,3 +452,4 @@ def bgroup {α β : Type} (name: String) (benches : List (Benchmarkable α β))
     IO.FS.writeFile (System.mkFilePath [".", s!"benchmark-report-{name}.md"]) table
   return reports
 
+end

Ix/Benchmark/Change.lean

@@ -1,4 +1,7 @@
-import Ix.Benchmark.Data
+module
+public import Ix.Benchmark.Data
+
+public section
 
 -- TODO: Use in `MeasurementData` and save outliers in `tukey.json`
 structure LabeledSample where
@@ -83,3 +86,5 @@ def changeEstimates (newAvgTimes baseAvgTimes : Distribution) (config : Config)
   let (mean, median) := changeStats newAvgTimes baseAvgTimes
   let changeEstimates := buildChangeEstimates changeDistributions mean median config.confidenceLevel
   (changeEstimates, changeDistributions)
+
+end

Ix/Benchmark/Common.lean

@@ -1,3 +1,7 @@
+module
+
+public section
+
 inductive SamplingMode where
   | flat : SamplingMode
   | linear : SamplingMode
@@ -106,3 +110,5 @@ def Float.formatNanos (f : Float) : String :=
     (f / 10 ^ 3).floatPretty 2 ++ "µs"
   else
     f.floatPretty 2  ++ "ns"
+
+end

Ix/Benchmark/Data.lean

@@ -1,4 +1,7 @@
-import Ix.Benchmark.Distribution
+module
+public import Ix.Benchmark.Distribution
+
+public section
 
 structure Data where
   d : Array (Nat × Nat)
@@ -50,3 +53,5 @@ def Data.regression (data : Data) (config : Config) (gen : StdGen) : (Distributi
   let stdErr := distribution.stdDev mean
   let estimate : Estimate := { confidenceInterval, pointEstimate, stdErr }
   (distribution, estimate)
+
+end

Ix/Benchmark/Distribution.lean

@@ -1,5 +1,8 @@
-import Ix.Benchmark.Common
-import Ix.Benchmark.Estimate
+module
+public import Ix.Benchmark.Common
+public import Ix.Benchmark.Estimate
+
+public section
 
 -- TODO: Ensure all array instances are used linearly for optimal performance
 structure Distribution where
@@ -117,3 +120,5 @@ def Distribution.estimates (avgTimes : Distribution) (config : Config) (gen : St
   let dists := ((avgTimes.bootstrap config.numSamples config.bootstrapSamples).run gen).fst
   let est := dists.buildEstimates points config.confidenceLevel
   (dists, est)
+
+end

Ix/Benchmark/Estimate.lean

@@ -1,4 +1,7 @@
-import Lean.Data.Json
+module
+public import Lean.Data.Json
+
+public section
 
 structure ConfidenceInterval where
   confidenceLevel : Float
@@ -26,3 +29,4 @@ structure PointEstimates where
   medianAbsDev : Float
   stdDev : Float
 
+end

Ix/Benchmark/OneShot.lean

@@ -1,6 +1,10 @@
-import Lean.Data.Json.FromToJson
+module
+public import Lean.Data.Json.FromToJson
+
+public section
 
 structure OneShot where
   benchTime : Nat
   deriving Lean.ToJson, Lean.FromJson, Repr
 
+end

Ix/Benchmark/Serde.lean

@@ -1,6 +1,9 @@
-import Ix.Ixon
-import Ix.Benchmark.Change
-import Ix.Benchmark.OneShot
+module
+public import Ix.Ixon
+public import Ix.Benchmark.Change
+public import Ix.Benchmark.OneShot
+
+public section
 
 open Ixon
 
@@ -154,3 +157,5 @@ def loadFile [Lean.FromJson α] [Serialize α] (format : SerdeFormat) (path : Sy
   match format with
   | .json => loadJson path
   | .ixon => loadIxon path
+
+end

Ix/Benchmark/Tukey.lean

@@ -1,4 +1,7 @@
-import Ix.Benchmark.Distribution
+module
+public import Ix.Benchmark.Distribution
+
+public section
 
 /-- Outliers are classified per https://bheisler.github.io/criterion.rs/book/analysis.html#outlier-classification -/
 structure Outliers where
@@ -47,3 +50,5 @@ def Distribution.tukey (data : Distribution) : IO Unit := do
     if out.highSevere > 0 then
       let pct := Float.ofNat out.highSevere / (Float.ofNat samples) * 100
       IO.println s!"  {out.highSevere} ({pct.floatPretty 2}%) high severe"
+
+end

Ix/ByteArray.lean

@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace ByteArray
 
 def beqNoFFI (a b : ByteArray) : Bool :=
@@ -10,3 +14,5 @@ def beq : @& ByteArray → @& ByteArray → Bool :=
 instance : BEq ByteArray := ⟨ByteArray.beq⟩
 
 end ByteArray
+
+end