git.iko.soy/Idris-dev
on master help sign in
Simplify view definitions.
commite56b4bd24e0eeadb1b3deedd1abddbaa2f07979e authorMatus Tejiscak <ziman@functor.sk> dateFri 16 Jun 2017, 19:04 (9 years ago) parentefec5c7
4 files changed+25−31
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+9−13 libs/base/Data/Nat/Views.idr+8−12 libs/base/Data/Vect/Views.idr+1−1 libs/prelude/Prelude/WellFounded.idr+7−5
libs/base/Data/List/Views.idr+9−13
@@ -61,22 +61,18 @@ data SplitRec : List a -> Type where
6161 (lrec : Lazy (SplitRec lefts)) ->
6262 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
6363
64−total
65−splitRecFix : (xs : List a) -> ((ys : List a) -> Smaller ys xs -> SplitRec ys) ->
66− SplitRec xs
67−splitRecFix xs srec with (split xs)
68− splitRecFix [] srec | SplitNil = SplitRecNil
69− splitRecFix [x] srec | SplitOne = SplitRecOne
70− splitRecFix (x :: (ys ++ (y :: zs))) srec | SplitPair
71− = let left = srec (x :: ys) (smallerLeft ys y zs)
72− right = srec (y :: zs) (smallerRight ys zs) in
73− SplitRecPair left right
74−
7564||| Covering function for the `SplitRec` view
7665||| Constructs the view in O(n lg n)
7766export total
7867splitRec : (xs : List a) -> SplitRec xs
79−splitRec = sizeInd splitRecFix
68+splitRec xs with (sizeAcc xs)
69+ splitRec xs | acc with (split xs)
70+ splitRec [] | acc | SplitNil = SplitRecNil
71+ splitRec [x] | acc | SplitOne = SplitRecOne
72+ splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair
73+ = SplitRecPair
74+ (splitRec (y :: ys) | acc (y :: ys) (smallerLeft ys z zs))
75+ (splitRec (z :: zs) | acc (z :: zs) (smallerRight ys zs))
8076
8177||| View for traversing a list backwards
8278public export
@@ -115,7 +111,7 @@ filteredROK p x xs = LTESucc (filterSmaller xs)
115111||| Constructs the view in O(n lg n)
116112export
117113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (accessible inp)
114+filtered p inp with (sizeAcc inp)
119115 filtered p [] | with_pat = FNil
120116 filtered p (x :: xs) | (Access xsrec)
121117 = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
libs/base/Data/Nat/Views.idr+8−12
@@ -22,17 +22,13 @@ half (S k) with (half k)
2222 HalfEven {n=S n}
2323 half (S (n + n)) | HalfEven = HalfOdd
2424
25−halfRecFix : (n : Nat) -> ((m : Nat) -> Smaller m n -> HalfRec m) -> HalfRec n
26−halfRecFix Z hrec = HalfRecZ
27−halfRecFix (S k) hrec with (half k)
28− halfRecFix (S (S (n + n))) hrec | HalfOdd
29− = rewrite plusSuccRightSucc (S n) n in
30− HalfRecEven (hrec (S n) (LTESucc (LTESucc (lteAddRight _))))
31− halfRecFix (S (n + n)) hrec | HalfEven
32− = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
33−
34−||| Covering function for the `HalfRec` view
3525export
3626halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (accessible n)
38−-- for some strange reason, (halfRec = sizeInd halfRecFix) does not typecheck here
27+halfRec n with (sizeAcc n)
28+ halfRec Z | acc = HalfRecZ
29+ halfRec (S n) | acc with (half n)
30+ halfRec' (S (S (k + k))) | Access acc | HalfOdd
31+ = rewrite plusSuccRightSucc (S k) k
32+ in HalfRecEven (halfRec' (S k) | acc (S k) (LTESucc (LTESucc (lteAddRight _))))
33+ halfRec' (S (k + k)) | Access acc | HalfEven
34+ = HalfRecOdd (halfRec' k | acc k (LTESucc (lteAddRight _)))
libs/base/Data/Vect/Views.idr+1−1
@@ -73,7 +73,7 @@ smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
7373||| Constructs the view in O(n lg n)
7474export
7575splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (accessible n)
76+splitRec {n} input with (sizeAcc n)
7777 splitRec input | acc with (split input)
7878 splitRec [] | acc | SplitNil = SplitRecNil
7979 splitRec [x] | acc | SplitOne = SplitRecOne
libs/prelude/Prelude/WellFounded.idr+7−5
@@ -85,7 +85,6 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8585 (x : a) -> P x
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
88−
8988||| Interface of types with sized values.
9089|||
9190||| The sizes are used for proofs of termination via accessibility.
@@ -97,10 +96,13 @@ interface Sized a where
9796Smaller : Sized a => a -> a -> Type
9897Smaller x y = size x `LT` size y
9998
99+SizeAcc : Sized a => a -> Type
100+SizeAcc = Accessible Smaller
101+
100102||| Proof of well-foundedness of `Smaller`.
101103||| Constructs accessibility for any given element of `a`, provided `Sized a`.
102−accessible : Sized a => (x : a) -> Accessible Smaller x
103−accessible x = Access $ f (size x) (ltAccessible $ size x)
104+sizeAcc : Sized a => (x : a) -> SizeAcc x
105+sizeAcc x = Access $ f (size x) (ltAccessible $ size x)
104106 where
105107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
106108 -> (y : a) -> (size y `LT` sizeX) -> Accessible Smaller y
@@ -125,14 +127,14 @@ sizeInd : Sized a
125127 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
126128 -> (z : a)
127129 -> P z
128−sizeInd step z = accInd step z (accessible z)
130+sizeInd step z = accInd step z (sizeAcc z)
129131
130132||| Strong recursion principle for sized types.
131133sizeRec : Sized a
132134 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
133135 -> (z : a)
134136 -> b
135−sizeRec step z = accRec step z (accessible z)
137+sizeRec step z = accRec step z (sizeAcc z)
136138
137139
138140implementation Sized Nat where