Implement new simplifications for boolean logic (#316)

... as standardized in dhall-lang/dhall-lang#109

Author: Gabriella439

dhall.cabal

@@ -139,6 +139,7 @@ Extra-Source-Files:
     tests/normalization/examples/Text/concatMap/*.dhall
     tests/normalization/examples/Text/concatMapSep/*.dhall
     tests/normalization/examples/Text/concatSep/*.dhall
+    tests/normalization/simplifications/*.dhall
     tests/parser/*.dhall
     tests/regression/*.dhall
     tests/tutorial/*.dhall

src/Dhall/Core.hs

@@ -32,6 +32,7 @@ module Dhall.Core (
     , normalize
     , normalizeWith
     , Normalizer
+    , judgmentallyEqual
     , subst
     , shift
     , isNormalized
@@ -1107,7 +1108,7 @@ alphaNormalize (Embed a) =
     However, `normalize` will not fail if the expression is ill-typed and will
     leave ill-typed sub-expressions unevaluated.
 -}
-normalize ::  Expr s a -> Expr t a
+normalize :: Eq a => Expr s a -> Expr t a
 normalize = normalizeWith (const Nothing)
 
 {-| This function is used to determine whether folds like @Natural/fold@ or
@@ -1209,7 +1210,7 @@ denote (Embed a             ) = Embed a
     with those functions is not total either.
 
 -}
-normalizeWith :: Normalizer a -> Expr s a -> Expr t a
+normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a
 normalizeWith ctx e0 = loop (denote e0)
  where
  loop e =  case e of
@@ -1356,32 +1357,40 @@ normalizeWith ctx e0 = loop (denote e0)
         decide (BoolLit False)  _              = BoolLit False
         decide  l              (BoolLit True ) = l
         decide  _              (BoolLit False) = BoolLit False
-        decide  l               r              = BoolAnd l r
+        decide  l               r
+            | judgmentallyEqual l r = l
+            | otherwise             = BoolAnd l r
     BoolOr x y -> decide (loop x) (loop y)
       where
         decide (BoolLit False)  r              = r
         decide (BoolLit True )  _              = BoolLit True
         decide  l              (BoolLit False) = l
         decide  _              (BoolLit True ) = BoolLit True
-        decide  l               r              = BoolOr l r
+        decide  l               r
+            | judgmentallyEqual l r = l
+            | otherwise             = BoolOr l r
     BoolEQ x y -> decide (loop x) (loop y)
       where
         decide (BoolLit True )  r              = r
         decide  l              (BoolLit True ) = l
-        decide (BoolLit False) (BoolLit False) = BoolLit True
-        decide  l               r              = BoolEQ l r
+        decide  l               r
+            | judgmentallyEqual l r = BoolLit True
+            | otherwise             = BoolEQ l r
     BoolNE x y -> decide (loop x) (loop y)
       where
         decide (BoolLit False)  r              = r
         decide  l              (BoolLit False) = l
-        decide (BoolLit True ) (BoolLit True ) = BoolLit False
-        decide  l               r              = BoolNE l r
+        decide  l               r
+            | judgmentallyEqual l r = BoolLit False
+            | otherwise             = BoolNE l r
     BoolIf bool true false -> decide (loop bool) (loop true) (loop false)
       where
         decide (BoolLit True )  l              _              = l
         decide (BoolLit False)  _              r              = r
         decide  b              (BoolLit True) (BoolLit False) = b
-        decide  b               l              r              = BoolIf b l r
+        decide  b               l              r
+            | judgmentallyEqual l r = l
+            | otherwise             = BoolIf b l r
     Natural -> Natural
     NaturalLit n -> NaturalLit n
     NaturalFold -> NaturalFold
@@ -1525,6 +1534,15 @@ normalizeWith ctx e0 = loop (denote e0)
     Note _ e' -> loop e'
     Embed a -> Embed a
 
+{-| Returns `True` if two expressions are α-equivalent and β-equivalent and
+    `False` otherwise
+-}
+judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
+judgmentallyEqual eL0 eR0 = alphaBetaNormalize eL0 == alphaBetaNormalize eR0
+  where
+    alphaBetaNormalize :: Eq a => Expr s a -> Expr () a
+    alphaBetaNormalize = alphaNormalize . normalize
+
 -- | Use this to wrap you embedded functions (see `normalizeWith`) to make them
 --   polymorphic enough to be used.
 type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)

src/Dhall/TypeCheck.hs

@@ -58,14 +58,6 @@ rule Type Type = return Type
 rule Kind Kind = return Kind
 rule Kind Type = return Type
 
-judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
-judgmentallyEqual eL0 eR0 = alphaBetaNormalize eL0 == alphaBetaNormalize eR0
-  where
-    alphaBetaNormalize :: Expr s a -> Expr X a
-    alphaBetaNormalize =
-            Dhall.Core.alphaNormalize
-        .   Dhall.Core.normalize
-
 {-| Type-check an expression and return the expression's type if type-checking
     succeeds or an error if type-checking fails
 
@@ -131,7 +123,7 @@ typeWithA tpa = loop
             Pi x _A _B -> return (x, _A, _B)
             _          -> Left (TypeError ctx e (NotAFunction f tf))
         _A' <- loop ctx a
-        if judgmentallyEqual _A _A'
+        if Dhall.Core.judgmentallyEqual _A _A'
             then do
                 let a'   = Dhall.Core.shift   1  (V x 0) a
                 let _B'  = Dhall.Core.subst (V x 0) a' _B
@@ -148,7 +140,7 @@ typeWithA tpa = loop
                 _ <- loop ctx _A0
                 let nf_A0 = Dhall.Core.normalize _A0
                 let nf_A1 = Dhall.Core.normalize _A1
-                if judgmentallyEqual _A0 _A1
+                if Dhall.Core.judgmentallyEqual _A0 _A1
                     then return ()
                     else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1))
             Nothing -> return ()
@@ -161,7 +153,7 @@ typeWithA tpa = loop
         _ <- loop ctx t
 
         t' <- loop ctx x
-        if judgmentallyEqual t t'
+        if Dhall.Core.judgmentallyEqual t t'
             then do
                 return t
             else do
@@ -237,7 +229,7 @@ typeWithA tpa = loop
             Const Type -> return ()
             _          -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz))
 
-        if judgmentallyEqual ty tz
+        if Dhall.Core.judgmentallyEqual ty tz
             then return ()
             else Left (TypeError ctx e (IfBranchMismatch y z ty tz))
         return ty
@@ -335,7 +327,7 @@ typeWithA tpa = loop
                     _ -> Left (TypeError ctx e (InvalidListType t))
                 flip traverseWithIndex_ xs (\i x -> do
                     t' <- loop ctx x
-                    if judgmentallyEqual t t'
+                    if Dhall.Core.judgmentallyEqual t t'
                         then return ()
                         else do
                             let nf_t  = Dhall.Core.normalize t
@@ -351,7 +343,7 @@ typeWithA tpa = loop
             _ -> Left (TypeError ctx e (InvalidListType t))
         flip traverseWithIndex_ xs (\i x -> do
             t' <- loop ctx x
-            if judgmentallyEqual t t'
+            if Dhall.Core.judgmentallyEqual t t'
                 then return ()
                 else do
                     let nf_t  = Dhall.Core.normalize t
@@ -369,7 +361,7 @@ typeWithA tpa = loop
             App List er -> return er
             _           -> Left (TypeError ctx e (CantListAppend r tr))
 
-        if judgmentallyEqual el er
+        if Dhall.Core.judgmentallyEqual el er
             then return (App List el)
             else Left (TypeError ctx e (ListAppendMismatch el er))
     loop _      ListBuild         = do
@@ -410,7 +402,7 @@ typeWithA tpa = loop
             _ -> Left (TypeError ctx e (InvalidOptionalType t))
         forM_ xs (\x -> do
             t' <- loop ctx x
-            if judgmentallyEqual t t'
+            if Dhall.Core.judgmentallyEqual t t'
                 then return ()
                 else do
                     let nf_t  = Dhall.Core.normalize t
@@ -538,10 +530,10 @@ typeWithA tpa = loop
                     Just tX  ->
                         case tX of
                             Pi _ tY' t' -> do
-                                if judgmentallyEqual tY tY'
+                                if Dhall.Core.judgmentallyEqual tY tY'
                                     then return ()
                                     else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
-                                if judgmentallyEqual t t'
+                                if Dhall.Core.judgmentallyEqual t t'
                                     then return ()
                                     else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'))
                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
@@ -577,10 +569,10 @@ typeWithA tpa = loop
                     Just tX  ->
                         case tX of
                             Pi _ tY' t' -> do
-                                if judgmentallyEqual tY tY'
+                                if Dhall.Core.judgmentallyEqual tY tY'
                                     then return ()
                                     else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
-                                if judgmentallyEqual t t'
+                                if Dhall.Core.judgmentallyEqual t t'
                                     then return ()
                                     else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'))
                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))

tests/Normalization.hs

@@ -25,6 +25,7 @@ normalizationTests :: TestTree
 normalizationTests =
     testGroup "normalization"
         [ examples
+        , simplifications
         , constantFolding
         , conversions
         , shouldNormalize "Optional build/fold fusion" "optionalBuildFold"
@@ -154,6 +155,16 @@ examples =
         , shouldNormalize "Text/concatSep" "./examples/Text/concatSep/1"
         ]
 
+simplifications :: TestTree
+simplifications =
+    testGroup "Simplifications"
+        [ shouldNormalize "if/then/else" "./simplifications/ifThenElse"
+        , shouldNormalize "||" "./simplifications/or"
+        , shouldNormalize "&&" "./simplifications/and"
+        , shouldNormalize "==" "./simplifications/eq"
+        , shouldNormalize "!=" "./simplifications/ne"
+        ]
+
 constantFolding :: TestTree
 constantFolding =
     testGroup "folding of constants"

tests/normalization/simplifications/andA.dhall

@@ -0,0 +1,6 @@
+{ example0 = λ(x : Bool) → x && True
+, example1 = λ(x : Bool) → True && x
+, example2 = λ(x : Bool) → x && False
+, example3 = λ(x : Bool) → False && x
+, example4 = λ(x : Bool) → x && x
+}

tests/normalization/simplifications/andB.dhall

@@ -0,0 +1,6 @@
+{ example0 = λ(x : Bool) → x
+, example1 = λ(x : Bool) → x
+, example2 = λ(x : Bool) → False
+, example3 = λ(x : Bool) → False
+, example4 = λ(x : Bool) → x
+}

tests/normalization/simplifications/eqA.dhall

@@ -0,0 +1,4 @@
+{ example0 = λ(x : Bool) → x == True
+, example1 = λ(x : Bool) → True == x
+, example2 = λ(x : Bool) → x == x
+}

tests/normalization/simplifications/eqB.dhall

@@ -0,0 +1,4 @@
+{ example0 = λ(x : Bool) → x
+, example1 = λ(x : Bool) → x
+, example2 = λ(x : Bool) → True
+}

tests/normalization/simplifications/ifThenElseA.dhall

@@ -0,0 +1,3 @@
+{ example0 = λ(x : Bool) → if x then True else False
+, example1 = λ(x : Bool) → λ(y : Text) → if x then y else y
+}

tests/normalization/simplifications/ifThenElseB.dhall

@@ -0,0 +1,3 @@
+{ example0 = λ(x : Bool) → x
+, example1 = λ(x : Bool) → λ(y : Text) → y
+}