pragmas

Stdlib/Data/Bool.juvix

@@ -5,6 +5,7 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
+{-# specialize: true, inline: case #-}
 instance
 boolEqI : Eq Bool :=
   mkEq
@@ -14,6 +15,7 @@ boolEqI : Eq Bool :=
       | _ _ := false
     };
 
+{-# specialize: true, inline: case #-}
 instance
 boolOrdI : Ord Bool :=
   mkOrd

Stdlib/Data/List.juvix

@@ -53,25 +53,25 @@ showListI {A} {{Show A}} : Show (List A) :=
       | s := "(" ++str go s ++str ")"
     };
 
-{-# inline: case #-}
+{-# specialize: true, inline: case #-}
 instance
 functorListI : Functor List :=
   mkFunctor@{
     map := listMap
   };
 
-{-# specialize: true, inline: case #-}
+{-# specialize: true, inline: true #-}
 instance
 monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;
 
-{-# inline: case #-}
+{-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableListI : Polymorphic.Foldable List :=
   Polymorphic.mkFoldable@{
     for := listFor;
     rfor := listRfor
   };
 
-{-# specialize: true, inline: case #-}
+{-# specialize: true, inline: true #-}
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;

Stdlib/Data/Maybe.juvix

@@ -10,6 +10,7 @@ import Stdlib.Trait.Functor open;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 
+{-# specialize: true, inline: case #-}
 instance
 eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
   mkEq
@@ -27,6 +28,7 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
       | (just a) := "just " ++str Show.show a
     };
 
+{-# specialize: true, inline: case #-}
 instance
 ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
   mkOrd
@@ -37,6 +39,7 @@ ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
       | (just _) nothing := GT
     };
 
+{-# specialize: true, inline: case #-}
 instance
 functorMaybeI : Functor Maybe :=
   mkFunctor@{
@@ -45,6 +48,6 @@ functorMaybeI : Functor Maybe :=
       | (just a) := just (f a)
   };
 
-{-# specialize: true, inline: case #-}
+{-# specizalize: true, inline: true #-}
 instance
 monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;

Stdlib/Data/Pair.juvix

@@ -8,10 +8,12 @@ import Stdlib.Trait.Eq open;
 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 eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
 
+{-# specialize: true, inline: case #-}
 instance
 ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
   | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=

Stdlib/Data/Result.juvix

@@ -7,6 +7,7 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Functor open;
 
+{-# specialize: true, inline: case #-}
 instance
 ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
   mkOrd@{
@@ -17,6 +18,7 @@ ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
       | (ok _) (error _) := GT
   };
 
+{-# specialize: true, inline: case #-}
 instance
 eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
   mkEq@{
@@ -26,12 +28,14 @@ eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
       | _ _ := false
   };
 
+{-# specialize: true, inline: case #-}
 instance
 functorResultI {err} : Functor (Result err) :=
   mkFunctor@{
     map := mapOk
   };
 
+{-# specialize: true, inline: true #-}
 instance
 monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
   fromPolymorphicFunctor;

Stdlib/Data/Unit.juvix

@@ -21,9 +21,12 @@ ordUnitI : Ord Unit := mkOrd λ {unit unit := EQ};
 instance
 showUnitI : Show Unit := mkShow λ {unit := "unit"};
 
+{-# specialize: true, inline: case #-}
 instance
 foldableUnitI : Foldable Unit Unit :=
   mkFoldable@{
+    {-# inline: true #-}
     rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit;
+    {-# inline: true #-}
     for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit
   };

Stdlib/Trait/Foldable/Monomorphic.juvix

@@ -4,6 +4,7 @@ import Stdlib.Function open;
 import Stdlib.Trait.Foldable.Polymorphic as Poly;
 
 --- A trait for combining elements into a single result, processing one element at a time.
+{-# specialize: true #-}
 trait
 type Foldable (container elem : Type) :=
   mkFoldable {
@@ -26,7 +27,7 @@ fromPolymorphicFoldable
     rfor := Poly.rfor
   };
 
-{-# inline: 2 #-}
+{-# inline: true #-}
 foldl
   {container elem}
   {{Foldable container elem}}
@@ -37,7 +38,7 @@ foldl
   : B := for (acc := ini) (x in ls) {g acc x};
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
-{-# inline: 1 #-}
+{-# inline: 2 #-}
 foldr
   {container elem : Type}
   {{Foldable container elem}}

Stdlib/Trait/Functor/Monomorphic.juvix

@@ -4,23 +4,28 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
 import Stdlib.Trait.Functor.Polymorphic as Poly;
 
+{-# specialize: true #-}
 trait
 type Functor (container elem : Type) :=
   mkFunctor {
     syntax iterator map {init := 0; range := 1};
+    {-# specialize: [1] #-}
     map : (elem -> elem) -> container -> container
   };
 
 open Functor public;
 
+{-# inline: case #-}
 fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elem :=
   mkFunctor@{
     map := Poly.map
   };
 
 syntax operator <$> lapp;
+{-# inline: true #-}
 <$> {container elem} {{Functor container elem}} : (elem -> elem) -> container -> container := map;
 
 syntax operator $> lapp;
+{-# inline: true #-}
 $> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container :=
   λ {_ := b} <$> fa;

Stdlib/Trait/Functor/Polymorphic.juvix

@@ -3,19 +3,24 @@ module Stdlib.Trait.Functor.Polymorphic;
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Unit open;
 
+{-# specialize: true #-}
 trait
 type Functor (f : Type -> Type) :=
   mkFunctor {
     syntax iterator map {init := 0; range := 1};
+    {-# specialize: [1] #-}
     map : {A B : Type} -> (A -> B) -> f A -> f B
   };
 
 open Functor public;
 
 syntax operator <$> lapp;
+{-# inline: true #-}
 <$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map;
 
 syntax operator $> lapp;
+{-# inline: true #-}
 $> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B := λ {_ := b} <$> fa;
 
+{-# inline: true #-}
 void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit;