diff --git a/dhall.cabal b/dhall.cabal index 31715aad5..79a392f96 100644 --- a/dhall.cabal +++ b/dhall.cabal @@ -83,6 +83,7 @@ Extra-Source-Files: Prelude/Text/concatSep tests/parser/*.dhall tests/regression/*.dhall + tests/tutorial/*.dhall Source-Repository head Type: git diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs index 01bae709a..7d4b25c79 100644 --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -325,6 +325,8 @@ data Expr s a -- | > Merge x y (Just t ) ~ merge x y : t -- | > Merge x y Nothing ~ merge x y | Merge (Expr s a) (Expr s a) (Maybe (Expr s a)) + -- | > Constructors e ~ constructors e + | Constructors (Expr s a) -- | > Field e x ~ e.x | Field (Expr s a) Text -- | > Note s x ~ e @@ -396,6 +398,7 @@ instance Monad (Expr s) where Combine a b >>= k = Combine (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) Field a b >>= k = Field (a >>= k) b Note a b >>= k = Note a (b >>= k) Embed a >>= k = k a @@ -456,6 +459,7 @@ instance Bifunctor Expr where first k (Combine a b ) = Combine (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) first k (Field a b ) = Field (first k a) b first k (Note a b ) = Note (k a) (first k b) first _ (Embed a ) = Embed a @@ -900,9 +904,10 @@ prettyExprD :: Pretty a => Expr s a -> Doc ann prettyExprD a0@(App _ _) = enclose' "" "" " " "" (fmap duplicate (reverse (docs a0))) where - docs (App a b) = prettyExprE b : docs a - docs (Note _ b) = docs b - docs b = [ prettyExprE b ] + docs (App a b) = prettyExprE b : docs a + docs (Constructors b) = [ prettyExprE b , "constructors" ] + docs (Note _ b) = docs b + docs b = [ prettyExprE b ] prettyExprD (Note _ b) = prettyExprD b prettyExprD a0 = prettyExprE a0 @@ -1239,9 +1244,10 @@ buildExprC9 a = buildExprD a -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser" buildExprD :: Buildable a => Expr s a -> Builder -buildExprD (App a b) = buildExprD a <> " " <> buildExprE b -buildExprD (Note _ b) = buildExprD b -buildExprD a = buildExprE a +buildExprD (App a b) = buildExprD a <> " " <> buildExprE b +buildExprD (Constructors b) = "constructors " <> buildExprE b +buildExprD (Note _ b) = buildExprD b +buildExprD a = buildExprE a -- | Builder corresponding to the @exprE@ parser in "Dhall.Parser" buildExprE :: Buildable a => Expr s a -> Builder @@ -1625,6 +1631,9 @@ shift d v (Merge a b c) = Merge a' b' c' a' = shift d v a b' = shift d v b c' = fmap (shift d v) c +shift d v (Constructors a) = Constructors a' + where + a' = shift d v a shift d v (Field a b) = Field a' b where a' = shift d v a @@ -1760,6 +1769,9 @@ subst x e (Merge a b c) = Merge a' b' c' a' = subst x e a b' = subst x e b c' = fmap (subst x e) c +subst x e (Constructors a) = Constructors a' + where + a' = subst x e a subst x e (Field a b) = Field a' b where a' = subst x e a @@ -2151,6 +2163,18 @@ normalizeWith ctx e0 = loop (shift 0 "_" e0) x' = loop x y' = loop y t' = fmap loop t + Constructors t -> + case t' of + Union kts -> RecordLit kvs + where + kvs = Data.Map.mapWithKey adapt kts + + adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest) + where + rest = Data.Map.delete k kts + _ -> Constructors t' + where + t' = loop t Field r x -> case loop r of RecordLit kvs -> @@ -2361,6 +2385,10 @@ isNormalized e = case shift 0 "_" e of -- `shift` is a hack to delete `Note` Nothing -> True _ -> True _ -> True + Constructors t -> isNormalized t && + case t of + Union _ -> False + _ -> True Field r x -> isNormalized r && case r of RecordLit kvs -> diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs index dfdbf164c..93a53ef27 100644 --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -511,6 +511,9 @@ _using = reserved "using" _merge :: Parser () _merge = reserved "merge" +_constructors :: Parser () +_constructors = reserved "constructors" + _NaturalFold :: Parser () _NaturalFold = reserved "Natural/fold" @@ -1151,8 +1154,10 @@ notEqualExpression = applicationExpression :: Parser a -> Parser (Expr Src a) applicationExpression embedded = do - a <- some (noted (selectorExpression embedded)) - return (foldl1 app a) + f <- (do _constructors; return Constructors) <|> return id + a <- noted (selectorExpression embedded) + b <- many (noted (selectorExpression embedded)) + return (foldl app (f a) b) where app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) = Note (Src before after (bytesL <> bytesR)) (App nL nR) diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs index 9c46d9ef9..0088586a2 100644 --- a/src/Dhall/Tutorial.hs +++ b/src/Dhall/Tutorial.hs @@ -1128,6 +1128,36 @@ import Dhall -- > , Empty -- > ] -- +-- ... and Dhall even provides the @constructors@ keyword to automate this +-- common pattern: +-- +-- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > +-- > in [ MyType.Empty {} +-- > , MyType.Person { name = "John", age = +23 } +-- > , MyType.Person { name = "Amy" , age = +25 } +-- > ] +-- +-- The @constructors@ keyword takes a union type argument and returns a record +-- with one field per union type constructor: +-- +-- > $ dhall --pretty +-- > constructors < Empty : {} | Person : { name : Text, age : Natural } > +-- > +-- > +-- > { Empty : +-- > ∀(Empty : {}) → < Empty : {} | Person : { age : Natural, name : Text } > +-- > , Person : +-- > ∀(Person : { age : Natural, name : Text }) +-- > → < Empty : {} | Person : { age : Natural, name : Text } > +-- > } +-- > +-- > { Empty = +-- > λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } > +-- > , Person = +-- > λ(Person : { age : Natural, name : Text }) +-- > → < Person = Person | Empty : {} > +-- > } +-- -- You can also extract fields during pattern matching such as in the following -- function which renders each value to `Text`: -- diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs index ff2d56dba..3b8578fc9 100644 --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -637,6 +637,16 @@ typeWithA tpa = loop _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) mapM_ process (Data.Map.toList ktsY) return t + loop ctx e@(Constructors t ) = do + _ <- loop ctx t + + kts <- case Dhall.Core.normalize t of + Union kts -> return kts + t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t')) + + let adapt k t_ = Pi k t_ (Union kts) + + return (Record (Data.Map.mapWithKey adapt kts)) loop ctx e@(Field r x ) = do t <- fmap Dhall.Core.normalize (loop ctx r) case t of @@ -711,6 +721,7 @@ data TypeMessage s a | InvalidHandlerOutputType Text (Expr s a) (Expr s a) | MissingMergeType | HandlerNotAFunction Text (Expr s a) + | ConstructorsRequiresAUnionType (Expr s a) (Expr s a) | NotARecord Text (Expr s a) (Expr s a) | MissingField Text (Expr s a) | CantAnd (Expr s a) (Expr s a) @@ -2751,6 +2762,58 @@ prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..} txt0 = build k txt1 = build expr0 +prettyTypeMessage (ConstructorsRequiresAUnionType expr0 expr1) = ErrorMessages {..} + where + short = "❰constructors❱ requires a union type" + + long = + "Explanation: You can only use the ❰constructors❱ keyword on an argument that is \n\ + \a union type literal, like this: \n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────────┐ \n\ + \ │ constructors < Left : Natural, Right : Bool > │ \n\ + \ └───────────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but you cannot use the ❰constructors❱ keyword on any other type of argument.\n\ + \For example, you cannot use a variable argument: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────────────┐ \n\ + \ │ λ(t : Type) → constructors t │ Invalid: ❰t❱ might not be a union type \n\ + \ └──────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌─────────────────────────────────────────────────┐ \n\ + \ │ let t : Type = < Left : Natural, Right : Bool > │ Invalid: Type-checking \n\ + \ │ in constructors t │ precedes normalization \n\ + \ └─────────────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \However, you can import the union type argument: \n\ + \ \n\ + \ \n\ + \ ┌────────────────────────────────┐ \n\ + \ │ constructors ./unionType.dhall │ Valid: Import resolution precedes \n\ + \ └────────────────────────────────┘ type-checking \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 union type literal \n" + where + txt0 = build expr0 + txt1 = build expr1 + prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..} where short = "Not a record" diff --git a/tests/Parser.hs b/tests/Parser.hs index 19318b756..0537833b6 100644 --- a/tests/Parser.hs +++ b/tests/Parser.hs @@ -107,6 +107,9 @@ parserTests = , shouldPass "merge" "./tests/parser/merge.dhall" + , shouldPass + "constructors" + "./tests/parser/constructors.dhall" , shouldPass "fields" "./tests/parser/fields.dhall" diff --git a/tests/Tutorial.hs b/tests/Tutorial.hs index 8806459fc..31e468a0f 100644 --- a/tests/Tutorial.hs +++ b/tests/Tutorial.hs @@ -10,8 +10,11 @@ import qualified Test.Tasty import qualified Test.Tasty.HUnit import qualified Util +import Data.Monoid ((<>)) +import Data.Text (Text) import Dhall (Inject) import GHC.Generics (Generic) +import Numeric.Natural (Natural) import Test.Tasty (TestTree) import Test.Tasty.HUnit ((@?=)) @@ -27,6 +30,13 @@ tutorialTests = , _Functions_1 , _Functions_2 ] + , Test.Tasty.testGroup "Unions" + [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall" + , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall" + , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall" + , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall" + , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall" + ] ] _Interpolation_0 :: TestTree @@ -67,3 +77,9 @@ _Functions_2 = Test.Tasty.HUnit.testCase "Example #2" (do f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" f (Example0 { foo = True, bar = False }) @?= False f (Example0 { foo = True, bar = True }) @?= True ) + +example :: Natural -> Text -> Text -> TestTree +example n text0 text1 = + Test.Tasty.HUnit.testCase + ("Example #" <> show n) + (Util.equivalent text0 text1) diff --git a/tests/Util.hs b/tests/Util.hs index f0fd03c18..58ab07cea 100644 --- a/tests/Util.hs +++ b/tests/Util.hs @@ -3,6 +3,7 @@ module Util ( code , codeWith + , equivalent , normalize' , normalizeWith' , assertNormalizesTo @@ -48,6 +49,12 @@ codeWith ctx strictText = do Right _ -> return () return expr1 +equivalent :: Data.Text.Text -> Data.Text.Text -> IO () +equivalent text0 text1 = do + expr0 <- fmap Dhall.Core.normalize (Util.code text0) :: IO (Expr X X) + expr1 <- fmap Dhall.Core.normalize (Util.code text1) :: IO (Expr X X) + assertEqual "Expressions are not equivalent" expr0 expr1 + assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO () assertNormalizesTo e expected = do assertBool msg (not $ Dhall.Core.isNormalized e) diff --git a/tests/parser/constructors.dhall b/tests/parser/constructors.dhall new file mode 100644 index 000000000..ce7f05c1a --- /dev/null +++ b/tests/parser/constructors.dhall @@ -0,0 +1 @@ +constructors < Left : Natural | Right : Bool > diff --git a/tests/tutorial/process b/tests/tutorial/process new file mode 100644 index 000000000..6a95a805d --- /dev/null +++ b/tests/tutorial/process @@ -0,0 +1,6 @@ + λ(union : < Left : Natural | Right : Bool >) +→ let handlers = + { Left = Natural/even -- Natural/even is a built-in function + , Right = λ(b : Bool) → b + } +in merge handlers union : Bool diff --git a/tests/tutorial/unions0A.dhall b/tests/tutorial/unions0A.dhall new file mode 100644 index 000000000..c95d17902 --- /dev/null +++ b/tests/tutorial/unions0A.dhall @@ -0,0 +1 @@ +./process < Left = +3 | Right : Bool > diff --git a/tests/tutorial/unions0B.dhall b/tests/tutorial/unions0B.dhall new file mode 100644 index 000000000..bc59c12aa --- /dev/null +++ b/tests/tutorial/unions0B.dhall @@ -0,0 +1 @@ +False diff --git a/tests/tutorial/unions1A.dhall b/tests/tutorial/unions1A.dhall new file mode 100644 index 000000000..dd761d442 --- /dev/null +++ b/tests/tutorial/unions1A.dhall @@ -0,0 +1 @@ +./process < Right = True | Left : Natural > diff --git a/tests/tutorial/unions1B.dhall b/tests/tutorial/unions1B.dhall new file mode 100644 index 000000000..0ca95142b --- /dev/null +++ b/tests/tutorial/unions1B.dhall @@ -0,0 +1 @@ +True diff --git a/tests/tutorial/unions2A.dhall b/tests/tutorial/unions2A.dhall new file mode 100644 index 000000000..5057bb0c0 --- /dev/null +++ b/tests/tutorial/unions2A.dhall @@ -0,0 +1,8 @@ + let Empty = < Empty = {=} | Person : { name : Text, age : Natural } > +in let Person = + λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} > +in [ Empty + , Person { name = "John", age = +23 } + , Person { name = "Amy" , age = +25 } + , Empty + ] diff --git a/tests/tutorial/unions2B.dhall b/tests/tutorial/unions2B.dhall new file mode 100644 index 000000000..a72266300 --- /dev/null +++ b/tests/tutorial/unions2B.dhall @@ -0,0 +1,5 @@ +[ < Empty = {=} | Person : { age : Natural, name : Text } > +, < Person = { age = +23, name = "John" } | Empty : {} > +, < Person = { age = +25, name = "Amy" } | Empty : {} > +, < Empty = {=} | Person : { age : Natural, name : Text } > +] diff --git a/tests/tutorial/unions3A.dhall b/tests/tutorial/unions3A.dhall new file mode 100644 index 000000000..a03b9d293 --- /dev/null +++ b/tests/tutorial/unions3A.dhall @@ -0,0 +1,5 @@ + let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } > +in [ MyType.Empty {=} + , MyType.Person { name = "John", age = +23 } + , MyType.Person { name = "Amy" , age = +25 } + ] diff --git a/tests/tutorial/unions3B.dhall b/tests/tutorial/unions3B.dhall new file mode 100644 index 000000000..166867706 --- /dev/null +++ b/tests/tutorial/unions3B.dhall @@ -0,0 +1,4 @@ +[ < Empty = {=} | Person : { age : Natural, name : Text } > +, < Person = { age = +23, name = "John" } | Empty : {} > +, < Person = { age = +25, name = "Amy" } | Empty : {} > +] diff --git a/tests/tutorial/unions4A.dhall b/tests/tutorial/unions4A.dhall new file mode 100644 index 000000000..3cb4cd1bb --- /dev/null +++ b/tests/tutorial/unions4A.dhall @@ -0,0 +1 @@ +constructors < Empty : {} | Person : { name : Text, age : Natural } > diff --git a/tests/tutorial/unions4B.dhall b/tests/tutorial/unions4B.dhall new file mode 100644 index 000000000..b2d06167b --- /dev/null +++ b/tests/tutorial/unions4B.dhall @@ -0,0 +1,6 @@ +{ Empty = + λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } > +, Person = + λ(Person : { age : Natural, name : Text }) + → < Person = Person | Empty : {} > +}