Prototyping: numbers (#368)

Adds number support to the prototype. Binary operators are next.

prototyping/Examples/OpSem.agda

@@ -6,4 +6,3 @@ open import Luau.Heap using (∅)
 
 ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
 ex1 = subst
-

prototyping/Examples/Run.agda

@@ -3,8 +3,8 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number)
-open import Luau.Value using (nil)
+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)
 
@@ -13,3 +13,6 @@ import Agda.Builtin.Equality.Rewrite
 
 ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
 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

prototyping/FFI/Data/Scientific.agda

@@ -1,6 +1,21 @@
 module FFI.Data.Scientific where
 
+open import Agda.Builtin.Float using (Float)
+open import FFI.Data.String using (String)
+open import FFI.Data.HaskellString using (HaskellString; pack; unpack)
+
 {-# FOREIGN GHC import qualified Data.Scientific #-}
+{-# FOREIGN GHC import qualified Text.Show #-}
 
 postulate Scientific : Set
 {-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}
+
+postulate
+  showHaskell : Scientific → HaskellString
+  toFloat : Scientific → Float
+
+{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
+{-# COMPILE GHC toFloat = \x -> Data.Scientific.toRealFloat x #-}
+
+show : Scientific → String
+show x = pack (showHaskell x)

prototyping/Interpreter.agda

@@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-

prototyping/Luau/RuntimeError.agda

@@ -3,13 +3,15 @@ module Luau.RuntimeError where
 open import Agda.Builtin.Equality using (_≡_)
 open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
+open import FFI.Data.String using (String)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number)
 
 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)
   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)
@@ -18,4 +20,3 @@ data RuntimeErrorᴱ H where
 data RuntimeErrorᴮ H where
   local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
   return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
-

prototyping/Luau/RuntimeError/ToString.agda

@@ -1,15 +1,18 @@
 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; UnboundVariable; SEGV; app; block)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block)
 open import Luau.Addr.ToString using (addrToString)
+open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
-open import Luau.Syntax using (name)
+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
@@ -17,3 +20,4 @@ errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ v
 
 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

@@ -1,6 +1,6 @@
 module Luau.Substitution where
 
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -13,6 +13,7 @@ _[_/_]ᴮunless_ : ∀ {a P} → Block a → 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
+(number y) [ v / x ]ᴱ = number y
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
 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
@@ -27,4 +28,3 @@ 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 ]ᴮ
-

prototyping/Luau/Syntax.agda

@@ -1,6 +1,7 @@
 module Luau.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float)
 open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
@@ -52,4 +53,4 @@ data Expr a where
   _$_ : Expr a → Expr a → Expr a
   function_is_end : FunDec a → Block a → Expr a
   block_is_end : Var → Block a → Expr a
-
+  number : Float → Expr a

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
@@ -9,6 +9,7 @@ open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; f
 open import FFI.Data.Bool using (true; false)
 open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; nothing; just)
+open import FFI.Data.Scientific using (toFloat)
 open import FFI.Data.String using (String; _++_)
 open import FFI.Data.Vector using (head; tail; null; empty)
 
@@ -19,6 +20,7 @@ lokal = fromString "local"
 list = fromString "list"
 name = fromString "name"
 type = fromString "type"
+value = fromString "value"
 values = fromString "values"
 vars = fromString "vars"
 
@@ -83,6 +85,10 @@ exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
 exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
 exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
 exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
+exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
+exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
+exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
 exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
 exprFromObject obj | nothing = Left "AstExpr missing type"

prototyping/Luau/Syntax/ToString.agda

@@ -1,6 +1,7 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
+open import Agda.Builtin.Float using (primShowFloat)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -36,6 +37,7 @@ exprToString′ lb (block b is B end) =
   "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
+exprToString′ lb (number x) = primShowFloat x
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++

prototyping/Luau/Type.agda

@@ -7,6 +7,7 @@ data Type : Set where
   _⇒_ : Type → Type → Type
   none : Type
   any : Type
+  number : Type
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
@@ -15,6 +16,7 @@ src nil = none
 src (S ⇒ T) = S
 src none = none
 src any = any
+src number = none
 src (S ∪ T) = (src S) ∪ (src T)
 src (S ∩ T) = (src S) ∩ (src T)
 
@@ -23,6 +25,7 @@ tgt nil = none
 tgt (S ⇒ T) = T
 tgt none = none
 tgt any = any
+tgt number = none
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
 
@@ -40,4 +43,3 @@ normalizeOptional (S ∪ T) | S′         | nil        = optional S′
 normalizeOptional (S ∪ T) | nil        | T′         = optional T′
 normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
 normalizeOptional T = T
-

prototyping/Luau/Type/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Type.FromJSON where
 
-open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any)
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
@@ -41,6 +41,7 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
 typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
 typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
 
 typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o

prototyping/Luau/Type/ToString.agda

@@ -1,7 +1,7 @@
 module Luau.Type.ToString where
 
 open import FFI.Data.String using (String; _++_)
-open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
+open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)
 
 {-# TERMINATING #-}
 typeToString : Type → String
@@ -12,6 +12,7 @@ typeToString nil = "nil"
 typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
 typeToString none = "none"
 typeToString any = "any"
+typeToString number = "number"
 typeToString (S ∪ T) with normalizeOptional(S ∪ T)
 typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
 typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"

prototyping/Luau/Value.agda

@@ -1,15 +1,16 @@
 module Luau.Value where
 
+open import Agda.Builtin.Float using (Float)
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr)
+open import Luau.Syntax using (Block; Expr; nil; addr; number)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
+  number : Float → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
-
+val (number x) = number x
-

prototyping/Luau/Value/ToString.agda

@@ -1,10 +1,11 @@
 module Luau.Value.ToString where
 
 open import Agda.Builtin.String using (String)
-open import Luau.Value using (Value; nil; addr)
+open import Agda.Builtin.Float using (primShowFloat)
+open import Luau.Value using (Value; nil; addr; number)
 open import Luau.Addr.ToString using (addrToString)
 
 valueToString : Value → String
 valueToString nil = "nil"
 valueToString (addr a) = addrToString a
- 
+valueToString (number x) = primShowFloat x

prototyping/PrettyPrinter.agda

@@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-

prototyping/Properties/Step.agda

@@ -3,11 +3,11 @@ module Properties.Step where
 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.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; UnboundVariable; SEGV; app; block; local; return)
+open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Value using (nil; addr; val)
+open import Luau.Value using (nil; addr; val; number)
 open import Properties.Remember using (remember; _,_)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@@ -30,9 +30,11 @@ stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
 stepᴱ H nil = value nil refl
 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)

prototyping/Tests/PrettyPrinter/smoke_test/in.lua

@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f : number = 123
 return id2(nil2)

prototyping/Tests/PrettyPrinter/smoke_test/out.txt

@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f : number = 123.0
 return id2(nil2)