git.iko.soy/Idris-dev
on master help sign in
Improvements from PR feedback, more cleanup.
commite06a3ec7411d5b71857fecee30c4a11d678c4d7c authorMatus Tejiscak <ziman@functor.sk> dateSat 17 Jun 2017, 08:04 (9 years ago) parente56b4bd
4 files changed+25−25
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+6−6 libs/base/Data/Nat/Views.idr+1−1 libs/base/Data/Vect/Views.idr+9−9 libs/prelude/Prelude/WellFounded.idr+9−9
libs/base/Data/List/Views.idr+6−6
@@ -65,7 +65,7 @@ data SplitRec : List a -> Type where
6565||| Constructs the view in O(n lg n)
6666export total
6767splitRec : (xs : List a) -> SplitRec xs
68−splitRec xs with (sizeAcc xs)
68+splitRec xs with (sizeAccessible xs)
6969 splitRec xs | acc with (split xs)
7070 splitRec [] | acc | SplitNil = SplitRecNil
7171 splitRec [x] | acc | SplitOne = SplitRecOne
@@ -111,11 +111,11 @@ filteredROK p x xs = LTESucc (filterSmaller xs)
111111||| Constructs the view in O(n lg n)
112112export
113113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
114−filtered p inp with (sizeAcc inp)
115− filtered p [] | with_pat = FNil
116− filtered p (x :: xs) | (Access xsrec)
117− = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
118− (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs))
114+filtered p inp with (sizeAccessible inp)
115+ filtered p [] | _ = FNil
116+ filtered p (x :: xs) | Access acc
117+ = FRec (filtered p (filter (\y => p y x) xs) | acc _ (filteredLOK p x xs))
118+ (filtered p (filter (\y => not (p y x)) xs) | acc _ (filteredROK p x xs))
119119
120120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
121121lenImpossible {n = Z} _ Refl impossible
libs/base/Data/Nat/Views.idr+1−1
@@ -24,7 +24,7 @@ half (S k) with (half k)
2424
2525export
2626halfRec : (n : Nat) -> HalfRec n
27−halfRec n with (sizeAcc n)
27+halfRec n with (sizeAccessible n)
2828 halfRec Z | acc = HalfRecZ
2929 halfRec (S n) | acc with (half n)
3030 halfRec' (S (S (k + k))) | Access acc | HalfOdd
libs/base/Data/Vect/Views.idr+9−9
@@ -61,23 +61,23 @@ data SplitRec : Vect n a -> Type where
6161 (lrec : Lazy (SplitRec xs)) ->
6262 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
6363
64−smallerPlus : LTE (S (S m)) (S (plus m (S k)))
65−smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
64+smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
65+smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
6666 (LTESucc (LTESucc (lteAddRight _)))
6767
68−smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
69−smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
68+smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
69+smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
7070 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
7171
7272||| Covering function for the `SplitRec` view
7373||| Constructs the view in O(n lg n)
7474export
7575splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (sizeAcc n)
76+splitRec {n} input with (sizeAccessible n)
7777 splitRec input | acc with (split input)
7878 splitRec [] | acc | SplitNil = SplitRecNil
7979 splitRec [x] | acc | SplitOne = SplitRecOne
80− splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
81− = let left = splitRec (x :: xs) | rec _ smallerPlus
82− right = splitRec (y :: ys) | rec _ smallerPlus' in
83− SplitRecPair left right
80+ splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
81+ = SplitRecPair
82+ (splitRec (x :: xs) | acc _ smallerPlusL)
83+ (splitRec (y :: ys) | acc _ smallerPlusR)
libs/prelude/Prelude/WellFounded.idr+9−9
@@ -86,8 +86,7 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
8888||| Interface of types with sized values.
89−|||
90−||| The sizes are used for proofs of termination via accessibility.
89+||| The size is used for proofs of termination via accessibility.
9190|||
9291||| @ a the type whose elements can be mapped to Nat
9392interface Sized a where
@@ -96,16 +95,17 @@ interface Sized a where
9695Smaller : Sized a => a -> a -> Type
9796Smaller x y = size x `LT` size y
9897
99−SizeAcc : Sized a => a -> Type
100−SizeAcc = Accessible Smaller
98+SizeAccessible : Sized a => a -> Type
99+SizeAccessible = Accessible Smaller
101100
102101||| Proof of well-foundedness of `Smaller`.
103102||| Constructs accessibility for any given element of `a`, provided `Sized a`.
104−sizeAcc : Sized a => (x : a) -> SizeAcc x
105−sizeAcc x = Access $ f (size x) (ltAccessible $ size x)
103+sizeAccessible : Sized a => (x : a) -> SizeAccessible x
104+sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
106105 where
106+ -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
108− -> (y : a) -> (size y `LT` sizeX) -> Accessible Smaller y
108+ -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
109109 f Z acc y pf = absurd pf
110110 f (S n) (Access acc) y (LTESucc yLEx)
111111 = Access (\z, zLTy =>
@@ -127,14 +127,14 @@ sizeInd : Sized a
127127 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
128128 -> (z : a)
129129 -> P z
130−sizeInd step z = accInd step z (sizeAcc z)
130+sizeInd step z = accInd step z (sizeAccessible z)
131131
132132||| Strong recursion principle for sized types.
133133sizeRec : Sized a
134134 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
135135 -> (z : a)
136136 -> b
137−sizeRec step z = accRec step z (sizeAcc z)
137+sizeRec step z = accRec step z (sizeAccessible z)
138138
139139
140140implementation Sized Nat where