From 4860d2b75186f9572ee05efcdd0da1e48193c55e Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 11 Jul 2019 23:38:25 +0200 Subject: [PATCH] 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 | 6 -- libs/prelude/Prelude.idr | 83 ++++++++++++++++++++++++++++ src/Idris/Desugar.idr | 17 ++++++ src/Idris/Parser.idr | 2 +- src/Idris/Syntax.idr | 12 ++++ src/Parser/Support.idr | 13 +++++ tests/idris2/total006/expected | 2 +- tests/typedd-book/chapter12/expected | 1 + tests/typedd-book/chapter12/run | 2 +- 9 files changed, 129 insertions(+), 9 deletions(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index aa46802..5d220e0 100644 --- a/libs/base/Data/Nat.idr +++ b/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 diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index afe4508..7e199a1 100644 --- a/libs/prelude/Prelude.idr +++ b/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)) + diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 3924cb9..6dccf57 100644 --- a/src/Idris/Desugar.idr +++ b/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} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index b4f5d54..c0bd435 100644 --- a/src/Idris/Parser.idr +++ b/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" diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 590d3eb..36406ef 100644 --- a/src/Idris/Syntax.idr +++ b/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 diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index 0a19002..64e6dfc 100644 --- a/src/Parser/Support.idr +++ b/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 diff --git a/tests/idris2/total006/expected b/tests/idris2/total006/expected index b92c2bf..dce1e70 100644 --- a/tests/idris2/total006/expected +++ b/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 diff --git a/tests/typedd-book/chapter12/expected b/tests/typedd-book/chapter12/expected index e13b4ea..243b67d 100644 --- a/tests/typedd-book/chapter12/expected +++ b/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) diff --git a/tests/typedd-book/chapter12/run b/tests/typedd-book/chapter12/run index af8927b..7800af2 100755 --- a/tests/typedd-book/chapter12/run +++ b/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