diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index 3ec5b8d1..69ff8e0b 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Interpreter where open import Agda.Builtin.IO using (IO) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index e41102d8..f0e39037 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -21,17 +21,25 @@ 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′ M N N′ V} → + + (M ≡ val V) → + H ⊢ N ⟶ᴱ N′ ⊣ H′ → + ----------------------------- + H ⊢ (M $ N) ⟶ᴱ (M $ N′) ⊣ H′ + + beta : ∀ {H a N 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 + N ≡ val V → + ----------------------------------------------------------------------------- + H ⊢ (addr a $ N) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H block : ∀ {H H′ B B′ b} → @@ -67,7 +75,7 @@ data _⊢_⟶ᴮ_⊣_ where H′ ≡ H ⊕ a ↦ (function F is C end) → -------------------------------------------------------------- - H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′ + H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) ⊣ H′ return : ∀ {H H′ M M′ B} → diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda index d84f75de..fc60a1a4 100644 --- a/prototyping/Luau/Run.agda +++ b/prototyping/Luau/Run.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.Run where open import Agda.Builtin.Equality using (_≡_; refl) diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 0ec8b4e2..0c4b11ca 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -15,7 +15,8 @@ data RuntimeErrorᴱ H where NilIsNotAFunction : ∀ {V} → RuntimeErrorᴱ H (nil $ 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 e8287157..c20d52e8 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -1,7 +1,9 @@ +{-# OPTIONS --rewriting #-} + module Luau.RuntimeError.ToString where open import FFI.Data.String using (String; _++_) -open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block) open import Luau.Addr.ToString using (addrToString) open import Luau.Var.ToString using (varToString) open import Luau.Syntax using (name) @@ -9,11 +11,12 @@ 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ᴱ (NilIsNotAFunction) = "nil 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ᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b +errToStringᴱ (app₁ E) = errToStringᴱ E +errToStringᴱ (app₂ E) = errToStringᴱ E +errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString (name b) 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/Substitution.agda b/prototyping/Luau/Substitution.agda index b956aeae..ffcc6fe1 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -17,7 +17,7 @@ addr a [ v / x ]ᴱ = addr a function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end -(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F)) +(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name(fun F))) (local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y)) (return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ) done [ v / x ]ᴮ = done diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 1edfa4d3..9361de69 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -23,9 +23,9 @@ data FunDec : Annotated → Set where _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a _⟨_⟩ : Var → VarDec maybe → FunDec maybe -fun : ∀ {a} → FunDec a → Var -fun (f ⟨ x ⟩∈ T) = f -fun (f ⟨ x ⟩) = f +fun : ∀ {a} → FunDec a → VarDec a +fun (f ⟨ x ⟩∈ T) = (var f ∈ T) +fun (f ⟨ x ⟩) = (var f) arg : ∀ {a} → FunDec a → VarDec a arg (f ⟨ x ⟩∈ T) = x @@ -50,5 +50,5 @@ data Expr a where addr : Addr → Expr a _$_ : Expr a → Expr a → Expr a function_is_end : FunDec a → Block a → Expr a - block_is_end : Var → Block a → Expr a + block_is_end : VarDec a → Block a → Expr a diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index b081d156..350039b5 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.Syntax.FromJSON where open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe) diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 8ab5eece..e9461c99 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -30,10 +30,14 @@ exprToString′ lb (function F is B end) = "function " ++ funDecToString F ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end" -exprToString′ lb (block b is B end) = +exprToString′ lb (block (var b) is B end) = "(function " ++ b ++ "()" ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end)()" +exprToString′ lb (block (var b ∈ T) is B end) = + "(function " ++ b ++ "(): " ++ typeToString(T) ++ lb ++ + " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ + "end)()" statToString′ lb (function F is B end) = "local function " ++ funDecToString F ++ lb ++ diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda index 4a6c7dd6..1ea74b68 100644 --- a/prototyping/PrettyPrinter.agda +++ b/prototyping/PrettyPrinter.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module PrettyPrinter where open import Agda.Builtin.IO using (IO) diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index cf7a5ae7..db4b3507 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -6,8 +6,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) -open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; 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; UnboundVariable; SEGV; app₁; app₂; block; local; return) open import Luau.Substitution using (_[_/_]ᴮ) open import Luau.Value using (nil; addr; val) open import Properties.Remember using (remember; _,_) @@ -33,12 +33,15 @@ stepᴱ H nil = value nil refl stepᴱ H (var x) = error (UnboundVariable x) stepᴱ H (addr a) = value (addr a) 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 (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 (M $ N) | value V p with stepᴱ H N +stepᴱ H (M $ N) | value V p | step H′ N′ D = step H′ (M $ N′) (app₂ p D) +stepᴱ H (nil $ _) | value nil refl | value W refl = error NilIsNotAFunction +stepᴱ H (addr a $ N) | value (addr a) refl | value W q with remember (H [ a ]) +stepᴱ H (addr a $ N) | value (addr a) refl | value W q | (nothing , p) = error (app₁ (SEGV a p)) +stepᴱ H (addr a $ N) | value (addr a) refl | value W q | (just(function F is B end) , p) = step H (block fun F is (B [ W / name(arg F) ]ᴮ) end) (beta p q) +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 refl) @@ -48,7 +51,7 @@ 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 (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) +stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / name(fun F) ]ᴮ) (function p) stepᴮ H (local x ← M ∙ B) with stepᴱ H M stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D) stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index af608df1..2b282cb0 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -21,8 +21,8 @@ open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) open import Properties.Dec using (Dec; yes; no) open import Properties.Contradiction using (CONTRADICTION) open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ) -open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst; refl; step) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) +open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; refl; step) +open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block; local; return) src = Luau.Type.src strict @@ -91,10 +91,11 @@ preservationᴱ : ∀ {H H′ M M′ Γ} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → preservationᴮ : ∀ {H H′ B B′ Γ} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B′) preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = ok refl -preservationᴱ (app s) with preservationᴱ s -preservationᴱ (app s) | ok p = ok (cong tgt p) -preservationᴱ (app s) | warning W = warning (app₁ W) -preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ T} p) = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!!}) +preservationᴱ (app₁ s) with preservationᴱ s +preservationᴱ (app₁ s) | ok p = ok (cong tgt p) +preservationᴱ (app₁ s) | warning W = warning (app₁ W) +preservationᴱ (app₂ p s) = ? +preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ T} p q) = ok (trans (cong tgt (cong orBot (cong typeOfᴹᴼ p))) {!!}) preservationᴱ (block s) with preservationᴮ s preservationᴱ (block s) | ok p = ok p preservationᴱ (block {b = b} s) | warning W = warning (block b W) @@ -201,17 +202,16 @@ reflect-weakeningᴼ h (function₁ f W′) = function₁ f (reflect-weakening reflectᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) reflectᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) -reflectᴱ (app s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (redn-⊑ s) -reflectᴱ (app s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′))) -reflectᴱ (app s) (app₀ p) | warning W | _ = expr (app₁ W) -reflectᴱ (app s) (app₀ p) | _ | warning W = expr (app₂ W) -reflectᴱ (app s) (app₁ W′) with reflectᴱ s W′ -reflectᴱ (app s) (app₁ W′) | heap W = heap W -reflectᴱ (app s) (app₁ W′) | expr W = expr (app₁ W) -reflectᴱ (app s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (redn-⊑ s) W′)) -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₀ p)) = expr (app₀ (λ r → p (trans (cong src (cong orBot (cong typeOfᴹᴼ (sym q)))) r))) -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = expr (app₂ W) -reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₂ W)) = heap (addr a q (function₁ f W)) +reflectᴱ (app₁ s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (redn-⊑ s) +reflectᴱ (app₁ s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′))) +reflectᴱ (app₁ s) (app₀ p) | warning W | _ = expr (app₁ W) +reflectᴱ (app₁ s) (app₀ p) | _ | warning W = expr (app₂ W) +reflectᴱ (app₁ s) (app₁ W′) with reflectᴱ s W′ +reflectᴱ (app₁ s) (app₁ W′) | heap W = heap W +reflectᴱ (app₁ s) (app₁ W′) | expr W = expr (app₁ W) +reflectᴱ (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (redn-⊑ s) W′)) +reflectᴱ (app₂ p s) W′ = ? +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q refl) (block (var f ∈ U) W′) = ? -- expr (app₀ (λ r → p (trans (cong src (cong orBot (cong typeOfᴹᴼ (sym q)))) r))) reflectᴱ (block s) (block b W′) with reflectᴮ s W′ reflectᴱ (block s) (block b W′) | heap W = heap W reflectᴱ (block s) (block b W′) | block W = expr (block b W) @@ -246,10 +246,13 @@ reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = expr (function₁ f W) reflectᴴᴱ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = expr (function₁ f (reflect-weakeningᴮ (snoc refl defn) W′)) reflectᴴᴱ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc refl p) W′)) -reflectᴴᴱ (app s) (heap W′) with reflectᴴᴱ s (heap W′) -reflectᴴᴱ (app s) (heap W′) | heap W = heap W -reflectᴴᴱ (app s) (heap W′) | expr W = expr (app₁ W) -reflectᴴᴱ (beta p) (heap W′) = heap W′ +reflectᴴᴱ (app₁ s) (heap W′) with reflectᴴᴱ s (heap W′) +reflectᴴᴱ (app₁ s) (heap W′) | heap W = heap W +reflectᴴᴱ (app₁ s) (heap W′) | expr W = expr (app₁ W) +reflectᴴᴱ (app₂ p s) (heap W′) with reflectᴴᴱ s (heap W′) +reflectᴴᴱ (app₂ p s) (heap W′) | heap W = heap W +reflectᴴᴱ (app₂ p s) (heap W′) | expr W = expr (app₂ W) +reflectᴴᴱ (beta p q) (heap W′) = heap W′ reflectᴴᴱ (block s) (heap W′) with reflectᴴᴮ s (heap W′) reflectᴴᴱ (block s) (heap W′) | heap W = heap W reflectᴴᴱ (block s) (heap W′) | block W = expr (block _ W) @@ -283,7 +286,8 @@ runtimeWarningᴱ (NilIsNotAFunction) | ok p = app₀ p runtimeWarningᴱ (NilIsNotAFunction) | warning W = app₂ W runtimeWarningᴱ (UnboundVariable x) = UnboundVariable x refl runtimeWarningᴱ (SEGV a p) = UnallocatedAddress a p -runtimeWarningᴱ (app err) = app₁ (runtimeWarningᴱ err) +runtimeWarningᴱ (app₁ err) = app₁ (runtimeWarningᴱ err) +runtimeWarningᴱ (app₂ err) = app₂ (runtimeWarningᴱ err) runtimeWarningᴱ (block b err) = block b (runtimeWarningᴮ err) runtimeWarningᴮ (local (var x ∈ T) err) = local₁ (runtimeWarningᴱ err)