diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 878b8bd0..89564769 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -23,17 +23,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} → diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index f9e684b3..a54d48fe 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -5,16 +5,18 @@ 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.Value using (val) data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M) - NumberIsNotAFunction : ∀ n {M} → RuntimeErrorᴱ H ((number n) $ M) + NilIsNotAFunction : ∀ {V} → RuntimeErrorᴱ H (nil $ val V) + NumberIsNotAFunction : ∀ n {V} → RuntimeErrorᴱ H (number n $ 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 diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index ac760fab..10c0fe08 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -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) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block) open import Luau.Addr.ToString using (addrToString) open import Luau.Syntax.ToString using (exprToString) open import Luau.Var.ToString using (varToString) @@ -15,9 +15,10 @@ 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ᴮ (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/Properties/Step.agda b/prototyping/Properties/Step.agda index 620dc618..914c3468 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -4,8 +4,8 @@ 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.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) +open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst) +open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block; local; return) open import Luau.Substitution using (_[_/_]ᴮ) open import Luau.Value using (nil; addr; val; number) open import Properties.Remember using (remember; _,_) @@ -32,13 +32,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 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) -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