From dbbe6788f53a6ce32c9715d1aa39f86e15ed3b44 Mon Sep 17 00:00:00 2001
From: "ajeffrey@roblox.com" <ajeffrey@roblox.com>
Date: Thu, 3 Feb 2022 14:49:33 -0600
Subject: [PATCH] Added more bindings from Data.Aeson

---
 prototyping/FFI/Data/Aeson.agda      | 22 ++++++++++++++++++++--
 prototyping/FFI/Data/Scientific.agda |  6 ++++++
 prototyping/FFI/Data/Vector.agda     |  7 +++++++
 prototyping/README.md                |  2 +-
 4 files changed, 34 insertions(+), 3 deletions(-)
 create mode 100644 prototyping/FFI/Data/Scientific.agda
 create mode 100644 prototyping/FFI/Data/Vector.agda

diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda
index 12211102..62d6b4b6 100644
--- a/prototyping/FFI/Data/Aeson.agda
+++ b/prototyping/FFI/Data/Aeson.agda
@@ -1,16 +1,34 @@
 module FFI.Data.Aeson where
 
+open import Agda.Builtin.Bool using (Bool)
 open import Agda.Builtin.String using (String)
 
 open import FFI.Data.ByteString using (ByteString)
 open import FFI.Data.HaskellString using (HaskellString; pack)
 open import FFI.Data.Maybe using (Maybe)
 open import FFI.Data.Either using (Either; mapLeft)
+open import FFI.Data.Scientific using (Scientific)
+open import FFI.Data.Vector using (Vector)
 
 {-# FOREIGN GHC import qualified Data.Aeson #-}
+{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}
 
-postulate Value : Set
-{-# COMPILE GHC Value = type Data.Aeson.Value #-}
+postulate KeyMap : Set → Set
+{-# POLARITY KeyMap ++ #-}
+{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
+
+data Value : Set where
+  object : KeyMap Value → Value
+  array : Vector Value → Value
+  string : String → Value
+  number : Scientific → Value
+  bool : Bool → Value
+  null : Value
+
+Object = KeyMap Value
+Array = Vector Value
+
+{-# COMPILE GHC Value = data Data.Aeson.Value (Data.Aeson.Object|Data.Aeson.Array|Data.Aeson.String|Data.Aeson.Number|Data.Aeson.Bool|Data.Aeson.Null) #-}
 
 postulate decode : ByteString → Maybe Value
 {-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
diff --git a/prototyping/FFI/Data/Scientific.agda b/prototyping/FFI/Data/Scientific.agda
new file mode 100644
index 00000000..8a5be39e
--- /dev/null
+++ b/prototyping/FFI/Data/Scientific.agda
@@ -0,0 +1,6 @@
+module FFI.Data.Scientific where
+
+{-# FOREIGN GHC import qualified Data.Scientific #-}
+
+postulate Scientific : Set
+{-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}
diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda
new file mode 100644
index 00000000..a2252c96
--- /dev/null
+++ b/prototyping/FFI/Data/Vector.agda
@@ -0,0 +1,7 @@
+module FFI.Data.Vector where
+
+{-# FOREIGN GHC import qualified Data.Vector #-}
+
+postulate Vector : Set → Set
+{-# POLARITY Vector ++ #-}
+{-# COMPILE GHC Vector = type Data.Vector.Vector #-}
diff --git a/prototyping/README.md b/prototyping/README.md
index bf7b05ab..45722197 100644
--- a/prototyping/README.md
+++ b/prototyping/README.md
@@ -11,7 +11,7 @@ First install Haskell and Agda.
 Install dependencies:
 ```
   cabal update
-  cabal install --lib aeson
+  cabal install --lib aeson scientific vector
 ```
 
 Then compile