diff --git a/todo.txt b/todo.txt deleted file mode 100644 index b3b7404..0000000 --- a/todo.txt +++ /dev/null @@ -1,199 +0,0 @@ ------ - -i don't think the last statement in cast-inert.agda is actually true. in -the case for lambdas, if both multi-steps are reflexive (i.e. you're done -stepping) you get down to - -Goal: (·λ .x [ .τ ] .d) == (·λ .x [ .τ ] .d') -———————————————————————————————————————————————————————————— -nic : no-id-casts .d .d' -wt : .Δ , .Γ ,, (.x , .τ) ⊢ .d :: .τ2 -x₁ : .Γ .x == None - -which isn't true. if d is (c < b => b >) then d' is (c) and the goal is -false. - ----------------- - -these are actually false! exactly because of the hole case. removing them -and trying to prove what they depended on syntactically rather than via weakening - - - --todo move to weakening when done - -- weaken-hole-synth : ∀{Γ x τ' u} → x # Γ → (Γ ,, (x , τ')) ⊢ ⦇⦈[ u ] ⇒ ⦇⦈ ~> ⦇⦈⟨ u , Id Γ ⟩ ⊣ ■ (u , (Γ , ⦇⦈)) - -- weaken-hole-synth apt = {!!} - - -- ex : ∀{Γ x τ' u} → x # Γ → (Γ ,, (x , τ')) ⊢ ⦇⦈[ u ] ⇒ ⦇⦈ ~> ⦇⦈⟨ u , Id (Γ ,, (x , τ')) ⟩ ⊣ ■ (u , ((Γ ,, (x , τ')) , ⦇⦈)) - -- ex = λ {Γ} {x} {τ'} {u} _ → ESEHole - - -- mutual - -- weaken-synth-expand : ∀{x Γ e τ d Δ τ'} → fresh x d - -- → Γ ⊢ e ⇒ τ ~> d ⊣ Δ - -- → (Γ ,, (x , τ')) ⊢ e ⇒ τ ~> d ⊣ Δ - -- weaken-synth-expand frsh ESConst = ESConst - -- weaken-synth-expand {x = y} {Γ = Γ} {τ = τ} frsh (ESVar {x = x} x₂) = ESVar (x∈∪l Γ (■ (y , _)) x τ x₂) - -- weaken-synth-expand {Γ = Γ} (FLam x₁ frsh) (ESLam x₂ syn) = ESLam (apart-extend1 Γ (flip x₁) x₂) (exchange-expand-synth {Γ = Γ} (flip x₁) (weaken-synth-expand frsh syn)) - -- weaken-synth-expand (FAp (FCast frsh) (FCast frsh₁)) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) = ESAp x₁ x₂ (weaken-synth (fresh-expand-ana2 frsh x₅) x₃) x₄ (weaken-ana-expand frsh x₅) (weaken-ana-expand frsh₁ x₆) - -- weaken-synth-expand (FHole (EFId x₁)) ESEHole = {!!} - -- weaken-synth-expand frsh (ESNEHole x₁ syn) = {!!} - -- weaken-synth-expand (FCast frsh) (ESAsc x₁) = ESAsc (weaken-ana-expand frsh x₁) - - -- weaken-ana-expand : ∀{ Γ e τ d τ' Δ x τ* } → fresh x d - -- → Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ - -- → (Γ ,, (x , τ*)) ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ - -- weaken-ana-expand {Γ = Γ} (FLam x₁ frsh) (EALam x₂ x₃ ana) = EALam (apart-extend1 Γ (flip x₁) x₂) x₃ (exchange-expand-ana {Γ = Γ} (flip x₁) (weaken-ana-expand frsh ana)) - -- weaken-ana-expand frsh (EASubsume x₁ x₂ x₃ x₄) = EASubsume x₁ x₂ (weaken-synth-expand frsh x₃) x₄ - -- weaken-ana-expand (FHole (EFId x₁)) EAEHole = {!!} - -- weaken-ana-expand (FNEHole (EFId x₁) frsh) (EANEHole x₂ x₃) = {!!} - - -- expand-ana-disjoint hd (EASubsume x x₁ x₂ x₃) E2 = expand-synth-disjoint hd x₂ E2 - -- expand-ana-disjoint (HDLam1 hd) (EALam x₁ x₂ E1) E2 = {!!} - -- --expand-ana-disjoint (HDLam1 hd) (EASubsume x₁ x₂ x₃ x₄) E2 = ? - -- -- expand-ana-disjoint hd ex1 {!!} -- (weaken-ana-expand {!fresh-expand-ana1 x₁ (expand-fresh-ana x₁ E2) E2!} E2) - -- expand-ana-disjoint (HDHole x) EAEHole E2 = ##-comm (expand-new-disjoint-ana x E2) - -- expand-ana-disjoint (HDNEHole x hd) (EANEHole x₁ x₂) E2 = disjoint-parts (expand-synth-disjoint hd x₂ E2) (##-comm (expand-new-disjoint-ana x E2)) - - -- expand-synth-disjoint : ∀{ e1 e2 τ1 τ2 e1' e2' τ2' Γ Δ1 Δ2 } → - -- holes-disjoint e1 e2 → - -- Γ ⊢ e1 ⇒ τ1 ~> e1' ⊣ Δ1 → - -- Γ ⊢ e2 ⇐ τ2 ~> e2' :: τ2' ⊣ Δ2 → - -- Δ1 ## Δ2 - -- expand-synth-disjoint HDConst ESConst ana = empty-disj _ - -- expand-synth-disjoint (HDAsc hd) (ESAsc x) ana = expand-ana-disjoint hd x ana - -- expand-synth-disjoint HDVar (ESVar x₁) ana = empty-disj _ - -- expand-synth-disjoint (HDLam1 hd) () ana - -- expand-synth-disjoint (HDLam2 hd) (ESLam x₁ synth) ana = {!!} -- expand-synth-disjoint hd synth {!!} -- (weaken-ana-expand {!!} ana) - -- expand-synth-disjoint (HDHole x) ESEHole ana = ##-comm (expand-new-disjoint-ana x ana) - -- expand-synth-disjoint (HDNEHole x hd) (ESNEHole x₁ synth) ana = disjoint-parts (expand-synth-disjoint hd synth ana) (##-comm (expand-new-disjoint-ana x ana)) - -- expand-synth-disjoint (HDAp hd hd₁) (ESAp x x₁ x₂ x₃ x₄ x₅) ana = disjoint-parts (expand-ana-disjoint hd x₄ ana) (expand-ana-disjoint hd₁ x₅ ana) - - ------------------------------- - data maybeneq : Maybe Nat → Nat → Set where - MNeqN : ∀{x} → maybeneq None x - MNeqS : ∀{x y} → x ≠ y → maybeneq (Some y) x - - - exists-fresh c (Some x) with different-nat x - ... | x' , neq = x' , FConst , MNeqS neq - exists-fresh c None = Z , FConst , MNeqN - - exists-fresh (X x) (Some y) with different-nat2 x y - ... | z , neq1 , neq2 = z , (FVar neq2) , (MNeqS neq1) - exists-fresh (X x) None with different-nat x - ... | x' , neq = x' , FVar neq , MNeqN - - exists-fresh (·λ x [ τ ] d) (Some x₂) = {!!} - exists-fresh (·λ x [ τ ] d) None with exists-fresh d (Some x) - exists-fresh (·λ x [ τ ] d) None | new , fr , MNeqS x₁ = new , FLam x₁ fr , MNeqN - - exists-fresh ⦇⦈⟨ u , σ ⟩ (Some x₁) = {!!} - exists-fresh ⦇⦈⟨ u , σ ⟩ None = {!!} - - exists-fresh ⦇ d ⦈⟨ u , σ ⟩ (Some x₁) = {!!} - exists-fresh ⦇ d ⦈⟨ u , σ ⟩ None = {!!} - - exists-fresh (d ∘ d₁) (Some x) = {!!} - exists-fresh (d ∘ d₁) None = {!!} - - exists-fresh (d ⟨ τ1 ⇒ τ2 ⟩) (Some x₂) = {!!} - exists-fresh (d ⟨ τ1 ⇒ τ2 ⟩) None = {!!} - - exists-fresh (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) (Some x₂) = {!!} - exists-fresh (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) None = {!!} - - ---------------- - - -- there is always a natural number that's fresh for any expression, - -- possibly avoiding one in particular - data used-list : dhexp → List Nat → Set where - ULConst : used-list c [] - ULVar : ∀{x} → used-list (X x) (x :: []) - ULLam : ∀{x τ d l} → used-list d l → used-list (·λ_[_]_ x τ d) (x :: l) - ULHole : - - exists-fresh : (d : dhexp) → Σ[ y ∈ Nat ] (fresh y d) - exists-fresh = {!!} - - -- rename all x's into y's in d to produce d' - data rename : (x : Nat) → (y : Nat) → (d : dhexp) (d' : dhexp) → Set where - RConst : ∀{x y} → rename x y c c - RVar1 : ∀{x y z} → x ≠ z → rename x y (X z) (X z) - RVar2 : ∀{x y} → rename x y (X x) (X y) - -- RLam : ∀{x y τ e} → rename x y ? ? - -- REHole - -- RNEHole - -- RAp - -- RCast - -- RFailedCast - - -- have to do something about the context in the typing judgement as well - -- and probably in the σs. bleh. - - exists-rename : (x y : Nat) (d : dhexp) → Σ[ d' ∈ dhexp ](rename x y d d') - exists-rename z y c = c , RConst - exists-rename z y (X x) with natEQ z x - exists-rename z y (X .z) | Inl refl = X y , RVar2 - exists-rename z y (X x) | Inr x₁ = X x , RVar1 x₁ - exists-rename z y (·λ x [ x₁ ] d) = {!!} - exists-rename z y ⦇⦈⟨ x ⟩ = {!!} - exists-rename z y ⦇ d ⦈⟨ x ⟩ = {!!} - exists-rename z y (d ∘ d₁) = {!!} - exists-rename z y (d ⟨ x ⇒ x₁ ⟩) = {!!} - exists-rename z y (d ⟨ x ⇒⦇⦈⇏ x₁ ⟩) = {!!} - - rename-ctx : {A : Set} → (x y : Nat) → (Γ : A ctx) → A ctx - rename-ctx x y Γ q with natEQ y q -- if you're asking about the new variable y, it's now gonna be whatever x was - rename-ctx x y Γ q | Inl x₁ = Γ x - rename-ctx x y Γ q | Inr x₁ = Γ q - - -- is this the right direction? try to use it below; need that y # Γ, likely - rename-preserve : ∀{x y d d' Δ Γ τ} → fresh y d - → rename x y d d' - → Δ , (rename-ctx x y Γ) ⊢ d' :: τ - → Δ , Γ ⊢ d :: τ - rename-preserve = {!!} - - ------ - -i think i actually can't do substitution the 312/abt way. you need a finite -collection, not a context with a possibly infinite domain, of the variables -that are used in a term so that you can pick something that's fresh -throughout. i tried to do just one but then you need two, etc. this is, i -think, ultimately not possible because freshness for dhexps is defined wrt -freshness for environments which has a \Gamma in it that's a function so i -can't iterate over all the elements of the domain and pick something that's -bigger than all of them. so this idea works, just not with this exact -representation of contexts. - ----- - - -- the variable name x does not appear in the term d - -- data var-name-new : (x : Nat) (d : ihexp) → Set where - -- VNNConst : ∀{x} → var-name-new x c - -- VNNVar : ∀{x y} → x ≠ y → var-name-new x (X y) - -- VNNLam2 : ∀{x d y τ} → x ≠ y - -- → var-name-new x d - -- → var-name-new x (·λ_[_]_ y τ d) - -- VNNHole : ∀{x u σ} → var-name-new-σ x σ - -- → var-name-new x (⦇⦈⟨ u , σ ⟩) - -- VNNNEHole : ∀{x u σ d } - -- → var-name-new-σ x σ - -- → var-name-new x d - -- → var-name-new x (⦇ d ⦈⟨ u , σ ⟩) - -- VNNAp : ∀{ x d1 d2 } → - -- var-name-new x d1 → - -- var-name-new x d2 → - -- var-name-new x (d1 ∘ d2) - -- VNNCast : ∀{x d τ1 τ2} → var-name-new x d → var-name-new x (d ⟨ τ1 ⇒ τ2 ⟩) - -- VNNFailedCast : ∀{x d τ1 τ2} → var-name-new x d → var-name-new x (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) ----- - binders-envfresh {Γ' = Γ'} {y = y} (STAId sub x) apt UBσId BUσId with ctxindirect Γ' y - binders-envfresh (STAId sub x₁) apt UBσId BUσId | Inl x = abort (somenotnone (! (π2 (sub _ x)) · apt)) - binders-envfresh (STAId sub x₁) apt UBσId BUσId | Inr x = EFId x - binders-envfresh {y = y} (STASubst {y = z} sub x₁) apt (UBσSubst x₂ ub) (BUσSubst x x₃) with natEQ y z - binders-envfresh (STASubst sub x₁) apt (UBσSubst x₂ ub) (BUσSubst x₃ x₄) | Inl refl = {!!} - binders-envfresh (STASubst sub x₁) apt (UBσSubst x₂ ub) (BUσSubst x₃ x₄) | Inr x = EFSubst (binders-fresh x₁ {!!} x₃ {!!} x₂ apt) - {!binders-envfresh sub ? !}