← Back

Modules

Leios

  • Abstract
  • Base
  • Blocks
  • Config
  • Defaults
  • FFD
  • Foreign.BaseTypes
  • Foreign.HsTypes
  • Foreign.Types
  • Foreign.Util
  • KeyRegistration
  • Network
  • Prelude
  • Protocol
  • Short
  • Short.Trace.Verifier
  • Simplified
  • Simplified.Deterministic
  • SpecStructure
  • Traces
  • Voting
  • VRF

Network

  • BasicBroadcast
  • Leios
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152
{-# OPTIONS --safe --without-K #-}
--------------------------------------------------------------------------------
-- assumption: try to solve the goal with one of the available assumptions
--------------------------------------------------------------------------------
 
module Tactic.Assumption where
 
open import Meta.Prelude
open import Meta.Init
 
open import Class.Functor
open import Class.Monad
open import Class.MonadError.Instances
open import Class.MonadReader.Instances
open import Class.MonadTC.Instances
 
open import Reflection.Tactic
open import Reflection.Utils
open import Reflection.Utils.TCI
 
instance
_ = Functor-M
 
solve : ⦃ TCOptions ⦄ → Term → Tactic
solve 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' : ITactic
assumption' = 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