Added more bindings from Data.Aeson

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
+postulate KeyMap : Set → Set
-{-# COMPILE GHC Value = type Data.Aeson.Value #-}
+{-# 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 #-}

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 #-}

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 #-}

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