git.iko.soy/Idris-dev
on master help sign in
Add the Sized interface + related utils.
c549f50Matus Tejiscak
libs/base/Data/List/Views.idr+5−5
compare with master
unifiedsplit
@@ -62,7 +62,7 @@ data SplitRec : List a -> Type where
62 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
62 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
63
63
64total
64total
65−splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
65+splitRecFix : (xs : List a) -> ((ys : List a) -> Smaller ys xs -> SplitRec ys) ->
66 SplitRec xs
66 SplitRec xs
67splitRecFix xs srec with (split xs)
67splitRecFix xs srec with (split xs)
68 splitRecFix [] srec | SplitNil = SplitRecNil
68 splitRecFix [] srec | SplitNil = SplitRecNil
@@ -76,7 +76,7 @@ splitRecFix xs srec with (split xs)
76||| Constructs the view in O(n lg n)
76||| Constructs the view in O(n lg n)
77export total
77export total
78splitRec : (xs : List a) -> SplitRec xs
78splitRec : (xs : List a) -> SplitRec xs
79−splitRec xs = accInd splitRecFix xs (smallerAcc xs)
79+splitRec = sizeInd splitRecFix
80
80
81||| View for traversing a list backwards
81||| View for traversing a list backwards
82public export
82public export
@@ -105,17 +105,17 @@ data Filtered : (a -> a -> Bool) -> List a -> Type where
105 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
105 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
106 Filtered p (x :: xs)
106 Filtered p (x :: xs)
107
107
108−filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => p y x) xs) (x :: xs)
108+filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => p y x) xs) (x :: xs)
109filteredLOK p x xs = LTESucc (filterSmaller xs)
109filteredLOK p x xs = LTESucc (filterSmaller xs)
110
110
111−filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => not (p y x)) xs) (x :: xs)
111+filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => not (p y x)) xs) (x :: xs)
112filteredROK p x xs = LTESucc (filterSmaller xs)
112filteredROK p x xs = LTESucc (filterSmaller xs)
113
113
114||| Covering function for the `Filtered` view
114||| Covering function for the `Filtered` view
115||| Constructs the view in O(n lg n)
115||| Constructs the view in O(n lg n)
116export
116export
117filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
117filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (smallerAcc inp)
118+filtered p inp with (accessible inp)
119 filtered p [] | with_pat = FNil
119 filtered p [] | with_pat = FNil
120 filtered p (x :: xs) | (Access xsrec)
120 filtered p (x :: xs) | (Access xsrec)
121 = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
121 = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
libs/base/Data/Nat/Views.idr+3−3
@@ -22,7 +22,7 @@ half (S k) with (half k)
22 HalfEven {n=S n}
22 HalfEven {n=S n}
23 half (S (n + n)) | HalfEven = HalfOdd
23 half (S (n + n)) | HalfEven = HalfOdd
24
24
25−halfRecFix : (n : Nat) -> ((m : Nat) -> LT m n -> HalfRec m) -> HalfRec n
25+halfRecFix : (n : Nat) -> ((m : Nat) -> Smaller m n -> HalfRec m) -> HalfRec n
26halfRecFix Z hrec = HalfRecZ
26halfRecFix Z hrec = HalfRecZ
27halfRecFix (S k) hrec with (half k)
27halfRecFix (S k) hrec with (half k)
28 halfRecFix (S (S (n + n))) hrec | HalfOdd
28 halfRecFix (S (S (n + n))) hrec | HalfOdd
@@ -34,5 +34,5 @@ halfRecFix (S k) hrec with (half k)
34||| Covering function for the `HalfRec` view
34||| Covering function for the `HalfRec` view
35export
35export
36halfRec : (n : Nat) -> HalfRec n
36halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAccessible n)
37+halfRec n = accInd halfRecFix n (accessible n)
38−
38+-- for some strange reason, (halfRec = sizeInd halfRecFix) does not typecheck here
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)
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 (ltAccessible n)
76+splitRec {n} input with (accessible 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
libs/prelude/Prelude/WellFounded.idr+45−22
@@ -85,28 +85,51 @@ wfInd : WellFounded rel => {P : a -> Type} ->
85 (x : a) -> P x
85 (x : a) -> P x
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
87
87
88−-- Some basic useful relations
89
88
90−||| LT is a well-founded relation on numbers
89+-- Accessibility for sized types
91−ltAccessible : (n : Nat) -> Accessible LT n
92−ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
93− where
94− ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
95− ltAccessible' Z x = absurd x
96− ltAccessible' (S k) (LTESucc x)
97− = Access (\val, p => ltAccessible' k (lteTransitive p x))
98−
99−-- First list is smaller than the second
100−smaller : List a -> List a -> Type
101−smaller xs ys = LT (length xs) (length ys)
102−
103−||| `smaller` is a well-founded relation on lists
104−smallerAcc : (xs : List a) -> Accessible WellFounded.smaller xs
105−smallerAcc xs = Access (\v, prf => smallerAcc' {xs'=v} xs prf)
106− where
107− smallerAcc' : (ys : List a) -> smaller xs' ys -> Accessible smaller xs'
108− smallerAcc' [] x = absurd x
109− smallerAcc' (y :: ys) (LTESucc x)
110− = Access (\val, p => smallerAcc' ys (lteTransitive p x))
111
90
91+interface Sized a where
92+ size : a -> Nat
112
93
94+Smaller : Sized a => a -> a -> Type
95+Smaller x y = size x `LT` size y
96+
97+accessible : Sized a => (x : a) -> Accessible Smaller x
98+accessible x = Access $ f (size x) (ltAccessible $ size x)
99+ where
100+ f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
101+ -> (y : a) -> (size y `LT` sizeX) -> Accessible Smaller y
102+ f Z acc y pf = absurd pf
103+ f (S n) (Access acc) y (LTESucc yLEx)
104+ = Access (\z, zLTy =>
105+ f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
106+ )
107+
108+ ||| LT is a well-founded relation on numbers
109+ ltAccessible : (n : Nat) -> Accessible LT n
110+ ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
111+ where
112+ ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
113+ ltAccessible' Z x = absurd x
114+ ltAccessible' (S k) (LTESucc x)
115+ = Access (\val, p => ltAccessible' k (lteTransitive p x))
116+
117+sizeInd : Sized a
118+ => {P : a -> Type}
119+ -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
120+ -> (z : a)
121+ -> P z
122+sizeInd step z = accInd step z (accessible z)
123+
124+sizeRec : Sized a
125+ => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
126+ -> (z : a)
127+ -> b
128+sizeRec step z = accRec step z (accessible z)
129+
130+
131+implementation Sized Nat where
132+ size = \x => x
133+
134+implementation Sized (List a) where
135+ size = length