79f8af1 · typeable/schematic

git.iko.soy/typeable/schematic

on master help sign in

SingKind instances

79f8af1Denis Redozubov9 years ago

src/Data/Schematic/JsonSchema.hs+11−11

compare with master

unifiedsplit

@@ -20,17 +20,17 @@ draft4 = "http://json-schema.org/draft-04/schema#"

20-- { D4._schemaVersion = pure draft4

21-- }

23−toJsonSchema

23+-- toJsonSchema

24− :: forall schema. (SingI schema)

24+-- :: forall schema. (SingI schema)

25− => Sing (schema :: Schema)

25+-- => Sing (schema :: Schema)

26− -> D4.Schema

26+-- -> D4.Schema

27−toJsonSchema _ = case fromSing (sing :: Sing schema) of

27+-- toJsonSchema _ = case fromSing (sing :: Sing schema) of

28− SchemaText tcs -> D4.emptySchema

28+-- SchemaText tcs -> D4.emptySchema

29− SchemaNumber ncs -> D4.emptySchema

29+-- SchemaNumber ncs -> D4.emptySchema

30− SchemaObject ocs -> D4.emptySchema

30+-- SchemaObject ocs -> D4.emptySchema

31− SchemaArray acs sch -> D4.emptySchema

31+-- SchemaArray acs sch -> D4.emptySchema

32− SchemaNull -> D4.emptySchema

32+-- SchemaNull -> D4.emptySchema

33− SchemaOptional sch -> D4.emptySchema

33+-- SchemaOptional sch -> D4.emptySchema

35-- jsonObject :: M.Map Text JsonSchema -> JsonSchema

36-- jsonObject m = JsonObject

src/Data/Schematic/Schema.hs+97−51

@@ -22,14 +22,11 @@ import Data.Vector as V

22import Data.Vinyl hiding (Dict)

23import qualified Data.Vinyl.TypeLevel as V

24import GHC.Generics (Generic)

25+import GHC.TypeLits (SomeNat(..), SomeSymbol(..), someSymbolVal, someNatVal)

25import Prelude as P

26import Prelude as P

26import Test.SmallCheck.Series

27import Test.SmallCheck.Series

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−

33type family CRepr (s :: Schema) :: Type where

30type family CRepr (s :: Schema) :: Type where

34 CRepr ('SchemaText cs) = TextConstraint

31 CRepr ('SchemaText cs) = TextConstraint

35 CRepr ('SchemaNumber cs) = NumberConstraint

32 CRepr ('SchemaNumber cs) = NumberConstraint

@@ -46,6 +43,40 @@ data TextConstraint

46 | TEnum [Symbol]

43 | TEnum [Symbol]

47 deriving (Generic)

44 deriving (Generic)

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)

50data DemotedTextConstraint

81data DemotedTextConstraint

51 = DTEq Integer

82 = DTEq Integer

@@ -64,7 +95,7 @@ data instance Sing (tc :: TextConstraint) where

64 STGt :: Sing n -> Sing ('TGt n)

95 STGt :: Sing n -> Sing ('TGt n)

65 STGe :: Sing n -> Sing ('TGe n)

96 STGe :: Sing n -> Sing ('TGe n)

66 STRegex :: Sing s -> Sing ('TRegex s)

97 STRegex :: Sing s -> Sing ('TRegex s)

67− STEnum :: All KnownSymbol ss => Sing ss -> Sing ('TEnum ss)

98+ STEnum :: Sing ss -> Sing ('TEnum ss)

69instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing

100instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing

70instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing

101instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing

@@ -72,7 +103,7 @@ instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing

72instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing

103instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing

73instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing

104instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing

74instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing

105instance (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

107

77instance Eq (Sing ('TEq n)) where _ == _ = True

108instance Eq (Sing ('TEq n)) where _ == _ = True

78instance Eq (Sing ('TLt n)) where _ == _ = True

109instance Eq (Sing ('TLt n)) where _ == _ = True

@@ -117,6 +148,31 @@ instance Eq (Sing ('NLe n)) where _ == _ = True

117instance Eq (Sing ('NGt n)) where _ == _ = True

148instance Eq (Sing ('NGt n)) where _ == _ = True

118instance Eq (Sing ('NGe n)) where _ == _ = True

149instance Eq (Sing ('NGe n)) where _ == _ = True

119

150

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+

120data ArrayConstraint

176data ArrayConstraint

121 = AEq Nat

177 = AEq Nat

122 deriving (Generic)

178 deriving (Generic)

@@ -132,6 +188,15 @@ instance KnownNat n => SingI ('AEq n) where sing = SAEq sing

132

188

133instance Eq (Sing ('AEq n)) where _ == _ = True

189instance Eq (Sing ('AEq n)) where _ == _ = True

134

190

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+

135data Schema

200data Schema

136 = SchemaText [TextConstraint]

201 = SchemaText [TextConstraint]

137 | SchemaNumber [NumberConstraint]

202 | SchemaNumber [NumberConstraint]

@@ -178,51 +243,32 @@ instance Eq (Sing ('SchemaArray as s)) where _ == _ = True

178instance Eq (Sing ('SchemaObject cs)) where _ == _ = True

243instance Eq (Sing ('SchemaObject cs)) where _ == _ = True

179instance Eq (Sing ('SchemaOptional s)) where _ == _ = True

244instance Eq (Sing ('SchemaOptional s)) where _ == _ = True

180

245

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

246+instance SingKind Schema where

187−-- type DemoteRep' TextConstraint = DemotedTextConstraint

247+ type DemoteRep Schema = DemotedSchema

188−-- fromSing' = \case

248+ fromSing = \case

189−-- STEq n -> withKnownNat n (DTEq $ natVal n)

249+ SSchemaText cs -> DSchemaText $ fromSing cs

190−-- STLt n -> withKnownNat n (DTLt $ natVal n)

250+ SSchemaNumber cs -> DSchemaNumber $ fromSing cs

191−-- STLe n -> withKnownNat n (DTLe $ natVal n)

251+ SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)

192−-- STGt n -> withKnownNat n (DTGt $ natVal n)

252+ SSchemaOptional s -> DSchemaOptional $ fromSing s

193−-- STGe n -> withKnownNat n (DTGe $ natVal n)

253+ SSchemaNull -> DSchemaNull

194−-- STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)

254+ SSchemaObject cs -> let

195−-- STEnum s -> let

196−-- d :: Sing (s :: [Symbol]) -> [Text]

255+ dem :: Sing (s :: [(Symbol, Schema)]) -> [(Text, DemotedSchema)]

197−-- d SNil = []

256+ dem SNil = []

257+ dem (SCons (STuple2 ss ssch) fs) = withKnownSymbol ss

198−-- d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs

258+ $ (T.pack (symbolVal ss), fromSing ssch) : dem fs

199−-- in DTEnum $ d s

259+ in DSchemaObject $ dem cs

200−

260+ toSing = \case

201−-- instance SingKind' NumberConstraint where

261+ DSchemaText cs -> case toSing cs of

202−-- type DemoteRep' NumberConstraint = DemotedNumberConstraint

262+ SomeSing scs -> SomeSing $ SSchemaText scs

203−-- fromSing' = \case

263+ DSchemaNumber cs -> case toSing cs of

204−-- SNLe n -> withKnownNat n (DNLe $ natVal n)

264+ SomeSing scs -> SomeSing $ SSchemaNumber scs

205−-- SNLt n -> withKnownNat n (DNLt $ natVal n)

265+ DSchemaArray cs sch -> case (toSing cs, toSing sch) of

206−-- SNGe n -> withKnownNat n (DNGe $ natVal n)

266+ (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch

207−-- SNGt n -> withKnownNat n (DNGt $ natVal n)

267+ DSchemaOptional sch -> case toSing sch of

208−-- SNEq n -> withKnownNat n (DNEq $ natVal n)

268+ SomeSing ssch -> SomeSing $ SSchemaOptional ssch

209−

269+ DSchemaNull -> SomeSing SSchemaNull

210−-- instance SingKind' ArrayConstraint where

270+ DSchemaObject cs -> case toSing ((\(sym,sch) -> (T.unpack sym, sch)) <$> cs) of

211−-- type DemoteRep' ArrayConstraint = DemotedArrayConstraint

271+ SomeSing scs -> SomeSing $ SSchemaObject scs

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−

226

272

227data FieldRepr :: (Symbol, Schema) -> Type where

273data FieldRepr :: (Symbol, Schema) -> Type where

228 FieldRepr

274 FieldRepr