@@ -1,20 +1,25 @@
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
13+import Data.Kind
1014import Data.Monoid
1115import Data.Schematic.Path
1216import Data.Schematic.Schema
1317import Data.Scientific
14−import Data.Singletons.Prelude
18+import Data.Singletons.Prelude hiding (Const)
1519import Data.Singletons.TypeLits
1620import Data.Text as T
1721import Data.Traversable
22+import Data.Type.Equality
1823import Data.Union
1924import Data.Vector as V
2025import Data.Vinyl
@@ -50,51 +55,51 @@ isValidationError (ValidationError _) = True
5055isValidationError _ = False
5156
5257validateTextConstraint
53− :: JSONPathText
58+ :: JSONPath
5459 -> Text
5560 -> Sing (tcs :: TextConstraint)
5661 -> Validation ()
57−validateTextConstraint (JSONPathText path) t = \case
62+validateTextConstraint (JSONPath path) t = \case
5863 STEq n -> do
5964 let
6065 nlen = withKnownNat n $ natVal n
6166 predicate = nlen == (fromIntegral $ T.length t)
62− errMsg = "length should be == " <> T.pack (show nlen)
67+ errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
6368 warn = vWarning $ mmSingleton path (pure errMsg)
6469 unless predicate warn
6570 STLt n -> do
6671 let
6772 nlen = withKnownNat n $ natVal n
6873 predicate = nlen > (fromIntegral $ T.length t)
69− errMsg = "length should be < " <> T.pack (show nlen)
74+ errMsg = "length of " <> path <> " should be < " <> T.pack (show nlen)
7075 warn = vWarning $ mmSingleton path (pure errMsg)
7176 unless predicate warn
7277 STLe n -> do
7378 let
7479 nlen = withKnownNat n $ natVal n
7580 predicate = nlen >= (fromIntegral $ T.length t)
76− errMsg = "length should be <= " <> T.pack (show nlen)
81+ errMsg = "length of " <> path <> " should be <= " <> T.pack (show nlen)
7782 warn = vWarning $ mmSingleton path (pure errMsg)
7883 unless predicate warn
7984 STGt n -> do
8085 let
8186 nlen = withKnownNat n $ natVal n
8287 predicate = nlen < (fromIntegral $ T.length t)
83− errMsg = "length should be > " <> T.pack (show nlen)
88+ errMsg = "length of " <> path <> " should be > " <> T.pack (show nlen)
8489 warn = vWarning $ mmSingleton path (pure errMsg)
8590 unless predicate warn
8691 STGe n -> do
8792 let
8893 nlen = withKnownNat n $ natVal n
8994 predicate = nlen <= (fromIntegral $ T.length t)
90− errMsg = "length should be >= " <> T.pack (show nlen)
95+ errMsg = "length of " <> path <> " should be >= " <> T.pack (show nlen)
9196 warn = vWarning $ mmSingleton path (pure errMsg)
9297 unless predicate warn
9398 STRegex r -> do
9499 let
95100 regex = withKnownSymbol r $ fromSing r
96101 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
97− errMsg = "must match " <> regex
102+ errMsg = path <> " must match " <> regex
98103 warn = vWarning $ mmSingleton path (pure errMsg)
99104 unless predicate warn
100105 STEnum ss -> do
@@ -102,101 +107,85 @@ validateTextConstraint (JSONPathText path) t = \case
102107 matching :: Sing (s :: [Symbol]) -> Bool
103108 matching SNil = False
104109 matching (SCons s@SSym fs) = T.pack (symbolVal s) == t || matching fs
105− errMsg = "must be one of " <> T.pack (show (fromSing ss))
110+ errMsg = path <> " must be one of " <> T.pack (show (fromSing ss))
106111 warn = vWarning $ mmSingleton path (pure errMsg)
107112 unless (matching ss) warn
108113
109114validateNumberConstraint
110− :: JSONPathText
115+ :: JSONPath
111116 -> Scientific
112117 -> Sing (tcs :: NumberConstraint)
113118 -> Validation ()
114−validateNumberConstraint (JSONPathText path) num = \case
119+validateNumberConstraint (JSONPath path) num = \case
115120 SNEq n -> do
116121 let
117122 nlen = withKnownNat n $ natVal n
118123 predicate = fromIntegral nlen == num
119− errMsg = "should be == " <> T.pack (show nlen)
124+ errMsg = path <> " should be == " <> T.pack (show nlen)
120125 warn = vWarning $ mmSingleton path (pure errMsg)
121126 unless predicate warn
122127 SNGt n -> do
123128 let
124129 nlen = withKnownNat n $ natVal n
125130 predicate = num > fromIntegral nlen
126− errMsg = "should be > " <> T.pack (show nlen)
131+ errMsg = path <> " should be > " <> T.pack (show nlen)
127132 warn = vWarning $ mmSingleton path (pure errMsg)
128133 unless predicate warn
129134 SNGe n -> do
130135 let
131136 nlen = withKnownNat n $ natVal n
132137 predicate = num >= fromIntegral nlen
133− errMsg = "should be >= " <> T.pack (show nlen)
138+ errMsg = path <> " should be >= " <> T.pack (show nlen)
134139 warn = vWarning $ mmSingleton path (pure errMsg)
135140 unless predicate warn
136141 SNLt n -> do
137142 let
138143 nlen = withKnownNat n $ natVal n
139144 predicate = num < fromIntegral nlen
140− errMsg = "should be < " <> T.pack (show nlen)
145+ errMsg = path <> " should be < " <> T.pack (show nlen)
141146 warn = vWarning $ mmSingleton path (pure errMsg)
142147 unless predicate warn
143148 SNLe n -> do
144149 let
145150 nlen = withKnownNat n $ natVal n
146151 predicate = num <= fromIntegral nlen
147− errMsg = "should be <= " <> T.pack (show nlen)
152+ errMsg = path <> " should be <= " <> T.pack (show nlen)
148153 warn = vWarning $ mmSingleton path (pure errMsg)
149154 unless predicate warn
150155
151156validateArrayConstraint
152− :: JSONPathText
157+ :: JSONPath
153158 -> V.Vector a
154159 -> Sing (tcs :: ArrayConstraint)
155160 -> Validation ()
156−validateArrayConstraint (JSONPathText path) v = \case
161+validateArrayConstraint (JSONPath path) v = \case
157162 SAEq n -> do
158163 let
159164 nlen = withKnownNat n $ natVal n
160165 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)
166+ errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
190167 warn = vWarning $ mmSingleton path (pure errMsg)
191168 unless predicate warn
192169
193−validateJsonRepr
194− :: Sing schema
195− -> JSONPath
170+lookaheadJsonRepr
171+ :: forall schema. (SingI schema)
172+ => [DemotedPathSegment]
196173 -> JsonRepr schema
197174 -> Validation ()
198−validateJsonRepr sschema dpath jr = case jr of
199− ReprText t -> case sschema of
175+lookaheadJsonRepr dpath jr = case sing :: Sing schema of
176+ SSchemaText s -> validateJsonRepr @schema dpath jr
177+ SSchemaNumber s -> validateJsonRepr @schema dpath jr
178+ SSchemaNull -> validateJsonRepr @schema dpath jr
179+ SSchemaBoolean -> validateJsonRepr @schema dpath jr
180+ SSchemaArray _ _ -> validateJsonRepr @schema dpath jr
181+ SSchemaObject _ -> validateJsonRepr @schema dpath jr
182+ SSchemaUnion _ -> validateJsonRepr @schema dpath jr
183+
184+class Validatable schema where
185+ validateJsonRepr :: [DemotedPathSegment] -> JsonRepr schema -> Validation ()
186+
187+instance SingI (SchemaText s) => Validatable (SchemaText s) where
188+ validateJsonRepr dpath (ReprText t) = case sing :: Sing (SchemaText s) of
200189 SSchemaText scs -> do
201190 let
202191 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -205,7 +194,9 @@ validateJsonRepr sschema dpath jr = case jr of
205194 validateTextConstraint (demotedPathToText dpath) t c
206195 process cs
207196 process scs
208− ReprNumber n -> case sschema of
197+
198+instance SingI (SchemaNumber s) => Validatable (SchemaNumber s) where
199+ validateJsonRepr dpath (ReprNumber n) = case sing :: Sing (SchemaNumber s) of
209200 SSchemaNumber scs -> do
210201 let
211202 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -214,9 +205,13 @@ validateJsonRepr sschema dpath jr = case jr of
214205 validateNumberConstraint (demotedPathToText dpath) n c
215206 process cs
216207 process scs
217− ReprNull -> pure ()
218− ReprBoolean _ -> pure ()
219− ReprArray v -> case sschema of
208+
209+instance Validatable SchemaNull where validateJsonRepr _ _ = pure ()
210+
211+instance Validatable SchemaBoolean where validateJsonRepr _ _ = pure ()
212+
213+instance SingI (SchemaArray css s) => Validatable (SchemaArray css s) where
214+ validateJsonRepr dpath (ReprArray v) = case sing :: Sing (SchemaArray css s) of
220215 SSchemaArray acs s -> do
221216 let
222217 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -226,61 +221,73 @@ validateJsonRepr sschema dpath jr = case jr of
226221 process cs
227222 process acs
228223 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
232− SSchemaOptional ss -> case d of
233− Just x -> validateJsonRepr ss dpath x
224+ let newPath = dpath <> pure (DIx $ fromIntegral ix)
225+ withSingI s $ lookaheadJsonRepr newPath jr'
226+
227+instance SingI (SchemaOptional s) => Validatable (SchemaOptional s) where
228+ validateJsonRepr dpath (ReprOptional s) = case sing :: Sing (SchemaOptional s) of
229+ SSchemaOptional ss -> case s of
230+ Just x -> withSingI ss $ lookaheadJsonRepr dpath x
234231 Nothing -> pure ()
235− ReprObject fs -> case sschema of
232+
233+instance SingI (SchemaObject s) => Validatable (SchemaObject s) where
234+ validateJsonRepr dpath (ReprObject fs) = case sing :: Sing (SchemaObject s) of
236235 SSchemaObject _ -> go fs
237236 where
238237 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
239238 go RNil = pure ()
240239 go (f@(FieldRepr d) :& ftl) = do
241− let newPath = dpath <> [Key (knownFieldName f)]
242− validateJsonRepr (knownFieldSchema f) newPath d
240+ let newPath = dpath <> [DKey (knownFieldName f)]
241+ withSingI (knownFieldSchema f)
242+ $ lookaheadJsonRepr newPath d
243243 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
261244
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
245+instance
246+ (SingI (SchemaUnion (s ': tl)))
247+ => Validatable (SchemaUnion (s ': tl)) where
248+ validateJsonRepr dpath (ReprUnion u) = do
249+ let
250+ v :: forall s. Sing s -> JsonRepr s -> Const (Validation ()) s
251+ v s j = withSingI s $ Const $ lookaheadJsonRepr dpath j
252+ peel :: Union (Const (Validation ())) ts -> Validation ()
253+ peel (That u) = peel u
254+ peel (This v) = getConst v
255+ umap' :: (forall a . Sing a -> f a -> g a) -> SList as -> Union f as -> Union g as
256+ umap' f (SCons s' stl') = \case
257+ This a -> This (f s' a)
258+ That u -> That (umap' f stl' u)
259+ peel (umap' v sing u)
260+
261+ -- ReprUnion u -> do
262+ -- let
263+ -- v :: forall s. JsonRepr s -> Const (Validation ()) s
264+ -- v j = Const $ validateJsonRepr (singByProxy j) dpath j
265+ -- peel :: Union (Const (Validation ())) ts -> Validation ()
266+ -- peel (That u) = peel u
267+ -- peel (This v) = getConst v
268+ -- peel (umap v u)
269+ -- ReprUnion u -> do
270+ -- let
271+ -- peel :: Union JsonRepr ss -> [DemotedSchema] -> Validation ()
272+ -- peel (That u) ds = peel u ds
273+ -- peel (This j) ds = case ds of
274+ -- [] -> error "peeling error: report this as a schematic bug"
275+ -- (ds' :_) -> let s' = toSing ds'
276+ -- in case s' of
277+ -- SomeSing s -> case s `testEquality` (singByProxy j) of
278+ -- Just Refl -> validateJsonRepr s dpath j
279+ -- case sschema of
280+ -- SSchemaUnion us -> peel u (fromSing us)
268281
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
282+class UPeel ss where
283+ upeel :: Union JsonRepr ss -> Sing (SchemaUnion ss :: Schema) -> Validation ()
274284
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
285+instance (UPeel stl) => UPeel (s ': stl) where
286+ upeel (That u) (SSchemaUnion (SCons _ stl)) = upeel @stl u (SSchemaUnion stl)
287+ upeel (This j) (SSchemaUnion (SCons s _)) = withSingI s $ lookaheadJsonRepr mempty j
281288
282−umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
283−umatch' _ u = umatch u
289+umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
290+umatch' _ = umatch
284291
285292parseAndValidateJson
286293 :: forall schema
@@ -292,7 +299,7 @@ parseAndValidateJson v =
292299 Left s -> DecodingError $ T.pack s
293300 Right jsonRepr ->
294301 let
295− validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
302+ validate = lookaheadJsonRepr [] jsonRepr
296303 res = runIdentity . runValidationTEither $ validate
297304 in case res of
298305 Left em -> ValidationError em