Update decidable equality of reflected syntax (#1226)

Author: jespercockx

.travis.yml

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

src/Reflection/Pattern.agda

@@ -10,6 +10,7 @@ module Reflection.Pattern where
 
 open import Data.List.Base hiding (_++_)
 open import Data.List.Properties
+import Data.Nat as Nat
 open import Data.Product
 open import Data.String as String using (String; braces; parens; _++_; _<+>_)
 import Reflection.Literal as Literal
@@ -32,69 +33,16 @@ open import Agda.Builtin.Reflection public using (Pattern)
 open Pattern public
 
 ------------------------------------------------------------------------
--- Decidable equality
-
-con-injective₁ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′
-con-injective₁ refl = refl
-
-con-injective₂ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → args ≡ args′
-con-injective₂ refl = refl
-
-con-injective : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
-con-injective = < con-injective₁ , con-injective₂ >
-
-var-injective : ∀ {x y} → var x ≡ var y → x ≡ y
-var-injective refl = refl
-
-lit-injective : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
-lit-injective refl = refl
-
-proj-injective : ∀ {x y} → proj x ≡ proj y → x ≡ y
-proj-injective refl = refl
-
-_≟s_ : Decidable (_≡_ {A = Args Pattern})
-_≟_  : Decidable (_≡_ {A = Pattern})
-
-con c ps ≟ con c′ ps′ = Dec.map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec ps ≟s ps′)
-var s    ≟ var s′     = Dec.map′ (cong var) var-injective (s String.≟ s′)
-lit l    ≟ lit l′     = Dec.map′ (cong lit) lit-injective (l Literal.≟ l′)
-proj a   ≟ proj a′    = Dec.map′ (cong proj) proj-injective (a Name.≟ a′)
-
-con x x₁ ≟ dot = no (λ ())
-con x x₁ ≟ var x₂ = no (λ ())
-con x x₁ ≟ lit x₂ = no (λ ())
-con x x₁ ≟ proj x₂ = no (λ ())
-con x x₁ ≟ absurd = no (λ ())
-dot ≟ con x x₁ = no (λ ())
-dot ≟ dot = yes refl
-dot ≟ var x = no (λ ())
-dot ≟ lit x = no (λ ())
-dot ≟ proj x = no (λ ())
-dot ≟ absurd = no (λ ())
-var s ≟ con x x₁ = no (λ ())
-var s ≟ dot = no (λ ())
-var s ≟ lit x = no (λ ())
-var s ≟ proj x = no (λ ())
-var s ≟ absurd = no (λ ())
-lit x ≟ con x₁ x₂ = no (λ ())
-lit x ≟ dot = no (λ ())
-lit x ≟ var _ = no (λ ())
-lit x ≟ proj x₁ = no (λ ())
-lit x ≟ absurd = no (λ ())
-proj x ≟ con x₁ x₂ = no (λ ())
-proj x ≟ dot = no (λ ())
-proj x ≟ var _ = no (λ ())
-proj x ≟ lit x₁ = no (λ ())
-proj x ≟ absurd = no (λ ())
-absurd ≟ con x x₁ = no (λ ())
-absurd ≟ dot = no (λ ())
-absurd ≟ var _ = no (λ ())
-absurd ≟ lit x = no (λ ())
-absurd ≟ proj x = no (λ ())
-absurd ≟ absurd = yes refl
-
-[]             ≟s []             = yes refl
-(arg i p ∷ xs) ≟s (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≟ q)) (xs ≟s ys)
-
-[]      ≟s (_ ∷ _) = no λ()
-(_ ∷ _) ≟s []      = no λ()
+-- Re-exporting definitions that used to be here
+
+open import Reflection.Term
+  using    ( proj-injective )
+  renaming ( pat-con-injective₁ to con-injective₁
+           ; pat-con-injective₂ to con-injective₂
+           ; pat-con-injective  to con-injective
+           ; pat-var-injective  to var-injective
+           ; pat-lit-injective  to lit-injective
+           ; _≟-Patterns_       to _≟s_
+           ; _≟-Pattern_        to _≟_
+           )
+  public

src/Reflection/Show.agda

@@ -16,6 +16,7 @@ import Data.Float as Float
 open import Data.List hiding (_++_; intersperse)
 import Data.Nat as ℕ
 import Data.Nat.Show as ℕ
+open import Data.Product using (_×_; _,_)
 open import Data.String as String
 import Data.Word as Word
 open import Relation.Nullary using (yes; no)
@@ -65,26 +66,6 @@ showLiteral (string x) = String.show x
 showLiteral (name x)   = showName x
 showLiteral (meta x)   = showMeta x
 
-mutual
-
-  showPatterns : List (Arg Pattern) → String
-  showPatterns []       = ""
-  showPatterns (a ∷ ps) = showArg a <+> showPatterns ps
-    where
-    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))
-
-  showPattern : Pattern → String
-  showPattern (con c []) = showName c
-  showPattern (con c ps) = parens (showName c <+> showPatterns ps)
-  showPattern dot        = "._"
-  showPattern (var s)    = s
-  showPattern (lit l)    = showLiteral l
-  showPattern (proj f)   = showName f
-  showPattern absurd     = "()"
-
 private
   -- add appropriate parens depending on the given visibility
   visibilityParen : Visibility → String → String
@@ -118,14 +99,36 @@ mutual
   showSort (lit n) = "Set" ++ ℕ.show n -- no space to disambiguate from set t
   showSort unknown = "unknown"
 
+  showPatterns : List (Arg Pattern) → String
+  showPatterns []       = ""
+  showPatterns (a ∷ ps) = showArg a <+> showPatterns ps
+    where
+    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))
+
+  showPattern : Pattern → String
+  showPattern (con c []) = showName c
+  showPattern (con c ps) = parens (showName c <+> showPatterns ps)
+  showPattern (dot t)    = "." ++ parens (showTerm t)
+  showPattern (var x)    = "pat-var" <+> ℕ.show x
+  showPattern (lit l)    = showLiteral l
+  showPattern (proj f)   = showName f
+  showPattern absurd     = "()"
+
   showClause : Clause → String
-  showClause (clause ps t)      = showPatterns ps <+> "→" <+> showTerm t
-  showClause (absurd-clause ps) = showPatterns ps
+  showClause (clause tel ps t)      = "[" <+> showTel tel <+> "]" <+> showPatterns ps <+> "→" <+> showTerm t
+  showClause (absurd-clause tel ps) = "[" <+> showTel tel <+> "]" <+> showPatterns ps
 
   showClauses : List Clause → String
   showClauses []       = ""
   showClauses (c ∷ cs) = showClause c <+> ";" <+> showClauses cs
 
+  showTel : List (String × Arg Type) → String
+  showTel [] = ""
+  showTel ((x , arg i t) ∷ tel) = visibilityParen (visibility i) (x <+> ":" <+> showTerm t) ++ showTel tel
+
 showDefinition : Definition → String
 showDefinition (function cs)       = "function" <+> braces (showClauses cs)
 showDefinition (data-type pars cs) =

src/Reflection/Term.agda

@@ -12,15 +12,16 @@ open import Data.List.Base hiding (_++_)
 import Data.List.Properties as Lₚ
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Product
+import Data.Product.Properties as Product
 open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.String as String using (String)
 open import Reflection.Abstraction
 open import Reflection.Argument
 open import Reflection.Argument.Information using (visibility)
 import Reflection.Argument.Visibility as Visibility; open Visibility.Visibility
 import Reflection.Literal as Literal
 import Reflection.Meta as Meta
 open import Reflection.Name as Name using (Name)
-import Reflection.Pattern as Pattern
 open import Relation.Nullary
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Decidable as Dec
@@ -31,17 +32,21 @@ open import Relation.Binary.PropositionalEquality
 -- Re-exporting the builtin type and constructors
 
 open import Agda.Builtin.Reflection as Builtin public
-  using (Sort; Type; Term; Clause)
+  using (Sort; Type; Term; Clause; Pattern)
 open Sort public
 open Term public renaming (agda-sort to sort)
 open Clause public
+open Pattern public
 
 ------------------------------------------------------------------------
 -- Handy synonyms
 
 Clauses : Set
 Clauses = List Clause
 
+Telescope : Set
+Telescope = List (String × Arg Type)
+
 -- Pattern synonyms for more compact presentation
 
 pattern vLam s t           = lam visible   (abs s t)
@@ -81,31 +86,42 @@ suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ (i ⋯⟅∷⟆ xs)
 ------------------------------------------------------------------------
 -- Decidable equality
 
-clause-injective₁ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′
+clause-injective₁ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → tel ≡ tel′
 clause-injective₁ refl = refl
 
-clause-injective₂ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → b ≡ b′
+clause-injective₂ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → ps ≡ ps′
 clause-injective₂ refl = refl
 
-clause-injective : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′ × b ≡ b′
-clause-injective = < clause-injective₁ , clause-injective₂ >
+clause-injective₃ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → b ≡ b′
+clause-injective₃ refl = refl
+
+clause-injective : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → tel ≡ tel′ × ps ≡ ps′ × b ≡ b′
+clause-injective = < clause-injective₁ , < clause-injective₂ , clause-injective₃ > >
+
+absurd-clause-injective₁ : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′
+absurd-clause-injective₁ refl = refl
+
+absurd-clause-injective₂ : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → ps ≡ ps′
+absurd-clause-injective₂ refl = refl
 
-absurd-clause-injective : ∀ {ps ps′} → absurd-clause ps ≡ absurd-clause ps′ → ps ≡ ps′
-absurd-clause-injective refl = refl
+absurd-clause-injective : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′ × ps ≡ ps′
+absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective₂ >
 
 infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
         _≟-Clause_ _≟-Clauses_ _≟_
-        _≟-Sort_
-
-_≟-AbsTerm_ : DecidableEquality (Abs Term)
-_≟-AbsType_ : DecidableEquality (Abs Type)
-_≟-ArgTerm_ : DecidableEquality (Arg Term)
-_≟-ArgType_ : DecidableEquality (Arg Type)
-_≟-Args_    : DecidableEquality (Args Term)
-_≟-Clause_  : DecidableEquality Clause
-_≟-Clauses_ : DecidableEquality Clauses
-_≟_         : DecidableEquality Term
-_≟-Sort_    : DecidableEquality Sort
+        _≟-Sort_ _≟-Pattern_ _≟-Patterns_
+
+_≟-AbsTerm_  : DecidableEquality (Abs Term)
+_≟-AbsType_  : DecidableEquality (Abs Type)
+_≟-ArgTerm_  : DecidableEquality (Arg Term)
+_≟-ArgType_  : DecidableEquality (Arg Type)
+_≟-Args_     : DecidableEquality (Args Term)
+_≟-Clause_   : DecidableEquality Clause
+_≟-Clauses_  : DecidableEquality Clauses
+_≟_          : DecidableEquality Term
+_≟-Sort_     : DecidableEquality Sort
+_≟-Patterns_ : Decidable (_≡_ {A = Args Pattern})
+_≟-Pattern_  : Decidable (_≡_ {A = Pattern})
 
 -- Decidable equality 'transformers'
 -- We need to inline these because the terms are not sized so termination
@@ -127,27 +143,38 @@ arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′)
 []       ≟-Clauses (_ ∷ _)  = no λ()
 (_ ∷ _)  ≟-Clauses []       = no λ()
 
-
-clause ps b ≟-Clause clause ps′ b′ =
-  Dec.map′ (uncurry (cong₂ clause)) clause-injective (ps Pattern.≟s ps′ ×-dec b ≟ b′)
-absurd-clause ps ≟-Clause absurd-clause ps′ =
-  Dec.map′ (cong absurd-clause) absurd-clause-injective (ps Pattern.≟s ps′)
-clause _ _      ≟-Clause absurd-clause _ = no λ()
-absurd-clause _ ≟-Clause clause _ _      = no λ()
-
-var-injective₁ : ∀ {x x′ args args′} → var x args ≡ var x′ args′ → x ≡ x′
+_≟-Telescope_ : DecidableEquality Telescope
+[] ≟-Telescope [] = yes refl
+((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = Lₚ.∷-dec
+  (map′ (uncurry (cong₂ _,_)) Product.,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′)))
+  (tel ≟-Telescope tel′)
+[] ≟-Telescope (_ ∷ _) = no λ ()
+(_ ∷ _) ≟-Telescope [] = no λ ()
+
+clause tel ps b ≟-Clause clause tel′ ps′ b′ =
+  Dec.map′ (λ (tel≡tel′ , ps≡ps′ , b≡b′) → cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′)
+           clause-injective
+           (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′ ×-dec b ≟ b′)
+absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ =
+  Dec.map′ (uncurry (cong₂ absurd-clause))
+           absurd-clause-injective
+           (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′)
+clause _ _ _      ≟-Clause absurd-clause _ _ = no λ()
+absurd-clause _ _ ≟-Clause clause _ _ _      = no λ()
+
+var-injective₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′
 var-injective₁ refl = refl
 
-var-injective₂ : ∀ {x x′ args args′} → var x args ≡ var x′ args′ → args ≡ args′
+var-injective₂ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → args ≡ args′
 var-injective₂ refl = refl
 
 var-injective :  ∀ {x x′ args args′} → var x args ≡ var x′ args′ → x ≡ x′ × args ≡ args′
 var-injective = < var-injective₁ , var-injective₂ >
 
-con-injective₁ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′
+con-injective₁ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → c ≡ c′
 con-injective₁ refl = refl
 
-con-injective₂ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → args ≡ args′
+con-injective₂ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → args ≡ args′
 con-injective₂ refl = refl
 
 con-injective : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
@@ -329,3 +356,69 @@ lit _   ≟-Sort set _   = no λ()
 lit _   ≟-Sort unknown = no λ()
 unknown ≟-Sort set _   = no λ()
 unknown ≟-Sort lit _   = no λ()
+
+
+pat-con-injective₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′
+pat-con-injective₁ refl = refl
+
+pat-con-injective₂ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → args ≡ args′
+pat-con-injective₂ refl = refl
+
+pat-con-injective : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
+pat-con-injective = < pat-con-injective₁ , pat-con-injective₂ >
+
+pat-var-injective : ∀ {x y} → var x ≡ var y → x ≡ y
+pat-var-injective refl = refl
+
+pat-lit-injective : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
+pat-lit-injective refl = refl
+
+proj-injective : ∀ {x y} → proj x ≡ proj y → x ≡ y
+proj-injective refl = refl
+
+dot-injective : ∀ {x y} → dot x ≡ dot y → x ≡ y
+dot-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′)
+
+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 (λ ())
+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 (λ ())
+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 (λ ())
+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 (λ ())
+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
+
+[]             ≟-Patterns []             = yes refl
+(arg i p ∷ xs) ≟-Patterns (arg j q ∷ ys) = Lₚ.∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys)
+
+[]      ≟-Patterns (_ ∷ _) = no λ()
+(_ ∷ _) ≟-Patterns []      = no λ()