@@ -1,95 +1,138 @@
1{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE InstanceSigs #-}
3{-# LANGUAGE InstanceSigs #-}
4+{-# LANGUAGE TypeInType #-}
3{-# LANGUAGE UndecidableInstances #-}
5{-# LANGUAGE UndecidableInstances #-}
4{-# OPTIONS_GHC -fprint-explicit-kinds #-}
6{-# OPTIONS_GHC -fprint-explicit-kinds #-}
6module Data.Schematic.Schema where
8module Data.Schematic.Schema where
8import Data.Functor.Foldable
10import Data.Functor.Foldable
9−import Data.Singletons.TH
10import Data.Kind hiding (Type)
11import Data.Kind hiding (Type)
11import Data.Proxy
12import Data.Proxy
13+import Data.Singletons.TH
14+import Data.Text (Text)
12import Data.Type.Equality
15import Data.Type.Equality
13import Data.Vinyl
16import Data.Vinyl
14import Data.Vinyl.Functor
17import Data.Vinyl.Functor
15import GHC.TypeLits (KnownNat, natVal, KnownSymbol, symbolVal, Symbol, Nat)
19import GHC.TypeLits (KnownNat, natVal, KnownSymbol, symbolVal, Symbol, Nat)
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
29−type family Repr (ty :: k1) :: k2 where
34+class Constrained (ty :: JType) c where
30− Repr 'Text = String -- because of matchRegex
35+ cRep :: Proxy ty -> Proxy c -> CRepr ty
31− Repr 'Number = Double
33−class Constrained c ty where
34− predicate :: Repr ty -> Bool
36data LengthEqNat nat
37data LengthEqNat nat
38−instance KnownNat nat => Constrained (LengthEqNat nat) Text where
39+instance KnownNat nat => Constrained 'JText (LengthEqNat nat) where
39− predicate n = natVal (Proxy @nat) == fromIntegral (length n)
40+ cRep _ _ = LengthEq $ natVal (Proxy @nat)
42+data Field field jty schema
44+instance (Schematic jty, Verifiable (JT jty) cs, KnownSymbol field)
45+ => Constrained JObject (Field field jty cs) where
47+ (symbolVal (Proxy @field), constructor (Proxy @jty) $ schema (Proxy @(JT jty)) (Proxy @cs))
49+class Verifiable ty cs where
50+ schema :: Proxy ty -> Proxy cs -> [CRepr ty]
52+instance Verifiable JText '[] where
56+ (Constrained JText c, Verifiable JText cs) => Verifiable JText (c ': cs) where
57+ schema _ _ = schema (Proxy @JText) (Proxy @cs) ++ schema (Proxy @JText) (Proxy @cs)
41−type instance CRepr (LengthEqNat nat) = Number
59+instance Verifiable JNumber '[] where
43−type family Verifiable (els :: k) (t :: z) :: Constraint where
62+instance
44− Verifiable '[] ty = ()
63+ (Constrained JNumber c, Verifiable JNumber cs) => Verifiable JNumber (c ': cs) where
45− Verifiable (e : els) ty = (Constrained e (CRepr e), Verifiable els ty)
64+ schema _ _ = schema (Proxy @JNumber) (Proxy @cs) ++ schema (Proxy @JNumber) (Proxy @cs)
47−data Schema (ty :: Type k) where
66+instance Verifiable JObject '[] where
48− SchemaText :: Verifiable cs Text => Rec Sing cs -> Schema Text
67+ schema _ _ = []
49− SchemaNumber :: Verifiable cs Number => Rec Sing cs -> Schema Number
68+
50− SchemaObjCons :: (KnownSymbol label, Verifiable cs t)
69+instance
51− => Proxy label
70+ (Constrained JObject c, Verifiable JObject cs, KnownSymbol field)
52− -> Rec Sing cs
71+ => Verifiable JObject ((Field field jty c) ': cs) where
53− -> Schema t -- new elem
72+ schema _ _ = cRep (Proxy @JObject) (Proxy @c) : schema (Proxy @JObject) (Proxy @cs)
54− -> Schema (Object tys) -- tail
73+
55− -> Schema (Object (t ': tys))
74+type family VerifiableFields (ty :: JType) (els :: [k]) :: Constraint where
56− SchemaObjNil :: Schema (Object '[])
75+ VerifiableFields ty '[] = ()
76+ VerifiableFields ty ((Field f jty s) ': elss)
77+ = (Constrained jty s, VerifiableFields ty elss)
79+type family CRepr (jty :: JType) :: * where
80+ CRepr JText = TextConstraint
81+ CRepr JNumber = NumberConstraint
82+ CRepr JObject = (String, Schema)
95+ = SchemaText [TextConstraint]
96+ | SchemaNumber [NumberConstraint]
97+ | SchemaObject [(String, Schema)]
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)
58class Schematic ty where
105class Schematic ty where
59− type SchemaOf ty :: Type t
106+ type JT ty :: JType
60− rep :: Proxy ty -> Schema (SchemaOf ty)
107+ constructor :: Proxy ty -> [CRepr (JT ty)] -> Schema
62−data c :% s
111+instance (Verifiable JText cs) => Schematic (SText cs) where
112+ type JT (SText cs) = JText
113+ constructor _ = SchemaText
64−instance Schematic s => Schematic (c :% s) where
115+-- example
65− type SchemaOf (c :% s) = SchemaOf s
116+type TextSchema = SText '[LengthEqNat 3]
66− rep _ = rep $ Proxy @s
68−data NilObj
118+data SNumber cs
70−instance Schematic NilObj where
120+instance (Verifiable JNumber cs) => Schematic (SNumber cs) where
71− type SchemaOf NilObj = Object '[]
121+ type JT (SNumber cs) = JNumber
72− rep _ = SchemaObjNil
122+ constructor _ = SchemaNumber
74−data (:**) (label :: Symbol) e (s :: k)
124+data SObject els
76−instance (KnownSymbol label, Schematic e, Schematic s)
126+instance (els ~ '[k], AllSatisfy Schematic els) => Schematic (SObject els) where
77− => Schematic (label :** e s) where
127+ type JT (SObject els) = JObject
78− type SchemaOf (label :** e s) = SchemaOf s
128+ constructor _ = SchemaObject
79− rep _ = SchemaObjCons
85−data JText
130+-- | Shows it's top-level definition according to the json-schema
87−instance Schematic JText where
133+instance Schematic (SObject spec) => TopLevel (SObject els)
90−-- | Signals it's appropriate as a top-level json type
135+-- toSchema :: forall spec cs. (Schematic spec, VerifiableFields (JT spec), TopLevel spec) => Proxy spec -> Schema
91−-- class Schematic ty => TopLevel ty
136+-- toSchema pspec = constructor pspec $ schema (Proxy @(JT spec)) pspec
93−-- -- type TestStruct
138+type TestStruct = SObject '[ '("carrier", [SText '[LengthEqNat 3]]) ]
94−-- -- = "carrier" (JString :% LengthEqNat 2 :% Regexp "[a-zA-Z]+")
95−-- -- :& "booking_classes" (JArray :% (LengthArrLe 5) (JString :% Regexp "[a-zA-Z]{2}"))