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 11:30:23 -06:00
parent 112cebb8b7
commit 7433e6e5f7
3 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
prototyping/Interpreter.agda
View file

@ -24,7 +24,7 @@ runBlock : ∀ {a} → Block a → IO ⊤
runBlock block with run block
runBlock block | return V D = putStrLn (valueToString V)
runBlock block | done D = putStrLn "nil"
runBlock block | error E D = putStrLn (errToStringᴮ E)
runBlock block | error E D = putStrLn (errToStringᴮ _ E)
runJSON : Value → IO ⊤
runJSON value with blockFromJSON(value)

20
prototyping/Properties/Step.agda
View file

@ -32,7 +32,7 @@ stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
stepᴱ H nil = value nil refl
stepᴱ H (var x) = error (UnboundVariable x)
stepᴱ H (var x) = error UnboundVariable
stepᴱ H (addr a) = value (addr a) refl
stepᴱ H (number x) = value (number x) refl
stepᴱ H (M $ N) with stepᴱ H M
@ -40,17 +40,17 @@ 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₂ v s)
stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ])
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV a p))
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV p))
stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p)
stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w refl refl (λ ()))
stepᴱ H (_ $ _) | value (number x) refl | value w refl = error (FunctionMismatch (number x) w refl refl (λ ()))
stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ()))
stepᴱ H (_ $ _) | value (number x) refl | value w refl = error (FunctionMismatch (number x) w (λ ()))
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
stepᴱ H (M $ N) | error E = error (app₁ E)
stepᴱ H (block b is B end) with stepᴮ H B
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
stepᴱ H (block b is (return _ ∙ B′) end) | return v refl = step H (val v) (return v)
stepᴱ H (block b is done end) | done refl = step H nil done
stepᴱ H (block b is B end) | error E = error (block b E)
stepᴱ H (block b is B end) | error E = error (block E)
stepᴱ H (function F is C end) with alloc H (function F is C end)
stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function a p)
stepᴱ H (binexp M op N) with stepᴱ H M
@ -58,10 +58,10 @@ stepᴱ H (binexp M op N) | value v refl with stepᴱ H N
stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s)
stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E)
stepᴱ H (binexp M op N) | value (number m) refl | value (number n) refl = step H (number (evalBinOp m op n)) binOpEval
stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ op nil w refl refl λ ())
stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ op (addr a) w refl refl λ ())
stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ op v nil refl refl (λ ()))
stepᴱ H (binexp M op N) | value v refl | value (addr a) refl = error (BinopMismatch₂ op v (addr a) refl refl (λ ()))
stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ nil w λ ())
stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ (addr a) w λ ())
stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ v nil (λ ()))
stepᴱ H (binexp M op N) | value v refl | value (addr a) refl = error (BinopMismatch₂ v (addr a) (λ ()))
stepᴱ H (binexp M op N) | step H′ M′ s = step H′ (binexp M′ op N) (binOp₁ s)
stepᴱ H (binexp M op N) | error E = error (bin₁ E)
@ -70,7 +70,7 @@ stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / na
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
stepᴮ H (local x ← _ ∙ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v)
stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
stepᴮ H (local x ← M ∙ B) | error E = error (local E)
stepᴮ H (return M ∙ B) with stepᴱ H M
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
stepᴮ H (return _ ∙ B) | value V refl = return V refl

14
prototyping/Properties/StrictMode.agda
View file

@ -366,18 +366,18 @@ reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)
runtimeWarningᴱ H (var x) (UnboundVariable x) = UnboundVariable x refl
runtimeWarningᴱ H (addr a) (SEGV a p) = UnallocatedAddress a p
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p q r) = {!!} -- app₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable x refl
runtimeWarningᴱ H (addr a) (SEGV p) = UnallocatedAddress a p
runtimeWarningᴱ H (M $ N) (FunctionMismatch v w r) = {!!} -- app₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
runtimeWarningᴱ H (block var b ∈ T is B end) (block _ err) = block₁ b (runtimeWarningᴮ H B err)
runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ op v w p q r) = {!!}
runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ op v w p q r) = {!!}
runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ b (runtimeWarningᴮ H B err)
runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ v w p) = {!!}
runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = {!!}
runtimeWarningᴱ H (binexp M op N) (bin₁ err) = {!!}
runtimeWarningᴱ H (binexp M op N) (bin₂ err) = {!!}
runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local _ err) = local₁ (runtimeWarningᴱ H M err)
runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err)
runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)
wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)