From cb73014a3e7880768bde27e5e202a0c22305f061 Mon Sep 17 00:00:00 2001 From: Ian Ernest Voysey Date: Mon, 19 Oct 2020 15:47:02 -0400 Subject: [PATCH] close #9 --- all.agda | 1 - core.agda | 48 ---------------------------------- livelits-checks.agda | 21 --------------- typed-livelit-elaboration.agda | 5 ---- 4 files changed, 75 deletions(-) delete mode 100644 livelits-checks.agda diff --git a/all.agda b/all.agda index 887d9f7..9b0a194 100644 --- a/all.agda +++ b/all.agda @@ -54,7 +54,6 @@ open import weakening open import binders-disjoint-checks open import continuity -open import livelits-checks open import typed-livelit-elaboration open import lemmas-freevars open import livelit-reasoning-principles diff --git a/core.agda b/core.agda index f65b733..1b3dc65 100644 --- a/core.agda +++ b/core.agda @@ -86,16 +86,8 @@ module core where model-type : typ expansion-type : typ - record fpaldef : Set where -- todo delete this with fpaldef - field - expand : eexp - model-type : typ - splice-type : typ - expansion-type : typ - data palctx-entry : Set where -- todo pal MPalDef : livelitdef → palctx-entry - FPalDef : fpaldef → palctx-entry -- todo this goes away so doesn't need to be a datatype any more -- unexpanded expressions, the outermost layer of expressions: a langauge -- exactly like eexp, but also with livelits @@ -123,11 +115,6 @@ module core where -- u doesn't appear here, it's a hole name which is nat but we can make a separate alias. todo: generally give aliases for names instead of Nat everywhere. - -- function-like livelits --TODO: delete these guys but tag a version - -- in git so that we can go back to it if we want to - let-fpal_be_·in_ : Nat → fpaldef → uexp → uexp - ap-fpal : Nat → eexp → uexp → uexp - -- type consistency data _~_ : (t1 t2 : typ) → Set where TCRefl : {τ : typ} → τ ~ τ @@ -917,11 +904,6 @@ module core where data _palctx' : (Φ' : palctx-entry ctx) → Set where PhiWFEmpty : ∅ palctx' - PhiWFInductive : ∀{ρ π} → - (Φ : palctx) → - ρ # π1 Φ → - ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π → - (π1 Φ ,, (ρ , FPalDef π)) palctx' PhiWFMac : ∀{ρ π} → (Φ : palctx) → ρ # π1 Φ → @@ -939,14 +921,6 @@ module core where palctx Φ ,, a :: π ⦅given #h ⦆ = ((Φ)₁ ,, (a , MPalDef π) , PhiWFMac Φ #h) - _,,_::_⦅given_and_⦆ : (Φ : palctx) → - (a : livelitname) → - (π : fpaldef) → - a # (Φ)₁ → - ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π → - palctx - Φ ,, a :: π ⦅given #h and eh ⦆ = ((Φ)₁ ,, (a , FPalDef π) , PhiWFInductive Φ #h eh) - -- livelit expansion -- todo, should this be called elaboration? mutual data _,_⊢_~~>_⇒_ : (Φ : palctx) → @@ -1001,23 +975,6 @@ module core where Φ , Γ ⊢ psplice ~~> esplice ⇐ τsplice → ∅ ⊢ eexpanded <= τsplice ==> (livelitdef.expansion-type π) → Φ , Γ ⊢ ap-pal ρ dm (τsplice , psplice) ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π - SPELetFPal : ∀{Φ Γ π ρ ê e τ} → - (#h : ρ # (Φ)₁) → - (eh : ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π) → - (Φ ,, ρ :: π ⦅given #h and eh ⦆) , Γ ⊢ ê ~~> e ⇒ τ → - Φ , Γ ⊢ let-fpal ρ be π ·in ê ~~> e ⇒ τ - SPEApFPal : ∀{Φ Γ π ρ emodel psplice esplice} → - holes-disjoint (fpaldef.expand π) emodel → - holes-disjoint (fpaldef.expand π) esplice → - holes-disjoint emodel esplice → - freshΓ Γ (fpaldef.expand π) → - freshΓ Γ emodel → - (ρ , FPalDef π) ∈ (Φ)₁ → - Φ , Γ ⊢ psplice ~~> esplice ⇐ fpaldef.splice-type π → - ∅ ⊢ emodel <= fpaldef.model-type π → - Φ , Γ ⊢ ap-fpal ρ emodel psplice ~~> - (((fpaldef.expand π ·: fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π) ∘ emodel) ∘ esplice) ⇒ - fpaldef.expansion-type π data _,_⊢_~~>_⇐_ : (Φ : palctx) → (Γ : tctx) → @@ -1035,8 +992,3 @@ module core where Φ , Γ ⊢ ê ~~> e ⇒ τ' → τ ~ τ' → Φ , Γ ⊢ ê ~~> e ⇐ τ - APELetFPal : ∀{Φ Γ π ρ ê e τ} → - (#h : ρ # (Φ)₁) → - (eh : ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π) → - (Φ ,, ρ :: π ⦅given #h and eh ⦆) , Γ ⊢ ê ~~> e ⇐ τ → - Φ , Γ ⊢ let-fpal ρ be π ·in ê ~~> e ⇐ τ diff --git a/livelits-checks.agda b/livelits-checks.agda deleted file mode 100644 index 062cbac..0000000 --- a/livelits-checks.agda +++ /dev/null @@ -1,21 +0,0 @@ -open import Nat -open import Prelude -open import core -open import contexts - -module livelits-checks where - -- in a well-formed livelit context, the `expand` of all definitions - -- analyzes against the proper type - llctx-well-typed : ∀{ρ π} → - (Φ : palctx) → - (ρ , FPalDef π) ∈ (Φ)₁ → - ∅ ⊢ fpaldef.expand π <= fpaldef.model-type π ==> fpaldef.splice-type π ==> fpaldef.expansion-type π - llctx-well-typed (_ , PhiWFEmpty) () - llctx-well-typed {ρ} (_ , PhiWFInductive {ρ'} Φ h1 h2) h3 with natEQ ρ ρ' - llctx-well-typed {.ρ'} (_ , PhiWFInductive {ρ'} Φ h1 h2) h3 | Inl refl with someinj (! (ctx-top ((Φ)₁) ρ' (FPalDef _) h1) · h3) - llctx-well-typed {.ρ'} (_ , PhiWFInductive {ρ'} Φ h1 h2) h3 | Inl refl | refl = h2 - llctx-well-typed {ρ} (_ , PhiWFInductive {ρ'} Φ h1 h2) h3 | Inr ne = llctx-well-typed Φ (lem-neq-union-eq {Γ = π1 Φ} ne h3) - llctx-well-typed {ρ} (_ , PhiWFMac {ρ'} Φ h1) h3 with natEQ ρ ρ' - llctx-well-typed {.ρ'} (_ , PhiWFMac {ρ'} Φ h1) h3 | Inl refl with (! (ctx-top (Φ ₁) ρ' (MPalDef _) h1) · h3) - llctx-well-typed {.ρ'} (_ , PhiWFMac {ρ'} Φ h1) h3 | Inl refl | () - llctx-well-typed {ρ} (_ , PhiWFMac {ρ'} Φ h1) h3 | Inr ne = llctx-well-typed Φ (lem-neq-union-eq {Γ = π1 Φ} ne h3) diff --git a/typed-livelit-elaboration.agda b/typed-livelit-elaboration.agda index 88a74fd..33ba941 100644 --- a/typed-livelit-elaboration.agda +++ b/typed-livelit-elaboration.agda @@ -2,7 +2,6 @@ open import Prelude open import core open import contexts open import weakening -open import livelits-checks module typed-livelit-elaboration where mutual @@ -17,9 +16,6 @@ module typed-livelit-elaboration where typed-livelit-elaboration-synth SPEHole = SEHole typed-livelit-elaboration-synth (SPNEHole x D) = SNEHole x (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) = - SAp (HDAp (HDAsc hd2) hd3) (SAp (HDAsc hd1) (SAsc (weaken-ana-closed fr1 (llctx-well-typed Φ h))) MAArr (weaken-ana-closed fr2 h2)) MAArr (typed-livelit-elaboration-ana h1) typed-livelit-elaboration-synth (SPEFst h x) = SFst (typed-livelit-elaboration-synth h) x typed-livelit-elaboration-synth (SPESnd h x) = SSnd (typed-livelit-elaboration-synth h) x typed-livelit-elaboration-synth (SPEPair h h₁ x) = SPair x (typed-livelit-elaboration-synth h) (typed-livelit-elaboration-synth h₁) @@ -29,4 +25,3 @@ 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 (APELetFPal pcH x D) = typed-livelit-elaboration-ana D