Skip to content

Commit

Permalink
derive some Ord instances
Browse files Browse the repository at this point in the history
  • Loading branch information
janmasrovira committed Nov 21, 2024
1 parent f0a1e1e commit 19aa0b0
Show file tree
Hide file tree
Showing 6 changed files with 16 additions and 48 deletions.
12 changes: 2 additions & 10 deletions Stdlib/Data/Bool.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -12,16 +12,8 @@ deriving instance
eqBoolI : Eq Bool;

{-# specialize: true, inline: case #-}
instance
ordBoolI : Ord Bool :=
mkOrd@{
cmp (x y : Bool) : Ordering :=
case x, y of
| false, false := Equal
| false, true := LessThan
| true, false := GreaterThan
| true, true := Equal;
};
deriving instance
ordBoolI : Ord Bool;

instance
showBoolI : Show Bool :=
Expand Down
12 changes: 2 additions & 10 deletions Stdlib/Data/Maybe.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,8 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
};

{-# specialize: true, inline: case #-}
instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
mkOrd@{
cmp (m1 m2 : Maybe A) : Ordering :=
case m1, m2 of
| nothing, nothing := Equal
| just a1, just a2 := Ord.cmp a1 a2
| nothing, just _ := LessThan
| just _, nothing := GreaterThan;
};
deriving instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A);

{-# specialize: true, inline: case #-}
instance
Expand Down
14 changes: 2 additions & 12 deletions Stdlib/Data/Pair.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,8 @@ deriving instance
eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);

{-# specialize: true, inline: case #-}
instance
ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
| {{mkOrd cmpA}} {{mkOrd cmpB}} :=
mkOrd@{
cmp (p1 p2 : Pair A B) : Ordering :=
case p1, p2 of
(a1, b1), a2, b2 :=
case cmpA a1 a2 of
| LessThan := LessThan
| GreaterThan := GreaterThan
| Equal := cmpB b1 b2;
};
deriving instance
ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B);

instance
showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
Expand Down
12 changes: 2 additions & 10 deletions Stdlib/Data/Result.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -11,17 +11,9 @@ import Stdlib.Trait.Show open;
import Stdlib.Trait open;

{-# specialize: true, inline: case #-}
instance
deriving instance
ordResultI
{Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
mkOrd@{
cmp (result1 result2 : Result Error Value) : Ordering :=
case result1, result2 of
| error a1, error a2 := Ord.cmp a1 a2
| ok b1, ok b2 := Ord.cmp b1 b2
| error _, ok _ := LessThan
| ok _, error _ := GreaterThan;
};
{Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value);

{-# specialize: true, inline: case #-}
deriving instance
Expand Down
7 changes: 2 additions & 5 deletions Stdlib/Data/Unit.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,8 @@ import Stdlib.Trait.Foldable open;
deriving instance
eqUnitI : Eq Unit;

instance
ordUnitI : Ord Unit :=
mkOrd@{
cmp (_ _ : Unit) : Ordering := Equal;
};
deriving instance
ordUnitI : Ord Unit;

instance
showUnitI : Show Unit :=
Expand Down
7 changes: 6 additions & 1 deletion Stdlib/Trait/Ord.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import Stdlib.Data.Fixity open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Trait.Eq open;

builtin ordering
type Ordering :=
| LessThan
| Equal
Expand All @@ -28,8 +29,12 @@ deriving instance
orderingEqI : Eq Ordering;

--- A trait for defining a total order
builtin ord
trait
type Ord A := mkOrd@{cmp : A -> A -> Ordering};
type Ord A := mkOrd@{builtin compare cmp : A -> A -> Ordering};

deriving instance
orderingOrdI : Ord Ordering;

syntax operator <= comparison;

Expand Down

0 comments on commit 19aa0b0

Please sign in to comment.