The 'absurd' pattern now takes a de Bruijn index in reflected syntax (#1362)

Co-authored-by: Ulf Norell <[email protected]>
Co-authored-by: Guillaume ALLAIS <[email protected]>

Author: 3 people

.travis.yml

@@ -56,7 +56,7 @@ matrix:
              cd ../ &&
              git clone https://github.com/agda/agda &&
              cd agda &&
-             git checkout a8077a59977d55d85743790924adf24dc0c9de2d &&
+             git checkout 696a77052a73f2974763fd2cbb9a80c44acb9d74 &&
              cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
           fi
 

src/Reflection/Annotated.agda

@@ -139,7 +139,7 @@ mutual
     var    : ∀ x → Patternₐ′ Ann (var x)
     lit    : ∀ l → Patternₐ′ Ann (lit l)
     proj   : ∀ f → Patternₐ′ Ann (proj f)
-    absurd : Patternₐ′ Ann absurd
+    absurd : ∀ x → Patternₐ′ Ann (absurd x)
 
 
 -- Mapping a code in the universe to its corresponding primed and
@@ -194,7 +194,7 @@ module _ (annFun : AnnotationFun Ann) where
     annotate′ {⟨pat⟩}     (var x)                = var x
     annotate′ {⟨pat⟩}     (lit l)                = lit l
     annotate′ {⟨pat⟩}     (proj f)               = proj f
-    annotate′ {⟨pat⟩}     absurd                 = absurd
+    annotate′ {⟨pat⟩}     (absurd x)             = absurd x
     annotate′ {⟨sort⟩}    (set t)                = set (annotate t)
     annotate′ {⟨sort⟩}    (lit n)                = lit n
     annotate′ {⟨sort⟩}    unknown                = unknown
@@ -231,7 +231,7 @@ mutual
   map′ ⟨pat⟩       f (var x)              = var x
   map′ ⟨pat⟩       f (lit l)              = lit l
   map′ ⟨pat⟩       f (proj g)             = proj g
-  map′ ⟨pat⟩       f absurd               = absurd
+  map′ ⟨pat⟩       f (absurd x)           = absurd x
   map′ ⟨sort⟩      f (set t)              = set (map f t)
   map′ ⟨sort⟩      f (lit n)              = lit n
   map′ ⟨sort⟩      f unknown              = unknown
@@ -268,7 +268,7 @@ module _ {W : Set ℓ} (ε : W) (_∪_ : W → W → W) where
   defaultAnn ⟨pat⟩       (var x)              = ε
   defaultAnn ⟨pat⟩       (lit l)              = ε
   defaultAnn ⟨pat⟩       (proj f)             = ε
-  defaultAnn ⟨pat⟩       absurd               = ε
+  defaultAnn ⟨pat⟩       (absurd x)           = ε
   defaultAnn ⟨sort⟩      (set t)              = ann t
   defaultAnn ⟨sort⟩      (lit n)              = ε
   defaultAnn ⟨sort⟩      unknown              = ε
@@ -318,7 +318,7 @@ module Traverse {M : Set → Set} (appl : RawApplicative M) where
       traverse′ {⟨pat⟩}     (var x)              = pure (var x)
       traverse′ {⟨pat⟩}     (lit l)              = pure (lit l)
       traverse′ {⟨pat⟩}     (proj f)             = pure (proj f)
-      traverse′ {⟨pat⟩}     absurd               = pure absurd
+      traverse′ {⟨pat⟩}     (absurd x)           = pure (absurd x)
       traverse′ {⟨sort⟩}    (set t)              = set <$> traverse t
       traverse′ {⟨sort⟩}    (lit n)              = pure (lit n)
       traverse′ {⟨sort⟩}    unknown              = pure unknown

src/Reflection/Annotated/Free.agda

@@ -54,6 +54,7 @@ private
 freeVars : AnnotationFun (λ _ → FVs)
 freeVars ⟨term⟩    (var x (⟨ fv ⟩ _))                                      = insert x fv
 freeVars ⟨pat⟩     (var x)                                                 = x ∷ []
+freeVars ⟨pat⟩     (absurd x)                                              = x ∷ []
          -- Note: variables are bound in the clause telescope, so we treat pattern variables as free
 freeVars ⟨clause⟩  (clause {tel = Γ} (⟨ fvΓ ⟩ _) (⟨ fvps ⟩ _) (⟨ fvt ⟩ _)) = fvΓ ∪ close (length Γ) (fvps ∪ fvt)
 freeVars ⟨clause⟩  (absurd-clause {tel = Γ} (⟨ fvΓ ⟩ _) (⟨ fvps ⟩ _))      = fvΓ ∪ close (length Γ) fvps

src/Reflection/Show.agda

@@ -115,7 +115,7 @@ mutual
   showPattern (var x)    = "pat-var" <+> ℕ.show x
   showPattern (lit l)    = showLiteral l
   showPattern (proj f)   = showName f
-  showPattern absurd     = "()"
+  showPattern (absurd _) = "()"
 
   showClause : Clause → String
   showClause (clause tel ps t)      = "[" <+> showTel tel <+> "]" <+> showPatterns ps <+> "→" <+> showTerm t

src/Reflection/Term.agda

@@ -379,43 +379,46 @@ proj-injective refl = refl
 dot-injective : ∀ {x y} → dot x ≡ dot y → x ≡ y
 dot-injective refl = refl
 
+absurd-injective : ∀ {x y} → absurd x ≡ absurd y → x ≡ y
+absurd-injective refl = refl
+
 con c ps ≟-Pattern con c′ ps′ = Dec.map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×-dec ps ≟-Patterns ps′)
 var x    ≟-Pattern var x′     = Dec.map′ (cong var) pat-var-injective (x ℕ.≟ x′)
 lit l    ≟-Pattern lit l′     = Dec.map′ (cong lit) pat-lit-injective (l Literal.≟ l′)
 proj a   ≟-Pattern proj a′    = Dec.map′ (cong proj) proj-injective (a Name.≟ a′)
 dot t    ≟-Pattern dot t′     = Dec.map′ (cong dot) dot-injective (t ≟ t′)
+absurd x ≟-Pattern absurd x′  = Dec.map′ (cong absurd) absurd-injective (x ℕ.≟ x′)
 
 con x x₁ ≟-Pattern dot x₂ = no (λ ())
 con x x₁ ≟-Pattern var x₂ = no (λ ())
 con x x₁ ≟-Pattern lit x₂ = no (λ ())
 con x x₁ ≟-Pattern proj x₂ = no (λ ())
-con x x₁ ≟-Pattern absurd = no (λ ())
+con x x₁ ≟-Pattern absurd x₂ = no (λ ())
 dot x ≟-Pattern con x₁ x₂ = no (λ ())
 dot x ≟-Pattern var x₁ = no (λ ())
 dot x ≟-Pattern lit x₁ = no (λ ())
 dot x ≟-Pattern proj x₁ = no (λ ())
-dot x ≟-Pattern absurd = no (λ ())
+dot x ≟-Pattern absurd x₁ = no (λ ())
 var s ≟-Pattern con x x₁ = no (λ ())
 var s ≟-Pattern dot x = no (λ ())
 var s ≟-Pattern lit x = no (λ ())
 var s ≟-Pattern proj x = no (λ ())
-var s ≟-Pattern absurd = no (λ ())
+var s ≟-Pattern absurd x = no (λ ())
 lit x ≟-Pattern con x₁ x₂ = no (λ ())
 lit x ≟-Pattern dot x₁ = no (λ ())
 lit x ≟-Pattern var _ = no (λ ())
 lit x ≟-Pattern proj x₁ = no (λ ())
-lit x ≟-Pattern absurd = no (λ ())
+lit x ≟-Pattern absurd x₁ = no (λ ())
 proj x ≟-Pattern con x₁ x₂ = no (λ ())
 proj x ≟-Pattern dot x₁ = no (λ ())
 proj x ≟-Pattern var _ = no (λ ())
 proj x ≟-Pattern lit x₁ = no (λ ())
-proj x ≟-Pattern absurd = no (λ ())
-absurd ≟-Pattern con x x₁ = no (λ ())
-absurd ≟-Pattern dot x₁ = no (λ ())
-absurd ≟-Pattern var _ = no (λ ())
-absurd ≟-Pattern lit x = no (λ ())
-absurd ≟-Pattern proj x = no (λ ())
-absurd ≟-Pattern absurd = yes refl
+proj x ≟-Pattern absurd x₁ = no (λ ())
+absurd x ≟-Pattern con x₁ x₂ = no (λ ())
+absurd x ≟-Pattern dot x₁ = no (λ ())
+absurd x ≟-Pattern var _ = no (λ ())
+absurd x ≟-Pattern lit x₁ = no (λ ())
+absurd x ≟-Pattern proj x₁ = no (λ ())
 
 []             ≟-Patterns []             = yes refl
 (arg i p ∷ xs) ≟-Patterns (arg j q ∷ ys) = Lₚ.∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys)

src/Reflection/Traversal.agda

@@ -120,7 +120,7 @@ module _ (actions : Actions) where
   traversePattern Γ (Pattern.var x)    = Pattern.var <$> onVar Γ x
   traversePattern Γ p@(Pattern.lit _)  = pure p
   traversePattern Γ p@(Pattern.proj _) = pure p
-  traversePattern Γ p@Pattern.absurd   = pure p
+  traversePattern Γ (Pattern.absurd x) = Pattern.absurd <$> onVar Γ x
 
   traversePats Γ [] = pure []
   traversePats Γ (arg i p ∷ ps) = _∷_ ∘ arg i <$> traversePattern Γ p ⊛ traversePats Γ ps