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

Merge remote-tracking branch 'upstream/master' into prototyping-binary-operations

Browse source
This commit is contained in:
Lily Brown 2022-02-18 14:49:18 -08:00
commit 92539bc3d0
4 changed files with 27 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
prototyping/Luau/OpSem.agda
View file

@ -32,17 +32,23 @@ data _⊢_⟶ᴱ_⊣_ where
-------------------------------------------
H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
app : ∀ {H H′ M M′ N} →
app₁ : ∀ {H H′ M M′ N} →
H ⊢ M ⟶ᴱ M′ ⊣ H′ →
-----------------------------
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
beta : ∀ {H M a F B} →
app₂ : ∀ {H H′ V N N′} →
H ⊢ N ⟶ᴱ N′ ⊣ H′ →
-----------------------------
H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′
beta : ∀ {H a F B V} →
H [ a ] ≡ just(function F is B end) →
-----------------------------------------------------
H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
-----------------------------------------------------------------------------
H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H
block : ∀ {H H′ B B′ b} →

3
prototyping/Luau/RuntimeError.agda
View file

@ -16,7 +16,8 @@ data RuntimeErrorᴱ H where
TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v)
UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
data RuntimeErrorᴮ H where

7
prototyping/Luau/RuntimeError/ToString.agda
View file

@ -2,7 +2,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; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; ValueIsNotANumber)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block; ValueIsNotANumber)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (exprToString)
open import Luau.Var.ToString using (varToString)
@ -15,10 +15,11 @@ errToStringᴱ NilIsNotAFunction = "nil is not a function"
errToStringᴱ (NumberIsNotAFunction n) = "number " ++ primShowFloat n ++ " is not a function"
errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (app E) = errToStringᴱ E
errToStringᴱ (app₁ E) = errToStringᴱ E
errToStringᴱ (app₂ E) = errToStringᴱ E
errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b
errToStringᴱ (ValueIsNotANumber v) = exprToString v ++ " is not a number"
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x)
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement"

19
prototyping/Properties/Step.agda
View file

@ -5,7 +5,7 @@ open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTi
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 ; beta; function; block; return; done; local; subst; binOp; evalBinOp)
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp; evalBinOp)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app; block; local; return)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Value using (nil; addr; val; number)
@ -33,13 +33,16 @@ stepᴱ H (var x) = error (UnboundVariable x)
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 (nil $ N) | value nil refl = error (TypeMismatch nil (nil $ N))
stepᴱ H ((number _) $ N) | value (number x) refl = error (NumberIsNotAFunction x)
stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
stepᴱ H (M $ N) | error E = error (app E)
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₂ s)
stepᴱ H (_ $ _) | value nil refl | value W refl = error NilIsNotAFunction
stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (NumberIsNotAFunction n)
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 | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
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