module Nat 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 (⊤)

-- multi-step addtion for natural numbers
-- In this file, `unify` succeeds

data Exp : Set where
  V_ : Nat → Exp
  E  : Exp → Exp → Exp

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

data Reduce* : Exp → Exp → Set where
  id*    : {n : Nat} → Reduce* (V n) (V n)
  trans* : (x y z : Exp) → Reduce x y → Reduce* y z → Reduce* 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 : Reduce (E (V 0) (V 1)) (V 1)
single-step = {!runTC!} -- runTC succeeds
-- single-step = plus refl

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