Skip to content

Commit

Permalink
close #9
Browse files Browse the repository at this point in the history
  • Loading branch information
@ivoysey
ivoysey committed Oct 19, 2020
1 parent 8e237e6 commit cb73014
Show file tree
Hide file tree
Showing 4 changed files with 0 additions and 75 deletions.
1 change: 0 additions & 1 deletion all.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
48 changes: 0 additions & 48 deletions core.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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} → τ ~ τ
Expand Down Expand Up @@ -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 Φ →
Expand All @@ -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) →
Expand Down Expand Up @@ -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) →
Expand All @@ -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 ⇐ τ
21 changes: 0 additions & 21 deletions livelits-checks.agda
View file

This file was deleted.

5 changes: 0 additions & 5 deletions typed-livelit-elaboration.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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₁)
Expand All @@ -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

0 comments on commit cb73014

Please sign in to comment.