git.iko.soy/Idris-dev
on master help sign in
Improvements from PR feedback, more cleanup.
e06a3ecMatus Tejiscak
libs/base/Data/List/Views.idr+6−6
compare with master
unifiedsplit
@@ -65,7 +65,7 @@ data SplitRec : List a -> Type where
65||| Constructs the view in O(n lg n)
65||| Constructs the view in O(n lg n)
66export total
66export total
67splitRec : (xs : List a) -> SplitRec xs
67splitRec : (xs : List a) -> SplitRec xs
68−splitRec xs with (sizeAcc xs)
68+splitRec xs with (sizeAccessible xs)
69 splitRec xs | acc with (split xs)
69 splitRec xs | acc with (split xs)
70 splitRec [] | acc | SplitNil = SplitRecNil
70 splitRec [] | acc | SplitNil = SplitRecNil
71 splitRec [x] | acc | SplitOne = SplitRecOne
71 splitRec [x] | acc | SplitOne = SplitRecOne
@@ -111,11 +111,11 @@ filteredROK p x xs = LTESucc (filterSmaller xs)
111||| Constructs the view in O(n lg n)
111||| Constructs the view in O(n lg n)
112export
112export
113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
114−filtered p inp with (sizeAcc inp)
114+filtered p inp with (sizeAccessible inp)
115− filtered p [] | with_pat = FNil
115+ filtered p [] | _ = FNil
116− filtered p (x :: xs) | (Access xsrec)
116+ filtered p (x :: xs) | Access acc
117− = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
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) | xsrec _ (filteredROK p x xs))
118+ (filtered p (filter (\y => not (p y x)) xs) | acc _ (filteredROK p x xs))
119
119
120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
121lenImpossible {n = Z} _ Refl impossible
121lenImpossible {n = Z} _ Refl impossible
libs/base/Data/Nat/Views.idr+1−1
@@ -24,7 +24,7 @@ half (S k) with (half k)
24
24
25export
25export
26halfRec : (n : Nat) -> HalfRec n
26halfRec : (n : Nat) -> HalfRec n
27−halfRec n with (sizeAcc n)
27+halfRec n with (sizeAccessible n)
28 halfRec Z | acc = HalfRecZ
28 halfRec Z | acc = HalfRecZ
29 halfRec (S n) | acc with (half n)
29 halfRec (S n) | acc with (half n)
30 halfRec' (S (S (k + k))) | Access acc | HalfOdd
30 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
61 (lrec : Lazy (SplitRec xs)) ->
61 (lrec : Lazy (SplitRec xs)) ->
62 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
62 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
63
63
64−smallerPlus : LTE (S (S m)) (S (plus m (S k)))
64+smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
65−smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
65+smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
66 (LTESucc (LTESucc (lteAddRight _)))
66 (LTESucc (LTESucc (lteAddRight _)))
67
67
68−smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
68+smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
69−smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
69+smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
70 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
70 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
71
71
72||| Covering function for the `SplitRec` view
72||| Covering function for the `SplitRec` view
73||| Constructs the view in O(n lg n)
73||| Constructs the view in O(n lg n)
74export
74export
75splitRec : (xs : Vect n a) -> SplitRec xs
75splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (sizeAcc n)
76+splitRec {n} input with (sizeAccessible n)
77 splitRec input | acc with (split input)
77 splitRec input | acc with (split input)
78 splitRec [] | acc | SplitNil = SplitRecNil
78 splitRec [] | acc | SplitNil = SplitRecNil
79 splitRec [x] | acc | SplitOne = SplitRecOne
79 splitRec [x] | acc | SplitOne = SplitRecOne
80− splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
80+ splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
81− = let left = splitRec (x :: xs) | rec _ smallerPlus
82− right = splitRec (y :: ys) | rec _ smallerPlus' in
83− SplitRecPair left right
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} ->
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
87
87
88||| Interface of types with sized values.
88||| 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.
91|||
90|||
92||| @ a the type whose elements can be mapped to Nat
91||| @ a the type whose elements can be mapped to Nat
93interface Sized a where
92interface Sized a where
@@ -96,16 +95,17 @@ interface Sized a where
96Smaller : Sized a => a -> a -> Type
95Smaller : Sized a => a -> a -> Type
97Smaller x y = size x `LT` size y
96Smaller x y = size x `LT` size y
98
97
99−SizeAcc : Sized a => a -> Type
98+SizeAccessible : Sized a => a -> Type
100−SizeAcc = Accessible Smaller
99+SizeAccessible = Accessible Smaller
101
100
102||| Proof of well-foundedness of `Smaller`.
101||| Proof of well-foundedness of `Smaller`.
103||| Constructs accessibility for any given element of `a`, provided `Sized a`.
102||| Constructs accessibility for any given element of `a`, provided `Sized a`.
104−sizeAcc : Sized a => (x : a) -> SizeAcc x
103+sizeAccessible : Sized a => (x : a) -> SizeAccessible x
105−sizeAcc x = Access $ f (size x) (ltAccessible $ size x)
104+sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
106 where
105 where
106+ -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
107 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
109 f Z acc y pf = absurd pf
109 f Z acc y pf = absurd pf
110 f (S n) (Access acc) y (LTESucc yLEx)
110 f (S n) (Access acc) y (LTESucc yLEx)
111 = Access (\z, zLTy =>
111 = Access (\z, zLTy =>
@@ -127,14 +127,14 @@ sizeInd : Sized a
127 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
127 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
128 -> (z : a)
128 -> (z : a)
129 -> P z
129 -> P z
130−sizeInd step z = accInd step z (sizeAcc z)
130+sizeInd step z = accInd step z (sizeAccessible z)
131
131
132||| Strong recursion principle for sized types.
132||| Strong recursion principle for sized types.
133sizeRec : Sized a
133sizeRec : Sized a
134 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
134 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
135 -> (z : a)
135 -> (z : a)
136 -> b
136 -> b
137−sizeRec step z = accRec step z (sizeAcc z)
137+sizeRec step z = accRec step z (sizeAccessible z)
138
138
139
139
140implementation Sized Nat where
140implementation Sized Nat where