git.iko.soy/Idris-dev
on master help sign in
Add the Sized interface + related utils.
commitc549f503a3ea214c72d7cb6aaf23cfa6776aad9e authorMatus Tejiscak <ziman@functor.sk> dateFri 16 Jun 2017, 14:25 (9 years ago) parent6db4204
4 files changed+54−31
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+5−5 libs/base/Data/Nat/Views.idr+3−3 libs/base/Data/Vect/Views.idr+1−1 libs/prelude/Prelude/WellFounded.idr+45−22
libs/base/Data/List/Views.idr+5−5
@@ -62,7 +62,7 @@ data SplitRec : List a -> Type where
6262 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
6363
6464total
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) ->
6666 SplitRec xs
6767splitRecFix xs srec with (split xs)
6868 splitRecFix [] srec | SplitNil = SplitRecNil
@@ -76,7 +76,7 @@ splitRecFix xs srec with (split xs)
7676||| Constructs the view in O(n lg n)
7777export total
7878splitRec : (xs : List a) -> SplitRec xs
79−splitRec xs = accInd splitRecFix xs (smallerAcc xs)
79+splitRec = sizeInd splitRecFix
8080
8181||| View for traversing a list backwards
8282public export
@@ -105,17 +105,17 @@ data Filtered : (a -> a -> Bool) -> List a -> Type where
105105 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
106106 Filtered p (x :: xs)
107107
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)
109109filteredLOK p x xs = LTESucc (filterSmaller xs)
110110
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)
112112filteredROK p x xs = LTESucc (filterSmaller xs)
113113
114114||| Covering function for the `Filtered` view
115115||| Constructs the view in O(n lg n)
116116export
117117filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (smallerAcc inp)
118+filtered p inp with (accessible inp)
119119 filtered p [] | with_pat = FNil
120120 filtered p (x :: xs) | (Access xsrec)
121121 = 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)
2222 HalfEven {n=S n}
2323 half (S (n + n)) | HalfEven = HalfOdd
2424
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
2626halfRecFix Z hrec = HalfRecZ
2727halfRecFix (S k) hrec with (half k)
2828 halfRecFix (S (S (n + n))) hrec | HalfOdd
@@ -34,5 +34,5 @@ halfRecFix (S k) hrec with (half k)
3434||| Covering function for the `HalfRec` view
3535export
3636halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAccessible n)
38−
37+halfRec n = accInd halfRecFix n (accessible n)
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
7373||| Constructs the view in O(n lg n)
7474export
7575splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (ltAccessible n)
76+splitRec {n} input with (accessible n)
7777 splitRec input | acc with (split input)
7878 splitRec [] | acc | SplitNil = SplitRecNil
7979 splitRec [x] | acc | SplitOne = SplitRecOne
libs/prelude/Prelude/WellFounded.idr+45−22
@@ -85,28 +85,51 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8585 (x : a) -> P x
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
88−-- Some basic useful relations
8988
90−||| LT is a well-founded relation on numbers
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))
89+-- Accessibility for sized types
11190
91+interface Sized a where
92+ size : a -> Nat
11293
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