ElaboratorReflection.agda

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Unit

open import Function

open import Reflection
open import Reflection.TypeChecking.Monad.Syntax

open import Agda.Builtin.Reflection using (withReconstructed)

open import Relation.Binary.PropositionalEquality

-- An example macro
macro
  myFavoriteValue : Term → TC ⊤
  myFavoriteValue hole = do
    goal ← inferType hole
    case goal of λ where
      (def (quote ℕ) [])    → unify hole (lit (nat 42))
      (def (quote Bool) []) → unify hole (con (quote true) [])
      _                     → typeError $ strErr "I don't have a favorite value of type " ∷ termErr goal ∷ []

test₁ : ℕ
test₁ = myFavoriteValue

test₂ : Bool
test₂ = myFavoriteValue

--test₃ : List ℕ
--test₃ = myFavoriteValue


-- A simple 'assumption' tactic that tries each variable in scope
macro
  assumption : Term → TC ⊤
  assumption hole = do
    vars ← length <$> getContext
    tryVars vars
    where
      tryVars : ℕ → TC ⊤
      tryVars zero    = typeError $ strErr "Assumption tactic: all variables failed" ∷ []
      tryVars (suc n) = 
        catchTC (unify hole (var n [])) 
                (tryVars n)

test₄ : Bool → ℕ → Bool
test₄ x y = assumption

test₅ : Bool → ℕ → ℕ
test₅ x y = assumption

--test₆ : Bool → ℕ → List ℕ
--test₆ x y = assumption

macro
  mkConst : {A : Set} → A → Term → TC ⊤
  mkConst {A} v hole = do
    body ← quoteTC (λ (x : A) → v)
    unify hole body

test₆ : Bool → ℕ
test₆ = mkConst 42

test₇ : {A : Set} → A → A → A
test₇ x = mkConst x

macro
  give : {A : Set} → A → Term → TC ⊤
  give x hole = do
    sol ← withReconstructed $ quoteTC x
    `sol ← quoteTC sol
    unify hole sol

test₈ : 5 ≡ 5
test₈ = give refl

macro
  doNothing : Term → TC ⊤
  doNothing hole = return tt

test₉ : ℕ
test₉ = doNothing



{-

Some problems I have with the current design:
---------------------------------------------

1. Lack of (quasi)quoting of terms in both expressions and patterns
2. De Bruijn indices are probably not the best way to represent variables
3. No fine-grained control over what parts of a term are quoted or not
4. Requires too much knowledge of Agda internals to use effectively


Possible questions for discussion:
----------------------------------

- Does your favorite language have similar problems?
- What alternative designs could solve these problems?

-}