WIP

prototyping/Interpreter.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module Interpreter where
 
 open import Agda.Builtin.IO using (IO)

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) →
-    -----------------------------------------------------
+    N ≡ val V →
-    H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
+    -----------------------------------------------------------------------------
+    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} →
   

prototyping/Luau/Run.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module Luau.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)

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

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ᴱ (app₁ E) = errToStringᴱ E
-errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
+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"

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

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 : ∀ {a} → FunDec a → VarDec a
-fun (f ⟨ x ⟩∈ T) = f
+fun (f ⟨ x ⟩∈ T) = (var f ∈ T)
-fun (f ⟨ x ⟩) = f
+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
 

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)

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 ++

prototyping/PrettyPrinter.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module PrettyPrinter where
 
 open import Agda.Builtin.IO using (IO)

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.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁; 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.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 (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
-stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
+stepᴱ H (M $ N) | value V p with stepᴱ H N
-stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
+stepᴱ H (M $ N) | value V p | step H′ N′ D = step H′ (M $ N′) (app₂ p D)
-stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
+stepᴱ H (nil $ _) | value nil refl | value W refl = error NilIsNotAFunction
-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 (addr a $ N) | value (addr a) refl | value W q with remember (H [ a ])
-stepᴱ H (M $ N) | error E = error (app E)
+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

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.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; 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.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) with preservationᴱ s
-preservationᴱ (app s) | ok p = ok (cong tgt p)
+preservationᴱ (app₁ s) | ok p = ok (cong tgt p)
-preservationᴱ (app s) | warning W = warning (app₁ W)
+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₂ 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) 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) | 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₀ 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′) with reflectᴱ s W′
-reflectᴱ (app s) (app₁ W′) | heap W = heap 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 W = expr (app₁ W)
-reflectᴱ (app s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (redn-⊑ s) 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ᴱ (app₂ p s) W′ = ?
-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 refl) (block (var f ∈ U) W′) = ? -- 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)) = heap (addr a q (function₁ f W))
 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′) with reflectᴴᴱ s (heap W′)
-reflectᴴᴱ (app s) (heap W′) | heap W = heap W
+reflectᴴᴱ (app₁ s) (heap W′) | heap W = heap W
-reflectᴴᴱ (app s) (heap W′) | expr W = expr (app₁ W)
+reflectᴴᴱ (app₁ s) (heap W′) | expr W = expr (app₁ W)
-reflectᴴᴱ (beta p) (heap W′) = heap 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)