git.iko.soy/Idris-dev
on master help sign in
Some naming in views
d280640Edwin Brady
libs/base/Data/List/Views.idr+4−3
compare with master
unifiedsplit
@@ -57,8 +57,9 @@ public export
57data SplitRec : List a -> Type where
57data SplitRec : List a -> Type where
58 SplitRecNil : SplitRec []
58 SplitRecNil : SplitRec []
59 SplitRecOne : {x : a} -> SplitRec [x]
59 SplitRecOne : {x : a} -> SplitRec [x]
60− SplitRecPair : {xs, ys : List a} -> -- Explicit, don't erase
60+ SplitRecPair : {lefts, rights : List a} -> -- Explicit, don't erase
61+ (lrec : Lazy (SplitRec lefts)) ->
61− Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
62+ (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
62
63
63total
64total
64splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
65splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
@@ -87,7 +88,7 @@ data SnocList : List a -> Type where
87snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
88snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
88snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
89snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
89snocListHelp {xs} x (y :: ys)
90snocListHelp {xs} x (y :: ys)
90− = rewrite appendAssociative xs [y] ys in snocListHelp (Snoc x {x=y}) ys
91+ = rewrite appendAssociative xs [y] ys in snocListHelp (Snoc x) ys
91
92
92||| Covering function for the `SnocList` view
93||| Covering function for the `SnocList` view
93||| Constructs the view in linear time
94||| Constructs the view in linear time
libs/base/Data/Nat/Views.idr+6−2
@@ -1,16 +1,19 @@
1module Data.Nat.Views
1module Data.Nat.Views
2
2
3public export
3public export
4+||| View for dividing a Nat in half
4data Half : Nat -> Type where
5data Half : Nat -> Type where
5 HalfOdd : {n : Nat} -> Half (S (n + n))
6 HalfOdd : {n : Nat} -> Half (S (n + n))
6 HalfEven : {n : Nat} -> Half (n + n)
7 HalfEven : {n : Nat} -> Half (n + n)
7
8
9+||| View for dividing a Nat in half, recursively
8public export
10public export
9data HalfRec : Nat -> Type where
11data HalfRec : Nat -> Type where
10 HalfRecZ : HalfRec Z
12 HalfRecZ : HalfRec Z
11− HalfRecEven : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (n + n)
13+ HalfRecEven : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (n + n)
12− HalfRecOdd : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (S (n + n))
14+ HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
13
15
16+||| Covering function for the `Half` view
14export
17export
15half : (n : Nat) -> Half n
18half : (n : Nat) -> Half n
16half Z = HalfEven {n=0}
19half Z = HalfEven {n=0}
@@ -28,6 +31,7 @@ halfRecFix (S k) hrec with (half k)
28 halfRecFix (S (n + n)) hrec | HalfEven
31 halfRecFix (S (n + n)) hrec | HalfEven
29 = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
32 = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
30
33
34+||| Covering function for the `HalfRec` view
31export
35export
32halfRec : (n : Nat) -> HalfRec n
36halfRec : (n : Nat) -> HalfRec n
33halfRec n = accInd halfRecFix n (ltAccessible n)
37halfRec n = accInd halfRecFix n (ltAccessible n)