12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152{-# OPTIONS --safe --without-K #-}---------------------------------------------------------------------------------- assumption: try to solve the goal with one of the available assumptions-------------------------------------------------------------------------------- module Tactic.Assumption where open import Meta.Preludeopen import Meta.Init open import Class.Functoropen import Class.Monadopen import Class.MonadError.Instancesopen import Class.MonadReader.Instancesopen import Class.MonadTC.Instances open import Reflection.Tacticopen import Reflection.Utilsopen import Reflection.Utils.TCI instance _ = Functor-M solve : ⦃ TCOptions ⦄ → Term → Tacticsolve t = initTac $ runSpeculative $ do inj₁ goal ← reader TCEnv.goal where _ → error1 "solve: Goal is not a term!" metas ← findMetas <$> checkType t goal if null metas then (_, true) <$> unify goal t else (_, false) <$> error1 "Unsolved metavariables remaining!" assumption' : ITacticassumption' = inDebugPath "assumption" do c ← getContext foldl (λ x k → do catch (unifyWithGoal (♯ k) >> debugLog ("Success with: " ∷ᵈ ♯ k ∷ᵈ [])) (λ _ → x)) (logAndError1 "No valid assumption!") (downFrom $ length c) module _ ⦃ _ : TCOptions ⦄ where macro assumption = initTac assumption' assumptionOpts = initTacOpts assumption' private open import Tactic.Defaults module Test where test₁ : {A B : Set} → A → B → A test₁ a b = assumption test₂ : {A B : Set} → A → B → B test₂ a b = assumption