parent
28179ceb76
commit
8c340c12dd
|
@ -255,8 +255,8 @@ data Expr s a
|
|||
| Text
|
||||
-- | > TextLit t ~ t
|
||||
| TextLit Builder
|
||||
-- | > TextAppend x y ~ x ++ y
|
||||
| TextAppend (Expr s a) (Expr s a)
|
||||
-- | > Append x y ~ x ++ y
|
||||
| Append (Expr s a) (Expr s a)
|
||||
-- | > List ~ List
|
||||
| List
|
||||
-- | > ListLit (Just t ) [x, y, z] ~ [x, y, z] : List t
|
||||
|
@ -349,7 +349,7 @@ instance Monad (Expr s) where
|
|||
DoubleShow >>= _ = DoubleShow
|
||||
Text >>= _ = Text
|
||||
TextLit a >>= _ = TextLit a
|
||||
TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k)
|
||||
Append a b >>= k = Append (a >>= k) (b >>= k)
|
||||
List >>= _ = List
|
||||
ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)
|
||||
ListBuild >>= _ = ListBuild
|
||||
|
@ -408,7 +408,7 @@ instance Bifunctor Expr where
|
|||
first _ DoubleShow = DoubleShow
|
||||
first _ Text = Text
|
||||
first _ (TextLit a ) = TextLit a
|
||||
first k (TextAppend a b ) = TextAppend (first k a) (first k b)
|
||||
first k (Append a b ) = Append (first k a) (first k b)
|
||||
first _ List = List
|
||||
first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b)
|
||||
first _ ListBuild = ListBuild
|
||||
|
@ -556,7 +556,7 @@ buildExprC0 a = buildExprC1 a
|
|||
|
||||
-- | Builder corresponding to the @exprC1@ parser in "Dhall.Parser"
|
||||
buildExprC1 :: Buildable a => Expr s a -> Builder
|
||||
buildExprC1 (TextAppend a b) = buildExprC2 a <> " ++ " <> buildExprC1 b
|
||||
buildExprC1 (Append a b) = buildExprC2 a <> " ++ " <> buildExprC1 b
|
||||
buildExprC1 (Note _ b) = buildExprC1 b
|
||||
buildExprC1 a = buildExprC2 a
|
||||
|
||||
|
@ -933,7 +933,7 @@ shift _ _ (DoubleLit a) = DoubleLit a
|
|||
shift _ _ DoubleShow = DoubleShow
|
||||
shift _ _ Text = Text
|
||||
shift _ _ (TextLit a) = TextLit a
|
||||
shift d v (TextAppend a b) = TextAppend a' b'
|
||||
shift d v (Append a b) = Append a' b'
|
||||
where
|
||||
a' = shift d v a
|
||||
b' = shift d v b
|
||||
|
@ -1073,7 +1073,7 @@ subst _ _ (DoubleLit a) = DoubleLit a
|
|||
subst _ _ DoubleShow = DoubleShow
|
||||
subst _ _ Text = Text
|
||||
subst _ _ (TextLit a) = TextLit a
|
||||
subst x e (TextAppend a b) = TextAppend a' b'
|
||||
subst x e (Append a b) = Append a' b'
|
||||
where
|
||||
a' = subst x e a
|
||||
b' = subst x e b
|
||||
|
@ -1384,13 +1384,17 @@ normalizeWith ctx e0 = loop (shift 0 "_" e0)
|
|||
DoubleShow -> DoubleShow
|
||||
Text -> Text
|
||||
TextLit t -> TextLit t
|
||||
TextAppend x y ->
|
||||
Append x y ->
|
||||
case x' of
|
||||
TextLit xt ->
|
||||
case y' of
|
||||
TextLit yt -> TextLit (xt <> yt)
|
||||
_ -> TextAppend x' y'
|
||||
_ -> TextAppend x' y'
|
||||
_ -> Append x' y'
|
||||
ListLit t xs ->
|
||||
case y' of
|
||||
ListLit _ ys -> ListLit t (xs <> ys)
|
||||
_ -> Append x' y'
|
||||
_ -> Append x' y'
|
||||
where
|
||||
x' = loop x
|
||||
y' = loop y
|
||||
|
@ -1615,12 +1619,16 @@ isNormalized e = case shift 0 "_" e of -- `shift` is a hack to delete `Note`
|
|||
DoubleShow -> True
|
||||
Text -> True
|
||||
TextLit _ -> True
|
||||
TextAppend x y -> isNormalized x && isNormalized y &&
|
||||
Append x y -> isNormalized x && isNormalized y &&
|
||||
case x of
|
||||
TextLit _ ->
|
||||
case y of
|
||||
TextLit _ -> False
|
||||
_ -> True
|
||||
ListLit _ _ ->
|
||||
case y of
|
||||
ListLit _ _ -> False
|
||||
_ -> True
|
||||
_ -> True
|
||||
List -> True
|
||||
ListLit t es -> all isNormalized t && all isNormalized es
|
||||
|
|
|
@ -187,7 +187,7 @@ doubleQuoteLiteral embedded = do
|
|||
a <- exprA embedded
|
||||
_ <- Text.Parser.Char.char '}'
|
||||
b <- go
|
||||
return (TextAppend a b)
|
||||
return (Append a b)
|
||||
|
||||
go2 = do
|
||||
_ <- Text.Parser.Char.text "''${"
|
||||
|
@ -195,10 +195,10 @@ doubleQuoteLiteral embedded = do
|
|||
let e = case b of
|
||||
TextLit cs ->
|
||||
TextLit ("${" <> cs)
|
||||
TextAppend (TextLit cs) d ->
|
||||
TextAppend (TextLit ("${" <> cs)) d
|
||||
Append (TextLit cs) d ->
|
||||
Append (TextLit ("${" <> cs)) d
|
||||
_ ->
|
||||
TextAppend (TextLit "${") b
|
||||
Append (TextLit "${") b
|
||||
return e
|
||||
|
||||
go3 = do
|
||||
|
@ -207,10 +207,10 @@ doubleQuoteLiteral embedded = do
|
|||
let e = case b of
|
||||
TextLit cs ->
|
||||
TextLit (build a <> cs)
|
||||
TextAppend (TextLit cs) d ->
|
||||
TextAppend (TextLit (build a <> cs)) d
|
||||
Append (TextLit cs) d ->
|
||||
Append (TextLit (build a <> cs)) d
|
||||
_ ->
|
||||
TextAppend (TextLit (build a)) b
|
||||
Append (TextLit (build a)) b
|
||||
return e
|
||||
|
||||
doubleSingleQuoteString :: Show a => Parser a -> Parser (Expr Src a)
|
||||
|
@ -249,10 +249,10 @@ doubleSingleQuoteString embedded = do
|
|||
[] -> []
|
||||
l:ls -> l:map (Data.Text.Lazy.drop shortestIndent) ls
|
||||
|
||||
let process trim (TextAppend (TextLit t) e) =
|
||||
TextAppend (TextLit (trim t)) (process trim1 e)
|
||||
process _ (TextAppend e0 e1) =
|
||||
TextAppend e0 (process trim1 e1)
|
||||
let process trim (Append (TextLit t) e) =
|
||||
Append (TextLit (trim t)) (process trim1 e)
|
||||
process _ (Append e0 e1) =
|
||||
Append e0 (process trim1 e1)
|
||||
process trim (TextLit t) =
|
||||
TextLit (trim t)
|
||||
process _ e =
|
||||
|
@ -263,8 +263,8 @@ doubleSingleQuoteString embedded = do
|
|||
-- This treats variable interpolation as breaking leading whitespace for the
|
||||
-- purposes of computing the shortest leading whitespace. The "${VAR}"
|
||||
-- could really be any text that breaks whitespace
|
||||
concatFragments (TextAppend (TextLit t) e) = t <> concatFragments e
|
||||
concatFragments (TextAppend _ e) = "${VAR}" <> concatFragments e
|
||||
concatFragments (Append (TextLit t) e) = t <> concatFragments e
|
||||
concatFragments (Append _ e) = "${VAR}" <> concatFragments e
|
||||
concatFragments (TextLit t) = t
|
||||
concatFragments _ = mempty
|
||||
|
||||
|
@ -285,10 +285,10 @@ doubleSingleQuoteString embedded = do
|
|||
let s4 = case s1 of
|
||||
TextLit s2 ->
|
||||
TextLit ("''" <> s2)
|
||||
TextAppend (TextLit s2) s3 ->
|
||||
TextAppend (TextLit ("''" <> s2)) s3
|
||||
Append (TextLit s2) s3 ->
|
||||
Append (TextLit ("''" <> s2)) s3
|
||||
_ ->
|
||||
TextAppend (TextLit "''") s1
|
||||
Append (TextLit "''") s1
|
||||
return s4
|
||||
|
||||
p3 = do
|
||||
|
@ -297,10 +297,10 @@ doubleSingleQuoteString embedded = do
|
|||
let s4 = case s1 of
|
||||
TextLit s2 ->
|
||||
TextLit ("${" <> s2)
|
||||
TextAppend (TextLit s2) s3 ->
|
||||
TextAppend (TextLit ("${" <> s2)) s3
|
||||
Append (TextLit s2) s3 ->
|
||||
Append (TextLit ("${" <> s2)) s3
|
||||
_ ->
|
||||
TextAppend (TextLit "${") s1
|
||||
Append (TextLit "${") s1
|
||||
return s4
|
||||
|
||||
p4 = do
|
||||
|
@ -313,9 +313,9 @@ doubleSingleQuoteString embedded = do
|
|||
let s4 = case s1 of
|
||||
TextLit s2 ->
|
||||
TextLit (build s0 <> s2)
|
||||
TextAppend (TextLit s2) s3 ->
|
||||
TextAppend (TextLit (build s0 <> s2)) s3
|
||||
_ -> TextAppend (TextLit (build s0)) s1
|
||||
Append (TextLit s2) s3 ->
|
||||
Append (TextLit (build s0 <> s2)) s3
|
||||
_ -> Append (TextLit (build s0)) s1
|
||||
return s4
|
||||
|
||||
p6 = do
|
||||
|
@ -324,7 +324,7 @@ doubleSingleQuoteString embedded = do
|
|||
s1 <- exprA embedded
|
||||
_ <- Text.Parser.Char.char '}'
|
||||
s3 <- p1
|
||||
return (TextAppend s1 s3)
|
||||
return (Append s1 s3)
|
||||
|
||||
lambda :: Parser ()
|
||||
lambda = symbol "\\" <|> symbol "λ"
|
||||
|
@ -480,7 +480,7 @@ exprC embedded = exprC0
|
|||
|
||||
exprC0 = chain exprC1 (symbol "||") BoolOr exprC0
|
||||
exprC1 = chain exprC2 (symbol "+" ) NaturalPlus exprC1
|
||||
exprC2 = chain exprC3 (symbol "++") TextAppend exprC2
|
||||
exprC2 = chain exprC3 (symbol "++") Append exprC2
|
||||
exprC3 = chain exprC4 (symbol "&&") BoolAnd exprC3
|
||||
exprC4 = chain exprC5 combine Combine exprC4
|
||||
exprC5 = chain exprC6 prefer Prefer exprC5
|
||||
|
|
|
@ -108,7 +108,7 @@ module Dhall.Tutorial (
|
|||
-- $text
|
||||
|
||||
-- *** @(++)@
|
||||
-- $textAppend
|
||||
-- $append
|
||||
|
||||
-- ** @List@
|
||||
-- $list
|
||||
|
@ -1780,7 +1780,7 @@ import Dhall
|
|||
--
|
||||
-- The only thing you can do with @Text@ values is concatenate them
|
||||
|
||||
-- $textAppend
|
||||
-- $append
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
|
@ -1791,11 +1791,22 @@ import Dhall
|
|||
-- >
|
||||
-- > "Hello, world!"
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > [1, 2, 3] ++ [4, 5, 6]
|
||||
-- >
|
||||
-- > List Integer
|
||||
-- >
|
||||
-- > [1, 2, 3, 4, 5, 6]
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
-- > Γ ⊢ x : Text Γ ⊢ y : Text
|
||||
-- > ───────────────────────────
|
||||
-- > Γ ⊢ x && y : Text
|
||||
-- > Γ ⊢ x ++ y : Text
|
||||
-- >
|
||||
-- > Γ ⊢ x : List a Γ ⊢ y : List a
|
||||
-- > ───────────────────────────
|
||||
-- > Γ ⊢ x ++ y : List a
|
||||
--
|
||||
-- Rules:
|
||||
--
|
||||
|
@ -1804,6 +1815,10 @@ import Dhall
|
|||
-- > x ++ "" = x
|
||||
-- >
|
||||
-- > "" ++ x = x
|
||||
-- >
|
||||
-- > x ++ ([] : List a) = x
|
||||
-- >
|
||||
-- > ([] : List a) ++ x = x
|
||||
|
||||
-- $list
|
||||
--
|
||||
|
|
|
@ -350,17 +350,16 @@ typeWith _ Text = do
|
|||
return (Const Type)
|
||||
typeWith _ (TextLit _ ) = do
|
||||
return Text
|
||||
typeWith ctx e@(TextAppend l r ) = do
|
||||
typeWith ctx e@(Append l r ) = do
|
||||
tl <- fmap Dhall.Core.normalize (typeWith ctx l)
|
||||
case tl of
|
||||
Text -> return ()
|
||||
_ -> Left (TypeError ctx e (CantTextAppend l tl))
|
||||
|
||||
tr <- fmap Dhall.Core.normalize (typeWith ctx r)
|
||||
case tr of
|
||||
Text -> return ()
|
||||
_ -> Left (TypeError ctx e (CantTextAppend r tr))
|
||||
return Text
|
||||
case (tl, tr) of
|
||||
(Text, Text) -> return Text
|
||||
(App List el, App List er) -> do
|
||||
if propEqual el er
|
||||
then return (App List el)
|
||||
else Left (TypeError ctx e (ListAppendMismatch el er))
|
||||
_ -> Left (TypeError ctx e (CantAppend tl tr))
|
||||
typeWith _ List = do
|
||||
return (Pi "_" (Const Type) (Const Type))
|
||||
typeWith ctx e@(ListLit Nothing xs) = do
|
||||
|
@ -681,7 +680,8 @@ data TypeMessage s
|
|||
| CantOr (Expr s X) (Expr s X)
|
||||
| CantEQ (Expr s X) (Expr s X)
|
||||
| CantNE (Expr s X) (Expr s X)
|
||||
| CantTextAppend (Expr s X) (Expr s X)
|
||||
| CantAppend (Expr s X) (Expr s X)
|
||||
| ListAppendMismatch (Expr s X) (Expr s X)
|
||||
| CantAdd (Expr s X) (Expr s X)
|
||||
| CantMultiply (Expr s X) (Expr s X)
|
||||
| NoDependentLet (Expr s X) (Expr s X)
|
||||
|
@ -2853,44 +2853,99 @@ prettyTypeMessage (CantEQ expr0 expr1) =
|
|||
prettyTypeMessage (CantNE expr0 expr1) =
|
||||
buildBooleanOperator "/=" expr0 expr1
|
||||
|
||||
prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..}
|
||||
prettyTypeMessage (CantAppend expr0 expr1) = ErrorMessages {..}
|
||||
where
|
||||
short = "❰++❱ only works on ❰Text❱"
|
||||
short = "❰++❱ can only append values that are both ❰Text❱ or both ❰List❱s"
|
||||
|
||||
long =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱
|
||||
Explanation: The ❰++❱ operator expects two arguments that are both ❰Text❱ or
|
||||
❰List❱s
|
||||
|
||||
For example, this is a valid use of ❰++❱:
|
||||
|
||||
|
||||
┌────────────────┐
|
||||
│ "ABC" ++ "DEF" │
|
||||
│ "ABC" ++ "DEF" │ Valid: Both arguments have type ❰Text❱
|
||||
└────────────────┘
|
||||
|
||||
|
||||
Some common reasons why you might get this error:
|
||||
|
||||
● You might have thought that ❰++❱ was the operator to combine two lists:
|
||||
... and so is this:
|
||||
|
||||
|
||||
┌────────────────────────┐
|
||||
│ [1, 2, 3] ++ [4, 5, 6] │ Not valid
|
||||
│ [1, 2, 3] ++ [4, 5, 6] │ Valid: Both arguments have type ❰List Integer❱
|
||||
└────────────────────────┘
|
||||
|
||||
|
||||
The Dhall programming language does not provide a built-in operator for
|
||||
combining two lists
|
||||
However, this is $_NOT legal:
|
||||
|
||||
|
||||
This has type ❰List Integer❱
|
||||
⇩
|
||||
┌────────────────────┐
|
||||
│ [1, 2, 3] ++ "ABC" │ Invalid: You cannot append different types of values
|
||||
└────────────────────┘
|
||||
⇧
|
||||
This has type ❰Text❱
|
||||
|
||||
|
||||
────────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
You provided this argument:
|
||||
The left argument of ❰++❱ has this type:
|
||||
|
||||
↳ $txt0
|
||||
|
||||
... which does not have type ❰Text❱ but instead has type:
|
||||
... whereas the right argument of ❰++❱ has this type:
|
||||
|
||||
↳ $txt1
|
||||
|
||||
... which is not the same type
|
||||
|]
|
||||
where
|
||||
txt0 = Text.toStrict (Dhall.Core.pretty expr0)
|
||||
txt1 = Text.toStrict (Dhall.Core.pretty expr1)
|
||||
|
||||
prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}
|
||||
where
|
||||
short = "You cannot append ❰List❱s that have different element types"
|
||||
|
||||
long =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Explanation: You can append two ❰List❱s with the ❰++❱ operator if they both
|
||||
have the same element type
|
||||
|
||||
For example, this is a valid use of ❰++❱:
|
||||
|
||||
|
||||
┌────────────────────────┐
|
||||
│ [1, 2, 3] ++ [4, 5, 6] │ Valid: Both ❰List❱s have ❰Integer❱ elements
|
||||
└────────────────────────┘
|
||||
|
||||
|
||||
However, this is $_NOT legal:
|
||||
|
||||
|
||||
This has type ❰List Integer❱
|
||||
⇩
|
||||
┌────────────────────────────┐
|
||||
│ [1, 2, 3] ++ [False, True] │ Invalid: The element types do not match
|
||||
└────────────────────────────┘
|
||||
⇧
|
||||
This has type ❰List Bool❱
|
||||
|
||||
|
||||
────────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
The left argument of ❰++❱ has this type:
|
||||
|
||||
↳ $txt0
|
||||
|
||||
... whereas the right argument of ❰++❱ has this type:
|
||||
|
||||
↳ $txt1
|
||||
|
||||
... which is not the same type
|
||||
|]
|
||||
where
|
||||
txt0 = Text.toStrict (Dhall.Core.pretty expr0)
|
||||
|
|
Loading…
Reference in New Issue
Block a user