module Dhall
(
input
, detailed
, Type(..)
, InputType(..)
, Interpret(..)
, InvalidType(..)
, auto
, InterpretOptions(..)
, defaultInterpretOptions
, bool
, natural
, integer
, double
, lazyText
, strictText
, maybe
, vector
, GenericInterpret(..)
, Inject(..)
, inject
, rawInput
, Natural
, Text
, Vector
, Generic
) where
import Control.Applicative (empty, liftA2, (<|>), Alternative)
import Control.Exception (Exception)
import Data.Functor.Contravariant (Contravariant(..))
import Data.Monoid ((<>))
import Data.Text.Buildable (Buildable(..))
import Data.Text.Lazy (Text)
import Data.Typeable (Typeable)
import Data.Vector (Vector)
import Dhall.Core (Expr(..))
import Dhall.Import (Imported(..))
import Dhall.Parser (Src(..))
import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
import GHC.Generics
import Numeric.Natural (Natural)
import Prelude hiding (maybe)
import Text.Trifecta.Delta (Delta(..))
import qualified Control.Exception
import qualified Data.ByteString.Lazy
import qualified Data.Map
import qualified Data.Text
import qualified Data.Text.Lazy
import qualified Data.Text.Lazy.Builder
import qualified Data.Text.Lazy.Encoding
import qualified Data.Vector
import qualified Dhall.Core
import qualified Dhall.Import
import qualified Dhall.Parser
import qualified Dhall.TypeCheck
throws :: Exception e => Either e a -> IO a
throws (Left e) = Control.Exception.throwIO e
throws (Right r) = return r
data InvalidType = InvalidType deriving (Typeable)
_ERROR :: String
_ERROR = "\ESC[1;31mError\ESC[0m"
instance Show InvalidType where
show InvalidType =
_ERROR <> ": Invalid Dhall.Type \n\
\ \n\
\Every Type must provide an extract function that succeeds if an expression \n\
\matches the expected type. You provided a Type that disobeys this contract \n"
instance Exception InvalidType
input
:: Type a
-> Text
-> IO a
input (Type {..}) txt = do
let delta = Directed "(input)" 0 0 0 0
expr <- throws (Dhall.Parser.exprFromText delta txt)
expr' <- Dhall.Import.load expr
let suffix =
( Data.ByteString.Lazy.toStrict
. Data.Text.Lazy.Encoding.encodeUtf8
. Data.Text.Lazy.Builder.toLazyText
. build
) expected
let annot = case expr' of
Note (Src begin end bytes) _ ->
Note (Src begin end bytes') (Annot expr' expected)
where
bytes' = bytes <> " : " <> suffix
_ ->
Annot expr' expected
_ <- throws (Dhall.TypeCheck.typeOf annot)
case extract (Dhall.Core.normalize expr') of
Just x -> return x
Nothing -> Control.Exception.throwIO InvalidType
rawInput
:: Alternative f
=> Type a
-> Expr s X
-> f a
rawInput (Type {..}) expr = do
case extract (Dhall.Core.normalize expr) of
Just x -> pure x
Nothing -> empty
detailed :: IO a -> IO a
detailed =
Control.Exception.handle handler1 . Control.Exception.handle handler0
where
handler0 :: Imported (TypeError Src) -> IO a
handler0 (Imported ps e) =
Control.Exception.throwIO (Imported ps (DetailedTypeError e))
handler1 :: TypeError Src -> IO a
handler1 e = Control.Exception.throwIO (DetailedTypeError e)
data Type a = Type
{ extract :: Expr Src X -> Maybe a
, expected :: Expr Src X
}
deriving (Functor)
bool :: Type Bool
bool = Type {..}
where
extract (BoolLit b) = pure b
extract _ = Nothing
expected = Bool
natural :: Type Natural
natural = Type {..}
where
extract (NaturalLit n) = pure n
extract _ = empty
expected = Natural
integer :: Type Integer
integer = Type {..}
where
extract (IntegerLit n) = pure n
extract _ = empty
expected = Integer
double :: Type Double
double = Type {..}
where
extract (DoubleLit n) = pure n
extract _ = empty
expected = Double
lazyText :: Type Text
lazyText = Type {..}
where
extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t)
extract _ = empty
expected = Text
strictText :: Type Data.Text.Text
strictText = fmap Data.Text.Lazy.toStrict lazyText
maybe :: Type a -> Type (Maybe a)
maybe (Type extractIn expectedIn) = Type extractOut expectedOut
where
extractOut (OptionalLit _ es) = traverse extractIn es'
where
es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)
extractOut _ = Nothing
expectedOut = App Optional expectedIn
vector :: Type a -> Type (Vector a)
vector (Type extractIn expectedIn) = Type extractOut expectedOut
where
extractOut (ListLit _ es) = traverse extractIn es
extractOut _ = Nothing
expectedOut = App List expectedIn
class Interpret a where
autoWith:: InterpretOptions -> Type a
default autoWith
:: (Generic a, GenericInterpret (Rep a)) => InterpretOptions -> Type a
autoWith options = fmap GHC.Generics.to (genericAutoWith options)
instance Interpret Bool where
autoWith _ = bool
instance Interpret Natural where
autoWith _ = natural
instance Interpret Integer where
autoWith _ = integer
instance Interpret Double where
autoWith _ = double
instance Interpret Text where
autoWith _ = lazyText
instance Interpret Data.Text.Text where
autoWith _ = strictText
instance Interpret a => Interpret (Maybe a) where
autoWith opts = maybe (autoWith opts)
instance Interpret a => Interpret (Vector a) where
autoWith opts = vector (autoWith opts)
instance (Inject a, Interpret b) => Interpret (a -> b) where
autoWith opts = Type extractOut expectedOut
where
extractOut e = Just (\i -> case extractIn (Dhall.Core.normalize (App e (embed i))) of
Just o -> o
Nothing -> error "Interpret: You cannot decode a function if it does not have the correct type" )
expectedOut = Pi "_" declared expectedIn
InputType {..} = inject
Type extractIn expectedIn = autoWith opts
auto :: Interpret a => Type a
auto = autoWith defaultInterpretOptions
data InterpretOptions = InterpretOptions
{ fieldModifier :: Text -> Text
, constructorModifier :: Text -> Text
}
defaultInterpretOptions :: InterpretOptions
defaultInterpretOptions = InterpretOptions
{ fieldModifier = id
, constructorModifier = id
}
class GenericInterpret f where
genericAutoWith :: InterpretOptions -> Type (f a)
instance GenericInterpret f => GenericInterpret (M1 D d f) where
genericAutoWith = fmap (fmap M1) genericAutoWith
instance GenericInterpret V1 where
genericAutoWith _ = Type {..}
where
extract _ = Nothing
expected = Union Data.Map.empty
instance (Constructor c1, Constructor c2, GenericInterpret f1, GenericInterpret f2) => GenericInterpret (M1 C c1 f1 :+: M1 C c2 f2) where
genericAutoWith options@(InterpretOptions {..}) = Type {..}
where
nL :: M1 i c1 f1 a
nL = undefined
nR :: M1 i c2 f2 a
nR = undefined
nameL = constructorModifier (Data.Text.Lazy.pack (conName nL))
nameR = constructorModifier (Data.Text.Lazy.pack (conName nR))
extract (UnionLit name e _)
| name == nameL = fmap (L1 . M1) (extractL e)
| name == nameR = fmap (R1 . M1) (extractR e)
| otherwise = Nothing
extract _ = Nothing
expected =
Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])
Type extractL expectedL = genericAutoWith options
Type extractR expectedR = genericAutoWith options
instance (Constructor c, GenericInterpret (f :+: g), GenericInterpret h) => GenericInterpret ((f :+: g) :+: M1 C c h) where
genericAutoWith options@(InterpretOptions {..}) = Type {..}
where
n :: M1 i c h a
n = undefined
name = constructorModifier (Data.Text.Lazy.pack (conName n))
extract u@(UnionLit name' e _)
| name == name' = fmap (R1 . M1) (extractR e)
| otherwise = fmap L1 (extractL u)
extract _ = Nothing
expected = Union (Data.Map.insert name expectedR expectedL)
Type extractL (Union expectedL) = genericAutoWith options
Type extractR expectedR = genericAutoWith options
instance (Constructor c, GenericInterpret f, GenericInterpret (g :+: h)) => GenericInterpret (M1 C c f :+: (g :+: h)) where
genericAutoWith options@(InterpretOptions {..}) = Type {..}
where
n :: M1 i c f a
n = undefined
name = constructorModifier (Data.Text.Lazy.pack (conName n))
extract u@(UnionLit name' e _)
| name == name' = fmap (L1 . M1) (extractL e)
| otherwise = fmap R1 (extractR u)
extract _ = Nothing
expected = Union (Data.Map.insert name expectedL expectedR)
Type extractL expectedL = genericAutoWith options
Type extractR (Union expectedR) = genericAutoWith options
instance (GenericInterpret (f :+: g), GenericInterpret (h :+: i)) => GenericInterpret ((f :+: g) :+: (h :+: i)) where
genericAutoWith options = Type {..}
where
extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e)
expected = Union (Data.Map.union expectedL expectedR)
Type extractL (Union expectedL) = genericAutoWith options
Type extractR (Union expectedR) = genericAutoWith options
instance GenericInterpret f => GenericInterpret (M1 C c f) where
genericAutoWith = fmap (fmap M1) genericAutoWith
instance GenericInterpret U1 where
genericAutoWith _ = Type {..}
where
extract _ = Just U1
expected = Record (Data.Map.fromList [])
instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where
genericAutoWith options = Type {..}
where
extract = liftA2 (liftA2 (:*:)) extractL extractR
expected = Record (Data.Map.union ktsL ktsR)
where
Record ktsL = expectedL
Record ktsR = expectedR
Type extractL expectedL = genericAutoWith options
Type extractR expectedR = genericAutoWith options
instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where
genericAutoWith opts@(InterpretOptions {..}) = Type {..}
where
n :: M1 i s f a
n = undefined
extract (RecordLit m) = do
case selName n of
"" -> Nothing
name -> do
let name' = fieldModifier (Data.Text.Lazy.pack name)
e <- Data.Map.lookup name' m
fmap (M1 . K1) (extract' e)
extract _ = Nothing
expected = Record (Data.Map.fromList [(key, expected')])
where
key = fieldModifier (Data.Text.Lazy.pack (selName n))
Type extract' expected' = autoWith opts
data InputType a = InputType
{ embed :: a -> Expr Src X
, declared :: Expr Src X
}
instance Contravariant InputType where
contramap f (InputType embed declared) = InputType embed' declared
where
embed' x = embed (f x)
class Inject a where
injectWith :: InterpretOptions -> InputType a
default injectWith
:: (Generic a, GenericInject (Rep a)) => InterpretOptions -> InputType a
injectWith options = contramap GHC.Generics.from (genericInjectWith options)
inject :: Inject a => InputType a
inject = injectWith defaultInterpretOptions
instance Inject Bool where
injectWith _ = InputType {..}
where
embed = BoolLit
declared = Bool
instance Inject Text where
injectWith _ = InputType {..}
where
embed text = TextLit (Data.Text.Lazy.Builder.fromLazyText text)
declared = Text
instance Inject Data.Text.Text where
injectWith _ = InputType {..}
where
embed text = TextLit (Data.Text.Lazy.Builder.fromText text)
declared = Text
instance Inject Natural where
injectWith _ = InputType {..}
where
embed = NaturalLit
declared = Natural
instance Inject Integer where
injectWith _ = InputType {..}
where
embed = IntegerLit
declared = Integer
instance Inject Double where
injectWith _ = InputType {..}
where
embed = DoubleLit
declared = Double
instance Inject a => Inject (Maybe a) where
injectWith options = InputType embedOut declaredOut
where
embedOut (Just x) =
OptionalLit declaredIn (Data.Vector.singleton (embedIn x))
embedOut Nothing =
OptionalLit declaredIn Data.Vector.empty
InputType embedIn declaredIn = injectWith options
declaredOut = App Optional declaredIn
instance Inject a => Inject (Vector a) where
injectWith options = InputType embedOut declaredOut
where
embedOut xs = ListLit (Just declaredIn) (fmap embedIn xs)
declaredOut = App List declaredIn
InputType embedIn declaredIn = injectWith options
class GenericInject f where
genericInjectWith :: InterpretOptions -> InputType (f a)
instance GenericInject f => GenericInject (M1 D d f) where
genericInjectWith = fmap (contramap unM1) genericInjectWith
instance GenericInject f => GenericInject (M1 C c f) where
genericInjectWith = fmap (contramap unM1) genericInjectWith
instance (Constructor c1, Constructor c2, GenericInject f1, GenericInject f2) => GenericInject (M1 C c1 f1 :+: M1 C c2 f2) where
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
where
embed (L1 (M1 l)) = UnionLit keyL (embedL l) Data.Map.empty
embed (R1 (M1 r)) = UnionLit keyR (embedR r) Data.Map.empty
declared =
Union (Data.Map.fromList [(keyL, declaredL), (keyR, declaredR)])
nL :: M1 i c1 f1 a
nL = undefined
nR :: M1 i c2 f2 a
nR = undefined
keyL = constructorModifier (Data.Text.Lazy.pack (conName nL))
keyR = constructorModifier (Data.Text.Lazy.pack (conName nR))
InputType embedL declaredL = genericInjectWith options
InputType embedR declaredR = genericInjectWith options
instance (Constructor c, GenericInject (f :+: g), GenericInject h) => GenericInject ((f :+: g) :+: M1 C c h) where
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
where
embed (L1 l) = UnionLit keyL valL (Data.Map.insert keyR declaredR ktsL')
where
UnionLit keyL valL ktsL' = embedL l
embed (R1 (M1 r)) = UnionLit keyR (embedR r) ktsL
nR :: M1 i c h a
nR = undefined
keyR = constructorModifier (Data.Text.Lazy.pack (conName nR))
declared = Union (Data.Map.insert keyR declaredR ktsL)
InputType embedL (Union ktsL) = genericInjectWith options
InputType embedR declaredR = genericInjectWith options
instance (Constructor c, GenericInject f, GenericInject (g :+: h)) => GenericInject (M1 C c f :+: (g :+: h)) where
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
where
embed (L1 (M1 l)) = UnionLit keyL (embedL l) ktsR
embed (R1 r) = UnionLit keyR valR (Data.Map.insert keyL declaredL ktsR')
where
UnionLit keyR valR ktsR' = embedR r
nL :: M1 i c f a
nL = undefined
keyL = constructorModifier (Data.Text.Lazy.pack (conName nL))
declared = Union (Data.Map.insert keyL declaredL ktsR)
InputType embedL declaredL = genericInjectWith options
InputType embedR (Union ktsR) = genericInjectWith options
instance (GenericInject (f :+: g), GenericInject (h :+: i)) => GenericInject ((f :+: g) :+: (h :+: i)) where
genericInjectWith options = InputType {..}
where
embed (L1 l) = UnionLit keyL valR (Data.Map.union ktsL' ktsR)
where
UnionLit keyL valR ktsL' = embedL l
embed (R1 r) = UnionLit keyR valR (Data.Map.union ktsL ktsR')
where
UnionLit keyR valR ktsR' = embedR r
declared = Union (Data.Map.union ktsL ktsR)
InputType embedL (Union ktsL) = genericInjectWith options
InputType embedR (Union ktsR) = genericInjectWith options
instance (GenericInject f, GenericInject g) => GenericInject (f :*: g) where
genericInjectWith options = InputType embedOut declaredOut
where
embedOut (l :*: r) = RecordLit (Data.Map.union mapL mapR)
where
RecordLit mapL = embedInL l
RecordLit mapR = embedInR r
declaredOut = Record (Data.Map.union mapL mapR)
where
Record mapL = declaredInL
Record mapR = declaredInR
InputType embedInL declaredInL = genericInjectWith options
InputType embedInR declaredInR = genericInjectWith options
instance GenericInject U1 where
genericInjectWith _ = InputType {..}
where
embed _ = RecordLit Data.Map.empty
declared = Record Data.Map.empty
instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where
genericInjectWith opts@(InterpretOptions {..}) =
InputType embedOut declaredOut
where
n :: M1 i s f a
n = undefined
name = fieldModifier (Data.Text.Lazy.pack (selName n))
embedOut (M1 (K1 x)) = RecordLit (Data.Map.singleton name (embedIn x))
declaredOut = Record (Data.Map.singleton name declaredIn)
InputType embedIn declaredIn = injectWith opts