Skip to content

Commit

Permalink
Add new operator for merging record types (#342)
Browse files Browse the repository at this point in the history
... as standardized in dhall-lang/dhall-lang#117
  • Loading branch information
Gabriella439 committed Mar 31, 2018
1 parent 4b2e428 commit 9cb89df
Show file tree
Hide file tree
Showing 10 changed files with 302 additions and 30 deletions.
1 change: 1 addition & 0 deletions dhall.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 37 additions & 0 deletions src/Dhall/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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₁
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
25 changes: 23 additions & 2 deletions src/Dhall/Diff.hs
Original file line number Diff line number Diff line change
Expand Up @@ -489,6 +489,12 @@ skeleton (Combine {}) =
<> operator ""
<> " "
<> ignore
skeleton (CombineTypes {}) =
ignore
<> " "
<> operator ""
<> " "
<> ignore
skeleton (Prefer {}) =
ignore
<> " "
Expand Down Expand Up @@ -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
Expand Down
11 changes: 10 additions & 1 deletion src/Dhall/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 "//")
Expand Down Expand Up @@ -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 =
Expand Down
54 changes: 36 additions & 18 deletions src/Dhall/Pretty/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand All @@ -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 _ _) =
enclose' "" " " (" " <> operator "!=" <> " ") (operator "!=" <> " ") (fmap duplicate (docs a0))
prettyExprC9 a0@(BoolEQ _ _) =
enclose' "" " " (" " <> operator "==" <> " ") (operator "==" <> " ") (fmap duplicate (docs a0))
where
docs (BoolNE a b) = prettyExprD a : docs b
docs (BoolEQ a b) = prettyExprC10 a : docs b
docs (Note _ b) = docs b
docs b = [ prettyExprD 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 ]
prettyExprC10 (Note _ a) =
prettyExprC10 a
prettyExprC10 a0 =
prettyExprD a0

prettyExprD :: Pretty a => Expr s a -> Doc Ann
Expand Down Expand Up @@ -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
Expand Down
15 changes: 15 additions & 0 deletions src/Dhall/Tutorial.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
--
Expand Down
Loading

0 comments on commit 9cb89df

Please sign in to comment.