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-24 10:46:27 -06:00
parent c6c0097729
commit ae0745e800
2 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
prototyping/Luau/OpSem.agda
View file

@ -52,11 +52,10 @@ data _⊢_⟶ᴱ_⊣_ where
----------------------------------------------------
H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′
return : ∀ v {H M B b} →
return : ∀ v {H B b} →
(M ≡ val v) →
--------------------------------------------------------
H ⊢ (block b is return M ∙ B end) ⟶ᴱ M ⊣ H
H ⊢ (block b is return (val v) ∙ B end) ⟶ᴱ val v ⊣ H
done : ∀ {H b} →

6
prototyping/Properties/StrictMode.agda
View file

@ -39,7 +39,7 @@ rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
rednᴱ⊑ (beta O v p q) = refl
rednᴱ⊑ (block s) = rednᴮ⊑ s
rednᴱ⊑ (return v p) = refl
rednᴱ⊑ (return v) = refl
rednᴱ⊑ done = refl
rednᴱ⊑ (binOpEval) = refl
rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
@ -163,7 +163,7 @@ preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (trans (typeOfᴱⱽ v) (cong orBot q))))
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v p) = {!!} -- ok refl
preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) = {!!} -- ok refl
preservationᴱ H (block var b ∈ T is done end) (done) = {!!} -- ok refl
preservationᴱ H (binexp M op N) s = {!!}
@ -340,7 +340,7 @@ reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′)
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W
reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ b W)
reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v s) (heap W′) = heap W′
reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′
reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′
reflectᴴᴱ H (binexp M op N) s W′ = {!!}