inline always

anoma · Oct 6, 2023 · f776f7f · f776f7f
1 parent 9970a3f
commit f776f7f
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 12 deletions.
diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
@@ -20,18 +20,18 @@ import Stdlib.Data.Int.Ord as Int;
 builtin int-to-string
 axiom intToString : Int -> String;
 
-{-# inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 eqIntI : Eq Int := mkEq (Int.==);
 
-{-# inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 ordIntI : Ord Int := mkOrd Int.compare;
 
 instance
 showIntI : Show Int := mkShow intToString;
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 naturalIntI : Natural Int :=
   mkNatural@{
@@ -42,7 +42,7 @@ naturalIntI : Natural Int :=
     fromNat := ofNat;
   };
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 integralIntI : Integral Int :=
   mkIntegral@{

diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
@@ -21,18 +21,18 @@ axiom natToString : Nat -> String;
 builtin string-to-nat
 axiom stringToNat : String -> Nat;
 
-{-# inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 eqNatI : Eq Nat := mkEq (Nat.==);
 
-{-# inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 ordNatI : Ord Nat := mkOrd Nat.compare;
 
 instance
 showNatI : Show Nat := mkShow natToString;
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: always #-}
 instance
 naturalNatI : Natural Nat :=
   mkNatural@{

diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
@@ -8,11 +8,11 @@ trait
 type Eq A := mkEq {eq : A -> A -> Bool};
 
 syntax operator == comparison;
+syntax operator /= comparison;
 
+{-# inline: always #-}
 == {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
 
-syntax operator /= comparison;
-
 --- Tests for inequality.
-{-# inline: true #-}
+{-# inline: always #-}
 /= {A} {{Eq A}} (x y : A) : Bool := not (x == y);
diff --git a/Stdlib/Trait/Natural.juvix b/Stdlib/Trait/Natural.juvix
@@ -15,10 +15,13 @@ type Natural A :=
 
 open Natural using {div; mod} public;
 
+syntax operator + additive;
+syntax operator * multiplicative;
+
 -- TODO: we need to define those separately because it's currently not possible
 -- to declare record fields as operators
-syntax operator + additive;
+{-# inline: always #-}
 + {A} {{Natural A}} : A -> A -> A := Natural.+;
 
-syntax operator * multiplicative;
+{-# inline: always #-}
 * {A} {{Natural A}} : A -> A -> A := Natural.*;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
@@ -28,6 +28,7 @@ type Ord A := mkOrd {cmp : A -> A -> Ordering};
 syntax operator <= comparison;
 
 --- Returns ;true; iff the first element is less than or equal to the second.
+{-# inline: always #-}
 <= {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of {
     | EQ := true
@@ -38,6 +39,7 @@ syntax operator <= comparison;
 syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
+{-# inline: always #-}
 < {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of {
     | EQ := false
@@ -48,15 +50,19 @@ syntax operator < comparison;
 syntax operator > comparison;
 
 --- Returns ;true; iff the first element is greater than the second.
+{-# inline: always #-}
 > {A} {{Ord A}} (x y : A) : Bool := y < x;
 
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
+{-# inline: always #-}
 >= {A} {{Ord A}} (x y : A) : Bool := y <= x;
 
 --- Returns the smaller element.
+{-# inline: always #-}
 min {A} {{Ord A}} (x y : A) : A := if (x < y) x y;
 
 --- Returns the larger element.
+{-# inline: always #-}
 max {A} {{Ord A}} (x y : A) : A := if (x > y) x y;