From 17a82dd466010b51924677b16a3f09a6c4c86a80 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Wed, 14 Aug 2024 17:03:51 +0200
Subject: [PATCH] Update pragmas (#122)

* Closes #121
* Depends on https://github.com/anoma/juvix/pull/2944
* Includes https://github.com/anoma/juvix-stdlib/pull/123
* Adds `Stdlib.Data.Range` to the Prelude. Since now `for` and `rfor`
are trait fields, there is no name clash anymore.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
---
 Stdlib/Data/Bool.juvix                  |  2 +
 Stdlib/Data/Bool/Base.juvix             |  2 +-
 Stdlib/Data/List.juvix                  |  4 ++
 Stdlib/Data/Maybe.juvix                 |  4 ++
 Stdlib/Data/Pair.juvix                  |  2 +
 Stdlib/Data/Range.juvix                 | 78 +++++++++++++++++--------
 Stdlib/Data/Result.juvix                |  4 ++
 Stdlib/Data/Unit.juvix                  |  3 +
 Stdlib/Prelude.juvix                    |  1 +
 Stdlib/Trait/Eq.juvix                   |  2 +-
 Stdlib/Trait/Foldable/Monomorphic.juvix |  6 +-
 Stdlib/Trait/Foldable/Polymorphic.juvix |  4 +-
 Stdlib/Trait/Functor/Monomorphic.juvix  |  5 ++
 Stdlib/Trait/Functor/Polymorphic.juvix  |  5 ++
 Stdlib/Trait/Ord.juvix                  |  4 +-
 Stdlib/Trait/Ord/Eq.juvix               |  2 +-
 16 files changed, 94 insertions(+), 34 deletions(-)

diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
index 5978e88b..bfc5d891 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/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
diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix
index 0743af31..ce31e40d 100644
--- a/Stdlib/Data/Bool/Base.juvix
+++ b/Stdlib/Data/Bool/Base.juvix
@@ -4,7 +4,7 @@ import Juvix.Builtin.V1.Bool open public;
 import Stdlib.Data.Fixity open;
 
 --- Logical negation.
-{-# isabelle-function: {name: "¬"} #-}
+{-# isabelle-function: {name: "\\<not>"} #-}
 not : Bool → Bool
   | true := false
   | false := true;
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index 0f5f3171..67d46218 100644
--- a/Stdlib/Data/List.juvix
+++ b/Stdlib/Data/List.juvix
@@ -53,15 +53,18 @@ showListI {A} {{Show A}} : Show (List A) :=
       | s := "(" ++str go s ++str ")"
     };
 
+{-# specialize: true, inline: case #-}
 instance
 functorListI : Functor List :=
   mkFunctor@{
     map := listMap
   };
 
+{-# specialize: true, inline: true #-}
 instance
 monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;
 
+{-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableListI : Polymorphic.Foldable List :=
   Polymorphic.mkFoldable@{
@@ -69,5 +72,6 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
     rfor := listRfor
   };
 
+{-# specialize: true, inline: true #-}
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index ce164aec..d10c21b8 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/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,5 +48,6 @@ functorMaybeI : Functor Maybe :=
       | (just a) := just (f a)
   };
 
+{-# specizalize: true, inline: true #-}
 instance
 monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index b3a24088..6ddf5275 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/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}} :=
diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
index 9e5a3d19..b70ad273 100644
--- a/Stdlib/Data/Range.juvix
+++ b/Stdlib/Data/Range.juvix
@@ -12,53 +12,81 @@ import Stdlib.Data.Nat open;
 type Range N :=
   mkRange {
     low : N;
-    high : N;
-    step : N
+    high : N
   };
 
-syntax iterator for {init := 1; range := 1};
-
-{-# specialize: [1, 2, 3, 5] #-}
-for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A) : Range N → A
-  | mkRange@{low; high; step} :=
-    let
-      {-# specialize-by: [f] #-}
-      terminating
-      go (acc : A) (n : N) : A := ite (n > high) acc (go (f acc n) (n + step));
-    in go a low;
+type StepRange N :=
+  mkStepRange {
+    range : Range N;
+    step : N
+  };
 
 syntax operator to range;
 
 --- `x to y` is the range [x..y]
 {-# inline: always #-}
-to {N} {{Natural N}} (l h : N) : Range N := mkRange l h 1;
+to {N} {{Natural N}} (l h : N) : Range N := mkRange l h;
 
 syntax operator step step;
 
 --- `x to y step s` is the range [x, x + s, ..., y]
 {-# inline: always #-}
-step {N} (r : Range N) (s : N) : Range N := r@Range{step := s};
+step {N} (r : Range N) (s : N) : StepRange N := mkStepRange r s;
+
+-- This instance assumes that `low <= high`.
+{-# specialize: true, inline: case #-}
+instance
+foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
+  mkFoldable@{
+    {-# specialize: [1, 3] #-}
+    for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+      | (mkRange low high) :=
+        let
+          {-# specialize-by: [f, high] #-}
+          terminating
+          go (acc : B) (next : N) : B :=
+            if
+              | next == high := f acc next
+              | else := go (f acc next) (next + 1);
+        in go ini low;
+    {-# specialize: [1, 3] #-}
+    rfor {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+      | (mkRange low high) :=
+        let
+          {-# specialize-by: [f, high] #-}
+          terminating
+          go (next : N) : B :=
+            if
+              | next == high := f ini next
+              | else := f (go (next + 1)) next;
+        in go low
+  };
 
 -- This instance assumes that (low + step*k > high) for some k.
+{-# specialize: true, inline: case #-}
 instance
-foldableRangeI {N} {{Ord N}} {{Natural N}} : Foldable (Range N) N :=
+foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
   mkFoldable@{
-    for {B : Type} (g : B -> N -> B) (ini : B) : Range N -> B
-      | (mkRange low high step) :=
+    {-# specialize: [1, 3] #-}
+    for {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+      | (mkStepRange (mkRange low high) step) :=
         let
+          {-# specialize-by: [f, high, step] #-}
           terminating
           go (acc : B) (next : N) : B :=
             if
-              | next <= high := go (g acc next) (next + step)
-              | else := acc;
+              | next > high := acc
+              | else := go (f acc next) (next + step);
         in go ini low;
-    rfor {B : Type} (g : B -> N -> B) (ini : B) : Range N -> B
-      | (mkRange low high step) :=
+    {-# specialize: [1, 3] #-}
+    rfor {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+      | (mkStepRange (mkRange low high) step) :=
         let
+          {-# specialize-by: [f, high, step] #-}
           terminating
-          go (base : B) (next : N) : B :=
+          go (next : N) : B :=
             if
-              | next <= high := g (go base (next + step)) next
-              | else := base;
-        in go ini low
+              | next <= high := f (go (next + step)) next
+              | else := ini;
+        in go low
   };
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index ef9dfd1e..d4195cc0 100644
--- a/Stdlib/Data/Result.juvix
+++ 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;
diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
index 9ac1bd11..3a882410 100644
--- a/Stdlib/Data/Unit.juvix
+++ b/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
   };
diff --git a/Stdlib/Prelude.juvix b/Stdlib/Prelude.juvix
index 4db565c7..bca3d057 100644
--- a/Stdlib/Prelude.juvix
+++ b/Stdlib/Prelude.juvix
@@ -14,6 +14,7 @@ import Stdlib.Data.Field open public;
 import Stdlib.Data.Pair open public;
 import Stdlib.Data.String open public;
 import Stdlib.Data.Result open public;
+import Stdlib.Data.Range open public;
 import Stdlib.Function open public;
 import Stdlib.System.IO open public;
 
diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
index 7ab2f679..9ccb3c4d 100644
--- a/Stdlib/Trait/Eq.juvix
+++ b/Stdlib/Trait/Eq.juvix
@@ -14,5 +14,5 @@ syntax operator /= comparison;
 == {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
 
 --- Tests for inequality.
-{-# inline: always, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-}
+{-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
 /= {A} {{Eq A}} (x y : A) : Bool := not (x == y);
diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index 22182b6c..319e62cc 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -4,15 +4,14 @@ 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 {
     syntax iterator for {init := 1; range := 1};
-    {-# inline: 0 #-}
     for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    {-# inline: 0 #-}
     rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
   };
 
@@ -20,6 +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 #-}
 fromPolymorphicFoldable
   {f : Type -> Type} {{foldable : Poly.Foldable f}} {elem} : Foldable (f elem) elem :=
   mkFoldable@{
@@ -27,6 +27,7 @@ fromPolymorphicFoldable
     rfor := Poly.rfor
   };
 
+{-# inline: true #-}
 foldl
   {container elem}
   {{Foldable container elem}}
@@ -37,6 +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: 2 #-}
 foldr
   {container elem : Type}
   {{Foldable container elem}}
diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
index d0a2a40c..624cb6cb 100644
--- a/Stdlib/Trait/Foldable/Polymorphic.juvix
+++ b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -7,20 +7,20 @@ trait
 type Foldable (f : Type -> Type) :=
   mkFoldable {
     syntax iterator for {init := 1; range := 1};
-    {-# inline: 0 #-}
     for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    {-# inline: 0 #-}
     rfor : {A B : Type} -> (B → A → B) -> B → f A → B
   };
 
 open Foldable public;
 
 --- Combine the elements of the type using the provided function starting with the element in the left-most position.
+{-# inline: true #-}
 foldl {f : Type -> Type} {{Foldable f}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : 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: true #-}
 foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : B :=
   rfor (acc := ini) (x in ls) {g x acc};
diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
index c6e3c4f8..c5c188e2 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/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;
diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
index 3c2a4a46..37b12c02 100644
--- a/Stdlib/Trait/Functor/Polymorphic.juvix
+++ b/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;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index 17a3e23b..8573c4ba 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -37,7 +37,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, isabelle-operator: {name: "≤", prec: 50, assoc: none} #-}
+{-# inline: always, isabelle-operator: {name: "\\<le>", prec: 50, assoc: none} #-}
 <= {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
     | EQ := true
@@ -63,7 +63,7 @@ syntax operator > comparison;
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
-{-# inline: always, isabelle-operator: {name: "≥", prec: 50, assoc: none} #-}
+{-# inline: always, isabelle-operator: {name: "\\<ge>", prec: 50, assoc: none} #-}
 >= {A} {{Ord A}} (x y : A) : Bool := y <= x;
 
 --- Returns the smaller element.
diff --git a/Stdlib/Trait/Ord/Eq.juvix b/Stdlib/Trait/Ord/Eq.juvix
index 8816d830..c4e90751 100644
--- a/Stdlib/Trait/Ord/Eq.juvix
+++ b/Stdlib/Trait/Ord/Eq.juvix
@@ -18,5 +18,5 @@ syntax operator == comparison;
 syntax operator /= comparison;
 
 --- Tests for inequality.
-{-# inline: true, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-}
+{-# inline: true, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
 /= {A} {{Ord A}} (x y : A) : Bool := not (x == y);