diff options
Diffstat (limited to 'src/CBPV/Family.agda')
| -rw-r--r-- | src/CBPV/Family.agda | 594 |
1 files changed, 314 insertions, 280 deletions
diff --git a/src/CBPV/Family.agda b/src/CBPV/Family.agda index 4a64726..dd01777 100644 --- a/src/CBPV/Family.agda +++ b/src/CBPV/Family.agda @@ -1,362 +1,396 @@ module CBPV.Family where -open import Data.List as List using (List; []; _∷_; map) +open import Data.List as List using (List; []; _∷_; foldr) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.Sum as ⊎ using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Unit using (⊤) -open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_return_of_) +open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_returning_of_) open import Reflection hiding (name; Name; _≟_) -open import Reflection.Argument using (_⟨∷⟩_) -open import Reflection.Term as Term using (_⋯⟅∷⟆_) -open import Relation.Binary.PropositionalEquality +open import Reflection.AST.Argument using (_⟨∷⟩_; _⟅∷⟆_) +open import Reflection.AST.Term as Term using (_⋯⟅∷⟆_) +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning) open import Relation.Nullary using (yes; no) -open import CBPV.Context +import Data.Sum.Properties as ⊎ + +open import CBPV.Context hiding (foldr) open import CBPV.Type -- Families and Morphisms ----------------------------------------------------- -infix 4 _⇾_ _⇾ᵛ_ _⇾ᶜ_ +infix 4 _⇾_ _⇾ᵗ_ + +_-Family : Set → Set₁ +A -Family = GenContext A → Set + +_-Sorted-_-Family : Set → Set → Set₁ +A -Sorted- B -Family = A → B -Family -Family : Set₁ -Family = Context → Set +_-SortedFamily : Set → Set₁ +A -SortedFamily = A -Sorted- A -Family ValFamily : Set₁ -ValFamily = ValType → Family +ValFamily = ValType -SortedFamily CompFamily : Set₁ -CompFamily = CompType → Family +CompFamily = CompType -Sorted- ValType -Family -_⇾_ : Family → Family → Set -X ⇾ Y = {Γ : Context} → X Γ → Y Γ +_⇾_ : {A : Set} → A -Family → A -Family → Set +X ⇾ Y = {Γ : _} → X Γ → Y Γ -_⇾ᵛ_ : ValFamily → ValFamily → Set -V ⇾ᵛ W = {A : ValType} → V A ⇾ W A - -_⇾ᶜ_ : CompFamily → CompFamily → Set -C ⇾ᶜ D = {B : CompType} → C B ⇾ D B +_⇾ᵗ_ : {A B : Set} → A -Sorted- B -Family → A -Sorted- B -Family → Set +V ⇾ᵗ W = {τ : _} → V τ ⇾ W τ -- Variables ------------------------------------------------------------------- private variable - Γ Δ Θ Π : Context - A A′ : ValType x y : Name - V W X : ValFamily + A B C : Set + Γ Δ Θ Π : GenContext A + τ τ′ : A + X Y : A -Sorted- B -Family -data VarPos (x : Name) (A : ValType) : Context → Set where - Here : VarPos x A (Γ :< (x :- A)) - There : VarPos x A Γ → VarPos x A (Γ :< (y :- A′)) +data VarPos (x : Name) (τ : A) : GenContext A → Set where + Here : VarPos x τ (Γ :< (x :- τ)) + There : VarPos x τ Γ → VarPos x τ (Γ :< (y :- τ′)) -weaklPos : (Δ : Context) → VarPos x A Γ → VarPos x A (Γ ++ Δ) -weaklPos [<] i = i -weaklPos (Δ :< (x :- A)) i = There (weaklPos Δ i) +record Var (τ : A) (Γ : GenContext A) : Set where + constructor MkVar + field + name : Name + pos : VarPos name τ Γ --- Reflection +open Var public -wknTerm : Term → Term -wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ [] +toVar : VarPos x τ Γ → Var τ Γ +toVar pos = MkVar _ pos -weaklTerm : Term → Term → Term -weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ [] +-- Substitutions -------------------------------------------------------------- -searchCtx : - (wkn : Term → Term) → - (hole : Term) → - (name : Term) → - (Γ : Term) → - TC ⊤ -searchCtx wkn hole name (meta m _) = blockOnMeta m -searchCtx wkn hole name (con (quote [<]) []) = - typeError (termErr name ∷ strErr " not in context." ∷ []) -searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (meta x _ ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) = - blockOnMeta x -searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) = - catchTC - (do - debugPrint "squid" 10 (strErr "checking name " ∷ termErr x ∷ strErr "..." ∷ []) - unify name x - let soln = wkn (quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ []) - debugPrint "squid" 10 (strErr "testing solution " ∷ termErr soln ∷ strErr "..." ∷ []) - unify soln hole - debugPrint "squid" 10 (strErr "success!" ∷ [])) - (searchCtx (wkn ∘ wknTerm) hole name Γ) -searchCtx wkn hole name (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) = - catchTC - (searchCtx wkn hole name Δ) - (searchCtx (wkn ∘ weaklTerm Δ) hole name Γ) -searchCtx wkn hole name Γ = - typeError (termErr name ∷ strErr " not in context " ∷ termErr Γ ∷ []) --- searchCtx (con (quote [<]) []) y = return [] --- searchCtx (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) y = --- -- with x Term.≟ y --- -- ... | yes _ = --- do --- let head = quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ [] --- tail ← searchCtx Γ y --- return (head ∷ map wknTerm tail) --- -- ... | no _ = --- -- do --- -- tail ← searchCtx Γ y --- -- return (map wknTerm tail) --- searchCtx (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) y = --- do --- right ← searchCtx Δ y --- left ← searchCtx Γ y --- return (right List.++ map (weaklTerm Δ) left) - --- searchCtx (meta m _) y = blockOnMeta m --- searchCtx Γ y = --- do --- debugPrint "squid" 10 (strErr "stuck matching term " ∷ termErr Γ ∷ []) --- return [] - --- tryEach : List Term → Term → TC ⊤ --- tryEach [] hole = typeError (strErr "not in context" ∷ []) --- tryEach (t ∷ []) hole = --- do --- debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ []) --- unify t hole --- debugPrint "squid" 10 (strErr "success!" ∷ []) --- tryEach (t ∷ ts@(_ ∷ _)) hole = --- do --- debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ []) --- catchTC --- (do --- unify t hole --- debugPrint "squid" 10 (strErr "success!" ∷ [])) --- (tryEach ts hole) - -searchVarPos : Context → Name → Term → TC ⊤ -searchVarPos Γ x hole = - do - Γ ← quoteTC Γ - x ← quoteTC x - case x return (λ _ → TC ⊤) of λ - { (meta x _) → blockOnMeta x - ; _ → return _ - } - debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) - debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) - searchCtx (λ t → t) hole x Γ +infixl 9 _⨾_ [_]_⨾_ _⨾′_ _≈⨾_ _≈⨾′_ _⨾≈_ +infixl 4 copair _∥ˡ_ _∥ʳ_ +infixl 5 _:<_↦_ subst-step +infix 4 _~[_]↝_ _↝_ [_]_≈_ _≈_ --- searchVarPos : Context → Name → Term → TC ⊤ --- searchVarPos Γ x hole = --- do --- Γ ← quoteTC Γ --- (case Γ return (λ _ → TC ⊤) of λ --- { (meta m _) → blockOnMeta m --- ; _ → return _ --- }) --- x ← quoteTC x --- debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) --- debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) --- guesses ← searchCtx Γ x --- tryEach guesses hole - --- Back to business as normal - -record Var (A : ValType) (Γ : Context) : Set where - constructor %%_ +record _~[_]↝_ (Γ : GenContext A) (X : A -Sorted- B -Family) (Δ : GenContext B) : Set where + constructor tabulate + infixr 8 _＠_ field - name : Name - @(tactic searchVarPos Γ name) {pos} : VarPos name A Γ + _＠_ : Var τ Γ → X τ Δ -open Var public +open _~[_]↝_ public -toVar : VarPos x A Γ → Var A Γ -toVar pos = (%% _) {pos} +_↝_ : GenContext A → GenContext A → Set +Γ ↝ Δ = Γ ~[ Var ]↝ Δ -ThereVar : Var A Γ → Var A (Γ :< (y :- A′)) -ThereVar i = toVar $ There (i .pos) +[_]_＠_ : (X : A -Sorted- B -Family) → Γ ~[ X ]↝ Δ → Var τ Γ → X τ Δ +[ X ] σ ＠ i = σ ＠ i --- Substitutions -------------------------------------------------------------- +-- Equality -infixl 9 _⨾_ [_]_⨾_ -infixr 8 _＠_ -infixl 5 _:<_↦_ -infix 4 Subst _↝_ +record _≈_ (σ ς : Γ ~[ X ]↝ Δ) : Set where + constructor tabulate≈ + infixr 8 _＠_ + field + _＠_ : (i : Var τ Γ) → σ ＠ i ≡ ς ＠ i -data Subst (V : ValFamily) (Δ : Context) : Context → Set where - [<] : Subst V Δ [<] - _:<_↦_ : Subst V Δ Γ → (x : Name) → V A Δ → Subst V Δ (Γ :< (x :- A)) +open _≈_ public -syntax Subst V Δ Γ = Γ ~[ V ]↝ Δ +[_]_≈_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → Γ ~[ X ]↝ Δ → Set +[ V ] σ ≈ ς = σ ≈ ς -_↝_ : Context → Context → Set -Γ ↝ Δ = Γ ~[ Var ]↝ Δ +trans≈ : {σ₁ σ₂ σ₃ : Γ ~[ X ]↝ Δ} → σ₁ ≈ σ₂ → σ₂ ≈ σ₃ → σ₁ ≈ σ₃ +trans≈ σ₁≈σ₂ σ₂≈σ₃ ＠ i = trans (σ₁≈σ₂ ＠ i) (σ₂≈σ₃ ＠ i) + +-- Combinators + +_⨾_ : Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ +(σ ⨾ f) ＠ i = f (σ ＠ i) -_⨾_ : Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ -[<] ⨾ f = [<] -(σ :< x ↦ v) ⨾ f = (σ ⨾ f) :< x ↦ f v +_⨾′_ : Γ ↝ Δ → Δ ~[ X ]↝ Θ → Γ ~[ X ]↝ Θ +(ρ ⨾′ f) ＠ i = f ＠ (ρ ＠ i) -[_]_⨾_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ +[_]_⨾_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ [ V ] σ ⨾ f = σ ⨾ f -tabulate : (∀ {A} → Var A Γ → V A Δ) → Γ ~[ V ]↝ Δ -tabulate {Γ = [<]} f = [<] -tabulate {Γ = Γ :< (x :- A)} f = tabulate (f ∘ ThereVar) :< x ↦ f (toVar Here) +_≈⨾_ : {σ ς : Γ ~[ X ]↝ Δ} → σ ≈ ς → (f : ∀ {τ} → X τ Δ → Y τ Θ) → [ Y ] (σ ⨾ f) ≈ (ς ⨾ f) +(σ≈ς ≈⨾ f) ＠ i = cong f (σ≈ς ＠ i) -lookup : Γ ~[ V ]↝ Δ → VarPos x A Γ → V A Δ -lookup (σ :< x ↦ v) Here = v -lookup (σ :< x ↦ v) (There i) = lookup σ i +_≈⨾′_ : {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → (σ : Δ ~[ X ]↝ Θ) → ρ ⨾′ σ ≈ ϱ ⨾′ σ +(ρ≈ϱ ≈⨾′ σ) ＠ i = cong (σ ＠_) (ρ≈ϱ ＠ i) -_＠_ : Γ ~[ V ]↝ Δ → Var A Γ → V A Δ -σ ＠ i = lookup σ (i .pos) +_⨾≈_ : (ρ : Γ ↝ Δ) → {σ ς : Δ ~[ X ]↝ Θ} → σ ≈ ς → ρ ⨾′ σ ≈ ρ ⨾′ ς +(ρ ⨾≈ σ≈ς) ＠ i = σ≈ς ＠ ρ ＠ i -[_]_＠_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → Var A Γ → V A Δ -[ V ] σ ＠ i = σ ＠ i +-- Particular Substitutions + +-- id id : Γ ↝ Γ id = tabulate (λ x → x) -weakrPos : VarPos x A Δ → VarPos x A (Γ ++ Δ) +-- empty + +empty : [<] ~[ X ]↝ Γ +empty = tabulate (λ ()) + +-- weakr + +weakrPos : VarPos x τ Δ → VarPos x τ (Γ ++ Δ) weakrPos Here = Here weakrPos (There i) = There (weakrPos i) -weakrF : Var A Δ → Var A (Γ ++ Δ) +weakrF : Var τ Δ → Var τ (Γ ++ Δ) weakrF i = toVar $ weakrPos $ i .pos weakr : Δ ↝ Γ ++ Δ weakr = tabulate weakrF -weaklF : (Δ : Context) → Var A Γ → Var A (Γ ++ Δ) +-- weakl + +weaklPos : (Δ : GenContext A) → VarPos x τ Γ → VarPos x τ (Γ ++ Δ) +weaklPos [<] i = i +weaklPos (Δ :< (x :- τ)) i = There (weaklPos Δ i) + +weaklF : (Δ : GenContext A) → Var τ Γ → Var τ (Γ ++ Δ) weaklF Δ i = toVar $ weaklPos Δ $ i .pos -weakl : (Δ : Context) → Γ ↝ Γ ++ Δ +weakl : (Δ : GenContext A) → Γ ↝ Γ ++ Δ weakl Δ = tabulate (weaklF Δ) -copair : Γ ~[ V ]↝ Θ → Δ ~[ V ]↝ Θ → Γ ++ Δ ~[ V ]↝ Θ -copair σ [<] = σ -copair σ (ς :< x ↦ v) = copair σ ς :< x ↦ v +-- copair + +splitPos : (Δ : GenContext A) → VarPos x τ (Γ ++ Δ) → VarPos x τ Γ ⊎ VarPos x τ Δ +splitPos [<] i = inj₁ i +splitPos (Δ :< _) Here = inj₂ Here +splitPos (Δ :< _) (There i) = ⊎.map₂ There (splitPos Δ i) + +splitF : (Δ : GenContext A) → Var τ (Γ ++ Δ) → Var τ Γ ⊎ Var τ Δ +splitF Δ i = ⊎.map toVar toVar $ splitPos Δ $ i .pos + +copair : Γ ~[ X ]↝ Θ → Δ ~[ X ]↝ Θ → Γ ++ Δ ~[ X ]↝ Θ +copair σ ς ＠ i = [ σ ＠_ , ς ＠_ ] $ splitF _ i + +syntax copair σ ς = σ ∥ ς + +copairₙ : {Γs : List (GenContext A)} → All (_~[ X ]↝ Θ) Γs → foldr _++_ [<] Γs ~[ X ]↝ Θ +copairₙ [] ＠ () +copairₙ (σ ∷ σs) = σ ∥ copairₙ σs -pull : (Δ Θ : Context) → Γ ++ Δ ++ Θ ↝ Γ ++ Θ ++ Δ -pull Δ Θ = - copair {Δ = Θ} - (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) - (weakr ⨾ (weakl Δ ＠_)) +-- singleton + +singleton : (x : Name) → X τ Γ → [< x :- τ ] ~[ X ]↝ Γ +singleton x v ＠ (MkVar .x Here) = v + +-- snoc + +_:<_↦_ : Γ ~[ X ]↝ Δ → (x : Name) → X τ Δ → Γ :< (x :- τ) ~[ X ]↝ Δ +σ :< x ↦ v = σ ∥ singleton x v + +-- weakening + +data Path {A : Set} : GenContext A → GenContext A → Set where + ⌞_⌟ : (Γ : GenContext A) → Path Γ Γ + _∥ˡ_ : Path Γ Δ → (Θ : GenContext A) → Path Γ (Δ ++ Θ) + _∥ʳ_ : (Θ : GenContext A) → Path Γ Δ → Path Γ (Θ ++ Δ) + +wkn : Path Γ Δ → Γ ↝ Δ +wkn ⌞ Γ ⌟ = id +wkn (path ∥ˡ Θ) = wkn path ⨾′ weakl Θ +wkn (Θ ∥ʳ path) = wkn path ⨾′ weakr + +-- lift + +lift′ : (Θ : GenContext A) → Γ ↝ Δ → Γ ++ Θ ↝ Δ ++ Θ +lift′ Θ ρ = ρ ⨾ weaklF Θ ∥ weakr + +-- weakening variables + +_↑_ : Var τ Γ → (Δ : GenContext A) → Var τ (Γ ++ Δ) +i ↑ Δ = weakl Δ ＠ i + +_↑[_] : Var τ Γ → (x : Name) → Var τ (Γ :< (x :- τ′)) +i ↑[ x ] = i ↑ [< x :- _ ] + +_↑ : Var τ Γ → Var τ (Γ :< (x :- τ′)) +i ↑ = i ↑[ _ ] + +-- interaction with map + +map⁺Pos : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → VarPos x τ (map f Γ) → X τ Δ +map⁺Pos {Γ = Γ :< (x :- τ)} σ Here = σ ＠ toVar Here +map⁺Pos {Γ = Γ :< (x :- τ)} {X = X} σ (There i) = map⁺Pos {X = X} (tabulate (λ i → σ ＠ (i ↑))) i + +map⁺ : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → map f Γ ~[ X ]↝ Δ +map⁺ σ ＠ i = map⁺Pos σ (i .pos) + +varPosMap⁺ : {f : A → B} → VarPos x τ Γ → VarPos x (f τ) (map f Γ) +varPosMap⁺ Here = Here +varPosMap⁺ (There i) = There (varPosMap⁺ i) + +varMap⁺ : {f : A → B} → Var τ Γ → Var (f τ) (map f Γ) +varMap⁺ v = toVar (varPosMap⁺ $ v .pos) + +map⁻ : {f : A → B} → map f Γ ~[ X ]↝ Δ → Γ ~[ X ∘ f ]↝ Δ +map⁻ σ ＠ i = σ ＠ varMap⁺ i -- Properties -subst-ext : (σ ς : Γ ~[ V ]↝ Δ) → (∀ {A} → (i : Var A Γ) → σ ＠ i ≡ ς ＠ i) → σ ≡ ς -subst-ext [<] [<] ext = refl -subst-ext (σ :< x ↦ v) (ς :< .x ↦ w) ext = - cong₂ (_:< x ↦_) (subst-ext σ ς $ λ i → ext $ ThereVar i) (ext $ %% x) - -⨾-assoc : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (g : ∀ {A} → W A Θ → X A Π) → - _⨾_ {V = W} {W = X} (σ ⨾ f) g ≡ σ ⨾ (g ∘ f) -⨾-assoc [<] f g = refl -⨾-assoc (σ :< x ↦ v) f g = cong (_:< x ↦ g (f v)) (⨾-assoc σ f g) - -⨾-cong : - (σ : Γ ~[ V ]↝ Δ) {f g : ∀ {A} → V A Δ → W A Θ} → - (∀ {A} → (v : V A Δ) → f v ≡ g v) → - _⨾_ {W = W} σ f ≡ σ ⨾ g -⨾-cong [<] ext = refl -⨾-cong (σ :< x ↦ v) ext = cong₂ (_:< x ↦_) (⨾-cong σ ext) (ext v) - -lookup-⨾ : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : VarPos x A Γ) → - lookup {V = W} (σ ⨾ f) i ≡ f (lookup σ i) -lookup-⨾ (σ :< x ↦ v) f Here = refl -lookup-⨾ (σ :< x ↦ v) f (There i) = lookup-⨾ σ f i - -lookup-tabulate : - (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : VarPos x A Γ) → - lookup {V = V} (tabulate f) i ≡ f (toVar i) -lookup-tabulate V f Here = refl -lookup-tabulate V f (There i) = lookup-tabulate V (f ∘ ThereVar) i - -＠-⨾ : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : Var A Γ) → - _＠_ {V = W} (σ ⨾ f) i ≡ f (σ ＠ i) -＠-⨾ σ f i = lookup-⨾ σ f (i .pos) - -＠-tabulate : - (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : Var A Γ) → - _＠_ {V = V} (tabulate f) i ≡ f i -＠-tabulate V f i = lookup-tabulate V f (i .pos) - -tabulate-cong : - (V : ValFamily) → - {f g : ∀ {A} → Var A Γ → V A Δ} → - (∀ {A} → (v : Var A Γ) → f v ≡ g v) → - tabulate {V = V} f ≡ tabulate g -tabulate-cong {Γ = [<]} V ext = refl -tabulate-cong {Γ = Γ :< (x :- A)} V ext = - cong₂ (_:< x ↦_) (tabulate-cong V (ext ∘ ThereVar)) (ext $ %% x) - -tabulate-⨾ : - (f : ∀ {A} → Var A Γ → V A Δ) (g : ∀ {A} → V A Δ → W A Θ) → - tabulate {V = V} f ⨾ g ≡ tabulate {V = W} (g ∘ f) -tabulate-⨾ {Γ = [<]} f g = refl -tabulate-⨾ {Γ = Γ :< (x :- A)} f g = cong (_:< x ↦ g (f $ toVar Here)) (tabulate-⨾ (f ∘ ThereVar) g) - -tabulate-＠ : (σ : Γ ~[ V ]↝ Δ) → tabulate (σ ＠_) ≡ σ -tabulate-＠ [<] = refl -tabulate-＠ (σ :< x ↦ v) = cong (_:< x ↦ v) (tabulate-＠ σ) - -copair-⨾ : - (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (f : ∀ {A} → V A Θ → W A Π) → - copair {V = W} (σ ⨾ f) (ς ⨾ f) ≡ copair {V = V} σ ς ⨾ f -copair-⨾ σ [<] f = refl -copair-⨾ σ (ς :< x ↦ v) f = cong (_:< x ↦ f v) (copair-⨾ σ ς f) - -copair-left : - (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (i : VarPos x A Γ) → - lookup (copair σ ς) (weaklPos Δ i) ≡ lookup σ i -copair-left σ [<] i = refl -copair-left σ (ς :< x ↦ v) i = copair-left σ ς i - -pull-left : - (Δ Θ : Context) (i : VarPos x A Γ) → - lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i) ≡ toVar (weaklPos Δ $ weaklPos Θ i) -pull-left {Γ = Γ} Δ Θ i = - begin - lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i) - ≡⟨ copair-left (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weakr {Γ = Γ} ⨾ (weakl Δ ＠_)) (weaklPos Δ i) ⟩ - lookup (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weaklPos Δ i) - ≡⟨ copair-left {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr i ⟩ - lookup (weakl Θ ⨾ (weakl Δ ＠_)) i - ≡⟨ lookup-⨾ (weakl Θ) (weakl Δ ＠_) i ⟩ - weakl Δ ＠ lookup (weakl Θ) i - ≡⟨ cong (weakl Δ ＠_) (lookup-tabulate Var (weaklF Θ) i) ⟩ - lookup (weakl Δ) (weaklPos Θ i) - ≡⟨ lookup-tabulate Var (weaklF Δ) (weaklPos Θ i) ⟩ - toVar (weaklPos Δ $ weaklPos Θ i) - ∎ +subst-step : + {x : Name} {σ ς : Γ :< (x :- τ) ~[ X ]↝ Δ} → + weakl [< x :- τ ] ⨾′ σ ≈ weakl [< x :- τ ] ⨾′ ς → + σ ＠ MkVar x Here ≡ ς ＠ MkVar x Here → + σ ≈ ς +subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x Here = σ₀≡ς₀ +subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x (There pos) = σ↑≈ς↑ ＠ MkVar x pos + +syntax subst-step {x = x} σ≈ς v≡w = σ≈ς :< x ⇒ v≡w + +-- weakl [<] is id + +weakl[<]≈id : weakl {Γ = Γ} [<] ≈ id +weakl[<]≈id = tabulate≈ (λ i → refl) + +-- copair is coslice coproduct + +splitPos-weaklPos : (Δ : GenContext A) → (i : VarPos x τ Γ) → splitPos Δ (weaklPos Δ i) ≡ inj₁ i +splitPos-weaklPos [<] i = refl +splitPos-weaklPos (Δ :< _) i = cong (⊎.map₂ There) (splitPos-weaklPos Δ i) + +splitF-weaklF : (Δ : GenContext A) (i : Var τ Γ) → splitF Δ (weaklF Δ i) ≡ inj₁ i +splitF-weaklF Δ i = cong (⊎.map toVar toVar) (splitPos-weaklPos Δ $ i .pos) + +copair-weakl : + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) → + [ X ] weakl Δ ⨾′ (σ ∥ ς) ≈ σ +copair-weakl σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weaklF _ i) + +splitPos-weakrPos : + (Γ : GenContext A) → (i : VarPos x τ Δ) → + splitPos {Γ = Γ} Δ (weakrPos i) ≡ inj₂ i +splitPos-weakrPos Γ Here = refl +splitPos-weakrPos Γ (There i) = cong (⊎.map₂ There) (splitPos-weakrPos Γ i) + +splitF-weakrF : (Γ : GenContext A) (i : Var τ Δ) → splitF Δ (weakrF i) ≡ inj₂ i +splitF-weakrF Γ i = cong (⊎.map toVar toVar) (splitPos-weakrPos Γ $ i .pos) + +copair-weakr : + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) → + [ X ] weakr {Γ = Γ} ⨾′ (σ ∥ ς) ≈ ς +copair-weakr σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weakrF _ i) + +weakPos-splitPos : + (Δ : GenContext A) (i : VarPos x τ (Γ ++ Δ)) → + [ weaklPos Δ , weakrPos ] (splitPos Δ i) ≡ i +weakPos-splitPos [<] i = refl +weakPos-splitPos (Δ :< _) Here = refl +weakPos-splitPos (Δ :< _) (There i) = begin + [ There ∘ weaklPos Δ , weakrPos ]′ (⊎.map₂ There $ splitPos Δ i) ≡⟨ ⊎.[,]-map (splitPos Δ i) ⟩ + [ There ∘ weaklPos Δ , weakrPos ∘ There ]′ (splitPos Δ i) ≡⟨⟩ + [ There ∘ weaklPos Δ , There ∘ weakrPos ]′ (splitPos Δ i) ≡˘⟨ ⊎.[,]-∘ There (splitPos Δ i) ⟩ + There ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ i) ≡⟨ cong There (weakPos-splitPos Δ i) ⟩ + There i ∎ + where open ≡-Reasoning + +weakF-splitF : (Δ : GenContext A) (i : Var τ (Γ ++ Δ)) → [ weaklF Δ , weakrF ] (splitF Δ i) ≡ i +weakF-splitF Δ i = begin + [ weaklF Δ , weakrF ] (splitF Δ i) ≡⟨ ⊎.[,]-map (splitPos Δ $ i .pos) ⟩ + [ weaklF Δ ∘ toVar , weakrF ∘ toVar ] (splitPos Δ $ i .pos) ≡⟨⟩ + [ toVar ∘ weaklPos Δ , toVar ∘ weakrPos ] (splitPos Δ $ i .pos) ≡˘⟨ ⊎.[,]-∘ toVar (splitPos Δ $ i .pos) ⟩ + toVar ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ $ i .pos) ≡⟨ cong toVar (weakPos-splitPos Δ (i .pos)) ⟩ + toVar (i .pos) ≡⟨⟩ + i ∎ + where open ≡-Reasoning + +copair-unique : + {X : A -Sorted- B -Family} → + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) (s : Γ ++ Δ ~[ X ]↝ Θ) → + (weakl Δ ⨾′ s ≈ σ) → (weakr ⨾′ s ≈ ς) → + (σ ∥ ς) ≈ s +copair-unique {Δ = Δ} σ ς s wkl⨾s≈σ wkr⨾s≈ς ＠ i = begin + [ σ ＠_ , ς ＠_ ] (splitF Δ i) ≡˘⟨ ⊎.[,]-cong (wkl⨾s≈σ ＠_) (wkr⨾s≈ς ＠_) (splitF Δ i) ⟩ + [ (weakl Δ ⨾′ s) ＠_ , (weakr ⨾′ s) ＠_ ] (splitF Δ i) ≡˘⟨ ⊎.[,]-∘ (s ＠_) (splitF Δ i) ⟩ + s ＠ ([ weaklF Δ , weakrF ] $ splitF Δ i) ≡⟨ cong (s ＠_) (weakF-splitF Δ i) ⟩ + s ＠ i ∎ where open ≡-Reasoning -- Special Families ----------------------------------------------------------- infixr 5 _⇒_ -_⇒_ : Family → Family → Family +_⇒_ : A -Family → A -Family → A -Family (X ⇒ Y) Γ = X Γ → Y Γ -_^_ : Family → ValFamily → Family -(X ^ V) Γ = {Δ : Context} → Γ ~[ V ]↝ Δ → X Δ - -_^ᵛ_ : ValFamily → ValFamily → ValFamily -(W ^ᵛ V) A = W A ^ V +_^_ : A -Family → B -Sorted- A -Family → B -Family +(X ^ V) Γ = {Δ : GenContext _} → Γ ~[ V ]↝ Δ → X Δ -_^ᶜ_ : CompFamily → ValFamily → CompFamily -(C ^ᶜ V) B = C B ^ V +_^ᵗ_ : A -Sorted- B -Family → C -Sorted- B -Family → A -Sorted- C -Family +(W ^ᵗ V) τ = W τ ^ V -□_ : Family → Family +□_ : A -Family → A -Family □_ = _^ Var -□ᵛ_ : ValFamily → ValFamily -□ᵛ_ = _^ᵛ Var +□ᵗ_ : A -Sorted- B -Family → A -Sorted- B -Family +□ᵗ_ = _^ᵗ Var -□ᶜ_ : CompFamily → CompFamily -□ᶜ_ = _^ᶜ Var - -δ : Context → Family → Family +δ : GenContext A → A -Family → A -Family δ Δ X Γ = X (Γ ++ Δ) -δᵛ : Context → ValFamily → ValFamily -δᵛ Δ V A = δ Δ (V A) +δᵗ : GenContext B → A -Sorted- B -Family → A -Sorted- B -Family +δᵗ Δ V τ = δ Δ (V τ) + +-- Reflection ------------------------------------------------------------------ + +wknTerm : Term → Term +wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ [] + +weaklTerm : Term → Term → Term +weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ [] + +searchCtx : + (wkn : Term → Term) → + (hole : Term) → + (name : Term) → + (Γ : Term) → + TC ⊤ +searchCtx wkn hole name (meta m _) = blockOnMeta m +searchCtx wkn hole name (con (quote _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ meta x _ ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) = + blockOnMeta x +searchCtx wkn hole name (con (quote _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ x ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) = + catchTC + (do + debugPrint "squid" 10 (strErr "checking name " ∷ termErr x ∷ strErr "..." ∷ []) + unify name x + let soln = wkn (quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ []) + debugPrint "squid" 10 (strErr "testing solution " ∷ termErr soln ∷ strErr "..." ∷ []) + unify soln hole + debugPrint "squid" 10 (strErr "success!" ∷ [])) + (searchCtx (wkn ∘ wknTerm) hole name Γ) +searchCtx wkn hole name (con (quote [<]) (_ ⟅∷⟆ [])) = + typeError (termErr name ∷ strErr " not in context." ∷ []) +searchCtx wkn hole name (def (quote _++_) (_ ⟅∷⟆ Γ ⟨∷⟩ Δ ⟨∷⟩ [])) = + catchTC + (searchCtx wkn hole name Δ) + (searchCtx (wkn ∘ weaklTerm Δ) hole name Γ) +searchCtx wkn hole name Γ = + typeError (termErr name ∷ strErr " not in context " ∷ termErr Γ ∷ []) + +searchVarPos : {A : Set} → GenContext A → Name → Term → TC ⊤ +searchVarPos Γ x hole = + do + Γ ← quoteTC Γ + x ← quoteTC x + case x returning (λ _ → TC ⊤) of λ + { (meta x _) → blockOnMeta x + ; _ → pure _ + } + debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) + debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) + searchCtx (λ t → t) hole x Γ -δᶜ : Context → CompFamily → CompFamily -δᶜ Δ C B = δ Δ (C B) +%%_ : + {A : Set} → {ty : A} → {Γ : GenContext A} → + (x : Name) → {@(tactic searchVarPos Γ x) pos : VarPos x ty Γ} → Var ty Γ +%%_ x {pos} = MkVar x pos |