@@ -1,595 +1,159 @@
11{-# LANGUAGE AllowAmbiguousTypes #-}
2−{-# LANGUAGE CPP #-}
3−{-# LANGUAGE OverloadedLists #-}
4−{-# LANGUAGE OverloadedStrings #-}
2+{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE InstanceSigs #-}
4+{-# LANGUAGE UndecidableInstances #-}
55{-# OPTIONS_GHC -fprint-explicit-kinds #-}
66
77module Data.Schematic.Schema where
88
9−import Control.Applicative ((<|>))
10−import Control.Monad
11−import Data.Aeson as J
12−import Data.Aeson.Types as J
13−import Data.HashMap.Strict as H
14−import Data.Kind
15−import Data.Maybe
16−import Data.Schematic.Generator
17−import Data.Schematic.Instances ()
18−import Data.Scientific
19−import Data.Singletons.Prelude.List hiding (All, Union)
20−import Data.Singletons.TH
21−import Data.Singletons.TypeLits
22−import Data.Text as T
23−import Data.Union
24−import Data.Vector as V
25−import Data.Vinyl hiding (Dict)
26−import qualified Data.Vinyl.TypeLevel as V
27−import GHC.Exts
28−import GHC.Generics (Generic)
29−import GHC.TypeLits
30− (SomeNat(..), SomeSymbol(..), someNatVal, someSymbolVal)
31−import Prelude as P
32−import Test.SmallCheck.Series
33−
34−
35−type family CRepr (s :: Schema) :: Type where
36− CRepr ('SchemaText cs) = TextConstraint
37− CRepr ('SchemaNumber cs) = NumberConstraint
38− CRepr ('SchemaObject fs) = (String, Schema)
39− CRepr ('SchemaArray ar s) = ArrayConstraint
9+import Data.Kind hiding (Type)
10+import Data.Proxy
11+import Data.Text (Text)
12+import GHC.TypeLits (KnownNat, natVal, KnownSymbol, symbolVal, Symbol, Nat)
13+
14+
15+-- | Type Tags
16+data JType
17+ = JText
18+ | JNumber
19+ | JArray
20+ | JObject
21+ | JNull
22+
23+type family Repr (ty :: JType) :: * where
24+ Repr 'JText = String -- because of matchRegex
25+ Repr 'JNumber = Double
26+
27+class Constrained (ty :: JType) c where
28+ cRep :: Proxy ty -> Proxy c -> CRepr ty
29+
30+-- Validators
31+
32+data LengthEqNat nat
33+
34+instance KnownNat nat => Constrained 'JText (LengthEqNat nat) where
35+ cRep _ _ = LengthEq $ natVal (Proxy @nat)
36+
37+data Gt nat
38+
39+instance KnownNat nat => Constrained 'JNumber (Gt nat) where
40+ cRep _ _ = Gt $ natVal (Proxy @nat)
41+
42+-- /Validators
43+
44+data Field field ty schema
45+
46+data Empty
47+
48+class Verifiable ty cs where
49+ schema :: Proxy ty -> Proxy cs -> [CRepr ty]
50+
51+instance
52+ ( Constrained 'JText c
53+ , Verifiable 'JText cs )
54+ => Verifiable 'JText (c ': cs) where
55+ schema _ _ = cRep (Proxy @'JText) (Proxy @c)
56+ : schema (Proxy @'JText) (Proxy @cs)
57+
58+instance
59+ ( Constrained 'JNumber c
60+ , Verifiable 'JNumber cs )
61+ => Verifiable 'JNumber (c ': cs) where
62+ schema _ _ = cRep (Proxy @'JNumber) (Proxy @c)
63+ : schema (Proxy @'JNumber) (Proxy @cs)
64+
65+instance Verifiable jty '[] where
66+ schema _ _ = []
67+
68+instance
69+ ( SchemaConstructor jty
70+ , Verifiable 'JObject fs
71+ , KnownSymbol field
72+ , Verifiable jty cs )
73+ => Verifiable 'JObject ((Field field jty cs) ': fs) where
74+ schema _ _ = (fieldName, fieldSchema) : schema (Proxy @'JObject) (Proxy @fs)
75+ where
76+ fieldName = symbolVal (Proxy @field)
77+ fieldSchema = constructor (Proxy @jty) $ schema (Proxy @jty) (Proxy @cs)
78+
79+type family CRepr (jty :: JType) :: * where
80+ CRepr JText = TextConstraint
81+ CRepr JNumber = NumberConstraint
82+ CRepr JObject = (String, Schema)
4083
4184data TextConstraint
42− = TEq Nat
43− | TLt Nat
44− | TLe Nat
45− | TGt Nat
46− | TGe Nat
47− | TRegex Symbol
48− | TEnum [Symbol]
49− deriving (Generic)
50−
51−instance SingKind TextConstraint where
52− type Demote TextConstraint = DemotedTextConstraint
53− fromSing = \case
54− STEq n -> withKnownNat n (DTEq . fromIntegral $ natVal n)
55− STLt n -> withKnownNat n (DTLt . fromIntegral $ natVal n)
56− STLe n -> withKnownNat n (DTLe . fromIntegral $ natVal n)
57− STGt n -> withKnownNat n (DTGt . fromIntegral $ natVal n)
58− STGe n -> withKnownNat n (DTGe . fromIntegral $ natVal n)
59− STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
60− STEnum s -> let
61− d :: Sing (s :: [Symbol]) -> [Text]
62− d SNil = []
63− d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
64− in DTEnum $ d s
65− toSing = \case
66− DTEq n -> case someNatVal n of
67− Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
68− Nothing -> error "Negative singleton nat"
69− DTLt n -> case someNatVal n of
70− Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
71− Nothing -> error "Negative singleton nat"
72− DTLe n -> case someNatVal n of
73− Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
74− Nothing -> error "Negative singleton nat"
75− DTGt n -> case someNatVal n of
76− Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
77− Nothing -> error "Negative singleton nat"
78− DTGe n -> case someNatVal n of
79− Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
80− Nothing -> error "Negative singleton nat"
81− DTRegex s -> case someSymbolVal (T.unpack s) of
82− SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
83− DTEnum ss -> case toSing ss of
84− SomeSing l -> SomeSing (STEnum l)
85−
86−data DemotedTextConstraint
87− = DTEq Integer
88− | DTLt Integer
89− | DTLe Integer
90− | DTGt Integer
91− | DTGe Integer
92− | DTRegex Text
93− | DTEnum [Text]
94− deriving (Generic, Eq, Show)
95−
96−data instance Sing (tc :: TextConstraint) where
97− STEq :: Sing n -> Sing ('TEq n)
98− STLt :: Sing n -> Sing ('TLt n)
99− STLe :: Sing n -> Sing ('TLe n)
100− STGt :: Sing n -> Sing ('TGt n)
101− STGe :: Sing n -> Sing ('TGe n)
102− STRegex :: Sing s -> Sing ('TRegex s)
103− STEnum :: Sing ss -> Sing ('TEnum ss)
104−
105−instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
106−instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
107−instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
108−instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
109−instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
110−instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
111−instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
112−
113−instance Eq (Sing ('TEq n)) where _ == _ = True
114−instance Eq (Sing ('TLt n)) where _ == _ = True
115−instance Eq (Sing ('TLe n)) where _ == _ = True
116−instance Eq (Sing ('TGt n)) where _ == _ = True
117−instance Eq (Sing ('TGe n)) where _ == _ = True
118−instance Eq (Sing ('TRegex t)) where _ == _ = True
119−instance Eq (Sing ('TEnum ss)) where _ == _ = True
85+ = LengthEq Integer
86+ | LengthLe Integer
87+ | LengthGt Integer
88+ deriving (Show, Eq)
12089
12190data NumberConstraint
122− = NLe Nat
123− | NLt Nat
124− | NGt Nat
125− | NGe Nat
126− | NEq Nat
127− deriving (Generic)
128−
129−data DemotedNumberConstraint
130− = DNLe Integer
131− | DNLt Integer
132− | DNGt Integer
133− | DNGe Integer
134− | DNEq Integer
135− deriving (Generic, Eq, Show)
136−
137−data instance Sing (nc :: NumberConstraint) where
138− SNEq :: Sing n -> Sing ('NEq n)
139− SNGt :: Sing n -> Sing ('NGt n)
140− SNGe :: Sing n -> Sing ('NGe n)
141− SNLt :: Sing n -> Sing ('NLt n)
142− SNLe :: Sing n -> Sing ('NLe n)
143−
144−instance KnownNat n => SingI ('NEq n) where sing = SNEq sing
145−instance KnownNat n => SingI ('NGt n) where sing = SNGt sing
146−instance KnownNat n => SingI ('NGe n) where sing = SNGe sing
147−instance KnownNat n => SingI ('NLt n) where sing = SNLt sing
148−instance KnownNat n => SingI ('NLe n) where sing = SNLe sing
149−
150−instance Eq (Sing ('NEq n)) where _ == _ = True
151−instance Eq (Sing ('NLt n)) where _ == _ = True
152−instance Eq (Sing ('NLe n)) where _ == _ = True
153−instance Eq (Sing ('NGt n)) where _ == _ = True
154−instance Eq (Sing ('NGe n)) where _ == _ = True
155−
156−instance SingKind NumberConstraint where
157− type Demote NumberConstraint = DemotedNumberConstraint
158− fromSing = \case
159− SNEq n -> withKnownNat n (DNEq . fromIntegral $ natVal n)
160− SNGt n -> withKnownNat n (DNGt . fromIntegral $ natVal n)
161− SNGe n -> withKnownNat n (DNGe . fromIntegral $ natVal n)
162− SNLt n -> withKnownNat n (DNLt . fromIntegral $ natVal n)
163− SNLe n -> withKnownNat n (DNLe . fromIntegral $ natVal n)
164− toSing = \case
165− DNEq n -> case someNatVal n of
166− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
167− Nothing -> error "Negative singleton nat"
168− DNGt n -> case someNatVal n of
169− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
170− Nothing -> error "Negative singleton nat"
171− DNGe n -> case someNatVal n of
172− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
173− Nothing -> error "Negative singleton nat"
174− DNLt n -> case someNatVal n of
175− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
176− Nothing -> error "Negative singleton nat"
177− DNLe n -> case someNatVal n of
178− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
179− Nothing -> error "Negative singleton nat"
180−
181−data ArrayConstraint
182− = AEq Nat
183− | AGt Nat
184− | AGe Nat
185− | ALt Nat
186− | ALe Nat
187− deriving (Generic)
188−
189−data DemotedArrayConstraint
190− = DAEq Integer
191− | DAGt Integer
192− | DAGe Integer
193− | DALt Integer
194− | DALe Integer
195− deriving (Generic, Eq, Show)
196−
197−data instance Sing (ac :: ArrayConstraint) where
198− SAEq :: Sing n -> Sing ('AEq n)
199− SAGt :: Sing n -> Sing ('AGt n)
200− SAGe :: Sing n -> Sing ('AGe n)
201− SALt :: Sing n -> Sing ('ALt n)
202− SALe :: Sing n -> Sing ('ALe n)
203−
204−instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
205−instance KnownNat n => SingI ('AGt n) where sing = SAGt sing
206−instance KnownNat n => SingI ('AGe n) where sing = SAGe sing
207−instance KnownNat n => SingI ('ALt n) where sing = SALt sing
208−instance KnownNat n => SingI ('ALe n) where sing = SALe sing
209−
210−instance Eq (Sing ('AEq n)) where _ == _ = True
211−instance Eq (Sing ('AGt n)) where _ == _ = True
212−instance Eq (Sing ('AGe n)) where _ == _ = True
213−instance Eq (Sing ('ALt n)) where _ == _ = True
214−instance Eq (Sing ('ALe n)) where _ == _ = True
215−
216−instance SingKind ArrayConstraint where
217− type Demote ArrayConstraint = DemotedArrayConstraint
218− fromSing = \case
219− SAEq n -> withKnownNat n (DAEq . fromIntegral $ natVal n)
220− SAGt n -> withKnownNat n (DAGt . fromIntegral $ natVal n)
221− SAGe n -> withKnownNat n (DAGe . fromIntegral $ natVal n)
222− SALt n -> withKnownNat n (DALt . fromIntegral $ natVal n)
223− SALe n -> withKnownNat n (DALe . fromIntegral $ natVal n)
224− toSing = \case
225− DAEq n -> case someNatVal n of
226− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
227− Nothing -> error "Negative singleton nat"
228− DAGt n -> case someNatVal n of
229− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAGt (SNat :: Sing n))
230− Nothing -> error "Negative singleton nat"
231− DAGe n -> case someNatVal n of
232− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAGe (SNat :: Sing n))
233− Nothing -> error "Negative singleton nat"
234− DALt n -> case someNatVal n of
235− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SALt (SNat :: Sing n))
236− Nothing -> error "Negative singleton nat"
237− DALe n -> case someNatVal n of
238− Just (SomeNat (_ :: Proxy n)) -> SomeSing (SALe (SNat :: Sing n))
239− Nothing -> error "Negative singleton nat"
91+ = Le Integer
92+ | Gt Integer
93+ | Eq Integer
94+ deriving (Show, Eq)
24095
24196data Schema
24297 = SchemaText [TextConstraint]
243− | SchemaBoolean
24498 | SchemaNumber [NumberConstraint]
245− | SchemaObject [(Symbol, Schema)]
246− | SchemaArray [ArrayConstraint] Schema
247− | SchemaNull
248− | SchemaOptional Schema
249− | SchemaUnion [Schema]
250− deriving (Generic)
251−
252−data DemotedSchema
253− = DSchemaText [DemotedTextConstraint]
254− | DSchemaNumber [DemotedNumberConstraint]
255− | DSchemaBoolean
256− | DSchemaObject [(Text, DemotedSchema)]
257− | DSchemaArray [DemotedArrayConstraint] DemotedSchema
258− | DSchemaNull
259− | DSchemaOptional DemotedSchema
260− | DSchemaUnion [DemotedSchema]
261− deriving (Generic, Eq, Show)
262−
263−data instance Sing (schema :: Schema) where
264− SSchemaText :: Sing tcs -> Sing ('SchemaText tcs)
265− SSchemaNumber :: Sing ncs -> Sing ('SchemaNumber ncs)
266− SSchemaBoolean :: Sing 'SchemaBoolean
267− SSchemaArray :: Sing acs -> Sing schema -> Sing ('SchemaArray acs schema)
268− SSchemaObject :: Sing fields -> Sing ('SchemaObject fields)
269− SSchemaOptional :: Sing s -> Sing ('SchemaOptional s)
270− SSchemaNull :: Sing 'SchemaNull
271− SSchemaUnion :: Sing ss -> Sing ('SchemaUnion ss)
272−
273−instance SingI sl => SingI ('SchemaText sl) where
274− sing = SSchemaText sing
275−instance SingI sl => SingI ('SchemaNumber sl) where
276− sing = SSchemaNumber sing
277−instance SingI 'SchemaNull where
278− sing = SSchemaNull
279−instance SingI 'SchemaBoolean where
280− sing = SSchemaBoolean
281−instance (SingI ac, SingI s) => SingI ('SchemaArray ac s) where
282− sing = SSchemaArray sing sing
283−instance SingI stl => SingI ('SchemaObject stl) where
284− sing = SSchemaObject sing
285−instance SingI s => SingI ('SchemaOptional s) where
286− sing = SSchemaOptional sing
287−instance SingI s => SingI ('SchemaUnion s) where
288− sing = SSchemaUnion sing
289−
290−instance Eq (Sing ('SchemaText cs)) where _ == _ = True
291−instance Eq (Sing ('SchemaNumber cs)) where _ == _ = True
292−instance Eq (Sing 'SchemaNull) where _ == _ = True
293−instance Eq (Sing 'SchemaBoolean) where _ == _ = True
294−instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
295−instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
296−instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
297−instance Eq (Sing ('SchemaUnion s)) where _ == _ = True
298−
299−instance SingKind Schema where
300− type Demote Schema = DemotedSchema
301− fromSing = \case
302− SSchemaText cs -> DSchemaText $ fromSing cs
303− SSchemaNumber cs -> DSchemaNumber $ fromSing cs
304− SSchemaBoolean -> DSchemaBoolean
305− SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
306− SSchemaOptional s -> DSchemaOptional $ fromSing s
307− SSchemaNull -> DSchemaNull
308− SSchemaObject cs -> DSchemaObject $ fromSing cs
309− SSchemaUnion ss -> DSchemaUnion $ fromSing ss
310− toSing = \case
311− DSchemaText cs -> case toSing cs of
312− SomeSing scs -> SomeSing $ SSchemaText scs
313− DSchemaNumber cs -> case toSing cs of
314− SomeSing scs -> SomeSing $ SSchemaNumber scs
315− DSchemaBoolean -> SomeSing $ SSchemaBoolean
316− DSchemaArray cs sch -> case (toSing cs, toSing sch) of
317− (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
318− DSchemaOptional sch -> case toSing sch of
319− SomeSing ssch -> SomeSing $ SSchemaOptional ssch
320− DSchemaNull -> SomeSing SSchemaNull
321− DSchemaObject cs -> case toSing cs of
322− SomeSing scs -> SomeSing $ SSchemaObject scs
323− DSchemaUnion ss -> case toSing ss of
324− SomeSing sss -> SomeSing $ SSchemaUnion sss
325−
326−data FieldRepr :: (Symbol, Schema) -> Type where
327− FieldRepr
328− :: (SingI schema, KnownSymbol name)
329− => JsonRepr schema
330− -> FieldRepr '(name, schema)
331−
332−-- | Forgetful Functor Ufr
333−toJsonRepr :: FieldRepr '(fn, sch) -> JsonRepr sch
334−toJsonRepr (FieldRepr x) = x
335−
336−knownFieldName
337− :: forall proxy (fieldName :: Symbol) schema
338− . KnownSymbol fieldName
339− => proxy '(fieldName, schema)
340− -> Text
341−knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
342−
343−knownFieldSchema
344− :: forall proxy fieldName schema
345− . SingI schema
346− => proxy '(fieldName, schema)
347− -> Sing schema
348−knownFieldSchema _ = sing
349−
350−deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
351−
352−instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
353− FieldRepr a == FieldRepr b = a == b
99+ | SchemaObject [(String, Schema)]
100+ | SchemaArray Schema
101+ deriving (Show, Eq)
354102
355−instance
356− ( KnownSymbol name
357− , SingI schema
358− , Serial m (JsonRepr schema) )
359− => Serial m (FieldRepr '(name, schema)) where
360− series = FieldRepr <$> series
361−
362−type family USubsets (u :: [k]) :: Constraint where
363− USubsets '[] = ()
364− USubsets (h ': tl) = (USubset tl (h ': tl) (V.RImage tl (h ': tl)), USubsets tl)
365−
366−data JsonRepr :: Schema -> Type where
367− ReprText :: Text -> JsonRepr ('SchemaText cs)
368− ReprNumber :: Scientific -> JsonRepr ('SchemaNumber cs)
369− ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
370− ReprNull :: JsonRepr 'SchemaNull
371− ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
372− ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
373− ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
374− ReprUnion :: Union JsonRepr (h ': tl) -> JsonRepr ('SchemaUnion (h ': tl))
375−
376−instance (Monad m, Serial m Text, SingI cs)
377− => Serial m (JsonRepr ('SchemaText cs)) where
378− series = decDepth $ fmap ReprText $ textSeries $ fromSing (sing :: Sing cs)
379−
380−instance (Monad m, Serial m Scientific, SingI cs)
381− => Serial m (JsonRepr ('SchemaNumber cs)) where
382− series = decDepth $ fmap ReprNumber
383− $ numberSeries $ fromSing (sing :: Sing cs)
384−
385−instance Monad m => Serial m (JsonRepr 'SchemaNull) where
386− series = cons0 ReprNull
387−
388−instance (Serial m (JsonRepr s), Serial m (V.Vector (JsonRepr s)), SingI cs)
389− => Serial m (JsonRepr ('SchemaArray cs s)) where
390− series = decDepth $ fmap ReprArray
391− $ arraySeries $ fromSing (sing :: Sing cs)
392−
393−instance (Serial m (JsonRepr s))
394− => Serial m (JsonRepr ('SchemaOptional s)) where
395− series = cons1 ReprOptional
396−
397−instance (Monad m, Serial m (Rec FieldRepr fs))
398− => Serial m (JsonRepr ('SchemaObject fs)) where
399− series = cons1 ReprObject
400−
401−-- | Move to the union package
402−instance Show (JsonRepr ('SchemaText cs)) where
403− show (ReprText t) = "ReprText " P.++ show t
404−
405−instance Show (JsonRepr ('SchemaNumber cs)) where
406− show (ReprNumber n) = "ReprNumber " P.++ show n
407−
408−instance Show (JsonRepr 'SchemaBoolean) where
409− show (ReprBoolean n) = "ReprBoolean " P.++ show n
410−
411−instance Show (JsonRepr 'SchemaNull) where show _ = "ReprNull"
412−
413−instance Show (JsonRepr s) => Show (JsonRepr ('SchemaArray acs s)) where
414− show (ReprArray v) = "ReprArray " P.++ show v
415−
416−#if MIN_VERSION_base(4,12,0)
417−instance
418− ( V.RecAll FieldRepr fs Show, RMap fs, ReifyConstraint Show FieldRepr fs
419− , RecordToList fs )
420− => Show (JsonRepr ('SchemaObject fs)) where
421− show (ReprObject fs) = "ReprObject " P.++ show fs
422−#else
423−instance V.RecAll FieldRepr fs Show => Show (JsonRepr ('SchemaObject fs)) where
424− show (ReprObject fs) = "ReprObject " P.++ show fs
425−#endif
103+-- | Apply constraint for each element of list
104+-- type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
105+-- AllSatisfy c '[] = ()
106+-- AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
426107
427−instance Show (JsonRepr s) => Show (JsonRepr ('SchemaOptional s)) where
428− show (ReprOptional s) = "ReprOptional " P.++ show s
429−
430−instance Show (Union JsonRepr (h ': tl))
431− => Show (JsonRepr ('SchemaUnion (h ': tl))) where
432− show (ReprUnion s) = "ReprUnion " P.++ show s
433−
434−instance Eq (Rec FieldRepr fs) => Eq (JsonRepr ('SchemaObject fs)) where
435− ReprObject a == ReprObject b = a == b
436−
437−instance Eq (JsonRepr ('SchemaText cs)) where
438− ReprText a == ReprText b = a == b
439−
440−instance Eq (JsonRepr ('SchemaNumber cs)) where
441− ReprNumber a == ReprNumber b = a == b
442−
443−instance Eq (JsonRepr 'SchemaBoolean) where
444− ReprBoolean a == ReprBoolean b = a == b
445−
446−instance Eq (JsonRepr 'SchemaNull) where
447− ReprNull == ReprNull = True
448−
449−instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaArray as s)) where
450− ReprArray a == ReprArray b = a == b
451−
452−instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaOptional s)) where
453− ReprOptional a == ReprOptional b = a == b
454−
455−instance Eq (Union JsonRepr (h ': tl))
456− => Eq (JsonRepr ('SchemaUnion (h ': tl))) where
457− ReprUnion a == ReprUnion b = a == b
458−
459−instance Ord (Rec FieldRepr fs) => Ord (JsonRepr ('SchemaObject fs)) where
460− ReprObject a `compare` ReprObject b = a `compare` b
461−
462−instance Ord (JsonRepr ('SchemaText cs)) where
463− ReprText a `compare` ReprText b = a `compare` b
464−
465−instance Ord (JsonRepr ('SchemaNumber cs)) where
466− ReprNumber a `compare` ReprNumber b = a `compare` b
467−
468−instance Ord (JsonRepr 'SchemaBoolean) where
469− ReprBoolean a `compare` ReprBoolean b = a `compare` b
470−
471−instance Ord (JsonRepr 'SchemaNull) where
472− compare _ _ = EQ
473−
474−instance Ord (JsonRepr s) => Ord (JsonRepr ('SchemaArray as s)) where
475− ReprArray a `compare` ReprArray b = a `compare` b
476−
477−instance Ord (JsonRepr s) => Ord (JsonRepr ('SchemaOptional s)) where
478− ReprOptional a `compare` ReprOptional b = a `compare` b
479−
480−instance Ord (Union JsonRepr (h ': tl))
481− => Ord (JsonRepr ('SchemaUnion (h ': tl))) where
482− ReprUnion a `compare` ReprUnion b = a `compare` b
483−
484−instance IsList (JsonRepr ('SchemaArray cs s)) where
485− type Item (JsonRepr ('SchemaArray cs s)) = JsonRepr s
486− fromList = ReprArray . GHC.Exts.fromList
487− toList (ReprArray v) = GHC.Exts.toList v
488−
489−instance Num (JsonRepr ('SchemaNumber cs)) where
490− ReprNumber a + ReprNumber b = ReprNumber $ a + b
491− ReprNumber a - ReprNumber b = ReprNumber $ a - b
492− ReprNumber a * ReprNumber b = ReprNumber $ a * b
493− abs (ReprNumber a) = ReprNumber $ abs a
494− signum (ReprNumber a) = ReprNumber $ signum a
495− fromInteger = ReprNumber . fromIntegral
496−
497−instance IsString (JsonRepr ('SchemaText cs)) where
498− fromString = ReprText . fromString
499−
500−fromOptional
501− :: SingI s
502− => Sing ('SchemaOptional s)
503− -> J.Value
504− -> Parser (Maybe (JsonRepr s))
505−fromOptional _ = parseJSON
506−
507−parseUnion
508− :: FromJSON (JsonRepr ('SchemaUnion ss))
509− => sing (ss :: [Schema])
510− -> Value
511− -> Parser (JsonRepr ('SchemaUnion ss))
512−parseUnion _ val = parseJSON val
513−
514−instance FromJSON (Union JsonRepr '[]) where
515− parseJSON = fail "empty union"
516−
517−instance (SingI a, FromJSON (Union JsonRepr as)) => FromJSON (Union JsonRepr (a ': as)) where
518− parseJSON val = (This <$> parseJSON val)
519− <|> (That <$> (parseJSON val :: Parser (Union JsonRepr as)))
520−
521−instance ToJSON (Union JsonRepr as) where
522− toJSON (This fa) = toJSON fa
523− toJSON (That u) = toJSON u
524−
525−instance SingI schema => J.FromJSON (JsonRepr schema) where
526− parseJSON value = case sing :: Sing schema of
527− SSchemaText _ -> withText "String" (pure . ReprText) value
528− SSchemaNumber _ -> withScientific "Number" (pure . ReprNumber) value
529− SSchemaBoolean -> ReprBoolean <$> parseJSON value
530− SSchemaNull -> case value of
531− J.Null -> pure ReprNull
532− _ -> typeMismatch "Null" value
533− so@(SSchemaOptional s) -> withSingI s $ ReprOptional <$> fromOptional so value
534− SSchemaArray sa sb -> withSingI sa $ withSingI sb
535− $ withArray "Array" (fmap ReprArray . traverse parseJSON) value
536− SSchemaObject fs -> do
537− let
538− demoteFields :: SList s -> H.HashMap Text J.Value -> Parser (Rec FieldRepr s)
539− demoteFields SNil _ = pure RNil
540− demoteFields (SCons (STuple2 (n :: Sing fn) s) tl) h = withKnownSymbol n $ do
541− let fieldName = T.pack $ symbolVal (Proxy @fn)
542− fieldRepr <- case s of
543− SSchemaText so -> case H.lookup fieldName h of
544− Just v -> withSingI so $ FieldRepr <$> parseJSON v
545− Nothing -> fail $ "No text field: " P.++ show fieldName
546− SSchemaNumber so -> case H.lookup fieldName h of
547− Just v -> withSingI so $ FieldRepr <$> parseJSON v
548− Nothing -> fail $ "No number field: " P.++ show fieldName
549− SSchemaBoolean -> case H.lookup fieldName h of
550− Just v -> FieldRepr <$> parseJSON v
551− Nothing -> fail $ "No boolean field: " P.++ show fieldName
552− SSchemaNull -> case H.lookup fieldName h of
553− Just v -> FieldRepr <$> parseJSON v
554− Nothing -> fail $ "No null field: " P.++ show fieldName
555− SSchemaArray sa sb -> case H.lookup fieldName h of
556− Just v -> withSingI sa $ withSingI sb $ FieldRepr <$> parseJSON v
557− Nothing -> fail $ "No array field: " P.++ show fieldName
558− SSchemaObject so -> case H.lookup fieldName h of
559− Just v -> withSingI so $ FieldRepr <$> parseJSON v
560− Nothing -> fail $ "No object field" P.++ show fieldName
561− SSchemaOptional so -> case H.lookup fieldName h of
562− Just v -> withSingI so $ FieldRepr <$> parseJSON v
563− Nothing -> withSingI so $ pure $ FieldRepr $ ReprOptional Nothing
564− SSchemaUnion ss -> withSingI ss $ FieldRepr <$> parseUnion ss value
565− (fieldRepr :&) <$> demoteFields tl h
566− ReprObject <$> withObject "Object" (demoteFields fs) value
567− SSchemaUnion ss -> parseUnion ss value
568−
569−instance J.ToJSON (JsonRepr a) where
570− toJSON ReprNull = J.Null
571− toJSON (ReprBoolean b) = J.Bool b
572− toJSON (ReprText t) = J.String t
573− toJSON (ReprNumber n) = J.Number n
574− toJSON (ReprOptional s) = case s of
575− Just v -> toJSON v
576− Nothing -> J.Null
577− toJSON (ReprArray v) = J.Array $ toJSON <$> v
578− toJSON (ReprObject r) = J.Object . H.fromList . fold $ r
579− where
580− extract :: forall name s . (KnownSymbol name)
581− => FieldRepr '(name, s)
582− -> (Text, Value)
583− extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
584− fold :: Rec FieldRepr fs -> [(Text, J.Value)]
585− fold = \case
586− RNil -> []
587− fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
588− toJSON (ReprUnion u) = toJSON u
589−
590−class FalseConstraint a
591−
592−type family TopLevel (schema :: Schema) :: Constraint where
593− TopLevel ('SchemaArray acs s) = ()
594− TopLevel ('SchemaObject o) = ()
595− TopLevel spec = 'True ~ 'False
108+class SchemaConstructor jty where
109+ constructor :: Proxy jty -> [CRepr jty] -> Schema
110+
111+instance SchemaConstructor 'JText where
112+ constructor _ = SchemaText
113+
114+instance SchemaConstructor 'JNumber where
115+ constructor _ = SchemaNumber
116+
117+instance SchemaConstructor 'JObject where
118+ constructor _ = SchemaObject
119+
120+class (SchemaConstructor (JT ty)) => Schematic ty where
121+ type JT (ty :: k) :: JType
122+ build :: Proxy ty -> Schema
123+
124+data SText cs
125+
126+instance (Verifiable 'JText cs) => Schematic (SText cs) where
127+ type JT (SText cs) = 'JText
128+ build _ = constructor (Proxy @(JT (SText cs))) $ schema (Proxy @JText) (Proxy @cs)
129+
130+data SNumber cs
131+
132+instance (Verifiable 'JNumber cs) => Schematic (SNumber cs) where
133+ type JT (SNumber cs) = 'JNumber
134+ build _ = constructor (Proxy @(JT (SNumber cs))) $ schema (Proxy @'JNumber) (Proxy @cs)
135+
136+instance (Verifiable (JT ty) cs, SchemaConstructor (JT ty)) => Schematic (Field field ty cs) where
137+ type JT (Field field ty cs) = JT ty
138+ build _ = constructor (Proxy @(JT (Field field ty cs)))
139+ $ schema (Proxy @(JT (Field field ty cs))) (Proxy @cs)
140+
141+data SObject els
142+
143+instance (Verifiable 'JObject els) => Schematic (SObject els) where
144+ type JT (SObject els) = 'JObject
145+ build _ =
146+ constructor (Proxy @(JT (SObject els)))
147+ $ schema (Proxy @(JT (SObject els))) (Proxy @els)
148+
149+-- | Shows it's top-level definition according to the json-schema
150+class TopLevel spec
151+
152+instance Schematic (SObject els) => TopLevel (SObject els)
153+
154+-- | TODO: abstract over objects and arrays
155+-- toSchema
156+-- :: forall els (e :: [k]). (e ~ '[], Verifiable (JT (SObject els)) e, Schematic (SObject els))
157+-- => Proxy (SObject els)
158+-- -> Schema
159+-- toSchema p = constructor p $ schema (Proxy @(JT (SObject els))) (Proxy @els)