@@ -1,95 +1,138 @@
11{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE DataKinds #-}
23{-# LANGUAGE InstanceSigs #-}
4+{-# LANGUAGE TypeInType #-}
35{-# LANGUAGE UndecidableInstances #-}
46{-# OPTIONS_GHC -fprint-explicit-kinds #-}
57
68module Data.Schematic.Schema where
79
810import Data.Functor.Foldable
9−import Data.Singletons.TH
1011import Data.Kind hiding (Type)
1112import Data.Proxy
13+import Data.Singletons.TH
14+import Data.Text (Text)
1215import Data.Type.Equality
1316import Data.Vinyl
1417import Data.Vinyl.Functor
18+import GHC.Exts
1519import GHC.TypeLits (KnownNat, natVal, KnownSymbol, symbolVal, Symbol, Nat)
1620
17−singletons [d|
18− data Type els
19− = Text
20− | Number
21− | Array
22− | Object els
23− | Null
2421
25− |]
22+-- | Type Tags
23+data JType
24+ = JText
25+ | JNumber
26+ | JArray
27+ | JObject
28+ | JNull
2629
27−type family CRepr (ty :: k) :: Type els
30+type family Repr (ty :: JType) :: * where
31+ Repr 'JText = String -- because of matchRegex
32+ Repr 'JNumber = Double
2833
29−type family Repr (ty :: k1) :: k2 where
30− Repr 'Text = String -- because of matchRegex
31− Repr 'Number = Double
32−
33−class Constrained c ty where
34− predicate :: Repr ty -> Bool
34+class Constrained (ty :: JType) c where
35+ cRep :: Proxy ty -> Proxy c -> CRepr ty
3536
3637data LengthEqNat nat
3738
38−instance KnownNat nat => Constrained (LengthEqNat nat) Text where
39− predicate n = natVal (Proxy @nat) == fromIntegral (length n)
39+instance KnownNat nat => Constrained 'JText (LengthEqNat nat) where
40+ cRep _ _ = LengthEq $ natVal (Proxy @nat)
41+
42+data Field field jty schema
43+
44+instance (Schematic jty, Verifiable (JT jty) cs, KnownSymbol field)
45+ => Constrained JObject (Field field jty cs) where
46+ cRep _ _ =
47+ (symbolVal (Proxy @field), constructor (Proxy @jty) $ schema (Proxy @(JT jty)) (Proxy @cs))
48+
49+class Verifiable ty cs where
50+ schema :: Proxy ty -> Proxy cs -> [CRepr ty]
51+
52+instance Verifiable JText '[] where
53+ schema _ _ = []
54+
55+instance
56+ (Constrained JText c, Verifiable JText cs) => Verifiable JText (c ': cs) where
57+ schema _ _ = schema (Proxy @JText) (Proxy @cs) ++ schema (Proxy @JText) (Proxy @cs)
4058
41−type instance CRepr (LengthEqNat nat) = Number
59+instance Verifiable JNumber '[] where
60+ schema _ _ = []
4261
43−type family Verifiable (els :: k) (t :: z) :: Constraint where
44− Verifiable '[] ty = ()
45− Verifiable (e : els) ty = (Constrained e (CRepr e), Verifiable els ty)
62+instance
63+ (Constrained JNumber c, Verifiable JNumber cs) => Verifiable JNumber (c ': cs) where
64+ schema _ _ = schema (Proxy @JNumber) (Proxy @cs) ++ schema (Proxy @JNumber) (Proxy @cs)
4665
47−data Schema (ty :: Type k) where
48− SchemaText :: Verifiable cs Text => Rec Sing cs -> Schema Text
49− SchemaNumber :: Verifiable cs Number => Rec Sing cs -> Schema Number
50− SchemaObjCons :: (KnownSymbol label, Verifiable cs t)
51− => Proxy label
52− -> Rec Sing cs
53− -> Schema t -- new elem
54− -> Schema (Object tys) -- tail
55− -> Schema (Object (t ': tys))
56− SchemaObjNil :: Schema (Object '[])
66+instance Verifiable JObject '[] where
67+ schema _ _ = []
68+
69+instance
70+ (Constrained JObject c, Verifiable JObject cs, KnownSymbol field)
71+ => Verifiable JObject ((Field field jty c) ': cs) where
72+ schema _ _ = cRep (Proxy @JObject) (Proxy @c) : schema (Proxy @JObject) (Proxy @cs)
73+
74+type family VerifiableFields (ty :: JType) (els :: [k]) :: Constraint where
75+ VerifiableFields ty '[] = ()
76+ VerifiableFields ty ((Field f jty s) ': elss)
77+ = (Constrained jty s, VerifiableFields ty elss)
78+
79+type family CRepr (jty :: JType) :: * where
80+ CRepr JText = TextConstraint
81+ CRepr JNumber = NumberConstraint
82+ CRepr JObject = (String, Schema)
83+
84+data TextConstraint
85+ = LengthEq Integer
86+ | LengthLe Integer
87+ | LengthGt Integer
88+
89+data NumberConstraint
90+ = Le Integer
91+ | Gt Integer
92+ | Eq Integer
93+
94+data Schema
95+ = SchemaText [TextConstraint]
96+ | SchemaNumber [NumberConstraint]
97+ | SchemaObject [(String, Schema)]
98+ | SchemaArray Schema
99+
100+-- | Apply constraint for each element of list
101+type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
102+ AllSatisfy c '[] = ()
103+ AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
57104
58105class Schematic ty where
59− type SchemaOf ty :: Type t
60− rep :: Proxy ty -> Schema (SchemaOf ty)
106+ type JT ty :: JType
107+ constructor :: Proxy ty -> [CRepr (JT ty)] -> Schema
108+
109+data SText cs
61110
62−data c :% s
111+instance (Verifiable JText cs) => Schematic (SText cs) where
112+ type JT (SText cs) = JText
113+ constructor _ = SchemaText
63114
64−instance Schematic s => Schematic (c :% s) where
65− type SchemaOf (c :% s) = SchemaOf s
66− rep _ = rep $ Proxy @s
115+-- example
116+type TextSchema = SText '[LengthEqNat 3]
67117
68−data NilObj
118+data SNumber cs
69119
70−instance Schematic NilObj where
71− type SchemaOf NilObj = Object '[]
72− rep _ = SchemaObjNil
120+instance (Verifiable JNumber cs) => Schematic (SNumber cs) where
121+ type JT (SNumber cs) = JNumber
122+ constructor _ = SchemaNumber
73123
74−data (:**) (label :: Symbol) e (s :: k)
124+data SObject els
75125
76−instance (KnownSymbol label, Schematic e, Schematic s)
77− => Schematic (label :** e s) where
78− type SchemaOf (label :** e s) = SchemaOf s
79− rep _ = SchemaObjCons
80− (Proxy @label)
81− RNil
82− (rep $ Proxy @e)
83− (rep $ Proxy @s)
126+instance (els ~ '[k], AllSatisfy Schematic els) => Schematic (SObject els) where
127+ type JT (SObject els) = JObject
128+ constructor _ = SchemaObject
84129
85−data JText
130+-- | Shows it's top-level definition according to the json-schema
131+class TopLevel spec
86132
87−instance Schematic JText where
88− rep _ = SchemaText
133+instance Schematic (SObject spec) => TopLevel (SObject els)
89134
90−-- | Signals it's appropriate as a top-level json type
91−-- class Schematic ty => TopLevel ty
135+-- toSchema :: forall spec cs. (Schematic spec, VerifiableFields (JT spec), TopLevel spec) => Proxy spec -> Schema
136+-- toSchema pspec = constructor pspec $ schema (Proxy @(JT spec)) pspec
92137
93−-- -- type TestStruct
94−-- -- = "carrier" (JString :% LengthEqNat 2 :% Regexp "[a-zA-Z]+")
95−-- -- :& "booking_classes" (JArray :% (LengthArrLe 5) (JString :% Regexp "[a-zA-Z]{2}"))
138+type TestStruct = SObject '[ '("carrier", [SText '[LengthEqNat 3]]) ]