From e852097ce41243fcebf2923f62b34f9197378bda Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 14 Nov 2024 15:29:14 +0100 Subject: [PATCH 1/2] make Eq builtin --- Stdlib/Trait/Eq.juvix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix index 71cb707f..fe3d7c7f 100644 --- a/Stdlib/Trait/Eq.juvix +++ b/Stdlib/Trait/Eq.juvix @@ -4,8 +4,9 @@ import Stdlib.Data.Bool.Base open; import Stdlib.Data.Fixity open; --- A trait defining equality +builtin eq trait -type Eq A := mkEq@{eq : A -> A -> Bool}; +type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool}; syntax operator == comparison; syntax operator /= comparison; From e9bf3dd6486de488d5faeb0f62e8d275b65e3f2f Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 20 Nov 2024 08:24:22 +0100 Subject: [PATCH 2/2] derive some Eq instances --- Stdlib/Data/Bool.juvix | 11 ++--------- Stdlib/Data/Maybe.juvix | 11 ++--------- Stdlib/Data/Pair.juvix | 9 ++------- Stdlib/Data/Result.juvix | 11 ++--------- Stdlib/Data/Unit.juvix | 7 ++----- Stdlib/Trait/Ord.juvix | 11 ++--------- 6 files changed, 12 insertions(+), 48 deletions(-) diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix index 73490d07..6b275e43 100644 --- a/Stdlib/Data/Bool.juvix +++ b/Stdlib/Data/Bool.juvix @@ -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 diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix index 2fff90d6..25103e62 100644 --- a/Stdlib/Data/Maybe.juvix +++ b/Stdlib/Data/Maybe.juvix @@ -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) := diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix index bcadcc76..fcf6a17e 100644 --- a/Stdlib/Data/Pair.juvix +++ b/Stdlib/Data/Pair.juvix @@ -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 diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix index 8da00279..a836b286 100644 --- a/Stdlib/Data/Result.juvix +++ b/Stdlib/Data/Result.juvix @@ -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 diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix index 1bdb887c..a719b592 100644 --- a/Stdlib/Data/Unit.juvix +++ b/Stdlib/Data/Unit.juvix @@ -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 := diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix index d590a868..c55ab9e8 100644 --- a/Stdlib/Trait/Ord.juvix +++ b/Stdlib/Trait/Ord.juvix @@ -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