git.iko.soy/schematic
on cf38e1f help sign in
schematic/src/Data/Schematic/Schema.hs
507 lines 19 kB history raw
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE OverloadedLists #-}
3{-# LANGUAGE OverloadedStrings #-}
4{-# OPTIONS_GHC -fprint-explicit-kinds #-}
6module Data.Schematic.Schema where
8import Control.Applicative ((<|>))
9import Control.Monad
10import Data.Aeson as J
11import Data.Aeson.Types as J
12import Data.HashMap.Strict as H
13import Data.Kind
14import Data.Maybe
15import Data.Schematic.Instances ()
16import Data.Scientific
17import Data.Singletons.Prelude.List hiding (All, Union)
18import Data.Singletons.TH
19import Data.Singletons.TypeLits
20import Data.Text as T
21import Data.Union
22import Data.Vector as V
23import Data.Vinyl hiding (Dict)
24import qualified Data.Vinyl.TypeLevel as V
25import GHC.Exts
26import GHC.Generics (Generic)
27import GHC.TypeLits (SomeNat(..), SomeSymbol(..), someSymbolVal, someNatVal)
28import Prelude as P
29import Test.SmallCheck.Series
32type family CRepr (s :: Schema) :: Type where
33 CRepr ('SchemaText cs) = TextConstraint
34 CRepr ('SchemaNumber cs) = NumberConstraint
35 CRepr ('SchemaObject fs) = (String, Schema)
36 CRepr ('SchemaArray ar s) = ArrayConstraint
38data TextConstraint
39 = TEq Nat
40 | TLt Nat
41 | TLe Nat
42 | TGt Nat
43 | TGe Nat
44 | TRegex Symbol
45 | TEnum [Symbol]
46 deriving (Generic)
48instance SingKind TextConstraint where
49 type Demote TextConstraint = DemotedTextConstraint
50 fromSing = \case
51 STEq n -> withKnownNat n (DTEq . fromIntegral $ natVal n)
52 STLt n -> withKnownNat n (DTLt . fromIntegral $ natVal n)
53 STLe n -> withKnownNat n (DTLe . fromIntegral $ natVal n)
54 STGt n -> withKnownNat n (DTGt . fromIntegral $ natVal n)
55 STGe n -> withKnownNat n (DTGe . fromIntegral $ natVal n)
56 STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
57 STEnum s -> let
58 d :: Sing (s :: [Symbol]) -> [Text]
59 d SNil = []
60 d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
61 in DTEnum $ d s
62 toSing = \case
63 DTEq n -> case someNatVal n of
64 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
65 Nothing -> error "Negative singleton nat"
66 DTLt n -> case someNatVal n of
67 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
68 Nothing -> error "Negative singleton nat"
69 DTLe n -> case someNatVal n of
70 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
71 Nothing -> error "Negative singleton nat"
72 DTGt n -> case someNatVal n of
73 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
74 Nothing -> error "Negative singleton nat"
75 DTGe n -> case someNatVal n of
76 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
77 Nothing -> error "Negative singleton nat"
78 DTRegex s -> case someSymbolVal (T.unpack s) of
79 SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
80 DTEnum ss -> case toSing ss of
81 SomeSing l -> SomeSing (STEnum l)
83data DemotedTextConstraint
84 = DTEq Integer
85 | DTLt Integer
86 | DTLe Integer
87 | DTGt Integer
88 | DTGe Integer
89 | DTRegex Text
90 | DTEnum [Text]
91 deriving (Generic)
93data instance Sing (tc :: TextConstraint) where
94 STEq :: Sing n -> Sing ('TEq n)
95 STLt :: Sing n -> Sing ('TLt n)
96 STLe :: Sing n -> Sing ('TLe n)
97 STGt :: Sing n -> Sing ('TGt n)
98 STGe :: Sing n -> Sing ('TGe n)
99 STRegex :: Sing s -> Sing ('TRegex s)
100 STEnum :: Sing ss -> Sing ('TEnum ss)
102instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
103instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
104instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
105instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
106instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
107instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
108instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
110instance Eq (Sing ('TEq n)) where _ == _ = True
111instance Eq (Sing ('TLt n)) where _ == _ = True
112instance Eq (Sing ('TLe n)) where _ == _ = True
113instance Eq (Sing ('TGt n)) where _ == _ = True
114instance Eq (Sing ('TGe n)) where _ == _ = True
115instance Eq (Sing ('TRegex t)) where _ == _ = True
116instance Eq (Sing ('TEnum ss)) where _ == _ = True
118data NumberConstraint
119 = NLe Nat
120 | NLt Nat
121 | NGt Nat
122 | NGe Nat
123 | NEq Nat
124 deriving (Generic)
126data DemotedNumberConstraint
127 = DNLe Integer
128 | DNLt Integer
129 | DNGt Integer
130 | DNGe Integer
131 | DNEq Integer
132 deriving (Generic)
134data instance Sing (nc :: NumberConstraint) where
135 SNEq :: Sing n -> Sing ('NEq n)
136 SNGt :: Sing n -> Sing ('NGt n)
137 SNGe :: Sing n -> Sing ('NGe n)
138 SNLt :: Sing n -> Sing ('NLt n)
139 SNLe :: Sing n -> Sing ('NLe n)
141instance KnownNat n => SingI ('NEq n) where sing = SNEq sing
142instance KnownNat n => SingI ('NGt n) where sing = SNGt sing
143instance KnownNat n => SingI ('NGe n) where sing = SNGe sing
144instance KnownNat n => SingI ('NLt n) where sing = SNLt sing
145instance KnownNat n => SingI ('NLe n) where sing = SNLe sing
147instance Eq (Sing ('NEq n)) where _ == _ = True
148instance Eq (Sing ('NLt n)) where _ == _ = True
149instance Eq (Sing ('NLe n)) where _ == _ = True
150instance Eq (Sing ('NGt n)) where _ == _ = True
151instance Eq (Sing ('NGe n)) where _ == _ = True
153instance SingKind NumberConstraint where
154 type Demote NumberConstraint = DemotedNumberConstraint
155 fromSing = \case
156 SNEq n -> withKnownNat n (DNEq . fromIntegral $ natVal n)
157 SNGt n -> withKnownNat n (DNGt . fromIntegral $ natVal n)
158 SNGe n -> withKnownNat n (DNGe . fromIntegral $ natVal n)
159 SNLt n -> withKnownNat n (DNLt . fromIntegral $ natVal n)
160 SNLe n -> withKnownNat n (DNLe . fromIntegral $ natVal n)
161 toSing = \case
162 DNEq n -> case someNatVal n of
163 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
164 Nothing -> error "Negative singleton nat"
165 DNGt n -> case someNatVal n of
166 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
167 Nothing -> error "Negative singleton nat"
168 DNGe n -> case someNatVal n of
169 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
170 Nothing -> error "Negative singleton nat"
171 DNLt n -> case someNatVal n of
172 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
173 Nothing -> error "Negative singleton nat"
174 DNLe n -> case someNatVal n of
175 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
176 Nothing -> error "Negative singleton nat"
178data ArrayConstraint
179 = AEq Nat
180 deriving (Generic)
182data DemotedArrayConstraint
183 = DAEq Integer
184 deriving (Generic)
186data instance Sing (ac :: ArrayConstraint) where
187 SAEq :: Sing n -> Sing ('AEq n)
189instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
191instance Eq (Sing ('AEq n)) where _ == _ = True
193instance SingKind ArrayConstraint where
194 type Demote ArrayConstraint = DemotedArrayConstraint
195 fromSing = \case
196 SAEq n -> withKnownNat n (DAEq . fromIntegral $ natVal n)
197 toSing = \case
198 DAEq n -> case someNatVal n of
199 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
200 Nothing -> error "Negative singleton nat"
202data Schema
203 = SchemaText [TextConstraint]
204 | SchemaBoolean
205 | SchemaNumber [NumberConstraint]
206 | SchemaObject [(Symbol, Schema)]
207 | SchemaArray [ArrayConstraint] Schema
208 | SchemaNull
209 | SchemaOptional Schema
210 | SchemaUnion [Schema]
211 deriving (Generic)
213data DemotedSchema
214 = DSchemaText [DemotedTextConstraint]
215 | DSchemaNumber [DemotedNumberConstraint]
216 | DSchemaBoolean
217 | DSchemaObject [(Text, DemotedSchema)]
218 | DSchemaArray [DemotedArrayConstraint] DemotedSchema
219 | DSchemaNull
220 | DSchemaOptional DemotedSchema
221 | DSchemaUnion [DemotedSchema]
222 deriving (Generic)
224data instance Sing (schema :: Schema) where
225 SSchemaText :: Sing tcs -> Sing ('SchemaText tcs)
226 SSchemaNumber :: Sing ncs -> Sing ('SchemaNumber ncs)
227 SSchemaBoolean :: Sing 'SchemaBoolean
228 SSchemaArray :: Sing acs -> Sing schema -> Sing ('SchemaArray acs schema)
229 SSchemaObject :: Sing fields -> Sing ('SchemaObject fields)
230 SSchemaOptional :: Sing s -> Sing ('SchemaOptional s)
231 SSchemaNull :: Sing 'SchemaNull
232 SSchemaUnion :: Sing ss -> Sing ('SchemaUnion ss)
234instance SingI sl => SingI ('SchemaText sl) where
235 sing = SSchemaText sing
236instance SingI sl => SingI ('SchemaNumber sl) where
237 sing = SSchemaNumber sing
238instance SingI 'SchemaNull where
239 sing = SSchemaNull
240instance SingI 'SchemaBoolean where
241 sing = SSchemaBoolean
242instance (SingI ac, SingI s) => SingI ('SchemaArray ac s) where
243 sing = SSchemaArray sing sing
244instance SingI stl => SingI ('SchemaObject stl) where
245 sing = SSchemaObject sing
246instance SingI s => SingI ('SchemaOptional s) where
247 sing = SSchemaOptional sing
248instance SingI s => SingI ('SchemaUnion s) where
249 sing = SSchemaUnion sing
251instance Eq (Sing ('SchemaText cs)) where _ == _ = True
252instance Eq (Sing ('SchemaNumber cs)) where _ == _ = True
253instance Eq (Sing 'SchemaNull) where _ == _ = True
254instance Eq (Sing 'SchemaBoolean) where _ == _ = True
255instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
256instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
257instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
258instance Eq (Sing ('SchemaUnion s)) where _ == _ = True
260instance SingKind Schema where
261 type Demote Schema = DemotedSchema
262 fromSing = \case
263 SSchemaText cs -> DSchemaText $ fromSing cs
264 SSchemaNumber cs -> DSchemaNumber $ fromSing cs
265 SSchemaBoolean -> DSchemaBoolean
266 SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
267 SSchemaOptional s -> DSchemaOptional $ fromSing s
268 SSchemaNull -> DSchemaNull
269 SSchemaObject cs -> DSchemaObject $ fromSing cs
270 SSchemaUnion ss -> DSchemaUnion $ fromSing ss
271 toSing = \case
272 DSchemaText cs -> case toSing cs of
273 SomeSing scs -> SomeSing $ SSchemaText scs
274 DSchemaNumber cs -> case toSing cs of
275 SomeSing scs -> SomeSing $ SSchemaNumber scs
276 DSchemaBoolean -> SomeSing $ SSchemaBoolean
277 DSchemaArray cs sch -> case (toSing cs, toSing sch) of
278 (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
279 DSchemaOptional sch -> case toSing sch of
280 SomeSing ssch -> SomeSing $ SSchemaOptional ssch
281 DSchemaNull -> SomeSing SSchemaNull
282 DSchemaObject cs -> case toSing cs of
283 SomeSing scs -> SomeSing $ SSchemaObject scs
284 DSchemaUnion ss -> case toSing ss of
285 SomeSing sss -> SomeSing $ SSchemaUnion sss
287data FieldRepr :: (Symbol, Schema) -> Type where
288 FieldRepr
289 :: (SingI schema, KnownSymbol name)
290 => JsonRepr schema
291 -> FieldRepr '(name, schema)
293-- | Forgetful Functor Ufr
294toJsonRepr :: FieldRepr '(fn, sch) -> JsonRepr sch
295toJsonRepr (FieldRepr x) = x
297knownFieldName
298 :: forall proxy (fieldName :: Symbol) schema
299 . KnownSymbol fieldName
300 => proxy '(fieldName, schema)
301 -> Text
302knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
304knownFieldSchema
305 :: forall proxy fieldName schema
306 . SingI schema
307 => proxy '(fieldName, schema)
308 -> Sing schema
309knownFieldSchema _ = sing
311deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
313instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
314 FieldRepr a == FieldRepr b = a == b
316instance
317 ( KnownSymbol name
318 , SingI schema
319 , Serial m (JsonRepr schema) )
320 => Serial m (FieldRepr '(name, schema)) where
321 series = FieldRepr <$> series
323type family USubsets (u :: [k]) :: Constraint where
324 USubsets '[] = ()
325 USubsets (h ': tl) = (USubset tl (h ': tl) (V.RImage tl (h ': tl)), USubsets tl)
327data JsonRepr :: Schema -> Type where
328 ReprText :: Text -> JsonRepr ('SchemaText cs)
329 ReprNumber :: Scientific -> JsonRepr ('SchemaNumber cs)
330 ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
331 ReprNull :: JsonRepr 'SchemaNull
332 ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
333 ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
334 ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
335 ReprUnion :: Union JsonRepr (h ': tl) -> JsonRepr ('SchemaUnion (h ': tl))
337-- | Move to the union package
338instance Show (JsonRepr ('SchemaText cs)) where
339 show (ReprText t) = "ReprText " P.++ show t
341instance Show (JsonRepr ('SchemaNumber cs)) where
342 show (ReprNumber n) = "ReprNumber " P.++ show n
344instance Show (JsonRepr 'SchemaNull) where show _ = "ReprNull"
346instance Show (JsonRepr s) => Show (JsonRepr ('SchemaArray acs s)) where
347 show (ReprArray v) = "ReprArray " P.++ show v
349instance V.RecAll FieldRepr fs Show => Show (JsonRepr ('SchemaObject fs)) where
350 show (ReprObject fs) = "ReprObject " P.++ show fs
352instance Show (JsonRepr s) => Show (JsonRepr ('SchemaOptional s)) where
353 show (ReprOptional s) = "ReprOptional " P.++ show s
355instance (Monad m, Serial m Text)
356 => Serial m (JsonRepr ('SchemaText cs)) where
357 series = cons1 ReprText
359instance (Monad m, Serial m Scientific)
360 => Serial m (JsonRepr ('SchemaNumber cs)) where
361 series = cons1 ReprNumber
363instance Monad m => Serial m (JsonRepr 'SchemaNull) where
364 series = cons0 ReprNull
366instance (Serial m (V.Vector (JsonRepr s)))
367 => Serial m (JsonRepr ('SchemaArray cs s)) where
368 series = cons1 ReprArray
370instance (Serial m (JsonRepr s))
371 => Serial m (JsonRepr ('SchemaOptional s)) where
372 series = cons1 ReprOptional
374instance (Monad m, Serial m (Rec FieldRepr fs))
375 => Serial m (JsonRepr ('SchemaObject fs)) where
376 series = cons1 ReprObject
378instance Eq (Rec FieldRepr fs) => Eq (JsonRepr ('SchemaObject fs)) where
379 ReprObject a == ReprObject b = a == b
381instance Eq (JsonRepr ('SchemaText cs)) where
382 ReprText a == ReprText b = a == b
384instance Eq (JsonRepr ('SchemaNumber cs)) where
385 ReprNumber a == ReprNumber b = a == b
387instance Eq (JsonRepr 'SchemaNull) where
388 ReprNull == ReprNull = True
390instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaArray as s)) where
391 ReprArray a == ReprArray b = a == b
393instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaOptional s)) where
394 ReprOptional a == ReprOptional b = a == b
396instance IsList (JsonRepr ('SchemaArray cs s)) where
397 type Item (JsonRepr ('SchemaArray cs s)) = JsonRepr s
398 fromList = ReprArray . GHC.Exts.fromList
399 toList (ReprArray v) = GHC.Exts.toList v
401instance Num (JsonRepr ('SchemaNumber cs)) where
402 ReprNumber a + ReprNumber b = ReprNumber $ a + b
403 ReprNumber a - ReprNumber b = ReprNumber $ a - b
404 ReprNumber a * ReprNumber b = ReprNumber $ a * b
405 abs (ReprNumber a) = ReprNumber $ abs a
406 signum (ReprNumber a) = ReprNumber $ signum a
407 fromInteger = ReprNumber . fromIntegral
409instance IsString (JsonRepr ('SchemaText cs)) where
410 fromString = ReprText . fromString
412fromOptional
413 :: SingI s
414 => Sing ('SchemaOptional s)
415 -> J.Value
416 -> Parser (Maybe (JsonRepr s))
417fromOptional _ = parseJSON
419parseUnion
420 :: FromJSON (JsonRepr ('SchemaUnion ss))
421 => sing (ss :: [Schema])
422 -> Value
423 -> Parser (JsonRepr ('SchemaUnion ss))
424parseUnion _ val = parseJSON val
426instance FromJSON (Union JsonRepr '[]) where
427 parseJSON = fail "empty union"
429instance (SingI a, FromJSON (Union JsonRepr as)) => FromJSON (Union JsonRepr (a ': as)) where
430 parseJSON val = (This <$> parseJSON val)
431 <|> (That <$> (parseJSON val :: Parser (Union JsonRepr as)))
433instance ToJSON (Union JsonRepr as) where
434 toJSON (This fa) = toJSON fa
435 toJSON (That u) = toJSON u
437instance SingI schema => J.FromJSON (JsonRepr schema) where
438 parseJSON value = case sing :: Sing schema of
439 SSchemaText _ -> withText "String" (pure . ReprText) value
440 SSchemaNumber _ -> withScientific "Number" (pure . ReprNumber) value
441 SSchemaBoolean -> ReprBoolean <$> parseJSON value
442 SSchemaNull -> case value of
443 J.Null -> pure ReprNull
444 _ -> typeMismatch "Null" value
445 so@(SSchemaOptional s) -> withSingI s $ ReprOptional <$> fromOptional so value
446 SSchemaArray sa sb -> withSingI sa $ withSingI sb
447 $ withArray "Array" (fmap ReprArray . traverse parseJSON) value
448 SSchemaObject fs -> do
449 let
450 demoteFields :: SList s -> H.HashMap Text J.Value -> Parser (Rec FieldRepr s)
451 demoteFields SNil _ = pure RNil
452 demoteFields (SCons (STuple2 (n :: Sing fn) s) tl) h = withKnownSymbol n $ do
453 let fieldName = T.pack $ symbolVal (Proxy @fn)
454 fieldRepr <- case s of
455 SSchemaText so -> case H.lookup fieldName h of
456 Just v -> withSingI so $ FieldRepr <$> parseJSON v
457 Nothing -> fail "schematext"
458 SSchemaNumber so -> case H.lookup fieldName h of
459 Just v -> withSingI so $ FieldRepr <$> parseJSON v
460 Nothing -> fail "schemanumber"
461 SSchemaBoolean -> case H.lookup fieldName h of
462 Just v -> FieldRepr <$> parseJSON v
463 Nothing -> fail "schemaboolean"
464 SSchemaNull -> case H.lookup fieldName h of
465 Just v -> FieldRepr <$> parseJSON v
466 Nothing -> fail "schemanull"
467 SSchemaArray sa sb -> case H.lookup fieldName h of
468 Just v -> withSingI sa $ withSingI sb $ FieldRepr <$> parseJSON v
469 Nothing -> fail "schemaarray"
470 SSchemaObject so -> case H.lookup fieldName h of
471 Just v -> withSingI so $ FieldRepr <$> parseJSON v
472 Nothing -> fail "schemaobject"
473 SSchemaOptional so -> case H.lookup fieldName h of
474 Just v -> withSingI so $ FieldRepr <$> parseJSON v
475 Nothing -> fail "schemaoptional"
476 SSchemaUnion ss -> withSingI ss $ FieldRepr <$> parseUnion ss value
477 (fieldRepr :&) <$> demoteFields tl h
478 ReprObject <$> withObject "Object" (demoteFields fs) value
479 SSchemaUnion ss -> parseUnion ss value
481instance J.ToJSON (JsonRepr a) where
482 toJSON ReprNull = J.Null
483 toJSON (ReprBoolean b) = J.Bool b
484 toJSON (ReprText t) = J.String t
485 toJSON (ReprNumber n) = J.Number n
486 toJSON (ReprOptional s) = case s of
487 Just v -> toJSON v
488 Nothing -> J.Null
489 toJSON (ReprArray v) = J.Array $ toJSON <$> v
490 toJSON (ReprObject r) = J.Object . H.fromList . fold $ r
491 where
492 extract :: forall name s . (KnownSymbol name)
493 => FieldRepr '(name, s)
494 -> (Text, Value)
495 extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
496 fold :: Rec FieldRepr fs -> [(Text, J.Value)]
497 fold = \case
498 RNil -> []
499 fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
500 toJSON (ReprUnion u) = toJSON u
502class FalseConstraint a
504type family TopLevel (schema :: Schema) :: Constraint where
505 TopLevel ('SchemaArray acs s) = ()
506 TopLevel ('SchemaObject o) = ()
507 TopLevel spec = 'True ~ 'False