idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-27 13:40:15 +03:00
Code Issues Projects Releases Wiki Activity

[ fix ] natToFinLt is O(n) (#2689)

Browse Source
This commit is contained in:
Stefan Höck 2022-09-29 15:36:32 +02:00 committed by GitHub
parent 1402194f14
commit 7eebeff905
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 43 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libs/base/Data/Fin.idr
View File

@ -184,11 +184,10 @@ natToFinLT Z {prf = LTESucc _} = FZ
natToFinLT (S k) {prf = LTESucc _} = FS $ natToFinLT k
public export
natToFinLt : (x : Nat) -> {n : Nat} ->
natToFinLt : (x : Nat) -> {0 n : Nat} ->
{auto 0 prf : So (x < n)} ->
Fin n
natToFinLt Z {n = S _} = FZ
natToFinLt (S k) {n = S _} = FS $ natToFinLt k
natToFinLt x = let 0 p := ltOpReflectsLT x n prf in natToFinLT x
public export
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

8
libs/base/Data/Nat.idr
View File

@ -1,5 +1,6 @@
module Data.Nat
import Data.So
import public Control.Relation
import public Control.Ord
import public Control.Order
@ -267,6 +268,13 @@ export
ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n === True -> k `LT` n
ltReflectsLT k n prf = lteReflectsLTE (S k) n prf
public export
ltOpReflectsLT : (m,n : Nat) -> So (m < n) -> LT m n
ltOpReflectsLT 0 (S k) prf = LTESucc LTEZero
ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
ltOpReflectsLT (S k) 0 prf impossible
ltOpReflectsLT 0 0 prf impossible
export
gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n === True -> k `GT` n
gtReflectsGT k n prf = ltReflectsLT n k prf

1
tests/Main.idr
View File

@ -295,6 +295,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez)
, "memo"
, "newints"
, "integers"
, "nat2fin"
, "semaphores001"
, "semaphores002"
, "perf001"

18
tests/chez/nat2fin/Check.idr Normal file
View File

@ -0,0 +1,18 @@
import Data.List
import Data.String
import System.File
path : String
path = "build/exec/test_app/test.ss"
mainLine : String -> Bool
mainLine str =
("(define Main-main(" `isPrefixOf` str) && (" 375))))" `isInfixOf` str)
main : IO ()
main = do
Right str <- readFile path
| Left err => putStrLn "Error when reading \{path}"
case any mainLine (lines str) of
True => putStrLn "natToFinLt optimized away"
False => putStrLn "failed to optimize away natToFinLt"

4
tests/chez/nat2fin/Test.idr Normal file
View File

@ -0,0 +1,4 @@
import Data.Fin
main : IO ()
main = printLn (the (Fin 1000) 375)

3
tests/chez/nat2fin/expected Normal file
View File

@ -0,0 +1,3 @@
1/1: Building Check (Check.idr)
Main> natToFinLt optimized away
Main> Bye for now!

2
tests/chez/nat2fin/input Normal file
View File

@ -0,0 +1,2 @@
:exec main
:q

5
tests/chez/nat2fin/run Normal file
View File

@ -0,0 +1,5 @@
rm -rf build
$1 --no-banner --no-color --quiet -o test Test.idr
$1 --no-banner --no-color --console-width 0 Check.idr < input