{-# OPTIONS --safe --without-K #-}
module Tactic.ByEq where

open import Meta.Init hiding (TC)
open import Meta.Prelude
open import Class.Functor.Core; open import Class.Functor.Instances
open import Class.Monad.Core; open import Class.Monad.Instances
open import Reflection using (TC; withNormalisation; inferType; unify)
open import Reflection.Utils

-- Introduce as many arguments as possible and then:
--   1. for those of type `_ ≡ _`, unify with  `refl`
--   2. ignore the rest of the arguments (unify with `_`)
--   3. unify the hole with `refl`
by-eq : Hole → TC ⊤
by-eq hole = do
  ty ← withNormalisation true $ inferType hole
  let ps : Args Pattern
      ps = argTys ty <&> fmap λ {(def (quote _≡_) _) → quote refl ◇; _ → dot unknown}
  unify hole $ pat-lam [ clause [] ps (quote refl ◆) ] []

macro $by-eq = by-eq

private
  -- test that macro works
  _ : ∀ {n m k : ℕ} → n ≡ m → m ≡ k → n ≡ k
  _ = $by-eq

  _ : ∀ {n m k x y : ℕ} → n ≡ m → x ≡ y → m ≡ n
  _ = $by-eq

  -- test that tactic arguments work
  f : {@(tactic by-eq) _ : ∀ {n m : ℕ} → n ≡ m → m ≡ n} → Bool → Bool
  f = id

  _ : f {λ where refl → refl} true ≡ true
  _ = refl

  _ : f {$by-eq} true ≡ true
  _ = refl

  _ : f true ≡ true
  _ = refl

  -- test that normalisation works
  Sym = ∀ {n m : ℕ} → n ≡ m → m ≡ n

  g : {@(tactic by-eq) _ : Sym} → Bool → Bool
  g = id

  _ : g {λ where refl → refl} true ≡ true
  _ = refl

  _ : g {$by-eq} true ≡ true
  _ = refl

  _ : g true ≡ true
  _ = refl