Add showConstructor keyword (#2384)

Gabriella439 · darichey · web-flow · commit a13c6564d3d0 · 2022-02-15T21:53:14.000-08:00
… as standardized in dhall-lang/dhall-lang#1257 Co-authored-by: David Richey <darichey1@gmail.com>
diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs
@@ -340,6 +340,7 @@ dhallToStatement expr0 var0 = go (Dhall.Core.normalize expr0)
     go e@(RecordCompletion {}) = Left (UnsupportedStatement e)
     go e@(Merge            {}) = Left (UnsupportedStatement e)
     go e@(ToMap            {}) = Left (UnsupportedStatement e)
+    go e@(ShowConstructor  {}) = Left (UnsupportedStatement e)
     go e@(Field            {}) = Left (UnsupportedStatement e)
     go e@(Project          {}) = Left (UnsupportedStatement e)
     go e@(Assert           {}) = Left (UnsupportedStatement e)
diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs
@@ -1045,6 +1045,11 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
             a' =      loop a
             b' = fmap loop b
 
+        Core.ShowConstructor a ->
+            Core.ShowConstructor a'
+          where
+            a' = loop a
+
         Core.Field a b ->
             Core.Field a' b
           where
diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs
@@ -142,6 +142,8 @@ data CompileError
     -- ^ Nix does not provide a way to reference a shadowed variable
     | CannotProjectByType
     -- ^ We currently do not support threading around type information
+    | CannotShowConstructor
+    -- ^ We currently do not support the `showConstructor` keyword
     deriving (Typeable)
 
 instance Show CompileError where
@@ -205,6 +207,16 @@ The ❰dhall-to-nix❱ compiler does not support projecting out a subset of a re
 by the expected type (i.e. ❰someRecord.(someType)❱ 
     |]
 
+    show CannotShowConstructor =
+        Data.Text.unpack [NeatInterpolation.text|
+$_ERROR: Cannot translate the ❰showConstructor❱ keyword
+
+The ❰dhall-to-nix❱ compiler does not support the ❰showConstructor❱ keyword.
+
+In theory this keyword shouldn't need to be translated anyway since the keyword
+doesn't survive β-normalization, so if you see this error message there might be
+an internal error in ❰dhall-to-nix❱ that you should report.
+    |]
 
 _ERROR :: Data.Text.Text
 _ERROR = "\ESC[1;31mError\ESC[0m"
@@ -614,6 +626,8 @@ dhallToNix e =
         let map_ = Fix (NBinary NApp "map" (Fix (NAbs "k" (Fix (NSet NNonRecursive setBindings)))))
         let toMap = Fix (NAbs "kvs" (Fix (NBinary NApp map_ ks)))
         return (Fix (NBinary NApp toMap a'))
+    loop (ShowConstructor _) = do
+        Left CannotShowConstructor
     loop (Prefer _ _ b c) = do
         b' <- loop b
         c' <- loop c
diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs
@@ -638,6 +638,9 @@ decodeExpressionInternal decodeEmbed = go
                                 let minutes = sign (_HH * 60 + _MM)
 
                                 return (TimeZoneLiteral (Time.TimeZone minutes False ""))
+                            34 -> do
+                                t <- go
+                                return (ShowConstructor t)
                             _ ->
                                 die ("Unexpected tag: " <> show tag)
 
@@ -1060,6 +1063,11 @@ encodeExpressionInternal encodeEmbed = go
 
             (_HH, _MM) = abs minutes `divMod` 60
 
+        ShowConstructor t ->
+            encodeList2
+                (Encoding.encodeInt 34)
+                (go t)
+
         Note _ b ->
             go b
 
diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs
@@ -636,6 +636,10 @@ skeleton (ToMap {}) =
         keyword "toMap"
     <>  " "
     <>  ignore
+skeleton (ShowConstructor {}) =
+        keyword "showConstructor"
+    <>  " "
+    <>  ignore
 skeleton (Field {}) =
         ignore
     <>  dot
@@ -783,6 +787,15 @@ diffAnnotatedExpression l@(ToMap {}) r =
     mismatch l r
 diffAnnotatedExpression l r@(ToMap {}) =
     mismatch l r
+diffAnnotatedExpression (ShowConstructor aL) (ShowConstructor aR) = align doc
+  where
+    doc =   keyword "showConstructor"
+        <>  " "
+        <>  format " " (diffWithExpression aL aR)
+diffAnnotatedExpression l@(ShowConstructor {}) r =
+    mismatch l r
+diffAnnotatedExpression l r@(ShowConstructor {}) =
+    mismatch l r
 diffAnnotatedExpression (ListLit aL@(Just _) bL) (ListLit aR bR) = align doc
   where
     doc =   format " " (diffList bL bR)
diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs
@@ -228,6 +228,7 @@ data Val a
     | VPrefer !(Val a) !(Val a)
     | VMerge !(Val a) !(Val a) !(Maybe (Val a))
     | VToMap !(Val a) !(Maybe (Val a))
+    | VShowConstructor !(Val a)
     | VField !(Val a) !Text
     | VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
     | VProject !(Val a) !(Either (Set Text) (Val a))
@@ -807,6 +808,14 @@ eval !env t0 =
                     in  VListLit Nothing s
                 (x', ma') ->
                     VToMap x' ma'
+        ShowConstructor x ->
+            case eval env x of
+                VInject m k _
+                    | Just _ <- Map.lookup k m -> VTextLit (VChunks [] k)
+                    | otherwise                -> error errorMsg
+                VSome _ -> VTextLit (VChunks [] "Some")
+                VNone _ -> VTextLit (VChunks [] "None")
+                x' -> VShowConstructor x'
         Field t (Syntax.fieldSelectionLabel -> k) ->
             vField (eval env t) k
         Project t (Left ks) ->
@@ -1033,6 +1042,8 @@ conv !env t0 t0' =
             conv env t t' && conv env u u'
         (VToMap t _, VToMap t' _) ->
             conv env t t'
+        (VShowConstructor t, VShowConstructor t') ->
+            conv env t t'
         (VField t k, VField t' k') ->
             conv env t t' && k == k'
         (VProject t (Left ks), VProject t' (Left ks')) ->
@@ -1243,6 +1254,8 @@ quote !env !t0 =
             Merge (quote env t) (quote env u) (fmap (quote env) ma)
         VToMap t ma ->
             ToMap (quote env t) (fmap (quote env) ma)
+        VShowConstructor t ->
+            ShowConstructor (quote env t)
         VField t k ->
             Field (quote env t) $ Syntax.makeFieldSelection k
         VProject t p ->
@@ -1442,6 +1455,8 @@ alphaNormalize = goEnv EmptyNames
                 Merge (go x) (go y) (fmap go ma)
             ToMap x ma ->
                 ToMap (go x) (fmap go ma)
+            ShowConstructor x ->
+                ShowConstructor (go x)
             Field t k ->
                 Field (go t) k
             Project t ks ->
diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs
@@ -623,6 +623,18 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                 return (ListLit listType keyValues)
             _ ->
                 return (ToMap x' t')
+    ShowConstructor x -> do
+        x' <- loop x
+        return $ case x' of
+            Field (Union ktsY) (Syntax.fieldSelectionLabel -> kY) ->
+                case Dhall.Map.lookup kY ktsY of
+                    Just _ -> TextLit (Chunks [] kY)
+                    _ -> ShowConstructor x'
+            Some _ ->
+                TextLit (Chunks [] "Some")
+            App None _ ->
+                TextLit (Chunks [] "None")
+            _ -> ShowConstructor x'
     Field r k@FieldSelection{fieldSelectionLabel = x}        -> do
         let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)
 
@@ -909,6 +921,11 @@ isNormalized e0 = loop (Syntax.denote e0)
       ToMap x t -> case x of
           RecordLit _ -> False
           _ -> loop x && all loop t
+      ShowConstructor x -> loop x && case x of
+          Field (Union _) _ -> False
+          Some _ -> False
+          App None _ -> False
+          _ -> True
       Field r (FieldSelection Nothing k Nothing) -> case r of
           RecordLit _ -> False
           Project _ _ -> False
diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs
@@ -520,10 +520,15 @@ parsers embedded = Parsers{..}
 
                     return (\a -> ToMap a Nothing, Just "argument to ❰toMap❱")
 
-            let alternative3 =
+            let alternative3 = do
+                    try (_showConstructor *> nonemptyWhitespace)
+
+                    return (\a -> ShowConstructor a, Just "argument to ❰showConstructor❱")
+
+            let alternative4 =
                     return (id, Nothing)
 
-            (f, maybeMessage) <- alternative0 <|> alternative1 <|> alternative2 <|> alternative3
+            (f, maybeMessage) <- alternative0 <|> alternative1 <|> alternative2 <|> alternative3 <|> alternative4
 
             let adapt parser =
                     case maybeMessage of
diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs
@@ -47,6 +47,7 @@ module Dhall.Parser.Token (
     _using,
     _merge,
     _toMap,
+    _showConstructor,
     _assert,
     _Some,
     _None,
@@ -952,6 +953,13 @@ _merge = keyword "merge"
 _toMap :: Parser ()
 _toMap = keyword "toMap"
 
+{-| Parse the @showConstructor@ keyword
+
+    This corresponds to the @showConstructor@ rule from the official grammar
+-}
+_showConstructor :: Parser ()
+_showConstructor = keyword "showConstructor"
+
 {-| Parse the @assert@ keyword
 
     This corresponds to the @assert@ rule from the official grammar
diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs
@@ -1199,6 +1199,7 @@ prettyPrinters characterSet =
             Some a            -> app (builtin "Some") (a : args)
             Merge a b Nothing -> app (keyword "merge") (a : b : args)
             ToMap a Nothing   -> app (keyword "toMap") (a : args)
+            ShowConstructor a -> app (keyword "showConstructor") (a : args)
             e | Note _ b <- e ->
                   go args b
               | null args ->
@@ -1480,7 +1481,19 @@ prettyPrinters characterSet =
                                 <>  keyword "toMap"
                                 <>  case shallowDenote val' of
                                         RecordCompletion _T r ->
-                                            completion _T r
+                                                " "
+                                            <>  completion _T r
+                                        _ ->    Pretty.hardline
+                                            <>  "    "
+                                            <>  prettyImportExpression_ val'
+
+                            ShowConstructor val' ->
+                                    " "
+                                <>  keyword "showConstructor"
+                                <>  case shallowDenote val' of
+                                        RecordCompletion _T r ->
+                                                " "
+                                            <>  completion _T r
                                         _ ->    Pretty.hardline
                                             <>  "    "
                                             <>  prettyImportExpression_ val'
diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs
@@ -632,6 +632,8 @@ data Expr s a
     -- | > ToMap x (Just t)                         ~  toMap x : t
     --   > ToMap x  Nothing                         ~  toMap x
     | ToMap (Expr s a) (Maybe (Expr s a))
+    -- | > ShowConstructor x                        ~  showConstructor x
+    | ShowConstructor (Expr s a)
     -- | > Field e (FieldSelection _ x _)              ~  e.x
     | Field (Expr s a) (FieldSelection s)
     -- | > Project e (Left xs)                      ~  e.{ xs }
@@ -879,6 +881,7 @@ unsafeSubExpressions f (Prefer cs a b c) = Prefer cs <$> a' <*> f b <*> f c
 unsafeSubExpressions f (RecordCompletion a b) = RecordCompletion <$> f a <*> f b
 unsafeSubExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t
 unsafeSubExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t
+unsafeSubExpressions f (ShowConstructor a) = ShowConstructor <$> f a
 unsafeSubExpressions f (Project a b) = Project <$> f a <*> traverse f b
 unsafeSubExpressions f (Assert a) = Assert <$> f a
 unsafeSubExpressions f (Equivalent cs a b) = Equivalent cs <$> f a <*> f b
diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs
@@ -1130,6 +1130,14 @@ infer typer = loop
 
                        die (MapTypeMismatch (quote names (mapType _T')) _T₁'')
 
+        ShowConstructor e -> do
+            _E' <- loop ctx e
+            case _E' of
+              VUnion _ -> pure VText
+              VOptional _ -> pure VText
+
+              _ -> die ShowConstructorNotOnUnion
+
         Field e (Syntax.fieldSelectionLabel -> x) -> do
             _E' <- loop ctx e
 
@@ -1396,6 +1404,7 @@ data TypeMessage s a
     | CantListAppend (Expr s a) (Expr s a)
     | CantAdd (Expr s a) (Expr s a)
     | CantMultiply (Expr s a) (Expr s a)
+    | ShowConstructorNotOnUnion
     deriving (Show)
 
 formatHints :: [Doc Ann] -> Doc Ann
@@ -4550,6 +4559,12 @@ prettyTypeMessage (CantAdd expr0 expr1) =
 prettyTypeMessage (CantMultiply expr0 expr1) =
         buildNaturalOperator "*" expr0 expr1
 
+prettyTypeMessage ShowConstructorNotOnUnion = ErrorMessages {..}
+  where
+      short = "ShowConstructorNotOnUnion"
+      hints = []
+      long = ""
+
 buildBooleanOperator :: Pretty a => Text -> Expr s a -> Expr s a -> ErrorMessages
 buildBooleanOperator operator expr0 expr1 = ErrorMessages {..}
   where
@@ -4831,6 +4846,8 @@ messageExpressions f m = case m of
         CantAdd <$> f a <*> f b
     CantMultiply a b ->
         CantMultiply <$> f a <*> f b
+    ShowConstructorNotOnUnion ->
+        pure ShowConstructorNotOnUnion
 
 {-| Newtype used to wrap error messages so that they render with a more
     detailed explanation of what went wrong
diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs
@@ -1,3 +1,5 @@
+-- TODO: update because we added ShowConstructor constructor to Expr in Dhall.Syntax
+
 {-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleInstances   #-}
@@ -405,6 +407,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where
             % (7 :: W "RecordCompletion")
             % (1 :: W "Merge")
             % (1 :: W "ToMap")
+            % (1 :: W "ShowConstructor")
             % (7 :: W "Field")
             % (7 :: W "Project")
             % (1 :: W "Assert")
