close #10

hazelgrove · Oct 19, 2020 · 8e237e6 · 8e237e6
1 parent 7b58a50
commit 8e237e6
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 13 deletions.
diff --git a/core.agda b/core.agda
@@ -113,7 +113,6 @@ module core where
     snd     : uexp → uexp
     -- new forms below
     -- macro-like livelits --todo pal
-    let-pal_be_·in_ : Nat → livelitdef → uexp → uexp -- delete this but also tag in version control
     ap-pal : livelitname → iexp → (typ × uexp) → uexp  -- paper: $a<d_model; {phi_i} i<n >^u
 
     -- ap-pal : ($a : Nat) → (d : iexp) → (splice : typ × uexp) → uexp -- give livelit name = nat and then this first nat is that
@@ -992,11 +991,6 @@ module core where
                            Φ , Γ ⊢ ê2 ~~> e2 ⇒ τ2 →
                            holes-disjoint e1 e2 →
                            Φ , Γ ⊢ ⟨ ê1 , ê2 ⟩ ~~> ⟨ e1 , e2 ⟩ ⇒ τ1 ⊗ τ2
-        SPELetPal : ∀{Φ Γ π ρ ê e τ} → --todo rule names here
-                           (#h : ρ # (Φ)₁) →
-                           ∅ , ∅ ⊢ livelitdef.expand π :: ((livelitdef.model-type π) ==> Exp) →
-                           (Φ ,, ρ :: π ⦅given #h ⦆) , Γ ⊢ ê ~~> e ⇒ τ →
-                           Φ , Γ ⊢ let-pal ρ be π ·in ê ~~> e ⇒ τ
         SPEApPal  : ∀{Φ Γ ρ dm π denc eexpanded τsplice psplice esplice} →
                          holes-disjoint eexpanded esplice →
                          freshΓ Γ eexpanded →
@@ -1041,11 +1035,6 @@ module core where
                            Φ , Γ ⊢ ê ~~> e ⇒ τ' →
                            τ ~ τ' →
                            Φ , Γ ⊢ ê ~~> e ⇐ τ
-        APELetPal  : ∀{Φ Γ π ρ ê e τ} →
-                           (#h : ρ # (Φ)₁) →
-                           ∅ , ∅ ⊢ livelitdef.expand π :: ((livelitdef.model-type π) ==> Exp) →
-                           (Φ ,, ρ :: π ⦅given #h ⦆) , Γ ⊢ ê ~~> e ⇐ τ →
-                           Φ , Γ ⊢ let-pal ρ be π ·in ê ~~> e ⇐ τ
         APELetFPal : ∀{Φ Γ π ρ ê e τ} →
                            (#h : ρ # (Φ)₁) →
                            (eh : ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π) →

diff --git a/typed-livelit-elaboration.agda b/typed-livelit-elaboration.agda
@@ -16,7 +16,6 @@ module typed-livelit-elaboration where
     typed-livelit-elaboration-synth (SPEAp D1 x D2 x₂) = SAp x₂ (typed-livelit-elaboration-synth D1) x (typed-livelit-elaboration-ana D2)
     typed-livelit-elaboration-synth SPEHole = SEHole
     typed-livelit-elaboration-synth (SPNEHole x D) = SNEHole x (typed-livelit-elaboration-synth D)
-    typed-livelit-elaboration-synth (SPELetPal _ _ D) = typed-livelit-elaboration-synth D
     typed-livelit-elaboration-synth (SPEApPal hd fr x x₁ x₂ x₃ x₄ x₅) = SAp (HDAsc hd) (SAsc (weaken-ana-closed fr x₅)) MAArr (typed-livelit-elaboration-ana x₄)
     typed-livelit-elaboration-synth (SPELetFPal _ _ D) = typed-livelit-elaboration-synth D
     typed-livelit-elaboration-synth {Φ} (SPEApFPal hd1 hd2 hd3 fr1 fr2 h h1 h2) =
@@ -30,5 +29,4 @@ module typed-livelit-elaboration where
                                   Γ ⊢ e <= τ
     typed-livelit-elaboration-ana (APELam x₁ x₂ D) = ALam x₁ x₂ (typed-livelit-elaboration-ana D)
     typed-livelit-elaboration-ana (APESubsume h ch) = ASubsume (typed-livelit-elaboration-synth h) ch
-    typed-livelit-elaboration-ana (APELetPal pcH x D) = typed-livelit-elaboration-ana D
     typed-livelit-elaboration-ana (APELetFPal pcH x D) = typed-livelit-elaboration-ana D