agda-eq-derivation

EqReflection.agda

-- Automatic derivation of equality for inductive types. Examples.
-- Inspired by https://github.com/alhassy/gentle-intro-to-reflection.
-- Tested on: Agda version 2.6.2.1-59c7944, std-lib 1.7

module _ where

open import Data.Bool
open import Data.List
open import Data.Unit
open import Relation.Binary.PropositionalEquality

open import Agda.Builtin.Reflection
open import Reflection


-- Preparation

constructors : Definition → List Name
constructors (data-type pars cs) = cs
constructors _ = []

vra : {A : Set} → A → Arg A
vra = arg (arg-info visible (modality relevant quantity-0))

hra : {A : Set} → A → Arg A
hra = arg (arg-info hidden (modality relevant quantity-0))

map2 : ∀ {a b} {A : Set a} {B : Set b} → (A → A → B) → List A → List B
map2 {A = A} {B = B} f l = map2' f l l
  where
  map2' : (A → A → B) → List A → List A → List B
  map2' f [] _ = []
  map2' f (x ∷ xs) l = map (f x) l ++ map2' f xs l 

mk-cls : Name → Name → Clause
mk-cls q1 q2 with primQNameEquality q1 q2
... | true  = clause [] (vra (con q1 []) ∷ vra (con q2 []) ∷ []) (con (quote true)  [])
... | false = clause [] (vra (con q1 []) ∷ vra (con q2 []) ∷ []) (con (quote false) [])



--  Examples --------------------------------------------------------------

-- Simple type

data QQ : Set where
  aa bb : QQ

ddef : Name → TC ⊤
ddef nom = do
       δ ← getDefinition (quote QQ)
       let clauses = map2 mk-cls (constructors δ)
       defineFun nom clauses

eq : QQ → QQ → Bool
unquoteDef eq = ddef eq 


_ : eq aa aa ≡ true
_ = refl

_ : eq aa bb ≡ false
_ = refl

_ : eq bb bb ≡ true
_ = refl

_ : eq bb aa ≡ false
_ = refl


-- More complicated type

data Typ : Set where
  AA BB : Typ
  
data Val : Typ → Set where
  a1 a2 : Val AA
  b1    : Val BB


ddef2 : Name → TC ⊤
ddef2 nom = do
       δ ← getDefinition (quote Val)
       let clauses = map2 mk-cls (constructors δ)
       defineFun nom clauses

eq2 : {A B : Typ} → (x : Val A) → (y : Val B) → Bool
unquoteDef eq2 = ddef2 eq2 

_ : eq2 a1 a1 ≡ true
_ = refl

_ : eq2 a1 a2 ≡ false
_ = refl

_ : eq2 a1 b1 ≡ false
_ = refl

_ : eq2 a2 a1 ≡ false
_ = refl

_ : eq2 a2 a2 ≡ true
_ = refl

_ : eq2 a2 b1 ≡ false
_ = refl

_ : eq2 b1 a1 ≡ false
_ = refl

_ : eq2 b1 a2 ≡ false
_ = refl

_ : eq2 b1 b1 ≡ true
_ = refl