Fin.restrict fix (#4337)
* Explicitly pass bounds to `Fin.fromInteger` from `Fin.restrict`
commita6037b914391d63c1951805c309db899eeda69d0
authorTrevon Sutton <trevon.sutton.dev@gmail.com>
dateSun 18 Feb 2018, 10:50 (9 years ago)
parent6d7fd7b
libs/base/Data/Fin.idr+1−1
@@ -135,7 +135,7 @@ restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
135135 -- reasoning about primitives, so we need the
136136 -- 'believe_me'. It's fine because val' must be
137137 -- in the right range
138− fromInteger val'
138+ fromInteger {n = S n} val'
139139 {prf = believe_me {a=IsJust (Just val')} ItIsJust}
140140
141141%language ErrorReflection
test/TestData.hs+2−1
@@ -76,7 +76,8 @@ testFamiliesData = [
7676 ( 22, NODE_CG ),
7777 ( 23, ANY ),
7878 ( 24, ANY ),
79− ( 25, ANY )]),
79+ ( 25, ANY ),
80+ ( 26, ANY )]),
8081 ("bignum", "Bignum",
8182 [ ( 1, ANY ),
8283 ( 2, ANY )]),
test/basic026/basic026.idrnew file+12
@@ -0,0 +1,12 @@
1+module Main
2+
3+import Data.Vect
4+
5+||| Verifies that `Fin.restrict` generates a valid `Fin`
6+||| by using it to index a `Vect`.
7+main : IO ()
8+main = do
9+ let xs = the (Vect 2 Char) ['a','b']
10+ printLn $ Vect.index (restrict 1 0) xs == 'a'
11+ printLn $ Vect.index (restrict 1 1) xs == 'b'
12+
test/basic026/expectednew file+2
@@ -0,0 +1,2 @@
1+True
2+True
test/basic026/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ basic026.idr -o basic026
3+./basic026
4+rm -f basic026 *.ibc