AnyMacro.agda

--{-# OPTIONS -v any-auto:10 #-}

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties using
  (singleton⁺; map⁺; mapMaybe⁺; ++⁺ˡ; ++⁺ʳ; concat⁺)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Unit

open import Function

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

open import Relation.Binary.Bundles
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Macro = Term → TC ⊤

goalMacro : (Term → Type → TC ⊤) → Macro
goalMacro m hole = do
  goal ← inferType hole >>= reduce
  case goal of λ where
    (meta x _) → blockOnMeta x
    _          → m hole goal

record Hint (f : Name) : Set where
  field
    theHint : List (Arg Term) → Macro


≡-auto' : Macro
≡-auto' = goalMacro λ where
  hole (def (quote _≡_) (_ ∷ _ ∷ arg _ x ∷ arg _ y ∷ _)) →
    unify hole (con (quote refl) [])
  hole goal → typeError (strErr "≡-auto: invalid goal: " ∷ termErr goal ∷ [])

mAny-auto : Macro → Macro
mAny-auto m = goalMacro λ where
  hole (def (quote MAny) (_ ∷ _ ∷ _ ∷ _ ∷ arg _ mx ∷ _)) → do
    hole' ← newMeta unknown
    unify hole (con (quote MAny.just) (vArg hole' ∷ []))
    m hole'
  hole goal → typeError (strErr "mAny-auto: invalid goal: " ∷ termErr goal ∷ [])

data Normalise? : Set where yes no : Normalise?

maybeNormalise : Normalise? → Term → TC Term
maybeNormalise yes = normalise
maybeNormalise no  = return

{-# TERMINATING #-}
any-auto' : {{Normalise?}} → Macro → Macro
any-auto' {{norm}} p-auto = goalMacro λ where
    hole (def (quote Any) (_ ∷ _ ∷ _ ∷ _ ∷ arg _ xs ∷ _)) → do
      debugPrint "any-auto" 10 (strErr "any-auto: found list " ∷ termErr xs ∷ [])
      xs ← maybeNormalise norm xs
      let err = typeError (strErr "any-auto: failed on list: " ∷ termErr xs ∷ [])
      aux p-auto err hole xs
    hole goal → typeError (strErr "any-auto: invalid goal: " ∷ termErr goal ∷ [])
  where
    unknowns : ℕ → List (Arg Term)
    unknowns n = replicate n (hArg unknown)

    fail : TC ⊤
    fail = typeError []

    admit : TC ⊤
    admit = return _

    -- Main loop of the tactic:
    -- * `p-auto` is the macro used for proving `P` holds for an individual element
    -- * `fallback` is the action that should be taken on a failure:
    --   + It should be `admit` when we have only made unforced choices,
    --     and we are not at the top-level
    --   + It should be a hard `typeError` otherwise
    -- * `hole` is the current hole we are trying to fill
    -- * `xs` is the list of elements for which we are trying to prove `Any P`
    aux : (p-auto : Macro) (fallback : TC ⊤) (hole : Term) (xs : Term) → TC ⊤
    aux p-auto fallback hole = λ where
      (con (quote List._∷_) (_ ∷ _ ∷ arg _ x ∷ arg _ xs ∷ _)) → catchTC
        (do debugPrint "any-auto" 10 (strErr "any-auto: trying here " ∷ termErr x ∷ [])
            hole' ← newMeta unknown
            unify hole (con (quote here) (vArg hole' ∷ []))
            p-auto hole')
        (do debugPrint "any-auto" 10 (strErr "any-auto: trying there " ∷ termErr xs ∷ [])
            hole' ← newMeta unknown
            unify hole (con (quote there) (vArg hole' ∷ []))
            aux p-auto fallback hole' xs)
      (def (quote [_]) (_ ∷ _ ∷ arg _ x ∷ _)) → do
        debugPrint "any-auto" 10 (strErr "any-auto: trying singleton⁺ " ∷ termErr x ∷ [])
        hole' ← newMeta unknown
        unify hole (def (quote singleton⁺) (vArg hole' ∷ []))
        catchTC (p-auto hole') fallback
      (def (quote map) (_ ∷ _ ∷ _ ∷ _ ∷ arg _ f ∷ arg _ xs ∷ _)) → do
        debugPrint "any-auto" 10 (strErr "any-auto: trying map⁺ " ∷ termErr xs ∷ [])
        hole' ← newMeta unknown
        unify hole (def (quote map⁺) (unknowns 4 ++ hArg f ∷ unknowns 2 ++ hArg xs ∷ vArg hole' ∷ []))
        aux p-auto admit hole' xs
      (def (quote mapMaybe) (_ ∷ _ ∷ _ ∷ _ ∷ arg _ f ∷ arg _ xs ∷ _)) → do
        debugPrint "any-auto" 10 (strErr "any-auto: trying mapMaybe⁺ " ∷ termErr xs ∷ [])
        hole' ← newMeta unknown
        unify hole (def (quote mapMaybe⁺) (vArg f ∷ vArg xs ∷ vArg hole' ∷ []))
        aux (mAny-auto p-auto) admit hole' xs
      (def (quote _++_) (_ ∷ _ ∷ arg _ xs ∷ arg _ ys ∷ _)) → catchTC
        (do debugPrint "any-auto" 10 (strErr "any-auto: trying ++⁺ˡ " ∷ termErr xs ∷ [])
            hole' ← newMeta unknown
            unify hole (def (quote ++⁺ˡ) (unknowns 4 ++ hArg xs ∷ vArg hole' ∷ []))
            aux p-auto fail hole' xs)
        (do debugPrint "any-auto" 10 (strErr "any-auto: trying ++⁺ʳ " ∷ termErr ys ∷ [])
            hole' ← newMeta unknown
            unify hole (def (quote ++⁺ʳ) (vArg xs ∷ vArg hole' ∷ []))
            aux p-auto fallback hole' xs)
      (def (quote concat) (_ ∷ _ ∷ arg _ xss ∷ _)) → do
        debugPrint "any-auto" 10 (strErr "any-auto: trying concat⁺ " ∷ termErr xss ∷ [])
        hole' ← newMeta unknown
        unify hole (def (quote concat⁺) (unknowns 4 ++ hArg xss ∷ vArg hole' ∷ []))
        aux (any-auto' p-auto) admit hole' xss
      xs → fallback

macro
  any-auto : {{Normalise?}} → Macro → Macro
  any-auto = any-auto'

  ∈-auto : {{Normalise?}} → Macro
  ∈-auto = any-auto' ≡-auto'

private module _ where
  -- In the test cases below, you can see the actual output of the
  -- macro by creating a hole around `∈-auto` and pressing `C-u C-c
  -- C-m` (without the `C-u` you get the reduced proofs).

  instance _ = Normalise?.no

  test₁ : 3 ∈ (1 ∷ 2 ∷ 3 ∷ [])
  test₁ = ∈-auto

  test₂ : {x : ℕ} → x ∈ [ x ]
  test₂ = ∈-auto

  test₃ : 3 ∈ map (_+ 1) (0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
  test₃ = ∈-auto

  pred : ℕ → Maybe ℕ
  pred zero    = nothing
  pred (suc n) = just n

  test₄ : 2 ∈ mapMaybe pred (0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
  test₄ = ∈-auto

  test₅ : 3 ∈ (0 ∷ 1 ∷ []) ++ (2 ∷ 3 ∷ [])
  test₅ = ∈-auto

  test₆ : 3 ∈ concat ([ 1 ] ∷ [ 2 ] ∷ [] ∷ (3 ∷ 4 ∷ []) ∷ [])
  test₆ = ∈-auto