forked from idris-lang/Idris2
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[ new ] Data.OpenUnion (idris-lang#1050)
- Loading branch information
1 parent
5384560
commit a060dcc
Showing
9 changed files
with
371 additions
and
23 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,109 @@ | ||
module Data.List.AtIndex | ||
|
||
import Data.DPair | ||
import Data.List.HasLength | ||
import Data.Nat | ||
import Decidable.Equality | ||
|
||
%default total | ||
|
||
||| @AtIndex witnesses the fact that a natural number encodes a membership proof. | ||
||| It is meant to be used as a runtime-irrelevant gadget to guarantee that the | ||
||| natural number is indeed a valid index. | ||
public export | ||
data AtIndex : a -> List a -> Nat -> Type where | ||
Z : AtIndex a (a :: as) Z | ||
S : AtIndex a as n -> AtIndex a (b :: as) (S n) | ||
|
||
||| Inversion principle for Z constructor | ||
export | ||
inverseZ : AtIndex x (y :: xs) Z -> x === y | ||
inverseZ Z = Refl | ||
|
||
||| inversion principle for S constructor | ||
export | ||
inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n | ||
inverseS (S p) = p | ||
|
||
||| An empty list cannot possibly have members | ||
export | ||
Uninhabited (AtIndex a [] n) where | ||
uninhabited Z impossible | ||
uninhabited (S _) impossible | ||
|
||
||| For a given list and a given index, there is only one possible value | ||
||| stored at that index in that list | ||
export | ||
atIndexUnique : AtIndex a as n -> AtIndex b as n -> a === b | ||
atIndexUnique Z Z = Refl | ||
atIndexUnique (S p) (S q) = atIndexUnique p q | ||
|
||
||| Provided that equality is decidable, we can look for the first occurence | ||
||| of a value inside of a list | ||
public export | ||
find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs)) | ||
find x [] = No (\ p => void (absurd (snd p))) | ||
find x (y :: xs) with (decEq x y) | ||
find x (x :: xs) | Yes Refl = Yes (Element Z Z) | ||
find x (y :: xs) | No neqxy = case find x xs of | ||
Yes (Element n prf) => Yes (Element (S n) (S prf)) | ||
No notInxs => No \case | ||
(Element Z p) => void (neqxy (inverseZ p)) | ||
(Element (S n) prf) => absurd (notInxs (Element n (inverseS prf))) | ||
|
||
||| If the equality is not decidable, we may instead rely on interface resolution | ||
public export | ||
interface FindElement (0 t : a) (0 ts : List a) where | ||
findElement : Subset Nat (AtIndex t ts) | ||
|
||
FindElement t (t :: ts) where | ||
findElement = Element 0 Z | ||
|
||
FindElement t ts => FindElement t (u :: ts) where | ||
findElement = let (Element n prf) = findElement in | ||
Element (S n) (S prf) | ||
|
||
||| Given an index, we can decide whether there is a value corresponding to it | ||
public export | ||
lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n)) | ||
lookup n [] = No (\ p => void (absurd (snd p))) | ||
lookup Z (x :: xs) = Yes (Element x Z) | ||
lookup (S n) (x :: xs) = case lookup n xs of | ||
Yes (Element x p) => Yes (Element x (S p)) | ||
No notInxs => No (\ (Element x p) => void (notInxs (Element x (inverseS p)))) | ||
|
||
||| An AtIndex proof implies that n is less than the length of the list indexed into | ||
public export | ||
inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs) | ||
inRange n [] p = void (absurd p) | ||
inRange Z (x :: xs) p = LTEZero | ||
inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p)) | ||
|
||
||| | ||
export | ||
weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n | ||
weakenR Z = Z | ||
weakenR (S p) = S (weakenR p) | ||
|
||
export | ||
weakenL : (p : Subset Nat (HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n) | ||
weakenL m p = case view m of | ||
Z => p | ||
(S m) => S (weakenL m p) | ||
|
||
export | ||
strengthenL : (p : Subset Nat (HasLength xs)) -> | ||
lt n (fst p) === True -> | ||
AtIndex x (xs ++ ys) n -> AtIndex x xs n | ||
strengthenL m lt idx = case view m of | ||
S m => case idx of | ||
Z => Z | ||
S idx => S (strengthenL m lt idx) | ||
|
||
export | ||
strengthenR : (p : Subset Nat (HasLength ws)) -> | ||
lte (fst p) n === True -> | ||
AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p)) | ||
strengthenR m lt idx = case view m of | ||
Z => rewrite minusZeroRight n in idx | ||
S m => case idx of S idx => strengthenR m lt idx |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,138 @@ | ||
||| This module implements a relation between a natural number and a list. | ||
||| The relation witnesses the fact the number is the length of the list. | ||
||| | ||
||| It is meant to be used in a runtime-irrelevant fashion in computations | ||
||| manipulating data indexed over lists where the computation actually only | ||
||| depends on the length of said lists. | ||
||| | ||
||| Instead of writing: | ||
||| ``` | ||
||| f0 : (xs : List a) -> P xs | ||
||| ``` | ||
||| | ||
||| We would write either of: | ||
||| ``` | ||
||| f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs | ||
||| f2 : (n : Subset n (HasLength xs)) -> P xs | ||
||| ``` | ||
||| | ||
||| See `sucR` for an example where the update to the runtime-relevant Nat is O(1) | ||
||| but the udpate to the list (were we to keep it around) an O(n) traversal. | ||
|
||
module Data.List.HasLength | ||
|
||
import Data.DPair | ||
import Data.List | ||
|
||
%default total | ||
|
||
------------------------------------------------------------------------ | ||
-- Type | ||
|
||
||| Ensure that the list's length is the provided natural number | ||
public export | ||
data HasLength : List a -> Nat -> Type where | ||
Z : HasLength [] Z | ||
S : HasLength xs n -> HasLength (x :: xs) (S n) | ||
|
||
------------------------------------------------------------------------ | ||
-- Properties | ||
|
||
||| The length is unique | ||
export | ||
hasLengthUnique : HasLength xs m -> HasLength xs n -> m === n | ||
hasLengthUnique Z Z = Refl | ||
hasLengthUnique (S p) (S q) = cong S (hasLengthUnique p q) | ||
|
||
||| This specification corresponds to the length function | ||
export | ||
hasLength : (xs : List a) -> HasLength xs (length xs) | ||
hasLength [] = Z | ||
hasLength (_ :: xs) = S (hasLength xs) | ||
|
||
export | ||
map : (f : a -> b) -> HasLength xs n -> HasLength (map f xs) n | ||
map f Z = Z | ||
map f (S n) = S (map f n) | ||
|
||
||| @sucR demonstrates that snoc only increases the lenght by one | ||
||| So performing this operation while carrying the list around would cost O(n) | ||
||| but relying on n together with an erased HasLength proof instead is O(1) | ||
export | ||
sucR : HasLength xs n -> HasLength (snoc xs x) (S n) | ||
sucR Z = S Z | ||
sucR (S n) = S (sucR n) | ||
|
||
------------------------------------------------------------------------ | ||
-- Views | ||
|
||
namespace SubsetView | ||
|
||
||| We provide this view as a convenient way to perform nested pattern-matching | ||
||| on values of type `Subset Nat (HasLength xs)`. Functions using this view will | ||
||| be seen as terminating as long as the index list `xs` is left untouched. | ||
||| See e.g. listTerminating below for such a function. | ||
public export | ||
data View : (xs : List a) -> Subset Nat (HasLength xs) -> Type where | ||
Z : View [] (Element Z Z) | ||
S : (p : Subset Nat (HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p))) | ||
|
||
||| This auxiliary function gets around the limitation of the check ensuring that | ||
||| we do not match on runtime-irrelevant data to produce runtime-relevant data. | ||
viewZ : (0 p : HasLength xs Z) -> View xs (Element Z p) | ||
viewZ Z = Z | ||
|
||
||| This auxiliary function gets around the limitation of the check ensuring that | ||
||| we do not match on runtime-irrelevant data to produce runtime-relevant data. | ||
viewS : (n : Nat) -> (0 p : HasLength xs (S n)) -> View xs (Element (S n) p) | ||
viewS n (S p) = S (Element n p) | ||
|
||
||| Proof that the view covers all possible cases. | ||
export | ||
view : (p : Subset Nat (HasLength xs)) -> View xs p | ||
view (Element Z p) = viewZ p | ||
view (Element (S n) p) = viewS n p | ||
|
||
namespace CurriedView | ||
|
||
||| We provide this view as a convenient way to perform nested pattern-matching | ||
||| on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations | ||
||| to the list between recursive calls (e.g. mapping over the list) that prevent | ||
||| it from being a valid termination metric, it is best to take the Nat argument | ||
||| separately from the HasLength proof and the Subset view is not as useful anymore. | ||
||| See e.g. natTerminating below for (a contrived example of) such a function. | ||
public export | ||
data View : (xs : List a) -> (n : Nat) -> HasLength xs n -> Type where | ||
Z : View [] Z Z | ||
S : (n : Nat) -> (0 p : HasLength xs n) -> View (x :: xs) (S n) (S p) | ||
|
||
||| Proof that the view covers all possible cases. | ||
export | ||
view : (n : Nat) -> (0 p : HasLength xs n) -> View xs n p | ||
view Z Z = Z | ||
view (S n) (S p) = S n p | ||
|
||
------------------------------------------------------------------------ | ||
-- Examples | ||
|
||
-- /!\ Do NOT re-export these examples | ||
|
||
listTerminating : (p : Subset Nat (HasLength xs)) -> HasLength (xs ++ [x]) (S (fst p)) | ||
listTerminating p = case view p of | ||
Z => S Z | ||
S p => S (listTerminating p) | ||
|
||
data P : List Nat -> Type where | ||
PNil : P [] | ||
PCon : P (map id xs) -> P (x :: xs) | ||
|
||
covering | ||
notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs | ||
notListTerminating p = case view p of | ||
Z => PNil | ||
S p => PCon (notListTerminating {xs = map id (tail xs)} (record { snd $= map id } p)) | ||
|
||
natTerminating : (n : Nat) -> (0 p : HasLength xs n) -> P xs | ||
natTerminating n p = case view n p of | ||
Z => PNil | ||
S n p => PCon (natTerminating n (map id p)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.