
  0 | ||| Common types and instances for JSON interoperability.
  1 | |||
  2 | ||| (C) The Idris Community, 2021
  3 | module Language.LSP.Message.Utils
  4 | 
  5 | import public Data.OneOf
  6 | import Language.JSON
  7 | import Language.JSON.Interfaces
  8 | import Language.LSP.Message.Derive
  9 | 
 10 | %default total
 11 | 
 12 | ||| Singleton type that models `null` in JSON.
 13 | public export
 14 | data Null = MkNull
 15 | 
 16 | public export
 17 | Eq Null where
 18 |   MkNull == MkNull = True
 19 | 
 20 | public export
 21 | Ord Null where
 22 |   compare MkNull MkNull = EQ
 23 | 
 24 | public export
 25 | Show Null where
 26 |   show MkNull = "null"
 27 | 
 28 | export
 29 | ToJSON Null where
 30 |   toJSON MkNull = JNull
 31 | 
 32 | export
 33 | FromJSON Null where
 34 |   fromJSON JNull = pure MkNull
 35 |   fromJSON _ = neutral
 36 | 
 37 | ||| Converts an `UntaggedEither` value to the isomorphic value in `Either`.
 38 | public export
 39 | toEither : OneOf [a, b] -> Either a b
 40 | toEither (Here x)  = Left x
 41 | toEither (There (Here x)) = Right x
 42 | 
 43 | ||| Converts an `Either` value to the isomorphic value in `UntaggedEither`.
 44 | public export
 45 | fromEither : Either a b -> OneOf [a, b]
 46 | fromEither (Left x)  = make x
 47 | fromEither (Right x) = make x
 48 | 
 49 | public export
 50 | toMaybe : OneOf [a, Null] -> Maybe a
 51 | toMaybe (Here x) = Just x
 52 | toMaybe (There (Here MkNull)) = Nothing
 53 | 
 54 | public export
 55 | fromMaybe : Maybe a -> OneOf [a, Null]
 56 | fromMaybe (Just x) = make x
 57 | fromMaybe Nothing = make MkNull
 58 | 
 59 | public export
 60 | ConstraintList : (Type -> Type) -> List Type -> Type
 61 | ConstraintList f [] = ()
 62 | ConstraintList f (x :: xs) = (f x, ConstraintList f xs)
 63 | 
 64 | export
 65 | ConstraintList ToJSON as => ToJSON (OneOf as) where
 66 |   toJSON (Here x) = toJSON x
 67 |   toJSON (There x) = toJSON x
 68 | 
 69 | export
 70 | {as : _} -> ConstraintList FromJSON as => FromJSON (OneOf as) where
 71 |   -- NOTE: The rightmost type is parsed first, since in the LSP specification
 72 |   --       the most specific type appears also rightmost.
 73 |   fromJSON {as = []} @{()} v = Nothing
 74 |   fromJSON {as = (x :: xs)} @{(c, cs)} v = (There <$> fromJSON v) <|> (Here <$> fromJSON v)
 75 |