diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix index 73490d07..af191c98 100644 --- a/Stdlib/Data/Bool.juvix +++ b/Stdlib/Data/Bool.juvix @@ -8,27 +8,12 @@ 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 -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 := diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index f62aa06d..fb72292a 100644 --- a/Stdlib/Data/List.juvix +++ b/Stdlib/Data/List.juvix @@ -21,6 +21,7 @@ phead {A} {{Partial}} : List A -> A | (x :: _) := x | nil := fail "head: empty list"; +{-# specialize: true, inline: case #-} instance eqListI {A} {{Eq A}} : Eq (List A) := let @@ -37,6 +38,7 @@ eqListI {A} {{Eq A}} : Eq (List A) := isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list; +{-# specialize: true, inline: case #-} instance ordListI {A} {{Ord A}} : Ord (List A) := let @@ -71,7 +73,7 @@ functorListI : Functor List := map := listMap; }; -{-# specialize: true, inline: true #-} +{-# specialize: true, inline: case #-} instance monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor; @@ -84,7 +86,7 @@ polymorphicFoldableListI : Polymorphic.Foldable List := rfor := listRfor; }; -{-# specialize: true, inline: true #-} +{-# specialize: true, inline: case #-} instance foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable; diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix index 75ee1f53..16a598c5 100644 --- a/Stdlib/Data/Map.juvix +++ b/Stdlib/Data/Map.juvix @@ -32,6 +32,7 @@ value {Key Value} (binding : Binding Key Value) : Value := toPair {Key Value} (binding : Binding Key Value) : Pair Key Value := key binding, value binding; +{-# specialize: true, inline: case #-} instance bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) := mkOrd@{ diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix index 2fff90d6..f2fe5036 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) := @@ -34,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 diff --git a/Stdlib/Data/Ordering.juvix b/Stdlib/Data/Ordering.juvix new file mode 100644 index 00000000..b399d754 --- /dev/null +++ b/Stdlib/Data/Ordering.juvix @@ -0,0 +1,38 @@ +module Stdlib.Data.Ordering; + +import Stdlib.Trait.Eq open; +import Stdlib.Data.Bool.Base open; +import Stdlib.Trait.Show open; + +builtin ordering +type Ordering := + | LessThan + | Equal + | GreaterThan; + +isLessThan (ordering : Ordering) : Bool := + case ordering of + | LessThan := true + | _ := false; + +isEqual (ordering : Ordering) : Bool := + case ordering of + | Equal := true + | _ := false; + +isGreaterThan (ordering : Ordering) : Bool := + case ordering of + | GreaterThan := true + | _ := false; + +deriving instance +orderingEqI : Eq Ordering; + +instance +orderingShowI : Show Ordering := + mkShow@{ + show : Ordering -> String + | Equal := "Equal" + | LessThan := "LessThan" + | GreaterThan := "GreaterThan"; + }; diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix index bcadcc76..76fdd832 100644 --- a/Stdlib/Data/Pair.juvix +++ b/Stdlib/Data/Pair.juvix @@ -9,27 +9,12 @@ 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 -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) diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix index 8da00279..ad2eb1e9 100644 --- a/Stdlib/Data/Result.juvix +++ b/Stdlib/Data/Result.juvix @@ -11,28 +11,12 @@ import Stdlib.Trait.Show open; import Stdlib.Trait open; {-# specialize: true, inline: case #-} -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; - }; +deriving instance +ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value); {-# 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..c004f780 100644 --- a/Stdlib/Data/Unit.juvix +++ b/Stdlib/Data/Unit.juvix @@ -10,17 +10,11 @@ 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 := - mkOrd@{ - cmp (_ _ : Unit) : Ordering := Equal; - }; +deriving instance +ordUnitI : Ord Unit; instance showUnitI : Show Unit := diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix index 71cb707f..1f0ce368 100644 --- a/Stdlib/Trait/Eq.juvix +++ b/Stdlib/Trait/Eq.juvix @@ -4,8 +4,13 @@ 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; diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix index da38c701..5bdd161e 100644 --- a/Stdlib/Trait/Foldable/Monomorphic.juvix +++ b/Stdlib/Trait/Foldable/Monomorphic.juvix @@ -19,7 +19,7 @@ open Foldable public; --- Make a monomorphic ;Foldable; instance from a polymorphic one. --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance. -{-# inline: case #-} +{-# inline: always #-} fromPolymorphicFoldable {F : Type -> Type} {{foldable : Poly.Foldable F}} diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix index 076fde2c..4dd92fc6 100644 --- a/Stdlib/Trait/Functor/Monomorphic.juvix +++ b/Stdlib/Trait/Functor/Monomorphic.juvix @@ -15,7 +15,7 @@ type Functor (Container Elem : Type) := open Functor public; -{-# inline: case #-} +{-# inline: always #-} fromPolymorphicFunctor {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem := mkFunctor@{ diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix index d590a868..a8627de5 100644 --- a/Stdlib/Trait/Ord.juvix +++ b/Stdlib/Trait/Ord.juvix @@ -3,40 +3,19 @@ module Stdlib.Trait.Ord; import Stdlib.Data.Fixity open; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Eq open; - -type Ordering := - | LessThan - | Equal - | GreaterThan; - -isLessThan (ordering : Ordering) : Bool := - case ordering of - | LessThan := true - | _ := false; - -isEqual (ordering : Ordering) : Bool := - case ordering of - | Equal := true - | _ := false; - -isGreaterThan (ordering : Ordering) : Bool := - case ordering of - | 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; - }; +import Stdlib.Data.Ordering open public; --- 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; diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix index 1670c417..ff57bdc9 100644 --- a/Stdlib/Trait/Partial.juvix +++ b/Stdlib/Trait/Partial.juvix @@ -4,7 +4,10 @@ import Stdlib.Data.String.Base open; import Stdlib.Debug.Fail as Debug; trait -type Partial := mkPartial@{fail : {A : Type} -> String -> A}; +type Partial := + mkPartial@{ + fail : {A : Type} -> String -> A; + }; open Partial public; diff --git a/Stdlib/Trait/Show.juvix b/Stdlib/Trait/Show.juvix index 099513b0..9ca64c21 100644 --- a/Stdlib/Trait/Show.juvix +++ b/Stdlib/Trait/Show.juvix @@ -1,6 +1,9 @@ module Stdlib.Trait.Show; -import Stdlib.Data.String.Base open; +import Juvix.Builtin.V1.String open public; trait -type Show A := mkShow@{show : A -> String}; +type Show A := + mkShow@{ + show : A -> String; + };