Proper interfaces / prelude

- MetaPrelude~>Meta.Prelude - Meta~>Meta.Init
agda · Sep 13, 2024 · d55da1f · d55da1f
1 parent 0f49baa
commit d55da1f
Show file tree

Hide file tree

Showing 36 changed files with 60 additions and 60 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -13,13 +13,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
-      - uses: omelkonian/setup-agda@master
+      - uses: omelkonian/setup-agda@v2
         with:
-          agda-version: 2.6.4
-          stdlib-version: 2.0
-          libraries: |
-            omelkonian/agda-stdlib-classes#v2.0
-          main: Main
+          agda-version: 2.7.0
+          stdlib-version: 2.1.1
+          libraries: omelkonian/agda-stdlib-classes#v2.1.1
+          main: standard-library-meta
           deploy: ${{ github.ref == 'refs/heads/master' }}
           token: ${{ secrets.GITHUB_TOKEN }}
           ribbon: true

diff --git a/Class/MonadError.agda b/Class/MonadError.agda
@@ -2,7 +2,7 @@
 
 open import Level
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Class.Monad
 open import Reflection using (TC; ErrorPart; typeError; catchTC; strErr)

diff --git a/Class/MonadReader.agda b/Class/MonadReader.agda
@@ -2,7 +2,7 @@
 
 module Class.MonadReader where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Class.Monad
 open import Class.Functor

diff --git a/Class/MonadTC.agda b/Class/MonadTC.agda
@@ -2,7 +2,7 @@
 
 module Class.MonadTC where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Data.List using (map)
 

diff --git a/Meta.agda → Meta/Init.agda b/Meta.agda → Meta/Init.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --safe --without-K #-}
 
-module Meta where
+module Meta.Init where
 
 open import Reflection.Debug public
 open import Reflection.TCI public

diff --git a/MetaPrelude.agda → Meta/Prelude.agda b/MetaPrelude.agda → Meta/Prelude.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --safe --without-K #-}
 
-module MetaPrelude where
+module Meta.Prelude where
 
 open import Level renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ) public
 open import Function public

diff --git a/Reflection/AlphaEquality.agda b/Reflection/AlphaEquality.agda
@@ -8,8 +8,8 @@
 
 module Reflection.AlphaEquality where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 open import Relation.Nullary.Decidable using (⌊_⌋)
 open import Relation.Binary            using (DecidableEquality)
 

diff --git a/Reflection/AntiUnification.agda b/Reflection/AntiUnification.agda
@@ -9,8 +9,8 @@
 
 module Reflection.AntiUnification where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 import Data.Maybe as Maybe
 import Data.Nat as Nat

diff --git a/Reflection/Debug.agda b/Reflection/Debug.agda
@@ -2,7 +2,7 @@
 
 module Reflection.Debug where
 
-open import MetaPrelude hiding (⊤; _∧_; _∨_; filter)
+open import Meta.Prelude hiding (⊤; _∧_; _∨_; filter)
 
 import Data.Bool as B
 import Data.String as S

diff --git a/Reflection/Syntax.agda b/Reflection/Syntax.agda
@@ -2,7 +2,7 @@
 
 module Reflection.Syntax where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Reflection.AST.Argument public
   hiding (map)

diff --git a/Reflection/TCI.agda b/Reflection/TCI.agda
@@ -5,7 +5,7 @@
 
 module Reflection.TCI where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Data.List using (map)
 

diff --git a/Reflection/Tactic.agda b/Reflection/Tactic.agda
@@ -8,8 +8,8 @@ module Reflection.Tactic where
 import Reflection as R
 open import Class.Monad hiding (Monad-TC)
 open import Class.MonadTC
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open MonadTC ⦃...⦄
 

diff --git a/Reflection/Utils.agda b/Reflection/Utils.agda
@@ -1,8 +1,8 @@
 {-# OPTIONS --safe --without-K #-}
 module Reflection.Utils where
 
-open import MetaPrelude
-open import Meta hiding (toℕ)
+open import Meta.Prelude
+open import Meta.Init hiding (toℕ)
 
 import Reflection.AST.Abstraction as Abs
 import Reflection.AST.Name as Name

diff --git a/Reflection/Utils/Debug.agda b/Reflection/Utils/Debug.agda
@@ -4,7 +4,7 @@
 {-# OPTIONS --safe --without-K #-}
 module Reflection.Utils.Debug where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 import Data.String as Str
 open import Data.Fin using (Fin)

diff --git a/Reflection/Utils/TCI.agda b/Reflection/Utils/TCI.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --safe --without-K #-}
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Class.Monad
 open import Class.MonadError.Instances

diff --git a/Tactic/AnyOf.agda b/Tactic/AnyOf.agda
@@ -5,8 +5,8 @@
 
 module Tactic.AnyOf where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Reflection.Utils.TCI
 open import Reflection.Tactic

diff --git a/Tactic/Assumption.agda b/Tactic/Assumption.agda
@@ -5,8 +5,8 @@
 
 module Tactic.Assumption where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Class.Functor
 open import Class.Monad
@@ -47,6 +47,6 @@ private
   module Test where
     test₁ : {A B : Set} → A → B → A
     test₁ a b = assumption
-    
+
     test₂ : {A B : Set} → A → B → B
     test₂ a b = assumption
diff --git a/Tactic/ByEq.agda b/Tactic/ByEq.agda
@@ -1,8 +1,8 @@
 {-# OPTIONS --safe --without-K #-}
 module Tactic.ByEq where
 
-open import Meta hiding (TC)
-open import MetaPrelude
+open import Meta.Init hiding (TC)
+open import Meta.Prelude
 open import Class.Functor.Core; open import Class.Functor.Instances
 open import Class.Monad.Core; open import Class.Monad.Instances
 open import Reflection using (TC; withNormalisation; inferType; unify)

diff --git a/Tactic/Case.agda b/Tactic/Case.agda
@@ -5,8 +5,8 @@
 
 module Tactic.Case where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Data.List using (map)
 

diff --git a/Tactic/ClauseBuilder.agda b/Tactic/ClauseBuilder.agda
@@ -1,8 +1,8 @@
 {-# OPTIONS --safe --without-K #-}
 module Tactic.ClauseBuilder where
 
-open import MetaPrelude hiding ([_,_])
-open import Meta hiding (sort)
+open import Meta.Prelude hiding ([_,_])
+open import Meta.Init hiding (sort)
 
 import Data.List.NonEmpty as NE
 open import Data.List using (zipWith)

diff --git a/Tactic/Constrs.agda b/Tactic/Constrs.agda
@@ -6,8 +6,8 @@
 
 module Tactic.Constrs where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Data.List
 

diff --git a/Tactic/Defaults.agda b/Tactic/Defaults.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --safe --without-K #-}
 module Tactic.Defaults where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Class.MonadTC
 open import Reflection.Debug

diff --git a/Tactic/Derive.agda b/Tactic/Derive.agda
@@ -15,11 +15,11 @@
 
 {-# OPTIONS -v allTactics:100 #-}
 {-# OPTIONS --safe --without-K #-}
-open import Meta
+open import Meta.Init
 
 module Tactic.Derive (className : Name) (projName : Name) where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Agda.Builtin.Reflection using () renaming (primShowQName to showName)
 

diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda
@@ -10,8 +10,8 @@
 {-# OPTIONS --safe #-}
 module Tactic.Derive.DecEq where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 import Data.List as L
 import Data.List.NonEmpty as NE

diff --git a/Tactic/Derive/Show.agda b/Tactic/Derive/Show.agda
@@ -4,8 +4,8 @@
 {-# OPTIONS --safe #-}
 module Tactic.Derive.Show where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Agda.Builtin.Reflection using (primShowQName)
 

diff --git a/Tactic/Derive/TestTypes.agda b/Tactic/Derive/TestTypes.agda
@@ -2,9 +2,10 @@
 {-# OPTIONS -v allTactics:100 #-}
 module Tactic.Derive.TestTypes where
 
-open import MetaPrelude
 open import Data.Fin
-open import Meta
+
+open import Meta.Prelude
+open import Meta.Init
 
 data E0 : Set where
 

diff --git a/Tactic/EquationalReasoning.agda b/Tactic/EquationalReasoning.agda
@@ -5,7 +5,7 @@
 
 module Tactic.EquationalReasoning where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 import Relation.Binary.PropositionalEquality as ≡
 open import Agda.Builtin.Reflection

diff --git a/Tactic/Eta.agda b/Tactic/Eta.agda
@@ -5,8 +5,8 @@
 
 module Tactic.Eta where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Data.List
 open import Data.Fin

diff --git a/Tactic/Existentials.agda b/Tactic/Existentials.agda
@@ -1,6 +1,6 @@
 module Tactic.Existentials where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Reflection hiding (_>>=_; _>>_; _≟_)
 open import Reflection.Syntax

diff --git a/Tactic/Extra.agda b/Tactic/Extra.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS -v extra:100 #-}
 module Tactic.Extra where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Data.Integer as Int using (ℤ)
 open import Data.List using (List; drop; map; [_]; [])

diff --git a/Tactic/Intro.agda b/Tactic/Intro.agda
@@ -5,8 +5,8 @@
 
 module Tactic.Intro where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Class.Monad
 open import Class.MonadTC.Instances

diff --git a/Tactic/J.agda b/Tactic/J.agda
@@ -11,7 +11,7 @@ open import Meta
 
 module Tactic.J (J-name refl-name : Name) where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Class.Monad
 open import Class.MonadError

diff --git a/Tactic/ReduceDec.agda b/Tactic/ReduceDec.agda
@@ -5,8 +5,8 @@
 
 module Tactic.ReduceDec where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Reflection.Tactic
 open import Reflection.Utils

diff --git a/Tactic/Rewrite.agda b/Tactic/Rewrite.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS -v rewrite:100 #-}
 module Tactic.Rewrite where
 
-open import MetaPrelude hiding (_^_)
+open import Meta.Prelude hiding (_^_)
 
 open import Data.List.Membership.DecPropositional using (_∈?_)
 open import Data.List.NonEmpty using (List⁺; _∷_)

diff --git a/Tactic/Try.agda b/Tactic/Try.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS -v try:100 #-}
 module Tactic.Try where
 
-open import MetaPrelude
+open import Meta.Prelude
 
 open import Data.List
 open import Reflection hiding (_>>=_; _>>_; _≟_)

diff --git a/Main.agda → standard-library-meta.agda b/Main.agda → standard-library-meta.agda
@@ -1,4 +1,4 @@
-module Main where
+module standard-library-meta where
 
 open import Algebra.Function