e56b4bd · Idris-dev · git.iko.soy

libs/base/Data/List/Views.idr+9−13

compare with master

unifiedsplit

@@ -61,22 +61,18 @@ data SplitRec : List a -> Type where

61 (lrec : Lazy (SplitRec lefts)) ->

62 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)

63

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−

75||| Covering function for the `SplitRec` view

64||| Covering function for the `SplitRec` view

76||| Constructs the view in O(n lg n)

65||| Constructs the view in O(n lg n)

77export total

66export total

78splitRec : (xs : List a) -> SplitRec xs

67splitRec : (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))

80

76

81||| View for traversing a list backwards

77||| View for traversing a list backwards

82public export

78public export

@@ -115,7 +111,7 @@ filteredROK p x xs = LTESucc (filterSmaller xs)

115||| Constructs the view in O(n lg n)

111||| Constructs the view in O(n lg n)

116export

112export

117filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs

113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs

118−filtered p inp with (accessible inp)

114+filtered p inp with (sizeAcc inp)

119 filtered p [] | with_pat = FNil

115 filtered p [] | with_pat = FNil

120 filtered p (x :: xs) | (Access xsrec)

116 filtered p (x :: xs) | (Access xsrec)

121 = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))

117 = 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)

22 HalfEven {n=S n}

23 half (S (n + n)) | HalfEven = HalfOdd

24

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

35export

25export

36halfRec : (n : Nat) -> HalfRec n

26halfRec : (n : Nat) -> HalfRec n

37−halfRec n = accInd halfRecFix n (accessible n)

27+halfRec n with (sizeAcc n)

38−-- for some strange reason, (halfRec = sizeInd halfRecFix) does not typecheck here

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

73||| Constructs the view in O(n lg n)

74export

75splitRec : (xs : Vect n a) -> SplitRec xs

76−splitRec {n} input with (accessible n)

76+splitRec {n} input with (sizeAcc n)

77 splitRec input | acc with (split input)

78 splitRec [] | acc | SplitNil = SplitRecNil

79 splitRec [x] | acc | SplitOne = SplitRecOne

libs/prelude/Prelude/WellFounded.idr+7−5

@@ -85,7 +85,6 @@ wfInd : WellFounded rel => {P : a -> Type} ->

85 (x : a) -> P x

86wfInd {rel} step x = accInd step x (wellFounded {rel} x)

87

88−

89||| Interface of types with sized values.

88||| Interface of types with sized values.

90|||

89|||

91||| The sizes are used for proofs of termination via accessibility.

90||| The sizes are used for proofs of termination via accessibility.

@@ -97,10 +96,13 @@ interface Sized a where

97Smaller : Sized a => a -> a -> Type

96Smaller : Sized a => a -> a -> Type

98Smaller x y = size x `LT` size y

97Smaller x y = size x `LT` size y

99

98

99+SizeAcc : Sized a => a -> Type

100+SizeAcc = Accessible Smaller

101+

100||| Proof of well-foundedness of `Smaller`.

102||| Proof of well-foundedness of `Smaller`.

101||| Constructs accessibility for any given element of `a`, provided `Sized a`.

103||| Constructs accessibility for any given element of `a`, provided `Sized a`.

102−accessible : Sized a => (x : a) -> Accessible Smaller x

104+sizeAcc : Sized a => (x : a) -> SizeAcc x

103−accessible x = Access $ f (size x) (ltAccessible $ size x)

105+sizeAcc x = Access $ f (size x) (ltAccessible $ size x)

104 where

106 where

105 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)

107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)

106 -> (y : a) -> (size y `LT` sizeX) -> Accessible Smaller y

108 -> (y : a) -> (size y `LT` sizeX) -> Accessible Smaller y

@@ -125,14 +127,14 @@ sizeInd : Sized a

125 -> (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)

126 -> (z : a)

128 -> (z : a)

127 -> P z

129 -> P z

128−sizeInd step z = accInd step z (accessible z)

130+sizeInd step z = accInd step z (sizeAcc z)

129

131

130||| Strong recursion principle for sized types.

132||| Strong recursion principle for sized types.

131sizeRec : Sized a

133sizeRec : Sized a

132 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)

134 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)

133 -> (z : a)

135 -> (z : a)

134 -> b

136 -> b

135−sizeRec step z = accRec step z (accessible z)

137+sizeRec step z = accRec step z (sizeAcc z)

136

138

137

139

138implementation Sized Nat where

140implementation Sized Nat where