module Dhall
(
input
, detailed
, Type
, Interpret(..)
, bool
, natural
, integer
, double
, text
, maybe
, vector
, Natural
, Text
, Vector
, Generic
) where
import Control.Applicative (empty, liftA2, (<|>))
import Control.Exception (Exception)
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.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
import qualified GHC.Generics
throws :: Exception e => Either e a -> IO a
throws (Left e) = Control.Exception.throwIO e
throws (Right r) = return r
input
:: Type a
-> Text
-> IO a
input (Type {..}) text = do
let delta = Directed "(input)" 0 0 0 0
expr <- throws (Dhall.Parser.exprFromText delta text)
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
typeExpr <- throws (Dhall.TypeCheck.typeOf annot)
case extract (Dhall.Core.normalize expr') of
Just x -> return x
Nothing -> fail "input: malformed `Type`"
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 X 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
text :: Type Text
text = Type {..}
where
extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t)
extract _ = empty
expected = Text
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)
expectedOut = App Optional expectedIn
vector :: Type a -> Type (Vector a)
vector (Type extractIn expectedIn) = Type extractOut expectedOut
where
extractOut (ListLit _ es) = traverse extractIn es
expectedOut = App List expectedIn
class Interpret a where
auto :: Type a
default auto :: (Generic a, GenericInterpret (Rep a)) => Type a
auto = fmap GHC.Generics.to genericAuto
instance Interpret Bool where
auto = bool
instance Interpret Natural where
auto = natural
instance Interpret Integer where
auto = integer
instance Interpret Double where
auto = double
instance Interpret Text where
auto = text
instance Interpret a => Interpret (Maybe a) where
auto = maybe auto
instance Interpret a => Interpret (Vector a) where
auto = vector auto
class GenericInterpret f where
genericAuto :: Type (f a)
instance GenericInterpret f => GenericInterpret (M1 D d f) where
genericAuto = fmap M1 genericAuto
instance GenericInterpret V1 where
genericAuto = 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
genericAuto = Type {..}
where
nL :: M1 i c1 f1 a
nL = undefined
nR :: M1 i c2 f2 a
nR = undefined
nameL = Data.Text.Lazy.pack (conName nL)
nameR = 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
expected =
Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])
Type extractL expectedL = genericAuto
Type extractR expectedR = genericAuto
instance (Constructor c, GenericInterpret (f :+: g), GenericInterpret h) => GenericInterpret ((f :+: g) :+: M1 C c h) where
genericAuto = Type {..}
where
n :: M1 i c h a
n = undefined
name = Data.Text.Lazy.pack (conName n)
extract u@(UnionLit name' e _)
| name == name' = fmap (R1 . M1) (extractR e)
| otherwise = fmap L1 (extractL u)
expected = Union (Data.Map.insert name expectedR expectedL)
Type extractL (Union expectedL) = genericAuto
Type extractR expectedR = genericAuto
instance (Constructor c, GenericInterpret f, GenericInterpret (g :+: h)) => GenericInterpret (M1 C c f :+: (g :+: h)) where
genericAuto = Type {..}
where
n :: M1 i c f a
n = undefined
name = Data.Text.Lazy.pack (conName n)
extract u@(UnionLit name' e _)
| name == name' = fmap (L1 . M1) (extractL e)
| otherwise = fmap R1 (extractR u)
expected = Union (Data.Map.insert name expectedL expectedR)
Type extractL expectedL = genericAuto
Type extractR (Union expectedR) = genericAuto
instance (GenericInterpret (f :+: g), GenericInterpret (h :+: i)) => GenericInterpret ((f :+: g) :+: (h :+: i)) where
genericAuto = Type {..}
where
extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e)
expected = Union (Data.Map.union expectedL expectedR)
Type extractL (Union expectedL) = genericAuto
Type extractR (Union expectedR) = genericAuto
instance GenericInterpret f => GenericInterpret (M1 C c f) where
genericAuto = fmap M1 genericAuto
instance GenericInterpret U1 where
genericAuto = Type {..}
where
extract _ = Just U1
expected = Record (Data.Map.fromList [])
instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where
genericAuto = Type {..}
where
extract = liftA2 (liftA2 (:*:)) extractL extractR
expected = Record (Data.Map.union ktsL ktsR)
where
Record ktsL = expectedL
Record ktsR = expectedR
Type extractL expectedL = genericAuto
Type extractR expectedR = genericAuto
instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where
genericAuto = Type {..}
where
n :: M1 i s f a
n = undefined
extract (RecordLit m) = do
case selName n of
"" -> Nothing
name -> do
e <- Data.Map.lookup (Data.Text.Lazy.pack name) m
fmap (M1 . K1) (extract' e)
extract _ = Nothing
expected = Record (Data.Map.fromList [(key, expected')])
where
key = Data.Text.Lazy.pack (selName n)
Type extract' expected' = auto