Added first cut syntax

prototyping/FFI/Data/Aeson.agda

@@ -3,9 +3,9 @@ module FFI.Data.Aeson where
 open import Agda.Builtin.String using (String)
 
 open import FFI.Data.ByteString using (ByteString)
-open import FFI.Data.HaskellString using (HaskellString)
+open import FFI.Data.HaskellString using (HaskellString; pack)
 open import FFI.Data.Maybe using (Maybe)
-open import FFI.Data.Either using (Either)
+open import FFI.Data.Either using (Either; mapLeft)
 
 {-# FOREIGN GHC import qualified Data.Aeson #-}
 
@@ -15,5 +15,9 @@ postulate Value : Set
 postulate decode : ByteString → Maybe Value
 {-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
 
-postulate eitherDecode : ByteString → Either HaskellString Value
-{-# COMPILE GHC eitherDecode = Data.Aeson.eitherDecodeStrict #-}
+postulate eitherHDecode : ByteString → Either HaskellString Value
+{-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}
+
+eitherDecode : ByteString → Either String Value
+eitherDecode bytes = mapLeft pack (eitherHDecode bytes)
+

prototyping/FFI/Data/Either.agda

@@ -6,3 +6,11 @@ data Either (A B : Set) : Set where
   Left : A → Either A B
   Right : B → Either A B
 {-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-}
+
+mapLeft : ∀ {A B C} → (A → B) → (Either A C) → (Either B C)
+mapLeft f (Left x) = Left (f x)
+mapLeft f (Right x) = Right x
+
+mapRight : ∀ {A B C} → (B → C) → (Either A B) → (Either A C)
+mapRight f (Left x) = Left x
+mapRight f (Right x) = Right (f x)

prototyping/FFI/IO.agda

@@ -2,21 +2,29 @@ module FFI.IO where
 
 open import Agda.Builtin.IO using (IO)
 open import Agda.Builtin.Unit using (⊤)
+open import Agda.Builtin.String using (String)
 
-open import FFI.Data.HaskellString using (HaskellString)
+open import FFI.Data.HaskellString using (HaskellString; pack ; unpack)
 
 infixl 1 _>>=_
 
 postulate
   return : ∀ {a} {A : Set a} → A → IO A
   _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
+  fmap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B
 
 {-# COMPILE GHC return = \_ _ -> return    #-}
 {-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
+{-# COMPILE GHC fmap  = \_ _ _ _ -> fmap #-}
 
-postulate getContents : IO HaskellString
-{-# COMPILE GHC getContents = getContents #-}
+postulate getHContents : IO HaskellString
+{-# COMPILE GHC getHContents = getContents #-}
 
-postulate putStrLn : HaskellString → IO ⊤
-{-# COMPILE GHC putStrLn = putStrLn #-}
+postulate putHStrLn : HaskellString → IO ⊤
+{-# COMPILE GHC putHStrLn = putStrLn #-}
 
+getContents : IO String
+getContents = fmap pack getHContents
+
+putStrLn : String → IO ⊤
+putStrLn txt = putHStrLn (unpack txt)

prototyping/Luau/Syntax.agda

@@ -0,0 +1,27 @@
+module Luau.Syntax where
+
+open import Agda.Builtin.String using (String)
+
+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 Expr : Set
+
+data Block where
+  function_⟨_⟩_end_ : Var → Block → Block → Block
+  local_←_∙_ : Var → Expr → Block → Block
+  return : Expr → Block
+
+data Expr where
+  nil : Expr
+  var : Var → Expr
+  _$_ : Expr → Expr → Expr

prototyping/Luau/Syntax/FromJSON.agda

@@ -0,0 +1,17 @@
+module Luau.Syntax.FromJSON where
+
+open import Luau.Syntax using (Type; Block; Expr; nil; return)
+
+open import Agda.Builtin.String using (String)
+
+open import FFI.Data.Aeson using (Value)
+open import FFI.Data.Either using (Either; Left; Right)
+
+exprFromJSON : Value → Either String Expr
+blockFromJSON : Value → Either String Block
+
+-- TODO: implement this!
+exprFromJSON v = Left "Not implemented yet"
+
+-- TODO: implement this!
+blockFromJSON v = Left "Not implemented yet"

prototyping/Main.agda

@@ -2,18 +2,29 @@ module Main where
 
 open import Agda.Builtin.IO using (IO)
 open import Agda.Builtin.Unit using (⊤)
+open import Agda.Builtin.String using (String) renaming (primStringAppend to _++_)
 
 open import FFI.IO using (getContents; putStrLn; _>>=_)
 open import FFI.Data.Aeson using (Value; eitherDecode)
 open import FFI.Data.Either using (Left; Right)
-open import FFI.Data.HaskellString using (HaskellString; pack; unpack)
 open import FFI.Data.Text.Encoding using (encodeUtf8)
 
-main2 : HaskellString → IO ⊤
-main2 txt with eitherDecode (encodeUtf8 (pack txt))
-main2 txt | (Left x) = putStrLn x
-main2 txt | (Right x) = putStrLn (unpack "OK")
+open import Luau.Syntax using (Block)
+open import Luau.Syntax.FromJSON using (blockFromJSON)
+
+runBlock : Block → IO ⊤
+runBlock block = putStrLn "OK"
+
+runJSON : Value → IO ⊤
+runJSON value with blockFromJSON(value)
+runJSON value | (Left err) = putStrLn ("Luau error: " ++ err)
+runJSON value | (Right block) = runBlock block
+
+runString : String → IO ⊤
+runString txt with eitherDecode (encodeUtf8 txt)
+runString txt | (Left err) = putStrLn ("JSON error: " ++ err)
+runString txt | (Right value) = runJSON value
 
 main : IO ⊤
-main = getContents >>= main2
+main = getContents >>= runString