Skip to content

Commit

Permalink
derive some Eq instances
Browse files Browse the repository at this point in the history
  • Loading branch information
janmasrovira committed Nov 20, 2024
1 parent a1a019b commit f0a1e1e
Show file tree
Hide file tree
Showing 6 changed files with 12 additions and 48 deletions.
11 changes: 2 additions & 9 deletions Stdlib/Data/Bool.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,8 @@ import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;

{-# specialize: true, inline: case #-}
instance
eqBoolI : Eq Bool :=
mkEq@{
eq (x y : Bool) : Bool :=
case x, y of
| true, true := true
| false, false := true
| _ := false;
};
deriving instance
eqBoolI : Eq Bool;

{-# specialize: true, inline: case #-}
instance
Expand Down
11 changes: 2 additions & 9 deletions Stdlib/Data/Maybe.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,8 @@ import Stdlib.Data.String.Base open;
import Stdlib.Data.Pair.Base open;

{-# specialize: true, inline: case #-}
instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
mkEq@{
eq (m1 m2 : Maybe A) : Bool :=
case m1, m2 of
| nothing, nothing := true
| just a1, just a2 := Eq.eq a1 a2
| _ := false;
};
deriving instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A);

instance
showMaybeI {A} {{Show A}} : Show (Maybe A) :=
Expand Down
9 changes: 2 additions & 7 deletions Stdlib/Data/Pair.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,8 @@ import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;

{-# specialize: true, inline: case #-}
instance
eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
| {{mkEq eqA}} {{mkEq eqB}} :=
mkEq@{
eq (p1 p2 : Pair A B) : Bool :=
case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2;
};
deriving instance
eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);

{-# specialize: true, inline: case #-}
instance
Expand Down
11 changes: 2 additions & 9 deletions Stdlib/Data/Result.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,8 @@ ordResultI
};

{-# specialize: true, inline: case #-}
instance
eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
mkEq@{
eq (result1 result2 : Result Error Value) : Bool :=
case result1, result2 of
| error a1, error a2 := a1 == a2
| ok b1, ok b2 := b1 == b2
| _, _ := false;
};
deriving instance
eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value);

instance
showResultI
Expand Down
7 changes: 2 additions & 5 deletions Stdlib/Data/Unit.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,8 @@ import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Foldable open;

instance
eqUnitI : Eq Unit :=
mkEq@{
eq (_ _ : Unit) : Bool := true;
};
deriving instance
eqUnitI : Eq Unit;

instance
ordUnitI : Ord Unit :=
Expand Down
11 changes: 2 additions & 9 deletions Stdlib/Trait/Ord.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,8 @@ isGreaterThan (ordering : Ordering) : Bool :=
| GreaterThan := true
| _ := false;

instance
orderingEqI : Eq Ordering :=
mkEq@{
eq (ordering1 ordering2 : Ordering) : Bool :=
case ordering2 of
| LessThan := isLessThan ordering1
| Equal := isEqual ordering1
| GreaterThan := isGreaterThan ordering1;
};
deriving instance
orderingEqI : Eq Ordering;

--- A trait for defining a total order
trait
Expand Down

0 comments on commit f0a1e1e

Please sign in to comment.