@@ -1,25 +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
13−import Data.Kind
1410import Data.Monoid
1511import Data.Schematic.Path
1612import Data.Schematic.Schema
1713import Data.Scientific
18−import Data.Singletons.Prelude hiding (Const)
14+import Data.Singletons.Prelude
1915import Data.Singletons.TypeLits
2016import Data.Text as T
2117import Data.Traversable
22−import Data.Type.Equality
2318import Data.Union
2419import Data.Vector as V
2520import Data.Vinyl
@@ -55,51 +50,51 @@ isValidationError (ValidationError _) = True
5550isValidationError _ = False
5651
5752validateTextConstraint
58− :: JSONPath
53+ :: JSONPathText
5954 -> Text
6055 -> Sing (tcs :: TextConstraint)
6156 -> Validation ()
62−validateTextConstraint (JSONPath path) t = \case
57+validateTextConstraint (JSONPathText path) t = \case
6358 STEq n -> do
6459 let
6560 nlen = withKnownNat n $ natVal n
6661 predicate = nlen == (fromIntegral $ T.length t)
67− errMsg = "length of " <> path <> " should be == " <> T.pack (show nlen)
62+ errMsg = "length should be == " <> T.pack (show nlen)
6863 warn = vWarning $ mmSingleton path (pure errMsg)
6964 unless predicate warn
7065 STLt n -> do
7166 let
7267 nlen = withKnownNat n $ natVal n
7368 predicate = nlen > (fromIntegral $ T.length t)
74− errMsg = "length of " <> path <> " should be < " <> T.pack (show nlen)
69+ errMsg = "length should be < " <> T.pack (show nlen)
7570 warn = vWarning $ mmSingleton path (pure errMsg)
7671 unless predicate warn
7772 STLe n -> do
7873 let
7974 nlen = withKnownNat n $ natVal n
8075 predicate = nlen >= (fromIntegral $ T.length t)
81− errMsg = "length of " <> path <> " should be <= " <> T.pack (show nlen)
76+ errMsg = "length should be <= " <> T.pack (show nlen)
8277 warn = vWarning $ mmSingleton path (pure errMsg)
8378 unless predicate warn
8479 STGt n -> do
8580 let
8681 nlen = withKnownNat n $ natVal n
8782 predicate = nlen < (fromIntegral $ T.length t)
88− errMsg = "length of " <> path <> " should be > " <> T.pack (show nlen)
83+ errMsg = "length should be > " <> T.pack (show nlen)
8984 warn = vWarning $ mmSingleton path (pure errMsg)
9085 unless predicate warn
9186 STGe n -> do
9287 let
9388 nlen = withKnownNat n $ natVal n
9489 predicate = nlen <= (fromIntegral $ T.length t)
95− errMsg = "length of " <> path <> " should be >= " <> T.pack (show nlen)
90+ errMsg = "length should be >= " <> T.pack (show nlen)
9691 warn = vWarning $ mmSingleton path (pure errMsg)
9792 unless predicate warn
9893 STRegex r -> do
9994 let
10095 regex = withKnownSymbol r $ fromSing r
10196 predicate = matchTest (makeRegex (T.unpack regex) :: Regex) (T.unpack t)
102− errMsg = path <> " must match " <> regex
97+ errMsg = "must match " <> regex
10398 warn = vWarning $ mmSingleton path (pure errMsg)
10499 unless predicate warn
105100 STEnum ss -> do
@@ -107,85 +102,101 @@ validateTextConstraint (JSONPath path) t = \case
107102 matching :: Sing (s :: [Symbol]) -> Bool
108103 matching SNil = False
109104 matching (SCons s@SSym fs) = T.pack (symbolVal s) == t || matching fs
110− errMsg = path <> " must be one of " <> T.pack (show (fromSing ss))
105+ errMsg = "must be one of " <> T.pack (show (fromSing ss))
111106 warn = vWarning $ mmSingleton path (pure errMsg)
112107 unless (matching ss) warn
113108
114109validateNumberConstraint
115− :: JSONPath
110+ :: JSONPathText
116111 -> Scientific
117112 -> Sing (tcs :: NumberConstraint)
118113 -> Validation ()
119−validateNumberConstraint (JSONPath path) num = \case
114+validateNumberConstraint (JSONPathText path) num = \case
120115 SNEq n -> do
121116 let
122117 nlen = withKnownNat n $ natVal n
123118 predicate = fromIntegral nlen == num
124− errMsg = path <> " should be == " <> T.pack (show nlen)
119+ errMsg = "should be == " <> T.pack (show nlen)
125120 warn = vWarning $ mmSingleton path (pure errMsg)
126121 unless predicate warn
127122 SNGt n -> do
128123 let
129124 nlen = withKnownNat n $ natVal n
130125 predicate = num > fromIntegral nlen
131− errMsg = path <> " should be > " <> T.pack (show nlen)
126+ errMsg = "should be > " <> T.pack (show nlen)
132127 warn = vWarning $ mmSingleton path (pure errMsg)
133128 unless predicate warn
134129 SNGe n -> do
135130 let
136131 nlen = withKnownNat n $ natVal n
137132 predicate = num >= fromIntegral nlen
138− errMsg = path <> " should be >= " <> T.pack (show nlen)
133+ errMsg = "should be >= " <> T.pack (show nlen)
139134 warn = vWarning $ mmSingleton path (pure errMsg)
140135 unless predicate warn
141136 SNLt n -> do
142137 let
143138 nlen = withKnownNat n $ natVal n
144139 predicate = num < fromIntegral nlen
145− errMsg = path <> " should be < " <> T.pack (show nlen)
140+ errMsg = "should be < " <> T.pack (show nlen)
146141 warn = vWarning $ mmSingleton path (pure errMsg)
147142 unless predicate warn
148143 SNLe n -> do
149144 let
150145 nlen = withKnownNat n $ natVal n
151146 predicate = num <= fromIntegral nlen
152− errMsg = path <> " should be <= " <> T.pack (show nlen)
147+ errMsg = "should be <= " <> T.pack (show nlen)
153148 warn = vWarning $ mmSingleton path (pure errMsg)
154149 unless predicate warn
155150
156151validateArrayConstraint
157− :: JSONPath
152+ :: JSONPathText
158153 -> V.Vector a
159154 -> Sing (tcs :: ArrayConstraint)
160155 -> Validation ()
161−validateArrayConstraint (JSONPath path) v = \case
156+validateArrayConstraint (JSONPathText path) v = \case
162157 SAEq n -> do
163158 let
164159 nlen = withKnownNat n $ natVal n
165160 predicate = nlen == fromIntegral (V.length v)
166− 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)
167190 warn = vWarning $ mmSingleton path (pure errMsg)
168191 unless predicate warn
169192
170−lookaheadJsonRepr
171− :: forall schema. (SingI schema)
172− => [DemotedPathSegment]
193+validateJsonRepr
194+ :: Sing schema
195+ -> JSONPath
173196 -> JsonRepr schema
174197 -> Validation ()
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
198+validateJsonRepr sschema dpath jr = case jr of
199+ ReprText t -> case sschema of
189200 SSchemaText scs -> do
190201 let
191202 process :: Sing (cs :: [TextConstraint]) -> Validation ()
@@ -194,9 +205,7 @@ instance SingI (SchemaText s) => Validatable (SchemaText s) where
194205 validateTextConstraint (demotedPathToText dpath) t c
195206 process cs
196207 process scs
197−
198−instance SingI (SchemaNumber s) => Validatable (SchemaNumber s) where
199− validateJsonRepr dpath (ReprNumber n) = case sing :: Sing (SchemaNumber s) of
208+ ReprNumber n -> case sschema of
200209 SSchemaNumber scs -> do
201210 let
202211 process :: Sing (cs :: [NumberConstraint]) -> Validation ()
@@ -205,13 +214,9 @@ instance SingI (SchemaNumber s) => Validatable (SchemaNumber s) where
205214 validateNumberConstraint (demotedPathToText dpath) n c
206215 process cs
207216 process scs
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
217+ ReprNull -> pure ()
218+ ReprBoolean _ -> pure ()
219+ ReprArray v -> case sschema of
215220 SSchemaArray acs s -> do
216221 let
217222 process :: Sing (cs :: [ArrayConstraint]) -> Validation ()
@@ -221,73 +226,61 @@ instance SingI (SchemaArray css s) => Validatable (SchemaArray css s) where
221226 process cs
222227 process acs
223228 for_ (V.indexed v) $ \(ix, jr') -> do
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
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
231234 Nothing -> pure ()
232−
233−instance SingI (SchemaObject s) => Validatable (SchemaObject s) where
234− validateJsonRepr dpath (ReprObject fs) = case sing :: Sing (SchemaObject s) of
235+ ReprObject fs -> case sschema of
235236 SSchemaObject _ -> go fs
236237 where
237238 go :: Rec FieldRepr (ts :: [(Symbol, Schema)] ) -> Validation ()
238239 go RNil = pure ()
239240 go (f@(FieldRepr d) :& ftl) = do
240− let newPath = dpath <> [DKey (knownFieldName f)]
241− withSingI (knownFieldSchema f)
242− $ lookaheadJsonRepr newPath d
241+ let newPath = dpath <> [Key (knownFieldName f)]
242+ validateJsonRepr (knownFieldSchema f) 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
244261
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)
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
281268
282−class UPeel ss where
283− 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
284274
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
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
288281
289−umatch' :: UElem a as i => Sing a -> Union JsonRepr as -> Maybe (JsonRepr a)
290−umatch' _ = umatch
282+umatch' :: UElem a as i => Sing a -> Union f as -> Maybe (f a)
283+umatch' _ u = umatch u
291284
292285parseAndValidateJson
293286 :: forall schema
@@ -299,7 +292,7 @@ parseAndValidateJson v =
299292 Left s -> DecodingError $ T.pack s
300293 Right jsonRepr ->
301294 let
302− validate = lookaheadJsonRepr [] jsonRepr
295+ validate = validateJsonRepr (sing :: Sing schema) [] jsonRepr
303296 res = runIdentity . runValidationTEither $ validate
304297 in case res of
305298 Left em -> ValidationError em