{-# 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        = []
downFrom (suc n) = suc n ∷ downFrom n

theorem : ∀ n → sum (map (_^ ) (downFrom n)) *  ≡
                 n * (n + ) * ( * n + )
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) ^  ≡ a ^  +  * a * b + b ^ 

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

proof₁ : ∀ a b → Example a b
proof₁ a b = fromJust $
  prove ((var  ⟨+⟩ var ) ⟨*⟩ (var  ⟨+⟩ var ))
        (var  ⟨*⟩ var  ⟨+⟩ lit  ⟨*⟩ var  ⟨*⟩ var  ⟨+⟩ var  ⟨*⟩ var )
        (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 
                       ; one = lit 
                       ; _+_ = _⟨+⟩_
                       ; _*_ = _⟨*⟩_ }

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


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

open import Builtin.Reflection

-- Primitives --

nameOfNat : Name
nameOfNat = quote Nat

quoteThree : Term
quoteThree = quoteTerm ( +  ofType Nat)

quoteGoalExample : (n : Nat) → n ≥ 
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  []) ∷ [])) []

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.

--  Proof monad (MTac approach)?
--    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
  instance MonadMTac       : Monad MTac
  try                      : MTac Term → MTac Term → MTac Term  -- ?
  exact                    : Term → MTac ⊤
  currentGoal              : MTac Term
  run                      : MTac ⊤ → Term

mtac-tactic : MTac ⊤
mtac-tactic =
  currentGoal >>= λ g →
  exact (proof-tactic g)

proof₅ : ∀ a b → Example a b
proof₅ a b = {!unquote (run mtac-tactic)!}