Skip to content
Permalink
Browse files

extrication

  • Loading branch information
jmchapman committed Jan 14, 2020
1 parent b578803 commit ef2a342658013a923aaf079fd50600f701c3b2c7
Showing with 9 additions and 9 deletions.
  1. +9 −9 metatheory/Scoped/Extrication.lagda
@@ -31,9 +31,9 @@ extricateNe⋆ : ∀{Γ K}(A : Γ ⊢Ne⋆ K) → ScopedTy (len⋆ Γ)
-- intrinsically typed terms should also carry user chosen names as
-- instructions to the pretty printer

extricateNf⋆ (Π {K = K} x A) = Π K (extricateNf⋆ A)
extricateNf⋆ (Π {K = K} A) = Π K (extricateNf⋆ A)
extricateNf⋆ (A ⇒ B) = extricateNf⋆ A ⇒ extricateNf⋆ B
extricateNf⋆ (ƛ {K = K} x A) = ƛ K (extricateNf⋆ A)
extricateNf⋆ (ƛ {K = K} A) = ƛ K (extricateNf⋆ A)
extricateNf⋆ (ne n) = extricateNe⋆ n
extricateNf⋆ (con c) = con c

@@ -55,9 +55,9 @@ len (Γ , A) = S (len Γ)
open import Relation.Binary.PropositionalEquality as Eq

extricateVar : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ∋ A → WeirdFin (len Γ)
extricateVar (Z _) = Z
extricateVar Z = Z
extricateVar (S x) = S (extricateVar x)
extricateVar (T x _) = T (extricateVar x)
extricateVar (T x) = T (extricateVar x)

extricateC : ∀{Γ}{A : Γ ⊢Nf⋆ *} → B.TermCon A → Scoped.TermCon
extricateC (integer i) = integer i
@@ -86,15 +86,15 @@ extricateTel σ [] x = []
extricateTel σ (A ∷ As) (t P., ts) = extricate t ∷ extricateTel σ As ts

extricate (` x) = ` (extricateVar x)
extricate {Φ}{Γ} (ƛ {A = A} x t) = ƛ (extricateNf⋆ A) (extricate t)
extricate {Φ}{Γ} (ƛ {A = A} t) = ƛ (extricateNf⋆ A) (extricate t)
extricate (t · u) = extricate t · extricate u
extricate (Λ {K = K} x t) = Λ K (extricate t)
extricate {Φ}{Γ} (·⋆ t A _) = extricate t ScopedTm.·⋆ extricateNf⋆ A
extricate (Λ {K = K} t) = Λ K (extricate t)
extricate {Φ}{Γ} (_·⋆_ t A) = extricate t ScopedTm.·⋆ extricateNf⋆ A
extricate {Φ}{Γ} (wrap1 pat arg t) = wrap (extricateNf⋆ pat) (extricateNf⋆ arg)
(extricate t)
extricate (unwrap1 t _) = unwrap (extricate t)
extricate (unwrap1 t) = unwrap (extricate t)
extricate (con c) = con (extricateC c)
extricate {Φ}{Γ} (builtin b σ ts _) =
extricate {Φ}{Γ} (builtin b σ ts) =
builtin b (extricateSub σ) (extricateTel σ _ ts)
extricate {Φ}{Γ} (error A) = error (extricateNf⋆ A)
\end{code}

0 comments on commit ef2a342

Please sign in to comment.
You can’t perform that action at this time.