Added pretty printer

prototyping/FFI/Data/Aeson.agda

@@ -11,11 +11,21 @@ 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.Key #-}
 {-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}
 
-postulate KeyMap : Set → Set
+postulate
+  KeyMap : Set → Set
+  Key : Set
+  fromString : String → Key
+  toString : Key → String
+  lookup : ∀ {A} → Key -> KeyMap A -> Maybe A
 {-# POLARITY KeyMap ++ #-}
 {-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
+{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
+{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
+{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
+{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}
 
 data Value : Set where
   object : KeyMap Value → Value
@@ -24,16 +34,15 @@ data Value : Set where
   number : Scientific → Value
   bool : Bool → Value
   null : 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) #-}
 
 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
-postulate decode : ByteString → Maybe Value
+  eitherHDecode : ByteString → Either HaskellString Value
 {-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
-
-postulate eitherHDecode : ByteString → Either HaskellString Value
 {-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}
 
 eitherDecode : ByteString → Either String Value

prototyping/FFI/Data/Bool.agda

@@ -0,0 +1,8 @@
+module FFI.Data.Bool where
+
+{-# FOREIGN GHC import qualified Data.Bool #-}
+
+data Bool : Set where
+  false : Bool
+  true : Bool
+{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.True|Data.Bool.False) #-}

prototyping/FFI/Data/Maybe.agda

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

prototyping/FFI/Data/String.agda

@@ -0,0 +1,8 @@
+module FFI.Data.String where
+
+import Agda.Builtin.String
+
+String = Agda.Builtin.String.String
+
+infixr 5 _++_
+_++_ = Agda.Builtin.String.primStringAppend

prototyping/FFI/Data/Vector.agda

@@ -1,7 +1,26 @@
 module FFI.Data.Vector where
 
+open import FFI.Data.Bool using (Bool; false; true)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
 {-# FOREIGN GHC import qualified Data.Vector #-}
 
 postulate Vector : Set → Set
 {-# POLARITY Vector ++ #-}
 {-# COMPILE GHC Vector = type Data.Vector.Vector #-}
+
+postulate
+  empty : ∀ {A} → (Vector A)
+  null : ∀ {A} → (Vector A) → Bool
+  unsafeHead : ∀ {A} → (Vector A) → A
+  tail : ∀ {A} → (Vector A) → (Vector A)
+{-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
+{-# COMPILE GHC null = \_ -> Data.Vector.null #-}
+{-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
+{-# COMPILE GHC tail = \_ -> Data.Vector.tail #-}
+
+head : ∀ {A} → (Vector A) → (Maybe A)
+head vec with null vec
+head vec | false = just (unsafeHead vec)
+head vec | true = nothing
+

prototyping/Luau/Syntax.agda

@@ -17,7 +17,7 @@ data Block : Set
 data Expr : Set
 
 data Block where
-  function_⟨_⟩_end_ : Var → Block → Block → Block
+  function_⟨_⟩_end_ : Var → Var → Block → Block → Block
   local_←_∙_ : Var → Expr → Block → Block
   return : Expr → Block
 

prototyping/Luau/Syntax/FromJSON.agda

@@ -4,14 +4,40 @@ 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.Aeson using (Value; Array; Object; object; array; fromString; lookup)
 open import FFI.Data.Either using (Either; Left; Right)
+open import FFI.Data.Maybe using (nothing; just)
+open import FFI.Data.Vector using (head; empty)
+
+AstExprConstantNil = fromString "AstExprConstantNil"
+AstStatReturn = fromString "AstStatReturn"
 
 exprFromJSON : Value → Either String Expr
+exprFromObject : Object → Either String Expr
 blockFromJSON : Value → Either String Block
+blockFromArray : Array → Either String Block
+blockFromObject : Object → Array → Either String Block
+
+exprFromJSON (object obj) = exprFromObject obj
+exprFromJSON val = Left "Expr should be an object"
+
+exprFromObject obj with lookup AstExprConstantNil obj
+exprFromObject obj | just val = Right nil
+exprFromObject obj | nothing = Left "Unsupported Expr"
+
+blockFromJSON (object obj) = blockFromObject obj empty
+blockFromJSON (array arr) = blockFromArray arr
+blockFromJSON _ = Left "Block should be an object or array"
+
+blockFromArray arr with head arr
+blockFromArray arr | nothing = Right (return nil)
+blockFromArray arr | just (object obj) = blockFromObject obj arr
+blockFromArray arr | just (x) = Left "Stat should be an object"
+
+blockFromObject obj arr with lookup AstStatReturn obj
+blockFromObject obj arr | just val with exprFromJSON val
+blockFromObject obj arr | just val | Left err = Left err
+blockFromObject obj arr | just val | Right exp = Right (return exp)
+blockFromObject obj arr | nothing = Left "Unsupported Stat"
 
--- TODO: implement this!
-exprFromJSON v = Left "Not implemented yet"
 
--- TODO: implement this!
-blockFromJSON v = Left "Not implemented yet"

prototyping/Luau/Syntax/ToString.agda

@@ -0,0 +1,28 @@
+module Luau.Syntax.ToString where
+
+open import Luau.Syntax using (Type; Block; Expr; nil; var; _$_; return ; function_⟨_⟩_end_ ; local_←_∙_)
+
+open import FFI.Data.String using (String; _++_)
+
+exprToString : Expr → String
+exprToString nil = "nil"
+exprToString (var x) = x
+exprToString (M $ N) = (exprToString M) ++ "(" ++ (exprToString N) ++ ")"
+
+blockToString′ : String → Block → String
+blockToString′ lb (function f ⟨ x ⟩ B end C) =
+  "function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  blockToString′ lb C
+blockToString′ lb (local x ← M ∙ B) =
+  "local " ++ x ++ " = " ++ (exprToString M) ++ lb ++
+  (blockToString′ lb B)
+blockToString′ lb (return M) =
+  "return " ++ (exprToString M)
+
+blockToString : Block → String
+blockToString = blockToString′ "\n"
+
+
+
+

prototyping/Main.agda

@@ -2,18 +2,19 @@ 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.String using (String; _++_)
 open import FFI.Data.Text.Encoding using (encodeUtf8)
 
 open import Luau.Syntax using (Block)
 open import Luau.Syntax.FromJSON using (blockFromJSON)
+open import Luau.Syntax.ToString using (blockToString)
 
 runBlock : Block → IO ⊤
-runBlock block = putStrLn "OK"
+runBlock block = putStrLn (blockToString block)
 
 runJSON : Value → IO ⊤
 runJSON value with blockFromJSON(value)