dhall/format: Keep track of CharacterSet for Equivalent (#2176)

Author: basile-henry

dhall-json/src/Dhall/JSON.hs

@@ -1040,8 +1040,8 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
           where
             a' = loop a
 
-        Core.Equivalent a b ->
-            Core.Equivalent a' b'
+        Core.Equivalent cs a b ->
+            Core.Equivalent cs a' b'
           where
             a' = loop a
             b' = loop b

dhall-nix/src/Dhall/Nix.hs

@@ -642,7 +642,7 @@ dhallToNix e =
         Left CannotProjectByType
     loop (Assert _) =
         return untranslatable
-    loop (Equivalent _ _) =
+    loop (Equivalent _ _ _) =
         return untranslatable
     loop a@With{} =
         loop (Dhall.Core.desugarWith a)

dhall/src/Dhall/Binary.hs

@@ -319,7 +319,7 @@ decodeExpressionInternal decodeEmbed = go
                                     9  -> return (Prefer mempty PreferFromSource)
                                     10 -> return (CombineTypes mempty)
                                     11 -> return ImportAlt
-                                    12 -> return Equivalent
+                                    12 -> return (Equivalent mempty)
                                     13 -> return RecordCompletion
                                     _  -> die ("Unrecognized operator code: " <> show opcode)
 
@@ -792,7 +792,7 @@ encodeExpressionInternal encodeEmbed = go
         ImportAlt l r ->
             encodeOperator 11 l r
 
-        Equivalent l r ->
+        Equivalent _ l r ->
             encodeOperator 12 l r
 
         RecordCompletion l r ->

dhall/src/Dhall/Diff.hs

@@ -992,7 +992,7 @@ diffEquivalentExpression
 diffEquivalentExpression l@(Equivalent {}) r@(Equivalent {}) =
     enclosed' "  " (operator "≡" <> " ") (docs l r)
   where
-    docs (Equivalent aL bL) (Equivalent aR bR) =
+    docs (Equivalent _ aL bL) (Equivalent _ aR bR) =
         Data.List.NonEmpty.cons (diffApplicationExpression aL aR) (docs bL bR)
     docs aL aR =
         pure (diffApplicationExpression aL aR)

dhall/src/Dhall/Eval.hs

@@ -787,7 +787,7 @@ eval !env t0 =
                     VProject (eval env t) (Right e')
         Assert t ->
             VAssert (eval env t)
-        Equivalent t u ->
+        Equivalent _ t u ->
             VEquivalent (eval env t) (eval env u)
         With e₀ ks v ->
             vWith (eval env e₀) ks (eval env v)
@@ -1188,7 +1188,7 @@ quote !env !t0 =
         VAssert t ->
             Assert (quote env t)
         VEquivalent t u ->
-            Equivalent (quote env t) (quote env u)
+            Equivalent mempty (quote env t) (quote env u)
         VWith e ks v ->
             With (quote env e) ks (quote env v)
         VInject m k Nothing ->
@@ -1374,8 +1374,8 @@ alphaNormalize = goEnv EmptyNames
                 Project (go t) (fmap go ks)
             Assert t ->
                 Assert (go t)
-            Equivalent t u ->
-                Equivalent (go t) (go u)
+            Equivalent cs t u ->
+                Equivalent cs (go t) (go u)
             With e k v ->
                 With (go e) k (go v)
             Note s e ->

dhall/src/Dhall/Normalize.hs

@@ -668,11 +668,11 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
         t' <- loop t
 
         pure (Assert t')
-    Equivalent l r -> do
+    Equivalent cs l r -> do
         l' <- loop l
         r' <- loop r
 
-        pure (Equivalent l' r')
+        pure (Equivalent cs l' r')
     With e ks v -> do
         e' <- loop e
         v' <- loop v
@@ -917,7 +917,7 @@ isNormalized e0 = loop (Syntax.denote e0)
                   Record _ -> False
                   _ -> loop e'
       Assert t -> loop t
-      Equivalent l r -> loop l && loop r
+      Equivalent _ l r -> loop l && loop r
       With{} -> False
       Note _ e' -> loop e'
       ImportAlt _ _ -> False

dhall/src/Dhall/Parser/Expression.hs

@@ -350,7 +350,7 @@ parsers embedded = Parsers {..}
 
     operatorParsers :: [Parser (Expr s a -> Expr s a -> Expr s a)]
     operatorParsers =
-        [ Equivalent                  <$ _equivalent    <* whitespace
+        [ Equivalent . Just           <$> _equivalent   <* whitespace
         , ImportAlt                   <$ _importAlt     <* nonemptyWhitespace
         , BoolOr                      <$ _or            <* whitespace
         , NaturalPlus                 <$ _plus          <* nonemptyWhitespace
@@ -359,7 +359,7 @@ parsers embedded = Parsers {..}
         , BoolAnd                     <$ _and           <* whitespace
         , (\cs -> Combine (Just cs) Nothing)         <$> _combine <* whitespace
         , (\cs -> Prefer (Just cs) PreferFromSource) <$> _prefer  <* whitespace
-        , (CombineTypes . Just)       <$> _combineTypes <* whitespace
+        , CombineTypes . Just         <$> _combineTypes <* whitespace
         , NaturalTimes                <$ _times         <* whitespace
         -- Make sure that `==` is not actually the prefix of `===`
         , BoolEQ                      <$ try (_doubleEqual <* Text.Megaparsec.notFollowedBy (char '=')) <* whitespace

dhall/src/Dhall/Parser/Token.hs

@@ -1207,8 +1207,10 @@ _at :: Parser ()
 _at = reservedChar '@' <?> "\"@\""
 
 -- | Parse the equivalence symbol (@===@ or @≡@)
-_equivalent :: Parser ()
-_equivalent = (void (char '≡' <?> "\"≡\"") <|> void (text "===")) <?> "operator"
+_equivalent :: Parser CharacterSet
+_equivalent =
+        (Unicode <$ char '≡' <?> "\"≡\"")
+    <|> (ASCII <$ text "===" <?> "===")
 
 -- | Parse the @missing@ keyword
 _missing :: Parser ()

dhall/src/Dhall/Pretty/Internal.hs

@@ -153,6 +153,7 @@ detectCharacterSet = foldOf (cosmosOf subExpressions . to exprToCharacterSet)
         Combine (Just Unicode) _ _ _ -> Unicode
         CombineTypes (Just Unicode) _ _ -> Unicode
         Prefer (Just Unicode) _ _ _ -> Unicode
+        Equivalent (Just Unicode) _ _ -> Unicode
         _ -> mempty
 
 -- | Pretty print an expression
@@ -927,10 +928,10 @@ prettyPrinters characterSet =
         spacer = if Text.length op == 1 then " "  else "  "
 
     prettyEquivalentExpression :: Pretty a => Expr Src a -> Doc Ann
-    prettyEquivalentExpression a0@(Equivalent _ _) =
+    prettyEquivalentExpression a0@(Equivalent _ _ _) =
         prettyOperator (equivalent characterSet) (docs a0)
       where
-        docs (Equivalent a b) = prettyImportAltExpression b : docs a
+        docs (Equivalent _ a b) = prettyImportAltExpression b : docs a
         docs a
             | Just doc <- preserveSource a =
                 [ doc ]

dhall/src/Dhall/Syntax.hs

@@ -440,10 +440,10 @@ data Expr s a
     -- | > Var (V x 0)                              ~  x
     --   > Var (V x n)                              ~  x@n
     | Var Var
-    -- | > Lam (FunctionBinding _ "x" _ _ A) b      ~  λ(x : A) -> b
+    -- | > Lam _ (FunctionBinding _ "x" _ _ A) b    ~  λ(x : A) -> b
     | Lam (Maybe CharacterSet) (FunctionBinding s a) (Expr s a)
-    -- | > Pi "_" A B                               ~        A  -> B
-    --   > Pi x   A B                               ~  ∀(x : A) -> B
+    -- | > Pi _ "_" A B                               ~        A  -> B
+    --   > Pi _ x   A B                               ~  ∀(x : A) -> B
     | Pi  (Maybe CharacterSet) Text (Expr s a) (Expr s a)
     -- | > App f a                                  ~  f a
     | App (Expr s a) (Expr s a)
@@ -581,7 +581,7 @@ data Expr s a
     | RecordLit (Map Text (RecordField s a))
     -- | > Union        [(k1, Just t1), (k2, Nothing)] ~  < k1 : t1 | k2 >
     | Union     (Map Text (Maybe (Expr s a)))
-    -- | > Combine Nothing x y                      ~  x ∧ y
+    -- | > Combine _ Nothing x y                    ~  x ∧ y
     --
     -- The first field is a `Just` when the `Combine` operator is introduced
     -- as a result of desugaring duplicate record fields:
@@ -592,9 +592,9 @@ data Expr s a
     --   >              (Combine (Just k) x y)
     --   >            )]
     | Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a)
-    -- | > CombineTypes x y                         ~  x ⩓ y
+    -- | > CombineTypes _ x y                       ~  x ⩓ y
     | CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a)
-    -- | > Prefer False x y                         ~  x ⫽ y
+    -- | > Prefer _ False x y                       ~  x ⫽ y
     --
     -- The first field is a `True` when the `Prefer` operator is introduced as a
     -- result of desugaring a @with@ expression
@@ -614,8 +614,8 @@ data Expr s a
     | Project (Expr s a) (Either [Text] (Expr s a))
     -- | > Assert e                                 ~  assert : e
     | Assert (Expr s a)
-    -- | > Equivalent x y                           ~  x ≡ y
-    | Equivalent (Expr s a) (Expr s a)
+    -- | > Equivalent _ x y                           ~  x ≡ y
+    | Equivalent (Maybe CharacterSet) (Expr s a) (Expr s a)
     -- | > With x y e                               ~  x with y = e
     | With (Expr s a) (NonEmpty Text) (Expr s a)
     -- | > Note s x                                 ~  e
@@ -842,7 +842,7 @@ 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 (Project a b) = Project <$> f a <*> traverse f b
 unsafeSubExpressions f (Assert a) = Assert <$> f a
-unsafeSubExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b
+unsafeSubExpressions f (Equivalent cs a b) = Equivalent cs <$> f a <*> f b
 unsafeSubExpressions f (With a b c) = With <$> f a <*> pure b <*> f c
 unsafeSubExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r
 unsafeSubExpressions _ (Let {}) = unhandledConstructor "Let"
@@ -1138,6 +1138,7 @@ denote = \case
     Lam _ a b -> Lam Nothing (denoteFunctionBinding a) (denote b)
     Pi _ t a b -> Pi Nothing t (denote a) (denote b)
     Field a (FieldSelection _ b _) -> Field (denote a) (FieldSelection Nothing b Nothing)
+    Equivalent _ a b -> Equivalent Nothing (denote a) (denote b)
     expression -> Lens.over unsafeSubExpressions denote expression
   where
     denoteRecordField (RecordField _ e _ _) = RecordField Nothing (denote e) Nothing Nothing

dhall/src/Dhall/TypeCheck.hs

@@ -1225,7 +1225,7 @@ infer typer = loop
                 _ ->
                     die (NotAnEquivalence _T)
 
-        Equivalent x y -> do
+        Equivalent _ x y -> do
             _A₀' <- loop ctx x
 
             let _A₀'' = quote names _A₀'