{-# OPTIONS -vtactic.hlevel:20 -vtc.def:10 #-}
open import 1Lab.Reflection.Record
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.Reflection
open import 1Lab.Type.Sigma
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type
open import Data.Bool
open import Data.List
open import Meta.Foldable
open import Prim.Data.Nat
module 1Lab.Reflection.HLevel where
data Arg-spec : Type where
`level-minus : (n : Nat) → Arg-spec
`search-under : (n : Nat) → Arg-spec
`meta : Arg-spec
pattern `search = `search-under 0
pattern `level = `level-minus 0
data hlevel-decomposition {ℓ} (T : Type ℓ) : Type where
decomp
: (h-level-lemma : Name) (arguments : List Arg-spec)
→ hlevel-decomposition T
record hlevel-projection (proj : Name) : Type where
field
has-level : Name
get-level : Term → TC Term
get-argument : List (Arg Term) → TC Term
open hlevel-projection
private
backtrack : ∀ {ℓ} {A : Type ℓ} → List ErrorPart → TC A
backtrack note = do
debugPrint "tactic.hlevel" 10 $ "Backtracking search... " ∷ note
typeError $ "Search hit a dead-end: " ∷ note
hlevel-types : List Name
hlevel-types = quote is-hlevel ∷ quote is-prop ∷ quote is-set ∷ []
pattern nat-lit n =
def (quote Number.fromNat) (_ ∷ _ ∷ _ ∷ lit (nat n) v∷ _)
decompose-is-hlevel′ : Term → TC (Term × Term)
decompose-is-hlevel : Term → TC (Term × Term)
decompose-is-hlevel goal = do
ty ← withReduceDefs (false , hlevel-types) $ inferType goal >>= reduce
decompose-is-hlevel′ ty
decompose-is-hlevel′ ty = do
def (quote is-hlevel) (_ ∷ ty v∷ lv v∷ []) ← pure ty
where
def (quote is-set) (_ ∷ ty v∷ []) → do
ty ← wait-just-a-bit ty
pure (ty , quoteTerm 2)
def (quote is-prop) (_ ∷ ty v∷ []) → do
ty ← wait-just-a-bit ty
pure (ty , quoteTerm 1)
def (quote is-contr) (_ ∷ ty v∷ []) → do
ty ← wait-just-a-bit ty
pure (ty , quoteTerm 0)
_ → backtrack "Goal type isn't is-hlevel"
ty ← wait-just-a-bit ty
lv ← wait-just-a-bit lv
pure (ty , lv)
lift-sol : Term → Term → Nat → Term
lift-sol tm _ 0 = tm
lift-sol tm l1 l = def (quote is-hlevel-+) (l1 v∷ lit (nat l) v∷ tm v∷ [])
pred-term : Term → Maybe Term
pred-term (con (quote suc) (x v∷ [])) = just x
pred-term (lit (nat n)) with n
... | suc k = just (lit (nat k))
... | _ = nothing
pred-term _ = nothing
{-# TERMINATING #-}
lifting-loop : Nat → Term → Term → Term → Term → TC ⊤
lifting-loop it solution goal l1 l2 =
let's-hope <|> do
(just l2′) ← pred-term <$> normalise l2 where
nothing → backtrack "Lifting loop reached its end with no success"
lifting-loop (suc it) solution goal l1 l2′
where
let's-hope : TC ⊤
let's-hope = do
debugPrint "tactic.hlevel" 30 $ "Lifting loop: Trying " ∷ termErr (lift-sol solution l1 it) ∷ " for level " ∷ termErr l2 ∷ []
unify goal (lift-sol solution l1 it)
treat-as-n-type : ∀ {n} → hlevel-projection n → Term → TC ⊤
treat-as-n-type projection goal = do
(ty , wanted-level) ← decompose-is-hlevel goal
debugPrint "tactic.hlevel" 10 $
"Attempting to treat as " ∷ termErr wanted-level ∷ "-Type: " ∷ termErr ty ∷ []
ty ← reduce ty
def namen args ← returnTC ty
where what → backtrack $ "Thing isn't an application, it is " ∷ termErr what ∷ []
it ← projection .get-argument args
actual-level ← inferType it >>= projection .get-level
debugPrint "tactic.hlevel" 10 $
"... but it's actually a(n) " ∷ termErr actual-level ∷ "-Type" ∷ []
lv ← normalise wanted-level
lv′ ← normalise actual-level
lifting-loop 0 (def (projection .has-level) (it v∷ [])) goal lv′ lv
commitTC
use-instance-search : Bool → Term → TC ⊤
use-instance-search has-alts goal = runSpeculative $ do
(ty , lv) ← decompose-is-hlevel goal
solved@(meta mv _) ←
new-meta (def (quote H-Level) (ty v∷ lv v∷ [])) where _ → backtrack []
instances ← getInstances mv
t ← quoteTC instances
debugPrint "tactic.hlevel" 10 $
"Using instance search for\n" ∷ termErr ty ∷
"\nFound candidates\n " ∷ termErr t ∷ []
let
go : List Term → TC (⊤ × Bool)
go = λ where
(x ∷ []) → do
unify solved x
withReduceDefs (false , quote hlevel ∷ []) $ withReconstructed true $
unify goal (def (quote hlevel) (lv v∷ []))
pure (tt , true)
[] → if has-alts
then backtrack "No possible instances, but have other decompositions to try"
else pure (tt , false)
_ → backtrack "Too many possible instances; will not use instance search for this goal"
go instances
search : Bool → Term → Nat → Term → TC ⊤
search has-alts _ zero goal = unify goal unknown
search has-alts level (suc n) goal =
use-projections
<|> use-hints
<|> use-instance-search has-alts goal
<|> typeError "Search failed!!"
where
open hlevel-projection
use-projections : TC ⊤
use-projections = do
def qn _ ← (fst <$> decompose-is-hlevel goal) >>= reduce
where _ → backtrack "Term is not headed by a definition; ignoring projections."
goalt ← inferType goal
debugPrint "tactic.hlevel" 20 $
"Will attempt to use projections for goal\n " ∷ termErr goalt ∷ []
(solved , instances) ← runSpeculative $ do
solved@(meta mv _) ← new-meta (def (quote hlevel-projection) (lit (name qn) v∷ []))
where _ → typeError (termErr goal ∷ [])
(x ∷ xs) ← getInstances mv
where [] → pure ((unknown , []) , false)
pure ((solved , x ∷ xs) , true)
nondet (eff List) instances λ a → do
projection ← unquoteTC {A = hlevel-projection qn} a
ty ← withReduceDefs (false , hlevel-types) (inferType goal >>= reduce)
debugPrint "tactic.hlevel" 20 $
"Outer type: " ∷ termErr ty ∷ []
treat-as-n-type projection goal >> unify solved a
remove-invisible : Term → Term → TC Term
remove-invisible
(lam _ (abs _ t))
(pi (arg (arginfo invisible _) _) (abs _ ret))
= remove-invisible t ret
remove-invisible inner _ = pure inner
wrap-lams : Nat → Term → Term
wrap-lams zero r = r
wrap-lams (suc x) r = lam visible $ abs "a" $ wrap-lams x r
extend-n : ∀ {ℓ} → Nat → TC ((A : Type ℓ) → TC A → TC A)
extend-n zero = pure λ _ x → x
extend-n (suc n) = do
rest ← extend-n n
lift mv ← rest (Lift _ Term) $ lift <$> new-meta unknown
let domain = arg (arginfo visible (modality relevant quantity-ω)) mv
pure λ a k → rest a $ extendContext "a" domain $ k
gen-args
: Bool
→ Term
→ Name
→ List Arg-spec
→ List (Arg Term)
→ TC ⊤
→ TC ⊤
gen-args has-alts level defn [] accum cont = do
unify goal (def defn (reverse accum))
debugPrint "tactic.hlevel" 10 $
"Committed to solution: " ∷ termErr (def defn (reverse accum)) ∷ []
cont
gen-args has-alts level defn (x ∷ args) accum cont with x
... | `level-minus 0 = gen-args has-alts level defn args (level v∷ accum) cont
... | `level-minus n@(suc _) =
do
level ← normalise level
debugPrint "tactic.hlevel" 10 $
"Hint demands offset, performing symbolic monus, subtracting from\n " ∷ termErr level ∷ []
level′′ ← monus level n
gen-args has-alts level defn args (level′′ v∷ accum) cont
where
monus : Term → Nat → TC Term
monus (lit (nat n)) k = pure $ lit (nat (n - k))
monus tm zero = pure tm
monus thezero@(con (quote zero) []) (suc it) = pure thezero
monus (con (quote suc) (x v∷ [])) (suc it) = do
x ← reduce x
monus x it
monus tm (suc it) = do
debugPrint "tactic.hlevel" 10 $ "Dunno how to take 1 from " ∷ termErr tm ∷ []
typeError []
... | `meta = gen-args has-alts level defn args (unknown v∷ accum) cont
... | `search-under under = do
debugPrint "tactic.hlevel" 10 $ "Going under " ∷ termErr (lit (nat under)) ∷ []
gounder ← extend-n under
mv ← gounder Term $ do
debugPrint "tactic.hlevel" 10 $ "In extended context"
new-meta unknown
debugPrint "tactic.hlevel" 10 $ "Metavariable: " ∷ termErr (wrap-lams under mv) ∷ []
gen-args has-alts level defn args (wrap-lams under mv v∷ accum) $ do
cont
gounder ⊤ $ search has-alts unknown n mv
use-decomp-hints : (Term × Term) → Term → List Term → TC (⊤ × Bool)
use-decomp-hints (goal-ty , lv) solved (c1 ∷ cs) = do
ty ← inferType c1
c1′ ← reduce c1
(remove-invisible c1′ ty >>= λ where
(con (quote decomp) (_ ∷ _ ∷ nm v∷ argspec v∷ [])) → do
debugPrint "tactic.hlevel" 10 $
"Using " ∷ termErr nm ∷ " decomposition for:\n "
∷ termErr (def (quote is-hlevel) (goal-ty v∷ lv v∷ [])) ∷ []
nm′ ← unquoteTC nm
argsp ← unquoteTC argspec
gen-args (not (length cs == 0)) lv nm′ argsp [] (returnTC tt)
unify solved c1
pure (tt , true)
_ → backtrack "Non-canonical hint")
<|> use-decomp-hints (goal-ty , lv) solved cs
use-decomp-hints (goal-ty , _) _ [] =
backtrack $ "Ran out of decomposition hints for " ∷ termErr goal-ty ∷ []
use-hints : TC ⊤
use-hints = runSpeculative $ do
(ty , lv) ← decompose-is-hlevel goal
pure ty >>= λ where
(meta m _) → do
debugPrint "tactic.hlevel" 10
"Type under is-hlevel is metavariable, blocking to avoid infinite loop"
blockOnMeta m
_ → pure tt
solved@(meta mv _) ← new-meta (def (quote hlevel-decomposition) (ty v∷ []))
where _ → typeError (termErr ty ∷ [])
instances ← getInstances mv
t ← quoteTC instances
debugPrint "tactic.hlevel" 10 $
"Finding decompositions for\n" ∷
termErr ty ∷
"\nFound candidates\n " ∷
termErr t ∷ []
use-decomp-hints (ty , lv) solved instances
decompose-is-hlevel-top
: ∀ {ℓ} {A : Type ℓ}
→ Term → TC (Term × Term × (TC A → TC A) × (Term → Term))
decompose-is-hlevel-top goal =
do
ty ← withReduceDefs (false , hlevel-types) $
(inferType goal >>= reduce) >>= wait-just-a-bit
go ty
where
go : Term → TC _
go (pi (arg as at) (abs vn cd)) = do
(inner , hlevel , enter , leave) ← go cd
pure $ inner , hlevel , extendContext vn (arg as at) , λ t → lam (ArgInfo.arg-vis as) (abs vn t)
go tm = do
(inner , hlevel) ← decompose-is-hlevel′ tm
pure $ inner , hlevel , (λ x → x) , (λ x → x)
hlevel-tactic-worker : Term → TC ⊤
hlevel-tactic-worker goal = do
ty ← withReduceDefs (false , hlevel-types) $ inferType goal >>= reduce
(ty , lv , enter , leave) ← decompose-is-hlevel-top goal <|>
typeError
( "hlevel tactic: goal type is not of the form ``is-hlevel A n'':\n"
∷ termErr ty
∷ [])
solved ← enter $ do
goal′ ← new-meta (def (quote is-hlevel) (ty v∷ lv v∷ []))
search false lv 10 goal′
pure goal′
unify goal (leave solved)
macro hlevel! = hlevel-tactic-worker
el! : ∀ {ℓ} (A : Type ℓ) {n} {@(tactic hlevel-tactic-worker) hl : is-hlevel A n} → n-Type ℓ n
∣ el! A {hl = hl} ∣ = A
el! A {hl = hl} .is-tr = hl
prop-ext!
: ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′}
{@(tactic hlevel-tactic-worker) aprop : is-hlevel A 1}
{@(tactic hlevel-tactic-worker) bprop : is-hlevel B 1}
→ (A → B) → (B → A)
→ A ≃ B
prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop
Σ-prop-path!
: ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′}
→ {@(tactic hlevel-tactic-worker) bxprop : ∀ x → is-hlevel (B x) 1}
→ {x y : Σ A B}
→ x .fst ≡ y .fst
→ x ≡ y
Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop
prop!
: ∀ {ℓ} {A : I → Type ℓ} {@(tactic hlevel-tactic-worker) aip : is-hlevel (A i0) 1}
→ {x : A i0} {y : A i1}
→ PathP (λ i → A i) x y
prop! {A = A} {aip = aip} {x} {y} =
is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i aip) x y
open hlevel-projection
instance
decomp-lift : ∀ {ℓ ℓ′} {T : Type ℓ} → hlevel-decomposition (Lift ℓ′ T)
decomp-lift = decomp (quote Lift-is-hlevel) (`level ∷ `search ∷ [])
decomp-pi³
: ∀ {ℓa ℓb ℓc ℓd} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc}
→ {D : ∀ x y (z : C x y) → Type ℓd}
→ hlevel-decomposition (∀ a b c → D a b c)
decomp-pi³ = decomp (quote Π-is-hlevel³) (`level ∷ `search-under 3 ∷ [])
decomp-pi²
: ∀ {ℓa ℓb ℓc} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc}
→ hlevel-decomposition (∀ a b → C a b)
decomp-pi² = decomp (quote Π-is-hlevel²) (`level ∷ `search-under 2 ∷ [])
decomp-pi : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} → hlevel-decomposition (∀ a → B a)
decomp-pi = decomp (quote Π-is-hlevel) (`level ∷ `search-under 1 ∷ [])
decomp-impl-pi : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} → hlevel-decomposition (∀ {a} → B a)
decomp-impl-pi = decomp (quote Π-is-hlevel′) (`level ∷ `search-under 1 ∷ [])
decomp-sigma : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} → hlevel-decomposition (Σ A B)
decomp-sigma = decomp (quote Σ-is-hlevel) (`level ∷ `search ∷ `search-under 1 ∷ [])
decomp-path′ : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b)
decomp-path′ = decomp (quote Path-is-hlevel') (`level ∷ `search ∷ `meta ∷ `meta ∷ [])
decomp-path : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b)
decomp-path = decomp (quote Path-is-hlevel) (`level ∷ `search ∷ [])
decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B)
decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] )
decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A)
decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ [])
decomp-ntype : ∀ {ℓ} {n} → hlevel-decomposition (n-Type ℓ n)
decomp-ntype = decomp (quote n-Type-is-hlevel) (`level-minus 1 ∷ [])
hlevel-proj-n-type : hlevel-projection (quote n-Type.∣_∣)
hlevel-proj-n-type .has-level = quote n-Type.is-tr
hlevel-proj-n-type .get-level ty = do
def (quote n-Type) (ell v∷ lv′t v∷ []) ← reduce ty
where _ → backtrack $ "Type of thing isn't n-Type, it is " ∷ termErr ty ∷ []
normalise lv′t
hlevel-proj-n-type .get-argument (_ ∷ _ ∷ it v∷ []) = pure it
hlevel-proj-n-type .get-argument _ = typeError []
private
module _ {ℓ} {A : n-Type ℓ 2} {B : ∣ A ∣ → n-Type ℓ 3} where
_ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 5
_ = hlevel!
_ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 3
_ = hlevel!
_ : is-hlevel ∣ A ∣ 2
_ = hlevel!
_ : ∀ n → is-hlevel (n-Type ℓ n) (suc n)
_ = hlevel!
_ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ (2 + n)
_ = λ n x → hlevel!