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

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

6f495d1Aaron Craelius11 years ago

.travis.yml+1

compare with master

unifiedsplit

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

107 echo "make -j2 $test";

108 make -j2 $test;

109 done

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

benchmarks/fasta/fasta.idr+9−10

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

1module Main

3import System

4−import Data.Floats

6alu : String

5alu : String

7alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

6alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

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

9 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

8 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

10 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

9 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

12−iub : List (Char, Float)

11+iub : List (Char, Double)

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

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

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

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

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

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

17−homosapiens : List (Char, Float)

16+homosapiens : List (Char, Double)

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

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

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

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

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

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

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

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

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

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

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

34 where

33 where

35 go "" = return ()

34 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

38replicate : Int -> Char -> String

37replicate : Int -> Char -> String

39replicate 0 c = ""

38replicate 0 c = ""

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

44 [] => []

43 [] => []

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

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

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

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

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

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

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

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

51make name n0 tbl seed0 = do

50make name n0 tbl seed0 = do

52 putStrLn name

51 putStrLn name

53 make' n0 0 seed0 ""

52 make' n0 0 seed0 ""

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

55 modulus : Int

54 modulus : Int

56 modulus = 139968

55 modulus = 139968

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

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

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

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

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

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

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

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

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

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

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

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

66 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

69 make' n col seed buf = do

68 make' n col seed buf = do

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

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

71 let nextchar = strIndex lookupTable newseed

70 let nextchar = strIndex lookupTable newseed

72 let newbuf = buf <+> singleton nextchar

71 let newbuf = buf <+> singleton nextchar

73 if col+1 >= 60

72 if col+1 >= 60

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

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

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

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

benchmarks/pidigits/pidigits.idr+10−10

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

1import System

2+import Data.Vect

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

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

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

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

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

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

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

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

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

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.

12 It almost runs in constant space.

13 It almost runs in constant space.

13-}

14-}

15−data F = mkF Integer Integer Integer

16+data F = MkF Integer Integer Integer

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

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

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

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

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

23 loop k (S k') xs

24 loop k (S k') xs

25fn : Integer -> F

26fn : Integer -> F

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

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

28flr : Integer -> F -> Integer

29flr : 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

31comp : F -> F -> F

32comp : 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)

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

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

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

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

36str _ _ Z = Nil

37str _ _ Z = Nil

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

38str 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

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

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

40 where y = flr 3 z

41 where y = flr 3 z

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

43pidigit = do

44pidigit = do

44 [_,a] <- getArgs

45 [_,a] <- getArgs

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

46 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

47 loop 10 0 l

48 loop 10 0 l

48 return ()

49 return ()

50main : IO ()

51main : IO ()

51main = pidigit

52main = pidigit

52−

benchmarks/quasigroups/Main.idr+14−11

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

10 case args of

11 [_, path] => do

12 f <- readFile path

13+ case f of

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

15+ Right f' =>

13− case parse f of

16+ case parse f' of

14− Left err => putStrLn err

17+ Left err => putStrLn err

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

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

16− putStrLn "Got board:"

19+ putStrLn "Got board:"

17− printLn board

20+ printLn board

18− putStrLn "Solving..."

21+ putStrLn "Solving..."

19− case fillBoard board legal of

22+ case fillBoard board legal of

20− Nothing => putStrLn "No solution found"

23+ Nothing => putStrLn "No solution found"

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

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

22− putStrLn "Solution found:"

25+ putStrLn "Solution found:"

23− printLn solved

26+ printLn solved

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

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

benchmarks/quasigroups/Parser.idr+3−2

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

1module Parser

3import Decidable.Equality

4+import Data.Vect

5import Solver

6import Solver

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

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

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

62 step i l =

63 step i l =

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

64 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

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

66 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)

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

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

69 helper FZ l = step FZ l

70 helper FZ l = step FZ l

benchmarks/quasigroups/Solver.idr+3−2

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

3import Decidable.Equality

4import Control.Monad.State

5+import Data.Vect

5import Data.Vect.Quantifiers

6import Data.Vect.Quantifiers

7%default total

8%default total

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

95 case colSafe b x v of

96 case colSafe b x v of

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

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

97 Yes prf' =>

98 Yes prf' =>

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

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

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

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

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

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

101

102

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

194

195

195 %assert_total

196 %assert_total

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

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

197− recurse start =

198+ recurse start =

198 case tryAll start of

199 case tryAll start of

199 (_, Nothing) => Nothing

200 (_, Nothing) => Nothing

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

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

benchmarks/trivial/sortvec.idr+4−3

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

1module Main

3import System

4+import Effects

4import Effect.Random

5import Effect.Random

6+import Data.Vect

6total

8total

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

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

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

12vsort [] = []

14vsort [] = []

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

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

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

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

16mkSortVec Z = return []

18mkSortVec Z = return []

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

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

19main : IO ()

21main : IO ()

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

22main = 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)))

23 putStrLn "Made vector"

24 putStrLn "Made vector"

24 printLn (vsort vec)

25 printLn (vsort vec)

docs/tutorial/typesfuns.rst+6−4

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

149

150.. note::

151

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

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

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

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

154+ 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+ is actually ``(S (S (S (S Z))))``

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

155− checked at the Idris prompt:

157+ This can be checked at the Idris prompt:

156

158

157::

159::

158

160

libs/base/Data/String.idr+1

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

1module Data.String

2+%access public

3private

4private

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

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

libs/base/System.idr+1−1

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

56exit : Int -> IO ()

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

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

60time : IO Integer

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

62 return t

src/Idris/Prover.hs+13−15

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

156 iputGoal rendered

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

158 let OK ty = goalAtFocus ps

159− let OK env = envAtFocus ps

159+ OK env = envAtFocus ps

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

160+ state = prettyOtherGoals hs <> line <>

161 prettyAssumptions inElab ty env <> line <>

162 prettyMetaValues (reverse menv) <>

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

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

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

216

217 prettyAssumptions inElab g env =

218− if length env == 0 then

218+ if null env then empty

219− empty

220 else

219 else

221 text "---------- Assumptions: ----------" <>

220 text "---------- Assumptions: ----------" <>

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

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

223

222

224 prettyOtherGoals hs =

223 prettyOtherGoals hs =

225− if length hs == 0 then

224+ if null hs then empty

226− empty

227 else

225 else

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

226 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)

230

228

231 freeEnvNames :: Env -> [Name]

229 freeEnvNames :: Env -> [Name]

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

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

233

231

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

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

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

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

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

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

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

248 Left err -> ierror err

246 Left err -> ierror err

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

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

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

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

251 case IdeMode.sexpToCommand sexp of

249 case IdeMode.sexpToCommand sexp of

252 Just (IdeMode.REPLCompletions prefix) ->

250 Just (IdeMode.REPLCompletions prefix) ->

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

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

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

309 Success (Left cmd') ->

307 Success (Left cmd') ->

310 case cmd' of

308 case cmd' of

311 EQED -> do hs <- lifte e get_holes

309 EQED -> do hs <- lifte e get_holes

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

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

313 iputStrLn "Proof completed!"

311 iputStrLn "Proof completed!"

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

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

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

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

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

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

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

334 Success (Right cmd') ->

332 Success (Right cmd') ->

335 case cmd' of

333 case cmd' of

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

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

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

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

338 DoLet fc i ifc Placeholder expr ->

336 DoLet fc i ifc Placeholder expr ->

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

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

340 ctxt <- getContext

338 ctxt <- getContext

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

380 else do ok

378 else do ok

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

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

382

380

383− where

381+ where

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

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

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

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

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

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

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

412 return (i, h)

410 return (i, h)

413 (cmd, step) <- case x of

411 (cmd, step) <- case x of

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

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

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

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

416 case cmd of

414 case cmd of

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

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

418 _ -> return ()

416 _ -> return ()

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

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

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

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

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

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

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

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

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

430 iputStrLn "Proof completed!"

428 iputStrLn "Proof completed!"

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

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

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

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