DQuery.idr

module DQuery

import Record

namespace Json
  data Json
    = JsonString String
    | JsonBool Bool
    | JsonInt Int
    | JsonObject (List (String, Json))
    | JsonList (List Json)

  decodeString : Json -> Maybe String
  decodeString (JsonString val) = Just val
  decodeString _ = Nothing

  decodeBool : Json -> Maybe Bool
  decodeBool (JsonBool val) = Just val
  decodeBool _ = Nothing

  decodeInt : Json -> Maybe Int
  decodeInt (JsonInt val) = Just val
  decodeInt _ = Nothing

  decodeList : (itemDecoder : Json -> Maybe a) -> Json -> Maybe (List a)
  decodeList itemDecoder (JsonList items) = traverse itemDecoder items
  decodeList _ _ = Nothing


namespace Specification
  data Spec
    = StringSpec
    | BoolSpec
    | IntSpec
    | ObjectSpec (List (String, Spec))
    | ListSpec Spec

  mutual
    fieldTypes : List (String, Spec) -> List (String, Type)
    fieldTypes [] = []
    fieldTypes ((field, spec) :: xs) = (field, SpecType spec) :: fieldTypes xs
    
    SpecType : Spec -> Type
    SpecType StringSpec = String
    SpecType BoolSpec = Bool
    SpecType IntSpec = Int
    SpecType (ObjectSpec fieldSpecs) = Record (fieldTypes fieldSpecs)
    SpecType (ListSpec itemSpec) = List (SpecType itemSpec)

  mutual
    objectSpecFieldsDecoder : (fieldSpecs : List (String, Spec)) -> Json -> Maybe (Record (fieldTypes fieldSpecs))
    objectSpecFieldsDecoder [] (JsonObject _) = Just []
    objectSpecFieldsDecoder ((key, valSpec) :: rest) json@(JsonObject jsonFields) = do
      jsonFieldVal <- lookup key jsonFields
      val <- specDecoder valSpec jsonFieldVal
      restRecord <- objectSpecFieldsDecoder rest json
      pure $ (key := val) :: restRecord
    objectSpecFieldsDecoder _ _ = Nothing

    specDecoder : (s : Spec) -> Json -> Maybe (SpecType s)
    specDecoder StringSpec = decodeString
    specDecoder BoolSpec = decodeBool
    specDecoder IntSpec = decodeInt
    specDecoder (ObjectSpec fieldSpecs) = objectSpecFieldsDecoder fieldSpecs
    specDecoder (ListSpec itemSpec) = decodeList (specDecoder itemSpec)


namespace MySchema
  data UserField : Type where
    Name : UserField
    IsAdmin : UserField
    Age : UserField

  userFieldSpec : UserField -> Spec
  userFieldSpec Name = StringSpec
  userFieldSpec IsAdmin = BoolSpec
  userFieldSpec Age = IntSpec

  data QueryField : Type where
    User : (id : String) -> (fields : List (String, UserField)) -> QueryField

  queryFieldSpec : QueryField -> Spec
  queryFieldSpec (User id fields) = ObjectSpec (map (map userFieldSpec) fields)

  querySpec : List (String, QueryField) -> Spec
  querySpec fields = ObjectSpec (map (map queryFieldSpec) fields)

namespace MyQuery
  someQuery : List (String, QueryField)
  someQuery =
    [ ("user1", User "1" [("name", Name), ("isAdmin", IsAdmin), ("age", Age)])
    , ("user2", User "2" [("name", Name), ("isAdmin", IsAdmin)])
    ]

  someQueryResponseJson : Json
  someQueryResponseJson =
    JsonObject
      [ ("user1", JsonObject [("name", JsonString "alice"), ("isAdmin", JsonBool True), ("age", JsonInt 900)])
      , ("user2", JsonObject [("name", JsonString "bob"), ("isAdmin", JsonBool False)])
      ]

  someQueryDecodedResult : Maybe (SpecType (querySpec DQuery.MyQuery.someQuery))
  someQueryDecodedResult =
    specDecoder (querySpec someQuery) someQueryResponseJson

  userSummaries : List (String, Bool)
  userSummaries = fromMaybe [] (summarize <$> someQueryDecodedResult) where
    summarize : SpecType (querySpec DQuery.MyQuery.someQuery) -> List (String, Bool)
    summarize result =
      [ (result .. "user1" .. "name", result .. "user1" .. "isAdmin")
      , (result .. "user2" .. "name", result .. "user2" .. "isAdmin")
      ]
  --[("alice", True), ("bob", False)]

Record.idr

-- adapted from https://github.com/jmars/Records
module Record

%access public export

infix 5 :=
infix 5 -:
infixl 9 ..

-- A record field is some label type paired with a value. := just
-- gives a nicer syntax than tuples for this....

data Field : lbl -> Type -> Type where
      (:=) : (field_label : lbl) -> 
              (value : b) -> Field field_label b

-- Then a record is essentially a heterogeneous list where everything
-- is labelled.
data Record : List (lbl, Type) -> Type where
      Nil : Record {lbl} []
      (::) : Field lbl a -> Record xs -> Record ((lbl, a) :: xs)

-- FieldType 'lbl rec ty 
-- is a predicate stating that the label 'lbl in record with index
-- rec has type ty.

data FieldType : (field : lbl) -> Type -> List (lbl, Type) -> Type where
  First : FieldType field ty ((field, ty) :: xs)
  Later : FieldType field t xs -> FieldType field t (a :: xs)

-- To extract a field from the record, we need the field label, a
-- record, and a proof that the field is valid for the type we want.

get' : Record xs -> FieldType field t xs -> t
get' ((_ := val) :: xs) First = val
get' (_ :: xs) (Later y) = get' xs y

(..) : Record {lbl} xs -> (field : lbl) -> { auto prf : FieldType field t xs} -> t
(..) rec f {prf} = get' rec prf

-- Delete a field

delete' : FieldType field t zs -> Record {lbl} zs -> (m ** Record {lbl} m)
delete' First (x :: xs) = (_ ** xs)
delete' (Later y) (x :: xs) with (delete' y xs)
  | (ts ** ys) = (_ :: ts ** x :: ys)

(-) : (field : lbl) -> Record {lbl} xs ->
      { auto prf : FieldType field t xs } ->
      (m ** Record {lbl} m)
(-) f rec {prf} = delete' prf rec

-- Combine two records (prototypal inheritance)

(++) : Record {lbl} xs -> Record {lbl} ys -> Record (xs ++ ys)
(++) []        ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

-- Update a field, possibly changing the type

update' : Record {lbl} xs -> FieldType field t xs -> Field field a -> (m ** Record {lbl} m)
update' (x :: xs) First v = (_ ** v :: xs)
update' (x :: xs) (Later y) v with (update' xs y v)
  | (ts ** ys) = (_ :: ts ** x :: ys)

(-:) : Field field t -> Record {lbl} xs ->
        { auto prf : FieldType field t xs } ->
        (m ** Record {lbl} m)
(-:) f rec {prf} = update' rec prf f