Add new ⩓ operator for merging record types (#342)
... as standardized in https://github.com/dhall-lang/dhall-lang/pull/117
This commit is contained in:
Gabriel Gonzalez
GitHub
parent
4b2e428d06
commit
9cb89df6d6
|
|
@ -82,6 +82,7 @@ Extra-Source-Files:
|
|||
Prelude/Text/concatMapSep
|
||||
Prelude/Text/concatSep
|
||||
tests/format/*.dhall
|
||||
tests/normalization/tutorial/combineTypes/*.dhall
|
||||
tests/normalization/*.dhall
|
||||
tests/normalization/examples/Bool/and/*.dhall
|
||||
tests/normalization/examples/Bool/build/*.dhall
|
||||
|
|
|
|||
|
|
@ -315,6 +315,8 @@ data Expr s a
|
|||
| UnionLit Text (Expr s a) (InsOrdHashMap Text (Expr s a))
|
||||
-- | > Combine x y ~ x ∧ y
|
||||
| Combine (Expr s a) (Expr s a)
|
||||
-- | > CombineTypes x y ~ x ⩓ y
|
||||
| CombineTypes (Expr s a) (Expr s a)
|
||||
-- | > CombineRight x y ~ x ⫽ y
|
||||
| Prefer (Expr s a) (Expr s a)
|
||||
-- | > Merge x y (Just t ) ~ merge x y : t
|
||||
|
|
@ -391,6 +393,7 @@ instance Monad (Expr s) where
|
|||
Union a >>= k = Union (fmap (>>= k) a)
|
||||
UnionLit a b c >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)
|
||||
Combine a b >>= k = Combine (a >>= k) (b >>= k)
|
||||
CombineTypes a b >>= k = CombineTypes (a >>= k) (b >>= k)
|
||||
Prefer a b >>= k = Prefer (a >>= k) (b >>= k)
|
||||
Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)
|
||||
Constructors a >>= k = Constructors (a >>= k)
|
||||
|
|
@ -452,6 +455,7 @@ instance Bifunctor Expr where
|
|||
first k (Union a ) = Union (fmap (first k) a)
|
||||
first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c)
|
||||
first k (Combine a b ) = Combine (first k a) (first k b)
|
||||
first k (CombineTypes a b ) = CombineTypes (first k a) (first k b)
|
||||
first k (Prefer a b ) = Prefer (first k a) (first k b)
|
||||
first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c)
|
||||
first k (Constructors a ) = Constructors (first k a)
|
||||
|
|
@ -690,6 +694,10 @@ shift d v (Combine a b) = Combine a' b'
|
|||
where
|
||||
a' = shift d v a
|
||||
b' = shift d v b
|
||||
shift d v (CombineTypes a b) = CombineTypes a' b'
|
||||
where
|
||||
a' = shift d v a
|
||||
b' = shift d v b
|
||||
shift d v (Prefer a b) = Prefer a' b'
|
||||
where
|
||||
a' = shift d v a
|
||||
|
|
@ -830,6 +838,10 @@ subst x e (Combine a b) = Combine a' b'
|
|||
where
|
||||
a' = subst x e a
|
||||
b' = subst x e b
|
||||
subst x e (CombineTypes a b) = CombineTypes a' b'
|
||||
where
|
||||
a' = subst x e a
|
||||
b' = subst x e b
|
||||
subst x e (Prefer a b) = Prefer a' b'
|
||||
where
|
||||
a' = subst x e a
|
||||
|
|
@ -1074,6 +1086,12 @@ alphaNormalize (Combine l₀ r₀) =
|
|||
where
|
||||
l₁ = alphaNormalize l₀
|
||||
|
||||
r₁ = alphaNormalize r₀
|
||||
alphaNormalize (CombineTypes l₀ r₀) =
|
||||
CombineTypes l₁ r₁
|
||||
where
|
||||
l₁ = alphaNormalize l₀
|
||||
|
||||
r₁ = alphaNormalize r₀
|
||||
alphaNormalize (Prefer l₀ r₀) =
|
||||
Prefer l₁ r₁
|
||||
|
|
@ -1194,6 +1212,7 @@ denote (RecordLit a ) = RecordLit (fmap denote a)
|
|||
denote (Union a ) = Union (fmap denote a)
|
||||
denote (UnionLit a b c ) = UnionLit a (denote b) (fmap denote c)
|
||||
denote (Combine a b ) = Combine (denote a) (denote b)
|
||||
denote (CombineTypes a b ) = CombineTypes (denote a) (denote b)
|
||||
denote (Prefer a b ) = Prefer (denote a) (denote b)
|
||||
denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c)
|
||||
denote (Constructors a ) = Constructors (denote a)
|
||||
|
|
@ -1493,6 +1512,17 @@ normalizeWith ctx e0 = loop (denote e0)
|
|||
RecordLit (Data.HashMap.Strict.InsOrd.unionWith decide m n)
|
||||
decide l r =
|
||||
Combine l r
|
||||
CombineTypes x y -> decide (loop x) (loop y)
|
||||
where
|
||||
decide (Record m) r | Data.HashMap.Strict.InsOrd.null m =
|
||||
r
|
||||
decide l (Record n) | Data.HashMap.Strict.InsOrd.null n =
|
||||
l
|
||||
decide (Record m) (Record n) =
|
||||
Record (Data.HashMap.Strict.InsOrd.unionWith decide m n)
|
||||
decide l r =
|
||||
CombineTypes l r
|
||||
|
||||
Prefer x y -> decide (loop x) (loop y)
|
||||
where
|
||||
decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m =
|
||||
|
|
@ -1704,6 +1734,13 @@ isNormalized e = case denote e of
|
|||
RecordLit _ -> False
|
||||
_ -> True
|
||||
_ -> True
|
||||
CombineTypes x y -> isNormalized x && isNormalized y && combine
|
||||
where
|
||||
combine = case x of
|
||||
Record _ -> case y of
|
||||
Record _ -> False
|
||||
_ -> True
|
||||
_ -> True
|
||||
Prefer x y -> isNormalized x && isNormalized y && combine
|
||||
where
|
||||
combine = case x of
|
||||
|
|
|
|||
|
|
@ -489,6 +489,12 @@ skeleton (Combine {}) =
|
|||
<> operator "∧"
|
||||
<> " "
|
||||
<> ignore
|
||||
skeleton (CombineTypes {}) =
|
||||
ignore
|
||||
<> " "
|
||||
<> operator "⩓"
|
||||
<> " "
|
||||
<> ignore
|
||||
skeleton (Prefer {}) =
|
||||
ignore
|
||||
<> " "
|
||||
|
|
@ -739,14 +745,29 @@ diffPrefer l@(Prefer {}) r@(Prefer {}) =
|
|||
enclosed' " " (operator "⫽" <> " ") (docs l r)
|
||||
where
|
||||
docs (Prefer aL bL) (Prefer aR bR) =
|
||||
Data.List.NonEmpty.cons (diffNaturalTimes aL aR) (docs bL bR)
|
||||
Data.List.NonEmpty.cons (diffCombineTypes aL aR) (docs bL bR)
|
||||
docs aL aR =
|
||||
pure (diffNaturalTimes aL aR)
|
||||
pure (diffCombineTypes aL aR)
|
||||
diffPrefer l@(Prefer {}) r =
|
||||
mismatch l r
|
||||
diffPrefer l r@(Prefer {}) =
|
||||
mismatch l r
|
||||
diffPrefer l r =
|
||||
diffCombineTypes l r
|
||||
|
||||
diffCombineTypes :: Pretty a => Expr s a -> Expr s a -> Diff
|
||||
diffCombineTypes l@(CombineTypes {}) r@(CombineTypes {}) =
|
||||
enclosed' " " (operator "*" <> " ") (docs l r)
|
||||
where
|
||||
docs (CombineTypes aL bL) (CombineTypes aR bR) =
|
||||
Data.List.NonEmpty.cons (diffNaturalTimes aL aR) (docs bL bR)
|
||||
docs aL aR =
|
||||
pure (diffNaturalTimes aL aR)
|
||||
diffCombineTypes l@(CombineTypes {}) r =
|
||||
mismatch l r
|
||||
diffCombineTypes l r@(CombineTypes {}) =
|
||||
mismatch l r
|
||||
diffCombineTypes l r =
|
||||
diffNaturalTimes l r
|
||||
|
||||
diffNaturalTimes :: Pretty a => Expr s a -> Expr s a -> Diff
|
||||
|
|
|
|||
|
|
@ -683,6 +683,11 @@ _combine = do
|
|||
void (Text.Parser.Char.char '∧' <?> "\"∧\"") <|> void (Text.Parser.Char.text "/\\")
|
||||
whitespace
|
||||
|
||||
_combineTypes :: Parser ()
|
||||
_combineTypes = do
|
||||
void (Text.Parser.Char.char '⩓' <?> "\"⩓\"") <|> void (Text.Parser.Char.text "//\\\\")
|
||||
whitespace
|
||||
|
||||
_prefer :: Parser ()
|
||||
_prefer = do
|
||||
void (Text.Parser.Char.char '⫽' <?> "\"⫽\"") <|> void (Text.Parser.Char.text "//")
|
||||
|
|
@ -1149,7 +1154,11 @@ combineExpression =
|
|||
|
||||
preferExpression :: Parser a -> Parser (Expr Src a)
|
||||
preferExpression =
|
||||
makeOperatorExpression timesExpression _prefer Prefer
|
||||
makeOperatorExpression combineTypesExpression _prefer Prefer
|
||||
|
||||
combineTypesExpression :: Parser a -> Parser (Expr Src a)
|
||||
combineTypesExpression =
|
||||
makeOperatorExpression timesExpression _combineTypes CombineTypes
|
||||
|
||||
timesExpression :: Parser a -> Parser (Expr Src a)
|
||||
timesExpression =
|
||||
|
|
|
|||
|
|
@ -600,10 +600,10 @@ prettyExprC6 a0 =
|
|||
prettyExprC7 a0
|
||||
|
||||
prettyExprC7 :: Pretty a => Expr s a -> Doc Ann
|
||||
prettyExprC7 a0@(NaturalTimes _ _) =
|
||||
enclose' "" " " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))
|
||||
prettyExprC7 a0@(CombineTypes _ _) =
|
||||
enclose' "" " " (" " <> operator "⩓" <> " ") (operator "⩓" <> " ") (fmap duplicate (docs a0))
|
||||
where
|
||||
docs (NaturalTimes a b) = prettyExprC8 a : docs b
|
||||
docs (CombineTypes a b) = prettyExprC8 a : docs b
|
||||
docs (Note _ b) = docs b
|
||||
docs b = [ prettyExprC8 b ]
|
||||
prettyExprC7 (Note _ a) =
|
||||
|
|
@ -612,27 +612,39 @@ prettyExprC7 a0 =
|
|||
prettyExprC8 a0
|
||||
|
||||
prettyExprC8 :: Pretty a => Expr s a -> Doc Ann
|
||||
prettyExprC8 a0@(BoolEQ _ _) =
|
||||
enclose' "" " " (" " <> operator "==" <> " ") (operator "==" <> " ") (fmap duplicate (docs a0))
|
||||
prettyExprC8 a0@(NaturalTimes _ _) =
|
||||
enclose' "" " " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))
|
||||
where
|
||||
docs (BoolEQ a b) = prettyExprC9 a : docs b
|
||||
docs (Note _ b) = docs b
|
||||
docs b = [ prettyExprC9 b ]
|
||||
docs (NaturalTimes a b) = prettyExprC9 a : docs b
|
||||
docs (Note _ b) = docs b
|
||||
docs b = [ prettyExprC9 b ]
|
||||
prettyExprC8 (Note _ a) =
|
||||
prettyExprC8 a
|
||||
prettyExprC8 a0 =
|
||||
prettyExprC9 a0
|
||||
|
||||
prettyExprC9 :: Pretty a => Expr s a -> Doc Ann
|
||||
prettyExprC9 a0@(BoolNE _ _) =
|
||||
prettyExprC9 a0@(BoolEQ _ _) =
|
||||
enclose' "" " " (" " <> operator "==" <> " ") (operator "==" <> " ") (fmap duplicate (docs a0))
|
||||
where
|
||||
docs (BoolEQ a b) = prettyExprC10 a : docs b
|
||||
docs (Note _ b) = docs b
|
||||
docs b = [ prettyExprC10 b ]
|
||||
prettyExprC9 (Note _ a) =
|
||||
prettyExprC9 a
|
||||
prettyExprC9 a0 =
|
||||
prettyExprC10 a0
|
||||
|
||||
prettyExprC10 :: Pretty a => Expr s a -> Doc Ann
|
||||
prettyExprC10 a0@(BoolNE _ _) =
|
||||
enclose' "" " " (" " <> operator "!=" <> " ") (operator "!=" <> " ") (fmap duplicate (docs a0))
|
||||
where
|
||||
docs (BoolNE a b) = prettyExprD a : docs b
|
||||
docs (Note _ b) = docs b
|
||||
docs b = [ prettyExprD b ]
|
||||
prettyExprC9 (Note _ a) =
|
||||
prettyExprC9 a
|
||||
prettyExprC9 a0 =
|
||||
prettyExprC10 (Note _ a) =
|
||||
prettyExprC10 a
|
||||
prettyExprC10 a0 =
|
||||
prettyExprD a0
|
||||
|
||||
prettyExprD :: Pretty a => Expr s a -> Doc Ann
|
||||
|
|
@ -976,21 +988,27 @@ buildExprC6 a = buildExprC7 a
|
|||
|
||||
-- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser"
|
||||
buildExprC7 :: Buildable a => Expr s a -> Builder
|
||||
buildExprC7 (NaturalTimes a b) = buildExprC8 a <> " * " <> buildExprC7 b
|
||||
buildExprC7 (CombineTypes a b) = buildExprC8 a <> " ⩓ " <> buildExprC7 b
|
||||
buildExprC7 (Note _ b) = buildExprC7 b
|
||||
buildExprC7 a = buildExprC8 a
|
||||
|
||||
-- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser"
|
||||
buildExprC8 :: Buildable a => Expr s a -> Builder
|
||||
buildExprC8 (BoolEQ a b) = buildExprC9 a <> " == " <> buildExprC8 b
|
||||
buildExprC8 (Note _ b) = buildExprC8 b
|
||||
buildExprC8 a = buildExprC9 a
|
||||
buildExprC8 (NaturalTimes a b) = buildExprC9 a <> " * " <> buildExprC8 b
|
||||
buildExprC8 (Note _ b) = buildExprC8 b
|
||||
buildExprC8 a = buildExprC9 a
|
||||
|
||||
-- | Builder corresponding to the @exprC9@ parser in "Dhall.Parser"
|
||||
buildExprC9 :: Buildable a => Expr s a -> Builder
|
||||
buildExprC9 (BoolNE a b) = buildExprD a <> " != " <> buildExprC9 b
|
||||
buildExprC9 (BoolEQ a b) = buildExprC10 a <> " == " <> buildExprC9 b
|
||||
buildExprC9 (Note _ b) = buildExprC9 b
|
||||
buildExprC9 a = buildExprD a
|
||||
buildExprC9 a = buildExprC10 a
|
||||
|
||||
-- | Builder corresponding to the @exprC10@ parser in "Dhall.Parser"
|
||||
buildExprC10 :: Buildable a => Expr s a -> Builder
|
||||
buildExprC10 (BoolNE a b) = buildExprD a <> " != " <> buildExprC10 b
|
||||
buildExprC10 (Note _ b) = buildExprC10 b
|
||||
buildExprC10 a = buildExprD a
|
||||
|
||||
-- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"
|
||||
buildExprD :: Buildable a => Expr s a -> Builder
|
||||
|
|
|
|||
|
|
@ -900,6 +900,21 @@ import Dhall
|
|||
--
|
||||
-- __Exercise__: Combine any record with the empty record. What do you expect
|
||||
-- to happen?
|
||||
--
|
||||
-- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53):
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > { foo : Natural } ⩓ { bar : Text }
|
||||
-- > <Ctrl-D>
|
||||
-- > { foo : Natural, bar : Text }
|
||||
--
|
||||
-- ... which behaves the exact same, except at the type level, meaning that the
|
||||
-- operator descends recursively into record types:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }
|
||||
-- > <Ctrl-D>
|
||||
-- > { foo : { bar : Text, baz : Bool }, qux : Integer }
|
||||
|
||||
-- $let
|
||||
--
|
||||
|
|
|
|||
|
|
@ -539,6 +539,52 @@ typeWithA tpa = loop
|
|||
return (Record (Data.HashMap.Strict.InsOrd.fromList kts))
|
||||
|
||||
combineTypes ktsX ktsY
|
||||
loop ctx e@(CombineTypes l r) = do
|
||||
tL <- loop ctx l
|
||||
let l' = Dhall.Core.normalize l
|
||||
cL <- case tL of
|
||||
Const cL -> return cL
|
||||
_ -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
|
||||
tR <- loop ctx r
|
||||
let r' = Dhall.Core.normalize r
|
||||
cR <- case tR of
|
||||
Const cR -> return cR
|
||||
_ -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))
|
||||
let decide Type Type =
|
||||
return Type
|
||||
decide Kind Kind =
|
||||
return Kind
|
||||
decide x y =
|
||||
Left (TypeError ctx e (RecordTypeMismatch x y l r))
|
||||
c <- decide cL cR
|
||||
|
||||
ktsL0 <- case l' of
|
||||
Record kts -> return kts
|
||||
_ -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
|
||||
ktsR0 <- case r' of
|
||||
Record kts -> return kts
|
||||
_ -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))
|
||||
|
||||
let combineTypes ktsL ktsR = do
|
||||
let ksL =
|
||||
Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsL)
|
||||
let ksR =
|
||||
Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsR)
|
||||
let ks = Data.Set.union ksL ksR
|
||||
forM_ (toList ks) (\k -> do
|
||||
case (Data.HashMap.Strict.InsOrd.lookup k ktsL, Data.HashMap.Strict.InsOrd.lookup k ktsR) of
|
||||
(Just (Record ktsL'), Just (Record ktsR')) -> do
|
||||
combineTypes ktsL' ktsR'
|
||||
(Nothing, Just _) -> do
|
||||
return ()
|
||||
(Just _, Nothing) -> do
|
||||
return ()
|
||||
_ -> do
|
||||
Left (TypeError ctx e (FieldCollision k)) )
|
||||
|
||||
combineTypes ktsL0 ktsR0
|
||||
|
||||
return (Const c)
|
||||
loop ctx e@(Prefer kvsX kvsY) = do
|
||||
tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)
|
||||
ktsX <- case tKvsX of
|
||||
|
|
@ -701,6 +747,8 @@ data TypeMessage s a
|
|||
| ListAppendMismatch (Expr s a) (Expr s a)
|
||||
| DuplicateAlternative Text
|
||||
| MustCombineARecord Char (Expr s a) (Expr s a)
|
||||
| CombineTypesRequiresRecordType (Expr s a) (Expr s a)
|
||||
| RecordTypeMismatch Const Const (Expr s a) (Expr s a)
|
||||
| FieldCollision Text
|
||||
| MustMergeARecord (Expr s a) (Expr s a)
|
||||
| MustMergeUnion (Expr s a) (Expr s a)
|
||||
|
|
@ -2346,13 +2394,103 @@ prettyTypeMessage (MustCombineARecord c expr0 expr1) = ErrorMessages {..}
|
|||
txt0 = build expr0
|
||||
txt1 = build expr1
|
||||
|
||||
prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) =
|
||||
ErrorMessages {..}
|
||||
where
|
||||
short = "❰⩓❱ requires arguments that are record types"
|
||||
|
||||
long =
|
||||
"Explanation: You can only use the ❰⩓❱ operator on arguments that are record type\n\
|
||||
\literals, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────┐ \n\
|
||||
\ │ { age : Natural } ⩓ { name : Text } │ \n\
|
||||
\ └─────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\... but you cannot use the ❰⩓❱ operator on any other type of arguments. For \n\
|
||||
\example, you cannot use variable arguments: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────────┐ \n\
|
||||
\ │ λ(t : Type) → t ⩓ { name : Text } │ Invalid: ❰t❱ might not be a record \n\
|
||||
\ └───────────────────────────────────┘ type \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\────────────────────────────────────────────────────────────────────────────────\n\
|
||||
\ \n\
|
||||
\You tried to supply the following argument: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt0 <> " \n\
|
||||
\ \n\
|
||||
\... which normalized to: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt1 <> " \n\
|
||||
\ \n\
|
||||
\... which is not a record type literal \n"
|
||||
where
|
||||
txt0 = build expr0
|
||||
txt1 = build expr1
|
||||
|
||||
prettyTypeMessage (RecordTypeMismatch const0 const1 expr0 expr1) =
|
||||
ErrorMessages {..}
|
||||
where
|
||||
short = "Record type mismatch"
|
||||
|
||||
long =
|
||||
"Explanation: You can only use the ❰⩓❱ operator on record types if they are both \n\
|
||||
\ ❰Type❱s or ❰Kind❱s: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────┐ \n\
|
||||
\ │ { age : Natural } ⩓ { name : Text } │ Valid: Both arguments are ❰Type❱s \n\
|
||||
\ └─────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────────┐ \n\
|
||||
\ │ { Input : Type } ⩓ { Output : Type } │ Valid: Both arguments are ❰Kind❱s \n\
|
||||
\ └──────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\... but you cannot combine a ❰Type❱ and a ❰Kind❱: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────────────────┐ \n\
|
||||
\ │ { Input : Type } ⩓ { name : Text } │ Invalid: The arguments do not match \n\
|
||||
\ └────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\────────────────────────────────────────────────────────────────────────────────\n\
|
||||
\ \n\
|
||||
\You tried to combine the following record type: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt0 <> " \n\
|
||||
\ \n\
|
||||
\... with this record types: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt1 <> " \n\
|
||||
\ \n\
|
||||
\... but the former record type is a: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt2 <> " \n\
|
||||
\ \n\
|
||||
\... but the latter record type is a: \n\
|
||||
\ \n\
|
||||
\↳ " <> txt3 <> " \n"
|
||||
where
|
||||
txt0 = build expr0
|
||||
txt1 = build expr1
|
||||
txt2 = build const0
|
||||
txt3 = build const1
|
||||
|
||||
prettyTypeMessage (FieldCollision k) = ErrorMessages {..}
|
||||
where
|
||||
short = "Field collision"
|
||||
|
||||
long =
|
||||
"Explanation: You can combine records if they don't share any fields in common, \n\
|
||||
\like this: \n\
|
||||
"Explanation: You can combine records or record types if they don't share any \n\
|
||||
\fields in common, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────────────────┐ \n\
|
||||
|
|
@ -2360,19 +2498,43 @@ prettyTypeMessage (FieldCollision k) = ErrorMessages {..}
|
|||
\ └───────────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────┐ \n\
|
||||
\ │ { foo : Text } ⩓ { bar : Bool } │ \n\
|
||||
\ └─────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────────────────────┐ \n\
|
||||
\ │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │ \n\
|
||||
\ └────────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\... but you cannot merge two records that share the same field \n\
|
||||
\... but you cannot merge two records that share the same field unless the field \n\
|
||||
\is a record on both sides. \n\
|
||||
\ \n\
|
||||
\For example, the following expression is " <> _NOT <> " valid: \n\
|
||||
\For example, the following expressions are " <> _NOT <> " valid: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────────────────┐ \n\
|
||||
\ │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ fields\n\
|
||||
\ └───────────────────────────────────────────┘ \n\
|
||||
\ │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ \n\
|
||||
\ └───────────────────────────────────────────┘ fields \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────┐ \n\
|
||||
\ │ { foo : Bool } ∧ { foo : Text } │ Invalid: Colliding ❰foo❱ fields \n\
|
||||
\ └─────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\... but the following expressions are valid: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────────────────────┐ \n\
|
||||
\ │ { foo = { bar = True } } ∧ { foo = { baz = 1 } } │ Valid: Both ❰foo❱ \n\
|
||||
\ └──────────────────────────────────────────────────┘ fields are records \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────┐ \n\
|
||||
\ │ { foo : { bar : Bool } } ⩓ { foo : { baz : Text } } │ Valid: Both ❰foo❱ \n\
|
||||
\ └─────────────────────────────────────────────────────┘ fields are records \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\Some common reasons why you might get this error: \n\
|
||||
|
|
|
|||
|
|
@ -24,7 +24,8 @@ import Util
|
|||
normalizationTests :: TestTree
|
||||
normalizationTests =
|
||||
testGroup "normalization"
|
||||
[ examples
|
||||
[ tutorialExamples
|
||||
, preludeExamples
|
||||
, simplifications
|
||||
, constantFolding
|
||||
, conversions
|
||||
|
|
@ -33,8 +34,14 @@ normalizationTests =
|
|||
, shouldNormalize "a remote-systems.conf builder" "remoteSystems"
|
||||
]
|
||||
|
||||
examples :: TestTree
|
||||
examples =
|
||||
tutorialExamples :: TestTree
|
||||
tutorialExamples =
|
||||
testGroup "Tutorial examples"
|
||||
[ shouldNormalize "⩓" "./tutorial/combineTypes/0"
|
||||
]
|
||||
|
||||
preludeExamples :: TestTree
|
||||
preludeExamples =
|
||||
testGroup "Prelude examples"
|
||||
[ shouldNormalize "Bool/and" "./examples/Bool/and/0"
|
||||
, shouldNormalize "Bool/and" "./examples/Bool/and/1"
|
||||
|
|
|
|||
1
tests/normalization/tutorial/combineTypes/0A.dhall
Normal file
1
tests/normalization/tutorial/combineTypes/0A.dhall
Normal file
|
|
@ -0,0 +1 @@
|
|||
{ foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }
|
||||
1
tests/normalization/tutorial/combineTypes/0B.dhall
Normal file
1
tests/normalization/tutorial/combineTypes/0B.dhall
Normal file
|
|
@ -0,0 +1 @@
|
|||
{ foo : { bar : Text, baz : Bool }, qux : Integer }
|
||||
Loading…
Reference in New Issue
Block a user