git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical
commitb5dd4020a0faca7d274a235ea16956a1b71ea40a authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 20 Apr 2015, 15:08 (12 years ago) parent3047ae80ed16d7
16 files changed+111−55
compare with master
unifiedsplit
idris.cabal+7 libs/contrib/Control/Partial.idr+14 libs/contrib/Data/String.idr+31 libs/contrib/contrib.ipkg+2−1 libs/prelude/Builtins.idr+2−1 src/Idris/Core/Binary.hs+3−3 src/Idris/DataOpts.hs+6 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Term.hs+34−17 src/Idris/Elab/Transform.hs+1−1 test/bignum002/bignum002.idr+5 test/bignum002/expected+1 test/bignum002/run+4 test/folding002/expected−2 test/folding002/folding002.idr−25 test/folding002/run−4
idris.cabal+7
@@ -349,6 +349,9 @@ Extra-source-files:
349349 test/bignum001/run
350350 test/bignum001/*.idr
351351 test/bignum001/expected
352+ test/bignum002/run
353+ test/bignum002/*.idr
354+ test/bignum002/expected
352355
353356 test/delab001/*.idr
354357 test/delab001/run
@@ -421,6 +424,10 @@ Extra-source-files:
421424 test/ffi006/run
422425 test/ffi006/expected
423426
427+ test/folding001/*.idr
428+ test/folding001/run
429+ test/folding001/expected
430+
424431 test/idrisdoc001/run
425432 test/idrisdoc001/expected
426433 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
33opts = "--nobasepkgs --total -i ../prelude -i ../base"
44modules = Control.Algebra,
55 Control.Isomorphism.Primitives,
6+ Control.Partial,
67 Control.WellFounded,
78 Classes.Verified,
8− Data.Fun, Data.Rel,
9+ Data.Fun, Data.Rel,
910 Data.Hash, Data.Matrix,
1011 Data.Nat,
1112 Data.ZZ, Data.Sign,
libs/prelude/Builtins.idr+2−1
@@ -36,7 +36,8 @@ namespace Builtins
3636 ||| it. Another way to see dependent pairs is as just data - for instance, the
3737 ||| length of a vector paired with that vector.
3838 |||
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
4041 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
4142 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
4243
src/Idris/Core/Binary.hs+3−3
@@ -6,7 +6,7 @@ module Idris.Core.Binary where
66import Data.Binary
77import Data.Vector.Binary
88import qualified Data.Text as T
9−
9+import qualified Data.Text.Encoding as E
1010import Idris.Core.TT
1111
1212instance Binary ErrorReportPart where
@@ -267,9 +267,9 @@ instance Binary Name where
267267 _ -> error "Corrupted binary data for Name"
268268
269269instance Binary T.Text where
270− put x = put (str x)
270+ put x = put (E.encodeUtf8 x)
271271 get = do x <- get
272− return (txt x)
272+ return (E.decodeUtf8 x)
273273
274274instance Binary SpecialName where
275275 put x
src/Idris/DataOpts.hs+6
@@ -63,6 +63,12 @@ instance Optimisable (TT Name) where
6363 applyOpts (P _ (NS (UN fn) mod) _)
6464 | fn == txt "mult" && mod == prel
6565 = 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)
6672 applyOpts (App _ (P _ (NS (UN fn) mod) _) x)
6773 | fn == txt "fromIntegerNat" && mod == prel
6874 = 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
626626 aux <- getAux
627627 mapM_ (elabCaseHole (case_decls aux)) hs
628628 tt <- get_term
629− let (tm, ds) = runState (collectDeferred (Just fname) tt) []
629+ let (tm, ds) = runState (collectDeferred (Just fname) ctxt tt) []
630630 probs <- get_probs
631631 return (tm, ds, is, probs, ctxt', newDecls))
632632 setContext ctxt'
src/Idris/Elab/Term.hs+34−17
@@ -112,9 +112,9 @@ build ist info emode opts fn tm
112112 update_term orderPats)
113113 EState is _ impls <- getAux
114114 tt <- get_term
115− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
116− log <- getLog
117115 ctxt <- get_context
116+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []
117+ log <- getLog
118118 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
119119 else return (ElabResult tm ds is ctxt impls)
120120 where pattern = emode == ELHS
@@ -154,9 +154,9 @@ buildTC ist info emode opts fn tm
154154 lift (Error (CantMatch (getInferTerm tm)))
155155 EState is _ impls <- getAux
156156 tt <- get_term
157− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
158− log <- getLog
159157 ctxt <- get_context
158+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []
159+ log <- getLog
160160 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
161161 else return (ElabResult tm ds is ctxt impls)
162162 where pattern = emode == ELHS
@@ -1547,23 +1547,40 @@ resTC' tcs defaultOn topholes depth topg fn ist
15471547 where isImp (PImp p _ _ _ _) = (True, p)
15481548 isImp arg = (False, priority arg)
15491549
1550−collectDeferred :: Maybe Name ->
1550+collectDeferred :: Maybe Name -> Context ->
15511551 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) =
15531553 do ds <- get
1554− t' <- collectDeferred top t
1555− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
1556− collectDeferred top app
1557−collectDeferred top (Bind n b t) = do b' <- cdb b
1558− t' <- collectDeferred top t
1559− return (Bind n b' t')
1554+ t' <- collectDeferred top ctxt t
1555+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
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+
1574+collectDeferred top ctxt (Bind n b t) = do b' <- cdb b
1575+ t' <- collectDeferred top ctxt t
1576+ return (Bind n b' t')
15601577 where
1561− cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
1562− cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
1563− cdb b = do ty' <- collectDeferred top (binderTy b)
1578+ cdb (Let t v) = liftM2 Let (collectDeferred top ctxt t) (collectDeferred top ctxt v)
1579+ cdb (Guess t v) = liftM2 Guess (collectDeferred top ctxt t) (collectDeferred top ctxt v)
1580+ cdb b = do ty' <- collectDeferred top ctxt (binderTy b)
15641581 return (b { binderTy = ty' })
1565−collectDeferred top (App s f a) = liftM2 (App s) (collectDeferred top f) (collectDeferred top a)
1566−collectDeferred top t = return t
1582+collectDeferred top ctxt (App s f a) = liftM2 (App s) (collectDeferred top ctxt f) (collectDeferred top ctxt a)
1583+collectDeferred top ctxt t = return t
15671584
15681585case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
15691586case_ 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
7575 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
7676 erun fc $ psolve lhs_tm
7777 tt <- get_term
78− let (rhs', defer) = runState (collectDeferred Nothing tt) []
78+ let (rhs', defer) = runState (collectDeferred Nothing ctxt tt) []
7979 return (rhs', defer, ctxt', newDecls))
8080 setContext ctxt'
8181 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