6f495d1 · Idris-dev · git.iko.soy

.travis.yml+1

@@ -107,3 +107,4 @@ script:

107107 echo "make -j2 $test";

108108 make -j2 $test;

109109 done

110+ - cd benchmarks && ./build.pl && ./run.pl && cd ..

benchmarks/fasta/fasta.idr+9−10

@@ -1,7 +1,6 @@

11module Main

22

33import System

4−import Data.Floats

54

65alu : String

76alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

@@ -9,12 +8,12 @@ alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

98 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

109 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

1110

12−iub : List (Char, Float)

11+iub : List (Char, Double)

1312iub = [('a',0.27),('c',0.12),('g',0.12),('t',0.27),('B',0.02)

1413 ,('D',0.02),('H',0.02),('K',0.02),('M',0.02),('N',0.02)

1514 ,('R',0.02),('S',0.02),('V',0.02),('W',0.02),('Y',0.02)]

1615

17−homosapiens : List (Char, Float)

16+homosapiens : List (Char, Double)

1817homosapiens = [('a',0.3029549426680),('c',0.1979883004921)

1918 ,('g',0.1975473066391),('t',0.3015094502008)]

2019

@@ -30,10 +29,10 @@ splitAt' : Nat -> String -> (String, String)

3029splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')

3130

3231writeAlu : String -> String -> IO ()

33−writeAlu name s0 = putStrLn name $> go s0

32+writeAlu name s0 = putStrLn name *> go s0

3433 where

3534 go "" = return ()

36− go s = let (h,t) = splitAt' 60 s in putStrLn h $> go t

35+ go s = let (h,t) = splitAt' 60 s in putStrLn h *> go t

3736

3837replicate : Int -> Char -> String

3938replicate 0 c = ""

@@ -44,10 +43,10 @@ scanl f q ls = q :: (case ls of

4443 [] => []

4544 x::xs => scanl f (f q x) xs)

4645

47−accum : (Char,Float) -> (Char,Float) -> (Char,Float)

46+accum : (Char,Double) -> (Char,Double) -> (Char,Double)

4847accum (_,p) (c,q) = (c,p+q)

4948

50−make : String -> Int -> List (Char, Float) -> Int -> IO Int

49+make : String -> Int -> List (Char, Double) -> Int -> IO Int

5150make name n0 tbl seed0 = do

5251 putStrLn name

5352 make' n0 0 seed0 ""

@@ -55,7 +54,7 @@ make name n0 tbl seed0 = do

5554 modulus : Int

5655 modulus = 139968

5756

58− fill : List (Char,Float) -> Int -> List String

57+ fill : List (Char,Double) -> Int -> List String

5958 fill ((c,p) :: cps) j =

6059 let k = min modulus (cast (cast modulus * p + 1))

6160 in replicate (k - j) c :: fill cps k

@@ -65,13 +64,13 @@ make name n0 tbl seed0 = do

6564 lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)

6665

6766 make' : Int -> Int -> Int -> String -> IO Int

68− make' 0 col seed buf = when (col > 0) (putStrLn buf) $> return seed

67+ make' 0 col seed buf = when (col > 0) (putStrLn buf) *> return seed

6968 make' n col seed buf = do

7069 let newseed = modInt (seed * 3877 + 29573) modulus

7170 let nextchar = strIndex lookupTable newseed

7271 let newbuf = buf <+> singleton nextchar

7372 if col+1 >= 60

74− then putStrLn newbuf $> make' (n-1) 0 newseed ""

73+ then putStrLn newbuf *> make' (n-1) 0 newseed ""

7574 else make' (n-1) (col+1) newseed newbuf

7675

7776

benchmarks/pidigits/pidigits.idr+10−10

@@ -1,18 +1,19 @@

11import System

2+import Data.Vect

23

34{- Toy program that outputs the n first digits of Pi.

45

5− Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

6+ Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

67 The original ns and str lazy lists have been replaced by strict functions.

78

8− Memory usage seems to be excessive. One of the branches of str is tail recursive, and

9+ Memory usage seems to be excessive. One of the branches of str is tail recursive, and

910 the other one only needs to cons an extra Integer.

1011

11− For reference, the Haskell version runs in 0m0.230s when printing to /dev/null.

12+ For reference, the Haskell version runs in 0m0.230s when printing to /dev/null.

1213 It almost runs in constant space.

1314-}

1415

15−data F = mkF Integer Integer Integer

16+data F = MkF Integer Integer Integer

1617

1718-- Prints the list of digits by groups of 10

1819loop : Nat -> Nat -> List Integer -> IO()

@@ -23,19 +24,19 @@ loop (S k) k' (x::xs) = do putStr (show x)

2324 loop k (S k') xs

2425

2526fn : Integer -> F

26−fn k = mkF k (4*k+2) (2*k+1)

27+fn k = MkF k (4*k+2) (2*k+1)

2728

2829flr : Integer -> F -> Integer

29−flr x (mkF q r t) = (q*x + r) `div` t

30+flr x (MkF q r t) = (q*x + r) `div` t

3031

3132comp : F -> F -> F

32−comp (mkF q r t) (mkF u v x) = mkF (q*u) (q*v+r*x) (t*x)

33+comp (MkF q r t) (MkF u v x) = MkF (q*u) (q*v+r*x) (t*x)

3334

3435-- Returns the list of digits of pi. Memory hungry.

3536str : F -> Integer -> Nat -> List Integer

3637str _ _ Z = Nil

3738str z k (S n) = if(y == flr 4 z)

38− then y :: str (comp (mkF 10 (-10*y) 1) z ) k n

39+ then y :: str (comp (MkF 10 (-10*y) 1) z ) k n

3940 else str (comp z (fn k)) (k+1) (S n)

4041 where y = flr 3 z

4142

@@ -43,10 +44,9 @@ pidigit : IO()

4344pidigit = do

4445 [_,a] <- getArgs

4546 let n = fromIntegerNat (the Integer (cast a))

46− let l = str (mkF 1 0 1) 1 n

47+ let l = str (MkF 1 0 1) 1 n

4748 loop 10 0 l

4849 return ()

4950

5051main : IO ()

5152main = pidigit

52−

benchmarks/quasigroups/Main.idr+14−11

@@ -10,15 +10,18 @@ main = do

1010 case args of

1111 [_, path] => do

1212 f <- readFile path

13− case parse f of

14− Left err => putStrLn err

15− Right (_ ** (board ** legal)) => do

16− putStrLn "Got board:"

17− printLn board

18− putStrLn "Solving..."

19− case fillBoard board legal of

20− Nothing => putStrLn "No solution found"

21− Just (solved ** _) => do

22− putStrLn "Solution found:"

23− printLn solved

13+ case f of

14+ Left _err => putStrLn $ "Error reading file: " ++ path

15+ Right f' =>

16+ case parse f' of

17+ Left err => putStrLn err

18+ Right (_ ** (board ** legal)) => do

19+ putStrLn "Got board:"

20+ printLn board

21+ putStrLn "Solving..."

22+ case fillBoard board legal of

23+ Nothing => putStrLn "No solution found"

24+ Just (solved ** _) => do

25+ putStrLn "Solution found:"

26+ printLn solved

2427 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

benchmarks/quasigroups/Parser.idr+3−2

@@ -1,6 +1,7 @@

11module Parser

22

33import Decidable.Equality

4+import Data.Vect

45

56import Solver

67

@@ -61,9 +62,9 @@ parseRows {n=S k} _ l rs = helper last l

6162 step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

6263 step i l =

6364 let cs = fromList (words (index i rs)) in

64− case decEq (length cs) (S k) of

65+ case decEq (Parser.length cs) (S k) of

6566 No _ => Left "Row length not equal to column height"

66− Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed

67+ Yes prf => parseCols i l (replace {P=\n => Vect n String} prf cs)

6768

6869 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

6970 helper FZ l = step FZ l

benchmarks/quasigroups/Solver.idr+3−2

@@ -2,6 +2,7 @@ module Solver

22

33import Decidable.Equality

44import Control.Monad.State

5+import Data.Vect

56import Data.Vect.Quantifiers

67

78%default total

@@ -95,7 +96,7 @@ legalVal b (x, y) v =

9596 case colSafe b x v of

9697 No prf' => No (\(_, cf, _) => prf' cf)

9798 Yes prf' =>

98− case empty (getCell b (x, y)) of

99+ case Solver.empty (getCell b (x, y)) of

99100 No prf'' => No (\(ef, _, _) => prf'' ef)

100101 Yes prf'' => Yes (prf'', prf', prf)

101102

@@ -194,7 +195,7 @@ fillBoard {n=(S n)} b l with (emptyCell b)

194195

195196 %assert_total

196197 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197− recurse start =

198+ recurse start =

198199 case tryAll start of

199200 (_, Nothing) => Nothing

200201 (FZ, Just (b' ** l')) => fillBoard b' l'

benchmarks/trivial/sortvec.idr+4−3

@@ -1,7 +1,9 @@

11module Main

22

33import System

4+import Effects

45import Effect.Random

6+import Data.Vect

57

68total

79insert : Ord a => a -> Vect n a -> Vect (S n) a

@@ -12,13 +14,12 @@ vsort : Ord a => Vect n a -> Vect n a

1214vsort [] = []

1315vsort (x :: xs) = insert x (vsort xs)

1416

15−mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)

17+mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]

1618mkSortVec Z = return []

1719mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

1820

1921main : IO ()

2022main = do (_ :: arg :: _) <- getArgs

21−-- let arg = "2000"

22− let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

23+ let vec = runPure $ (srand 123456789 *> mkSortVec (fromInteger (cast arg)))

2324 putStrLn "Made vector"

2425 printLn (vsort vec)

docs/tutorial/typesfuns.rst+6−4

@@ -149,10 +149,12 @@ Idris prompt:

149149

150150.. note::

151151

152− Idris automatically desugars the ``Nat`` representation into a

153− more human readable format. The result of ``plus (S (S Z)) (S (S Z))``

154− is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be

155− checked at the Idris prompt:

152+ When displaying an element of ``Nat`` such as ``(S (S (S (S Z))))``,

153+ Idris displays it as ``4``.

154+ The result of ``plus (S (S Z)) (S (S Z))``

155+ is actually ``(S (S (S (S Z))))``

156+ which is the natural number ``4``.

157+ This can be checked at the Idris prompt:

156158

157159::

158160

libs/base/Data/String.idr+1

@@ -1,4 +1,5 @@

11module Data.String

2+%access public

23

34private

45parseNumWithoutSign : List Char -> Integer -> Maybe Integer

libs/base/System.idr+1−1

@@ -56,7 +56,7 @@ getEnvironment = getAllPairs 0 []

5656exit : Int -> IO ()

5757exit code = foreign FFI_C "exit" (Int -> IO ()) code

5858

59−||| Get the numbers of sections since 1st January 1970, 00:00 UTC

59+||| Get the numbers of seconds since 1st January 1970, 00:00 UTC

6060time : IO Integer

6161time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))

6262 return t

src/Idris/Prover.hs+13−15

@@ -156,8 +156,8 @@ dumpState ist inElab menv ps | [] <- holes ps =

156156 iputGoal rendered

157157dumpState ist inElab menv ps | (h : hs) <- holes ps = do

158158 let OK ty = goalAtFocus ps

159− let OK env = envAtFocus ps

160− let state = prettyOtherGoals hs <> line <>

159+ OK env = envAtFocus ps

160+ state = prettyOtherGoals hs <> line <>

161161 prettyAssumptions inElab ty env <> line <>

162162 prettyMetaValues (reverse menv) <>

163163 prettyGoal (zip (assumptionNames env) (repeat False)) ty

@@ -215,21 +215,19 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

215215 bindingOf h False <+> colon <+> align (prettyG bnd ty)

216216

217217 prettyAssumptions inElab g env =

218− if length env == 0 then

219− empty

218+ if null env then empty

220219 else

221220 text "---------- Assumptions: ----------" <>

222221 nest nestingSize (prettyPs inElab g [] $ reverse env)

223222

224223 prettyOtherGoals hs =

225− if length hs == 0 then

226− empty

224+ if null hs then empty

227225 else

228226 text "---------- Other goals: ----------" <$$>

229− nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

227+ nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)

230228

231229 freeEnvNames :: Env -> [Name]

232− freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))

230+ freeEnvNames = concatMap (\(n, b) -> freeNames (Bind n b Erased))

233231

234232lifte :: ElabState EState -> ElabD a -> Idris a

235233lifte st e = do (v, _) <- elabStep st e

@@ -247,7 +245,7 @@ receiveInput h e =

247245 (sexp, id) <- case IdeMode.parseMessage l of

248246 Left err -> ierror err

249247 Right (sexp, id) -> return (sexp, id)

250− putIState $ i { idris_outputmode = (IdeMode id h) }

248+ putIState $ i { idris_outputmode = IdeMode id h }

251249 case IdeMode.sexpToCommand sexp of

252250 Just (IdeMode.REPLCompletions prefix) ->

253251 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

@@ -309,7 +307,7 @@ elabloop fn d prompt prf e prev h env

309307 Success (Left cmd') ->

310308 case cmd' of

311309 EQED -> do hs <- lifte e get_holes

312− when (not (null hs)) $ ifail "Incomplete proof"

310+ unless (null hs) $ ifail "Incomplete proof"

313311 iputStrLn "Proof completed!"

314312 return (False, prev, e, True, prf, env, Right $ iPrintResult "")

315313 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev

@@ -333,8 +331,8 @@ elabloop fn d prompt prf e prev h env

333331 return (d', prev, st', done, prf', env, go)

334332 Success (Right cmd') ->

335333 case cmd' of

336− DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"

337− DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"

334+ DoLetP {} -> ifail "Pattern-matching let not supported here"

335+ DoBindP {} -> ifail "Pattern-matching <- not supported here"

338336 DoLet fc i ifc Placeholder expr ->

339337 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

340338 ctxt <- getContext

@@ -380,7 +378,7 @@ elabloop fn d prompt prf e prev h env

380378 else do ok

381379 elabloop fn d prompt prf' st prev' h' env'

382380

383− where

381+ where

384382 -- A bit of a hack: wrap the value up in a let binding, which will

385383 -- normalise away. It would be better to figure out how to call

386384 -- the elaborator with a custom environment here to avoid the

@@ -412,7 +410,7 @@ ploop fn d prompt prf e h

412410 return (i, h)

413411 (cmd, step) <- case x of

414412 Nothing -> do iPrintError ""; ifail "Abandoned"

415− Just input -> do return (parseTactic i input, input)

413+ Just input -> return (parseTactic i input, input)

416414 case cmd of

417415 Success Abandon -> do iPrintError ""; ifail "Abandoned"

418416 _ -> return ()

@@ -426,7 +424,7 @@ ploop fn d prompt prf e h

426424 iputStrLn $ "TT: " ++ show tm ++ "\n"

427425 return (False, e, False, prf, Right $ iPrintResult "")

428426 Success Qed -> do hs <- lifte e get_holes

429− when (not (null hs)) $ ifail "Incomplete proof"

427+ unless (null hs) $ ifail "Incomplete proof"

430428 iputStrLn "Proof completed!"

431429 return (False, e, True, prf, Right $ iPrintResult "")

432430 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n