diff --git a/core.agda b/core.agda index aec7559..64e349c 100644 --- a/core.agda +++ b/core.agda @@ -85,34 +85,41 @@ module core where model-type : typ expansion-type : typ + -- unexpanded expressions, the outermost layer of expressions: a langauge -- exactly like eexp, but also with livelits - data uexp : Set where - c : uexp - _·:_ : uexp → typ → uexp - X : varname → uexp - ·λ : varname → uexp → uexp - ·λ_[_]_ : varname → typ → uexp → uexp - ⦇⦈[_] : holename → uexp - ⦇⌜_⌟⦈[_] : uexp → holename → uexp - _∘_ : uexp → uexp → uexp - ⟨_,_⟩ : uexp → uexp → uexp - fst : uexp → uexp - snd : uexp → uexp - -- new forms below - -- macro-like livelits --todo pal - ap-pal : livelitname → iexp → (typ × uexp) → uexp -- paper: $a^u - - -- ap-pal : ($a : Nat) → (d : iexp) → (splice : typ × uexp) → uexp -- - -- give livelit name = nat and then this first nat is that - - -- phi is a splice, which is a pair of typ and uexp. in the paper it's - -- n-ary but here we have one becauase we could tuple it up. look into - -- making it List (type × uexp). also define a type for splice that's this pair. - - -- u doesn't appear here, it's a hole name which is nat but we can make - -- a separate alias. add it but just carry it around. todo: generally - -- give aliases for names instead of Nat everywhere. + mutual + data uexp : Set where + c : uexp + _·:_ : uexp → typ → uexp + X : varname → uexp + ·λ : varname → uexp → uexp + ·λ_[_]_ : varname → typ → uexp → uexp + ⦇⦈[_] : holename → uexp + ⦇⌜_⌟⦈[_] : uexp → holename → uexp + _∘_ : uexp → uexp → uexp + ⟨_,_⟩ : uexp → uexp → uexp + fst : uexp → uexp + snd : uexp → uexp + -- new forms below + -- macro-like livelits --todo pal + --ap-pal : livelitname → iexp → splice → uexp -- paper: $a^u + ＄_⟨_⁏_⟩[_] : livelitname → iexp → splice → holename → uexp + + -- ap-pal : ($a : Nat) → (d : iexp) → (splice : typ × uexp) → uexp -- + -- give livelit name = nat and then this first nat is that + + -- phi is a splice, which is a pair of typ and uexp. in the paper it's + -- n-ary but here we have one becauase we could tuple it up. look into + -- making it List (type × uexp). also define a type for splice that's this pair. + + -- u doesn't appear here, it's a hole name which is nat but we can make + -- a separate alias. add it but just carry it around. todo: generally + -- give aliases for names instead of Nat everywhere. + + splice : Set + splice = typ × uexp + -- type consistency data _~_ : (t1 t2 : typ) → Set where @@ -964,16 +971,16 @@ module core where Φ , Γ ⊢ ê2 ~~> e2 ⇒ τ2 → holes-disjoint e1 e2 → Φ , Γ ⊢ ⟨ ê1 , ê2 ⟩ ~~> ⟨ e1 , e2 ⟩ ⇒ τ1 ⊗ τ2 - SPEApPal : ∀{Φ Γ ρ dm π denc eexpanded τsplice psplice esplice} → + SPEApPal : ∀{Φ Γ a dm π denc eexpanded τsplice psplice esplice u} → holes-disjoint eexpanded esplice → freshΓ Γ eexpanded → - (ρ , π) ∈ (Φ)₁ → + (a , π) ∈ (Φ)₁ → ∅ , ∅ ⊢ dm :: (livelitdef.model-type π) → ((livelitdef.expand π) ∘ dm) ⇓ denc → denc ↑ eexpanded → Φ , Γ ⊢ psplice ~~> esplice ⇐ τsplice → ∅ ⊢ eexpanded <= τsplice ==> (livelitdef.expansion-type π) → - Φ , Γ ⊢ ap-pal ρ dm (τsplice , psplice) ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π + Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) ⟩[ u ] ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π data _,_⊢_~~>_⇐_ : (Φ : palctx) → (Γ : tctx) → diff --git a/livelit-reasoning-principles.agda b/livelit-reasoning-principles.agda index 0eda53c..908c1d7 100644 --- a/livelit-reasoning-principles.agda +++ b/livelit-reasoning-principles.agda @@ -27,9 +27,9 @@ module livelit-reasoning-principles where splice-typing : Φ , Γ ⊢ êsplice ~~> esplice ⇐ τsplice × Γ ⊢ esplice <= τsplice context-independence : free-vars (eexpanded ·: τsplice ==> τresult) == [] - livelit-reasoning-principles : ∀{Φ Γ ρ dm τsplice psplice eresult τresult} → - Φ , Γ ⊢ ap-pal ρ dm (τsplice , psplice) ~~> eresult ⇒ τresult → - reasoning-principles Φ Γ ρ dm τsplice psplice eresult τresult + livelit-reasoning-principles : ∀{Φ Γ a dm τsplice psplice eresult τresult u} → + Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) ⟩[ u ] ~~> eresult ⇒ τresult → + reasoning-principles Φ Γ a dm τsplice psplice eresult τresult livelit-reasoning-principles h@(SPEApPal {dm = dm} {π} {denc} {eexpanded} {esplice = esplice} x x₁ x₂ x₃ x₄ x₅ x₆ x₇) = record { π = π