diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda index 4b576377..291d39b4 100644 --- a/prototyping/Examples.agda +++ b/prototyping/Examples.agda @@ -1,4 +1,5 @@ module Examples where import Examples.Syntax +import Examples.OpSem diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda new file mode 100644 index 00000000..e5a1f0cf --- /dev/null +++ b/prototyping/Examples/OpSem.agda @@ -0,0 +1,11 @@ +module Examples.OpSem where + +open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; local) +open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_end) +open import Luau.Heap using (emp) + +x = var "x" + +ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp +ex1 = local + diff --git a/prototyping/Examples/SmokeTestOutput.lua b/prototyping/Examples/SmokeTestOutput.lua new file mode 100644 index 00000000..b1b91e19 --- /dev/null +++ b/prototyping/Examples/SmokeTestOutput.lua @@ -0,0 +1,12 @@ +local function id(x) + return x +end +local function comp(f) + return function(g) + return function(x) + return f(g(x)) + end + end +end +local id2 = id(id) +local nil2 = id2(nil) diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda index d16dfebb..8af9bca8 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -2,7 +2,7 @@ module Examples.Syntax where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.String using (_++_) -open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; _∙; _∙_) +open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_) open import Luau.Syntax.ToString using (exprToString; blockToString) f = var "f" @@ -12,11 +12,11 @@ ex1 : exprToString(f $ x) ≡ "f(x)" ex1 = refl -ex2 : blockToString(return nil ∙) ≡ +ex2 : blockToString(return nil ∙ done) ≡ "return nil" ex2 = refl -ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡ +ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡ "local function f(x)\n" ++ " return x\n" ++ "end\n" ++ diff --git a/prototyping/FFI/Data/HaskellInt.agda b/prototyping/FFI/Data/HaskellInt.agda new file mode 100644 index 00000000..9ab0868e --- /dev/null +++ b/prototyping/FFI/Data/HaskellInt.agda @@ -0,0 +1,14 @@ +module FFI.Data.HaskellInt where + +open import Agda.Builtin.Int using (Int) + +{-# FOREIGN GHC import qualified Data.Int #-} + +postulate HaskellInt : Set +{-# COMPILE GHC HaskellInt = type Data.Int.Int #-} + +postulate + intToHaskellInt : Int → HaskellInt + haskellIntToInt : HaskellInt → Int +{-# COMPILE GHC intToHaskellInt = fromIntegral #-} +{-# COMPILE GHC haskellIntToInt = fromIntegral #-} diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 8ef8d63c..0b49c786 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -1,6 +1,9 @@ module FFI.Data.Vector where +open import Agda.Builtin.Int using (Int; pos; negsuc) +open import Agda.Builtin.Nat using (Nat) open import FFI.Data.Bool using (Bool; false; true) +open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt) open import FFI.Data.Maybe using (Maybe; just; nothing) {-# FOREIGN GHC import qualified Data.Vector #-} @@ -14,10 +17,16 @@ postulate null : ∀ {A} → (Vector A) → Bool unsafeHead : ∀ {A} → (Vector A) → A unsafeTail : ∀ {A} → (Vector A) → (Vector A) + hLength : ∀ {A} → (Vector A) → HaskellInt + hLookup : ∀ {A} → (Vector A) → HaskellInt → (Maybe A) + snoc : ∀ {A} → (Vector A) → A → (Vector A) {-# COMPILE GHC empty = \_ -> Data.Vector.empty #-} {-# COMPILE GHC null = \_ -> Data.Vector.null #-} {-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-} {-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-} +{-# COMPILE GHC hLength = \_ -> Data.Vector.length #-} +{-# COMPILE GHC hLookup = \_ -> (Data.Vector.!?) #-} +{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-} head : ∀ {A} → (Vector A) → (Maybe A) head vec with null vec @@ -29,3 +38,10 @@ tail vec with null vec tail vec | false = unsafeTail vec tail vec | true = empty +length : ∀ {A} → (Vector A) → Nat +length vec with haskellIntToInt(hLength vec) +length vec | pos n = n +length vec | negsuc n = 0 + +lookup : ∀ {A} → (Vector A) → Nat → Maybe A +lookup vec n = hLookup vec (intToHaskellInt (pos n)) diff --git a/prototyping/Luau/Addr.agda b/prototyping/Luau/Addr.agda new file mode 100644 index 00000000..f1497f23 --- /dev/null +++ b/prototyping/Luau/Addr.agda @@ -0,0 +1,21 @@ +module Luau.Addr where + +open import Agda.Builtin.Bool using (true; false) +open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Int using (Int; primShowInteger; pos) +open import Agda.Builtin.Nat using (Nat; _==_) +open import Agda.Builtin.String using (String) +open import Agda.Builtin.TrustMe using (primTrustMe) +open import Properties.Dec using (Dec; yes; no; ⊥) + +Addr : Set +Addr = Nat + +addrToString : Addr → String +addrToString a = primShowInteger (pos a) + +_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b) +a ≡ᴬ b with a == b +a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ᴬ b | true = yes primTrustMe + diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda new file mode 100644 index 00000000..56a09785 --- /dev/null +++ b/prototyping/Luau/Heap.agda @@ -0,0 +1,21 @@ +module Luau.Heap where + +open import FFI.Data.Maybe using (Maybe; just) +open import FFI.Data.Vector using (Vector; length; snoc) +open import Luau.Addr using (Addr) +open import Luau.Value using (Value) + +Heap = Vector Value + +data _≡_⊕_↦_ : Heap → Heap → Addr → Value → Set where + + defn : ∀ {H val} → + + ----------------------------------- + (snoc H val) ≡ H ⊕ (length H) ↦ val + +lookup : Heap → Addr → Maybe Value +lookup = FFI.Data.Vector.lookup + +emp : Heap +emp = FFI.Data.Vector.empty diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda new file mode 100644 index 00000000..2719918d --- /dev/null +++ b/prototyping/Luau/OpSem.agda @@ -0,0 +1,65 @@ +module Luau.OpSem where + +open import Agda.Builtin.Equality using (_≡_) +open import FFI.Data.Maybe using (just) +open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup) +open import Luau.Substitution using (_[_/_]ᴮ) +open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_end; local_←_; _∙_; done; function_⟨_⟩_end; return) +open import Luau.Value using (function⟨_⟩_end; addr; val) + +data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set +data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set + +data _⊢_⟶ᴱ_⊣_ where + + nil : ∀ {H} → + + ------------------- + H ⊢ nil ⟶ᴱ nil ⊣ H + + function : ∀ {H H′ a x B} → + + H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ B end) → + ------------------------------------------- + H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′ + + app : ∀ {H H′ M M′ N} → + + H ⊢ M ⟶ᴱ M′ ⊣ H′ → + ----------------------------- + H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′ + + beta : ∀ {H M a x B} → + + (lookup H a) ≡ just(function⟨ x ⟩ B end) → + ----------------------------------------------------- + H ⊢ (addr a $ M) ⟶ᴱ (block local x ← M ∙ B end) ⊣ H + + block : ∀ {H H′ B B′} → + + H ⊢ B ⟶ᴮ B′ ⊣ H′ → + ------------------------------------------ + H ⊢ (block B end) ⟶ᴱ (block B′ end) ⊣ H′ + + return : ∀ {H M B} → + + ---------------------------- + H ⊢ (block return M ∙ B end) ⟶ᴱ M ⊣ H + + done : ∀ {H} → + + --------------------------------- + H ⊢ (block done end) ⟶ᴱ nil ⊣ H + +data _⊢_⟶ᴮ_⊣_ where + + local : ∀ {H x v B} → + + ------------------------------------------------- + H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H + + function : ∀ {H H′ a f x B C} → + + H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ C end) → + -------------------------------------------------------------- + H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′ diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda new file mode 100644 index 00000000..a30b7f70 --- /dev/null +++ b/prototyping/Luau/Substitution.agda @@ -0,0 +1,30 @@ +module Luau.Substitution where + +open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_end; local_←_; _∙_; done; function_⟨_⟩_end; return) +open import Luau.Value using (Value; val) +open import Luau.Var using (Var; _≡ⱽ_) +open import Properties.Dec using (Dec; yes; no) + +_[_/_]ᴱ : Expr → Value → Var → Expr +_[_/_]ᴮ : Block → Value → Var → Block +var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr +_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block + +nil [ v / x ]ᴱ = nil +var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y) +addr a [ v / x ]ᴱ = addr a +(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ) +function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ y) end +block C end [ v / x ]ᴱ = block C [ v / x ]ᴮ end + +(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f)) +(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y)) +(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ) +done [ v / x ]ᴮ = done + +var y [ v / x ]ᴱwhenever yes p = val v +var y [ v / x ]ᴱwhenever no p = var y + +B [ v / x ]ᴮunless yes p = B +B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ + diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index c1d9c951..eed15b65 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -1,27 +1,17 @@ module Luau.Syntax where -open import Agda.Builtin.String using (String) +open import Luau.Var using (Var) +open import Luau.Addr using (Addr) infixr 5 _∙_ -data Type : Set where - nil : Type - _⇒_ : Type → Type → Type - none : Type - any : Type - _∪_ : Type → Type → Type - _∩_ : Type → Type → Type - -Var : Set -Var = String - data Block : Set data Stat : Set data Expr : Set data Block where _∙_ : Stat → Block → Block - _∙ : Stat → Block + done : Block data Stat where function_⟨_⟩_end : Var → Var → Block → Stat @@ -31,5 +21,7 @@ data Stat where data Expr where nil : Expr var : Var → Expr + addr : Addr → Expr _$_ : Expr → Expr → Expr function⟨_⟩_end : Var → Block → Expr + block_end : Block → Expr diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 36432118..0a4164fb 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 (Type; Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; _∙; _∙_) +open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_) open import Agda.Builtin.List using (List; _∷_; []) @@ -117,11 +117,9 @@ blockFromJSON (object obj) | nothing | _ = Left "AstStatBlock missing type" blockFromJSON _ = Left "AstBlock not an array or AstStatBlock object" blockFromArray arr with head arr -blockFromArray arr | nothing = Left "Block should be a non-empty array" +blockFromArray arr | nothing = Right done blockFromArray arr | just value with statFromJSON value blockFromArray arr | just value | Left err = Left err -blockFromArray arr | just value | Right S with null (tail arr) -blockFromArray arr | just value | Right S | true = Right (S ∙) -blockFromArray arr | just value | Right S | false with blockFromArray(tail arr) -blockFromArray arr | just value | Right S | false | Left err = Left (err) -blockFromArray arr | just value | Right S | false | Right B = Right (S ∙ B) +blockFromArray arr | just value | Right S with blockFromArray(tail arr) +blockFromArray arr | just value | Right S | Left err = Left (err) +blockFromArray arr | just value | Right S | Right B = Right (S ∙ B) diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 87876565..59a15c64 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -1,8 +1,9 @@ module Luau.Syntax.ToString where -open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; _∙) - +open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_end) open import FFI.Data.String using (String; _++_) +open import Luau.Addr using (addrToString) +open import Luau.Var using (varToString) exprToString′ : String → Expr → String statToString′ : String → Stat → String @@ -10,14 +11,20 @@ blockToString′ : String → Block → String exprToString′ lb nil = "nil" +exprToString′ lb (addr a) = + addrToString(a) exprToString′ lb (var x) = - x + varToString(x) exprToString′ lb (M $ N) = (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")" exprToString′ lb (function⟨ x ⟩ B end) = "function(" ++ x ++ ")" ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end" +exprToString′ lb (block B end) = + "(function()" ++ lb ++ + " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ + "end)()" statToString′ lb (function f ⟨ x ⟩ B end) = "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++ @@ -28,8 +35,9 @@ statToString′ lb (local x ← M) = statToString′ lb (return M) = "return " ++ (exprToString′ lb M) +blockToString′ lb (S ∙ done) = statToString′ lb S blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B -blockToString′ lb (S ∙) = statToString′ lb S +blockToString′ lb (done) = "" exprToString : Expr → String exprToString = exprToString′ "\n" diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda new file mode 100644 index 00000000..8da3a985 --- /dev/null +++ b/prototyping/Luau/Type.agda @@ -0,0 +1,10 @@ +module Luau.Type where + +data Type : Set where + nil : Type + _⇒_ : Type → Type → Type + none : Type + any : Type + _∪_ : Type → Type → Type + _∩_ : Type → Type → Type + diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda new file mode 100644 index 00000000..a9e6d124 --- /dev/null +++ b/prototyping/Luau/Value.agda @@ -0,0 +1,16 @@ +module Luau.Value where + +open import Luau.Addr using (Addr) +open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end) +open import Luau.Var using (Var) + +data Value : Set where + nil : Value + addr : Addr → Value + function⟨_⟩_end : Var → Block → Value + +val : Value → Expr +val nil = nil +val (addr a) = addr a +val (function⟨ x ⟩ B end) = function⟨ x ⟩ B end + diff --git a/prototyping/Luau/Var.agda b/prototyping/Luau/Var.agda new file mode 100644 index 00000000..03d37496 --- /dev/null +++ b/prototyping/Luau/Var.agda @@ -0,0 +1,19 @@ +module Luau.Var where + +open import Agda.Builtin.Bool using (true; false) +open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.String using (String; primStringEquality) +open import Agda.Builtin.TrustMe using (primTrustMe) +open import Properties.Dec using (Dec; yes; no; ⊥) + +Var : Set +Var = String + +varToString : Var → String +varToString x = x + +_≡ⱽ_ : (a b : Var) → Dec (a ≡ b) +a ≡ⱽ b with primStringEquality a b +a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ⱽ b | true = yes primTrustMe + diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda new file mode 100644 index 00000000..a3c685d1 --- /dev/null +++ b/prototyping/Properties.agda @@ -0,0 +1,3 @@ +module Properties where + +import Properties.Dec diff --git a/prototyping/Properties/Dec.agda b/prototyping/Properties/Dec.agda new file mode 100644 index 00000000..d89fd754 --- /dev/null +++ b/prototyping/Properties/Dec.agda @@ -0,0 +1,8 @@ +module Properties.Dec where + +data ⊥ : Set where + +data Dec(A : Set) : Set where + yes : A → Dec A + no : (A → ⊥) → Dec A +