@@ -22,14 +22,11 @@ import Data.Vector as V
2222import Data.Vinyl hiding (Dict)
2323import qualified Data.Vinyl.TypeLevel as V
2424import GHC.Generics (Generic)
25+import GHC.TypeLits (SomeNat(..), SomeSymbol(..), someSymbolVal, someNatVal)
2526import Prelude as P
2627import Test.SmallCheck.Series
2728
2829
29−type family All (c :: k -> Constraint) (s :: [k]) :: Constraint where
30− All c '[] = ()
31− All c (a ': as) = (c a, All c as)
32−
3330type family CRepr (s :: Schema) :: Type where
3431 CRepr ('SchemaText cs) = TextConstraint
3532 CRepr ('SchemaNumber cs) = NumberConstraint
@@ -46,6 +43,40 @@ data TextConstraint
4643 | TEnum [Symbol]
4744 deriving (Generic)
4845
46+instance SingKind TextConstraint where
47+ type DemoteRep TextConstraint = DemotedTextConstraint
48+ fromSing = \case
49+ STEq n -> withKnownNat n (DTEq $ natVal n)
50+ STLt n -> withKnownNat n (DTLt $ natVal n)
51+ STLe n -> withKnownNat n (DTLe $ natVal n)
52+ STGt n -> withKnownNat n (DTGt $ natVal n)
53+ STGe n -> withKnownNat n (DTGe $ natVal n)
54+ STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
55+ STEnum s -> let
56+ d :: Sing (s :: [Symbol]) -> [Text]
57+ d SNil = []
58+ d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
59+ in DTEnum $ d s
60+ toSing = \case
61+ DTEq n -> case someNatVal n of
62+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
63+ Nothing -> error "Negative singleton nat"
64+ DTLt n -> case someNatVal n of
65+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
66+ Nothing -> error "Negative singleton nat"
67+ DTLe n -> case someNatVal n of
68+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
69+ Nothing -> error "Negative singleton nat"
70+ DTGt n -> case someNatVal n of
71+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
72+ Nothing -> error "Negative singleton nat"
73+ DTGe n -> case someNatVal n of
74+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
75+ Nothing -> error "Negative singleton nat"
76+ DTRegex s -> case someSymbolVal (T.unpack s) of
77+ SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
78+ DTEnum ss -> case toSing (T.unpack <$> ss) of
79+ SomeSing l -> SomeSing (STEnum l)
4980
5081data DemotedTextConstraint
5182 = DTEq Integer
@@ -64,7 +95,7 @@ data instance Sing (tc :: TextConstraint) where
6495 STGt :: Sing n -> Sing ('TGt n)
6596 STGe :: Sing n -> Sing ('TGe n)
6697 STRegex :: Sing s -> Sing ('TRegex s)
67− STEnum :: All KnownSymbol ss => Sing ss -> Sing ('TEnum ss)
98+ STEnum :: Sing ss -> Sing ('TEnum ss)
6899
69100instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
70101instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
@@ -72,7 +103,7 @@ instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
72103instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
73104instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
74105instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
75−instance (All KnownSymbol ss, SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
106+instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
76107
77108instance Eq (Sing ('TEq n)) where _ == _ = True
78109instance Eq (Sing ('TLt n)) where _ == _ = True
@@ -117,6 +148,31 @@ instance Eq (Sing ('NLe n)) where _ == _ = True
117148instance Eq (Sing ('NGt n)) where _ == _ = True
118149instance Eq (Sing ('NGe n)) where _ == _ = True
119150
151+instance SingKind NumberConstraint where
152+ type DemoteRep NumberConstraint = DemotedNumberConstraint
153+ fromSing = \case
154+ SNEq n -> withKnownNat n (DNEq $ natVal n)
155+ SNGt n -> withKnownNat n (DNGt $ natVal n)
156+ SNGe n -> withKnownNat n (DNGe $ natVal n)
157+ SNLt n -> withKnownNat n (DNLt $ natVal n)
158+ SNLe n -> withKnownNat n (DNLe $ natVal n)
159+ toSing = \case
160+ DNEq n -> case someNatVal n of
161+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
162+ Nothing -> error "Negative singleton nat"
163+ DNGt n -> case someNatVal n of
164+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
165+ Nothing -> error "Negative singleton nat"
166+ DNGe n -> case someNatVal n of
167+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
168+ Nothing -> error "Negative singleton nat"
169+ DNLt n -> case someNatVal n of
170+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
171+ Nothing -> error "Negative singleton nat"
172+ DNLe n -> case someNatVal n of
173+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
174+ Nothing -> error "Negative singleton nat"
175+
120176data ArrayConstraint
121177 = AEq Nat
122178 deriving (Generic)
@@ -132,6 +188,15 @@ instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
132188
133189instance Eq (Sing ('AEq n)) where _ == _ = True
134190
191+instance SingKind ArrayConstraint where
192+ type DemoteRep ArrayConstraint = DemotedArrayConstraint
193+ fromSing = \case
194+ SAEq n -> withKnownNat n (DAEq $ natVal n)
195+ toSing = \case
196+ DAEq n -> case someNatVal n of
197+ Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
198+ Nothing -> error "Negative singleton nat"
199+
135200data Schema
136201 = SchemaText [TextConstraint]
137202 | SchemaNumber [NumberConstraint]
@@ -178,51 +243,32 @@ instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
178243instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
179244instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
180245
181−-- | One-way 'SingKind` variation
182−-- class SingKind' k where
183−-- type DemoteRep' k :: *
184−-- fromSing' :: Sing (a :: k) -> DemoteRep' k
185−
186−-- instance SingKind' TextConstraint where
187−-- type DemoteRep' TextConstraint = DemotedTextConstraint
188−-- fromSing' = \case
189−-- STEq n -> withKnownNat n (DTEq $ natVal n)
190−-- STLt n -> withKnownNat n (DTLt $ natVal n)
191−-- STLe n -> withKnownNat n (DTLe $ natVal n)
192−-- STGt n -> withKnownNat n (DTGt $ natVal n)
193−-- STGe n -> withKnownNat n (DTGe $ natVal n)
194−-- STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
195−-- STEnum s -> let
196−-- d :: Sing (s :: [Symbol]) -> [Text]
197−-- d SNil = []
198−-- d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
199−-- in DTEnum $ d s
200−
201−-- instance SingKind' NumberConstraint where
202−-- type DemoteRep' NumberConstraint = DemotedNumberConstraint
203−-- fromSing' = \case
204−-- SNLe n -> withKnownNat n (DNLe $ natVal n)
205−-- SNLt n -> withKnownNat n (DNLt $ natVal n)
206−-- SNGe n -> withKnownNat n (DNGe $ natVal n)
207−-- SNGt n -> withKnownNat n (DNGt $ natVal n)
208−-- SNEq n -> withKnownNat n (DNEq $ natVal n)
209−
210−-- instance SingKind' ArrayConstraint where
211−-- type DemoteRep' ArrayConstraint = DemotedArrayConstraint
212−-- fromSing' = \case
213−-- SAEq n -> withKnownNat n (DAEq $ natVal n)
214−
215−-- instance SingKind' Schema where
216−-- type DemoteRep' Schema = DemotedSchema
217−-- fromSing' = \case
218−-- SSchemaText tcs -> DSchemaText $ fromSing' tcs
219− -- SchemaText [TextConstraint]
220− -- SchemaNumber [NumberConstraint]
221− -- SchemaObject [(Symbol, Schema)]
222− -- SchemaArray [ArrayConstraint] Schema
223− -- SchemaNull
224− -- SchemaOptional Schema
225−
246+instance SingKind Schema where
247+ type DemoteRep Schema = DemotedSchema
248+ fromSing = \case
249+ SSchemaText cs -> DSchemaText $ fromSing cs
250+ SSchemaNumber cs -> DSchemaNumber $ fromSing cs
251+ SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
252+ SSchemaOptional s -> DSchemaOptional $ fromSing s
253+ SSchemaNull -> DSchemaNull
254+ SSchemaObject cs -> let
255+ dem :: Sing (s :: [(Symbol, Schema)]) -> [(Text, DemotedSchema)]
256+ dem SNil = []
257+ dem (SCons (STuple2 ss ssch) fs) = withKnownSymbol ss
258+ $ (T.pack (symbolVal ss), fromSing ssch) : dem fs
259+ in DSchemaObject $ dem cs
260+ toSing = \case
261+ DSchemaText cs -> case toSing cs of
262+ SomeSing scs -> SomeSing $ SSchemaText scs
263+ DSchemaNumber cs -> case toSing cs of
264+ SomeSing scs -> SomeSing $ SSchemaNumber scs
265+ DSchemaArray cs sch -> case (toSing cs, toSing sch) of
266+ (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
267+ DSchemaOptional sch -> case toSing sch of
268+ SomeSing ssch -> SomeSing $ SSchemaOptional ssch
269+ DSchemaNull -> SomeSing SSchemaNull
270+ DSchemaObject cs -> case toSing ((\(sym,sch) -> (T.unpack sym, sch)) <$> cs) of
271+ SomeSing scs -> SomeSing $ SSchemaObject scs
226272
227273data FieldRepr :: (Symbol, Schema) -> Type where
228274 FieldRepr