module Data.Schematic.Schema where
import Control.Applicative ()
import Control.Monad
import Data.Aeson as J
import Data.Aeson.Types as J
import Data.HashMap.Strict as H
import Data.Kind
import Data.Maybe
import Data.Schematic.Instances ()
import Data.Scientific
import Data.Singletons.Prelude.List hiding (All)
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Data.Text as T
import Data.Vector as V
import Data.Vinyl hiding (Dict)
import qualified Data.Vinyl.TypeLevel as V
import GHC.Generics (Generic)
import GHC.TypeLits (SomeNat(..), SomeSymbol(..), someSymbolVal, someNatVal)
import Prelude as P
import Test.SmallCheck.Series
type family CRepr (s :: Schema) :: Type where
CRepr ('SchemaText cs) = TextConstraint
CRepr ('SchemaNumber cs) = NumberConstraint
CRepr ('SchemaObject fs) = (String, Schema)
CRepr ('SchemaArray ar s) = ArrayConstraint
data TextConstraint
= TEq Nat
| TLt Nat
| TLe Nat
| TGt Nat
| TGe Nat
| TRegex Symbol
| TEnum [Symbol]
deriving (Generic)
instance SingKind TextConstraint where
type DemoteRep TextConstraint = DemotedTextConstraint
fromSing = \case
STEq n -> withKnownNat n (DTEq $ natVal n)
STLt n -> withKnownNat n (DTLt $ natVal n)
STLe n -> withKnownNat n (DTLe $ natVal n)
STGt n -> withKnownNat n (DTGt $ natVal n)
STGe n -> withKnownNat n (DTGe $ natVal n)
STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
STEnum s -> let
d :: Sing (s :: [Symbol]) -> [Text]
d SNil = []
d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
in DTEnum $ d s
toSing = \case
DTEq n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DTLt n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DTLe n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DTGt n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DTGe n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DTRegex s -> case someSymbolVal (T.unpack s) of
SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
DTEnum ss -> case toSing (T.unpack <$> ss) of
SomeSing l -> SomeSing (STEnum l)
data DemotedTextConstraint
= DTEq Integer
| DTLt Integer
| DTLe Integer
| DTGt Integer
| DTGe Integer
| DTRegex Text
| DTEnum [Text]
deriving (Generic)
data instance Sing (tc :: TextConstraint) where
STEq :: Sing n -> Sing ('TEq n)
STLt :: Sing n -> Sing ('TLt n)
STLe :: Sing n -> Sing ('TLe n)
STGt :: Sing n -> Sing ('TGt n)
STGe :: Sing n -> Sing ('TGe n)
STRegex :: Sing s -> Sing ('TRegex s)
STEnum :: Sing ss -> Sing ('TEnum ss)
instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
instance Eq (Sing ('TEq n)) where _ == _ = True
instance Eq (Sing ('TLt n)) where _ == _ = True
instance Eq (Sing ('TLe n)) where _ == _ = True
instance Eq (Sing ('TGt n)) where _ == _ = True
instance Eq (Sing ('TGe n)) where _ == _ = True
instance Eq (Sing ('TRegex t)) where _ == _ = True
instance Eq (Sing ('TEnum ss)) where _ == _ = True
data NumberConstraint
= NLe Nat
| NLt Nat
| NGt Nat
| NGe Nat
| NEq Nat
deriving (Generic)
data DemotedNumberConstraint
= DNLe Integer
| DNLt Integer
| DNGt Integer
| DNGe Integer
| DNEq Integer
deriving (Generic)
data instance Sing (nc :: NumberConstraint) where
SNEq :: Sing n -> Sing ('NEq n)
SNGt :: Sing n -> Sing ('NGt n)
SNGe :: Sing n -> Sing ('NGe n)
SNLt :: Sing n -> Sing ('NLt n)
SNLe :: Sing n -> Sing ('NLe n)
instance KnownNat n => SingI ('NEq n) where sing = SNEq sing
instance KnownNat n => SingI ('NGt n) where sing = SNGt sing
instance KnownNat n => SingI ('NGe n) where sing = SNGe sing
instance KnownNat n => SingI ('NLt n) where sing = SNLt sing
instance KnownNat n => SingI ('NLe n) where sing = SNLe sing
instance Eq (Sing ('NEq n)) where _ == _ = True
instance Eq (Sing ('NLt n)) where _ == _ = True
instance Eq (Sing ('NLe n)) where _ == _ = True
instance Eq (Sing ('NGt n)) where _ == _ = True
instance Eq (Sing ('NGe n)) where _ == _ = True
instance SingKind NumberConstraint where
type DemoteRep NumberConstraint = DemotedNumberConstraint
fromSing = \case
SNEq n -> withKnownNat n (DNEq $ natVal n)
SNGt n -> withKnownNat n (DNGt $ natVal n)
SNGe n -> withKnownNat n (DNGe $ natVal n)
SNLt n -> withKnownNat n (DNLt $ natVal n)
SNLe n -> withKnownNat n (DNLe $ natVal n)
toSing = \case
DNEq n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DNGt n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DNGe n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DNLt n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
DNLe n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
data ArrayConstraint
= AEq Nat
deriving (Generic)
data DemotedArrayConstraint
= DAEq Integer
deriving (Generic)
data instance Sing (ac :: ArrayConstraint) where
SAEq :: Sing n -> Sing ('AEq n)
instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
instance Eq (Sing ('AEq n)) where _ == _ = True
instance SingKind ArrayConstraint where
type DemoteRep ArrayConstraint = DemotedArrayConstraint
fromSing = \case
SAEq n -> withKnownNat n (DAEq $ natVal n)
toSing = \case
DAEq n -> case someNatVal n of
Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
Nothing -> error "Negative singleton nat"
data Schema
= SchemaText [TextConstraint]
| SchemaBoolean
| SchemaNumber [NumberConstraint]
| SchemaObject [(Symbol, Schema)]
| SchemaArray [ArrayConstraint] Schema
| SchemaNull
| SchemaOptional Schema
deriving (Generic)
data DemotedSchema
= DSchemaText [DemotedTextConstraint]
| DSchemaNumber [DemotedNumberConstraint]
| DSchemaBoolean
| DSchemaObject [(Text, DemotedSchema)]
| DSchemaArray [DemotedArrayConstraint] DemotedSchema
| DSchemaNull
| DSchemaOptional DemotedSchema
deriving (Generic)
data instance Sing (schema :: Schema) where
SSchemaText :: Sing tcs -> Sing ('SchemaText tcs)
SSchemaNumber :: Sing ncs -> Sing ('SchemaNumber ncs)
SSchemaBoolean :: Sing 'SchemaBoolean
SSchemaArray :: Sing acs -> Sing schema -> Sing ('SchemaArray acs schema)
SSchemaObject :: Sing fields -> Sing ('SchemaObject fields)
SSchemaOptional :: Sing s -> Sing ('SchemaOptional s)
SSchemaNull :: Sing 'SchemaNull
instance SingI sl => SingI ('SchemaText sl) where
sing = SSchemaText sing
instance SingI sl => SingI ('SchemaNumber sl) where
sing = SSchemaNumber sing
instance SingI 'SchemaNull where
sing = SSchemaNull
instance SingI 'SchemaBoolean where
sing = SSchemaBoolean
instance (SingI ac, SingI s) => SingI ('SchemaArray ac s) where
sing = SSchemaArray sing sing
instance SingI stl => SingI ('SchemaObject stl) where
sing = SSchemaObject sing
instance SingI s => SingI ('SchemaOptional s) where
sing = SSchemaOptional sing
instance Eq (Sing ('SchemaText cs)) where _ == _ = True
instance Eq (Sing ('SchemaNumber cs)) where _ == _ = True
instance Eq (Sing 'SchemaNull) where _ == _ = True
instance Eq (Sing 'SchemaBoolean) where _ == _ = True
instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
instance SingKind Schema where
type DemoteRep Schema = DemotedSchema
fromSing = \case
SSchemaText cs -> DSchemaText $ fromSing cs
SSchemaNumber cs -> DSchemaNumber $ fromSing cs
SSchemaBoolean -> DSchemaBoolean
SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
SSchemaOptional s -> DSchemaOptional $ fromSing s
SSchemaNull -> DSchemaNull
SSchemaObject cs -> let
dem :: Sing (s :: [(Symbol, Schema)]) -> [(Text, DemotedSchema)]
dem SNil = []
dem (SCons (STuple2 ss ssch) fs) = withKnownSymbol ss
$ (T.pack (symbolVal ss), fromSing ssch) : dem fs
in DSchemaObject $ dem cs
toSing = \case
DSchemaText cs -> case toSing cs of
SomeSing scs -> SomeSing $ SSchemaText scs
DSchemaNumber cs -> case toSing cs of
SomeSing scs -> SomeSing $ SSchemaNumber scs
DSchemaBoolean -> SomeSing $ SSchemaBoolean
DSchemaArray cs sch -> case (toSing cs, toSing sch) of
(SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
DSchemaOptional sch -> case toSing sch of
SomeSing ssch -> SomeSing $ SSchemaOptional ssch
DSchemaNull -> SomeSing SSchemaNull
DSchemaObject cs -> case toSing ((\(sym,sch) -> (T.unpack sym, sch)) <$> cs) of
SomeSing scs -> SomeSing $ SSchemaObject scs
data FieldRepr :: (Symbol, Schema) -> Type where
FieldRepr
:: (SingI schema, KnownSymbol name)
=> JsonRepr schema
-> FieldRepr '(name, schema)
toJsonRepr :: FieldRepr '(fn, sch) -> JsonRepr sch
toJsonRepr (FieldRepr x) = x
knownFieldName
:: forall proxy (fieldName :: Symbol) schema
. KnownSymbol fieldName
=> proxy '(fieldName, schema)
-> Text
knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
knownFieldSchema
:: forall proxy fieldName schema
. SingI schema
=> proxy '(fieldName, schema)
-> Sing schema
knownFieldSchema _ = sing
deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
FieldRepr a == FieldRepr b = a == b
instance
( KnownSymbol name
, SingI schema
, Serial m (JsonRepr schema) )
=> Serial m (FieldRepr '(name, schema)) where
series = FieldRepr <$> series
data JsonRepr :: Schema -> Type where
ReprText :: Text -> JsonRepr ('SchemaText cs)
ReprNumber :: Scientific -> JsonRepr ('SchemaNumber cs)
ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
ReprNull :: JsonRepr 'SchemaNull
ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
instance Show (JsonRepr ('SchemaText cs)) where
show (ReprText t) = "ReprText " P.++ show t
instance Show (JsonRepr ('SchemaNumber cs)) where
show (ReprNumber n) = "ReprNumber " P.++ show n
instance Show (JsonRepr 'SchemaNull) where show _ = "ReprNull"
instance Show (JsonRepr s) => Show (JsonRepr ('SchemaArray acs s)) where
show (ReprArray v) = "ReprArray " P.++ show v
instance V.RecAll FieldRepr fs Show => Show (JsonRepr ('SchemaObject fs)) where
show (ReprObject fs) = "ReprObject " P.++ show fs
instance Show (JsonRepr s) => Show (JsonRepr ('SchemaOptional s)) where
show (ReprOptional s) = "ReprOptional " P.++ show s
instance (Monad m, Serial m Text)
=> Serial m (JsonRepr ('SchemaText cs)) where
series = cons1 ReprText
instance (Monad m, Serial m Scientific)
=> Serial m (JsonRepr ('SchemaNumber cs)) where
series = cons1 ReprNumber
instance Monad m => Serial m (JsonRepr 'SchemaNull) where
series = cons0 ReprNull
instance (Serial m (V.Vector (JsonRepr s)))
=> Serial m (JsonRepr ('SchemaArray cs s)) where
series = cons1 ReprArray
instance (Serial m (JsonRepr s))
=> Serial m (JsonRepr ('SchemaOptional s)) where
series = cons1 ReprOptional
instance (Monad m, Serial m (Rec FieldRepr fs))
=> Serial m (JsonRepr ('SchemaObject fs)) where
series = cons1 ReprObject
instance Eq (Rec FieldRepr fs) => Eq (JsonRepr ('SchemaObject fs)) where
ReprObject a == ReprObject b = a == b
instance Eq (JsonRepr ('SchemaText cs)) where
ReprText a == ReprText b = a == b
instance Eq (JsonRepr ('SchemaNumber cs)) where
ReprNumber a == ReprNumber b = a == b
instance Eq (JsonRepr 'SchemaNull) where
ReprNull == ReprNull = True
instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaArray as s)) where
ReprArray a == ReprArray b = a == b
instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaOptional s)) where
ReprOptional a == ReprOptional b = a == b
fromOptional
:: SingI s
=> Sing ('SchemaOptional s)
-> J.Value
-> Parser (Maybe (JsonRepr s))
fromOptional _ = parseJSON
instance SingI schema => J.FromJSON (JsonRepr schema) where
parseJSON value = case sing :: Sing schema of
SSchemaText _ -> withText "String" (pure . ReprText) value
SSchemaNumber _ -> withScientific "Number" (pure . ReprNumber) value
SSchemaBoolean -> ReprBoolean <$> parseJSON value
SSchemaNull -> case value of
J.Null -> pure ReprNull
_ -> typeMismatch "Null" value
so@(SSchemaOptional s) -> withSingI s $ ReprOptional <$> fromOptional so value
SSchemaArray sa sb -> withSingI sa $ withSingI sb
$ withArray "Array" (fmap ReprArray . traverse parseJSON) value
SSchemaObject fs -> do
let
demoteFields :: SList s -> H.HashMap Text J.Value -> Parser (Rec FieldRepr s)
demoteFields SNil _ = pure RNil
demoteFields (SCons (STuple2 (n :: Sing fn) s) tl) h = withKnownSymbol n $ do
let fieldName = T.pack $ symbolVal (Proxy @fn)
fieldRepr <- case s of
SSchemaText so -> case H.lookup fieldName h of
Just v -> withSingI so $ FieldRepr <$> parseJSON v
Nothing -> fail "schematext"
SSchemaNumber so -> case H.lookup fieldName h of
Just v -> withSingI so $ FieldRepr <$> parseJSON v
Nothing -> fail "schemanumber"
SSchemaBoolean -> case H.lookup fieldName h of
Just v -> FieldRepr <$> parseJSON v
Nothing -> fail "schemaboolean"
SSchemaNull -> case H.lookup fieldName h of
Just v -> FieldRepr <$> parseJSON v
Nothing -> fail "schemanull"
SSchemaArray sa sb -> case H.lookup fieldName h of
Just v -> withSingI sa $ withSingI sb $ FieldRepr <$> parseJSON v
Nothing -> fail "schemaarray"
SSchemaObject so -> case H.lookup fieldName h of
Just v -> withSingI so $ FieldRepr <$> parseJSON v
Nothing -> fail "schemaobject"
SSchemaOptional so -> case H.lookup fieldName h of
Just v -> withSingI so $ FieldRepr <$> parseJSON v
Nothing -> fail "schemaoptional"
(fieldRepr :&) <$> demoteFields tl h
ReprObject <$> withObject "Object" (demoteFields fs) value
instance J.ToJSON (JsonRepr a) where
toJSON ReprNull = J.Null
toJSON (ReprBoolean b) = J.Bool b
toJSON (ReprText t) = J.String t
toJSON (ReprNumber n) = J.Number n
toJSON (ReprOptional s) = case s of
Just v -> toJSON v
Nothing -> J.Null
toJSON (ReprArray v) = J.Array $ toJSON <$> v
toJSON (ReprObject r) = J.Object . H.fromList . fold $ r
where
extract :: forall name s . (KnownSymbol name)
=> FieldRepr '(name, s)
-> (Text, Value)
extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
fold :: Rec FieldRepr fs -> [(Text, J.Value)]
fold = \case
RNil -> []
fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
class FalseConstraint a
type family TopLevel (schema :: Schema) :: Constraint where
TopLevel ('SchemaArray acs s) = ()
TopLevel ('SchemaObject o) = ()
TopLevel spec = 'True ~ 'False