luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-22 12:04:27 -06:00
parent 0cf9acc799
commit afe72cfd86
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
prototyping/Properties/StrictMode.agda
View file

@ -95,19 +95,25 @@ substitutivityᴮ : ∀ {Γ T H} B v x → (just T ≡ typeOfⱽ H v) → (typeO
substitutivityᴱ = {!!} substitutivityᴱ = {!!}
substitutivityᴮ = {!!} substitutivityᴮ = {!!}
preservationᴱ : ∀ {H H′ M M′ Γ} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M′) preservationᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
preservationᴮ : ∀ {H H′ B B′ Γ} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B′) preservationᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)
preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = ok refl preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = ok refl
preservationᴱ (app₁ s) with preservationᴱ s preservationᴱ (app₁ s) with preservationᴱ s
preservationᴱ (app₁ s) | ok p = ok (cong tgt p) preservationᴱ (app₁ s) | ok p = ok (cong tgt p)
preservationᴱ (app₁ s) | warning (expr W) = warning (expr (app₁ W)) preservationᴱ (app₁ s) | warning (expr W) = warning (expr (app₁ W))
preservationᴱ (app₁ s) | warning (heap W) = warning (heap W) preservationᴱ (app₁ s) | warning (heap W) = warning (heap W)
preservationᴱ (app₂ p s) = {!!} preservationᴱ (app₂ p s) with heap-weakeningᴱ (redn-⊑ s)
preservationᴱ {H = H} {Γ = Γ} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p q) with just S ≡ᴹᵀ typeOfⱽ H V | T ≡ᵀ typeOfᴮ H (Γ ⊕ x ↦ S) B preservationᴱ (app₂ p s) | ok q = ok (cong tgt q)
preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ _} {B = B} {V = V} p q) | yes r | yes refl = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) (substitutivityᴮ B V x r)) preservationᴱ (app₂ p s) | warning W = warning (expr (app₁ W))
preservationᴱ (beta p q) | _ | no r = {!!} -- ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!q!}) preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) with remember (typeOfⱽ H V)
preservationᴱ (beta p q) | no r | _ = {!!} -- ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!q!}) preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (just U , q) | yes refl | yes refl = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) (substitutivityᴮ B V x (sym q)))
preservationᴱ {H = H} (beta {a = a} {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ f r)))
preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (just U , q) | no r | _ = warning (expr (app₀ (λ s → r (trans (trans (sym (cong src (cong orBot (cong typeOfᴹᴼ p)))) (trans s (typeOfᴱⱽ V))) (cong orBot q)))))
preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (nothing , q) with typeOf-val-not-bot V
preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ V) (cong orBot q))))
preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) | (nothing , q) | warning W = warning (expr (app₂ W))
preservationᴱ (block s) with preservationᴮ s preservationᴱ (block s) with preservationᴮ s
preservationᴱ (block s) | ok p = ok p preservationᴱ (block s) | ok p = ok p
preservationᴱ (block {b = b} s) | warning (block W) = warning (expr (block b W)) preservationᴱ (block {b = b} s) | warning (block W) = warning (expr (block b W))