Specialize Expr's ToTerm instance to (Expr X a) (#1143)
* This simplifies pattern matching during encoding.
This commit is contained in:
parent
88d6671e38
commit
c8a0df3748
|
@ -639,6 +639,7 @@ Library
|
|||
Dhall.Import.Types,
|
||||
Dhall.Eval,
|
||||
Dhall.Util,
|
||||
Dhall.X
|
||||
Paths_dhall
|
||||
if flag(with-http)
|
||||
Other-Modules:
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
|
@ -43,6 +44,7 @@ import Dhall.Core
|
|||
, Var(..)
|
||||
)
|
||||
|
||||
import Dhall.X (X(..))
|
||||
import Data.Foldable (toList)
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
import Data.Monoid ((<>))
|
||||
|
@ -128,7 +130,7 @@ unApply e₀ = (baseFunction₀, diffArguments₀ [])
|
|||
class ToTerm a where
|
||||
encode :: a -> Term
|
||||
|
||||
instance ToTerm a => ToTerm (Expr s a) where
|
||||
instance ToTerm a => ToTerm (Expr X a) where
|
||||
encode (Var (V "_" n)) =
|
||||
TInt n
|
||||
encode (Var (V x n)) =
|
||||
|
@ -285,10 +287,10 @@ instance ToTerm a => ToTerm (Expr s a) where
|
|||
| null xs₀ = TList [ TInt label, _T₁ ]
|
||||
| otherwise = TList ([ TInt 4, TNull ] ++ xs₁)
|
||||
where
|
||||
(label, _T₁) = case fmap Dhall.Core.shallowDenote _T₀ of
|
||||
Nothing -> (4 , TNull)
|
||||
Just (App t0 t1) | List <- Dhall.Core.shallowDenote t0 -> (4 , encode t1)
|
||||
Just t -> (28, encode t)
|
||||
(label, _T₁) = case _T₀ of
|
||||
Nothing -> (4 , TNull)
|
||||
Just (App List t) -> (4 , encode t)
|
||||
Just t -> (28, encode t)
|
||||
|
||||
xs₁ = map encode (Data.Foldable.toList xs₀)
|
||||
encode (Some t₀) =
|
||||
|
@ -426,8 +428,7 @@ instance ToTerm a => ToTerm (Expr s a) where
|
|||
where
|
||||
t₁ = encode t₀
|
||||
_T₁ = encode _T₀
|
||||
encode (Note _ e) =
|
||||
encode e
|
||||
encode (Note (X absurd) _) = absurd
|
||||
|
||||
instance ToTerm Import where
|
||||
encode import_ =
|
||||
|
@ -445,7 +446,7 @@ instance ToTerm Import where
|
|||
Nothing ->
|
||||
TNull
|
||||
Just h ->
|
||||
encode h
|
||||
encodeExpression h
|
||||
|
||||
scheme₁ = case scheme₀ of
|
||||
HTTP -> 0
|
||||
|
@ -494,6 +495,9 @@ instance ToTerm Import where
|
|||
|
||||
ImportHashed {..} = importHashed
|
||||
|
||||
instance ToTerm X where
|
||||
encode = absurd
|
||||
|
||||
-- | Types that can be decoded from a CBOR `Term`
|
||||
class FromTerm a where
|
||||
decode :: Term -> Maybe a
|
||||
|
@ -889,6 +893,9 @@ instance FromTerm Import where
|
|||
|
||||
decode _ = empty
|
||||
|
||||
instance FromTerm X where
|
||||
decode _ = empty
|
||||
|
||||
strip55799Tag :: Term -> Term
|
||||
strip55799Tag term =
|
||||
case term of
|
||||
|
@ -934,8 +941,11 @@ strip55799Tag term =
|
|||
TDouble a
|
||||
|
||||
-- | Encode a Dhall expression as a CBOR `Term`
|
||||
--
|
||||
-- This 'Dhall.Core.denote's the expression before encoding it. To encode an
|
||||
-- already denoted expression, it is more efficient to directly use 'encode'.
|
||||
encodeExpression :: Expr s Import -> Term
|
||||
encodeExpression = encode
|
||||
encodeExpression e = encode (Dhall.Core.denote e :: Expr X Import)
|
||||
|
||||
-- | Decode a Dhall expression from a CBOR `Term`
|
||||
decodeExpression :: FromTerm a => Term -> Either DecodingFailure (Expr s a)
|
||||
|
|
|
@ -78,6 +78,7 @@ import Dhall.Core (
|
|||
-- import Dhall.Import.Types (InternalError)
|
||||
import Dhall.Map (Map)
|
||||
import Dhall.Set (Set)
|
||||
import Dhall.X (X)
|
||||
import GHC.Natural (Natural)
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
|
@ -667,8 +668,8 @@ conv !env t t' =
|
|||
(VIntegerToDouble t , VIntegerToDouble t') -> convE t t'
|
||||
|
||||
(VDouble , VDouble) -> True
|
||||
(VDoubleLit n , VDoubleLit n') -> Dhall.Binary.encode (DoubleLit n :: Expr Void Import) ==
|
||||
Dhall.Binary.encode (DoubleLit n' :: Expr Void Import)
|
||||
(VDoubleLit n , VDoubleLit n') -> Dhall.Binary.encode (DoubleLit n :: Expr X Import) ==
|
||||
Dhall.Binary.encode (DoubleLit n' :: Expr X Import)
|
||||
(VDoubleShow t , VDoubleShow t') -> convE t t'
|
||||
|
||||
(VText, VText) -> True
|
||||
|
|
|
@ -972,7 +972,7 @@ encodeExpression _standardVersion expression = bytesStrict
|
|||
intermediateExpression = fmap absurd expression
|
||||
|
||||
term :: Term
|
||||
term = Dhall.Binary.encode intermediateExpression
|
||||
term = Dhall.Binary.encodeExpression intermediateExpression
|
||||
|
||||
taggedTerm :: Term
|
||||
taggedTerm =
|
||||
|
|
|
@ -530,7 +530,7 @@ command (Options {..}) = do
|
|||
Encode {..} -> do
|
||||
expression <- getExpression file
|
||||
|
||||
let term = Dhall.Binary.encode expression
|
||||
let term = Dhall.Binary.encodeExpression expression
|
||||
|
||||
let bytes = Codec.Serialise.serialise term
|
||||
|
||||
|
|
|
@ -21,9 +21,7 @@ module Dhall.TypeCheck (
|
|||
, TypeMessage(..)
|
||||
) where
|
||||
|
||||
import Control.Applicative (empty)
|
||||
import Control.Exception (Exception)
|
||||
import Data.Data (Data(..))
|
||||
import Data.Functor (void)
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
import Data.Monoid (Endo(..), First(..))
|
||||
|
@ -33,10 +31,11 @@ import Data.Set (Set)
|
|||
import Data.Text (Text)
|
||||
import Data.Text.Prettyprint.Doc (Doc, Pretty(..))
|
||||
import Data.Typeable (Typeable)
|
||||
import Dhall.Binary (FromTerm(..), ToTerm(..))
|
||||
import Dhall.Binary (ToTerm(..))
|
||||
import Dhall.Core (Binding(..), Const(..), Chunks(..), Expr(..), Var(..))
|
||||
import Dhall.Context (Context)
|
||||
import Dhall.Pretty (Ann, layoutOpts)
|
||||
import Dhall.X (X(..))
|
||||
|
||||
import qualified Data.Foldable
|
||||
import qualified Data.Map
|
||||
|
@ -869,29 +868,6 @@ typeWithA tpa = loop
|
|||
typeOf :: Expr s X -> Either (TypeError s X) (Expr s X)
|
||||
typeOf = typeWith Dhall.Context.empty
|
||||
|
||||
-- | Like `Data.Void.Void`, except with a shorter inferred type
|
||||
newtype X = X { absurd :: forall a . a }
|
||||
|
||||
instance Show X where
|
||||
show = absurd
|
||||
|
||||
instance Eq X where
|
||||
_ == _ = True
|
||||
|
||||
instance Data X where
|
||||
dataTypeOf = absurd
|
||||
gunfold _ _ _ = undefined
|
||||
toConstr = absurd
|
||||
|
||||
instance Pretty X where
|
||||
pretty = absurd
|
||||
|
||||
instance FromTerm X where
|
||||
decode _ = empty
|
||||
|
||||
instance ToTerm X where
|
||||
encode = absurd
|
||||
|
||||
-- | The specific type error
|
||||
data TypeMessage s a
|
||||
= UnboundVariable Text
|
||||
|
|
23
dhall/src/Dhall/X.hs
Normal file
23
dhall/src/Dhall/X.hs
Normal file
|
@ -0,0 +1,23 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
module Dhall.X where
|
||||
|
||||
import Data.Data (Data(..))
|
||||
import Data.Text.Prettyprint.Doc (Pretty(..))
|
||||
|
||||
-- | Like `Data.Void.Void`, except with a shorter inferred type
|
||||
newtype X = X { absurd :: forall a . a }
|
||||
|
||||
instance Show X where
|
||||
show = absurd
|
||||
|
||||
instance Eq X where
|
||||
_ == _ = True
|
||||
|
||||
instance Data X where
|
||||
dataTypeOf = absurd
|
||||
gunfold _ _ _ = undefined
|
||||
toConstr = absurd
|
||||
|
||||
instance Pretty X where
|
||||
pretty = absurd
|
|
@ -121,7 +121,7 @@ shouldParse path = do
|
|||
|
||||
expression <- Core.throws (Parser.exprFromText mempty text)
|
||||
|
||||
let term = Binary.encode expression
|
||||
let term = Binary.encodeExpression expression
|
||||
|
||||
let bytes = Serialise.serialise term
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user