git.iko.soy/Idris-dev
on master help sign in
Some naming in views
commitd280640d7ac6ae86efed6086e66578187da854ab authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 28 Apr 2016, 18:50 (10 years ago) parent055a1cf
2 files changed+10−5
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+4−3 libs/base/Data/Nat/Views.idr+6−2
libs/base/Data/List/Views.idr+4−3
@@ -57,8 +57,9 @@ public export
5757data SplitRec : List a -> Type where
5858 SplitRecNil : SplitRec []
5959 SplitRecOne : {x : a} -> SplitRec [x]
60− SplitRecPair : {xs, ys : List a} -> -- Explicit, don't erase
61− Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
60+ SplitRecPair : {lefts, rights : List a} -> -- Explicit, don't erase
61+ (lrec : Lazy (SplitRec lefts)) ->
62+ (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
6263
6364total
6465splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
@@ -87,7 +88,7 @@ data SnocList : List a -> Type where
8788snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
8889snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
8990snocListHelp {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
9192
9293||| Covering function for the `SnocList` view
9394||| Constructs the view in linear time
libs/base/Data/Nat/Views.idr+6−2
@@ -1,16 +1,19 @@
11module Data.Nat.Views
22
33public export
4+||| View for dividing a Nat in half
45data Half : Nat -> Type where
56 HalfOdd : {n : Nat} -> Half (S (n + n))
67 HalfEven : {n : Nat} -> Half (n + n)
78
9+||| View for dividing a Nat in half, recursively
810public export
911data HalfRec : Nat -> Type where
1012 HalfRecZ : HalfRec Z
11− HalfRecEven : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (n + n)
12− HalfRecOdd : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (S (n + n))
13+ HalfRecEven : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (n + n)
14+ HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
1315
16+||| Covering function for the `Half` view
1417export
1518half : (n : Nat) -> Half n
1619half Z = HalfEven {n=0}
@@ -28,6 +31,7 @@ halfRecFix (S k) hrec with (half k)
2831 halfRecFix (S (n + n)) hrec | HalfEven
2932 = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
3033
34+||| Covering function for the `HalfRec` view
3135export
3236halfRec : (n : Nat) -> HalfRec n
3337halfRec n = accInd halfRecFix n (ltAccessible n)