git.iko.soy/typeable/schematic
on master help sign in
singletons rewrite WIPw
commit760387be7a7d8012363539af16fad99eb37e81d3 authorDenis Redozubov <denis.redozubov@gmail.com> dateThu 18 May 2017, 23:13 (9 years ago) parent5943faa
3 files changed+181−95
compare with master
unifiedsplit
schematic.cabal+4 src/Data/Aeson/Validation.hs+58−59 src/Data/Schematic/Validation.hs+119−36
schematic.cabal+4
@@ -36,6 +36,7 @@ library
3636 , InstanceSigs
3737 , LambdaCase
3838 , MultiParamTypeClasses
39+ , OverloadedLists
3940 , OverloadedStrings
4041 , PolyKinds
4142 , QuasiQuotes
@@ -56,10 +57,12 @@ library
5657 , deriving-compat
5758 , recursion-schemes
5859 , regex-compat
60+ , scientific
5961 , singletons
6062 , text
6163 , unordered-containers
6264 , validationt >= 0.1.0.1
65+ , vector
6366 , vinyl
6467 hs-source-dirs: src
6568 default-language: Haskell2010
@@ -81,6 +84,7 @@ test-suite spec
8184 , KindSignatures
8285 , InstanceSigs
8386 , MultiParamTypeClasses
87+ , OverloadedLists
8488 , OverloadedStrings
8589 , PolyKinds
8690 , QuasiQuotes
src/Data/Aeson/Validation.hs+58−59
@@ -9,7 +9,6 @@ import Data.Functor.Foldable
99import Data.HashMap.Strict as H
1010import Data.Maybe
1111import Data.Proxy
12−import Data.Schematic.Schema (TopLevel, toSchema, JT, Schematic)
1312import Data.Schematic.Validation
1413import Data.Singletons
1514import Data.Singletons.Decide
@@ -22,64 +21,64 @@ import Data.Traversable
2221
2322infixl 3 <&&>
2423
25−validateConstraint
26− :: SDecide JType
27− => Sing jtype
28− -> CRepr jtype
29− -> Value
30− -> Maybe Bool
31−validateConstraint s c = \case
32− J.String t -> case s %~ SJText of
33− Proved Refl -> pure $ case c of
34− LengthEq n -> (== n) . fromIntegral . T.length $ t
35− LengthLe n -> (<= n) . fromIntegral . T.length $ t
36− LengthGt n -> (> n) . fromIntegral . T.length $ t
37− Disproved _ -> mzero
38− J.Number i -> case s %~ SJNumber of
39− Proved Refl -> pure $ case c of
40− Eq n -> i == fromIntegral n
41− Le n -> i <= fromIntegral n
42− Gt n -> i > fromIntegral n
43− Disproved _ -> mzero
44− J.Array v -> case s %~ SJArray of
45− Proved Refl -> case c of
46− LengthArrEq n -> pure . (== fromIntegral n) . F.length $ v
47− Disproved _ -> Nothing
48− J.Null -> Just True
49− _ -> Just False
24+-- validateConstraint
25+-- :: TopLevel spec
26+-- => Sing spec
27+-- -> CRepr spec
28+-- -> Value
29+-- -> Maybe Bool
30+-- validateConstraint s c = \case
31+-- J.String t -> case s %~ SJText of
32+-- Proved Refl -> pure $ case fromSing c of
33+-- TEq n -> (== n) . fromIntegral . T.length $ t
34+-- TLe n -> (<= n) . fromIntegral . T.length $ t
35+-- TGt n -> (> n) . fromIntegral . T.length $ t
36+-- Disproved _ -> mzero
37+-- J.Number i -> case s %~ SJNumber of
38+-- Proved Refl -> pure $ case fromSing c of
39+-- NEq n -> i == fromIntegral n
40+-- NLe n -> i <= fromIntegral n
41+-- NGt n -> i > fromIntegral n
42+-- Disproved _ -> mzero
43+-- J.Array v -> case s %~ SJArray of
44+-- Proved Refl -> case fromSing c of
45+-- AEq n -> pure . (== fromIntegral n) . F.length $ v
46+-- Disproved _ -> Nothing
47+-- J.Null -> Just True
48+-- _ -> Just False
5049
51−validateConstraints
52− :: SDecide JType
53− => Sing jtype
54− -> [CRepr jtype]
55− -> Value
56− -> Maybe Bool
57−validateConstraints s cs v = and <$> traverse alg cs
58− where
59− alg c = validateConstraint s c v
50+-- validateConstraints
51+-- :: SDecide JType
52+-- => Sing jtype
53+-- -> [CRepr jtype]
54+-- -> Value
55+-- -> Maybe Bool
56+-- validateConstraints s cs v = and <$> traverse alg cs
57+-- where
58+-- alg c = validateConstraint s c v
6059
61−validateJson
62− :: (SDecide JType, TopLevel spec)
63− => Proxy spec
64− -> Value
65− -> Maybe Bool
66−validateJson ps v = let s = toSchema ps in validateBySchema s v
60+-- validateJson
61+-- :: (SDecide JType, TopLevel spec)
62+-- => Sing spec
63+-- -> Value
64+-- -> Maybe Bool
65+-- validateJson = validateBySchema . fromSing
6766
68−validateBySchema
69− :: SDecide JType
70− => Schema
71− -> Value
72− -> Maybe Bool
73−validateBySchema s v = case (unfix s, v) of
74− (SchemaArray cs ss, jv@(J.Array v)) -> do
75− itself <- validateConstraints SJArray cs jv
76− content <- traverse (validateBySchema ss) v
77− pure $ itself && and content
78− (SchemaObject ocs, J.Object o) -> do
79− fmap and $ for ocs $ \(fieldName, s) -> do
80− val <- H.lookup (T.pack fieldName) o
81− validateBySchema s val
82− (SchemaText cs, js@(J.String _)) -> validateConstraints SJText cs js
83− (SchemaNumber cs, jn@(J.Number _)) -> validateConstraints SJNumber cs jn
84− (SchemaNull, J.Null) -> Just True
85− _ -> Nothing
67+-- validateBySchema
68+-- :: SDecide JType
69+-- => Schema
70+-- -> Value
71+-- -> Maybe Bool
72+-- validateBySchema s v = case (unfix s, v) of
73+-- (SchemaArray cs ss, jv@(J.Array v)) -> do
74+-- itself <- validateConstraints SJArray cs jv
75+-- content <- traverse (validateBySchema ss) v
76+-- pure $ itself && and content
77+-- (SchemaObject ocs, J.Object o) -> do
78+-- fmap and $ for ocs $ \(fieldName, s) -> do
79+-- val <- H.lookup (T.pack fieldName) o
80+-- validateBySchema s val
81+-- (SchemaText cs, js@(J.String _)) -> validateConstraints SJText cs js
82+-- (SchemaNumber cs, jn@(J.Number _)) -> validateConstraints SJNumber cs jn
83+-- (SchemaNull, J.Null) -> Just True
84+-- _ -> Nothing
src/Data/Schematic/Validation.hs+119−36
@@ -1,24 +1,32 @@
11{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE OverloadedLists #-}
3+{-# LANGUAGE OverloadedStrings #-}
24
35module Data.Schematic.Validation where
46
57import Control.Applicative
68import Control.Category ((<<<), (>>>))
9+import Data.Aeson as J
710import Data.Eq.Deriving (deriveEq1)
811import Data.Foldable as F
912import Data.Functor.Classes
1013import Data.Functor.Foldable
14+import Data.HashMap.Strict as H
1115import Data.Kind
1216import Data.Maybe
17+import Data.Scientific
1318import Data.Singletons.Decide
19+import Data.Singletons.Prelude.List
1420import Data.Singletons.TH
21+import Data.Singletons.TypeLits
1522import Data.Text as T
23+import Data.Vector as V
1624import Data.Vinyl hiding (Dict)
1725import Data.Vinyl.Functor
1826import Text.Show.Deriving (deriveShow1)
1927
2028
21−-- | Type Tags
29+-- -- | Type Tags
2230data JType
2331 = JText
2432 | JNumber
@@ -29,52 +37,127 @@ data JType
2937
3038genSingletons [ ''JType ]
3139
32−instance Show (Sing JText) where showsPrec 4 _ = showString "SJText"
33−instance Show (Sing JNumber) where showsPrec 4 _ = showString "SJNumber"
34−instance Show (Sing JArray) where showsPrec 4 _ = showString "SJArray"
35−instance Show (Sing JObject) where showsPrec 4 _ = showString "SJObject"
36−instance Show (Sing JNull) where showsPrec 4 _ = showString "SJNull"
40+-- instance Show (Sing JText) where showsPrec 4 _ = showString "SJText"
41+-- instance Show (Sing JNumber) where showsPrec 4 _ = showString "SJNumber"
42+-- instance Show (Sing JArray) where showsPrec 4 _ = showString "SJArray"
43+-- instance Show (Sing JObject) where showsPrec 4 _ = showString "SJObject"
44+-- instance Show (Sing JNull) where showsPrec 4 _ = showString "SJNull"
3745
38−instance Eq (Sing JText) where (==) _ _ = True
39−instance Eq (Sing JNumber) where (==) _ _ = True
40−instance Eq (Sing JArray) where (==) _ _ = True
41−instance Eq (Sing JObject) where (==) _ _ = True
42−instance Eq (Sing JNull) where (==) _ _ = True
46+-- instance Eq (Sing JText) where (==) _ _ = True
47+-- instance Eq (Sing JNumber) where (==) _ _ = True
48+-- instance Eq (Sing JArray) where (==) _ _ = True
49+-- instance Eq (Sing JObject) where (==) _ _ = True
50+-- instance Eq (Sing JNull) where (==) _ _ = True
4351
44−type family CRepr (jty :: JType) :: Type where
45− CRepr JText = TextConstraint
46− CRepr JNumber = NumberConstraint
47− CRepr JObject = (String, Schema)
48− CRepr JArray = ArrayConstraint
52+type family CRepr (jty :: Schema) :: Type where
53+ CRepr (SchemaText cs) = TextConstraint
54+ CRepr (SchemaNumber cs) = NumberConstraint
55+ CRepr (SchemaObject fs) = (String, Schema)
56+ CRepr (SchemaArray ar s) = ArrayConstraint
4957
5058data TextConstraint
51− = LengthEq Integer
52− | LengthLe Integer
53− | LengthGt Integer
54− deriving (Show, Eq)
59+ = TEq Nat
60+ | TLe Nat
61+ | TGt Nat
62+ | Regex Symbol
63+
64+data instance Sing (tc :: TextConstraint) where
65+ STextLengthEq :: Sing n -> Sing (TEq n)
66+ STextLengthLe :: Sing n -> Sing (TLe n)
67+ STextLengthGt :: Sing n -> Sing (TGt n)
5568
5669data NumberConstraint
57− = Le Integer
58− | Gt Integer
59− | Eq Integer
60− deriving (Show, Eq)
70+ = NLe Nat
71+ | NGt Nat
72+ | NEq Nat
73+
74+data instance Sing (nc :: NumberConstraint) where
75+ SNumberEq :: Sing n -> Sing (NEq n)
76+ SNumberGt :: Sing n -> Sing (NGt n)
77+ SNumberLe :: Sing n -> Sing (NLe n)
6178
6279data ArrayConstraint
63− = LengthArrEq Integer
64− deriving (Show, Eq)
80+ = AEq Nat
6581
66−type ObjectConstraint s = [(String, s)]
82+data instance Sing (ac :: ArrayConstraint) where
83+ SArrayEq :: Sing n -> Sing (AEq n)
6784
68−data SchemaF s
85+data Schema
6986 = SchemaText [TextConstraint]
7087 | SchemaNumber [NumberConstraint]
71− | SchemaObject (ObjectConstraint s)
72− | SchemaArray [ArrayConstraint] s
88+ | SchemaObject [(Symbol, Schema)]
89+ | SchemaArray [ArrayConstraint] Schema
7390 | SchemaNull
74− deriving (Functor)
75−
76−type Schema = Fix SchemaF
77−
78−deriveEq1 ''SchemaF
7991
80−deriveShow1 ''SchemaF
92+data instance Sing (schema :: Schema) where
93+ SSchemaText :: Sing tcs -> Sing (SchemaText tcs)
94+ SSchemaNumber :: Sing ncs -> Sing (SchemaNumber ncs)
95+ SSchemaArray :: Sing acs -> Sing schema -> Sing (SchemaArray acs schema)
96+ SSchemaObject :: Sing fields -> Sing (SchemaObject fields)
97+ SSchemaNull :: Sing SchemaNull
98+
99+type family MapSnd (l :: [(k, Schema)]) :: [Schema] where
100+ MapSnd '[] = '[]
101+ MapSnd ( '(f,s) ': tl) = s ': MapSnd tl
102+
103+data FieldRepr :: (Symbol, Schema) -> Type where
104+ FieldRepr :: KnownSymbol name => JsonRepr schema -> FieldRepr '(name, schema)
105+
106+data JsonRepr :: Schema -> Type where
107+ ReprText :: Text -> JsonRepr (SchemaText cs)
108+ ReprNumber :: Scientific -> JsonRepr (SchemaNumber cs)
109+ ReprNull :: JsonRepr SchemaNull
110+ ReprArray :: V.Vector (JsonRepr s) -> JsonRepr (SchemaArray cs s)
111+ ReprObject :: Rec FieldRepr fs -> JsonRepr (SchemaObject fs)
112+
113+instance J.ToJSON (JsonRepr a) where
114+ toJSON (ReprText t) = J.String t
115+ toJSON ReprNull = J.Null
116+ toJSON (ReprNumber n) = J.Number n
117+ toJSON (ReprArray v) = J.Array $ toJSON <$> v
118+ toJSON (ReprObject r) = let
119+ extract
120+ :: forall name s
121+ . (KnownSymbol name)
122+ => FieldRepr '(name, s)
123+ -> (Text, Value)
124+ extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
125+ fold :: Rec FieldRepr fs -> [(Text, J.Value)]
126+ fold = \case
127+ RNil -> []
128+ fr@(FieldRepr s) :& tl -> (extract fr) : fold tl
129+ in J.Object . H.fromList . fold $ r
130+
131+type Spec
132+ = SchemaObject
133+ '[ '("foo", SchemaArray '[AEq 3] (SchemaNumber '[NGt 10]))
134+ , '("bar", SchemaText '[Regex "\\w+"])]
135+
136+spec :: (SingKind Schema, SingI Spec) => DemoteRep Schema
137+spec = fromSing (sing :: Sing Spec)
138+
139+exampleTest :: JsonRepr (SchemaText '[TEq 3])
140+exampleTest = ReprText "ololo"
141+
142+exampleNumber :: JsonRepr (SchemaNumber '[NEq 3])
143+exampleNumber = ReprNumber 3
144+
145+exampleArray :: JsonRepr (SchemaArray '[AEq 1] (SchemaNumber '[NEq 3]))
146+exampleArray = ReprArray [exampleNumber]
147+
148+exampleObject
149+ :: JsonRepr (SchemaObject '[ '("foo", SchemaArray '[AEq 1] (SchemaNumber '[NEq 3]))] )
150+exampleObject = ReprObject $ FieldRepr exampleArray :& RNil
151+
152+example :: JsonRepr Spec
153+example = ReprObject $
154+ FieldRepr (ReprArray [ReprNumber 3])
155+ :& FieldRepr (ReprText "test")
156+ :& RNil
157+
158+class FalseConstraint
159+
160+type family TopLevel (spec :: Schema) :: Constraint where
161+ TopLevel (SchemaArray a e) = ()
162+ TopLevel (SchemaObject o) = ()
163+ TopLevel spec = FalseConstraint