{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Tactic.By {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where
open Derived-definitions-and-properties eq
import Agda.Builtin.Bool as B
open import Agda.Builtin.Nat using (_==_)
open import Agda.Builtin.String
open import Prelude
open import List eq
open import Monad eq
open import Monad.State eq hiding (set)
open import TC-monad eq as TC hiding (Type)
type-of-cong : (Term → Term → TC.Type) → ℕ → TC.Type
type-of-cong equality n = levels (suc n)
where
arguments : ℕ → ℕ → List (Arg Term)
arguments delta (suc m) = varg (var (delta + 2 * m + 1 + n) []) ∷
arguments delta m
arguments delta zero = []
equalities : ℕ → TC.Type
equalities (suc m) =
pi (varg (equality (var (1 + 2 * m + 1 + (n ∸ suc m)) [])
(var (0 + 2 * m + 1 + (n ∸ suc m)) []))) $
abs "x≡y" $
equalities m
equalities zero =
equality (var n (arguments 1 n))
(var n (arguments 0 n))
function-type : ℕ → TC.Type
function-type (suc m) = pi (varg (var (3 * n) []))
(abs "_" (function-type m))
function-type zero = var (3 * n) []
variables : ℕ → TC.Type
variables (suc m) =
pi (harg unknown) $ abs "x" $
pi (harg unknown) $ abs "y" $
variables m
variables zero =
pi (varg (function-type n)) $ abs "f" $
equalities n
types : ℕ → TC.Type
types (suc m) = pi (harg (agda-sort (set (var n [])))) $ abs "A" $
types m
types zero = variables n
levels : ℕ → TC.Type
levels (suc n) = pi (harg (def (quote Level) [])) $ abs "a" $
levels n
levels zero = types (suc n)
⟨_⟩ : ∀ {a} {A : Type a} → A → A
⟨_⟩ = id
{-# NOINLINE ⟨_⟩ #-}
module _
(deconstruct-equality :
TC.Type → TC (Maybe (Term × TC.Type × Term × Term)))
where
private
blockOnMeta′ : {A : Type} → String → Meta → TC A
blockOnMeta′ s m = do
debugPrint "by" 20
(strErr "by/⟨by⟩ is blocking on meta" ∷
strErr (primShowMeta m) ∷ strErr "in" ∷ strErr s ∷ [])
blockOnMeta m
deconstruct-equality′ :
List ErrorPart → TC.Type → TC (Term × TC.Type × Term × Term)
deconstruct-equality′ err (meta m _) =
blockOnMeta′ "deconstruct-equality′" m
deconstruct-equality′ err t = do
just r ← deconstruct-equality t
where nothing → typeError err
return r
apply-to-metas : TC.Type → Term → TC (TC.Type × Term)
apply-to-metas A t = apply A t =<< compute-args fuel [] A
where
fuel : ℕ
fuel = 100
mutual
compute-args :
ℕ → List (Arg Term) → TC.Type → TC (List (Arg Term))
compute-args zero _ _ =
typeError (strErr "apply-to-metas failed" ∷ [])
compute-args (suc n) args τ =
compute-args′ n args =<< reduce τ
compute-args′ :
ℕ → List (Arg Term) → TC.Type → TC (List (Arg Term))
compute-args′ n args (pi a@(arg i _) (abs x τ)) =
extendContext x a $
compute-args n (arg i unknown ∷ args) τ
compute-args′ n args (meta x _) =
blockOnMeta′ "apply-to-metas" x
compute-args′ n args _ = return (reverse args)
module ⟨By⟩
{Ctxt : Type}
(context : TC Ctxt)
(sym : Ctxt → Term → Term)
(cong : Ctxt → Term → Term → Term → Term → Term)
(cong-with-lhs-and-rhs : Bool)
where
private
⟨by⟩-tactic : ∀ {a} {A : Type a} → A → Term → TC Term
⟨by⟩-tactic {A} t goal = do
goal-type ← reduce =<< inferType goal
_ , _ , lhs , _ ← deconstruct-equality′ err₁ goal-type
f ← construct-context lhs
A ← quoteTC A
t ← quoteTC t
A , t ← apply-to-metas A t
if not cong-with-lhs-and-rhs
then conclude unknown unknown f t
else do
A ← reduce A
_ , _ , lhs , rhs ← deconstruct-equality′ err₂ A
conclude lhs rhs f t
where
err₁ = strErr "⟨by⟩: ill-formed goal" ∷ []
err₂ = strErr "⟨by⟩: ill-formed proof" ∷ []
try : Term → TC ⊤
try t = do
debugPrint "by" 10 $
strErr "Term tried by ⟨by⟩:" ∷ termErr t ∷ []
unify t goal
conclude : Term → Term → Term → Term → TC Term
conclude lhs rhs f t = do
ctxt ← context
let t₁ = cong ctxt lhs rhs f t
t₂ = cong ctxt rhs lhs f (sym ctxt t)
catchTC (try t₁) (try t₂)
return t₁
mutual
context-term : ℕ → Term → StateT ℕ TC Term
context-term n = λ where
(def f args) → if eq-Name f (quote ⟨_⟩)
then modify suc >> return (var n [])
else def f ⟨$⟩ context-args n args
(var x args) → var (weaken-var n 1 x) ⟨$⟩
context-args n args
(con c args) → con c ⟨$⟩ context-args n args
(lam v t) → lam v ⟨$⟩ context-abs n t
(pi a b) → flip pi ⟨$⟩ context-abs n b ⊛ context-arg n a
(meta m _) → liftʳ $ blockOnMeta′ "construct-context" m
t → return (weaken-term n 1 t)
context-abs : ℕ → Abs Term → StateT ℕ TC (Abs Term)
context-abs n (abs s t) = abs s ⟨$⟩ context-term (suc n) t
context-arg : ℕ → Arg Term → StateT ℕ TC (Arg Term)
context-arg n (arg i t) = arg i ⟨$⟩ context-term n t
context-args :
ℕ → List (Arg Term) → StateT ℕ TC (List (Arg Term))
context-args n = λ where
[] → return []
(a ∷ as) → flip _∷_ ⟨$⟩ context-args n as ⊛ context-arg n a
construct-context : Term → TC Term
construct-context lhs = do
debugPrint "by" 20
(strErr "⟨by⟩ was given the left-hand side" ∷
termErr lhs ∷ [])
body , n ← run (context-term 0 lhs) 0
case n of λ where
(suc _) → return (lam visible (abs "x" body))
zero → typeError $
strErr "⟨by⟩: no occurrence of ⟨_⟩ found" ∷ []
macro
⟨by⟩ : ∀ {a} {A : Type a} → A → Term → TC ⊤
⟨by⟩ t goal = do
⟨by⟩-tactic t goal
return _
debug-⟨by⟩ : ∀ {a} {A : Type a} → A → Term → TC ⊤
debug-⟨by⟩ t goal = do
t ← ⟨by⟩-tactic t goal
typeError (strErr "Term found by ⟨by⟩:" ∷ termErr t ∷ [])
module By
(sym : Term → Term)
(equality : Term → Term → TC.Type)
(refl : Term → Term → Term → Term)
(make-cong : ℕ → TC Name)
(extra-check-in-try-refl : Bool)
where
private
by-tactic : ∀ {a} {A : Type a} → A → Term → TC Term
by-tactic {A} t goal = do
A ← quoteTC A
t ← quoteTC t
_ , t ← apply-to-metas A t
by-tactic′ fuel t goal
where
fuel : ℕ
fuel = 100
by-tactic′ : ℕ → Term → Term → TC Term
by-tactic′ zero _ _ = typeError
(strErr "by: no more fuel" ∷ [])
by-tactic′ (suc n) t goal = do
goal-type ← reduce =<< inferType goal
block-if-meta goal-type
catchTC (try-refl goal-type) $
catchTC (try t) $
catchTC (try (sym t)) $
try-cong goal-type
where
ill-formed : List ErrorPart
ill-formed = strErr "by: ill-formed goal" ∷ []
failure : {A : Type} → TC A
failure = typeError (strErr "by failed" ∷ [])
block-if-meta : TC.Type → TC ⊤
block-if-meta type = do
eq ← deconstruct-equality′ ill-formed type
case eq of λ where
(_ , _ , meta m _ , _) → blockOnMeta′
"block-if-meta (left)" m
(_ , _ , _ , meta m _) → blockOnMeta′
"block-if-meta (right)" m
_ → return _
try-refl : TC.Type → TC Term
try-refl type = do
a , A , lhs , _ ← deconstruct-equality′ ill-formed type
let t′ = refl a A lhs
unify t′ goal
if not extra-check-in-try-refl
then return t′
else do
goal ← reduce goal
case goal of λ where
(meta _ _) → failure
_ → return t′
try : Term → TC Term
try t = do
unify t goal
return t
try-cong : TC.Type → TC Term
try-cong type = do
_ , _ , y , z ← deconstruct-equality′ ill-formed type
head , ys , zs ← heads y z
args ← arguments ys zs
cong ← make-cong (length args)
let t = def cong (varg head ∷ args)
unify t goal
return t
where
heads : Term → Term →
TC (Term × List (Arg Term) × List (Arg Term))
heads = λ
{ (def y ys) (def z zs) → helper (primQNameEquality y z)
(def y) (def z) ys zs
; (con y ys) (con z zs) → helper (primQNameEquality y z)
(con y) (con z) ys zs
; (var y ys) (var z zs) → helper (y == z)
(var y) (var z) ys zs
; _ _ → failure
}
where
find-equal-arguments :
List (Arg Term) → List (Arg Term) →
List (Arg Term) × List (Arg Term) × List (Arg Term)
find-equal-arguments [] zs = [] , [] , zs
find-equal-arguments ys [] = [] , ys , []
find-equal-arguments (y ∷ ys) (z ∷ zs) with eq-Arg y z
... | false = [] , y ∷ ys , z ∷ zs
... | true with find-equal-arguments ys zs
... | (es , ys′ , zs′) = y ∷ es , ys′ , zs′
helper : B.Bool → _ → _ → _ → _ → _
helper B.false y z _ _ =
typeError (strErr "by: distinct heads:" ∷
termErr (y []) ∷ termErr (z []) ∷ [])
helper B.true y _ ys zs =
let es , ys′ , zs′ = find-equal-arguments ys zs in
return (y es , ys′ , zs′)
arguments : List (Arg Term) → List (Arg Term) →
TC (List (Arg Term))
arguments [] [] = return []
arguments (arg (arg-info visible _) y ∷ ys)
(arg (arg-info visible _) z ∷ zs) = do
goal ← checkType unknown (equality y z)
t ← by-tactic′ n t goal
args ← arguments ys zs
return (varg t ∷ args)
arguments (arg (arg-info hidden _) _ ∷ ys) zs = arguments ys zs
arguments (arg (arg-info instance′ _) _ ∷ ys) zs = arguments ys zs
arguments ys (arg (arg-info hidden _) _ ∷ zs) = arguments ys zs
arguments ys (arg (arg-info instance′ _) _ ∷ zs) = arguments ys zs
arguments _ _ = failure
macro
by : ∀ {a} {A : Type a} → A → Term → TC ⊤
by t goal = do
by-tactic t goal
return _
debug-by : ∀ {a} {A : Type a} → A → Term → TC ⊤
debug-by t goal = do
t ← by-tactic t goal
typeError (strErr "Term found by by:" ∷ termErr t ∷ [])
definition : ⊤
definition = _
module Tactics
(deconstruct-equality :
TC.Type → TC (Maybe (Term × TC.Type × Term × Term)))
(equality : Term → Term → TC.Type)
(refl : Term → Term → Term → Term)
(sym : Term → Term)
(cong : Term → Term → Term → Term → Term)
(cong-with-lhs-and-rhs : Bool)
(make-cong : ℕ → TC Name)
(extra-check-in-try-refl : Bool)
where
open ⟨By⟩ deconstruct-equality (return tt) (λ _ → sym) (λ _ → cong)
cong-with-lhs-and-rhs public
open By deconstruct-equality sym equality refl make-cong
extra-check-in-try-refl public