Changes related to a change to Agda's reflection machinery. (#1480)

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

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

Note that the function showTerm does not print erasure annotations.
However, it also does not print relevance annotations.

Author: nad

CHANGELOG.md

@@ -29,9 +29,11 @@ Non-backwards compatible changes
 
 #### Reflection
 
-* The representation of reflected syntax in `Reflection.Term` and
-  `Reflection.Pattern` has been updated to match the new
-  representation used in Agda 2.6.2. Specifically, the following changes were made:
+* The representation of reflected syntax in `Reflection.Term`,
+  `Reflection.Pattern`, `Reflection.Argument` and
+  `Reflection.Argument.Information` has been updated to match the new
+  representation used in Agda 2.6.2. Specifically, the following
+  changes were made:
 
   * The type of the `var` constructor of the `Pattern` datatype has
     been changed from `(x : String) → Pattern` to `(x : Int) →
@@ -48,6 +50,20 @@ Non-backwards compatible changes
     `prop : (t : Term) → Sort`, `propLit : (n : Nat) → Sort`, and
     `inf : (n : Nat) → Sort`.
 
+  * In `Reflection.Argument.Information` the function `relevance` was
+    replaced by `modality`.
+
+  * The type of the `arg-info` constructor is now
+    `(v : Visibility) (m : Modality) → ArgInfo`.
+
+  * In `Reflection.Argument` (as well as `Reflection`) there is a new
+    pattern synonym `defaultModality`, and the pattern synonyms
+    `vArg`, `hArg` and `iArg` have been changed.
+
+  * Two new modules have been added, `Reflection.Argument.Modality`
+    and `Reflection.Argument.Quantity`. The constructors of the types
+    `Modality` and `Quantity` are reexported from `Reflection`.
+
 #### Other
 
 * `Data.Maybe.Base` now re-exports the definition of `Maybe` given by

src/Reflection.agda

@@ -16,7 +16,7 @@ import Agda.Builtin.Reflection as Builtin
 open import Reflection.Abstraction as Abstraction public
   using (Abs; abs)
 open import Reflection.Argument as Argument public
-  using (Arg; arg; Args; vArg; hArg; iArg)
+  using (Arg; arg; Args; vArg; hArg; iArg; defaultModality)
 open import Reflection.Definition as Definition  public
   using (Definition)
 open import Reflection.Meta as Meta public
@@ -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.Modality'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,17 +9,21 @@
 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)
 
+private
+  variable
+    v v′ : Visibility
+    m m′ : Modality
+
 ------------------------------------------------------------------------
--- Re-exporting the builtins publically
+-- Re-exporting the builtins publicly
 
 open import Agda.Builtin.Reflection public using (ArgInfo)
 open ArgInfo public
@@ -30,23 +34,24 @@ 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′
+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)
+
+private
+  variable
+    r r′ : Relevance
+    q q′ : Quantity
+
+------------------------------------------------------------------------
+-- Re-exporting the builtins publicly
+
+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
+
+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 publicly
+
+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/Argument/Relevance.agda

@@ -13,7 +13,7 @@ open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
--- Re-exporting the builtins publically
+-- Re-exporting the builtins publicly
 
 open import Agda.Builtin.Reflection public using (Relevance)
 open Relevance public

src/Reflection/Argument/Visibility.agda

@@ -14,7 +14,7 @@ open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
--- Re-exporting the builtins publically
+-- Re-exporting the builtins publicly
 
 open import Agda.Builtin.Reflection public using (Visibility)
 open Visibility public

src/Reflection/DeBruijn.agda

@@ -59,7 +59,10 @@ 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 defaultModality) (var 0 []) ∷
+                       [])))
 
 η-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 = defaultModality
 
   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)