From ed96444c5db7970f8f762809bbfe81787414ff45 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Thu, 17 Feb 2022 13:40:48 -0800 Subject: [PATCH] revise w/ pr feedback --- prototyping/Examples/Run.agda | 4 ++-- prototyping/Interpreter.agda | 1 - prototyping/Luau/RuntimeError.agda | 5 +++-- prototyping/Luau/RuntimeError/ToString.agda | 8 +++++--- prototyping/Luau/Substitution.agda | 2 +- prototyping/Luau/Syntax.agda | 2 +- prototyping/Luau/Syntax/FromJSON.agda | 2 +- prototyping/Luau/Syntax/ToString.agda | 2 +- prototyping/Luau/Value.agda | 4 ++-- prototyping/PrettyPrinter.agda | 1 - prototyping/Properties/Step.agda | 12 ++++++------ 11 files changed, 22 insertions(+), 21 deletions(-) diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 5818ee0c..3cac564d 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -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 diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index 3ec5b8d1..fe311e57 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value main : IO ⊤ main = getContents >>= runString - diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 17ff7930..f9e684b3 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -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) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index 9ebec69b..ac760fab 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -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" + \ No newline at end of file diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index f8092c8a..e364a000 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -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) diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index a1898a92..1313456b 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -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 diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 94beec75..8191e9e7 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -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; _∷_; []) diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index cd4f9702..a20b360b 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -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) diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda index 7453d323..1086d39c 100644 --- a/prototyping/Luau/Value.agda +++ b/prototyping/Luau/Value.agda @@ -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 diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda index 4a6c7dd6..fdad32d6 100644 --- a/prototyping/PrettyPrinter.agda +++ b/prototyping/PrettyPrinter.agda @@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value main : IO ⊤ main = getContents >>= runString - diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index e42a30a9..620dc618 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -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)