From 9d583be8ae6b9f56a76b9e30158753aa707dab55 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Fri, 18 Feb 2022 15:44:40 -0800 Subject: [PATCH] they work --- prototyping/Examples/Run.agda | 5 ++++- prototyping/Luau/OpSem.agda | 14 ++++++++++++- prototyping/Luau/RuntimeError.agda | 4 +++- prototyping/Luau/RuntimeError/ToString.agda | 10 +++++---- prototyping/Luau/RuntimeType/ToString.agda | 9 ++++++++ prototyping/Properties/Step.agda | 23 ++++++++++++++------- 6 files changed, 51 insertions(+), 14 deletions(-) create mode 100644 prototyping/Luau/RuntimeType/ToString.agda diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 3cac564d..534bb122 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; binexp; +) 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) @@ -16,3 +16,6 @@ ex1 = refl ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _) ex2 = refl + +ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _) +ex3 = refl diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index e2e44183..691fc4e7 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -66,10 +66,22 @@ data _⊢_⟶ᴱ_⊣_ where --------------------------------- H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H - binOp : + binOpEval : ∀ {H x op y} → -------------------------------------------------------------------------- H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H + + binOp₁ : + ∀ {H H′ x x′ op y} → + H ⊢ x ⟶ᴱ x′ ⊣ H′ → + --------------------------------------------- + H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′ + + binOp₂ : + ∀ {H H′ x op y y′} → + H ⊢ y ⟶ᴱ y′ ⊣ H′ → + --------------------------------------------- + H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′ data _⊢_⟶ᴮ_⊣_ where diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 31249bb1..b479a72a 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -4,7 +4,7 @@ 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; _∙_; number) +open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp) open import Luau.RuntimeType using (RuntimeType; valueType) open import Luau.Value using (val) open import Properties.Equality using (_≢_) @@ -19,6 +19,8 @@ data RuntimeErrorᴱ H where 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) + bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N) + bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N) data RuntimeErrorᴮ H where local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index ecf13b89..d5528c8b 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -2,23 +2,25 @@ 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₁; app₂; block; ValueIsNotANumber) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; 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) open import Luau.Var.ToString using (varToString) +open import Luau.Value.ToString using (valueToString) 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ᴱ 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ᴱ (bin₁ E) = errToStringᴱ E +errToStringᴱ (bin₂ 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ᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x) errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement" diff --git a/prototyping/Luau/RuntimeType/ToString.agda b/prototyping/Luau/RuntimeType/ToString.agda new file mode 100644 index 00000000..be67ee0c --- /dev/null +++ b/prototyping/Luau/RuntimeType/ToString.agda @@ -0,0 +1,9 @@ +module Luau.RuntimeType.ToString where + +open import FFI.Data.String using (String) +open import Luau.RuntimeType using (RuntimeType; function; number; nil) + +runtimeTypeToString : RuntimeType → String +runtimeTypeToString function = "function" +runtimeTypeToString number = "number" +runtimeTypeToString nil = "nil" diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index f8fbbcd5..2a0978ff 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -5,8 +5,9 @@ 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₁ ; 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.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.RuntimeType using (function; number) open import Luau.Substitution using (_[_/_]ᴮ) open import Luau.Value using (nil; addr; val; number) open import Properties.Remember using (remember; _,_) @@ -36,8 +37,8 @@ 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₂ 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 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 ]) 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) @@ -50,8 +51,17 @@ 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 (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 p) -stepᴱ H (binexp x op y) with stepᴱ H x | stepᴱ H y -stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOp +stepᴱ H (binexp x op y) with stepᴱ H x +stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y +stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOpEval +stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s) +stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E) +stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ())) +stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ())) +stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ())) +stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ())) +stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s) +stepᴱ H (binexp x op y) | error E = error (bin₁ E) stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end) stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p) @@ -64,4 +74,3 @@ stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (r stepᴮ H (return _ ∙ B) | value V refl = return V refl stepᴮ H (return M ∙ B) | error E = error (return E) stepᴮ H done = done refl - \ No newline at end of file