Changes related to a change to Agda's reflection machinery.

The reflection machinery now supports erasure (in Arg), see
agda/agda#5317.

I made the code compile, but further changes may be warranted:

* I did not write anything in the changelog.

* I did not add any deprecation warnings.

* I changed the semantics of
  Tactic.RingSolver.Core.ReflectionHelp.getVisible.

* The function showTerm does not print erasure annotations (but it
  also does not print relevance annotations).

Author: nad

src/Reflection.agda

@@ -30,13 +30,17 @@ open import Reflection.Pattern as Pattern public
 open import Reflection.Term as Term public
   using (Term; Type; Clause; Clauses; Sort)
 
+import Reflection.Argument.Modality as Modality
+import Reflection.Argument.Quantity as Quantity
 import Reflection.Argument.Relevance as Relevance
 import Reflection.Argument.Visibility as Visibility
 import Reflection.Argument.Information as Information
 
 open Definition.Definition public
 open Information.ArgInfo public
 open Literal.Literal public
+open Modality.Modality public
+open Quantity.Quantity public
 open Relevance.Relevance public
 open Term.Term public
 open Visibility.Visibility public
@@ -166,10 +170,10 @@ visibility = Information.visibility
 Please use Reflection.Argument.Information's visibility instead."
 #-}
 
-relevance = Information.relevance
+relevance = Modality.relevance
 {-# WARNING_ON_USAGE relevance
 "Warning: relevance was deprecated in v1.3.
-Please use Reflection.Argument.Information's relevance instead."
+Please use Reflection.Argument.Relevance's relevance instead."
 #-}
 
 infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_

src/Reflection/Argument.agda

@@ -13,6 +13,8 @@ open import Data.Product using (_×_; _,_; uncurry; <_,_>)
 open import Data.Nat using (ℕ)
 open import Reflection.Argument.Visibility
 open import Reflection.Argument.Relevance
+open import Reflection.Argument.Quantity
+open import Reflection.Argument.Modality
 open import Reflection.Argument.Information as Information
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
@@ -34,9 +36,11 @@ open Arg public
 
 -- Pattern synonyms
 
-pattern vArg ty = arg (arg-info visible relevant)   ty
-pattern hArg ty = arg (arg-info hidden relevant)    ty
-pattern iArg ty = arg (arg-info instance′ relevant) ty
+pattern defaultModality = modality relevant quantity-ω
+
+pattern vArg ty = arg (arg-info visible   defaultModality) ty
+pattern hArg ty = arg (arg-info hidden    defaultModality) ty
+pattern iArg ty = arg (arg-info instance′ defaultModality) ty
 
 ------------------------------------------------------------------------
 -- Lists of arguments

src/Reflection/Argument/Information.agda

@@ -9,13 +9,12 @@
 module Reflection.Argument.Information where
 
 open import Data.Product
-open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
-open import Reflection.Argument.Relevance as Relevance using (Relevance)
+open import Reflection.Argument.Modality as Modality using (Modality)
 open import Reflection.Argument.Visibility as Visibility using (Visibility)
 
 ------------------------------------------------------------------------
@@ -30,23 +29,29 @@ open ArgInfo public
 visibility : ArgInfo → Visibility
 visibility (arg-info v _) = v
 
-relevance : ArgInfo → Relevance
-relevance (arg-info _ r) = r
+modality : ArgInfo → Modality
+modality (arg-info _ m) = m
 
 ------------------------------------------------------------------------
 -- Decidable equality
 
-arg-info-injective₁ : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
+private
+  variable
+    v v′ : Visibility
+    m m′ : Modality
+
+arg-info-injective₁ : arg-info v m ≡ arg-info v′ m′ → v ≡ v′
 arg-info-injective₁ refl = refl
 
-arg-info-injective₂ : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
+arg-info-injective₂ : arg-info v m ≡ arg-info v′ m′ → m ≡ m′
 arg-info-injective₂ refl = refl
 
-arg-info-injective : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′ × r ≡ r′
+arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′
 arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ >
 
 _≟_ : DecidableEquality ArgInfo
-arg-info v r ≟ arg-info v′ r′ =
-  Dec.map′ (uncurry (cong₂ arg-info))
-           arg-info-injective
-           (v Visibility.≟ v′ ×-dec r Relevance.≟ r′)
+arg-info v m ≟ arg-info v′ m′ =
+  Dec.map′
+    (uncurry (cong₂ arg-info))
+    arg-info-injective
+    (v Visibility.≟ v′ ×-dec m Modality.≟ m′)

src/Reflection/Argument/Modality.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Modalities used in the reflection machinery
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Reflection.Argument.Modality where
+
+open import Data.Product
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+open import Reflection.Argument.Relevance as Relevance using (Relevance)
+open import Reflection.Argument.Quantity as Quantity using (Quantity)
+
+------------------------------------------------------------------------
+-- Re-exporting the builtins publically
+
+open import Agda.Builtin.Reflection public using (Modality)
+open Modality public
+
+------------------------------------------------------------------------
+-- Operations
+
+relevance : Modality → Relevance
+relevance (modality r _) = r
+
+quantity : Modality → Quantity
+quantity (modality _ q) = q
+
+------------------------------------------------------------------------
+-- Decidable equality
+
+private
+  variable
+    r r′ : Relevance
+    q q′ : Quantity
+
+modality-injective₁ : modality r q ≡ modality r′ q′ → r ≡ r′
+modality-injective₁ refl = refl
+
+modality-injective₂ : modality r q ≡ modality r′ q′ → q ≡ q′
+modality-injective₂ refl = refl
+
+modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′
+modality-injective = < modality-injective₁ , modality-injective₂ >
+
+_≟_ : DecidableEquality Modality
+modality r q ≟ modality r′ q′ =
+  Dec.map′
+    (uncurry (cong₂ modality))
+    modality-injective
+    (r Relevance.≟ r′ ×-dec q Quantity.≟ q′)

src/Reflection/Argument/Quantity.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Argument quantities used in the reflection machinery
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Reflection.Argument.Quantity where
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+------------------------------------------------------------------------
+-- Re-exporting the builtins publically
+
+open import Agda.Builtin.Reflection public using (Quantity)
+open Quantity public
+
+------------------------------------------------------------------------
+-- Decidable equality
+
+_≟_ : DecidableEquality Quantity
+quantity-ω ≟ quantity-ω = yes refl
+quantity-0 ≟ quantity-0 = yes refl
+quantity-ω ≟ quantity-0 = no λ()
+quantity-0 ≟ quantity-ω = no λ()

src/Reflection/DeBruijn.agda

@@ -59,7 +59,11 @@ module _ where
 
 private
   η : Visibility → (Args Term → Term) → Args Term → Term
-  η h f args = lam h (abs "x" (f (weakenArgs 1 args ++ arg (arg-info h relevant) (var 0 []) ∷ [])))
+  η h f args =
+    lam h (abs "x" (f (weakenArgs 1 args ++
+                       arg (arg-info h m) (var 0 []) ∷ [])))
+    where
+    m = modality relevant quantity-ω
 
 η-expand : Visibility → Term → Term
 η-expand h (var x      args) = η h (var (suc x)) args

src/Reflection/Show.agda

@@ -20,12 +20,13 @@ open import Data.Product using (_×_; _,_)
 open import Data.String as String
 import Data.Word as Word
 open import Relation.Nullary using (yes; no)
-open import Function.Base using (_∘′_)
+open import Function.Base using (id; _∘′_; case_of_)
 
 open import Reflection.Abstraction hiding (map)
 open import Reflection.Argument hiding (map)
 open import Reflection.Argument.Relevance
 open import Reflection.Argument.Visibility
+open import Reflection.Argument.Modality
 open import Reflection.Argument.Information
 open import Reflection.Definition
 open import Reflection.Literal
@@ -106,10 +107,15 @@ mutual
   showPatterns []       = ""
   showPatterns (a ∷ ps) = showArg a <+> showPatterns ps
     where
+    -- Quantities are ignored.
     showArg : Arg Pattern → String
-    showArg (arg (arg-info visible r) p)   = showRel r ++ showPattern p
-    showArg (arg (arg-info hidden r) p)    = braces (showRel r ++ showPattern p)
-    showArg (arg (arg-info instance′ r) p) = braces (braces (showRel r ++ showPattern p))
+    showArg (arg (arg-info h (modality r _)) p) =
+      braces? (showRel r ++ showPattern p)
+      where
+      braces? = case h of λ where
+        visible   → id
+        hidden    → braces
+        instance′ → braces ∘′ braces
 
   showPattern : Pattern → String
   showPattern (con c []) = showName c

src/Reflection/Traversal.agda

@@ -80,13 +80,15 @@ module _ (actions : Actions) where
   traverseTerm Γ (var x args)      = var       <$> onVar Γ x ⊛ traverseArgs Γ args
   traverseTerm Γ (con c args)      = con       <$> onCon Γ c ⊛ traverseArgs Γ args
   traverseTerm Γ (def f args)      = def       <$> onDef Γ f ⊛ traverseArgs Γ args
-  traverseTerm Γ (lam v t)         = lam v     <$> traverseAbs (arg (arg-info v relevant) unknown) Γ t
   traverseTerm Γ (pat-lam cs args) = pat-lam   <$> traverseClauses Γ cs ⊛ traverseArgs Γ args
   traverseTerm Γ (pi a b)          = pi        <$> traverseArg Γ a ⊛ traverseAbs a Γ b
   traverseTerm Γ (agda-sort s)     = agda-sort <$> traverseSort Γ s
   traverseTerm Γ (meta x args)     = meta      <$> onMeta Γ x ⊛ traverseArgs Γ args
   traverseTerm Γ t@(lit _)         = pure t
   traverseTerm Γ t@unknown         = pure t
+  traverseTerm Γ (lam v t)         = lam v     <$> traverseAbs (arg (arg-info v m) unknown) Γ t
+    where
+    m = modality relevant quantity-ω
 
   traverseArg Γ (arg i t) = arg i <$> traverseTerm Γ t
   traverseArgs Γ []       = pure []

src/Tactic/RingSolver/Core/ReflectionHelp.agda

@@ -38,8 +38,8 @@ vlams : ∀ {n} → Vec String n → Term → Term
 vlams vs xs = Vec.foldr (const Term) (λ v vs → lam visible (abs v vs)) xs vs
 
 getVisible : Arg Term → Maybe Term
-getVisible (arg (arg-info visible relevant) x) = just x
-getVisible _                                   = nothing
+getVisible (arg (arg-info visible _) x) = just x
+getVisible _                            = nothing
 
 getArgs : ∀ n → Term → Maybe (Vec Term n)
 getArgs n (def _ xs) = Maybe.map Vec.reverse (List.foldl f c (List.mapMaybe getVisible xs) n)