git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commitf91a45a929b88af6ecc852170db9dd06cd3b79fe authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 13 Nov 2012, 12:06 (14 years ago) parent1a8630583fdb4d
4 files changed+55−12
compare with master
unifiedsplit
lib/Control/Arrow.idr+17−1 lib/Control/Category.idr+7−3 lib/Data/Morphisms.idr+28−8 src/Idris/Coverage.hs+3
lib/Control/Arrow.idr+17−1
@@ -15,9 +15,25 @@ class Category arr => Arrow (arr : Set -> Set -> Set) where
1515 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
1616 (&&&) : arr a b -> arr a b' -> arr a (b, b')
1717
18−instance Arrow Morphism where
18+instance Arrow Homomorphism where
1919 arrow f = Homo f
2020 first (Homo f) = Homo $ \(a, b) => (f a, b)
2121 second (Homo f) = Homo $ \(a, b) => (a, f b)
2222 (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
2323 (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
24+
25+instance Monad m => Arrow (Kleislimorphism m) where
26+ arrow f = Kleisli (return . f)
27+ first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a
28+ return (x, b)
29+
30+ second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
31+ return (a, x)
32+
33+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
34+ y <- g b
35+ return (x, y)
36+
37+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
38+ y <- g a
39+ return (x, y)
lib/Control/Category.idr+7−3
@@ -8,9 +8,13 @@ class Category (cat : Set -> Set -> Set) where
88 id : cat a a
99 (.) : cat b c -> cat a b -> cat a c
1010
11−instance Category Morphism where
12− id = Homo Builtins.id
13− (Homo f) . (Homo g) = Homo $ Builtins.(.) f g
11+instance Category Homomorphism where
12+ id = Homo Builtins.id
13+ (Homo f) . (Homo g) = Homo (f . g)
14+
15+instance Monad m => Category (Kleislimorphism m) where
16+ id = Kleisli (return . id)
17+ (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
1418
1519infixr 1 >>>
1620(>>>) : Category cat => cat a b -> cat b c -> cat a c
lib/Data/Morphisms.idr+28−8
@@ -1,22 +1,42 @@
11module Data.Morphisms
22
3+import Builtins
4+
35%access public
46
5−data Morphism : Set -> Set -> Set where
6− Homo : (a -> b) -> Morphism a b
7+data Homomorphism : Set -> Set -> Set where
8+ Homo : (a -> b) -> Homomorphism a b
9+
10+data Endomorphism : Set -> Set where
11+ Endo : (a -> a) -> Endomorphism a
12+
13+data Kleislimorphism : (Set -> Set) -> Set -> Set -> Set where
14+ Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
15+
16+applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
17+applyKleisli (Kleisli f) a = f a
718
8−($) : Morphism a b -> a -> b
9−(Homo f) $ a = f a
19+applyHomo : Homomorphism a b -> a -> b
20+applyHomo (Homo f) a = f a
1021
11−instance Monad (Morphism r) where
22+applyEndo : Endomorphism a -> a -> a
23+applyEndo (Endo f) a = f a
24+
25+instance Monad (Homomorphism r) where
1226 return a = Homo $ const a
13− (Homo h) >>= f = Homo $ \r => f (h r) $ r
27+ (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r
1428
15−instance Applicative (Morphism r) where
29+instance Applicative (Homomorphism r) where
1630 pure a = Homo $ const a
1731 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
1832
33+instance Semigroup (Endomorphism a) where
34+ (Endo f) <+> (Endo g) = Endo $ g . f
35+
36+instance Monoid (Endomorphism a) where
37+ neutral = Endo id
38+
1939infixr 1 ~>
2040
2141(~>) : Set -> Set -> Set
22−a ~> b = Morphism a b
42+a ~> b = Homomorphism a b
src/Idris/Coverage.hs+3
@@ -407,6 +407,7 @@ buildSCG (_, n) = do
407407 let newscg = buildSCG' ist sc args
408408 logLvl 5 $ show newscg
409409 addToCG n ( cg { scg = newscg } )
410+ [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
410411
411412buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
412413buildSCG' ist sc args = nub $ scg sc (zip args args)
@@ -505,6 +506,8 @@ checkSizeChange n = do
505506 let tot = map (checkMP ist (length (argsdef cg))) ms
506507 logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
507508 return (noPartial tot)
509+ [] -> do logLvl 5 $ "No paths for " ++ show n
510+ return Unchecked
508511
509512type MultiPath = [SCGEntry]
510513