git.iko.soy/typeable/schematic
on master help sign in
singletons rewrite WIPw
760387bDenis Redozubov
schematic.cabal+4
compare with master
unifiedsplit
@@ -36,6 +36,7 @@ library
36 , InstanceSigs
36 , InstanceSigs
37 , LambdaCase
37 , LambdaCase
38 , MultiParamTypeClasses
38 , MultiParamTypeClasses
39+ , OverloadedLists
39 , OverloadedStrings
40 , OverloadedStrings
40 , PolyKinds
41 , PolyKinds
41 , QuasiQuotes
42 , QuasiQuotes
@@ -56,10 +57,12 @@ library
56 , deriving-compat
57 , deriving-compat
57 , recursion-schemes
58 , recursion-schemes
58 , regex-compat
59 , regex-compat
60+ , scientific
59 , singletons
61 , singletons
60 , text
62 , text
61 , unordered-containers
63 , unordered-containers
62 , validationt >= 0.1.0.1
64 , validationt >= 0.1.0.1
65+ , vector
63 , vinyl
66 , vinyl
64 hs-source-dirs: src
67 hs-source-dirs: src
65 default-language: Haskell2010
68 default-language: Haskell2010
@@ -81,6 +84,7 @@ test-suite spec
81 , KindSignatures
84 , KindSignatures
82 , InstanceSigs
85 , InstanceSigs
83 , MultiParamTypeClasses
86 , MultiParamTypeClasses
87+ , OverloadedLists
84 , OverloadedStrings
88 , OverloadedStrings
85 , PolyKinds
89 , PolyKinds
86 , QuasiQuotes
90 , QuasiQuotes
src/Data/Aeson/Validation.hs+58−59
@@ -9,7 +9,6 @@ import Data.Functor.Foldable
9import Data.HashMap.Strict as H
9import Data.HashMap.Strict as H
10import Data.Maybe
10import Data.Maybe
11import Data.Proxy
11import Data.Proxy
12−import Data.Schematic.Schema (TopLevel, toSchema, JT, Schematic)
13import Data.Schematic.Validation
12import Data.Schematic.Validation
14import Data.Singletons
13import Data.Singletons
15import Data.Singletons.Decide
14import Data.Singletons.Decide
@@ -22,64 +21,64 @@ import Data.Traversable
22
21
23infixl 3 <&&>
22infixl 3 <&&>
24
23
25−validateConstraint
24+-- validateConstraint
26− :: SDecide JType
25+-- :: TopLevel spec
27− => Sing jtype
26+-- => Sing spec
28− -> CRepr jtype
27+-- -> CRepr spec
29− -> Value
28+-- -> Value
30− -> Maybe Bool
29+-- -> Maybe Bool
31−validateConstraint s c = \case
30+-- validateConstraint s c = \case
32− J.String t -> case s %~ SJText of
31+-- J.String t -> case s %~ SJText of
33− Proved Refl -> pure $ case c of
32+-- Proved Refl -> pure $ case fromSing c of
34− LengthEq n -> (== n) . fromIntegral . T.length $ t
33+-- TEq n -> (== n) . fromIntegral . T.length $ t
35− LengthLe n -> (<= n) . fromIntegral . T.length $ t
34+-- TLe n -> (<= n) . fromIntegral . T.length $ t
36− LengthGt n -> (> n) . fromIntegral . T.length $ t
35+-- TGt n -> (> n) . fromIntegral . T.length $ t
37− Disproved _ -> mzero
36+-- Disproved _ -> mzero
38− J.Number i -> case s %~ SJNumber of
37+-- J.Number i -> case s %~ SJNumber of
39− Proved Refl -> pure $ case c of
38+-- Proved Refl -> pure $ case fromSing c of
40− Eq n -> i == fromIntegral n
39+-- NEq n -> i == fromIntegral n
41− Le n -> i <= fromIntegral n
40+-- NLe n -> i <= fromIntegral n
42− Gt n -> i > fromIntegral n
41+-- NGt n -> i > fromIntegral n
43− Disproved _ -> mzero
42+-- Disproved _ -> mzero
44− J.Array v -> case s %~ SJArray of
43+-- J.Array v -> case s %~ SJArray of
45− Proved Refl -> case c of
44+-- Proved Refl -> case fromSing c of
46− LengthArrEq n -> pure . (== fromIntegral n) . F.length $ v
45+-- AEq n -> pure . (== fromIntegral n) . F.length $ v
47− Disproved _ -> Nothing
46+-- Disproved _ -> Nothing
48− J.Null -> Just True
47+-- J.Null -> Just True
49− _ -> Just False
48+-- _ -> Just False
50
49
51−validateConstraints
50+-- validateConstraints
52− :: SDecide JType
51+-- :: SDecide JType
53− => Sing jtype
52+-- => Sing jtype
54− -> [CRepr jtype]
53+-- -> [CRepr jtype]
55− -> Value
54+-- -> Value
56− -> Maybe Bool
55+-- -> Maybe Bool
57−validateConstraints s cs v = and <$> traverse alg cs
56+-- validateConstraints s cs v = and <$> traverse alg cs
58− where
57+-- where
59− alg c = validateConstraint s c v
58+-- alg c = validateConstraint s c v
60
59
61−validateJson
60+-- validateJson
62− :: (SDecide JType, TopLevel spec)
61+-- :: (SDecide JType, TopLevel spec)
63− => Proxy spec
62+-- => Sing spec
64− -> Value
63+-- -> Value
65− -> Maybe Bool
64+-- -> Maybe Bool
66−validateJson ps v = let s = toSchema ps in validateBySchema s v
65+-- validateJson = validateBySchema . fromSing
67
66
68−validateBySchema
67+-- validateBySchema
69− :: SDecide JType
68+-- :: SDecide JType
70− => Schema
69+-- => Schema
71− -> Value
70+-- -> Value
72− -> Maybe Bool
71+-- -> Maybe Bool
73−validateBySchema s v = case (unfix s, v) of
72+-- validateBySchema s v = case (unfix s, v) of
74− (SchemaArray cs ss, jv@(J.Array v)) -> do
73+-- (SchemaArray cs ss, jv@(J.Array v)) -> do
75− itself <- validateConstraints SJArray cs jv
74+-- itself <- validateConstraints SJArray cs jv
76− content <- traverse (validateBySchema ss) v
75+-- content <- traverse (validateBySchema ss) v
77− pure $ itself && and content
76+-- pure $ itself && and content
78− (SchemaObject ocs, J.Object o) -> do
77+-- (SchemaObject ocs, J.Object o) -> do
79− fmap and $ for ocs $ \(fieldName, s) -> do
78+-- fmap and $ for ocs $ \(fieldName, s) -> do
80− val <- H.lookup (T.pack fieldName) o
79+-- val <- H.lookup (T.pack fieldName) o
81− validateBySchema s val
80+-- validateBySchema s val
82− (SchemaText cs, js@(J.String _)) -> validateConstraints SJText cs js
81+-- (SchemaText cs, js@(J.String _)) -> validateConstraints SJText cs js
83− (SchemaNumber cs, jn@(J.Number _)) -> validateConstraints SJNumber cs jn
82+-- (SchemaNumber cs, jn@(J.Number _)) -> validateConstraints SJNumber cs jn
84− (SchemaNull, J.Null) -> Just True
83+-- (SchemaNull, J.Null) -> Just True
85− _ -> Nothing
84+-- _ -> Nothing
src/Data/Schematic/Validation.hs+119−36
@@ -1,24 +1,32 @@
1{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE OverloadedLists #-}
3+{-# LANGUAGE OverloadedStrings #-}
2
4
3module Data.Schematic.Validation where
5module Data.Schematic.Validation where
4
6
5import Control.Applicative
7import Control.Applicative
6import Control.Category ((<<<), (>>>))
8import Control.Category ((<<<), (>>>))
9+import Data.Aeson as J
7import Data.Eq.Deriving (deriveEq1)
10import Data.Eq.Deriving (deriveEq1)
8import Data.Foldable as F
11import Data.Foldable as F
9import Data.Functor.Classes
12import Data.Functor.Classes
10import Data.Functor.Foldable
13import Data.Functor.Foldable
14+import Data.HashMap.Strict as H
11import Data.Kind
15import Data.Kind
12import Data.Maybe
16import Data.Maybe
17+import Data.Scientific
13import Data.Singletons.Decide
18import Data.Singletons.Decide
19+import Data.Singletons.Prelude.List
14import Data.Singletons.TH
20import Data.Singletons.TH
21+import Data.Singletons.TypeLits
15import Data.Text as T
22import Data.Text as T
23+import Data.Vector as V
16import Data.Vinyl hiding (Dict)
24import Data.Vinyl hiding (Dict)
17import Data.Vinyl.Functor
25import Data.Vinyl.Functor
18import Text.Show.Deriving (deriveShow1)
26import Text.Show.Deriving (deriveShow1)
19
27
20
28
21−-- | Type Tags
29+-- -- | Type Tags
22data JType
30data JType
23 = JText
31 = JText
24 | JNumber
32 | JNumber
@@ -29,52 +37,127 @@ data JType
29
37
30genSingletons [ ''JType ]
38genSingletons [ ''JType ]
31
39
32−instance Show (Sing JText) where showsPrec 4 _ = showString "SJText"
40+-- instance Show (Sing JText) where showsPrec 4 _ = showString "SJText"
33−instance Show (Sing JNumber) where showsPrec 4 _ = showString "SJNumber"
41+-- instance Show (Sing JNumber) where showsPrec 4 _ = showString "SJNumber"
34−instance Show (Sing JArray) where showsPrec 4 _ = showString "SJArray"
42+-- instance Show (Sing JArray) where showsPrec 4 _ = showString "SJArray"
35−instance Show (Sing JObject) where showsPrec 4 _ = showString "SJObject"
43+-- instance Show (Sing JObject) where showsPrec 4 _ = showString "SJObject"
36−instance Show (Sing JNull) where showsPrec 4 _ = showString "SJNull"
44+-- instance Show (Sing JNull) where showsPrec 4 _ = showString "SJNull"
37
45
38−instance Eq (Sing JText) where (==) _ _ = True
46+-- instance Eq (Sing JText) where (==) _ _ = True
39−instance Eq (Sing JNumber) where (==) _ _ = True
47+-- instance Eq (Sing JNumber) where (==) _ _ = True
40−instance Eq (Sing JArray) where (==) _ _ = True
48+-- instance Eq (Sing JArray) where (==) _ _ = True
41−instance Eq (Sing JObject) where (==) _ _ = True
49+-- instance Eq (Sing JObject) where (==) _ _ = True
42−instance Eq (Sing JNull) where (==) _ _ = True
50+-- instance Eq (Sing JNull) where (==) _ _ = True
43
51
44−type family CRepr (jty :: JType) :: Type where
52+type family CRepr (jty :: Schema) :: Type where
45− CRepr JText = TextConstraint
53+ CRepr (SchemaText cs) = TextConstraint
46− CRepr JNumber = NumberConstraint
54+ CRepr (SchemaNumber cs) = NumberConstraint
47− CRepr JObject = (String, Schema)
55+ CRepr (SchemaObject fs) = (String, Schema)
48− CRepr JArray = ArrayConstraint
56+ CRepr (SchemaArray ar s) = ArrayConstraint
49
57
50data TextConstraint
58data TextConstraint
51− = LengthEq Integer
59+ = TEq Nat
52− | LengthLe Integer
60+ | TLe Nat
53− | LengthGt Integer
61+ | TGt Nat
54− deriving (Show, Eq)
62+ | Regex Symbol
63+
64+data instance Sing (tc :: TextConstraint) where
65+ STextLengthEq :: Sing n -> Sing (TEq n)
66+ STextLengthLe :: Sing n -> Sing (TLe n)
67+ STextLengthGt :: Sing n -> Sing (TGt n)
55
68
56data NumberConstraint
69data NumberConstraint
57− = Le Integer
70+ = NLe Nat
58− | Gt Integer
71+ | NGt Nat
59− | Eq Integer
72+ | NEq Nat
60− deriving (Show, Eq)
73+
74+data instance Sing (nc :: NumberConstraint) where
75+ SNumberEq :: Sing n -> Sing (NEq n)
76+ SNumberGt :: Sing n -> Sing (NGt n)
77+ SNumberLe :: Sing n -> Sing (NLe n)
61
78
62data ArrayConstraint
79data ArrayConstraint
63− = LengthArrEq Integer
80+ = AEq Nat
64− deriving (Show, Eq)
65
81
66−type ObjectConstraint s = [(String, s)]
82+data instance Sing (ac :: ArrayConstraint) where
83+ SArrayEq :: Sing n -> Sing (AEq n)
67
84
68−data SchemaF s
85+data Schema
69 = SchemaText [TextConstraint]
86 = SchemaText [TextConstraint]
70 | SchemaNumber [NumberConstraint]
87 | SchemaNumber [NumberConstraint]
71− | SchemaObject (ObjectConstraint s)
88+ | SchemaObject [(Symbol, Schema)]
72− | SchemaArray [ArrayConstraint] s
89+ | SchemaArray [ArrayConstraint] Schema
73 | SchemaNull
90 | SchemaNull
74− deriving (Functor)
75−
76−type Schema = Fix SchemaF
77−
78−deriveEq1 ''SchemaF
79
91
80−deriveShow1 ''SchemaF
92+data instance Sing (schema :: Schema) where
93+ SSchemaText :: Sing tcs -> Sing (SchemaText tcs)
94+ SSchemaNumber :: Sing ncs -> Sing (SchemaNumber ncs)
95+ SSchemaArray :: Sing acs -> Sing schema -> Sing (SchemaArray acs schema)
96+ SSchemaObject :: Sing fields -> Sing (SchemaObject fields)
97+ SSchemaNull :: Sing SchemaNull
98+
99+type family MapSnd (l :: [(k, Schema)]) :: [Schema] where
100+ MapSnd '[] = '[]
101+ MapSnd ( '(f,s) ': tl) = s ': MapSnd tl
102+
103+data FieldRepr :: (Symbol, Schema) -> Type where
104+ FieldRepr :: KnownSymbol name => JsonRepr schema -> FieldRepr '(name, schema)
105+
106+data JsonRepr :: Schema -> Type where
107+ ReprText :: Text -> JsonRepr (SchemaText cs)
108+ ReprNumber :: Scientific -> JsonRepr (SchemaNumber cs)
109+ ReprNull :: JsonRepr SchemaNull
110+ ReprArray :: V.Vector (JsonRepr s) -> JsonRepr (SchemaArray cs s)
111+ ReprObject :: Rec FieldRepr fs -> JsonRepr (SchemaObject fs)
112+
113+instance J.ToJSON (JsonRepr a) where
114+ toJSON (ReprText t) = J.String t
115+ toJSON ReprNull = J.Null
116+ toJSON (ReprNumber n) = J.Number n
117+ toJSON (ReprArray v) = J.Array $ toJSON <$> v
118+ toJSON (ReprObject r) = let
119+ extract
120+ :: forall name s
121+ . (KnownSymbol name)
122+ => FieldRepr '(name, s)
123+ -> (Text, Value)
124+ extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
125+ fold :: Rec FieldRepr fs -> [(Text, J.Value)]
126+ fold = \case
127+ RNil -> []
128+ fr@(FieldRepr s) :& tl -> (extract fr) : fold tl
129+ in J.Object . H.fromList . fold $ r
130+
131+type Spec
132+ = SchemaObject
133+ '[ '("foo", SchemaArray '[AEq 3] (SchemaNumber '[NGt 10]))
134+ , '("bar", SchemaText '[Regex "\\w+"])]
135+
136+spec :: (SingKind Schema, SingI Spec) => DemoteRep Schema
137+spec = fromSing (sing :: Sing Spec)
138+
139+exampleTest :: JsonRepr (SchemaText '[TEq 3])
140+exampleTest = ReprText "ololo"
141+
142+exampleNumber :: JsonRepr (SchemaNumber '[NEq 3])
143+exampleNumber = ReprNumber 3
144+
145+exampleArray :: JsonRepr (SchemaArray '[AEq 1] (SchemaNumber '[NEq 3]))
146+exampleArray = ReprArray [exampleNumber]
147+
148+exampleObject
149+ :: JsonRepr (SchemaObject '[ '("foo", SchemaArray '[AEq 1] (SchemaNumber '[NEq 3]))] )
150+exampleObject = ReprObject $ FieldRepr exampleArray :& RNil
151+
152+example :: JsonRepr Spec
153+example = ReprObject $
154+ FieldRepr (ReprArray [ReprNumber 3])
155+ :& FieldRepr (ReprText "test")
156+ :& RNil
157+
158+class FalseConstraint
159+
160+type family TopLevel (spec :: Schema) :: Constraint where
161+ TopLevel (SchemaArray a e) = ()
162+ TopLevel (SchemaObject o) = ()
163+ TopLevel spec = FalseConstraint