Skip to content

Commit

Permalink
Implement "Generalize empty list annotations"
Browse files Browse the repository at this point in the history 
…as standardized in dhall-lang/dhall-lang#630

Also:

* Update the dhall-lang submodule to the state of
  dhall-lang/dhall-lang#654.

* Skip the nonCharacter test for now.
  • Loading branch information
@sjakobi
sjakobi committed Jul 20, 2019
1 parent 8aa8add commit ed6e334
Show file tree
Hide file tree
Showing 9 changed files with 79 additions and 54 deletions.
2 changes: 1 addition & 1 deletion dhall/dhall-lang
Submodule dhall-lang updated 34 files
+0 −14 Prelude/Map.dhall
+66 −0 Prelude/XML/Type
+3 −0 Prelude/XML/attribute
+67 −0 Prelude/XML/element
+3 −0 Prelude/XML/emptyAttributes
+32 −0 Prelude/XML/leaf
+19 −0 Prelude/XML/package.dhall
+69 −0 Prelude/XML/render
+41 −0 Prelude/XML/text
+3 −0 Prelude/package.dhall
+1 −1 standard/README.md
+2 −2 standard/alpha-normalization.md
+34 −20 standard/beta-normalization.md
+14 −1 standard/binary.md
+61 −8 standard/dhall.abnf
+2 −2 standard/shift.md
+2 −2 standard/substitution.md
+3 −3 standard/type-inference.md
+1 −1 tests/normalization/success/unit/ListNormalizeTypeAnnotationA.dhall
+1 −1 tests/normalization/success/unit/ListNormalizeTypeAnnotationB.dhall
+1 −0 tests/normalization/success/unit/RecordProjectionNormalizeFieldsA.dhall
+1 −0 tests/normalization/success/unit/RecordProjectionNormalizeFieldsB.dhall
+1 −0 tests/parser/failure/nonCharacter.dhall
+4 −0 tests/parser/failure/nonUtf8.dhall
+0 −0 tests/parser/success/unit/ListLitEmpty1A.dhall
+ − tests/parser/success/unit/ListLitEmpty1B.dhallb
+1 −0 tests/parser/success/unit/ListLitEmpty2A.dhall
+ − tests/parser/success/unit/ListLitEmpty2B.dhallb
+0 −0 tests/parser/success/unit/ListLitEmptyPrecedenceA.dhall
+ − tests/parser/success/unit/ListLitEmptyPrecedenceB.dhallb
+1 −0 tests/type-inference/success/unit/ListLiteralEmptyNormalizeAnnotationA.dhall
+1 −0 tests/type-inference/success/unit/ListLiteralEmptyNormalizeAnnotationB.dhall
+1 −0 tests/typecheck/failure/unit/OptionalDeprecatedSyntaxAbsent.dhall
+1 −0 tests/typecheck/failure/unit/OptionalDeprecatedSyntaxPresent.dhall
15 changes: 10 additions & 5 deletions dhall/src/Dhall/Binary.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ import qualified Control.Monad as Monad
import qualified Data.ByteArray
import qualified Data.ByteString
import qualified Data.Sequence
import qualified Dhall.Core
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Options.Applicative
Expand Down Expand Up @@ -281,12 +282,13 @@ instance ToTerm a => ToTerm (Expr s a) where
l₁ = encode l₀
r₁ = encode r₀
encode (ListLit _T₀ xs₀)
| null xs₀ = TList [ TInt 4, _T₁ ]
| null xs₀ = TList [ TInt label, _T₁ ]
| otherwise = TList ([ TInt 4, TNull ] ++ xs₁)
where
_T₁ = case _T₀ of
Nothing -> TNull
Just t -> encode t
(label, _T₁) = case fmap Dhall.Core.denote _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₀) =
Expand Down Expand Up @@ -614,7 +616,7 @@ instance FromTerm a => FromTerm (Expr s a) where
return (op l₀ r₀)
decode (TList [ TInt 4, _T₁ ]) = do
_T₀ <- decode _T₁
return (ListLit (Just _T₀) empty)
return (ListLit (Just (App List _T₀)) empty)
decode (TList (TInt 4 : TNull : xs₁ )) = do
xs₀ <- traverse decode xs₁
return (ListLit Nothing (Data.Sequence.fromList xs₀))
Expand Down Expand Up @@ -780,6 +782,9 @@ instance FromTerm a => FromTerm (Expr s a) where
t₀ <- decode t₁
_T₀ <- decode _T₁
return (ToMap t₀ (Just _T₀))
decode (TList [ TInt 28, _T₁ ]) = do
_T₀ <- decode _T₁
return (ListLit (Just _T₀) empty)
decode _ =
empty

Expand Down
14 changes: 7 additions & 7 deletions dhall/src/Dhall/Core.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -426,7 +426,7 @@ data Expr s a
| TextShow
-- | > List ~ List
| List
-- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t
-- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : t
-- > ListLit Nothing [x, y, z] ~ [x, y, z]
| ListLit (Maybe (Expr s a)) (Seq (Expr s a))
-- | > ListAppend x y ~ x # y
Expand Down Expand Up @@ -1417,7 +1417,7 @@ normalizeWithM ctx e0 = loop (denote e0)
(ListAppend (ListLit Nothing (pure "a")) "as")
)

nil = ListLit (Just _A₀) empty
nil = ListLit (Just (App List _A₀)) empty
App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do
t' <- loop t
if boundedType t' then strict else lazy
Expand All @@ -1443,7 +1443,7 @@ normalizeWithM ctx e0 = loop (denote e0)
o = case Data.Sequence.viewr ys of
_ :> y -> Some y
_ -> App None t
App (App ListIndexed _A₀) (ListLit _A₁ as₀) -> loop (ListLit t as₁)
App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)
where
as₁ = Data.Sequence.mapWithIndex adapt as₀

Expand All @@ -1453,7 +1453,7 @@ normalizeWithM ctx e0 = loop (denote e0)
, ("value", _A₀)
]

t | null as₀ = Just _A₂
t | null as₀ = Just (App List _A₂)
| otherwise = Nothing

adapt n a_ =
Expand All @@ -1465,7 +1465,7 @@ normalizeWithM ctx e0 = loop (denote e0)
App (App ListReverse t) (ListLit _ xs) ->
loop (ListLit m (Data.Sequence.reverse xs))
where
m = if Data.Sequence.null xs then Just t else Nothing
m = if Data.Sequence.null xs then Just (App List t) else Nothing
App (App (App (App (App OptionalFold _) (App None _)) _) _) nothing ->
loop nothing
App (App (App (App (App OptionalFold _) (Some x)) _) just) _ ->
Expand Down Expand Up @@ -1697,8 +1697,8 @@ normalizeWithM ctx e0 = loop (denote e0)
let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))

let listType = case t' of
Just (App List itemType) | null keyValues ->
Just itemType
Just _ | null keyValues ->
t'
_ ->
Nothing

Expand Down
7 changes: 2 additions & 5 deletions dhall/src/Dhall/Diff.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ module Dhall.Diff (
) where

import Data.Foldable (fold, toList)
import Data.Function (on)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Monoid (Any(..))
import Data.Semigroup
Expand Down Expand Up @@ -573,8 +572,6 @@ skeleton (ListLit {}) =
<> " "
<> colon
<> " "
<> builtin "List"
<> " "
<> ignore
skeleton (ListAppend {}) =
ignore
Expand Down Expand Up @@ -778,11 +775,11 @@ diffAnnotatedExpression l r@(ToMap {}) =
diffAnnotatedExpression (ListLit aL@(Just _) bL) (ListLit aR bR) = align doc
where
doc = format " " (diffList bL bR)
<> format " " (diffMaybe (colon <> " ") (diffApplicationExpression `on` App List) aL aR)
<> format " " (diffMaybe (colon <> " ") diffApplicationExpression aL aR)
diffAnnotatedExpression (ListLit aL bL) (ListLit aR@(Just _) bR) = align doc
where
doc = format " " (diffList bL bR)
<> format " " (diffMaybe (colon <> " ") (diffApplicationExpression `on` App List) aL aR)
<> format " " (diffMaybe (colon <> " ") diffApplicationExpression aL aR)
diffAnnotatedExpression l@(Annot {}) r@(Annot {}) =
enclosed' " " (colon <> " ") (docs l r)
where
Expand Down
10 changes: 5 additions & 5 deletions dhall/src/Dhall/Eval.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ eval !env t =
`vApp` VHLam (Typed "a" a) (\x ->
VHLam (Typed "as" (VList a)) (\as ->
vListAppend (VListLit Nothing (pure x)) as))
`vApp` VListLit (Just a) mempty
`vApp` VListLit (Just (VList a)) mempty

ListFold -> VPrim $ \a -> VPrim $ \case
VListLit _ as ->
Expand Down Expand Up @@ -465,8 +465,8 @@ eval !env t =
ListIndexed -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> let
a' = if null as then
Just (VRecord (Dhall.Map.fromList
[("index", VNatural), ("value", a)]))
Just (VList (VRecord (Dhall.Map.fromList
[("index", VNatural), ("value", a)])))
else
Nothing
as' = Data.Sequence.mapWithIndex
Expand Down Expand Up @@ -529,8 +529,8 @@ eval !env t =
| otherwise -> error errorMsg
(x, y, ma) -> VMerge x y ma
ToMap x ma -> case (evalE x, evalE <$> ma) of
(VRecordLit m, Just (VList t)) | null m ->
VListLit (Just t) (Data.Sequence.empty)
(VRecordLit m, ma'@(Just _)) | null m ->
VListLit ma' (Data.Sequence.empty)
(VRecordLit m, _) -> let
entry (k, v) =
VRecordLit (Dhall.Map.fromList [("mapKey", VTextLit $ VChunks [] k),
Expand Down
19 changes: 7 additions & 12 deletions dhall/src/Dhall/Parser/Expression.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,18 +181,13 @@ parsers embedded = Parsers {..}

b <- expression

case (shallowDenote a, shallowDenote b) of
(ListLit _ xs, App f c) ->
case shallowDenote f of
List -> case xs of
[] -> return (ListLit (Just c) xs)
_ -> return (Annot a b)
_ ->
return (Annot a b)
(Merge c d _, e) ->
return (Merge c d (Just e))
(ToMap c _, d) ->
return (ToMap c (Just d))
case shallowDenote a of
ListLit _ [] ->
return (ListLit (Just b) [])
Merge c d _ ->
return (Merge c d (Just b))
ToMap c _ ->
return (ToMap c (Just b))
_ -> return (Annot a b)

alternative4A <|> alternative4B <|> pure a
Expand Down
2 changes: 1 addition & 1 deletion dhall/src/Dhall/Pretty/Internal.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -571,7 +571,7 @@ prettyCharacterSet characterSet expression =
prettyAnnotatedExpression (ListLit (Just a) b) =
list (map prettyExpression (Data.Foldable.toList b))
<> " : "
<> prettyApplicationExpression (App List a)
<> prettyApplicationExpression a
prettyAnnotatedExpression (Note _ a) =
prettyAnnotatedExpression a
prettyAnnotatedExpression a0 =
Expand Down
48 changes: 32 additions & 16 deletions dhall/src/Dhall/TypeCheck.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ typeWithA tpa = loop
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
_ -> Left (TypeError ctx e (InvalidListType (App List t)))
flip traverseWithIndex_ xs' (\i x -> do
t' <- loop ctx x
if Dhall.Core.judgmentallyEqual t t'
Expand All @@ -387,20 +387,25 @@ typeWithA tpa = loop
Left (TypeError ctx x err) )
return (App List t)
_ -> Left (TypeError ctx e MissingListType)
loop ctx e@(ListLit (Just t ) xs) = do
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
loop ctx e@(ListLit (Just t0) xs) = do
_ <- loop ctx t0
let nf_t0 = Dhall.Core.normalize t0
t1 <- case nf_t0 of
App List t1 -> do
s <- fmap Dhall.Core.normalize (loop ctx t1)
case s of
Const Type -> return t1
_ -> Left (TypeError ctx e (InvalidListType nf_t0))
_ -> Left (TypeError ctx e (InvalidListType nf_t0))
flip traverseWithIndex_ xs (\i x -> do
t' <- loop ctx x
if Dhall.Core.judgmentallyEqual t t'
if Dhall.Core.judgmentallyEqual t1 t'
then return ()
else do
let nf_t = Dhall.Core.normalize t
let nf_t = Dhall.Core.normalize t1
let nf_t' = Dhall.Core.normalize t'
Left (TypeError ctx x (InvalidListElement i nf_t x nf_t')) )
return (App List t)
return (App List t1)
loop ctx e@(ListAppend l r ) = do
tl <- fmap Dhall.Core.normalize (loop ctx l)
el <- case tl of
Expand Down Expand Up @@ -1874,11 +1879,11 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =

prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
where
short = "Invalid type for ❰List❱ elements"
short = "Invalid type for ❰List❱"

long =
"Explanation: ❰List❱s can optionally document the type of their elements with a \n\
\type annotation, like this: \n\
"Explanation: ❰List❱s can optionally document their type with a type annotation, \n\
\like this: \n\
\ \n\
\ \n\
\ ┌──────────────────────────┐ \n\
Expand All @@ -1892,8 +1897,19 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
\ ┌───────────────────┐ \n\
\ │ [] : List Natural │ An empty ❰List❱ \n\
\ └───────────────────┘ \n\
\ ⇧ \n\
\ You must specify the type when the ❰List❱ is empty \n\
\ ⇧ \n\
\ You must specify the type when the ❰List❱ is empty \n\
\ \n\
\ \n\
\The type must be of the form ❰List ...❱ and not something else. For example, \n\
\the following type annotation is " <> _NOT <> " valid: \n\
\ \n\
\ \n\
\ ┌────────────┐ \n\
\ │ ... : Bool │ \n\
\ └────────────┘ \n\
\ ⇧ \n\
\ This type does not have the form ❰List ...❱ \n\
\ \n\
\ \n\
\The element type must be a type and not something else. For example, the \n\
Expand All @@ -1914,11 +1930,11 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
\ This is a ❰Kind❱ and not a ❰Type❱ \n\
\ \n\
\ \n\
\You declared that the ❰List❱'s elements should have type: \n\
\You declared that the ❰List❱ should have type: \n\
\ \n\
\" <> txt0 <> "\n\
\ \n\
\... which is not a ❰Type❱ \n"
\... which is not a valid list type \n"
where
txt0 = insert expr0

Expand Down
16 changes: 14 additions & 2 deletions dhall/tests/Dhall/Test/Parser.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ import Prelude hiding (FilePath)
import Test.Tasty (TestTree)
import Turtle (FilePath, (</>))

import qualified Codec.CBOR.Read as CBOR
import qualified Codec.CBOR.Term as CBOR
import qualified Codec.Serialise as Serialise
import qualified Control.Monad as Monad
import qualified Data.ByteString as ByteString
Expand Down Expand Up @@ -74,6 +76,9 @@ getTests = do
-- The same performance improvements also broke the
-- precedence of parsing empty list literals
, parseDirectory </> "failure/unit/ListLitEmptyPrecedence.dhall"

-- https://github.com/dhall-lang/dhall-haskell/pull/1104
, parseDirectory </> "failure/nonCharacter.dhall"
]

Monad.guard (path `notElem` skip)
Expand Down Expand Up @@ -126,8 +131,15 @@ shouldParse path = do

let bytes = Serialise.serialise term

let message = "The expected CBOR representation doesn't match the actual one"
Tasty.HUnit.assertEqual message encoded bytes
Monad.unless (encoded == bytes) $ do
("", expected) <- Core.throws (CBOR.deserialiseFromBytes CBOR.decodeTerm encoded)

let message = "The expected CBOR representation doesn't match the actual one\n"
++ "expected: " ++ show expected ++ "\n but got: " ++ show term
++ "\n expr: " ++ show expression

Tasty.HUnit.assertFailure message


shouldNotParse :: Text -> TestTree
shouldNotParse path = do
Expand Down

0 comments on commit ed6e334

Please sign in to comment.