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

revise w/ pr feedback

Browse source
This commit is contained in:
Lily Brown 2022-02-17 13:40:48 -08:00
parent 3aa8fa2419
commit ed96444c5d
11 changed files with 22 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
prototyping/Examples/Run.agda
View file

@ -3,7 +3,7 @@
module Examples.Run where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number_)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number)
open import Luau.Value using (nil; number)
open import Luau.Run using (run; return)
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
@ -14,5 +14,5 @@ import Agda.Builtin.Equality.Rewrite
ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
ex1 = refl
ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (Luau.Syntax.Expr.number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (Luau.Value.Value.number 123.0) _)
ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
ex2 = refl

1
prototyping/Interpreter.agda
View file

@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value
main : IO ⊤
main = getContents >>= runString

5
prototyping/Luau/RuntimeError.agda
View file

@ -4,13 +4,14 @@ open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; _[_])
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String)
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number)
data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
data RuntimeErrorᴱ H where
ValueNotCallable : ∀ x → RuntimeErrorᴱ H x
NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
NumberIsNotAFunction : ∀ n {M} → RuntimeErrorᴱ H ((number n) $ M)
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)

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

@ -1,7 +1,8 @@
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; ValueNotCallable; UnboundVariable; SEGV; app; block)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (exprToString)
open import Luau.Var.ToString using (varToString)
@ -10,8 +11,8 @@ open import Luau.Syntax using (name; _$_)
errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
errToStringᴱ (ValueNotCallable (x $ _)) = "value " ++ exprToString x ++ " is not callable"
errToStringᴱ (ValueNotCallable x) = "value " ++ exprToString x ++ " is not callable"
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
@ -19,3 +20,4 @@ errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ v
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x)
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement"

2
prototyping/Luau/Substitution.agda
View file

@ -1,6 +1,6 @@
module Luau.Substitution where
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number_)
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number)
open import Luau.Value using (Value; val)
open import Luau.Var using (Var; _≡ⱽ_)
open import Properties.Dec using (Dec; yes; no)

2
prototyping/Luau/Syntax.agda
View file

@ -53,4 +53,4 @@ data Expr a where
_$_ : Expr a → Expr a → Expr a
function_is_end : FunDec a → Block a → Expr a
block_is_end : Var → Block a → Expr a
number_ : Float → Expr a
number : Float → Expr a

2
prototyping/Luau/Syntax/FromJSON.agda
View file

@ -1,6 +1,6 @@
module Luau.Syntax.FromJSON where
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number_)
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number)
open import Luau.Type.FromJSON using (typeFromJSON)
open import Agda.Builtin.List using (List; _∷_; [])

2
prototyping/Luau/Syntax/ToString.agda
View file

@ -1,7 +1,7 @@
module Luau.Syntax.ToString where
open import Agda.Builtin.Float using (primShowFloat)
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number_)
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number)
open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Type.ToString using (typeToString)

4
prototyping/Luau/Value.agda
View file

@ -2,7 +2,7 @@ module Luau.Value where
open import Agda.Builtin.Float using (Float)
open import Luau.Addr using (Addr)
open import Luau.Syntax using (Block; Expr; nil; addr)
open import Luau.Syntax using (Block; Expr; nil; addr; number)
open import Luau.Var using (Var)
data Value : Set where
@ -13,4 +13,4 @@ data Value : Set where
val : ∀ {a} → Value → Expr a
val nil = nil
val (addr a) = addr a
val (number x) = Luau.Syntax.Expr.number x
val (number x) = number x

1
prototyping/PrettyPrinter.agda
View file

@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value
main : IO ⊤
main = getContents >>= runString

12
prototyping/Properties/Step.agda
View file

@ -3,11 +3,11 @@ module Properties.Step where
open import Agda.Builtin.Equality using (_≡_; refl)
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_)
open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number)
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; ValueNotCallable; UnboundVariable; SEGV; app; block; local; return)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Value using (nil; addr; val)
open import Luau.Value using (nil; addr; val; number)
open import Properties.Remember using (remember; _,_)
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@ -30,11 +30,11 @@ stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
stepᴱ H nil = value nil refl
stepᴱ H (var x) = error (UnboundVariable x)
stepᴱ H (addr a) = value (addr a) refl
stepᴱ H (number x) = value (Luau.Value.Value.number x) 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 (ValueNotCallable (nil $ N))
stepᴱ H ((number _) $ N) | value (Luau.Value.Value.number x) refl = error (ValueNotCallable ((number x) $ N))
stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
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)