Skip to content

Commit d61818c

Browse files
chenson2018chenson2018
authored
feat: move to the module system (#243)
Closes #172. This PR moves CSLib to the module system, mostly following Mathlib's pattern of using `@[expose] public section` liberally for the simplest transition. This removes a few uses of `private` that conflicted: - `LTS.noε` - the `HasTau` instance in `Cslib.Computability.Automata.EpsilonNA.Basic` - `grind` lemmas about `ReductionSystem` - `FinFun.fromFun` I also think it might be less confusing if we move some `meta` sections to their own files, but will leave this for a future PR.
1 parent b55a607 commit d61818c

81 files changed

Lines changed: 599 additions & 272 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,14 @@ jobs:
1717
- uses: leanprover/lean-action@v1
1818
with:
1919
build-args: "--wfail --iofail"
20-
mk_all-check: "true"
21-
- name: "lake exe shake"
20+
- name: "lake exe mk_all --check --module"
2221
run: |
2322
set -e
24-
lake exe shake Cslib
23+
lake exe mk_all --check --module
24+
#- name: "lake exe shake"
25+
# run: |
26+
# set -e
27+
# lake exe shake Cslib
2528
- uses: leanprover-community/lint-style-action@main
2629
with:
2730
mode: check

‎Cslib.lean‎

Lines changed: 80 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -1,78 +1,80 @@
1-
import Cslib.Algorithms.Lean.MergeSort.MergeSort
2-
import Cslib.Algorithms.Lean.TimeM
3-
import Cslib.Computability.Automata.Acceptors.Acceptor
4-
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
5-
import Cslib.Computability.Automata.DA.Basic
6-
import Cslib.Computability.Automata.DA.Buchi
7-
import Cslib.Computability.Automata.DA.Prod
8-
import Cslib.Computability.Automata.DA.ToNA
9-
import Cslib.Computability.Automata.EpsilonNA.Basic
10-
import Cslib.Computability.Automata.EpsilonNA.ToNA
11-
import Cslib.Computability.Automata.NA.Basic
12-
import Cslib.Computability.Automata.NA.BuchiEquiv
13-
import Cslib.Computability.Automata.NA.BuchiInter
14-
import Cslib.Computability.Automata.NA.Concat
15-
import Cslib.Computability.Automata.NA.Hist
16-
import Cslib.Computability.Automata.NA.Loop
17-
import Cslib.Computability.Automata.NA.Prod
18-
import Cslib.Computability.Automata.NA.Sum
19-
import Cslib.Computability.Automata.NA.ToDA
20-
import Cslib.Computability.Automata.NA.Total
21-
import Cslib.Computability.Languages.ExampleEventuallyZero
22-
import Cslib.Computability.Languages.Language
23-
import Cslib.Computability.Languages.OmegaLanguage
24-
import Cslib.Computability.Languages.OmegaRegularLanguage
25-
import Cslib.Computability.Languages.RegularLanguage
26-
import Cslib.Foundations.Control.Monad.Free
27-
import Cslib.Foundations.Control.Monad.Free.Effects
28-
import Cslib.Foundations.Control.Monad.Free.Fold
29-
import Cslib.Foundations.Data.FinFun
30-
import Cslib.Foundations.Data.HasFresh
31-
import Cslib.Foundations.Data.Nat.Segment
32-
import Cslib.Foundations.Data.OmegaSequence.Defs
33-
import Cslib.Foundations.Data.OmegaSequence.Flatten
34-
import Cslib.Foundations.Data.OmegaSequence.InfOcc
35-
import Cslib.Foundations.Data.OmegaSequence.Init
36-
import Cslib.Foundations.Data.OmegaSequence.Temporal
37-
import Cslib.Foundations.Data.Relation
38-
import Cslib.Foundations.Lint.Basic
39-
import Cslib.Foundations.Semantics.FLTS.Basic
40-
import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
41-
import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
42-
import Cslib.Foundations.Semantics.FLTS.Prod
43-
import Cslib.Foundations.Semantics.LTS.Basic
44-
import Cslib.Foundations.Semantics.LTS.Bisimulation
45-
import Cslib.Foundations.Semantics.LTS.Simulation
46-
import Cslib.Foundations.Semantics.LTS.TraceEq
47-
import Cslib.Foundations.Semantics.ReductionSystem.Basic
48-
import Cslib.Foundations.Syntax.HasAlphaEquiv
49-
import Cslib.Foundations.Syntax.HasSubstitution
50-
import Cslib.Foundations.Syntax.HasWellFormed
51-
import Cslib.Init
52-
import Cslib.Languages.CCS.Basic
53-
import Cslib.Languages.CCS.BehaviouralTheory
54-
import Cslib.Languages.CCS.Semantics
55-
import Cslib.Languages.CombinatoryLogic.Basic
56-
import Cslib.Languages.CombinatoryLogic.Confluence
57-
import Cslib.Languages.CombinatoryLogic.Defs
58-
import Cslib.Languages.CombinatoryLogic.Evaluation
59-
import Cslib.Languages.CombinatoryLogic.Recursion
60-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
61-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
62-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
63-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
64-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
65-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
66-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
67-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
68-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
69-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
70-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
71-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
72-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
73-
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
74-
import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
75-
import Cslib.Logics.LinearLogic.CLL.Basic
76-
import Cslib.Logics.LinearLogic.CLL.CutElimination
77-
import Cslib.Logics.LinearLogic.CLL.EtaExpansion
78-
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
1+
module
2+
3+
public import Cslib.Algorithms.Lean.MergeSort.MergeSort
4+
public import Cslib.Algorithms.Lean.TimeM
5+
public import Cslib.Computability.Automata.Acceptors.Acceptor
6+
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
7+
public import Cslib.Computability.Automata.DA.Basic
8+
public import Cslib.Computability.Automata.DA.Buchi
9+
public import Cslib.Computability.Automata.DA.Prod
10+
public import Cslib.Computability.Automata.DA.ToNA
11+
public import Cslib.Computability.Automata.EpsilonNA.Basic
12+
public import Cslib.Computability.Automata.EpsilonNA.ToNA
13+
public import Cslib.Computability.Automata.NA.Basic
14+
public import Cslib.Computability.Automata.NA.BuchiEquiv
15+
public import Cslib.Computability.Automata.NA.BuchiInter
16+
public import Cslib.Computability.Automata.NA.Concat
17+
public import Cslib.Computability.Automata.NA.Hist
18+
public import Cslib.Computability.Automata.NA.Loop
19+
public import Cslib.Computability.Automata.NA.Prod
20+
public import Cslib.Computability.Automata.NA.Sum
21+
public import Cslib.Computability.Automata.NA.ToDA
22+
public import Cslib.Computability.Automata.NA.Total
23+
public import Cslib.Computability.Languages.ExampleEventuallyZero
24+
public import Cslib.Computability.Languages.Language
25+
public import Cslib.Computability.Languages.OmegaLanguage
26+
public import Cslib.Computability.Languages.OmegaRegularLanguage
27+
public import Cslib.Computability.Languages.RegularLanguage
28+
public import Cslib.Foundations.Control.Monad.Free
29+
public import Cslib.Foundations.Control.Monad.Free.Effects
30+
public import Cslib.Foundations.Control.Monad.Free.Fold
31+
public import Cslib.Foundations.Data.FinFun
32+
public import Cslib.Foundations.Data.HasFresh
33+
public import Cslib.Foundations.Data.Nat.Segment
34+
public import Cslib.Foundations.Data.OmegaSequence.Defs
35+
public import Cslib.Foundations.Data.OmegaSequence.Flatten
36+
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
37+
public import Cslib.Foundations.Data.OmegaSequence.Init
38+
public import Cslib.Foundations.Data.OmegaSequence.Temporal
39+
public import Cslib.Foundations.Data.Relation
40+
public import Cslib.Foundations.Lint.Basic
41+
public import Cslib.Foundations.Semantics.FLTS.Basic
42+
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
43+
public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
44+
public import Cslib.Foundations.Semantics.FLTS.Prod
45+
public import Cslib.Foundations.Semantics.LTS.Basic
46+
public import Cslib.Foundations.Semantics.LTS.Bisimulation
47+
public import Cslib.Foundations.Semantics.LTS.Simulation
48+
public import Cslib.Foundations.Semantics.LTS.TraceEq
49+
public import Cslib.Foundations.Semantics.ReductionSystem.Basic
50+
public import Cslib.Foundations.Syntax.HasAlphaEquiv
51+
public import Cslib.Foundations.Syntax.HasSubstitution
52+
public import Cslib.Foundations.Syntax.HasWellFormed
53+
public import Cslib.Init
54+
public import Cslib.Languages.CCS.Basic
55+
public import Cslib.Languages.CCS.BehaviouralTheory
56+
public import Cslib.Languages.CCS.Semantics
57+
public import Cslib.Languages.CombinatoryLogic.Basic
58+
public import Cslib.Languages.CombinatoryLogic.Confluence
59+
public import Cslib.Languages.CombinatoryLogic.Defs
60+
public import Cslib.Languages.CombinatoryLogic.Evaluation
61+
public import Cslib.Languages.CombinatoryLogic.Recursion
62+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
63+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
64+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
65+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
66+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
67+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
68+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
69+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
70+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
71+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
72+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
73+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
74+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
75+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
76+
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
77+
public import Cslib.Logics.LinearLogic.CLL.Basic
78+
public import Cslib.Logics.LinearLogic.CLL.CutElimination
79+
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
80+
public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic

‎Cslib/Algorithms/Lean/MergeSort/MergeSort.lean‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sorrachai Yingchareonthawornhcai
55
-/
66

7-
import Cslib.Algorithms.Lean.TimeM
8-
import Mathlib.Data.Nat.Cast.Order.Ring
9-
import Mathlib.Data.Nat.Lattice
10-
import Mathlib.Data.Nat.Log
7+
module
118

9+
public import Cslib.Algorithms.Lean.TimeM
10+
public import Mathlib.Data.Nat.Cast.Order.Ring
11+
public import Mathlib.Data.Nat.Lattice
12+
public import Mathlib.Data.Nat.Log
13+
14+
@[expose] public section
1215

1316
/-!
1417
# MergeSort on a list

‎Cslib/Algorithms/Lean/TimeM.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sorrachai Yingchareonthawornhcai
55
-/
66

7+
module
8+
79
import Cslib.Init
810

11+
@[expose] public section
12+
913
/-!
1014
1115
# TimeM: Time Complexity Monad

‎Cslib/Computability/Automata/Acceptors/Acceptor.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7-
import Cslib.Init
8-
import Mathlib.Computability.Language
7+
module
8+
9+
public import Cslib.Init
10+
public import Mathlib.Computability.Language
11+
12+
@[expose] public section
913

1014
namespace Cslib.Automata
1115

‎Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7-
import Cslib.Computability.Languages.OmegaLanguage
7+
module
8+
9+
public import Cslib.Computability.Languages.OmegaLanguage
10+
11+
@[expose] public section
812

913
namespace Cslib.Automata
1014

‎Cslib/Computability/Automata/DA/Basic.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi, Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.Acceptors.Acceptor
8-
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
9-
import Cslib.Foundations.Data.OmegaSequence.InfOcc
10-
import Cslib.Foundations.Semantics.FLTS.Basic
7+
module
8+
9+
public import Cslib.Computability.Automata.Acceptors.Acceptor
10+
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
11+
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
12+
public import Cslib.Foundations.Semantics.FLTS.Basic
13+
14+
@[expose] public section
1115

1216
/-! # Deterministic Automata
1317

‎Cslib/Computability/Automata/DA/Buchi.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.DA.Basic
7+
module
8+
9+
public import Cslib.Computability.Automata.DA.Basic
10+
11+
public section
812

913
/-! # Deterministic Buchi automata.
1014
-/

‎Cslib/Computability/Automata/DA/Prod.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.DA.Basic
8-
import Cslib.Foundations.Semantics.FLTS.Prod
7+
module
8+
9+
public import Cslib.Computability.Automata.DA.Basic
10+
public import Cslib.Foundations.Semantics.FLTS.Prod
11+
12+
@[expose] public section
913

1014
/-! # Product of deterministic automata. -/
1115

‎Cslib/Computability/Automata/DA/ToNA.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7-
import Cslib.Computability.Automata.DA.Basic
8-
import Cslib.Computability.Automata.NA.Basic
9-
import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
7+
module
8+
9+
public import Cslib.Computability.Automata.DA.Basic
10+
public import Cslib.Computability.Automata.NA.Basic
11+
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
12+
13+
@[expose] public section
1014

1115
/-! # Translation of Deterministic Automata into Nonodeterministic Automata.
1216

0 commit comments

Comments
 (0)