{-# OPTIONS --safe --without-K #-}
--------------------------------------------------------------------------------
-- anyOf: take the first term that type checks
--------------------------------------------------------------------------------

module Tactic.AnyOf where

open import Meta.Prelude
open import Meta.Init

open import Reflection.Utils.TCI
open import Reflection.Tactic

open import Class.Monad
open import Class.MonadError.Instances
open import Class.MonadTC.Instances

anyOf' : List Term → ITactic
anyOf' = inDebugPath "anyOf" ∘
  foldl (λ x t → catch (debugLog ("Attempting: " ∷ᵈ t ∷ᵈ []) >> unifyWithGoal t >> debugLog ("Success with: " ∷ᵈ t ∷ᵈ [])) (λ _ → x))
    (logAndError1 "None of the provded terms solve the goal!")

anyOfⁿ : List Name → ITactic
anyOfⁿ = inDebugPath "anyOf" ∘
  foldl (λ x n → catch (debugLog ("Attempting: " ∷ᵈ n ∷ᵈ []) >> unifyWithGoal (n ∙) >> debugLog ("Success with: " ∷ᵈ n ∷ᵈ [])) (λ _ → x))
    (logAndError1 "None of the provded terms solve the goal!")

module _ ⦃ _ : TCOptions ⦄ where
  anyOfᵗ : List Term → Tactic
  anyOfᵗ l = initTac $ anyOf' l

  anyOfⁿᵗ : List Name → Tactic
  anyOfⁿᵗ l = initTac $ anyOfⁿ l

  macro
    anyOf = anyOfᵗ