module Nat-param where

open import Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List using (_∷_; [])
open import Agda.Builtin.Nat using (Nat; _+_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Unit using (⊤; tt)

-- datatype definitions are parameterized, but parameters don't have real meanings
-- `unify` fails in the multi-step example

data Typ : Set where
  ⋆   : Typ

data Exp (v : Typ) : Set where
  V_ : Nat → Exp v
  E  : Exp v → Exp v → Exp v

data Reduce (v : Typ) : Exp v → Exp v → Set where
  plus_  : {n m r : Nat} → (n + m ≡ r) → Reduce v (E (V n) (V m)) (V r)
  right_ : {y : Exp v} {n m : Nat} → Reduce v y (V m) → Reduce v (E (V n) y) (E (V n) (V m))
  left_  : {x y : Exp v} {n : Nat} → Reduce v x (V n) → Reduce v (E x y) (E (V n) y)

data Reduce* (v : Typ) : Exp v → Exp v → Set where
  id*    : {n : Nat} → Reduce* v (V n) (V n)
  trans* : (x y z : Exp v) → Reduce v x y → Reduce* v y z → Reduce* v x z

macro
  runTC : Term → TC ⊤
  runTC hole = do
    m ← newMeta unknown
    unify (con (quote plus_) (arg (arg-info visible relevant) m ∷ [])) hole

single-step : (v : Typ) → Reduce v (E (V 0) (V 1)) (V 1)
single-step v = {!runTC!} -- runTC succeeds
-- single-step v = plus refl

multi-step : (v : Typ) → Reduce* v (E (V 0) (V 1)) (V 1)
multi-step v = trans* (E (V 0) (V 1))
                      {!!} -- 2nd arg
                      (V 1)
                      {!runTC!} -- 4th arg, runTC fails
                      {!!}
-- multi-step v = trans* (E (V 0) (V 1)) (V 1) (V 1) (plus refl) id*