```{-# OPTIONS -v profile.interactive:10 #-}
--- === Reflections on Reflection === ---
---
---           Ulf Norell

module Reflection where

open import Prelude
open import Tactic.Nat

--- === Introduction === ---

downFrom : Nat → List Nat
downFrom  0      = []
downFrom (suc n) = suc n ∷ downFrom n

theorem : ∀ n → sum (map (_^ 2) (downFrom n)) * 6 ≡
n * (n + 1) * (2 * n + 1)
theorem = induction

--- === Decision Procedures === ---

-- Basic idea:
--   - represent problem domain as a data type
--   - write a function to decide if a problem
--     is solvable
--   - prove that the function is sound

open import Tactic.Nat.Exp
open import Tactic.Nat.NF

--- === Decision procedure proofs === ---

import Tactic.Nat.Auto.Lemmas as Lemmas

module _ {Atom : Set} {{_ : Eq Atom}} {{_ : Ord Atom}} where

sound : ∀ e (ρ : Env Atom) → ⟦ e ⟧e ρ ≡ ⟦ norm e ⟧n ρ
sound = Lemmas.sound

prove : ∀ e₁ e₂ (ρ : Env Atom) → Maybe (⟦ e₁ ⟧e ρ ≡ ⟦ e₂ ⟧e ρ)
prove e₁ e₂ ρ with norm e₁ == norm e₂
... | no  _  = nothing
... | yes eq = just \$
sound e₁ ρ ⟨≡⟩
cong (λ nf → ⟦ nf ⟧n ρ) eq ⟨≡⟩ʳ
sound e₂ ρ

--- === Example === ---

Example : Nat → Nat → Set
Example a b = (a + b) ^ 2 ≡ a ^ 2 + 2 * a * b + b ^ 2

mkEnv : List Nat → Env Nat
mkEnv xs n = maybe 0 id (index xs n)

proof₁ : ∀ a b → Example a b
proof₁ a b = fromJust \$
prove ((var 0 ⟨+⟩ var 1) ⟨*⟩ (var 0 ⟨+⟩ var 1))
(var 0 ⟨*⟩ var 0 ⟨+⟩ lit 2 ⟨*⟩ var 0 ⟨*⟩ var 1 ⟨+⟩ var 1 ⟨*⟩ var 1)
(mkEnv (a ∷ b ∷ []))

--- === Type classes can help === ---

instance
NumberExp : ∀ {Atom} → Number (Exp Atom)
NumberExp = record { Constraint = λ _ → ⊤
; fromNat    = λ n → lit n }

SemiringExp : ∀ {Atom} → Semiring (Exp Atom)
SemiringExp = record { zro = lit 0
; one = lit 1
; _+_ = _⟨+⟩_
; _*_ = _⟨*⟩_ }

proof₂ : ∀ a b → Example a b
proof₂ a b = fromJust \$
prove ((x + y) ^ 2)
(x ^ 2 + 2 * x * y + y ^ 2) ρ
where x = var 0
y = var 1
ρ  = mkEnv (a ∷ b ∷ [])

--- === Reflection === ---

open import Builtin.Reflection

-- Primitives --

nameOfNat : Name
nameOfNat = quote Nat

quoteThree : Term
quoteThree = quoteTerm (1 + 2 ofType Nat)

quoteGoalExample : (n : Nat) → n ≥ 0
quoteGoalExample = quoteGoal g in {!g!}

three : unquote (def nameOfNat [])
three = unquote quoteThree

--- === Using reflection === ---

open import Tactic.Nat.Reflect
open import Tactic.Reflection.Quote

-- fromJust (prove e₁ e₂ ρ)

parseGoal : Term → Maybe ((Exp Var × Exp Var) × List Term)
parseGoal = termToEq

proof-tactic : Term → Term
proof-tactic goal =
case parseGoal goal of λ
{ nothing → lit (string "todo: error msg")
; (just ((e₁ , e₂) , Γ)) →
def (quote fromJust) \$
vArg (def (quote prove)
(vArg (` e₁) ∷ vArg (` e₂) ∷
vArg (quotedEnv Γ) ∷ [])) ∷ []
}

proof₃ : ∀ a b → Example a b
proof₃ a b = quoteGoal g in unquote (proof-tactic g)

--- === Macros === ---

-- macro f : Term → .. → Term
--   f v₁ .. vn desugars to
--   unquote (f (quoteTerm v₁) .. (quoteTerm vn))

-- proof₃ a b = quoteGoal g in unquote (proof-tactic g)

macro
magic : Term
magic = quote-goal \$ abs "g" \$
unquote-term (def (quote proof-tactic)
(vArg (var 0 []) ∷ [])) []

proof₄ : ∀ a b → Example a b
proof₄ a b = magic

--- === Stepping back === ---

-- Multiple levels
--   Level 0 tactic: Problem → Maybe Proof
--      fully certified
--
--   Level 1 tactic: Term → Term
--      reflected goal → reflected call to level 0
--
--   Level 2 tactic: Term
--      macro wrapping reflected level 1 in quote-goal

--  Problems: getting information between levels.

--  Combining tactics. Each tactic has its own Proof type,
--  so hard to combine at level 0.

--    Would let you do all the composing at level 1 and get rid of level 2.

--- === MTac === ---

postulate
MTac                     : Set → Set
instance FunctorMTac     : Functor MTac
instance ApplicativeMTac : Applicative MTac