git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev into liftDecls_js_backend
cb4f9e6Rui Barreiro
README.md+1−3
compare with master
unifiedsplit
@@ -28,9 +28,7 @@ Idris has support for external code generators. Supplied with the distribution
28is a C code generator to compile executables, and a JavaScript code generator
28is a C code generator to compile executables, and a JavaScript code generator
29with support for node.js and browser JavaScript.
29with support for node.js and browser JavaScript.
30
30
31−At this moment in time there are two external repositories with a
31+More information about [code generators can be found on the wiki](http://idris.readthedocs.io/en/latest/reference/codegen.html).
32−[Java code generator](https://github.com/idris-hackers/idris-java) and an
33−[LLVM-based code generator](https://github.com/idris-hackers/idris-llvm).
34
32
35## More Information
33## More Information
36
34
idris.cabal+1−1
@@ -358,7 +358,7 @@ Executable idris
358 , transformers
358 , transformers
359
359
360 ghc-prof-options: -auto-all -caf-all
360 ghc-prof-options: -auto-all -caf-all
361− ghc-options: -threaded -rtsopts -funbox-strict-fields
361+ ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
362
362
363Test-suite regression-and-feature-tests
363Test-suite regression-and-feature-tests
364 Type: exitcode-stdio-1.0
364 Type: exitcode-stdio-1.0
libs/contrib/Control/Algebra/NumericImplementations.idr+26−6
@@ -9,6 +9,8 @@ import Data.ZZ
9
9
10%access public export
10%access public export
11
11
12+-- Integer
13+
12Semigroup Integer where
14Semigroup Integer where
13 (<+>) = (+)
15 (<+>) = (+)
14
16
@@ -18,7 +20,7 @@ Monoid Integer where
18Group Integer where
20Group Integer where
19 inverse = (* -1)
21 inverse = (* -1)
20
22
21−AbelianGroup Integer where
23+AbelianGroup Integer where
22
24
23Ring Integer where
25Ring Integer where
24 (<.>) = (*)
26 (<.>) = (*)
@@ -26,6 +28,7 @@ Ring Integer where
26RingWithUnity Integer where
28RingWithUnity Integer where
27 unity = 1
29 unity = 1
28
30
31+-- Int
29
32
30Semigroup Int where
33Semigroup Int where
31 (<+>) = (+)
34 (<+>) = (+)
@@ -44,6 +47,7 @@ Ring Int where
44RingWithUnity Int where
47RingWithUnity Int where
45 unity = 1
48 unity = 1
46
49
50+-- Double
47
51
48Semigroup Double where
52Semigroup Double where
49 (<+>) = (+)
53 (<+>) = (+)
@@ -65,30 +69,46 @@ RingWithUnity Double where
65Field Double where
69Field Double where
66 inverseM f _ = 1 / f
70 inverseM f _ = 1 / f
67
71
72+-- Nat
68
73
69−Semigroup Nat where
74+[PlusNatSemi] Semigroup Nat where
70 (<+>) = (+)
75 (<+>) = (+)
71
76
72−Monoid Nat where
77+[PlusNatMonoid] Monoid Nat using PlusNatSemi where
73 neutral = 0
78 neutral = 0
74
79
80+[MultNatSemi] Semigroup Nat where
81+ (<+>) = (*)
82+
83+[MultNatMonoid] Monoid Nat using MultNatSemi where
84+ neutral = 1
85+
86+-- ZZ
87+
75−Semigroup ZZ where
88+[PlusZZSemi] Semigroup ZZ where
76 (<+>) = (+)
89 (<+>) = (+)
77
90
78−Monoid ZZ where
91+[PlusZZMonoid] Monoid ZZ using PlusZZSemi where
79 neutral = 0
92 neutral = 0
80
93
81−Group ZZ where
94+Group ZZ using PlusZZMonoid where
82 inverse = (* -1)
95 inverse = (* -1)
83
96
84AbelianGroup ZZ where
97AbelianGroup ZZ where
85
98
99+[MultZZSemi] Semigroup ZZ where
100+ (<+>) = (*)
101+
102+[MultZZMonoid] Monoid ZZ using MultZZSemi where
103+ neutral = 1
104+
86Ring ZZ where
105Ring ZZ where
87 (<.>) = (*)
106 (<.>) = (*)
88
107
89RingWithUnity ZZ where
108RingWithUnity ZZ where
90 unity = 1
109 unity = 1
91
110
111+-- Complex
92
112
93Semigroup a => Semigroup (Complex a) where
113Semigroup a => Semigroup (Complex a) where
94 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
114 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
libs/contrib/Control/ST.idr+3−5
@@ -593,15 +593,13 @@ runLoop fuel prog onEmpty
593||| responsibility of an implementation of an interface in IO which uses it
593||| responsibility of an implementation of an interface in IO which uses it
594||| to ensure that it isn't duplicated.
594||| to ensure that it isn't duplicated.
595export
595export
596−runWith : {resf : _} ->
597− Env res -> STrans IO a res (\result => resf result) ->
596+runWith : Env res -> STrans IO a res resf ->
598 IO (result ** Env (resf result))
597 IO (result ** Env (resf result))
599runWith env prog = runST env prog (\res, env' => pure (res ** env'))
598runWith env prog = runST env prog (\res, env' => pure (res ** env'))
600
599
601export
600export
602−runWithLoop : {resf : _} ->
603− Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
601+runWithLoop : Env res -> Fuel -> STransLoop IO a res resf ->
604− IO (Maybe (result ** Env (resf result)))
602+ IO (Maybe (result ** Env (resf result)))
605runWithLoop env fuel prog
603runWithLoop env fuel prog
606 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
604 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
607 (pure Nothing)
605 (pure Nothing)
libs/contrib/Data/SortedMap.idr+2−2
@@ -238,10 +238,10 @@ toList (M _ t) = treeToList t
238treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
238treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239treeMap f (Leaf k v) = Leaf k (f v)
239treeMap f (Leaf k v) = Leaf k (f v)
240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
241−treeMap f (Branch3 t1 k1 t2 k2 t3)
241+treeMap f (Branch3 t1 k1 t2 k2 t3)
242 = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
242 = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
243
243
244+export
244implementation Functor (SortedMap k) where
245implementation Functor (SortedMap k) where
245 map _ Empty = Empty
246 map _ Empty = Empty
246 map f (M n t) = M _ (treeMap f t)
247 map f (M n t) = M _ (treeMap f t)
247−
libs/contrib/Data/SortedSet.idr+27−3
@@ -2,8 +2,6 @@ module Data.SortedSet
2
2
3import Data.SortedMap
3import Data.SortedMap
4
4
5−-- TODO: add intersection, union, difference
6−
7export
5export
8data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
6data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
9
7
@@ -31,5 +29,31 @@ export
31toList : SortedSet k -> List k
29toList : SortedSet k -> List k
32toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
30toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
33
31
34−implementation Foldable SortedSet where
32+Foldable SortedSet where
35 foldr f e xs = foldr f e (Data.SortedSet.toList xs)
33 foldr f e xs = foldr f e (Data.SortedSet.toList xs)
34+
35+||| Set union. Inserts all elements of x into y
36+export
37+union : (x, y : SortedSet k) -> SortedSet k
38+union x y = foldr insert x y
39+
40+||| Set difference. Delete all elments in y from x
41+export
42+difference : (x, y : SortedSet k) -> SortedSet k
43+difference x y = foldr delete x y
44+
45+||| Set symmetric difference. Uses the union of the differences.
46+export
47+symDifference : (x, y : SortedSet k) -> SortedSet k
48+symDifference x y = union (difference x y) (difference y x)
49+
50+||| Set intersection. Implemented as the difference of the union and the symetric difference.
51+export
52+intersection : (x, y : SortedSet k) -> SortedSet k
53+intersection x y = difference x (difference x y)
54+
55+Ord k => Semigroup (SortedSet k) where
56+ (<+>) = union
57+
58+Ord k => Monoid (SortedSet k) where
59+ neutral = empty
libs/contrib/Interfaces/Verified.idr+81−37
@@ -2,7 +2,9 @@ module Interfaces.Verified
2
2
3import Control.Algebra
3import Control.Algebra
4import Control.Algebra.Lattice
4import Control.Algebra.Lattice
5+import Control.Algebra.NumericImplementations
5import Control.Algebra.VectorSpace
6import Control.Algebra.VectorSpace
7+import Data.ZZ
6
8
7%access public export
9%access public export
8
10
@@ -19,6 +21,12 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
19 (g1 : a -> b) -> (g2 : b -> c) ->
21 (g1 : a -> b) -> (g2 : b -> c) ->
20 map (g2 . g1) x = (map g2 . map g1) x
22 map (g2 . g1) x = (map g2 . map g1) x
21
23
24+VerifiedFunctor Maybe where
25+ functorIdentity Nothing = Refl
26+ functorIdentity (Just x) = Refl
27+ functorComposition Nothing g1 g2 = Refl
28+ functorComposition (Just x) g1 g2 = Refl
29+
22interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
30interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
23 applicativeMap : (x : f a) -> (g : a -> b) ->
31 applicativeMap : (x : f a) -> (g : a -> b) ->
24 map g x = pure g <*> x
32 map g x = pure g <*> x
@@ -30,6 +38,23 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
38 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
31 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
39 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
32
40
41+VerifiedApplicative Maybe where
42+ applicativeMap Nothing g = Refl
43+ applicativeMap (Just x) g = Refl
44+ applicativeIdentity Nothing = Refl
45+ applicativeIdentity (Just x) = Refl
46+ applicativeComposition Nothing Nothing Nothing = Refl
47+ applicativeComposition Nothing Nothing (Just x) = Refl
48+ applicativeComposition Nothing (Just x) Nothing = Refl
49+ applicativeComposition Nothing (Just x) (Just y) = Refl
50+ applicativeComposition (Just x) Nothing Nothing = Refl
51+ applicativeComposition (Just x) Nothing (Just y) = Refl
52+ applicativeComposition (Just x) (Just y) Nothing = Refl
53+ applicativeComposition (Just x) (Just y) (Just z) = Refl
54+ applicativeHomomorphism x g = Refl
55+ applicativeInterchange x Nothing = Refl
56+ applicativeInterchange x (Just y) = Refl
57+
33interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
58interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
34 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
59 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
35 mf <*> mx = mf >>= \f =>
60 mf <*> mx = mf >>= \f =>
@@ -40,6 +65,16 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
40 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
65 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
41 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
66 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
42
67
68+VerifiedMonad Maybe where
69+ monadApplicative Nothing Nothing = Refl
70+ monadApplicative Nothing (Just x) = Refl
71+ monadApplicative (Just x) Nothing = Refl
72+ monadApplicative (Just x) (Just y) = Refl
73+ monadLeftIdentity x f = Refl
74+ monadRightIdentity Nothing = Refl
75+ monadRightIdentity (Just x) = Refl
76+ monadAssociativity Nothing f g = Refl
77+ monadAssociativity (Just x) f g = Refl
43
78
44interface Semigroup a => VerifiedSemigroup a where
79interface Semigroup a => VerifiedSemigroup a where
45 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
80 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -47,17 +82,37 @@ interface Semigroup a => VerifiedSemigroup a where
47implementation VerifiedSemigroup (List a) where
82implementation VerifiedSemigroup (List a) where
48 semigroupOpIsAssociative = appendAssociative
83 semigroupOpIsAssociative = appendAssociative
49
84
50−--implementation VerifiedSemigroup Nat where
85+[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
51−-- semigroupOpIsAssociative = plusAssociative
86+ semigroupOpIsAssociative = plusAssociative
87+
88+[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
89+ semigroupOpIsAssociative = multAssociative
52
90
91+[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
92+ semigroupOpIsAssociative = plusAssociativeZ
93+
94+[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
95+ semigroupOpIsAssociative = multAssociativeZ
53
96
54interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
97interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
55 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
98 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
56 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
99 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
57
100
58−-- implementation VerifiedMonoid Nat where
101+[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
59−-- monoidNeutralIsNeutralL = plusZeroRightNeutral
102+ monoidNeutralIsNeutralL = plusZeroRightNeutral
60−-- monoidNeutralIsNeutralR = plusZeroLeftNeutral
103+ monoidNeutralIsNeutralR = plusZeroLeftNeutral
104+
105+[MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where
106+ monoidNeutralIsNeutralL = multOneRightNeutral
107+ monoidNeutralIsNeutralR = multOneLeftNeutral
108+
109+[PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where
110+ monoidNeutralIsNeutralL = plusZeroRightNeutralZ
111+ monoidNeutralIsNeutralR = plusZeroLeftNeutralZ
112+
113+[MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where
114+ monoidNeutralIsNeutralL = multOneRightNeutralZ
115+ monoidNeutralIsNeutralR = multOneLeftNeutralZ
61
116
62implementation VerifiedMonoid (List a) where
117implementation VerifiedMonoid (List a) where
63 monoidNeutralIsNeutralL = appendNilRightNeutral
118 monoidNeutralIsNeutralL = appendNilRightNeutral
@@ -67,22 +122,39 @@ interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
67 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
122 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
68 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
123 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
69
124
125+VerifiedGroup ZZ using PlusZZMonoidV where
126+ groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
127+ rewrite multNegLeftZ 0 k in
128+ rewrite multOneLeftNeutralZ k in
129+ plusNegateInverseLZ k
130+ groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
131+ rewrite multNegLeftZ 0 k in
132+ rewrite multOneLeftNeutralZ k in
133+ plusNegateInverseRZ k
134+
70interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
135interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
71 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
136 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
72
137
138+VerifiedAbelianGroup ZZ where
139+ abelianGroupOpIsCommutative = plusCommutativeZ
140+
73interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
141interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
74 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
142 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
75 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
143 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
76 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
144 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
77
145
146+VerifiedRing ZZ where
147+ ringOpIsAssociative = multAssociativeZ
148+ ringOpIsDistributiveL = multDistributesOverPlusRightZ
149+ ringOpIsDistributiveR = multDistributesOverPlusLeftZ
150+
78interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
151interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
79 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
152 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
80 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
153 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
81
154
82−--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
155+VerifiedRingWithUnity ZZ where
83−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity
156+ ringWithUnityIsUnityL = multOneRightNeutralZ
84−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity
157+ ringWithUnityIsUnityR = multOneLeftNeutralZ
85−
86
158
87interface JoinSemilattice a => VerifiedJoinSemilattice a where
159interface JoinSemilattice a => VerifiedJoinSemilattice a where
88 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
160 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
@@ -93,31 +165,3 @@ interface MeetSemilattice a => VerifiedMeetSemilattice a where
93 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
165 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
94 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
166 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
95 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
167 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
96−
97−{- FIXME: Some maintenance required here.
98− Algebra.top and Algebra.bottom don't exist!
99−-}
100−{-
101−
102−interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
103− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e
104−
105−interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
106− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e
107−
108−interface (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
109− total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
110− total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
111−
112−interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
113−
114−
115−--interface (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
116−-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
117−-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v
118−-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
119−-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
120−
121−--interface (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
122−
123−-}
libs/contrib/Network/Socket.idr+1
@@ -10,6 +10,7 @@ import Network.Socket.Raw
10%include C "idris_net.h"
10%include C "idris_net.h"
11%include C "sys/types.h"
11%include C "sys/types.h"
12%include C "sys/socket.h"
12%include C "sys/socket.h"
13+%include C "unistd.h"
13%include C "netdb.h"
14%include C "netdb.h"
14
15
15%access export
16%access export
libs/contrib/contrib.ipkg+1
@@ -8,6 +8,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
8 Control.Algebra.NumericImplementations,
8 Control.Algebra.NumericImplementations,
9 Control.Isomorphism.Primitives,
9 Control.Isomorphism.Primitives,
10 Control.Partial,
10 Control.Partial,
11+ Control.Pipeline,
11 Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
12 Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
12
13
13 Interfaces.Verified,
14 Interfaces.Verified,
src/IRTS/System.hs+4−3
@@ -30,7 +30,8 @@ import Control.Applicative ((<$>))
30import Data.List.Split
30import Data.List.Split
31import Data.Maybe (fromMaybe)
31import Data.Maybe (fromMaybe)
32import System.Environment
32import System.Environment
33−import System.FilePath (addTrailingPathSeparator, (</>))
33+import System.FilePath (addTrailingPathSeparator, dropTrailingPathSeparator,
34+ (</>))
34
35
35
36
36getIdrisDataDir :: IO String
37getIdrisDataDir :: IO String
@@ -81,7 +82,7 @@ gmpLib = []
81#endif
82#endif
82
83
83getLibFlags = do dir <- getIdrisCRTSDir
84getLibFlags = do dir <- getIdrisCRTSDir
84− return $ ["-L" ++ dir,
85+ return $ ["-L" ++ dropTrailingPathSeparator dir,
85 "-lidris_rts"] ++ extraLib ++ gmpLib ++ ["-lpthread"]
86 "-lidris_rts"] ++ extraLib ++ gmpLib ++ ["-lpthread"]
86
87
87getIdrisLibDir = addTrailingPathSeparator <$> overrideIdrisSubDirWith "libs" "IDRIS_LIBRARY_PATH"
88getIdrisLibDir = addTrailingPathSeparator <$> overrideIdrisSubDirWith "libs" "IDRIS_LIBRARY_PATH"
@@ -97,4 +98,4 @@ getIdrisCRTSDir = do
97 return $ addTrailingPathSeparator (ddir </> "rts")
98 return $ addTrailingPathSeparator (ddir </> "rts")
98
99
99getIncFlags = do dir <- getIdrisCRTSDir
100getIncFlags = do dir <- getIdrisCRTSDir
100− return $ ("-I" ++ dir) : extraInclude
101+ return $ ("-I" ++ dropTrailingPathSeparator dir) : extraInclude
src/Idris/Coverage.hs+29−12
@@ -410,31 +410,43 @@ recoverableCoverage _ _ = False
410-- with
410-- with
411checkRec :: Term -> Term -> State [(Name, Term)] Bool
411checkRec :: Term -> Term -> State [(Name, Term)] Bool
412checkRec (P Bound x _) tm
412checkRec (P Bound x _) tm
413− | (P yt _ _, _) <- unApply tm,
414− conType yt = do nmap <- get
413+ | isCon tm = do nmap <- get
415− case lookup x nmap of
414+ case lookup x nmap of
416− Nothing -> do put ((x, tm) : nmap)
415+ Nothing -> do put ((x, tm) : nmap)
417− return True
416+ return True
418− Just y' -> checkRec tm y'
417+ Just y' -> checkRec tm y'
419 where
418 where
419+ isCon tm
420+ | (P yt _ _, _) <- unApply tm,
421+ conType yt = True
422+ isCon (Constant _) = True
423+ isCon _ = False
424+
420 conType (DCon _ _ _) = True
425 conType (DCon _ _ _) = True
421 conType (TCon _ _) = True
426 conType (TCon _ _) = True
422 conType _ = False
427 conType _ = False
423
428
424checkRec tm (P Bound y _)
429checkRec tm (P Bound y _)
425− | (P xt _ _, _) <- unApply tm,
426− conType xt = do nmap <- get
430+ | isCon tm = do nmap <- get
427− case lookup y nmap of
431+ case lookup y nmap of
428− Nothing -> do put ((y, tm) : nmap)
432+ Nothing -> do put ((y, tm) : nmap)
429− return True
433+ return True
430− Just x' -> checkRec tm x'
434+ Just x' -> checkRec tm x'
431 where
435 where
436+ isCon tm
437+ | (P yt _ _, _) <- unApply tm,
438+ conType yt = True
439+ isCon (Constant _) = True
440+ isCon _ = False
441+
432 conType (DCon _ _ _) = True
442 conType (DCon _ _ _) = True
433 conType (TCon _ _) = True
443 conType (TCon _ _) = True
434 conType _ = False
444 conType _ = False
435
445
436checkRec (App _ f a) p@(P _ _ _) = checkRec f p
446checkRec (App _ f a) p@(P _ _ _) = checkRec f p
447+checkRec (App _ f a) p@(Constant _) = checkRec f p
437checkRec p@(P _ _ _) (App _ f a) = checkRec p f
448checkRec p@(P _ _ _) (App _ f a) = checkRec p f
449+checkRec p@(Constant _) (App _ f a) = checkRec p f
438checkRec fa@(App _ _ _) fa'@(App _ _ _)
450checkRec fa@(App _ _ _) fa'@(App _ _ _)
439 | (f, as) <- unApply fa,
451 | (f, as) <- unApply fa,
440 (f', as') <- unApply fa'
452 (f', as') <- unApply fa'
@@ -454,6 +466,7 @@ checkRec fa@(App _ _ _) fa'@(App _ _ _)
454 return (aok && asok)
466 return (aok && asok)
455 conType (P (DCon _ _ _) _ _) = True
467 conType (P (DCon _ _ _) _ _) = True
456 conType (P (TCon _ _) _ _) = True
468 conType (P (TCon _ _) _ _) = True
469+ conType (Constant _) = True
457 conType _ = False
470 conType _ = False
458
471
459checkRec (P xt x _) (P yt y _)
472checkRec (P xt x _) (P yt y _)
@@ -469,4 +482,8 @@ checkRec (P xt x _) (P yt y _)
469 | Bound <- x = True
482 | Bound <- x = True
470 | Bound <- y = True
483 | Bound <- y = True
471 | otherwise = False -- name is different, unrecoverable
484 | otherwise = False -- name is different, unrecoverable
485+-- A function reference against a constant might be recoverable if we get to
486+-- reduce the function
487+checkRec (P Ref _ _) (Constant _) = return True
488+checkRec (Constant _) (P Ref _ _) = return True
472checkRec _ _ = return False
489checkRec _ _ = return False
src/Idris/Elab/Clause.hs+1−1
@@ -836,7 +836,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
836
836
837 let rhs' = rhsElab
837 let rhs' = rhsElab
838
838
839− when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
839+ when (not (null defer)) $ logElab 2 $ "DEFERRED " ++
840 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
840 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
841
841
842 -- If there's holes, set the metavariables as undefinable
842 -- If there's holes, set the metavariables as undefinable
src/Idris/IBC.hs+12−12
@@ -223,7 +223,7 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch
223writeIBC :: FilePath -> FilePath -> Idris ()
223writeIBC :: FilePath -> FilePath -> Idris ()
224writeIBC src f
224writeIBC src f
225 = do
225 = do
226− logIBC 1 $ "Writing IBC for: " ++ show f
226+ logIBC 2 $ "Writing IBC for: " ++ show f
227 iReport 2 $ "Writing IBC for: " ++ show f
227 iReport 2 $ "Writing IBC for: " ++ show f
228 i <- getIState
228 i <- getIState
229-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
229-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
@@ -233,8 +233,8 @@ writeIBC src f
233 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
233 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
234 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
234 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
235 writeArchive f ibcf
235 writeArchive f ibcf
236− logIBC 1 "Written")
236+ logIBC 2 "Written")
237− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
237+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
238 return ()
238 return ()
239
239
240-- | Write a package index containing all the imports in the current
240-- | Write a package index containing all the imports in the current
@@ -244,14 +244,14 @@ writePkgIndex :: FilePath -> Idris ()
244writePkgIndex f
244writePkgIndex f
245 = do i <- getIState
245 = do i <- getIState
246 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
246 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
247− logIBC 1 $ "Writing package index " ++ show f ++ " including\n" ++
247+ logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++
248 show (map snd imps)
248 show (map snd imps)
249 resetNameIdx
249 resetNameIdx
250 let ibcf = initIBC { ibc_imports = imps }
250 let ibcf = initIBC { ibc_imports = imps }
251 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
251 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
252 writeArchive f ibcf
252 writeArchive f ibcf
253− logIBC 1 "Written")
253+ logIBC 2 "Written")
254− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
254+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
255 return ()
255 return ()
256
256
257mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
257mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
@@ -369,7 +369,7 @@ process :: Bool -- ^ Reexporting
369process reexp phase archive fn = do
369process reexp phase archive fn = do
370 ver <- getEntry 0 "ver" archive
370 ver <- getEntry 0 "ver" archive
371 when (ver /= ibcVersion) $ do
371 when (ver /= ibcVersion) $ do
372− logIBC 1 "ibc out of date"
372+ logIBC 2 "ibc out of date"
373 let e = if ver < ibcVersion
373 let e = if ver < ibcVersion
374 then "an earlier" else "a later"
374 then "an earlier" else "a later"
375 ldir <- runIO $ getIdrisLibDir
375 ldir <- runIO $ getIdrisLibDir
@@ -524,10 +524,10 @@ processImports reexp phase ar = do
524 p -> p
524 p -> p
525 case fp of
525 case fp of
526 LIDR fn -> do
526 LIDR fn -> do
527− logIBC 1 $ "Failed at " ++ fn
527+ logIBC 2 $ "Failed at " ++ fn
528 ifail "Must be an ibc"
528 ifail "Must be an ibc"
529 IDR fn -> do
529 IDR fn -> do
530− logIBC 1 $ "Failed at " ++ fn
530+ logIBC 2 $ "Failed at " ++ fn
531 ifail "Must be an ibc"
531 ifail "Must be an ibc"
532 IBC fn src -> loadIBC (reexp && re) phase' fn) fs
532 IBC fn src -> loadIBC (reexp && re) phase' fn) fs
533
533
@@ -650,7 +650,7 @@ processDefs ar = do
650 case d' of
650 case d' of
651 TyDecl _ _ -> return ()
651 TyDecl _ _ -> return ()
652 _ -> do
652 _ -> do
653− logIBC 1 $ "SOLVING " ++ show n
653+ logIBC 2 $ "SOLVING " ++ show n
654 solveDeferred emptyFC n
654 solveDeferred emptyFC n
655 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
655 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
656 where
656 where
@@ -749,9 +749,9 @@ processAccess reexp phase ar = do
749
749
750 if (not reexp)
750 if (not reexp)
751 then do
751 then do
752− logIBC 1 $ "Not exporting " ++ show n
752+ logIBC 2 $ "Not exporting " ++ show n
753 setAccessibility n Hidden
753 setAccessibility n Hidden
754− else logIBC 1 $ "Exporting " ++ show n
754+ else logIBC 2 $ "Exporting " ++ show n
755 -- Everything should be available at the REPL from
755 -- Everything should be available at the REPL from
756 -- things imported publicly
756 -- things imported publicly
757 when (phase == IBC_REPL True) $ setAccessibility n Public) ds
757 when (phase == IBC_REPL True) $ setAccessibility n Public) ds
src/Idris/Termination.hs+2−2
@@ -284,8 +284,8 @@ buildSCG (_, n) = do
284
284
285delazy = delazy' False -- not lazy codata
285delazy = delazy' False -- not lazy codata
286delazy' all t@(App _ f a)
286delazy' all t@(App _ f a)
287− | (P _ (UN l) _, [_, _, arg]) <- unApply t,
287+ | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
288− l == txt "Force" = delazy' all arg
288+ l == txt "Force" && (all || lty /= txt "Infinite") = delazy' all arg
289 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
289 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
290 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
290 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
291 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
291 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
test/TestData.hs+2−1
@@ -290,7 +290,8 @@ testFamiliesData = [
290 ( 19, ANY ),
290 ( 19, ANY ),
291 ( 20, ANY ),
291 ( 20, ANY ),
292 ( 21, ANY ),
292 ( 21, ANY ),
293− ( 22, ANY )]),
293+ ( 22, ANY ),
294+ ( 23, ANY )]),
294 ("tutorial", "Tutorial examples",
295 ("tutorial", "Tutorial examples",
295 [ ( 1, ANY ),
296 [ ( 1, ANY ),
296 ( 2, ANY ),
297 ( 2, ANY ),
test/regression002/Canonicity.idrnew file+13
@@ -0,0 +1,13 @@
1+module Canonicity
2+%default total
3+
4+data ZeroSumList : Integer -> Type where
5+ Cons : (m : Integer) -> ZeroSumList n -> ZeroSumList (m + n)
6+ Nil : ZeroSumList 0
7+
8+f : ZeroSumList 0 -> Nat
9+f Nil = 0
10+
11+NaN : Nat
12+NaN = f (Cons 0 Nil)
13+
test/regression002/expected+2
@@ -145,3 +145,5 @@ When checking argument value to function Prelude.Basics.the:
145 -0.0
145 -0.0
146 and
146 and
147 0.0
147 0.0
148+Canonicity.idr:9:1:Canonicity.f is not total as there are missing cases
149+Canonicity.idr:12:1:Canonicity.NaN is possibly not total due to: Canonicity.f
test/regression002/run+1
@@ -32,6 +32,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!
32:load reg076.idr
32:load reg076.idr
33:load reg077.idr
33:load reg077.idr
34:load DoubleEquality.idr
34:load DoubleEquality.idr
35+:load Canonicity.idr
35!
36!
36
37
37rm -f *.ibc
38rm -f *.ibc
test/totality023/expectednew file+2
@@ -0,0 +1,2 @@
1+totality023.idr:9:1:
2+Main.run is possibly not total due to recursive path Main.run --> Main.run
test/totality023/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ totality023.idr --check
3+rm -f *.ibc
test/totality023/totality023.idrnew file+11
@@ -0,0 +1,11 @@
1+data InfIO : Type where
2+ Do : IO a -> (a -> Inf InfIO) -> InfIO
3+
4+foo : InfIO
5+foo = Do (putStr "Foo") (\x => foo)
6+
7+total
8+run : InfIO -> IO ()
9+run (Do x f) = do r <- x
10+ run (f r)
11+