Add Range interface to prelude

This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.

libs/base/Data/Nat.idr

@@ -31,12 +31,6 @@ isItSucc : (n : Nat) -> Dec (IsSucc n)
 isItSucc Z = No absurd
 isItSucc (S n) = Yes ItIsSucc
 
-public export
-minus : Nat -> Nat -> Nat
-minus Z        right     = Z
-minus left     Z         = left
-minus (S left) (S right) = minus left right
-
 public export
 power : Nat -> Nat -> Nat
 power base Z       = S Z

libs/prelude/Prelude.idr

@@ -574,6 +574,12 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
+public export
+minus : Nat -> Nat -> Nat
+minus Z        right     = Z
+minus left     Z         = left
+minus (S left) (S right) = minus left right
+
 public export
 mult : Nat -> Nat -> Nat
 mult Z y = Z
@@ -1298,3 +1304,80 @@ export
 Cast Nat Double where
   cast = prim__cast_IntegerDouble . natToInteger
 
+------------
+-- RANGES --
+------------
+
+countFrom : n -> (n -> n) -> Stream n
+countFrom start diff = start :: countFrom (diff start) diff
+
+partial
+takeUntil : (n -> Bool) -> Stream n -> List n
+takeUntil p (x :: xs)
+    = if p x
+         then [x]
+         else x :: takeUntil p xs
+
+partial
+takeBefore : (n -> Bool) -> Stream n -> List n
+takeBefore p (x :: xs)
+    = if p x
+         then []
+         else x :: takeBefore p xs
+
+public export 
+interface Range a where
+  rangeFromTo : a -> a -> List a
+  rangeFromThenTo : a -> a -> a -> List a
+
+  rangeFrom : a -> Stream a
+  rangeFromThen : a -> a -> Stream a
+
+-- Idris 1 went to great lengths to prove that these were total. I don't really
+-- think it's worth going to those lengths! Let's keep it simple and assert.
+export
+Range Nat where
+  rangeFromTo x y 
+      = if y > x
+           then assert_total $ takeUntil (>= y) (countFrom x S)
+           else if x > y
+                   then assert_total $ takeUntil (<= y) (countFrom x (\n => minus n 1))
+                   else [x]
+  rangeFromThenTo x y z 
+      = if y > x
+           then (if z > x
+                    then assert_total $ takeBefore (> z) (countFrom x (plus (minus y x)))
+                    else [])
+           else (if x == y 
+                    then (if x == z then [x] else [])
+                    else assert_total $ takeBefore (< z) (countFrom x (\n => minus n (minus x y))))
+  rangeFrom x = countFrom x S
+  rangeFromThen x y 
+      = if y > x 
+           then countFrom x (plus (minus y x))
+           else countFrom x (\n => minus n (minus x y))
+           
+export
+(Integral a, Ord a, Neg a) => Range a where
+  rangeFromTo x y 
+      = if y > x
+           then assert_total $ takeUntil (>= y) (countFrom x (+1))
+           else if x > y
+                   then assert_total $ takeUntil (<= y) (countFrom x (\x => x-1))
+                   else [x]
+  rangeFromThenTo x y z 
+      = if (z - x) > (z - y)
+           then -- go up
+             assert_total $ takeBefore (> z) (countFrom x (+ (y-x)))
+           else if (z - x) < (z - y)
+                then -- go down
+                     assert_total $ takeBefore (< z) (countFrom x (\n => n - (x - y)))
+                else -- meaningless
+                  if x == y && y == z
+                     then [x] else []
+  rangeFrom x = countFrom x (1+)
+  rangeFromThen x y 
+      = if y > x 
+           then countFrom x (+ (y - x))
+           else countFrom x (\n => n - (x - y))
+

src/Idris/Desugar.idr

@@ -270,6 +270,23 @@ mutual
       toPure tm = DoExp fc (PApp fc (PRef fc (UN "pure")) tm)
   desugar side ps (PRewrite fc rule tm)
       = pure $ IRewrite fc !(desugar side ps rule) !(desugar side ps tm)
+  desugar side ps (PRange fc start next end)
+      = case next of
+             Nothing =>
+                desugar side ps (PApp fc 
+                                    (PApp fc (PRef fc (UN "rangeFromTo"))
+                                          start) end)
+             Just n =>
+                desugar side ps (PApp fc 
+                                    (PApp fc 
+                                        (PApp fc (PRef fc (UN "rangeFromThenTo"))
+                                              start) n) end)
+  desugar side ps (PRangeStream fc start next)
+      = case next of
+             Nothing =>
+                desugar side ps (PApp fc (PRef fc (UN "rangeFrom")) start)
+             Just n =>
+                desugar side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
 
   desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                   {auto c : Ref Ctxt Defs} ->

src/Idris/Parser.idr

@@ -823,7 +823,7 @@ dataOpt
 dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm -> 
            EmptyRule PDataDecl
 dataBody fname mincol start n indents ty
-    = do atEnd indents
+    = do atEndIndent indents
          end <- location
          pure (MkPLater (MkFC fname start end) n ty)
   <|> do keyword "where"

src/Idris/Syntax.idr

@@ -82,6 +82,10 @@ mutual
        PIfThenElse : FC -> PTerm -> PTerm -> PTerm -> PTerm
        PComprehension : FC -> PTerm -> List PDo -> PTerm
        PRewrite : FC -> PTerm -> PTerm -> PTerm
+       -- A list range  [x,y..z]
+       PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm
+       -- A stream range [x,y..]
+       PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
 
        -- TODO: Ranges, idiom brackets (?), 
        -- 'with' disambiguation
@@ -425,6 +429,14 @@ mutual
         deGuard tm = tm
     show (PRewrite _ rule tm)
         = "rewrite " ++ show rule ++ " in " ++ show tm
+    show (PRange _ start Nothing end)
+        = "[" ++ show start ++ " .. " ++ show end ++ "]"
+    show (PRange _ start (Just next) end)
+        = "[" ++ show start ++ ", " ++ show next ++ " .. " ++ show end ++ "]"
+    show (PRangeStream _ start Nothing)
+        = "[" ++ show start ++ " .. ]"
+    show (PRangeStream _ start (Just next))
+        = "[" ++ show start ++ ", " ++ show next ++ " .. ]"
 
 public export
 record IFaceInfo where

src/Parser/Support.idr

@@ -360,6 +360,7 @@ init = 0
 continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
 continueF err indent
     = do eoi; err
+  <|> do keyword "where"; err
   <|> do col <- column
          if (col <= indent)
             then err
@@ -409,6 +410,7 @@ isTerminator (Symbol "}") = True
 isTerminator (Symbol ")") = True
 isTerminator (Symbol "|") = True
 isTerminator (Keyword "in") = True
+isTerminator (Keyword "where") = True
 isTerminator EndInput = True
 isTerminator _ = False
 
@@ -427,6 +429,17 @@ atEnd indent
             then pure ()
             else fail "Not the end of a block entry"
 
+-- Check we're at the end, but only by looking at indentation
+export
+atEndIndent : (indent : IndentInfo) -> EmptyRule ()
+atEndIndent indent
+    = eoi
+  <|> do col <- column
+         if (col <= indent)
+            then pure ()
+            else fail "Not the end of a block entry"
+
+
 -- Parse a terminator, return where the next block entry
 -- must start, given where the current block entry started
 terminator : ValidIndent -> Int -> EmptyRule ValidIndent

tests/idris2/total006/expected

@@ -1,7 +1,7 @@
 1/1: Building Total (Total.idr)
 Welcome to Idris 2 version 0.0. Enjoy yourself!
 Main> Main.count is total
-Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:810:1--814:1 -> Prelude.map
+Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:816:1--820:1 -> Prelude.map
 Main> Main.process is total
 Main> Main.badProcess is not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
 Main> Main.doubleInt is total

tests/typedd-book/chapter12/expected

@@ -1,5 +1,6 @@
 1/1: Building ArithState (ArithState.idr)
 1/1: Building DataStore (DataStore.idr)
 1/1: Building Record (Record.idr)
+1/1: Building State (State.idr)
 1/1: Building StateMonad (StateMonad.idr)
 1/1: Building Traverse (Traverse.idr)

tests/typedd-book/chapter12/run

@@ -1,7 +1,7 @@
 $1 ArithState.idr --check
 $1 DataStore.idr --check
 $1 Record.idr --check
-# $1 State.idr --check
+$1 State.idr --check
 $1 StateMonad.idr --check
 $1 Traverse.idr --check
 # $1 TreeLabel.idr --check