Last active
December 3, 2021 09:57
-
-
Save jespercockx/8183b9e098de1c899cd028597ac57aa8 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment