blob.agda

{-# OPTIONS --verbose tc.constr:1000 #-}
module test2 where

open import Reflection
open import Agda.Builtin.Reflection
open import Prelude.Nat
open import Prelude.Unit
open import Prelude.Equality
open import Prelude.Function
open import Prelude.List
open import Prelude.Maybe


_ifMeta_ : {A : Set} → Term → (Meta → TC A) → TC A
meta x x₁ ifMeta f = f x
_ ifMeta _ = typeError (strErr "Error1" ∷ [])

foo : Constraint → TC Term
foo (valueCmp cmpEq y t1 t2) = return t2
foo _ = typeError (strErr "Error2" ∷ [])


q : Nat → Nat
q zero = zero
q (suc zero) = zero
q (suc (suc zero)) = zero
q (suc (suc (suc zero))) = 4
q (suc (suc (suc (suc n)))) = 4


macro
  mfun : Term → TC ⊤
  mfun hole
       = do
           unify hole (def (quote q) [])
--     = do
--         hole ifMeta (λ x → do
--                              c ← getConstraintsMentioning (x ∷ [])
--                              case c of
--                                λ {[] → typeError (strErr "Error3" ∷ [])
--                                  ; (c ∷ cs) → do
--                                                 g ← foo c
--                                                 unify hole g }
--                              )


g : (Q : Nat → Nat) → Q 3 ≡ 4
g = {!!}

f : q 3 ≡ 4
f = g mfun