[ cleanup ] Refactor equality functions using maybeEq

CHANGELOG_NEXT.md

@@ -87,3 +87,5 @@ should target this file (`CHANGELOG_NEXT`).
 #### Base
 
 * Added `rtrim` to `Data.String`.
+* Added `decToMaybe`, `maybeCong` and `maybeCong2` to `Data.Maybe`.
+* Added `maybeEq` to `Decidable.Equality`.

idris2api.ipkg

@@ -214,6 +214,8 @@ modules =
     Libraries.Data.WithDefault,
     Libraries.Data.WithData,
 
+    Libraries.Decidable.Equality,
+
     Libraries.System.Directory.Tree,
 
     Libraries.Text.Bounded,

libs/base/Data/Maybe.idr

@@ -51,6 +51,11 @@ toMaybe : Bool -> Lazy a -> Maybe a
 toMaybe True  j = Just j
 toMaybe False _ = Nothing
 
+public export
+decToMaybe : Dec a -> Maybe a
+decToMaybe (Yes a) = Just a
+decToMaybe (No _)  = Nothing
+
 export
 Injective Just where
   injective Refl = Refl
@@ -97,3 +102,17 @@ Zippable Maybe where
 
   unzipWith3 f Nothing  = (Nothing, Nothing, Nothing)
   unzipWith3 f (Just x) = let (a, b, c) = f x in (Just a, Just b, Just c)
+
+--------------------------------------------------------------------------------
+-- Proof helpers
+--------------------------------------------------------------------------------
+
+%inline
+public export
+maybeCong : (f : a -> b) -> Maybe (x = y) -> Maybe (f x = f y)
+maybeCong f = map (\eq => cong f eq)
+
+%inline
+public export
+maybeCong2 : (f : a -> b -> c) -> Maybe (x = y) -> Maybe (v = w) -> Maybe (f x v = f y w)
+maybeCong2 f mxy mvw = (\xy, vw => cong2 f xy vw) <$> mxy <*> mvw

libs/base/Decidable/Equality/Core.idr

@@ -1,6 +1,7 @@
 module Decidable.Equality.Core
 
 import Control.Function
+import Data.Maybe
 
 %default total
 
@@ -14,6 +15,11 @@ interface DecEq t where
   ||| Decide whether two elements of `t` are propositionally equal
   decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
 
+%inline
+public export
+maybeEq : DecEq t => (x1, x2 : t) -> Maybe (x1 = x2)
+maybeEq x1 x2 = decToMaybe (decEq x1 x2)
+
 --------------------------------------------------------------------------------
 -- Utility lemmas
 --------------------------------------------------------------------------------

src/Core/Case/CaseBuilder.idr

@@ -369,16 +369,6 @@ data ConType : Type where
      CDelay : ConType
      CConst : Constant -> ConType
 
-conTypeEq : (x, y : ConType) -> Maybe (x = y)
-conTypeEq (CName x tag) (CName x' tag')
-   = do Refl <- nameEq x x'
-        case decEq tag tag' of
-             Yes Refl => Just Refl
-             No contra => Nothing
-conTypeEq CDelay CDelay = Just Refl
-conTypeEq (CConst x) (CConst y) = (\xy => cong CConst xy) <$> constantEq x y
-conTypeEq _ _ = Nothing
-
 data Group : List Name -> -- pattern variables still to process
              Scoped where
      ConGroup : {newargs : _} ->

src/Core/Name.idr

@@ -2,7 +2,7 @@ module Core.Name
 
 import Data.Maybe
 import Data.String
-import Decidable.Equality
+import Libraries.Decidable.Equality as L
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
 import Libraries.Utils.String
@@ -394,68 +394,29 @@ Ord Name where
 
 export
 userNameEq : (x, y : UserName) -> Maybe (x = y)
-userNameEq (Basic x) (Basic y) with (decEq x y)
-  userNameEq (Basic x) (Basic y) | Yes prf = Just (cong Basic prf)
-  userNameEq (Basic x) (Basic y) | No nprf = Nothing
-userNameEq (Field x) (Field y) with (decEq x y)
-  userNameEq (Field x) (Field y) | Yes prf = Just (cong Field prf)
-  userNameEq (Field x) (Field y) | No nprf = Nothing
+userNameEq (Basic x) (Basic y) = L.maybeCong Basic (L.maybeEq x y)
+userNameEq (Field x) (Field y) = L.maybeCong Field (L.maybeEq x y)
 userNameEq Underscore Underscore = Just Refl
 userNameEq _ _ = Nothing
 
 
 export
 nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
-nameEq (NS xs x) (NS ys y) with (decEq xs ys)
-  nameEq (NS ys x) (NS ys y) | (Yes Refl) with (nameEq x y)
-    nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing
-    nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl
-  nameEq (NS xs x) (NS ys y) | (No contra) = Nothing
-nameEq (UN x) (UN y) = map (\xy => cong UN xy) (userNameEq x y)
-nameEq (MN x t) (MN x' t') with (decEq x x')
-  nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t')
-    nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl
-    nameEq (MN x t) (MN x t') | (Yes Refl) | (No contra) = Nothing
-  nameEq (MN x t) (MN x' t') | (No contra) = Nothing
-nameEq (PV x t) (PV y t') with (nameEq x y)
-  nameEq (PV y t) (PV y t') | (Just Refl) with (decEq t t')
-    nameEq (PV y t) (PV y t) | (Just Refl) | (Yes Refl) = Just Refl
-    nameEq (PV y t) (PV y t') | (Just Refl) | (No p) = Nothing
-  nameEq (PV x t) (PV y t') | Nothing = Nothing
-nameEq (DN x t) (DN y t') with (decEq x y)
-  nameEq (DN y t) (DN y t') | (Yes Refl) with (nameEq t t')
-    nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
-    nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
-  nameEq (DN x t) (DN y t') | (No p) = Nothing
-nameEq (Nested x y) (Nested x' y') with (decEq x x')
-  nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
-  nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')
-    nameEq (Nested x y) (Nested x y') | (Yes Refl) | Nothing = Nothing
-    nameEq (Nested x y) (Nested x y) | (Yes Refl) | (Just Refl) = Just Refl
-nameEq (CaseBlock x y) (CaseBlock x' y') with (decEq x x')
-  nameEq (CaseBlock x y) (CaseBlock x' y') | (No p) = Nothing
-  nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) with (decEq y y')
-    nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) | (No p) = Nothing
-    nameEq (CaseBlock x y) (CaseBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl
-nameEq (WithBlock x y) (WithBlock x' y') with (decEq x x')
-  nameEq (WithBlock x y) (WithBlock x' y') | (No p) = Nothing
-  nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) with (decEq y y')
-    nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) | (No p) = Nothing
-    nameEq (WithBlock x y) (WithBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl
-nameEq (Resolved x) (Resolved y) with (decEq x y)
-  nameEq (Resolved y) (Resolved y) | (Yes Refl) = Just Refl
-  nameEq (Resolved x) (Resolved y) | (No contra) = Nothing
+nameEq (NS xs x) (NS ys y) = L.maybeCong2 NS (L.maybeEq xs ys) (nameEq x y)
+nameEq (UN x) (UN y) = L.maybeCong UN (userNameEq x y)
+nameEq (MN x t) (MN x' t') = L.maybeCong2 MN (L.maybeEq x x') (L.maybeEq t t')
+nameEq (PV x t) (PV y t') = L.maybeCong2 PV (nameEq x y) (L.maybeEq t t')
+nameEq (DN x t) (DN y t') = L.maybeCong2 DN (L.maybeEq x y) (nameEq t t')
+nameEq (Nested x y) (Nested x' y') = L.maybeCong2 Nested (L.maybeEq x x') (nameEq y y')
+nameEq (CaseBlock x y) (CaseBlock x' y') = L.maybeCong2 CaseBlock (L.maybeEq x x') (L.maybeEq y y')
+nameEq (WithBlock x y) (WithBlock x' y') = L.maybeCong2 WithBlock (L.maybeEq x x') (L.maybeEq y y')
+nameEq (Resolved x) (Resolved y) = L.maybeCong Resolved (L.maybeEq x y)
 nameEq _ _ = Nothing
 
 export
 namesEq : (xs, ys : List Name) -> Maybe (xs = ys)
 namesEq [] [] = Just Refl
-namesEq (x :: xs) (y :: ys)
-    = do p <- nameEq x y
-         ps <- namesEq xs ys
-         rewrite p
-         rewrite ps
-         Just Refl
+namesEq (x :: xs) (y :: ys) = L.maybeCong2 (::) (nameEq x y) (namesEq xs ys)
 namesEq _ _ = Nothing
 
 ||| Generate the next machine name

src/Core/Name/Namespace.idr

@@ -199,15 +199,12 @@ export
 Ord ModuleIdent where
     compare (MkMI ms) (MkMI ns) = compare ms ns
 
-mkNSInjective : MkNS ms === MkNS ns -> ms === ns
-mkNSInjective Refl = Refl
+Injective MkNS where
+  injective Refl = Refl
 
 export
 DecEq Namespace where
-
-  decEq (MkNS ms) (MkNS ns) with (decEq ms ns)
-    decEq (MkNS ms) (MkNS ns) | No contra = No (contra . mkNSInjective)
-    decEq (MkNS ms) (MkNS ns) | Yes eqmsns = Yes (cong MkNS eqmsns)
+  decEq (MkNS ms) (MkNS ns) = decEqCong (decEq ms ns)
 
 -- TODO: move somewhere more appropriate
 export

src/Core/TT/Primitive.idr

@@ -5,11 +5,10 @@ import Core.Name
 import Data.String
 import Data.Vect
 
-import Decidable.Equality
-
 import Idris.Pretty.Annotations
 
 import Libraries.Data.Ordering.Extra
+import Libraries.Decidable.Equality as L
 import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default total
@@ -114,44 +113,20 @@ primTypeEq _ _ = Nothing
 
 export
 constantEq : (x, y : Constant) -> Maybe (x = y)
-constantEq (I x) (I y) = case decEq x y of
-                              Yes Refl => Just Refl
-                              No contra => Nothing
-constantEq (I8 x) (I8 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (I16 x) (I16 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (I32 x) (I32 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (I64 x) (I64 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (B8 x) (B8 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (B16 x) (B16 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (B32 x) (B32 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (B64 x) (B64 y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (BI x) (BI y) = case decEq x y of
-                                Yes Refl => Just Refl
-                                No contra => Nothing
-constantEq (Str x) (Str y) = case decEq x y of
-                                  Yes Refl => Just Refl
-                                  No contra => Nothing
-constantEq (Ch x) (Ch y) = case decEq x y of
-                                Yes Refl => Just Refl
-                                No contra => Nothing
+constantEq (I x) (I y) = L.maybeCong I (L.maybeEq x y)
+constantEq (I8 x) (I8 y) = L.maybeCong I8 (L.maybeEq x y)
+constantEq (I16 x) (I16 y) = L.maybeCong I16 (L.maybeEq x y)
+constantEq (I32 x) (I32 y) = L.maybeCong I32 (L.maybeEq x y)
+constantEq (I64 x) (I64 y) = L.maybeCong I64 (L.maybeEq x y)
+constantEq (B8 x) (B8 y) = L.maybeCong B8 (L.maybeEq x y)
+constantEq (B16 x) (B16 y) = L.maybeCong B16 (L.maybeEq x y)
+constantEq (B32 x) (B32 y) = L.maybeCong B32 (L.maybeEq x y)
+constantEq (B64 x) (B64 y) = L.maybeCong B64 (L.maybeEq x y)
+constantEq (BI x) (BI y) = L.maybeCong BI (L.maybeEq x y)
+constantEq (Str x) (Str y) = L.maybeCong Str (L.maybeEq x y)
+constantEq (Ch x) (Ch y) = L.maybeCong Ch (L.maybeEq x y)
 constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
-constantEq (PrT x) (PrT y) = (\xy => cong PrT xy) <$> primTypeEq x y
+constantEq (PrT x) (PrT y) = L.maybeCong PrT (primTypeEq x y)
 constantEq WorldVal WorldVal = Just Refl
 
 constantEq _ _ = Nothing

src/Libraries/Decidable/Equality.idr

@@ -0,0 +1,20 @@
+-- Remove as soon as 0.9.0 is released
+module Libraries.Decidable.Equality
+
+import public Decidable.Equality
+
+public export
+maybeEq : DecEq a => (x, y : a) -> Maybe (x = y)
+maybeEq x y = case decEq x y of
+                   Yes eq => Just eq
+                   No _   => Nothing
+
+%inline
+public export
+maybeCong : (f : a -> b) -> Maybe (x = y) -> Maybe (f x = f y)
+maybeCong f = map (\eq => cong f eq)
+
+%inline
+public export
+maybeCong2 : (f : a -> b -> c) -> Maybe (x = y) -> Maybe (v = w) -> Maybe (f x v = f y w)
+maybeCong2 f mxy mvw = (\xy, vw => cong2 f xy vw) <$> mxy <*> mvw