@@ -1,24 +1,20 @@
1−{-# LANGUAGE AllowAmbiguousTypes #-}
3module Data.Schematic.Validation where
1module Data.Schematic.Validation where
5−import Control.Applicative
6import Control.Monad
3import Control.Monad
7import Control.Monad.Validation
4import Control.Monad.Validation
8import Data.Aeson
5import Data.Aeson
6+import Data.Aeson.Internal
9import Data.Aeson.Types
7import Data.Aeson.Types
11import Data.Foldable
8import Data.Foldable
12import Data.Functor.Identity
9import Data.Functor.Identity
13import Data.Monoid
10import Data.Monoid
14import Data.Schematic.Path
11import Data.Schematic.Path
15import Data.Schematic.Schema
12import Data.Schematic.Schema
16import Data.Scientific
13import Data.Scientific
17−import Data.Singletons.Prelude hiding (Const)
14+import Data.Singletons.Prelude
18import Data.Singletons.TypeLits
15import Data.Singletons.TypeLits
19import Data.Text as T
16import Data.Text as T
20import Data.Traversable
17import Data.Traversable
21−import Data.Type.Equality
22import Data.Union
18import Data.Union
23import Data.Vector as V
19import Data.Vector as V
24import Data.Vinyl
20import Data.Vinyl
@@ -54,51 +50,51 @@ isValidationError (ValidationError _) = True
54isValidationError _ = False
50isValidationError _ = False
56validateTextConstraint
52validateTextConstraint
57− :: JSONPath
53+ :: JSONPathText
59 -> Sing (tcs :: TextConstraint)
55 -> Sing (tcs :: TextConstraint)
60 -> Validation ()
56 -> Validation ()
61−validateTextConstraint (JSONPath path) t = \case
57+validateTextConstraint (JSONPathText path) t = \case
62 STEq n -> do
58 STEq n -> do
64 nlen = withKnownNat n $ natVal n
60 nlen = withKnownNat n $ natVal n
65 predicate = nlen == (fromIntegral $ T.length t)
61 predicate = nlen == (fromIntegral $ T.length t)
66− errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
62+ errMsg = "length should be == " <> T.pack (show nlen)
67 warn = vWarning $ mmSingleton path (pure errMsg)
63 warn = vWarning $ mmSingleton path (pure errMsg)
68 unless predicate warn
64 unless predicate warn
69 STLt n -> do
65 STLt n -> do
71 nlen = withKnownNat n $ natVal n
67 nlen = withKnownNat n $ natVal n
72 predicate = nlen > (fromIntegral $ T.length t)
68 predicate = nlen > (fromIntegral $ T.length t)
73− errMsg = "length of " <> path <> " should be < " <> T.pack (show nlen)
69+ errMsg = "length should be < " <> T.pack (show nlen)
74 warn = vWarning $ mmSingleton path (pure errMsg)
70 warn = vWarning $ mmSingleton path (pure errMsg)
75 unless predicate warn
71 unless predicate warn
76 STLe n -> do
72 STLe n -> do
78 nlen = withKnownNat n $ natVal n
74 nlen = withKnownNat n $ natVal n
79 predicate = nlen >= (fromIntegral $ T.length t)
75 predicate = nlen >= (fromIntegral $ T.length t)
80− errMsg = "length of " <> path <> " should be <= " <> T.pack (show nlen)
76+ errMsg = "length should be <= " <> T.pack (show nlen)
81 warn = vWarning $ mmSingleton path (pure errMsg)
77 warn = vWarning $ mmSingleton path (pure errMsg)
82 unless predicate warn
78 unless predicate warn
83 STGt n -> do
79 STGt n -> do
85 nlen = withKnownNat n $ natVal n
81 nlen = withKnownNat n $ natVal n
86 predicate = nlen < (fromIntegral $ T.length t)
82 predicate = nlen < (fromIntegral $ T.length t)
87− errMsg = "length of " <> path <> " should be > " <> T.pack (show nlen)
83+ errMsg = "length should be > " <> T.pack (show nlen)
88 warn = vWarning $ mmSingleton path (pure errMsg)
84 warn = vWarning $ mmSingleton path (pure errMsg)
89 unless predicate warn
85 unless predicate warn
90 STGe n -> do
86 STGe n -> do
92 nlen = withKnownNat n $ natVal n
88 nlen = withKnownNat n $ natVal n
93 predicate = nlen <= (fromIntegral $ T.length t)
89 predicate = nlen <= (fromIntegral $ T.length t)
94− errMsg = "length of " <> path <> " should be >= " <> T.pack (show nlen)
90+ errMsg = "length should be >= " <> T.pack (show nlen)
95 warn = vWarning $ mmSingleton path (pure errMsg)
91 warn = vWarning $ mmSingleton path (pure errMsg)
96 unless predicate warn
92 unless predicate warn
97 STRegex r -> do
93 STRegex r -> do
99 regex = withKnownSymbol r $ fromSing r
95 regex = withKnownSymbol r $ fromSing r
100 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
96 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
101− errMsg = path <> " must match " <> regex
97+ errMsg = "must match " <> regex
102 warn = vWarning $ mmSingleton path (pure errMsg)
98 warn = vWarning $ mmSingleton path (pure errMsg)
103 unless predicate warn
99 unless predicate warn
104 STEnum ss -> do
100 STEnum ss -> do
@@ -106,76 +102,101 @@ validateTextConstraint (JSONPath path) t = \case
106 matching :: Sing (s :: [Symbol]) -> Bool
102 matching :: Sing (s :: [Symbol]) -> Bool
107 matching SNil = False
103 matching SNil = False
108 matching (SCons s@SSym fs) = T.pack (symbolVal s) == t || matching fs
104 matching (SCons s@SSym fs) = T.pack (symbolVal s) == t || matching fs
109− errMsg = path <> " must be one of " <> T.pack (show (fromSing ss))
105+ errMsg = "must be one of " <> T.pack (show (fromSing ss))
110 warn = vWarning $ mmSingleton path (pure errMsg)
106 warn = vWarning $ mmSingleton path (pure errMsg)
111 unless (matching ss) warn
107 unless (matching ss) warn
113validateNumberConstraint
109validateNumberConstraint
114− :: JSONPath
110+ :: JSONPathText
115 -> Scientific
111 -> Scientific
116 -> Sing (tcs :: NumberConstraint)
112 -> Sing (tcs :: NumberConstraint)
117 -> Validation ()
113 -> Validation ()
118−validateNumberConstraint (JSONPath path) num = \case
114+validateNumberConstraint (JSONPathText path) num = \case
119 SNEq n -> do
115 SNEq n -> do
121 nlen = withKnownNat n $ natVal n
117 nlen = withKnownNat n $ natVal n
122 predicate = fromIntegral nlen == num
118 predicate = fromIntegral nlen == num
123− errMsg = path <> " should be == " <> T.pack (show nlen)
119+ errMsg = "should be == " <> T.pack (show nlen)
124 warn = vWarning $ mmSingleton path (pure errMsg)
120 warn = vWarning $ mmSingleton path (pure errMsg)
125 unless predicate warn
121 unless predicate warn
126 SNGt n -> do
122 SNGt n -> do
128 nlen = withKnownNat n $ natVal n
124 nlen = withKnownNat n $ natVal n
129 predicate = num > fromIntegral nlen
125 predicate = num > fromIntegral nlen
130− errMsg = path <> " should be > " <> T.pack (show nlen)
126+ errMsg = "should be > " <> T.pack (show nlen)
131 warn = vWarning $ mmSingleton path (pure errMsg)
127 warn = vWarning $ mmSingleton path (pure errMsg)
132 unless predicate warn
128 unless predicate warn
133 SNGe n -> do
129 SNGe n -> do
135 nlen = withKnownNat n $ natVal n
131 nlen = withKnownNat n $ natVal n
136 predicate = num >= fromIntegral nlen
132 predicate = num >= fromIntegral nlen
137− errMsg = path <> " should be >= " <> T.pack (show nlen)
133+ errMsg = "should be >= " <> T.pack (show nlen)
138 warn = vWarning $ mmSingleton path (pure errMsg)
134 warn = vWarning $ mmSingleton path (pure errMsg)
139 unless predicate warn
135 unless predicate warn
140 SNLt n -> do
136 SNLt n -> do
142 nlen = withKnownNat n $ natVal n
138 nlen = withKnownNat n $ natVal n
143 predicate = num < fromIntegral nlen
139 predicate = num < fromIntegral nlen
144− errMsg = path <> " should be < " <> T.pack (show nlen)
140+ errMsg = "should be < " <> T.pack (show nlen)
145 warn = vWarning $ mmSingleton path (pure errMsg)
141 warn = vWarning $ mmSingleton path (pure errMsg)
146 unless predicate warn
142 unless predicate warn
147 SNLe n -> do
143 SNLe n -> do
149 nlen = withKnownNat n $ natVal n
145 nlen = withKnownNat n $ natVal n
150 predicate = num <= fromIntegral nlen
146 predicate = num <= fromIntegral nlen
151− errMsg = path <> " should be <= " <> T.pack (show nlen)
147+ errMsg = "should be <= " <> T.pack (show nlen)
152 warn = vWarning $ mmSingleton path (pure errMsg)
148 warn = vWarning $ mmSingleton path (pure errMsg)
153 unless predicate warn
149 unless predicate warn
155validateArrayConstraint
151validateArrayConstraint
156− :: JSONPath
152+ :: JSONPathText
157 -> V.Vector a
153 -> V.Vector a
158 -> Sing (tcs :: ArrayConstraint)
154 -> Sing (tcs :: ArrayConstraint)
159 -> Validation ()
155 -> Validation ()
160−validateArrayConstraint (JSONPath path) v = \case
156+validateArrayConstraint (JSONPathText path) v = \case
161 SAEq n -> do
157 SAEq n -> do
163 nlen = withKnownNat n $ natVal n
159 nlen = withKnownNat n $ natVal n
164 predicate = nlen == fromIntegral (V.length v)
160 predicate = nlen == fromIntegral (V.length v)
165− errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
161+ errMsg = "length should be == " <> T.pack (show nlen)
162+ warn = vWarning $ mmSingleton path (pure errMsg)
163+ unless predicate warn
166+ nlen = withKnownNat n $ natVal n
167+ predicate = fromIntegral (V.length v) > nlen
168+ errMsg = "length should be > " <> T.pack (show nlen)
169+ warn = vWarning $ mmSingleton path (pure errMsg)
170+ unless predicate warn
173+ nlen = withKnownNat n $ natVal n
174+ predicate = fromIntegral (V.length v) >= nlen
175+ errMsg = "length should be >= " <> T.pack (show nlen)
176+ warn = vWarning $ mmSingleton path (pure errMsg)
177+ unless predicate warn
180+ nlen = withKnownNat n $ natVal n
181+ predicate = fromIntegral (V.length v) < nlen
182+ errMsg = "length should be < " <> T.pack (show nlen)
183+ warn = vWarning $ mmSingleton path (pure errMsg)
184+ unless predicate warn
187+ nlen = withKnownNat n $ natVal n
188+ predicate = fromIntegral (V.length v) <= nlen
189+ errMsg = "length should be <= " <> T.pack (show nlen)
166 warn = vWarning $ mmSingleton path (pure errMsg)
190 warn = vWarning $ mmSingleton path (pure errMsg)
167 unless predicate warn
191 unless predicate warn
169−class Validatable schema where
170− validateJsonRepr :: [DemotedPathSegment] -> JsonRepr schema -> Validation ()
172validateJsonRepr
193validateJsonRepr
173− :: forall schema. SingI schema
194+ :: Sing schema
174− => [DemotedPathSegment]
195+ -> JSONPath
175 -> JsonRepr schema
196 -> JsonRepr schema
176 -> Validation ()
197 -> Validation ()
177−validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
198+validateJsonRepr sschema dpath jr = case jr of
178− ReprText t -> case sing :: Sing schema of
199+ ReprText t -> case sschema of
179 SSchemaText scs -> do
200 SSchemaText scs -> do
181 process :: Sing (cs :: [TextConstraint]) -> Validation ()
202 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -184,7 +205,7 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
184 validateTextConstraint (demotedPathToText dpath) t c
205 validateTextConstraint (demotedPathToText dpath) t c
185 process cs
206 process cs
186 process scs
207 process scs
187− ReprNumber n -> case sing :: Sing schema of
208+ ReprNumber n -> case sschema of
188 SSchemaNumber scs -> do
209 SSchemaNumber scs -> do
190 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
211 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -195,7 +216,7 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
195 process scs
216 process scs
196 ReprNull -> pure ()
217 ReprNull -> pure ()
197 ReprBoolean _ -> pure ()
218 ReprBoolean _ -> pure ()
198− ReprArray v -> case sing :: Sing schema of
219+ ReprArray v -> case sschema of
199 SSchemaArray acs s -> do
220 SSchemaArray acs s -> do
201 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
222 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -205,53 +226,61 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
205 process cs
226 process cs
206 process acs
227 process acs
207 for_ (V.indexed v) $ \(ix, jr') -> do
228 for_ (V.indexed v) $ \(ix, jr') -> do
208− let newPath = dpath <> pure (DIx $ fromIntegral ix)
229+ let newPath = dpath <> pure (Index $ fromIntegral ix)
209− withSingI s $ validateJsonRepr newPath jr'
230+ validateJsonRepr s newPath jr'
210− ReprOptional d -> case sing :: Sing schema of
231+ ReprOptional d -> case sschema of
211 SSchemaOptional ss -> case d of
232 SSchemaOptional ss -> case d of
212− Just x -> withSingI ss $ validateJsonRepr dpath x
233+ Just x -> validateJsonRepr ss dpath x
213 Nothing -> pure ()
234 Nothing -> pure ()
214− ReprObject fs -> case sing :: Sing schema of
235+ ReprObject fs -> case sschema of
215 SSchemaObject _ -> go fs
236 SSchemaObject _ -> go fs
217 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
238 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
218 go RNil = pure ()
239 go RNil = pure ()
219 go (f@(FieldRepr d) :& ftl) = do
240 go (f@(FieldRepr d) :& ftl) = do
220− let newPath = dpath <> [DKey (knownFieldName f)]
241+ let newPath = dpath <> [Key (knownFieldName f)]
221− withSingI (knownFieldSchema f)
242+ validateJsonRepr (knownFieldSchema f) newPath d
222− $ validateJsonRepr newPath d
224− ReprUnion u -> pure () -- upeel u (sing :: Sing schema)
244+ ReprUnion _ -> pure () -- FIXME
225− -- ReprUnion u -> do
227− -- v :: forall s. JsonRepr s -> Const (Validation ()) s
228− -- v j = Const $ validateJsonRepr (singByProxy j) dpath j
229− -- peel :: Union (Const (Validation ())) ts -> Validation ()
230− -- peel (That u) = peel u
231− -- peel (This v) = getConst v
233− -- ReprUnion u -> do
235− -- peel :: Union JsonRepr ss -> [DemotedSchema] -> Validation ()
236− -- peel (That u) ds = peel u ds
237− -- peel (This j) ds = case ds of
238− -- [] -> error "peeling error: report this as a schematic bug"
239− -- (ds' :_) -> let s' = toSing ds'
241− -- SomeSing s -> case s `testEquality` (singByProxy j) of
242− -- Just Refl -> validateJsonRepr s dpath j
243− -- case sschema of
245+ -- case sschema of
244− -- SSchemaUnion us -> peel u (fromSing us)
246+ -- SSchemaUnion ss -> case ss of
247+ -- SCons s stl -> case umatch' s u of
248+ -- Nothing -> case urestrict u of
250+ -- fail "impossible to produce subUnion, please report this as a bug"
253+ -- JSONPathText path = demotedPathToText dpath
255+ -- SNil -> void $ vWarning $ mmSingleton path
256+ -- $ pure "union handling error, please report this as bug"
258+ -- validateJsonRepr (SSchemaUnion (SCons s' stl')) dpath
259+ -- $ toUnion (SCons s' stl') x
260+ -- Just x -> validateJsonRepr s dpath x
263+-- :: Sing (s ': stl)
264+-- -> ( USubset stl (s ': stl) (RImage stl (s ': stl))
265+-- => Union f (s ': stl)
266+-- -> Maybe (Union f stl) )
267+-- subUnion (SCons s stl) = urestrict
246−class UPeel ss where
269+-- withUSubset
247− upeel :: Union JsonRepr ss -> Sing (SchemaUnion ss :: Schema) -> Validation ()
270+-- :: Sing (s ': stl)
271+-- -> (USubset stl (s ': stl) (RImage stl (s ': stl)) => Maybe (Union f stl))
272+-- -> Maybe (Union f stl)
273+-- withUSubset (SCons s stl) r = r
249−instance (UPeel stl) => UPeel (s ': stl) where
275+toUnion
250− upeel (That u) (SSchemaUnion (SCons _ stl)) = upeel @stl u (SSchemaUnion stl)
276+ :: USubset s' (s ': ss) (RImage s' (s ': ss))
251− upeel (This j) (SSchemaUnion (SCons s _)) = withSingI s $ validateJsonRepr mempty j
277+ => Sing (s ': ss)
278+ -> Union JsonRepr s'
279+ -> JsonRepr ('SchemaUnion (s ': ss))
280+toUnion _ = ReprUnion . urelax
253−umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
282+umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
254−umatch' _ = umatch
283+umatch' _ u = umatch u
256parseAndValidateJson
285parseAndValidateJson
257 :: forall schema
286 :: forall schema
@@ -263,7 +292,7 @@ parseAndValidateJson v =
263 Left s -> DecodingError $ T.pack s
292 Left s -> DecodingError $ T.pack s
264 Right jsonRepr ->
293 Right jsonRepr ->
266− validate = validateJsonRepr [] jsonRepr
295+ validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
267 res = runIdentity . runValidationTEither $ validate
296 res = runIdentity . runValidationTEither $ validate
268 in case res of
297 in case res of
269 Left em -> ValidationError em
298 Left em -> ValidationError em