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