{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module Toml.Type
( TOML (..)
, UValue (..)
, ValueType (..)
, Value (..)
, AnyValue (..)
, DateTime (..)
, typeCheck
) where
import Data.HashMap.Strict (HashMap)
import Data.Text (Text)
import Data.Time (Day, LocalTime, TimeOfDay, ZonedTime, zonedTimeToUTC)
import Data.Type.Equality ((:~:) (..))
import Toml.PrefixTree (Key (..), PrefixMap)
data TOML = TOML
{ tomlPairs :: HashMap Key AnyValue
, tomlTables :: PrefixMap TOML
} deriving (Show, Eq)
data ValueType = TBool | TInt | TFloat | TString | TDate | TArray
data Value (t :: ValueType) where
Bool :: Bool -> Value 'TBool
Int :: Integer -> Value 'TInt
Float :: Double -> Value 'TFloat
String :: Text -> Value 'TString
Date :: DateTime -> Value 'TDate
Array :: [Value t] -> Value 'TArray
deriving instance Show (Value t)
instance Eq (Value t) where
(Bool b1) == (Bool b2) = b1 == b2
(Int i1) == (Int i2) = i1 == i2
(Float f1) == (Float f2) = f1 == f2
(String s1) == (String s2) = s1 == s2
(Date d1) == (Date d2) = d1 == d2
(Array a1) == (Array a2) = eqValueList a1 a2
eqValueList :: [Value a] -> [Value b] -> Bool
eqValueList [] [] = True
eqValueList (x:xs) (y:ys) = case sameValue x y of
Just Refl -> x == y && eqValueList xs ys
Nothing -> False
eqValueList _ _ = False
data UValue
= UBool !Bool
| UInt !Integer
| UFloat !Double
| UString !Text
| UDate !DateTime
| UArray ![UValue]
data AnyValue = forall (t :: ValueType) . AnyValue (Value t)
instance Show AnyValue where
show (AnyValue v) = show v
instance Eq AnyValue where
(AnyValue (Bool b1)) == (AnyValue (Bool b2)) = b1 == b2
(AnyValue (Int i1)) == (AnyValue (Int i2)) = i1 == i2
(AnyValue (Float f1)) == (AnyValue (Float f2)) = f1 == f2
(AnyValue (String s1)) == (AnyValue (String s2)) = s1 == s2
(AnyValue (Date d1)) == (AnyValue (Date d2)) = d1 == d2
(AnyValue (Array a1)) == (AnyValue (Array a2)) = eqValueList a1 a2
_ == _ = False
data DateTime
= Zoned !ZonedTime
| Local !LocalTime
| Day !Day
| Hours !TimeOfDay
deriving (Show)
instance Eq DateTime where
(Zoned a) == (Zoned b) = zonedTimeToUTC a == zonedTimeToUTC b
(Local a) == (Local b) = a == b
(Day a) == (Day b) = a == b
(Hours a) == (Hours b) = a == b
_ == _ = False
typeCheck :: UValue -> Maybe AnyValue
typeCheck (UBool b) = justAny $ Bool b
typeCheck (UInt n) = justAny $ Int n
typeCheck (UFloat f) = justAny $ Float f
typeCheck (UString s) = justAny $ String s
typeCheck (UDate d) = justAny $ Date d
typeCheck (UArray a) = case a of
[] -> justAny $ Array []
(x:xs) -> do
AnyValue v <- typeCheck x
AnyValue . Array <$> checkElem v xs
where
checkElem :: Value t -> [UValue] -> Maybe [Value t]
checkElem v [] = Just [v]
checkElem v (x:xs) = do
AnyValue vx <- typeCheck x
Refl <- sameValue v vx
(v :) <$> checkElem vx xs
justAny :: Value t -> Maybe AnyValue
justAny = Just . AnyValue
sameValue :: Value a -> Value b -> Maybe (a :~: b)
sameValue Bool{} Bool{} = Just Refl
sameValue Int{} Int{} = Just Refl
sameValue Float{} Float{} = Just Refl
sameValue String{} String{} = Just Refl
sameValue Date{} Date{} = Just Refl
sameValue Array{} Array{} = Just Refl
sameValue _ _ = Nothing