generic range

Stdlib/Data/Range.juvix

@@ -0,0 +1,37 @@
+module Stdlib.Data.Range;
+
+import Stdlib.Data.Fixity open;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Natural open;
+import Stdlib.Trait.Ord open;
+
+--- A range of naturals
+type Range N :=
+  mkRange {
+    low : N;
+    high : N;
+    step : 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 :=
+        if (n > high) acc (go (f acc n) (n + step));
+    in go a low;
+
+syntax operator to range;
+
+--- `x to y` is the range [x..y]
+to {N} {{Natural N}} (l h : N) : Range N := mkRange l h (fromNat 1);
+
+syntax operator step step;
+
+--- `x to y step s` is the range [x,x+s,..,y]
+step {N} (r : Range N) (s : N) : Range N := r@Range{step := s};