Migrate Aeneas to the Lean module system

backends/lean/Aeneas.lean

@@ -1,6 +1,7 @@
-import Aeneas.Command
-import Aeneas.Data
-import Aeneas.Do
-import Aeneas.Extract
-import Aeneas.Std
-import Aeneas.Tactic
+module
+public import Aeneas.Command
+public import Aeneas.Data
+public import Aeneas.Do
+public import Aeneas.Extract
+public import Aeneas.Std
+public import Aeneas.Tactic

backends/lean/Aeneas/Command.lean

@@ -1,4 +1,5 @@
-import Aeneas.Command.Decompose
-import Aeneas.Command.Decompose.Tests
-import Aeneas.Command.Decompose.TestsBig
-import Aeneas.Command.Decompose.TestsRec
+module
+public import Aeneas.Command.Decompose
+public import Aeneas.Command.Decompose.Tests
+public import Aeneas.Command.Decompose.TestsBig
+public import Aeneas.Command.Decompose.TestsRec

backends/lean/Aeneas/Command/Decompose/Tests.lean

@@ -1,10 +1,12 @@
 /-
 Tests for the #decompose command
 -/
-import Aeneas.Command.Decompose
-import Aeneas.Std
-import Aeneas.Do.Elab
-import Aeneas.Do.Delab
+module
+public import Aeneas.Command.Decompose
+public import Aeneas.Std
+public import Aeneas.Do.Elab
+public import Aeneas.Do.Delab
+public section
 
 open Aeneas.Std
 open Aeneas.Command.Decompose

backends/lean/Aeneas/Command/Decompose/TestsBig.lean

@@ -1,10 +1,12 @@
 /-
 Big tests for the #decompose command (performance/stress tests)
 -/
-import Aeneas.Command.Decompose
-import Aeneas.Std
-import Aeneas.Do.Elab
-import Aeneas.Do.Delab
+module
+public import Aeneas.Command.Decompose
+public import Aeneas.Std
+public import Aeneas.Do.Elab
+public import Aeneas.Do.Delab
+public section
 
 open Aeneas.Std
 open Aeneas.Command.Decompose

backends/lean/Aeneas/Command/Decompose/TestsRec.lean

@@ -2,10 +2,12 @@
 Tests for `#decompose` on recursive functions (WF recursion, partial_fixpoint,
 structural recursion).
 -/
-import Aeneas.Command.Decompose
-import Aeneas.Std
-import Aeneas.Do.Elab
-import Aeneas.Do.Delab
+module
+public import Aeneas.Command.Decompose
+public import Aeneas.Std
+public import Aeneas.Do.Elab
+public import Aeneas.Do.Delab
+public section
 
 open Aeneas.Std
 open Aeneas.Command.Decompose

backends/lean/Aeneas/Data.lean

@@ -1,11 +1,12 @@
-import Aeneas.Data.Array
-import Aeneas.Data.BitVec
-import Aeneas.Data.Byte
-import Aeneas.Data.Discriminant
-import Aeneas.Data.Fin
-import Aeneas.Data.Int
-import Aeneas.Data.List
-import Aeneas.Data.Nat
-import Aeneas.Data.Range
-import Aeneas.Data.Tuples
-import Aeneas.Data.Vector
+module
+public import Aeneas.Data.Array
+public import Aeneas.Data.BitVec
+public import Aeneas.Data.Byte
+public import Aeneas.Data.Discriminant
+public import Aeneas.Data.Fin
+public import Aeneas.Data.Int
+public import Aeneas.Data.List
+public import Aeneas.Data.Nat
+public import Aeneas.Data.Range
+public import Aeneas.Data.Tuples
+public import Aeneas.Data.Vector

backends/lean/Aeneas/Data/Array.lean

@@ -1,5 +1,7 @@
-import Aeneas.Data.List
-import Aeneas.Tactic.Simp.SimpIfs
+module
+public import Aeneas.Data.List
+public import Aeneas.Tactic.Simp.SimpIfs
+public section
 
 namespace Array
 

backends/lean/Aeneas/Data/BitVec.lean

@@ -1,20 +1,22 @@
-import Init.Data.List.OfFn
-import Init.Data.BitVec.Lemmas
-import Batteries.Data.BitVec.Lemmas
-import Mathlib.Data.Nat.Basic
-import Mathlib.Data.Fin.Basic
-import Mathlib.Data.Nat.Cast.Basic
-import Mathlib.Data.BitVec
-import Mathlib.Tactic.Ring
-import Mathlib.Data.Nat.Bitwise
-import Aeneas.Data.Byte
-import Aeneas.Tactic.Conv.Bvify.Init
-import Aeneas.Tactic.Simp.SimpLists.SimpLists
-import Aeneas.Tactic.Conv.Natify.Natify
-import Aeneas.Tactic.Conv.ZModify.ZModify
-import Aeneas.Data.List
-import Aeneas.Tactic.Simp.SimpScalar
-import Aeneas.Tactic.Solver.Grind.Init
+module
+public import Init.Data.List.OfFn
+public import Init.Data.BitVec.Lemmas
+public import Batteries.Data.BitVec.Lemmas
+public import Mathlib.Data.Nat.Basic
+public import Mathlib.Data.Fin.Basic
+public import Mathlib.Data.Nat.Cast.Basic
+public import Mathlib.Data.BitVec
+public import Mathlib.Tactic.Ring
+public import Mathlib.Data.Nat.Bitwise
+public import Aeneas.Data.Byte
+public import Aeneas.Tactic.Conv.Bvify.Init
+public import Aeneas.Tactic.Simp.SimpLists.SimpLists
+public import Aeneas.Tactic.Conv.Natify.Natify
+public import Aeneas.Tactic.Conv.ZModify.ZModify
+public import Aeneas.Data.List
+public import Aeneas.Tactic.Simp.SimpScalar
+public import Aeneas.Tactic.Solver.Grind.Init
+public section
 
 open Lean
 

backends/lean/Aeneas/Data/Byte.lean

@@ -1,6 +1,8 @@
-import Lean
-import Aeneas.Tactic.Simp.SimpLists.Init
-import Aeneas.Tactic.Simp.SimpScalar.Init
+module
+public import Lean
+public meta import Aeneas.Tactic.Simp.SimpLists.Init
+public meta import Aeneas.Tactic.Simp.SimpScalar.Init
+public section
 
 abbrev Byte := BitVec 8
 abbrev Byte.ofNat := BitVec.ofNat 8

backends/lean/Aeneas/Data/Discriminant.lean

@@ -1,6 +1,9 @@
-import Lean
-import Aeneas.Std.Scalar.Core
-import Aeneas.Std.Scalar.Notations
+module
+public import Lean
+public meta import Aeneas.Std.Scalar.Core
+public import Aeneas.Std.Scalar.Notations
+public meta import Mathlib.Data.List.Monad
+public section
 
 namespace Aeneas
 
@@ -25,7 +28,7 @@ inductive ScalarTy where
 | U8 | U16 | U32 | U64 | U128 | Usize
 | I8 | I16 | I32 | I64 | I128 | Isize
 
-def mkScalarValue (ty : ScalarTy) (val : Nat) : TermElabM Term := do
+meta def mkScalarValue (ty : ScalarTy) (val : Nat) : TermElabM Term := do
   let value := Syntax.mkNumLit (toString val)
   match ty with
   | .U8 => `($(value)#u8)
@@ -41,7 +44,7 @@ def mkScalarValue (ty : ScalarTy) (val : Nat) : TermElabM Term := do
   | .I128 => `($(value)#i128)
   | .Isize => `($(value)#isize)
 
-def mkScalarTy (ty : ScalarTy) : TermElabM Term := do
+meta def mkScalarTy (ty : ScalarTy) : TermElabM Term := do
   match ty with
   | .U8 => `(_root_.Aeneas.Std.U8)
   | .U16 => `(_root_.Aeneas.Std.U16)
@@ -60,7 +63,7 @@ def mkScalarTy (ty : ScalarTy) : TermElabM Term := do
 
 This function is adapted from `Lean.Elab.Deriving.BEq`.
 -/
-def generateReadDiscriminantCmds (declName : Name) (ty : ScalarTy) (discrValues : Option (List Nat)) :
+meta def generateReadDiscriminantCmds (declName : Name) (ty : ScalarTy) (discrValues : Option (List Nat)) :
   TermElabM (List Syntax) := do
   -- Lookup the declaration, which should be an inductive
   let env ← getEnv
@@ -121,27 +124,27 @@ def generateReadDiscriminantCmds (declName : Name) (ty : ScalarTy) (discrValues
   let ty ← mkScalarTy ty
   let auxFunName := Name.mkStr declName "read_discriminant"
   let binders := header.binders
-  let defStx ← `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $ty := $body:term)
+  let defStx ← `(public def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $ty := $body:term)
 
   -- Generate the syntax for the instance
   let binders := binders.extract 0 indVal.numParams
   let args := header.argNames.map mkIdent
-  let instStx ← `(instance $binders:bracketedBinder* : Aeneas.Std.Discriminant ($header.targetType) ($ty) where
+  let instStx ← `(public instance $binders:bracketedBinder* : Aeneas.Std.Discriminant ($header.targetType) ($ty) where
       read_discriminant := @$(mkIdent auxFunName):ident $args*)
 
   --
   pure [defStx, instStx]
 
 /-- Given an inductive declaration name and an optional list of values, generate an instance
 of `Std.Discriminant`. If the list of values is not provided, we use values `0`, `1`, etc. -/
-def generateReadDiscriminant (declName : Name) (ty : ScalarTy) (discrValues : Option (List Nat)) :
+meta def generateReadDiscriminant (declName : Name) (ty : ScalarTy) (discrValues : Option (List Nat)) :
   CommandElabM Unit := do
   let cmds ← liftTermElabM (generateReadDiscriminantCmds declName ty discrValues)
   cmds.forM elabCommand
 
 syntax (name := readDiscriminant) "discriminant" ident ("["num,*"]")? : attr
 
-def elabTypeToken (stx : Syntax) : AttrM ScalarTy :=
+meta def elabTypeToken (stx : Syntax) : AttrM ScalarTy :=
   match stx.getId with
   | `u8 => pure ScalarTy.U8
   | `u16 => pure ScalarTy.U16
@@ -157,7 +160,7 @@ def elabTypeToken (stx : Syntax) : AttrM ScalarTy :=
   | `isize => pure ScalarTy.Isize
   | _ => throwUnsupportedSyntax
 
-def elabReadDiscriminantAttribute (stx : Syntax) : AttrM (ScalarTy × Option (List Nat)) :=
+meta def elabReadDiscriminantAttribute (stx : Syntax) : AttrM (ScalarTy × Option (List Nat)) :=
   withRef stx do
     match stx with
     | `(attr| discriminant $ty) => do
@@ -168,7 +171,7 @@ def elabReadDiscriminantAttribute (stx : Syntax) : AttrM (ScalarTy × Option (Li
       pure (← elabTypeToken ty, some ((x.getElems.toList.map Syntax.isNatLit?).map Option.get!))
     | _ => throwUnsupportedSyntax
 
-initialize discriminantAttribute : AttributeImpl ← do
+public meta initialize discriminantAttribute : AttributeImpl ← do
   let attrImpl : AttributeImpl := {
     name := `readDiscriminant
     descr := "Generates an instance of `Std.Discriminant` for the given inductive"

backends/lean/Aeneas/Data/Fin.lean

@@ -1,6 +1,8 @@
-import Lean
-import Mathlib.Tactic.OfNat
-import Aeneas.Tactic.Solver.ScalarTac.ScalarTac
+module
+public import Lean
+public import Mathlib.Tactic.OfNat
+public import Aeneas.Tactic.Solver.ScalarTac.ScalarTac
+public section
 
 attribute [scalar_tac_simps] Fin.val_ofNat
 

backends/lean/Aeneas/Data/Int.lean

@@ -1,4 +1,6 @@
-import Lean
+module
+public import Lean
+public section
 
 /-- Small helper
 

backends/lean/Aeneas/Data/List.lean

@@ -1 +1,2 @@
-import Aeneas.Data.List.List
+module
+public import Aeneas.Data.List.List

backends/lean/Aeneas/Data/List/List.lean

@@ -1,15 +1,17 @@
 /- Complementary functions and lemmas for the `List` type -/
-
-import Mathlib.Data.List.GetD
-import Aeneas.Tactic.Solver.ScalarTac
-import AeneasMeta.Utils
-import Aeneas.Tactic.Simp.SimpLemmas
-import Aeneas.Data.Nat
-import Aeneas.Tactic.Simp.SimpLists.Init
-import Aeneas.Std.Primitives
-import Aeneas.Tactic.Simp.SimpLists.SimpLists
-import Aeneas.Tactic.Simp.SimpScalar.SimpScalar
-import Aeneas.Tactic.Solver.Grind.Init
+module
+
+public import Mathlib.Data.List.GetD
+public import Aeneas.Tactic.Solver.ScalarTac
+public import AeneasMeta.Utils
+public import Aeneas.Tactic.Simp.SimpLemmas
+public import Aeneas.Data.Nat
+public import Aeneas.Tactic.Simp.SimpLists.Init
+public import Aeneas.Std.Primitives
+public import Aeneas.Tactic.Simp.SimpLists.SimpLists
+public import Aeneas.Tactic.Simp.SimpScalar.SimpScalar
+public import Aeneas.Tactic.Solver.Grind.Init
+public section
 
 namespace List -- We do not use the `Aeneas` namespace on purpose
 

backends/lean/Aeneas/Data/Nat.lean

@@ -1,4 +1,6 @@
-import Lean
+module
+public import Lean
+public section
 
 /-- Small helper
 

backends/lean/Aeneas/Data/Range.lean

@@ -1,5 +1,6 @@
-import Aeneas.Data.Range.DivRange
-import Aeneas.Data.Range.Lemmas
-import Aeneas.Data.Range.MulRange
-import Aeneas.Data.Range.Notations
-import Aeneas.Data.Range.SRRange
+module
+public import Aeneas.Data.Range.DivRange
+public import Aeneas.Data.Range.Lemmas
+public import Aeneas.Data.Range.MulRange
+public import Aeneas.Data.Range.Notations
+public import Aeneas.Data.Range.SRRange

backends/lean/Aeneas/Data/Range/DivRange.lean

@@ -1,3 +1,4 @@
-import Aeneas.Data.Range.DivRange.Basic
-import Aeneas.Data.Range.DivRange.Lemmas
-import Aeneas.Data.Range.DivRange.Notations
+module
+public import Aeneas.Data.Range.DivRange.Basic
+public import Aeneas.Data.Range.DivRange.Lemmas
+public import Aeneas.Data.Range.DivRange.Notations

backends/lean/Aeneas/Data/Range/DivRange/Basic.lean

@@ -1,6 +1,8 @@
-import Mathlib.Data.Nat.Basic
-import Mathlib.Algebra.Group.Basic
-import AeneasMeta.Utils
+module
+public import Mathlib.Data.Nat.Basic
+public import Mathlib.Algebra.Group.Basic
+public import AeneasMeta.Utils
+public section
 
 namespace Aeneas
 
@@ -27,7 +29,7 @@ instance : Membership Nat DivRange where
 namespace DivRange
 universe u v
 
-@[inline] protected def forIn' [Monad m] (range : DivRange) (init : β)
+@[inline, expose] protected def forIn' [Monad m] (range : DivRange) (init : β)
     (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop (maxSteps : Nat) (b : β) (i : Nat)
       (hs : ∃ k, i = range.start / range.divisor ^ k)
@@ -66,7 +68,7 @@ We now introduce a convenient `DivRange` definition
 -/
 
 -- TODO: don't use a fuel
-def divRange (start stop div : Nat) : List Nat :=
+@[expose] def divRange (start stop div : Nat) : List Nat :=
   let rec loop (fuel i : Nat) :=
     match fuel with
     | 0 => []
@@ -79,7 +81,7 @@ def divRange (start stop div : Nat) : List Nat :=
 namespace DivRange
 
 /-- A convenient utility for the proofs -/
-def foldWhile' {α : Type u} (r : DivRange) (f : α → (a : Nat) → (a ∈ r) → α) (i : Nat) (init : α)
+@[expose] def foldWhile' {α : Type u} (r : DivRange) (f : α → (a : Nat) → (a ∈ r) → α) (i : Nat) (init : α)
   (hi : i ≤ r.start ∧ ∃ k, i = r.start / r.divisor ^ k) : α :=
   if h: r.stop < i then
     foldWhile' r f (i / r.divisor)
@@ -94,7 +96,7 @@ termination_by i
 decreasing_by apply Nat.div_lt_self; omega; apply r.divisor_pos
 
 /-- A convenient utility for the proofs -/
-def foldWhile {α : Type u} (stop divisor : Nat) (hDiv : 1 < divisor)
+@[expose] def foldWhile {α : Type u} (stop divisor : Nat) (hDiv : 1 < divisor)
   (f : α → (a : Nat) → α) (i : Nat) (init : α) : α :=
 if stop < i then
     foldWhile stop divisor hDiv f (i / divisor) (f init i)