mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
WIP
This commit is contained in:
ajeffrey@roblox.com
parent
2b52a6eb68
commit
c6c0097729
5 changed files with 27 additions and 33 deletions
|
|
@ -33,20 +33,18 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
|
||||
|
||||
app₂ : ∀ {H H′ M V N N′} →
|
||||
app₂ : ∀ v {H H′ N N′} →
|
||||
|
||||
M ≡ val V →
|
||||
H ⊢ N ⟶ᴱ N′ ⊣ H′ →
|
||||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M $ N′) ⊣ H′
|
||||
H ⊢ (val v $ N) ⟶ᴱ (val v $ N′) ⊣ H′
|
||||
|
||||
beta : ∀ O v {H a N F B} →
|
||||
beta : ∀ O v {H a F B} →
|
||||
|
||||
(O ≡ function F is B end) →
|
||||
(N ≡ val v) →
|
||||
H [ a ] ≡ just(O) →
|
||||
-----------------------------------------------------------------------------
|
||||
H ⊢ (addr a $ N) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H
|
||||
H ⊢ (addr a $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H
|
||||
|
||||
block : ∀ {H H′ B B′ b} →
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ module Luau.RuntimeError.ToString where
|
|||
|
||||
open import Agda.Builtin.Float using (primShowFloat)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
|
||||
open import Luau.RuntimeType.ToString using (runtimeTypeToString)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Syntax.ToString using (exprToString)
|
||||
|
|
|
|||
|
|
@ -136,11 +136,6 @@ statFromObject obj | just(string "AstStatLocal") | just(_) | just(_) = Left "Ast
|
|||
statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "AstStatLocal missing values"
|
||||
statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
|
||||
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value with exprFromJSON value
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function "" ⟨ x ⟩ is B end) = Right (function f ⟨ x ⟩ is B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Left err = Left err
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ = Left "AstStatLocalFunction name is not a string"
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩ is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩ is B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
|
||||
|
|
@ -176,3 +171,4 @@ blockFromArray arr | just value | Left err = Left err
|
|||
blockFromArray arr | just value | Right S with blockFromArray(tail arr)
|
||||
blockFromArray arr | just value | Right S | Left err = Left (err)
|
||||
blockFromArray arr | just value | Right S | Right B = Right (S ∙ B)
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ open import FFI.Data.Maybe using (just; nothing)
|
|||
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +)
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpEval; evalBinOp; binOp₁; binOp₂)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
|
||||
open import Luau.RuntimeType using (function; number)
|
||||
open import Luau.Substitution using (_[_/_]ᴮ)
|
||||
open import Luau.Value using (nil; addr; val; number)
|
||||
|
|
@ -38,8 +38,8 @@ stepᴱ H (addr a) = value (addr a) refl
|
|||
stepᴱ H (number x) = value (number x) refl
|
||||
stepᴱ H (M $ N) with stepᴱ H M
|
||||
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
|
||||
stepᴱ H (_ $ N) | value V refl with stepᴱ H N
|
||||
stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ refl s)
|
||||
stepᴱ H (_ $ N) | value v refl with stepᴱ H N
|
||||
stepᴱ H (_ $ N) | value v refl | step H′ N′ s = step H′ (val v $ N′) (app₂ v s)
|
||||
stepᴱ H (_ $ _) | value nil refl | value W refl = {!!} -- error (app₁ (TypeMismatch function nil λ()))
|
||||
stepᴱ H (_ $ _) | value (number n) refl | value W refl = {!!} -- error (app₁ (TypeMismatch function (number n) λ()))
|
||||
stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H
|
|||
rednᴱ⊑ (function a p) = snoc p
|
||||
rednᴱ⊑ (app₁ s) = rednᴱ⊑ s
|
||||
rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s
|
||||
rednᴱ⊑ (beta O v p q r) = refl
|
||||
rednᴱ⊑ (beta O v p q) = refl
|
||||
rednᴱ⊑ (block s) = rednᴮ⊑ s
|
||||
rednᴱ⊑ (return v p) = refl
|
||||
rednᴱ⊑ done = refl
|
||||
|
|
@ -154,14 +154,14 @@ preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W)
|
|||
preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s)
|
||||
preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q)
|
||||
preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) with remember (typeOfⱽ H v)
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) | (just U , q) | yes refl | yes refl = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!!}) -- (substitutivityᴮ H B v x (sym q)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ f r)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) | (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 (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl refl p) | (nothing , q) with typeOf-val-not-bot v
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl 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 refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!!}) -- (substitutivityᴮ H B v x (sym q)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (function₀ f r)))
|
||||
preservationᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (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 (addr a $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-bot v
|
||||
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 done end) (done) = {!!} -- ok refl
|
||||
|
|
@ -289,14 +289,14 @@ reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakenin
|
|||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₀ f W′) = {!!}
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) with remember (typeOfⱽ H v)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (just S , q) with S ≡ᵀ T
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (just T , q) | yes refl = heap (addr a p (function₁ f (reflect-substitutionᴮ B v x (sym q) W′)))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (just S , q) | no r = expr (app₀ (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (nothing , q) with typeOf-val-not-bot v
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl refl p) (block₁ f W′) | (nothing , q) | warning W = expr (app₂ W)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₀ f W′) = {!!}
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) with remember (typeOfⱽ H v)
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just S , q) with S ≡ᵀ T
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just T , q) | yes refl = heap (addr a p (function₁ f (reflect-substitutionᴮ B v x (sym q) W′)))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (just S , q) | no r = expr (app₀ (λ s → r (trans (cong orBot (sym q)) (trans (sym (typeOfᴱⱽ v)) (trans (sym s) (cong src (cong orBot (cong typeOfᴹᴼ p))))))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) with typeOf-val-not-bot v
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) | ok r = CONTRADICTION (r (trans (cong orBot (sym q)) (sym (typeOfᴱⱽ v))))
|
||||
reflectᴱ H (addr a $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ f W′) | (nothing , q) | warning W = expr (app₂ W)
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ b W′) = {!!}
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ b W′) with reflectᴮ H B s W′
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ b W′) | heap W = heap W
|
||||
|
|
@ -336,7 +336,7 @@ reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W)
|
|||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′)
|
||||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W
|
||||
reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W)
|
||||
reflectᴴᴱ H (M $ N) (beta O v p q r) (heap W′) = heap W′
|
||||
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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue