b5dd402 · Idris-dev · git.iko.soy

idris.cabal+7

compare with master

unifiedsplit

@@ -349,6 +349,9 @@ Extra-source-files:

349 test/bignum001/run

350 test/bignum001/*.idr

351 test/bignum001/expected

352+ test/bignum002/run

353+ test/bignum002/*.idr

354+ test/bignum002/expected

352

355

353 test/delab001/*.idr

356 test/delab001/*.idr

354 test/delab001/run

357 test/delab001/run

@@ -421,6 +424,10 @@ Extra-source-files:

421 test/ffi006/run

424 test/ffi006/run

422 test/ffi006/expected

425 test/ffi006/expected

423

426

427+ test/folding001/*.idr

428+ test/folding001/run

429+ test/folding001/expected

430+

424 test/idrisdoc001/run

431 test/idrisdoc001/run

425 test/idrisdoc001/expected

432 test/idrisdoc001/expected

426 test/idrisdoc001/*.idr

433 test/idrisdoc001/*.idr

libs/contrib/Control/Partial.idrnew file+14

@@ -0,0 +1,14 @@

1+||| Control structures that are fundamentally partial

2+module Control.Partial

3+

4+

5+||| Repeatedly apply `f` to `v` until `p` is `True`.

6+|||

7+||| @ p the predicate to wait for

8+||| @ f the function to repeatedly apply

9+||| @ v the starting value

10+partial

11+until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a

12+until p f v with (p v)

13+ | False = until p f (f v)

14+ | True = v

libs/contrib/Data/String.idrnew file+31

@@ -0,0 +1,31 @@

1+module Data.String

2+

3+infixl 5 +>

4+infixr 5 <+

5+

6+||| Adds a character to the end of the specified string.

7+|||

8+||| ```idris example

9+||| strSnoc "AB" 'C'

10+||| ```

11+||| ```idris example

12+||| strSnoc "" 'A'

13+||| ```

14+strSnoc : String -> Char -> String

15+strSnoc s c = s ++ (singleton 'c')

16+

17+||| Alias of `strSnoc`

18+|||

19+||| ```idris example

20+||| "AB" +> 'C'

21+||| ```

22+(+>) : String -> Char -> String

23+(+>) = strSnoc

24+

25+||| Alias of `strCons`

26+|||

27+||| ```idris example

28+||| 'A' <+ "AB"

29+||| ```

30+(<+) : Char -> String -> String

31+(<+) = strCons

libs/contrib/contrib.ipkg+2−1

@@ -3,9 +3,10 @@ package contrib

3opts = "--nobasepkgs --total -i ../prelude -i ../base"

4modules = Control.Algebra,

5 Control.Isomorphism.Primitives,

6+ Control.Partial,

6 Control.WellFounded,

7 Control.WellFounded,

7 Classes.Verified,

8 Classes.Verified,

8− Data.Fun, Data.Rel,

9+ Data.Fun, Data.Rel,

9 Data.Hash, Data.Matrix,

10 Data.Hash, Data.Matrix,

10 Data.Nat,

11 Data.Nat,

11 Data.ZZ, Data.Sign,

12 Data.ZZ, Data.Sign,

libs/prelude/Builtins.idr+2−1

@@ -36,7 +36,8 @@ namespace Builtins

36 ||| it. Another way to see dependent pairs is as just data - for instance, the

37 ||| length of a vector paired with that vector.

38 |||

39− ||| @ a the type of the witness @ P the type of the proof

39+ ||| @ a the type of the witness

40+ ||| @ P the type of the proof

40 data Sigma : (a : Type) -> (P : a -> Type) -> Type where

41 data Sigma : (a : Type) -> (P : a -> Type) -> Type where

41 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

42 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

42

43

src/Idris/Core/Binary.hs+3−3

@@ -6,7 +6,7 @@ module Idris.Core.Binary where

6import Data.Binary

7import Data.Vector.Binary

8import qualified Data.Text as T

9−

9+import qualified Data.Text.Encoding as E

10import Idris.Core.TT

11

12instance Binary ErrorReportPart where

@@ -267,9 +267,9 @@ instance Binary Name where

267 _ -> error "Corrupted binary data for Name"

268

269instance Binary T.Text where

270− put x = put (str x)

270+ put x = put (E.encodeUtf8 x)

271 get = do x <- get

272− return (txt x)

272+ return (E.decodeUtf8 x)

273

274instance Binary SpecialName where

275 put x

src/Idris/DataOpts.hs+6

@@ -63,6 +63,12 @@ instance Optimisable (TT Name) where

63 applyOpts (P _ (NS (UN fn) mod) _)

64 | fn == txt "mult" && mod == prel

65 = return (P Ref (sUN "prim__mulBigInt") Erased)

66+ applyOpts (P _ (NS (UN fn) mod) _)

67+ | fn == txt "divNat" && mod == prel

68+ = return (P Ref (sUN "prim__sdivBigInt") Erased)

69+ applyOpts (P _ (NS (UN fn) mod) _)

70+ | fn == txt "modNat" && mod == prel

71+ = return (P Ref (sUN "prim__sremBigInt") Erased)

66 applyOpts (App _ (P _ (NS (UN fn) mod) _) x)

72 applyOpts (App _ (P _ (NS (UN fn) mod) _) x)

67 | fn == txt "fromIntegerNat" && mod == prel

73 | fn == txt "fromIntegerNat" && mod == prel

68 = applyOpts x

74 = applyOpts x

src/Idris/Elab/Clause.hs+1−1

@@ -626,7 +626,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

626 aux <- getAux

627 mapM_ (elabCaseHole (case_decls aux)) hs

628 tt <- get_term

629− let (tm, ds) = runState (collectDeferred (Just fname) tt) []

629+ let (tm, ds) = runState (collectDeferred (Just fname) ctxt tt) []

630 probs <- get_probs

631 return (tm, ds, is, probs, ctxt', newDecls))

632 setContext ctxt'

src/Idris/Elab/Term.hs+34−17

@@ -112,9 +112,9 @@ build ist info emode opts fn tm

112 update_term orderPats)

113 EState is _ impls <- getAux

114 tt <- get_term

115− let (tm, ds) = runState (collectDeferred (Just fn) tt) []

116− log <- getLog

117 ctxt <- get_context

115 ctxt <- get_context

116+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []

117+ log <- getLog

118 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

119 else return (ElabResult tm ds is ctxt impls)

120 where pattern = emode == ELHS

@@ -154,9 +154,9 @@ buildTC ist info emode opts fn tm

154 lift (Error (CantMatch (getInferTerm tm)))

155 EState is _ impls <- getAux

156 tt <- get_term

157− let (tm, ds) = runState (collectDeferred (Just fn) tt) []

158− log <- getLog

159 ctxt <- get_context

157 ctxt <- get_context

158+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []

159+ log <- getLog

160 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

161 else return (ElabResult tm ds is ctxt impls)

162 where pattern = emode == ELHS

@@ -1547,23 +1547,40 @@ resTC' tcs defaultOn topholes depth topg fn ist

1547 where isImp (PImp p _ _ _ _) = (True, p)

1548 isImp arg = (False, priority arg)

1549

1550−collectDeferred :: Maybe Name ->

1550+collectDeferred :: Maybe Name -> Context ->

1551 Term -> State [(Name, (Int, Maybe Name, Type))] Term

1552−collectDeferred top (Bind n (GHole i t) app) =

1552+collectDeferred top ctxt (Bind n (GHole i t) app) =

1553 do ds <- get

1554− t' <- collectDeferred top t

1554+ t' <- collectDeferred top ctxt t

1555− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])

1555+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])

1556− collectDeferred top app

1556+ collectDeferred top ctxt app

1557+ where

1558+ -- Evaluate the top level functions in arguments, if possible, so that

1559+ -- any immediate specialisation of the function applied to constructors

1560+ -- can be done

1561+ tidyArg env (Bind n b@(Pi im t k) sc)

1562+ = Bind n (Pi im (tidy ctxt env t) k)

1563+ (tidyArg ((n, b) : env) sc)

1564+ tidyArg env t = t

1565+

1566+ tidy ctxt env t | (f, args) <- unApply t,

1567+ P _ n _ <- getFn f

1568+ = fst $ specialise ctxt env [(n, 99999)] t

1569+ tidy ctxt env t = t

1570+

1571+ getFn (Bind n (Lam _) t) = getFn t

1572+ getFn t | (f, a) <- unApply t = f

1573+

1557−collectDeferred top (Bind n b t) = do b' <- cdb b

1574+collectDeferred top ctxt (Bind n b t) = do b' <- cdb b

1558− t' <- collectDeferred top t

1575+ t' <- collectDeferred top ctxt t

1559− return (Bind n b' t')

1576+ return (Bind n b' t')

1560 where

1577 where

1561− cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)

1578+ cdb (Let t v) = liftM2 Let (collectDeferred top ctxt t) (collectDeferred top ctxt v)

1562− cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

1579+ cdb (Guess t v) = liftM2 Guess (collectDeferred top ctxt t) (collectDeferred top ctxt v)

1563− cdb b = do ty' <- collectDeferred top (binderTy b)

1580+ cdb b = do ty' <- collectDeferred top ctxt (binderTy b)

1564 return (b { binderTy = ty' })

1581 return (b { binderTy = ty' })

1565−collectDeferred top (App s f a) = liftM2 (App s) (collectDeferred top f) (collectDeferred top a)

1582+collectDeferred top ctxt (App s f a) = liftM2 (App s) (collectDeferred top ctxt f) (collectDeferred top ctxt a)

1566−collectDeferred top t = return t

1583+collectDeferred top ctxt t = return t

1567

1584

1568case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1585case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1569case_ ind autoSolve ist fn tm = do

1586case_ ind autoSolve ist fn tm = do

src/Idris/Elab/Transform.hs+1−1

@@ -75,7 +75,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

75 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

76 erun fc $ psolve lhs_tm

77 tt <- get_term

78− let (rhs', defer) = runState (collectDeferred Nothing tt) []

78+ let (rhs', defer) = runState (collectDeferred Nothing ctxt tt) []

79 return (rhs', defer, ctxt', newDecls))

80 setContext ctxt'

81 processTacticDecls info newDecls

test/bignum002/bignum002.idrnew file+5

@@ -0,0 +1,5 @@

1+module Main

2+

3+main : IO ()

4+main = do

5+ putStrLn $ show $ divNat 1809022195644390369852458 91238741987

test/bignum002/expectednew file+1

@@ -0,0 +1 @@

1+19827346982734

test/bignum002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ bignum002.idr -o bignum002

3+./bignum002

4+rm -f bignum002 *.ibc

test/folding002/expecteddeleted−2

@@ -1,2 +0,0 @@

1−5000050000

2−5000050000

test/folding002/folding002.idrdeleted−25

@@ -1,25 +0,0 @@

1−import Data.Vect

2−

3−-- perform a very large foldr to test tail recursion

4−addAll : (Foldable t, Num a) => t a -> a

5−addAll = foldr (+) 0

6−

7−n : Integer

8−n = 100000

9−

10−numbersList : List Integer

11−numbersList = numbersList' n []

12− where

13− numbersList' : Integer -> List Integer -> List Integer

14− numbersList' 0 xs = xs

15− numbersList' k xs = numbersList' (k - 1) (fromInteger k :: xs)

16−

17−numbersVect : Vect (length numbersList) Integer

18−numbersVect = fromList numbersList

19−

20−main : IO ()

21−main = do

22− putStrLn . show . addAll $ numbersVect

23− putStrLn . show . addAll $ numbersList

24−

25−

test/folding002/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

2−idris $@ folding002.idr -o folding002

3−./folding002

4−rm -f folding002 *.ibc