@@ -1,24 +1,20 @@
1−{-# LANGUAGE AllowAmbiguousTypes #-}
2−
31module Data.Schematic.Validation where
42
5−import Control.Applicative
63import Control.Monad
74import Control.Monad.Validation
85import Data.Aeson
6+import Data.Aeson.Internal
97import Data.Aeson.Types
10−import Data.Coerce
118import Data.Foldable
129import Data.Functor.Identity
1310import Data.Monoid
1411import Data.Schematic.Path
1512import Data.Schematic.Schema
1613import Data.Scientific
17−import Data.Singletons.Prelude hiding (Const)
14+import Data.Singletons.Prelude
1815import Data.Singletons.TypeLits
1916import Data.Text as T
2017import Data.Traversable
21−import Data.Type.Equality
2218import Data.Union
2319import Data.Vector as V
2420import Data.Vinyl
@@ -54,51 +50,51 @@ isValidationError (ValidationError _) = True
5450isValidationError _ = False
5551
5652validateTextConstraint
57− :: JSONPath
53+ :: JSONPathText
5854 -> Text
5955 -> Sing (tcs :: TextConstraint)
6056 -> Validation ()
61−validateTextConstraint (JSONPath path) t = \case
57+validateTextConstraint (JSONPathText path) t = \case
6258 STEq n -> do
6359 let
6460 nlen = withKnownNat n $ natVal n
6561 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)
6763 warn = vWarning $ mmSingleton path (pure errMsg)
6864 unless predicate warn
6965 STLt n -> do
7066 let
7167 nlen = withKnownNat n $ natVal n
7268 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)
7470 warn = vWarning $ mmSingleton path (pure errMsg)
7571 unless predicate warn
7672 STLe n -> do
7773 let
7874 nlen = withKnownNat n $ natVal n
7975 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)
8177 warn = vWarning $ mmSingleton path (pure errMsg)
8278 unless predicate warn
8379 STGt n -> do
8480 let
8581 nlen = withKnownNat n $ natVal n
8682 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)
8884 warn = vWarning $ mmSingleton path (pure errMsg)
8985 unless predicate warn
9086 STGe n -> do
9187 let
9288 nlen = withKnownNat n $ natVal n
9389 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)
9591 warn = vWarning $ mmSingleton path (pure errMsg)
9692 unless predicate warn
9793 STRegex r -> do
9894 let
9995 regex = withKnownSymbol r $ fromSing r
10096 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
101− errMsg = path <> " must match " <> regex
97+ errMsg = "must match " <> regex
10298 warn = vWarning $ mmSingleton path (pure errMsg)
10399 unless predicate warn
104100 STEnum ss -> do
@@ -106,85 +102,101 @@ validateTextConstraint (JSONPath path) t = \case
106102 matching :: Sing (s :: [Symbol]) -> Bool
107103 matching SNil = False
108104 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))
110106 warn = vWarning $ mmSingleton path (pure errMsg)
111107 unless (matching ss) warn
112108
113109validateNumberConstraint
114− :: JSONPath
110+ :: JSONPathText
115111 -> Scientific
116112 -> Sing (tcs :: NumberConstraint)
117113 -> Validation ()
118−validateNumberConstraint (JSONPath path) num = \case
114+validateNumberConstraint (JSONPathText path) num = \case
119115 SNEq n -> do
120116 let
121117 nlen = withKnownNat n $ natVal n
122118 predicate = fromIntegral nlen == num
123− errMsg = path <> " should be == " <> T.pack (show nlen)
119+ errMsg = "should be == " <> T.pack (show nlen)
124120 warn = vWarning $ mmSingleton path (pure errMsg)
125121 unless predicate warn
126122 SNGt n -> do
127123 let
128124 nlen = withKnownNat n $ natVal n
129125 predicate = num > fromIntegral nlen
130− errMsg = path <> " should be > " <> T.pack (show nlen)
126+ errMsg = "should be > " <> T.pack (show nlen)
131127 warn = vWarning $ mmSingleton path (pure errMsg)
132128 unless predicate warn
133129 SNGe n -> do
134130 let
135131 nlen = withKnownNat n $ natVal n
136132 predicate = num >= fromIntegral nlen
137− errMsg = path <> " should be >= " <> T.pack (show nlen)
133+ errMsg = "should be >= " <> T.pack (show nlen)
138134 warn = vWarning $ mmSingleton path (pure errMsg)
139135 unless predicate warn
140136 SNLt n -> do
141137 let
142138 nlen = withKnownNat n $ natVal n
143139 predicate = num < fromIntegral nlen
144− errMsg = path <> " should be < " <> T.pack (show nlen)
140+ errMsg = "should be < " <> T.pack (show nlen)
145141 warn = vWarning $ mmSingleton path (pure errMsg)
146142 unless predicate warn
147143 SNLe n -> do
148144 let
149145 nlen = withKnownNat n $ natVal n
150146 predicate = num <= fromIntegral nlen
151− errMsg = path <> " should be <= " <> T.pack (show nlen)
147+ errMsg = "should be <= " <> T.pack (show nlen)
152148 warn = vWarning $ mmSingleton path (pure errMsg)
153149 unless predicate warn
154150
155151validateArrayConstraint
156− :: JSONPath
152+ :: JSONPathText
157153 -> V.Vector a
158154 -> Sing (tcs :: ArrayConstraint)
159155 -> Validation ()
160−validateArrayConstraint (JSONPath path) v = \case
156+validateArrayConstraint (JSONPathText path) v = \case
161157 SAEq n -> do
162158 let
163159 nlen = withKnownNat n $ natVal n
164160 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
164+ SAGt n -> do
165+ let
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
171+ SAGe n -> do
172+ let
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
178+ SALt n -> do
179+ let
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
185+ SALe n -> do
186+ let
187+ nlen = withKnownNat n $ natVal n
188+ predicate = fromIntegral (V.length v) <= nlen
189+ errMsg = "length should be <= " <> T.pack (show nlen)
166190 warn = vWarning $ mmSingleton path (pure errMsg)
167191 unless predicate warn
168192
169−lookaheadJsonRepr
170− :: forall schema. (SingI schema)
171− => [DemotedPathSegment]
193+validateJsonRepr
194+ :: Sing schema
195+ -> JSONPath
172196 -> JsonRepr schema
173197 -> Validation ()
174−lookaheadJsonRepr dpath jr = case sing :: Sing schema of
175− SSchemaText s -> validateJsonRepr @schema dpath jr
176− SSchemaNumber s -> validateJsonRepr @schema dpath jr
177− SSchemaNull -> validateJsonRepr @schema dpath jr
178− SSchemaBoolean -> validateJsonRepr @schema dpath jr
179− SSchemaArray _ _ -> validateJsonRepr @schema dpath jr
180− SSchemaObject _ -> validateJsonRepr @schema dpath jr
181− SSchemaUnion _ -> validateJsonRepr @schema dpath jr
182−
183−class Validatable schema where
184− validateJsonRepr :: [DemotedPathSegment] -> JsonRepr schema -> Validation ()
185−
186−instance SingI (SchemaText s) => Validatable (SchemaText s) where
187− validateJsonRepr dpath (ReprText t) = case sing :: Sing (SchemaText s) of
198+validateJsonRepr sschema dpath jr = case jr of
199+ ReprText t -> case sschema of
188200 SSchemaText scs -> do
189201 let
190202 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -193,9 +205,7 @@ instance SingI (SchemaText s) => Validatable (SchemaText s) where
193205 validateTextConstraint (demotedPathToText dpath) t c
194206 process cs
195207 process scs
196−
197−instance SingI (SchemaNumber s) => Validatable (SchemaNumber s) where
198− validateJsonRepr dpath (ReprNumber n) = case sing :: Sing (SchemaNumber s) of
208+ ReprNumber n -> case sschema of
199209 SSchemaNumber scs -> do
200210 let
201211 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -204,13 +214,9 @@ instance SingI (SchemaNumber s) => Validatable (SchemaNumber s) where
204214 validateNumberConstraint (demotedPathToText dpath) n c
205215 process cs
206216 process scs
207−
208−instance Validatable SchemaNull where validateJsonRepr _ _ = pure ()
209−
210−instance Validatable SchemaBoolean where validateJsonRepr _ _ = pure ()
211−
212−instance SingI (SchemaArray css s) => Validatable (SchemaArray css s) where
213− validateJsonRepr dpath (ReprArray v) = case sing :: Sing (SchemaArray css s) of
217+ ReprNull -> pure ()
218+ ReprBoolean _ -> pure ()
219+ ReprArray v -> case sschema of
214220 SSchemaArray acs s -> do
215221 let
216222 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -220,60 +226,61 @@ instance SingI (SchemaArray css s) => Validatable (SchemaArray css s) where
220226 process cs
221227 process acs
222228 for_ (V.indexed v) $ \(ix, jr') -> do
223− let newPath = dpath <> pure (DIx $ fromIntegral ix)
224− withSingI s $ lookaheadJsonRepr newPath jr'
225−
226−instance SingI (SchemaOptional s) => Validatable (SchemaOptional s) where
227− validateJsonRepr dpath (ReprOptional s) = case sing :: Sing (SchemaOptional s) of
228− SSchemaOptional ss -> case s of
229− Just x -> withSingI ss $ lookaheadJsonRepr dpath x
229+ let newPath = dpath <> pure (Index $ fromIntegral ix)
230+ validateJsonRepr s newPath jr'
231+ ReprOptional d -> case sschema of
232+ SSchemaOptional ss -> case d of
233+ Just x -> validateJsonRepr ss dpath x
230234 Nothing -> pure ()
231−
232−instance SingI (SchemaObject s) => Validatable (SchemaObject s) where
233− validateJsonRepr dpath (ReprObject fs) = case sing :: Sing (SchemaObject s) of
235+ ReprObject fs -> case sschema of
234236 SSchemaObject _ -> go fs
235237 where
236238 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
237239 go RNil = pure ()
238240 go (f@(FieldRepr d) :& ftl) = do
239− let newPath = dpath <> [DKey (knownFieldName f)]
240− withSingI (knownFieldSchema f)
241− $ lookaheadJsonRepr newPath d
241+ let newPath = dpath <> [Key (knownFieldName f)]
242+ validateJsonRepr (knownFieldSchema f) newPath d
242243 go ftl
244+ ReprUnion _ -> pure () -- FIXME
245+ -- case sschema of
246+ -- SSchemaUnion ss -> case ss of
247+ -- SCons s stl -> case umatch' s u of
248+ -- Nothing -> case urestrict u of
249+ -- Nothing ->
250+ -- fail "impossible to produce subUnion, please report this as a bug"
251+ -- Just x -> do
252+ -- let
253+ -- JSONPathText path = demotedPathToText dpath
254+ -- case stl of
255+ -- SNil -> void $ vWarning $ mmSingleton path
256+ -- $ pure "union handling error, please report this as bug"
257+ -- SCons s' stl' ->
258+ -- validateJsonRepr (SSchemaUnion (SCons s' stl')) dpath
259+ -- $ toUnion (SCons s' stl') x
260+ -- Just x -> validateJsonRepr s dpath x
243261
244−instance SingI (SchemaUnion s) => Validatable (SchemaUnion s) where
245− validateJsonRepr dpath (ReprUnion u) = pure ()
246−
247− -- ReprUnion u -> do
248− -- let
249− -- v :: forall s. JsonRepr s -> Const (Validation ()) s
250− -- v j = Const $ validateJsonRepr (singByProxy j) dpath j
251− -- peel :: Union (Const (Validation ())) ts -> Validation ()
252− -- peel (That u) = peel u
253− -- peel (This v) = getConst v
254− -- peel (umap v u)
255− -- ReprUnion u -> do
256− -- let
257− -- peel :: Union JsonRepr ss -> [DemotedSchema] -> Validation ()
258− -- peel (That u) ds = peel u ds
259− -- peel (This j) ds = case ds of
260− -- [] -> error "peeling error: report this as a schematic bug"
261− -- (ds' :_) -> let s' = toSing ds'
262− -- in case s' of
263− -- SomeSing s -> case s `testEquality` (singByProxy j) of
264− -- Just Refl -> validateJsonRepr s dpath j
265− -- case sschema of
266− -- SSchemaUnion us -> peel u (fromSing us)
262+-- subUnion
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
267268
268−class UPeel ss where
269− upeel :: Union JsonRepr ss -> Sing (SchemaUnion ss :: Schema) -> Validation ()
269+-- withUSubset
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
270274
271−instance (UPeel stl) => UPeel (s ': stl) where
272− upeel (That u) (SSchemaUnion (SCons _ stl)) = upeel @stl u (SSchemaUnion stl)
273− upeel (This j) (SSchemaUnion (SCons s _)) = withSingI s $ lookaheadJsonRepr mempty j
275+toUnion
276+ :: USubset s' (s ': ss) (RImage s' (s ': ss))
277+ => Sing (s ': ss)
278+ -> Union JsonRepr s'
279+ -> JsonRepr ('SchemaUnion (s ': ss))
280+toUnion _ = ReprUnion . urelax
274281
275−umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
276−umatch' _ = umatch
282+umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
283+umatch' _ u = umatch u
277284
278285parseAndValidateJson
279286 :: forall schema
@@ -285,7 +292,7 @@ parseAndValidateJson v =
285292 Left s -> DecodingError $ T.pack s
286293 Right jsonRepr ->
287294 let
288− validate = lookaheadJsonRepr [] jsonRepr
295+ validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
289296 res = runIdentity . runValidationTEither $ validate
290297 in case res of
291298 Left em -> ValidationError em