Tauto.agda

open import Data.List.Base

open import Data.Bool
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Unit

open import Function

open import Level using (Level)

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

open import Agda.Builtin.Reflection using ( getInstances )

variable
  ℓ : Level
  A B C D : Set ℓ
  x y z : A

Macro = Term → TC ⊤

ctxArgs : TC (Args Term)
ctxArgs = loop 0 [] <$> getContext
  where
    loop : ℕ → Args Term → Args Type → Args Term
    loop _ acc []             = acc
    loop n acc (arg i a ∷ as) = loop (suc n) (arg i (var n []) ∷ acc) as

-- The type `Hint A` contains a macro that should be applied to a hole
-- of type `A`. Here `A` is just a phantom parameter, but it will be
-- used by the `tauto` macro to determine what hints to try.
record Hint (A : Set ℓ) : Set where
  field
    theHint : Macro
open Hint public

-- The `tauto'` macro will create a new meta of type `Hint (typeOf
-- hole)` and then call `tryInstances` to try all the hints that apply
-- to the hole in turn until one succeeds.
tauto' : Macro
tauto' hole = do
  -- Block if the type is a meta, to avoid overly eager execution of
  -- hint macros.
  inferType hole >>= λ where
    (meta m _) → blockOnMeta m
    _ → return tt
  -- Create meta that will hold the hint
  hint@(meta m _) ← newMeta (def (quote Hint) (vArg (def (quote typeOf) (vArg hole ∷ [])) ∷ []))
    where _ → typeError (strErr "Hey, what's going on?" ∷ [])
  -- For each of the candidates for the hint meta...
  tryInstances m $ do
    -- ... get the hint ...
    tac ← unquoteTC {A = Macro} (def (quote theHint) (vArg hint ∷ []))
    -- ... and execute it.
    tac hole
  where
    tryInstances : Meta → TC A → TC A
    tryInstances {A = A} x m = do
      args ← ctxArgs
      getInstances x >>= λ where
        []       → typeError (strErr "no instances found" ∷ [])
        (c ∷ []) → tryInstance c args
        cs       → loop cs args
      where
        tryInstance : Term → Args Term → TC A
        tryInstance c args = unify (meta x args) c >> m

        loop : List Term → Args Term → TC A
        loop []       args = typeError (strErr "all instances failed" ∷ [])
        loop (c ∷ cs) args = catchTC (tryInstance c args) (loop cs args)

-- tauto is the macro version of tauto'
macro tauto = tauto'

-- A little helper function for creating subgoals that will
-- recursively be solved by `tauto`
subgoal : (Term → TC ⊤) → TC ⊤
subgoal f = do
  x ← newMeta unknown
  f x
  tauto' x

-- Now we can define new hints in a modular way by declaring new
-- instances of type `Hint ...`.

instance
  tauto-⊤ : Hint ⊤
  tauto-⊤ .theHint hole = return _

instance
  tauto-pair : Hint (A × B)
  tauto-pair .theHint hole =
    subgoal λ hole₁ →
    subgoal λ hole₂ →
    unify hole (con (quote _,_) (vArg hole₁ ∷ vArg hole₂ ∷ []))

instance
  tauto-inj₁ : Hint (A ⊎ B)
  tauto-inj₁ .theHint hole =
    subgoal λ hole' →
    unify hole (con (quote inj₁) (vArg hole' ∷ []))

instance
  tauto-inj₂ : Hint (A ⊎ B)
  tauto-inj₂ .theHint hole =
    subgoal λ hole' →
    unify hole (con (quote inj₂) (vArg hole' ∷ []))

test₁ : (⊤ ⊎ ⊥) × (⊥ ⊎ ⊤)
test₁ = tauto

instance
  tauto-magic : Hint (⊥ → A)
  tauto-magic .theHint hole = unify hole (def (quote ⊥-elim) [])

instance
  tauto-useless : Hint (⊤ → A)
  tauto-useless .theHint hole =
    subgoal λ hole' →
    unify hole (def (quote const) (vArg hole' ∷ []))

instance
  tauto-uncurry : Hint (A × B → C)
  tauto-uncurry .theHint hole =
    subgoal λ hole' →
    unify hole (def (quote uncurry) (vArg hole' ∷ []))

instance
  tauto-split : Hint (A ⊎ B → C)
  tauto-split .theHint hole =
    subgoal λ hole₁ →
    subgoal λ hole₂ →
    unify hole (def (quote [_,_]′) (vArg hole₁ ∷ vArg hole₂ ∷ []))

test₂ : (⊥ × ⊤ ⊎ ⊤ × ⊥) → ⊥
test₂ = tauto

-- TODO: have some priority system so this is only tried when none of
-- the above rules are
instance
  tauto-lam : Hint (A → B)
  tauto-lam .theHint hole = do
    hole' ← extendContext (vArg unknown) (newMeta unknown)
    unify hole (lam visible (abs "x" hole'))
    extendContext (vArg unknown) (tauto' hole')

subgoals : Type → (Args Term → TC ⊤) → TC ⊤
subgoals (meta m _)               _ = blockOnMeta m
subgoals (pi (arg i _) (abs _ b)) f = subgoal (λ x → subgoals b (f ∘ (arg i x ∷_)))
subgoals _                        f = f []

instance
  tauto-var : Hint A
  tauto-var .theHint hole = getContext >>= loop 0
    where
      tryVar : ℕ → Type → TC ⊤
      tryVar n t = subgoals t (λ args → unify hole (var n args))

      loop : ℕ → Args Type → TC ⊤
      loop _ []             = typeError []
      loop n (arg _ a ∷ as) = catchTC (tryVar n a) (loop (suc n) as)

test₃ : A → C → (A ⊎ B) × (B ⊎ C)
test₃ = tauto

test₄ : A → (A → B) → B
test₄ = tauto

contraposition : (A → B) → (B → ⊥) → (A → ⊥)
contraposition = tauto

modusponens : (A → B) × (B → C) → A → C
modusponens = tauto

deMorgan₁ : (A ⊎ B → ⊥) → (A → ⊥) × (B → ⊥)
deMorgan₁ = tauto

deMorgan₂ : (A → ⊥) × (B → ⊥) → (A ⊎ B → ⊥)
deMorgan₂ = tauto

deMorgan₃ : (A → ⊥) ⊎ (B → ⊥) → (A × B → ⊥)
deMorgan₃ = tauto

irrefutability : ((A ⊎ (A → ⊥)) → ⊥) → ⊥
irrefutability = tauto

-- TODO: have some check to prevent tauto from looping here
weakpeirce : ((((A → B) → A) → A) → B) → B
weakpeirce = {!tauto!}  -- tauto loops

-- TODO: figure out how tauto tactics actually work so it can solve
-- this example as well:
test₅ : (A → B ⊎ C) → (B → D) → (C → D) → A → D
test₅ = {!tauto!} -- tauto fails