git.iko.soy/Idris-dev
on master help sign in
Fix circular dependencies
c08dff7Edwin Brady
lib/prelude/list.idr+23
compare with master
unifiedsplit
@@ -110,3 +110,26 @@ split p xs = case break p xs of
110 (chunk, []) => [chunk]
110 (chunk, []) => [chunk]
111 (chunk, (c :: rest)) => chunk :: split p rest
111 (chunk, (c :: rest)) => chunk :: split p rest
112
112
113+--------------------------------------------------------------------------------
114+-- Conversions
115+--------------------------------------------------------------------------------
116+
117+maybeToList : Maybe a -> List a
118+maybeToList Nothing = []
119+maybeToList (Just j) = [j]
120+
121+listToMaybe : List a -> Maybe a
122+listToMaybe [] = Nothing
123+listToMaybe (x::xs) = Just x
124+
125+--------------------------------------------------------------------------------
126+-- Misc
127+--------------------------------------------------------------------------------
128+
129+catMaybes : List (Maybe a) -> List a
130+catMaybes [] = []
131+catMaybes (x::xs) =
132+ case x of
133+ Nothing => catMaybes xs
134+ Just j => j :: catMaybes xs
135+
lib/prelude/maybe.idr+2−30
@@ -1,12 +1,10 @@
1module prelude.maybe
1module prelude.maybe
2
2
3import builtins
3import builtins
4−import prelude.list
5−import prelude.monad
6
4
7data Maybe a
5data Maybe a
8− = Nothing
6+ = Nothing
9− | Just a
7+ | Just a
10
8
11--------------------------------------------------------------------------------
9--------------------------------------------------------------------------------
12-- Syntactic tests
10-- Syntactic tests
@@ -20,18 +18,6 @@ isJust : Maybe a -> Bool
20isJust Nothing = False
18isJust Nothing = False
21isJust (Just j) = True
19isJust (Just j) = True
22
20
23−--------------------------------------------------------------------------------
24−-- Conversions
25−--------------------------------------------------------------------------------
26−
27−maybeToList : Maybe a -> List a
28−maybeToList Nothing = []
29−maybeToList (Just j) = [j]
30−
31−listToMaybe : List a -> Maybe a
32−listToMaybe [] = Nothing
33−listToMaybe (x::xs) = Just x
34−
35--------------------------------------------------------------------------------
21--------------------------------------------------------------------------------
36-- Misc
22-- Misc
37--------------------------------------------------------------------------------
23--------------------------------------------------------------------------------
@@ -48,20 +34,6 @@ toMaybe : Bool -> a -> Maybe a
48toMaybe True j = Just j
34toMaybe True j = Just j
49toMaybe False j = Nothing
35toMaybe False j = Nothing
50
36
51−catMaybes : List (Maybe a) -> List a
52−catMaybes [] = []
53−catMaybes (x::xs) =
54− case x of
55− Nothing => catMaybes xs
56− Just j => j :: catMaybes xs
57−
58−mapMaybe : (a -> Maybe b) -> List a -> List b
59−mapMaybe f [] = []
60−mapMaybe f (x::xs) =
61− case f x of
62− Nothing => mapMaybe f xs
63− Just j => j :: mapMaybe f xs
64−
65--------------------------------------------------------------------------------
37--------------------------------------------------------------------------------
66-- Class instances
38-- Class instances
67--------------------------------------------------------------------------------
39--------------------------------------------------------------------------------
lib/prelude/monad.idr+1
@@ -3,6 +3,7 @@ module prelude.monad
3-- Monads and Functors
3-- Monads and Functors
4
4
5import builtins
5import builtins
6+import prelude.list
6
7
7%access public
8%access public
8
9
src/Core/CaseTree.hs+1−1
@@ -6,7 +6,7 @@ import Core.TT
6import Control.Monad.State
6import Control.Monad.State
7import Debug.Trace
7import Debug.Trace
8
8
9−data CaseDef = CaseDef [Name] SC
9+data CaseDef = CaseDef [Name] SC [Term]
10 deriving Show
10 deriving Show
11
11
12data SC = Case Name [CaseAlt]
12data SC = Case Name [CaseAlt]