@@ -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,76 +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
168−
169−class Validatable schema where
170− validateJsonRepr :: [DemotedPathSegment] -> JsonRepr schema -> Validation ()
171192
172193validateJsonRepr
173− :: forall schema. SingI schema
174− => [DemotedPathSegment]
194+ :: Sing schema
195+ -> JSONPath
175196 -> JsonRepr schema
176197 -> Validation ()
177−validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
178− ReprText t -> case sing :: Sing schema of
198+validateJsonRepr sschema dpath jr = case jr of
199+ ReprText t -> case sschema of
179200 SSchemaText scs -> do
180201 let
181202 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -184,7 +205,7 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
184205 validateTextConstraint (demotedPathToText dpath) t c
185206 process cs
186207 process scs
187− ReprNumber n -> case sing :: Sing schema of
208+ ReprNumber n -> case sschema of
188209 SSchemaNumber scs -> do
189210 let
190211 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -195,7 +216,7 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
195216 process scs
196217 ReprNull -> pure ()
197218 ReprBoolean _ -> pure ()
198− ReprArray v -> case sing :: Sing schema of
219+ ReprArray v -> case sschema of
199220 SSchemaArray acs s -> do
200221 let
201222 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -205,53 +226,61 @@ validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
205226 process cs
206227 process acs
207228 for_ (V.indexed v) $ \(ix, jr') -> do
208− let newPath = dpath <> pure (DIx $ fromIntegral ix)
209− withSingI s $ validateJsonRepr newPath jr'
210− ReprOptional d -> case sing :: Sing schema of
229+ let newPath = dpath <> pure (Index $ fromIntegral ix)
230+ validateJsonRepr s newPath jr'
231+ ReprOptional d -> case sschema of
211232 SSchemaOptional ss -> case d of
212− Just x -> withSingI ss $ validateJsonRepr dpath x
233+ Just x -> validateJsonRepr ss dpath x
213234 Nothing -> pure ()
214− ReprObject fs -> case sing :: Sing schema of
235+ ReprObject fs -> case sschema of
215236 SSchemaObject _ -> go fs
216237 where
217238 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
218239 go RNil = pure ()
219240 go (f@(FieldRepr d) :& ftl) = do
220− let newPath = dpath <> [DKey (knownFieldName f)]
221− withSingI (knownFieldSchema f)
222− $ validateJsonRepr newPath d
241+ let newPath = dpath <> [Key (knownFieldName f)]
242+ validateJsonRepr (knownFieldSchema f) newPath d
223243 go ftl
224− ReprUnion u -> pure () -- upeel u (sing :: Sing schema)
225− -- ReprUnion u -> do
226− -- let
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
232− -- peel (umap v u)
233− -- ReprUnion u -> do
234− -- let
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'
240− -- in case s' of
241− -- SomeSing s -> case s `testEquality` (singByProxy j) of
242− -- Just Refl -> validateJsonRepr s dpath j
243− -- case sschema of
244− -- SSchemaUnion us -> peel u (fromSing us)
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
261+
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
245268
246−class UPeel ss where
247− 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
248274
249−instance (UPeel stl) => UPeel (s ': stl) where
250− upeel (That u) (SSchemaUnion (SCons _ stl)) = upeel @stl u (SSchemaUnion stl)
251− upeel (This j) (SSchemaUnion (SCons s _)) = withSingI s $ validateJsonRepr 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
252281
253−umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
254−umatch' _ = umatch
282+umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
283+umatch' _ u = umatch u
255284
256285parseAndValidateJson
257286 :: forall schema
@@ -263,7 +292,7 @@ parseAndValidateJson v =
263292 Left s -> DecodingError $ T.pack s
264293 Right jsonRepr ->
265294 let
266− validate = validateJsonRepr [] jsonRepr
295+ validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
267296 res = runIdentity . runValidationTEither $ validate
268297 in case res of
269298 Left em -> ValidationError em