Small fixes to dhall diff (#1263)

* Small fixes to `dhall diff`

Related to https://github.com/dhall-lang/dhall-haskell/issues/1255

* Simplify function type diffs by omitting the bound variable name when possible
* Non-zero exit code when `dhall diff` is non-empty

Note that this is a breaking change to the `Dhall.Diff` API by changing the
exposed utilities to all expose the more general `Diff` type instead of a
`Doc`.  This means that we also no longer need separate exports for
`diff` and `diffExpression`.

* Fix build failure for tests

* Fix golden test result

* Rename `diffExpression` to `diff`

... as suggested by @sjakobi

* Add test coverage for diffing function types
This commit is contained in:
Gabriel Gonzalez 2019-08-31 08:18:46 -05:00 committed by mergify[bot]
parent dbcfe7019d
commit 0d266b91c5
9 changed files with 97 additions and 82 deletions

View File

@ -12,15 +12,14 @@
module Dhall.Diff ( module Dhall.Diff (
-- * Diff -- * Diff
Diff (..) Diff (..)
, diffExpression
, diffNormalized , diffNormalized
, Dhall.Diff.diff , diff
) where ) where
import Data.Foldable (fold, toList) import Data.Foldable (fold, toList)
import Data.List.NonEmpty (NonEmpty(..)) import Data.List.NonEmpty (NonEmpty(..))
import Data.Monoid (Any(..)) import Data.Monoid (Any(..))
import Data.Semigroup import Data.Semigroup hiding (diff)
import Data.Sequence (Seq) import Data.Sequence (Seq)
import Data.String (IsString(..)) import Data.String (IsString(..))
import Data.Text (Text) import Data.Text (Text)
@ -154,18 +153,12 @@ rparen :: Diff
rparen = token Internal.rparen rparen = token Internal.rparen
-- | Render the difference between the normal form of two expressions -- | Render the difference between the normal form of two expressions
diffNormalized :: (Eq a, Pretty a, ToTerm a) => Expr s a -> Expr s a -> Doc Ann diffNormalized :: (Eq a, Pretty a, ToTerm a) => Expr s a -> Expr s a -> Diff
diffNormalized l0 r0 = Dhall.Diff.diff l1 r1 diffNormalized l0 r0 = Dhall.Diff.diff l1 r1
where where
l1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize l0) l1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize l0)
r1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize r0) r1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize r0)
-- | Render the difference between two expressions
diff :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Doc Ann
diff l0 r0 = doc
where
Diff {..} = diffExpression l0 r0
diffPrimitive :: Eq a => (a -> Diff) -> a -> a -> Diff diffPrimitive :: Eq a => (a -> Diff) -> a -> a -> Diff
diffPrimitive f l r diffPrimitive f l r
| l == r = ignore | l == r = ignore
@ -211,7 +204,8 @@ diffInt :: Int -> Int -> Diff
diffInt = diffPrimitive (token . Internal.prettyInt) diffInt = diffPrimitive (token . Internal.prettyInt)
diffVar :: Var -> Var -> Diff diffVar :: Var -> Var -> Diff
diffVar (V xL nL) (V xR nR) = format mempty label <> "@" <> natural diffVar (V xL nL) (V xR nR) =
format mempty label <> if same natural then mempty else "@" <> natural
where where
label = diffLabel xL xR label = diffLabel xL xR
@ -259,7 +253,7 @@ diffKeyVals
-> Map Text (Expr Void a) -> Map Text (Expr Void a)
-> Map Text (Expr Void a) -> Map Text (Expr Void a)
-> [Diff] -> [Diff]
diffKeyVals assign = diffKeysWith assign diffExpression diffKeyVals assign = diffKeysWith assign diff
diffKeysWith diffKeysWith
:: Diff :: Diff
@ -359,7 +353,7 @@ diffChunks cL cR
chunkDiff a b = chunkDiff a b =
case (a, b) of case (a, b) of
(Left x, Left y ) -> diffText x y (Left x, Left y ) -> diffText x y
(Right x, Right y) -> diffExpression x y (Right x, Right y) -> diff x y
_ -> diffTextSkeleton _ -> diffTextSkeleton
diffList diffList
@ -369,7 +363,7 @@ diffList l r = bracketed (foldMap diffPart parts)
where where
-- Sections of the list that are only in left, only in right, or in both -- Sections of the list that are only in left, only in right, or in both
parts = parts =
Algo.Diff.getGroupedDiffBy ((same .) . diffExpression) (toList l) (toList r) Algo.Diff.getGroupedDiffBy ((same .) . diff) (toList l) (toList r)
-- Render each element of a list using an extra rendering function f -- Render each element of a list using an extra rendering function f
prettyElems f = map (f . token . Internal.prettyExpr) prettyElems f = map (f . token . Internal.prettyExpr)
@ -403,7 +397,7 @@ diffUnion
=> Map Text (Maybe (Expr Void a)) -> Map Text (Maybe (Expr Void a)) -> Diff => Map Text (Maybe (Expr Void a)) -> Map Text (Maybe (Expr Void a)) -> Diff
diffUnion kvsL kvsR = angled (diffKeysWith colon diffVals kvsL kvsR) diffUnion kvsL kvsR = angled (diffKeysWith colon diffVals kvsL kvsR)
where where
diffVals = diffMaybe (colon <> " ") diffExpression diffVals = diffMaybe (colon <> " ") diff
textSkeleton :: Diff textSkeleton :: Diff
textSkeleton = textSkeleton =
@ -616,8 +610,9 @@ skeleton x = token (Pretty.pretty x)
mismatch :: Pretty a => Expr s a -> Expr s a -> Diff mismatch :: Pretty a => Expr s a -> Expr s a -> Diff
mismatch l r = difference (skeleton l) (skeleton r) mismatch l r = difference (skeleton l) (skeleton r)
diffExpression :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff -- | Render the difference between two expressions
diffExpression l@(Lam {}) r@(Lam {}) = diff :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff
diff l@(Lam {}) r@(Lam {}) =
enclosed' " " (rarrow <> " ") (docs l r) enclosed' " " (rarrow <> " ") (docs l r)
where where
docs (Lam aL bL cL) (Lam aR bR cR) = docs (Lam aL bL cL) (Lam aR bR cR) =
@ -628,16 +623,16 @@ diffExpression l@(Lam {}) r@(Lam {}) =
<> format " " (diffLabel aL aR) <> format " " (diffLabel aL aR)
<> colon <> colon
<> " " <> " "
<> format mempty (diffExpression bL bR) <> format mempty (diff bL bR)
<> rparen <> rparen
docs aL aR = docs aL aR =
pure (diffExpression aL aR) pure (diff aL aR)
diffExpression l@(Lam {}) r = diff l@(Lam {}) r =
mismatch l r mismatch l r
diffExpression l r@(Lam {}) = diff l r@(Lam {}) =
mismatch l r mismatch l r
diffExpression l@(BoolIf {}) r@(BoolIf {}) = diff l@(BoolIf {}) r@(BoolIf {}) =
enclosed' " " (keyword "else" <> " ") (docs l r) enclosed' " " (keyword "else" <> " ") (docs l r)
where where
docs (BoolIf aL bL cL) (BoolIf aR bR cR) = docs (BoolIf aL bL cL) (BoolIf aR bR cR) =
@ -645,17 +640,17 @@ diffExpression l@(BoolIf {}) r@(BoolIf {}) =
where where
doc = keyword "if" doc = keyword "if"
<> " " <> " "
<> format " " (diffExpression aL aR) <> format " " (diff aL aR)
<> keyword "then" <> keyword "then"
<> " " <> " "
<> diffExpression bL bR <> diff bL bR
docs aL aR = docs aL aR =
pure (diffExpression aL aR) pure (diff aL aR)
diffExpression l@(BoolIf {}) r = diff l@(BoolIf {}) r =
mismatch l r mismatch l r
diffExpression l r@(BoolIf {}) = diff l r@(BoolIf {}) =
mismatch l r mismatch l r
diffExpression (Let asL bL ) (Let asR bR) = diff (Let asL bL ) (Let asR bR) =
enclosed' "" (keyword "in" <> " ") enclosed' "" (keyword "in" <> " ")
(Data.List.NonEmpty.zipWith docA asL asR <> pure docB) (Data.List.NonEmpty.zipWith docA asL asR <> pure docB)
where where
@ -664,23 +659,25 @@ diffExpression (Let asL bL ) (Let asR bR) =
doc = keyword "let" doc = keyword "let"
<> " " <> " "
<> format " " (diffLabel cL cR) <> format " " (diffLabel cL cR)
<> format " " (diffMaybe (colon <> " ") diffExpression dL dR) <> format " " (diffMaybe (colon <> " ") diff dL dR)
<> equals <> equals
<> " " <> " "
<> diffExpression eL eR <> diff eL eR
docB = diffExpression bL bR docB = diff bL bR
diffExpression l@(Let {}) r = diff l@(Let {}) r =
mismatch l r mismatch l r
diffExpression l r@(Let {}) = diff l r@(Let {}) =
mismatch l r mismatch l r
diffExpression l@(Pi {}) r@(Pi {}) = diff l@(Pi {}) r@(Pi {}) =
enclosed' " " (rarrow <> " ") (docs l r) enclosed' " " (rarrow <> " ") (docs l r)
where where
docs (Pi aL bL cL) (Pi aR bR cR) = docs (Pi aL bL cL) (Pi aR bR cR) =
Data.List.NonEmpty.cons (align doc) (docs cL cR) Data.List.NonEmpty.cons (align doc) (docs cL cR)
where where
doc | same docA && same docB = ignore doc | same docA && same docB = ignore
| same docA =
format mempty docB
| otherwise = | otherwise =
forall forall
<> lparen <> lparen
@ -692,14 +689,14 @@ diffExpression l@(Pi {}) r@(Pi {}) =
where where
docA = diffLabel aL aR docA = diffLabel aL aR
docB = diffExpression bL bR docB = diff bL bR
docs aL aR = pure (diffExpression aL aR) docs aL aR = pure (diff aL aR)
diffExpression l@(Pi {}) r = diff l@(Pi {}) r =
mismatch l r mismatch l r
diffExpression l r@(Pi {}) = diff l r@(Pi {}) =
mismatch l r mismatch l r
diffExpression l r = diff l r =
diffAnnotatedExpression l r diffAnnotatedExpression l r
diffAnnotatedExpression :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff diffAnnotatedExpression :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff
@ -740,7 +737,7 @@ diffAnnotatedExpression l@(Annot {}) r@(Annot {}) =
where where
doc = diffOperatorExpression aL aR doc = diffOperatorExpression aL aR
docs aL aR = docs aL aR =
diffExpression aL aR :| [] diff aL aR :| []
diffAnnotatedExpression l@(Annot {}) r = diffAnnotatedExpression l@(Annot {}) r =
mismatch l r mismatch l r
diffAnnotatedExpression l r@(Annot {}) = diffAnnotatedExpression l r@(Annot {}) =
@ -962,7 +959,7 @@ diffSelectorExpression l@(Field {}) r@(Field {}) =
docs (Project aL (Left bL)) (Project aR (Left bR)) = docs (Project aL (Left bL)) (Project aR (Left bR)) =
Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR) Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)
docs (Project aL (Right bL)) (Project aR (Right bR)) = docs (Project aL (Right bL)) (Project aR (Right bR)) =
Data.List.NonEmpty.cons (diffExpression bL bR) (docs aL aR) Data.List.NonEmpty.cons (diff bL bR) (docs aL aR)
docs aL aR = docs aL aR =
pure (diffPrimitiveExpression aL aR) pure (diffPrimitiveExpression aL aR)
diffSelectorExpression l@(Field {}) r = diffSelectorExpression l@(Field {}) r =
@ -977,7 +974,7 @@ diffSelectorExpression l@(Project {}) r@(Project {}) =
docs (Project aL (Left bL)) (Project aR (Left bR)) = docs (Project aL (Left bL)) (Project aR (Left bR)) =
Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR) Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)
docs (Project aL (Right bL)) (Project aR (Right bR)) = docs (Project aL (Right bL)) (Project aR (Right bR)) =
Data.List.NonEmpty.cons (diffExpression bL bR) (docs aL aR) Data.List.NonEmpty.cons (diff bL bR) (docs aL aR)
docs aL aR = docs aL aR =
pure (diffPrimitiveExpression aL aR) pure (diffPrimitiveExpression aL aR)
diffSelectorExpression l@(Project {}) r = diffSelectorExpression l@(Project {}) r =
@ -1230,4 +1227,4 @@ diffPrimitiveExpression aL aR =
then ignore then ignore
else align ("( " <> doc <> hardline <> ")") else align ("( " <> doc <> hardline <> ")")
where where
doc = diffExpression aL aR doc = diff aL aR

View File

@ -21,7 +21,7 @@ module Dhall.Main
) where ) where
import Control.Applicative (optional, (<|>)) import Control.Applicative (optional, (<|>))
import Control.Exception (SomeException) import Control.Exception (Handler(..), SomeException)
import Data.List.NonEmpty (NonEmpty(..)) import Data.List.NonEmpty (NonEmpty(..))
import Data.Monoid ((<>)) import Data.Monoid ((<>))
import Data.Text (Text) import Data.Text (Text)
@ -34,7 +34,7 @@ import Dhall.Parser (Src)
import Dhall.Pretty (Ann, CharacterSet(..), annToAnsiStyle, layoutOpts) import Dhall.Pretty (Ann, CharacterSet(..), annToAnsiStyle, layoutOpts)
import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
import Options.Applicative (Parser, ParserInfo) import Options.Applicative (Parser, ParserInfo)
import System.Exit (exitFailure) import System.Exit (ExitCode, exitFailure)
import System.IO (Handle) import System.IO (Handle)
import Text.Dot ((.->.)) import Text.Dot ((.->.))
@ -70,6 +70,7 @@ import qualified GHC.IO.Encoding
import qualified Options.Applicative import qualified Options.Applicative
import qualified Paths_dhall as Meta import qualified Paths_dhall as Meta
import qualified System.Console.ANSI import qualified System.Console.ANSI
import qualified System.Exit as Exit
import qualified System.IO import qualified System.IO
import qualified System.FilePath import qualified System.FilePath
import qualified Text.Dot import qualified Text.Dot
@ -303,12 +304,23 @@ command (Options {..}) = do
let toStatus = Dhall.Import.emptyStatus . rootDirectory let toStatus = Dhall.Import.emptyStatus . rootDirectory
let handle = let handle io =
Control.Exception.handle handler2 Control.Exception.catches io
. Control.Exception.handle handler1 [ Handler handleTypeError
. Control.Exception.handle handler0 , Handler handleImported
, Handler handleExitCode
]
where where
handler0 e = do handleAll e = do
let string = show (e :: SomeException)
if not (null string)
then System.IO.hPutStrLn System.IO.stderr string
else return ()
System.Exit.exitFailure
handleTypeError e = Control.Exception.handle handleAll $ do
let _ = e :: TypeError Src X let _ = e :: TypeError Src X
System.IO.hPutStrLn System.IO.stderr "" System.IO.hPutStrLn System.IO.stderr ""
if explain if explain
@ -317,7 +329,7 @@ command (Options {..}) = do
Data.Text.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" Data.Text.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"
Control.Exception.throwIO e Control.Exception.throwIO e
handler1 (Imported ps e) = do handleImported (Imported ps e) = Control.Exception.handle handleAll $ do
let _ = e :: TypeError Src X let _ = e :: TypeError Src X
System.IO.hPutStrLn System.IO.stderr "" System.IO.hPutStrLn System.IO.stderr ""
if explain if explain
@ -326,14 +338,8 @@ command (Options {..}) = do
Data.Text.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m" Data.Text.IO.hPutStrLn System.IO.stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"
Control.Exception.throwIO (Imported ps e) Control.Exception.throwIO (Imported ps e)
handler2 e = do handleExitCode e = do
let string = show (e :: SomeException) Control.Exception.throwIO (e :: ExitCode)
if not (null string)
then System.IO.hPutStrLn System.IO.stderr string
else return ()
System.Exit.exitFailure
let renderDoc :: Handle -> Doc Ann -> IO () let renderDoc :: Handle -> Doc Ann -> IO ()
renderDoc h doc = do renderDoc h doc = do
@ -470,7 +476,11 @@ command (Options {..}) = do
let diff = Dhall.Diff.diffNormalized expression1 expression2 let diff = Dhall.Diff.diffNormalized expression1 expression2
renderDoc System.IO.stdout diff renderDoc System.IO.stdout (Dhall.Diff.doc diff)
if Dhall.Diff.same diff
then return ()
else Exit.exitFailure
Format {..} -> do Format {..} -> do
Dhall.Format.format (Dhall.Format.Format {..}) Dhall.Format.format (Dhall.Format.Format {..})

View File

@ -1374,7 +1374,7 @@ prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
where where
short = "Wrong type of function argument\n" short = "Wrong type of function argument\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr1 expr3 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr3)
long = long =
"Explanation: Every function declares what type or kind of argument to accept \n\ "Explanation: Every function declares what type or kind of argument to accept \n\
@ -1508,7 +1508,7 @@ prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}
where where
short = "Expression doesn't match annotation\n" short = "Expression doesn't match annotation\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr1 expr2 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)
long = long =
"Explanation: You can annotate an expression with its type or kind using the \n\ "Explanation: You can annotate an expression with its type or kind using the \n\
\: symbol, like this: \n\ \: symbol, like this: \n\
@ -1791,7 +1791,7 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
where where
short = "❰if❱ branches must have matching types\n" short = "❰if❱ branches must have matching types\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr1 expr3 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr3)
long = long =
"Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\ "Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\
@ -1954,7 +1954,7 @@ prettyTypeMessage (MismatchedListElements i expr0 _expr1 expr2) =
where where
short = "List elements should all have the same type\n" short = "List elements should all have the same type\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr2 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr2)
long = long =
"Explanation: Every element in a list must have the same type \n\ "Explanation: Every element in a list must have the same type \n\
@ -1992,7 +1992,7 @@ prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =
where where
short = "List element has the wrong type\n" short = "List element has the wrong type\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr2 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr2)
long = long =
"Explanation: Every element in the list must have a type matching the type \n\ "Explanation: Every element in the list must have a type matching the type \n\
@ -2350,7 +2350,7 @@ prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}
where where
short = "You can only append ❰List❱s with matching element types\n" short = "You can only append ❰List❱s with matching element types\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr1 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)
long = long =
"Explanation: You can append two ❰List❱s using the ❰#❱ operator, like this: \n\ "Explanation: You can append two ❰List❱s using the ❰#❱ operator, like this: \n\
@ -2878,7 +2878,7 @@ prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
where where
short = "Wrong handler input type\n" short = "Wrong handler input type\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr1 expr2 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)
long = long =
"Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\ "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@ -2940,7 +2940,7 @@ prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
where where
short = "Wrong handler output type\n" short = "Wrong handler output type\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr1 expr2 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr1 expr2)
long = long =
"Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\ "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@ -3004,7 +3004,7 @@ prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =
where where
short = "Handlers should have the same output type\n" short = "Handlers should have the same output type\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr1 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)
long = long =
"Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\ "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@ -3142,7 +3142,7 @@ prettyTypeMessage (MapTypeMismatch expr0 expr1) = ErrorMessages {..}
where where
short = "❰toMap❱ result type doesn't match annotation" short = "❰toMap❱ result type doesn't match annotation"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr1 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)
long = long =
"Explanation: a ❰toMap❱ application has been annotated with a type that doesn't \n\ "Explanation: a ❰toMap❱ application has been annotated with a type that doesn't \n\
@ -3453,7 +3453,7 @@ prettyTypeMessage (ProjectionTypeMismatch k expr0 expr1 expr2 expr3) = ErrorMess
where where
short = "Projection type mismatch\n" short = "Projection type mismatch\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr2 expr3 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr2 expr3)
long = long =
"Explanation: You can project a subset of fields from a record by specifying the \n\ "Explanation: You can project a subset of fields from a record by specifying the \n\
@ -3500,7 +3500,7 @@ prettyTypeMessage (AssertionFailed expr0 expr1) = ErrorMessages {..}
where where
short = "Assertion failed\n" short = "Assertion failed\n"
<> "\n" <> "\n"
<> Dhall.Diff.diffNormalized expr0 expr1 <> Dhall.Diff.doc (Dhall.Diff.diffNormalized expr0 expr1)
long = long =
"Explanation: You can assert at type-checking time that two terms are equal if \n\ "Explanation: You can assert at type-checking time that two terms are equal if \n\

View File

@ -48,7 +48,7 @@ diffTest prefix =
expectedDiffText <- Text.IO.readFile diffFile expectedDiffText <- Text.IO.readFile diffFile
let actualDiffDocument = let actualDiffDocument =
Diff.diffNormalized leftInput rightInput <> "\n" Diff.doc (Diff.diffNormalized leftInput rightInput) <> "\n"
let options = let options =
Pretty.LayoutOptions Pretty.LayoutOptions

View File

@ -379,7 +379,7 @@ normalizeWithMIsConsistentWithNormalize expression =
isSameAsSelf :: Expr () Import -> Property isSameAsSelf :: Expr () Import -> Property
isSameAsSelf expression = isSameAsSelf expression =
hasNoImportAndTypechecks ==> Dhall.Diff.same (Dhall.Diff.diffExpression denoted denoted) hasNoImportAndTypechecks ==> Dhall.Diff.same (Dhall.Diff.diff denoted denoted)
where denoted = Dhall.Core.denote expression where denoted = Dhall.Core.denote expression
hasNoImportAndTypechecks = hasNoImportAndTypechecks =
case traverse (\_ -> Left ()) expression of case traverse (\_ -> Left ()) expression of

View File

@ -1,4 +1,4 @@
λ(… : … λ(… : …
→ …) → …)
→ …@… → …

View File

@ -0,0 +1,6 @@
→ …
→ …@- 1
+ 0
→ …

View File

@ -0,0 +1 @@
∀(a : Type) → ∀(b : Type) → ∀(x : a) → Bool

View File

@ -0,0 +1 @@
∀(a : Type) → ∀(b : Type) → ∀(x : b) → Bool