First cut reading JSON into Agda

prototyping/.gitignore

@@ -0,0 +1,4 @@
+*~
+*.agdai
+Main
+MAlonzo

prototyping/FFI/Data/Aeson.agda

@@ -0,0 +1,19 @@
+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.Maybe using (Maybe)
+open import FFI.Data.Either using (Either)
+
+{-# FOREIGN GHC import qualified Data.Aeson #-}
+
+postulate Value : Set
+{-# COMPILE GHC Value = type Data.Aeson.Value #-}
+
+postulate decode : ByteString → Maybe Value
+{-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
+
+postulate eitherDecode : ByteString → Either HaskellString Value
+{-# COMPILE GHC eitherDecode = Data.Aeson.eitherDecodeStrict #-}

prototyping/FFI/Data/ByteString.agda

@@ -0,0 +1,7 @@
+module FFI.Data.ByteString where
+
+{-# FOREIGN GHC import qualified Data.ByteString #-}
+
+postulate ByteString : Set
+{-# COMPILE GHC ByteString = type Data.ByteString.ByteString #-}
+

prototyping/FFI/Data/Either.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Either where
+
+{-# FOREIGN GHC import qualified Data.Either #-}
+
+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) #-}

prototyping/FFI/Data/HaskellString.agda

@@ -0,0 +1,16 @@
+module FFI.Data.HaskellString where
+
+open import Agda.Builtin.String using (String)
+
+{-# FOREIGN GHC import qualified Data.String #-}
+{-# FOREIGN GHC import qualified Data.Text #-}
+
+postulate HaskellString : Set
+{-# COMPILE GHC HaskellString = type Data.String.String #-}
+
+postulate pack : HaskellString → String
+{-# COMPILE GHC pack = Data.Text.pack #-}
+
+postulate unpack : String → HaskellString
+{-# COMPILE GHC unpack = Data.Text.unpack #-}
+

prototyping/FFI/Data/List.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Maybe where
+
+{-# FOREIGN GHC import qualified Data.Maybe #-}
+
+data Maybe (A : Set) : Set where
+  Nothing : Maybe A
+  Just : A → Maybe A
+{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}

prototyping/FFI/Data/Maybe.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Maybe where
+
+{-# FOREIGN GHC import qualified Data.Maybe #-}
+
+data Maybe (A : Set) : Set where
+  Nothing : Maybe A
+  Just : A → Maybe A
+{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}

prototyping/FFI/Data/Text/Encoding.agda

@@ -0,0 +1,10 @@
+module FFI.Data.Text.Encoding where
+
+open import Agda.Builtin.String using (String)
+
+open import FFI.Data.ByteString using (ByteString)
+
+{-# FOREIGN GHC import qualified Data.Text.Encoding #-}
+
+postulate encodeUtf8 : String → ByteString
+{-# COMPILE GHC encodeUtf8 = Data.Text.Encoding.encodeUtf8 #-}

prototyping/FFI/IO.agda

@@ -0,0 +1,22 @@
+module FFI.IO where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+
+open import FFI.Data.HaskellString using (HaskellString)
+
+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
+
+{-# COMPILE GHC return = \_ _ -> return    #-}
+{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
+
+postulate getContents : IO HaskellString
+{-# COMPILE GHC getContents = getContents #-}
+
+postulate putStrLn : HaskellString → IO ⊤
+{-# COMPILE GHC putStrLn = putStrLn #-}
+

prototyping/Main.agda

@@ -0,0 +1,19 @@
+module Main where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+
+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")
+
+main : IO ⊤
+main = getContents >>= main2
+

prototyping/README.md

@@ -0,0 +1,25 @@
+# Prototyping Luau
+
+An experimental prototyping system for the Luau type system. This is
+intended to allow core language features to be tested quickly, without
+having to interact with all the features of production Lua.
+
+## Building
+
+First install Haskell and Agda.
+
+Install dependencies:
+```
+  cabal update
+  cabal install --lib aeson
+```
+
+Then compile
+```
+  agda --compile Main.agda
+```
+
+and run!
+```
+  echo '{"some": "JSON"}' | ./Main
+```