@@ -1,20 +1,24 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+
13module Data.Schematic.Validation where
24
5+import Control.Applicative
36import Control.Monad
47import Control.Monad.Validation
58import Data.Aeson
6−import Data.Aeson.Internal
79import Data.Aeson.Types
10+import Data.Coerce
811import Data.Foldable
912import Data.Functor.Identity
1013import Data.Monoid
1114import Data.Schematic.Path
1215import Data.Schematic.Schema
1316import Data.Scientific
14−import Data.Singletons.Prelude
17+import Data.Singletons.Prelude hiding (Const)
1518import Data.Singletons.TypeLits
1619import Data.Text as T
1720import Data.Traversable
21+import Data.Type.Equality
1822import Data.Union
1923import Data.Vector as V
2024import Data.Vinyl
@@ -50,51 +54,51 @@ isValidationError (ValidationError _) = True
5054isValidationError _ = False
5155
5256validateTextConstraint
53− :: JSONPathText
57+ :: JSONPath
5458 -> Text
5559 -> Sing (tcs :: TextConstraint)
5660 -> Validation ()
57−validateTextConstraint (JSONPathText path) t = \case
61+validateTextConstraint (JSONPath path) t = \case
5862 STEq n -> do
5963 let
6064 nlen = withKnownNat n $ natVal n
6165 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)
6367 warn = vWarning $ mmSingleton path (pure errMsg)
6468 unless predicate warn
6569 STLt n -> do
6670 let
6771 nlen = withKnownNat n $ natVal n
6872 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)
7074 warn = vWarning $ mmSingleton path (pure errMsg)
7175 unless predicate warn
7276 STLe n -> do
7377 let
7478 nlen = withKnownNat n $ natVal n
7579 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)
7781 warn = vWarning $ mmSingleton path (pure errMsg)
7882 unless predicate warn
7983 STGt n -> do
8084 let
8185 nlen = withKnownNat n $ natVal n
8286 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)
8488 warn = vWarning $ mmSingleton path (pure errMsg)
8589 unless predicate warn
8690 STGe n -> do
8791 let
8892 nlen = withKnownNat n $ natVal n
8993 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)
9195 warn = vWarning $ mmSingleton path (pure errMsg)
9296 unless predicate warn
9397 STRegex r -> do
9498 let
9599 regex = withKnownSymbol r $ fromSing r
96100 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
97− errMsg = "must match " <> regex
101+ errMsg = path <> " must match " <> regex
98102 warn = vWarning $ mmSingleton path (pure errMsg)
99103 unless predicate warn
100104 STEnum ss -> do
@@ -102,101 +106,76 @@ validateTextConstraint (JSONPathText path) t = \case
102106 matching :: Sing (s :: [Symbol]) -> Bool
103107 matching SNil = False
104108 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))
106110 warn = vWarning $ mmSingleton path (pure errMsg)
107111 unless (matching ss) warn
108112
109113validateNumberConstraint
110− :: JSONPathText
114+ :: JSONPath
111115 -> Scientific
112116 -> Sing (tcs :: NumberConstraint)
113117 -> Validation ()
114−validateNumberConstraint (JSONPathText path) num = \case
118+validateNumberConstraint (JSONPath path) num = \case
115119 SNEq n -> do
116120 let
117121 nlen = withKnownNat n $ natVal n
118122 predicate = fromIntegral nlen == num
119− errMsg = "should be == " <> T.pack (show nlen)
123+ errMsg = path <> " should be == " <> T.pack (show nlen)
120124 warn = vWarning $ mmSingleton path (pure errMsg)
121125 unless predicate warn
122126 SNGt n -> do
123127 let
124128 nlen = withKnownNat n $ natVal n
125129 predicate = num > fromIntegral nlen
126− errMsg = "should be > " <> T.pack (show nlen)
130+ errMsg = path <> " should be > " <> T.pack (show nlen)
127131 warn = vWarning $ mmSingleton path (pure errMsg)
128132 unless predicate warn
129133 SNGe n -> do
130134 let
131135 nlen = withKnownNat n $ natVal n
132136 predicate = num >= fromIntegral nlen
133− errMsg = "should be >= " <> T.pack (show nlen)
137+ errMsg = path <> " should be >= " <> T.pack (show nlen)
134138 warn = vWarning $ mmSingleton path (pure errMsg)
135139 unless predicate warn
136140 SNLt n -> do
137141 let
138142 nlen = withKnownNat n $ natVal n
139143 predicate = num < fromIntegral nlen
140− errMsg = "should be < " <> T.pack (show nlen)
144+ errMsg = path <> " should be < " <> T.pack (show nlen)
141145 warn = vWarning $ mmSingleton path (pure errMsg)
142146 unless predicate warn
143147 SNLe n -> do
144148 let
145149 nlen = withKnownNat n $ natVal n
146150 predicate = num <= fromIntegral nlen
147− errMsg = "should be <= " <> T.pack (show nlen)
151+ errMsg = path <> " should be <= " <> T.pack (show nlen)
148152 warn = vWarning $ mmSingleton path (pure errMsg)
149153 unless predicate warn
150154
151155validateArrayConstraint
152− :: JSONPathText
156+ :: JSONPath
153157 -> V.Vector a
154158 -> Sing (tcs :: ArrayConstraint)
155159 -> Validation ()
156−validateArrayConstraint (JSONPathText path) v = \case
160+validateArrayConstraint (JSONPath path) v = \case
157161 SAEq n -> do
158162 let
159163 nlen = withKnownNat n $ natVal n
160164 predicate = nlen == fromIntegral (V.length v)
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)
165+ errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
190166 warn = vWarning $ mmSingleton path (pure errMsg)
191167 unless predicate warn
192168
169+class Validatable schema where
170+ validateJsonRepr :: [DemotedPathSegment] -> JsonRepr schema -> Validation ()
171+
193172validateJsonRepr
194− :: Sing schema
195− -> JSONPath
173+ :: forall schema. SingI schema
174+ => [DemotedPathSegment]
196175 -> JsonRepr schema
197176 -> Validation ()
198−validateJsonRepr sschema dpath jr = case jr of
199− ReprText t -> case sschema of
177+validateJsonRepr dpath jr = withSingI (sing :: Sing schema) $ case jr of
178+ ReprText t -> case sing :: Sing schema of
200179 SSchemaText scs -> do
201180 let
202181 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -205,7 +184,7 @@ validateJsonRepr sschema dpath jr = case jr of
205184 validateTextConstraint (demotedPathToText dpath) t c
206185 process cs
207186 process scs
208− ReprNumber n -> case sschema of
187+ ReprNumber n -> case sing :: Sing schema of
209188 SSchemaNumber scs -> do
210189 let
211190 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -216,7 +195,7 @@ validateJsonRepr sschema dpath jr = case jr of
216195 process scs
217196 ReprNull -> pure ()
218197 ReprBoolean _ -> pure ()
219− ReprArray v -> case sschema of
198+ ReprArray v -> case sing :: Sing schema of
220199 SSchemaArray acs s -> do
221200 let
222201 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -226,61 +205,53 @@ validateJsonRepr sschema dpath jr = case jr of
226205 process cs
227206 process acs
228207 for_ (V.indexed v) $ \(ix, jr') -> do
229− let newPath = dpath <> pure (Index $ fromIntegral ix)
230− validateJsonRepr s newPath jr'
231− ReprOptional d -> case sschema of
208+ let newPath = dpath <> pure (DIx $ fromIntegral ix)
209+ withSingI s $ validateJsonRepr newPath jr'
210+ ReprOptional d -> case sing :: Sing schema of
232211 SSchemaOptional ss -> case d of
233− Just x -> validateJsonRepr ss dpath x
212+ Just x -> withSingI ss $ validateJsonRepr dpath x
234213 Nothing -> pure ()
235− ReprObject fs -> case sschema of
214+ ReprObject fs -> case sing :: Sing schema of
236215 SSchemaObject _ -> go fs
237216 where
238217 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
239218 go RNil = pure ()
240219 go (f@(FieldRepr d) :& ftl) = do
241− let newPath = dpath <> [Key (knownFieldName f)]
242− validateJsonRepr (knownFieldSchema f) newPath d
220+ let newPath = dpath <> [DKey (knownFieldName f)]
221+ withSingI (knownFieldSchema f)
222+ $ validateJsonRepr newPath d
243223 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
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
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)
268245
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
246+class UPeel ss where
247+ upeel :: Union JsonRepr ss -> Sing (SchemaUnion ss :: Schema) -> Validation ()
274248
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
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
281252
282−umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
283−umatch' _ u = umatch u
253+umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
254+umatch' _ = umatch
284255
285256parseAndValidateJson
286257 :: forall schema
@@ -292,7 +263,7 @@ parseAndValidateJson v =
292263 Left s -> DecodingError $ T.pack s
293264 Right jsonRepr ->
294265 let
295− validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
266+ validate = validateJsonRepr [] jsonRepr
296267 res = runIdentity . runValidationTEither $ validate
297268 in case res of
298269 Left em -> ValidationError em