Skip to content

Commit 7e432b6

Browse files
JacquesCaretteJacquesCarette
authored
Tighten imports some more (#2343)
* no need to use Function when only import is from Function.Base * Use Function.Base when it suffices * use Data.Product.Base as much as possible. Make imports more precise in many of the files touched. Split an example off into a README instead of using more imports just for its sake. * more tightening of imports. * a few more tightening imports
1 parent 865dfb1 commit 7e432b6

File tree

22 files changed

+118
-92
lines changed

22 files changed

+118
-92
lines changed

‎doc/README/Effect/Monad/Partiality.agda

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
-----------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Example showing the use of the partiality Monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe --guardedness #-}
8+
9+
module README.Effect.Monad.Partiality where
10+
11+
open import Codata.Musical.Notation using (♯_)
12+
open import Data.Bool.Base using (false; true)
13+
open import Data.Nat using (ℕ; _+_; _∸_; _≤?_)
14+
open import Effect.Monad.Partiality
15+
open import Relation.Nullary.Decidable using (does)
16+
17+
open Workaround
18+
19+
-- McCarthy's f91:
20+
21+
f91′ : ℕ → ℕ ⊥P
22+
f91′ n with does (n ≤? 100)
23+
... | true = later (♯ (f91′ (11 + n) >>= f91′))
24+
... | false = now (n ∸ 10)
25+
26+
f91 : ℕ → ℕ ⊥
27+
f91 n = ⟦ f91′ n ⟧P

‎src/Algebra/Module/Construct/Idealization.agda

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,11 @@ import Algebra.Definitions as Definitions
4343
import Algebra.Module.Construct.DirectProduct as DirectProduct
4444
import Algebra.Module.Construct.TensorUnit as TensorUnit
4545
open import Algebra.Structures using (IsAbelianGroup; IsRing)
46-
open import Data.Product using (_,_; ∃-syntax)
46+
open import Data.Product.Base using (_,_; ∃-syntax)
4747
open import Level using (Level; _⊔_)
48-
open import Relation.Binary using (Rel; Setoid; IsEquivalence)
48+
open import Relation.Binary.Bundles using (Setoid)
49+
open import Relation.Binary.Core using (Rel)
50+
open import Relation.Binary.Structures using (IsEquivalence)
4951
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
5052

5153
------------------------------------------------------------------------

‎src/Algebra/Properties/CommutativeMonoid.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Bundles
10-
open import Algebra.Definitions
11-
open import Data.Product using (_,_; proj₂)
9+
open import Algebra.Bundles using (CommutativeMonoid)
10+
open import Algebra.Definitions using (LeftInvertible; RightInvertible; Invertible)
11+
open import Data.Product.Base using (_,_; proj₂)
1212

1313
module Algebra.Properties.CommutativeMonoid
1414
{g₁ g₂} (M : CommutativeMonoid g₁ g₂) where

‎src/Data/Container/Core.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
module Data.Container.Core where
1010

11-
open import Level
11+
open import Level using (Level; _⊔_; suc)
1212
open import Data.Product.Base as Product using (Σ-syntax)
13-
open import Function.Base
14-
open import Function using (Inverse; _↔_)
13+
open import Function.Base using (_∘_; _∘′_)
14+
open import Function.Bundles using (Inverse; _↔_)
1515
open import Relation.Unary using (Pred; _⊆_)
1616

1717
-- Definition of Containers

‎src/Data/Container/Indexed.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,14 @@
1111

1212
module Data.Container.Indexed where
1313

14-
open import Level
14+
open import Level using (Level; zero; _⊔_)
1515
open import Data.Product.Base as Prod hiding (map)
16-
open import Data.W.Indexed
16+
open import Data.W.Indexed using (W)
1717
open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
18-
open import Function using (_↔_; Inverse)
18+
open import Function.Bundles using (_↔_; Inverse)
1919
open import Relation.Unary using (Pred; _⊆_)
2020
open import Relation.Binary.Core using (Rel; REL)
21-
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; trans; subst)
21+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; trans; subst)
2222

2323
------------------------------------------------------------------------
2424

‎src/Data/Container/Indexed/Relation/Binary/Pointwise.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,11 @@
88

99
module Data.Container.Indexed.Relation.Binary.Pointwise where
1010

11-
open import Data.Product using (_,_; Σ-syntax)
12-
open import Function
11+
open import Data.Product.Base using (_,_; Σ-syntax)
12+
open import Function.Base using (_∘_)
1313
open import Level using (Level; _⊔_)
1414
open import Relation.Binary using (REL; _⇒_)
15-
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
15+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
1616

1717
open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
1818

‎src/Data/List/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
2323
open import Data.List.Relation.Unary.Any using (Any; here; there)
2424
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
2525
open import Data.Nat.Base
26-
open import Data.Nat.Divisibility
26+
open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
2727
open import Data.Nat.Properties
2828
open import Data.Product.Base as Product
2929
using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)

‎src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,10 @@ module Data.List.Relation.Ternary.Appending.Setoid.Properties
1313
where
1414

1515
open import Data.List.Base as List using (List; [])
16-
import Data.List.Properties as Listₚ
16+
import Data.List.Properties as List
1717
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
1818
import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
19-
open import Data.Product using (∃-syntax; _×_; _,_)
19+
open import Data.Product.Base using (∃-syntax; _×_; _,_)
2020
open import Function.Base using (id)
2121
open import Relation.Binary.Core using (_⇒_)
2222
open import Relation.Binary.PropositionalEquality.Core using (refl)
@@ -45,7 +45,7 @@ open Appendingₚ public
4545
++[]⁻¹ : Appending as [] cs → Pointwise _≈_ as cs
4646
++[]⁻¹ {as} {cs} ls with break ls
4747
... | cs₁ , cs₂ , refl , pw , []
48-
rewrite Listₚ.++-identityʳ cs₁
48+
rewrite List.++-identityʳ cs₁
4949
= pw
5050

5151
respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →

‎src/Data/List/Relation/Unary/First/Properties.agda

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -8,17 +8,16 @@
88

99
module Data.List.Relation.Unary.First.Properties where
1010

11-
open import Data.Empty
1211
open import Data.Fin.Base using (suc)
1312
open import Data.List.Base as List using (List; []; _∷_)
1413
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
1514
open import Data.List.Relation.Unary.Any as Any using (here; there)
1615
open import Data.List.Relation.Unary.First
1716
import Data.Sum as Sum
1817
open import Function.Base using (_∘′_; _$_; _∘_; id)
19-
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl; _≗_)
20-
open import Relation.Unary
21-
open import Relation.Nullary.Negation
18+
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
19+
open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
20+
open import Relation.Nullary.Negation using (contradiction)
2221

2322
------------------------------------------------------------------------
2423
-- map
@@ -52,7 +51,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
5251
module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
5352

5453
All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
55-
All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = ⊥-elim (p⇒¬q px qx)
54+
All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = contradiction qx (p⇒¬q px)
5655
All⇒¬First p⇒¬q (_ ∷ pxs) (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
5756

5857
First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -64,16 +63,16 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
6463

6564
unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
6665
unique-index p⇒¬q [ _ ] [ _ ] = refl
67-
unique-index p⇒¬q [ qx ] (px ∷ _) = ⊥-elim (p⇒¬q px qx)
68-
unique-index p⇒¬q (px ∷ _) [ qx ] = ⊥-elim (p⇒¬q px qx)
66+
unique-index p⇒¬q [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
67+
unique-index p⇒¬q (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
6968
unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = ≡.cong suc (unique-index p⇒¬q f₁ f₂)
7069

7170
irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
72-
irrelevant p⇒¬q p-irr q-irr [ qx₁ ] [ qx₂ ] = ≡.cong [_] (q-irr qx₁ qx₂)
73-
irrelevant p⇒¬q p-irr q-irr [ qx₁ ] (px₂ ∷ f₂) = ⊥-elim (p⇒¬q px₂ qx₁)
74-
irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) [ qx₂ ] = ⊥-elim (p⇒¬q px₁ qx₂)
75-
irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) (px₂ ∷ f₂) =
76-
≡.cong₂ _∷_ (p-irr px₁ px₂) (irrelevant p⇒¬q p-irr q-irr f₁ f₂)
71+
irrelevant p⇒¬q p-irr q-irr [ px ] [ qx ] = ≡.cong [_] (q-irr px qx)
72+
irrelevant p⇒¬q p-irr q-irr [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
73+
irrelevant p⇒¬q p-irr q-irr (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
74+
irrelevant p⇒¬q p-irr q-irr (px ∷ f) (qx ∷ g) =
75+
≡.cong₂ _∷_ (p-irr px qx) (irrelevant p⇒¬q p-irr q-irr f g)
7776

7877
------------------------------------------------------------------------
7978
-- Decidability

‎src/Data/Nat/Primality/Factorisation.agda

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,28 +8,33 @@
88

99
module Data.Nat.Primality.Factorisation where
1010

11-
open import Data.Empty using (⊥-elim)
1211
open import Data.Nat.Base
1312
open import Data.Nat.Divisibility
13+
using (_∣?_; quotient; quotient>1; quotient-<; quotient-∣; m∣n⇒n≡m*quotient; _∣_; ∣1⇒≡1;
14+
divides)
1415
open import Data.Nat.Properties
1516
open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
1617
open import Data.Nat.Primality
17-
open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂)
18+
using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
19+
2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
20+
open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
1821
open import Data.List.Base using (List; []; _∷_; _++_; product)
1922
open import Data.List.Membership.Propositional using (_∈_)
2023
open import Data.List.Membership.Propositional.Properties using (∈-∃++)
2124
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
2225
open import Data.List.Relation.Unary.Any using (here; there)
2326
open import Data.List.Relation.Binary.Permutation.Propositional
2427
using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
25-
open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
28+
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
29+
using (product-↭; All-resp-↭; shift)
2630
open import Data.Sum.Base using (inj₁; inj₂)
2731
open import Function.Base using (_$_; _∘_; _|>_; flip)
2832
open import Induction using (build)
2933
open import Induction.Lexicographic using (_⊗_; [_⊗_])
3034
open import Relation.Nullary.Decidable using (yes; no)
3135
open import Relation.Nullary.Negation using (contradiction)
32-
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
36+
open import Relation.Binary.PropositionalEquality
37+
using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
3338

3439
private
3540
variable

‎src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,16 @@
99
module Data.Product.Relation.Binary.Pointwise.NonDependent where
1010

1111
open import Data.Product.Base as Product
12-
open import Data.Product.Properties using (≡-dec)
13-
open import Data.Sum.Base
14-
open import Data.Unit.Base using (⊤)
12+
open import Data.Sum.Base using (inj₁; inj₂)
1513
open import Level using (Level; _⊔_; 0ℓ)
16-
open import Function
14+
open import Function.Base using (_on_; id)
15+
open import Function.Bundles using (Inverse)
1716
open import Relation.Nullary.Decidable using (_×-dec_)
18-
open import Relation.Binary
17+
open import Relation.Binary.Core using (Rel; _⇒_)
18+
open import Relation.Binary.Bundles
19+
using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
20+
open import Relation.Binary.Definitions
21+
open import Relation.Binary.Structures
1922
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
2023
import Relation.Binary.PropositionalEquality.Properties as ≡
2124

‎src/Data/Rational/Unnormalised/Base.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
module Data.Rational.Unnormalised.Base where
1010

1111
open import Algebra.Bundles.Raw
12+
using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
1213
open import Data.Bool.Base using (Bool; true; false; if_then_else_)
1314
open import Data.Integer.Base as ℤ
1415
using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)

‎src/Data/Sum/Algebra.agda

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,16 @@
88

99
module Data.Sum.Algebra where
1010

11-
open import Algebra
11+
open import Algebra.Bundles
12+
using (Magma; Semigroup; Monoid; CommutativeMonoid)
13+
open import Algebra.Definitions
14+
open import Algebra.Structures
15+
using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid)
1216
open import Data.Empty.Polymorphic using (⊥)
1317
open import Data.Product.Base using (_,_)
14-
open import Data.Sum.Base
15-
open import Data.Sum.Properties
16-
open import Data.Unit.Polymorphic using (⊤; tt)
18+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; map; [_,_]; swap; assocʳ; assocˡ)
19+
open import Data.Sum.Properties using (swap-involutive)
20+
open import Data.Unit.Polymorphic.Base using (⊤; tt)
1721
open import Function.Base using (id; _∘_)
1822
open import Function.Properties.Inverse using (↔-isEquivalence)
1923
open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)

‎src/Data/Sum/Function/Propositional.agda

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,18 @@
88

99
module Data.Sum.Function.Propositional where
1010

11-
open import Data.Sum.Base
11+
open import Data.Sum.Base using (_⊎_)
1212
open import Data.Sum.Function.Setoid
1313
open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_)
1414
open import Function.Construct.Composition as Compose
1515
open import Function.Related.Propositional
16-
open import Function
16+
open import Function.Base using (id)
17+
open import Function.Bundles
18+
using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _↩_; _↪_; _⤖_; _↔_)
1719
open import Function.Properties.Inverse as Inv
1820
open import Level using (Level; _⊔_)
19-
open import Relation.Binary using (REL; Setoid)
21+
open import Relation.Binary.Core using (REL)
22+
open import Relation.Binary.Bundles using (Setoid)
2023
open import Relation.Binary.PropositionalEquality using (setoid)
2124

2225
private

‎src/Data/Unit/Polymorphic/Properties.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ open import Relation.Binary.Structures
2323
open import Relation.Binary.Definitions
2424
using (Decidable; Antisymmetric; Total)
2525
open import Relation.Binary.PropositionalEquality
26+
using (_≡_; refl; trans; decSetoid; setoid; isEquivalence)
2627

2728
private
2829
variable

‎src/Effect/Monad/Partiality.agda

Lines changed: 9 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,15 @@
88

99
module Effect.Monad.Partiality where
1010

11-
open import Codata.Musical.Notation
12-
open import Effect.Functor
13-
open import Effect.Applicative
14-
open import Effect.Monad
11+
open import Codata.Musical.Notation using (∞; ♯_; ♭)
12+
open import Effect.Functor using (RawFunctor)
13+
open import Effect.Applicative using (RawApplicative)
14+
open import Effect.Monad using (RawMonad; module Join)
1515
open import Data.Bool.Base using (Bool; false; true)
16-
open import Data.Nat using (ℕ; zero; suc; _+_)
17-
open import Data.Product as Prod hiding (map)
16+
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
17+
open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
1818
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
19-
open import Function.Base
19+
open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
2020
open import Function.Bundles using (_⇔_; mk⇔)
2121
open import Level using (Level; _⊔_)
2222
open import Relation.Binary.Core as B hiding (Rel; _⇔_)
@@ -29,9 +29,8 @@ open import Relation.Binary.Bundles
2929
import Relation.Binary.Properties.Setoid as SetoidProperties
3030
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
3131
import Relation.Binary.PropositionalEquality.Properties as ≡
32-
open import Relation.Nullary
33-
open import Relation.Nullary.Decidable hiding (map)
34-
open import Relation.Nullary.Negation
32+
open import Relation.Nullary.Decidable using (yes; no; False; Dec; ¬¬-excluded-middle)
33+
open import Relation.Nullary.Negation using (¬_; ¬¬-Monad)
3534

3635
private
3736
variable
@@ -934,22 +933,3 @@ idempotent {A = A} B x f = sound (idem x)
934933
laterˡ (refl (Setoid.refl B))) ⟩
935934
(♭ x >>= λ y′ → ♭ x >>= λ y″ → f y′ y″) ≳⟨ idem (♭ x) ⟩≅
936935
(♭ x >>= λ y′ → f y′ y′) ∎))
937-
938-
------------------------------------------------------------------------
939-
-- Example
940-
941-
private
942-
module Example where
943-
944-
open Data.Nat
945-
open Workaround
946-
947-
-- McCarthy's f91:
948-
949-
f91′ : ℕ → ℕ ⊥P
950-
f91′ n with does (n ≤? 100)
951-
... | true = later (♯ (f91′ (11 + n) >>= f91′))
952-
... | false = now (n ∸ 10)
953-
954-
f91 : ℕ → ℕ ⊥
955-
f91 n = ⟦ f91′ n ⟧P

‎src/Function/Properties/Inverse/HalfAdjointEquivalence.agda

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,12 @@
88

99
module Function.Properties.Inverse.HalfAdjointEquivalence where
1010

11-
open import Function.Base
12-
open import Function
13-
open import Level
11+
open import Function.Base using (id; _∘_)
12+
open import Function.Bundles using (Inverse; _↔_; mk↔ₛ′)
13+
open import Level using (Level; _⊔_)
1414
open import Relation.Binary.PropositionalEquality
15+
using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality;
16+
cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
1517

1618
private
1719
variable

0 commit comments

Comments
 (0)