From 128648873cc5d90e041ec6b4c6d10a7b4f57b0c0 Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Sun, 7 Jan 2024 19:18:10 -0600 Subject: [PATCH 1/3] complete the relocation of contrib HVect into base as All --- libs/base/Data/Vect/Quantifiers.idr | 104 +++++++++++++ libs/contrib/Data/Fun/Extra.idr | 2 +- libs/contrib/Data/HVect.idr | 170 --------------------- libs/contrib/Data/Rel/Complement.idr | 2 +- libs/contrib/Decidable/Decidable/Extra.idr | 2 +- libs/contrib/contrib.ipkg | 2 - 6 files changed, 107 insertions(+), 175 deletions(-) delete mode 100644 libs/contrib/Data/HVect.idr diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr index 713fef2e4a..936b1e7d46 100644 --- a/libs/base/Data/Vect/Quantifiers.idr +++ b/libs/base/Data/Vect/Quantifiers.idr @@ -2,6 +2,9 @@ module Data.Vect.Quantifiers import Data.DPair import Data.Vect +import Data.Vect.Elem + +import Decidable.Equality %default total @@ -205,6 +208,10 @@ namespace All traversePropertyRelevant f [] = pure [] traversePropertyRelevant f (x :: xs) = [| f _ x :: traversePropertyRelevant f xs |] + export + consInjective : {0 xs, ys: All p ts} -> {0 x, y: p a} -> (x :: xs = y :: ys) -> (x = y, xs = ys) + consInjective Refl = (Refl, Refl) + public export tabulate : {n : _} -> {0 xs : Vect n _} -> @@ -227,6 +234,18 @@ namespace All show' acc @{[_]} [px] = acc ++ show px show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs + export + All (DecEq . p) xs => DecEq (All p xs) where + decEq [] [] = Yes Refl + decEq @{deq :: deqs} (x :: xs) (y :: ys) with (decEq x y) + decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) with (decEq xs ys) + decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) | (Yes prf') = + Yes (rewrite prf in rewrite prf' in Refl) + decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) | (No contra) = + No (contra . snd . consInjective) + decEq @{deq :: deqs} (x :: xs) (y :: ys) | (No contra) = + No (contra . fst . consInjective) + export All (Eq . p) xs => Eq (All p xs) where (==) [] [] = True @@ -288,3 +307,88 @@ namespace All drop' 0 ys = rewrite minusZeroRight k in ys drop' (S k) [] = [] drop' (S k) (y :: ys) = drop' k ys + + ||| Extract an element from an All. + ||| + ||| ```idris example + ||| > index 0 (the (HVect _) [1, "string"]) + ||| 1 + ||| ``` + export + index : (i : Fin k) -> All p ts -> p (index i ts) + index FZ (x :: xs) = x + index (FS j) (x :: xs) = index j xs + + ||| Delete an element from an All at the given position. + ||| + ||| ```idris example + ||| > deleteAt 0 (the (HVect _) [1, "string"]) + ||| ["string"] + ||| ``` + export + deleteAt : (i : Fin (S l)) -> All p ts -> All p (deleteAt i ts) + deleteAt FZ (x :: xs) = xs + deleteAt (FS FZ) (x :: (y :: xs)) = x :: xs + deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs) + + ||| Replace an element in an All at the given position. + ||| + ||| ```idris example + ||| > replaceAt 0 "firstString" (the (HVect _) [1, "string"]) + ||| ["firstString", "string"] + ||| ``` + export + replaceAt : (i : Fin k) -> + (x : p t) -> + All p ts -> + All p (replaceAt i t ts) + replaceAt FZ y (x :: xs) = y :: xs + replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs + + ||| Update an element in an All at the given position. + ||| + ||| ```idris example + ||| > updateAt 0 (const True) (the (HVect _) [1, "string"]) + ||| [True, "string"] + ||| ``` + export + updateAt : (i : Fin k) -> + (p (index i ts) -> p t) -> + All p ts -> + All p (replaceAt i t ts) + updateAt FZ f (x :: xs) = f x :: xs + updateAt (FS j) f (x :: xs) = x :: updateAt j f xs + + ||| Extract an element of an All. + ||| + ||| ```idris example + ||| > get [1, "string"] {p = Here} + ||| 1 + ||| ``` + export + get : All p ts -> Elem x ts -> p x + get (x :: xs) Here = x + get (x :: xs) (There e') = get xs e' + + ||| Replace an element of an All. + ||| + ||| ```idris example + ||| > replaceElem 2 [1, "string"] + ||| [2, "string"] + ||| ``` + export + replaceElem : All p ts -> (e : Elem t ts) -> p t' -> All p (replaceByElem ts e t') + replaceElem (x :: xs) Here y = y :: xs + replaceElem (x :: xs) (There p') y = x :: replaceElem xs p' y + + ||| Update an element of an All. + ||| + ||| ```idris example + ||| > updateElem (const "hello world!") [1, "string"] + ||| [1, "hello world!"] + ||| ``` + public export + updateElem : {0 p : _} -> (p t -> p t') -> All p ts -> (e : Elem t ts) -> All p (replaceByElem ts e t') + updateElem f (x :: xs) Here = f x :: xs + updateElem f (x :: xs) (There p') = x :: updateElem f xs p' + diff --git a/libs/contrib/Data/Fun/Extra.idr b/libs/contrib/Data/Fun/Extra.idr index 191bd93c7a..adc01ddc16 100644 --- a/libs/contrib/Data/Fun/Extra.idr +++ b/libs/contrib/Data/Fun/Extra.idr @@ -2,7 +2,7 @@ module Data.Fun.Extra import Data.Fun import Data.Rel -import Data.HVect +import Data.Vect.Quantifiers %default total diff --git a/libs/contrib/Data/HVect.idr b/libs/contrib/Data/HVect.idr deleted file mode 100644 index 80a2ded2b5..0000000000 --- a/libs/contrib/Data/HVect.idr +++ /dev/null @@ -1,170 +0,0 @@ -module Data.HVect - -import Decidable.Equality -import Data.List -import public Data.Vect -import Data.Vect.Elem - -%default total - -||| Heterogeneous vectors where the type index gives, element-wise, -||| the types of the contents. -public export -data HVect : Vect k Type -> Type where - Nil : HVect [] - (::) : t -> HVect ts -> HVect (t :: ts) - -||| Extract an element from an HVect. -||| -||| ```idris example -||| > index 0 (the (HVect _) [1, "string"]) -||| 1 -||| ``` -public export -index : (i : Fin k) -> HVect ts -> index i ts -index FZ (x :: xs) = x -index (FS j) (x :: xs) = index j xs - -||| Delete an element from an HVect. -||| -||| ```idris example -||| > deleteAt 0 (the (HVect _) [1, "string"]) -||| ["string"] -||| ``` -public export -deleteAt : (i : Fin (S l)) -> HVect ts -> HVect (deleteAt i ts) -deleteAt FZ (x :: xs) = xs -deleteAt (FS FZ) (x :: (y :: xs)) = x :: xs -deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs) - -||| Replace an element in an HVect. -||| -||| ```idris example -||| > replaceAt 0 "firstString" (the (HVect _) [1, "string"]) -||| ["firstString", "string"] -||| ``` -public export -replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts) -replaceAt FZ y (x :: xs) = y :: xs -replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs - -||| Update an element in an HVect. -||| -||| ```idris example -||| > updateAt 0 (const True) (the (HVect _) [1, "string"]) -||| [True, "string"] -||| ``` -public export -updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts) -updateAt FZ f (x :: xs) = f x :: xs -updateAt (FS j) f (x :: xs) = x :: updateAt j f xs - -||| Append two `HVect`s. -||| -||| ```idris example -||| > (the (HVect _) [1]) ++ (the (HVect _) ["string"]) -||| [1, "string"] -||| ``` -public export -(++) : HVect ts -> HVect us -> HVect (ts ++ us) -(++) [] ys = ys -(++) (x :: xs) ys = x :: (xs ++ ys) - -public export -Eq (HVect []) where - [] == [] = True - -public export -(Eq t, Eq (HVect ts)) => Eq (HVect (t :: ts)) where - (x :: xs) == (y :: ys) = x == y && xs == ys - -public export -consInjective1 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (x :: xs = y :: ys) -> x = y -consInjective1 Refl = Refl - -public export -consInjective2 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (x :: xs = y :: ys) -> xs = ys -consInjective2 Refl = Refl - -public export -DecEq (HVect []) where - decEq [] [] = Yes Refl - -public export -(DecEq t, DecEq (HVect ts)) => DecEq (HVect (t :: ts)) where - decEq (x :: xs) (y :: ys) with (decEq x y) - decEq (z :: xs) (z :: ys) | Yes Refl with (decEq xs ys) - decEq (z :: zs) (z :: zs) | Yes Refl | Yes Refl = Yes Refl - decEq (z :: xs) (z :: ys) | Yes Refl | No contra = No (contra . consInjective2) - decEq (x :: xs) (y :: ys) | No contra = No (contra . consInjective1) - -public export -interface Shows k ts where - shows : HVect {k} ts -> Vect k String - -public export -Shows Z [] where - shows [] = [] - -public export -(Show t, Shows len ts) => Shows (S len) (t :: ts) where - shows (x :: xs) = show x :: shows xs - -public export -(Shows len ts) => Show (HVect ts) where - show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]" - -||| Extract an arbitrary element of the correct type. -||| -||| ```idris example -||| > get [1, "string"] {p = Here} -||| 1 -||| ``` -public export -get : (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> t -get (x :: xs) {p = Here} = x -get (x :: xs) {p = (There p')} = get xs - -||| Replace an element with the correct type. (Homogeneous) -||| -||| ```idris example -||| > put 2 [1, "string"] -||| [2, "string"] -||| ``` -public export -put : t -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect ts -put y (x :: xs) {p = Here} = y :: xs -put y (x :: xs) {p = (There p')} = x :: put y xs - -||| Replace an element with the correct type. (Heterogeneous) -||| -||| ```idris example -||| > htPut True [1, "string"] {p = Here} -||| [True, "string"] -||| ``` -public export -htPut : u -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u) -htPut y (x :: xs) {p = Here} = y :: xs -htPut y (x :: xs) {p = There p'} = x :: htPut y xs - -||| Update an element with the correct type. (Homogeneous) -||| -||| ```idris example -||| > update (const "hello world!") [1, "string"] -||| [1, "hello world!"] -||| ``` -public export -update : (t -> t) -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect ts -update f (x :: xs) {p = Here} = f x :: xs -update f (x :: xs) {p = There p'} = x :: update f xs - -||| Update an element with the correct type. (Heterogeneous) -||| -||| ```idris example -||| > htUpdate (\_ : String => 2) [1, "string"] -||| [1, 2] -||| ``` -public export -htUpdate : (t -> u) -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u) -htUpdate f (x :: xs) {p = Here} = f x :: xs -htUpdate f (x :: xs) {p = (There p')} = x :: htUpdate f xs diff --git a/libs/contrib/Data/Rel/Complement.idr b/libs/contrib/Data/Rel/Complement.idr index ae8813d261..9efb8b4a49 100644 --- a/libs/contrib/Data/Rel/Complement.idr +++ b/libs/contrib/Data/Rel/Complement.idr @@ -3,7 +3,7 @@ module Data.Rel.Complement import Data.Rel import Data.Fun import Data.Fun.Extra -import Data.HVect +import Data.Vect.Quantifiers %default total diff --git a/libs/contrib/Decidable/Decidable/Extra.idr b/libs/contrib/Decidable/Decidable/Extra.idr index aa0d124bcd..6b1c2ce316 100644 --- a/libs/contrib/Decidable/Decidable/Extra.idr +++ b/libs/contrib/Decidable/Decidable/Extra.idr @@ -4,7 +4,7 @@ import Data.Rel import Data.Rel.Complement import Data.Fun import Data.Vect -import Data.HVect +import Data.Vect.Quantifiers import Data.Fun.Extra import Decidable.Decidable diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 4b3765aff3..627d59fdc2 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -113,8 +113,6 @@ modules = Control.ANSI, Data.Void, - Data.HVect, - Debug.Buffer, Decidable.Finite.Fin, From 73f86f10ed966317f2b4d71a350605320bde64db Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Sun, 7 Jan 2024 20:22:10 -0600 Subject: [PATCH 2/3] Frex needs these public exported and that feels reasonable enough to me --- libs/base/Data/Vect/Quantifiers.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr index 936b1e7d46..50c8a7dd8b 100644 --- a/libs/base/Data/Vect/Quantifiers.idr +++ b/libs/base/Data/Vect/Quantifiers.idr @@ -284,12 +284,12 @@ namespace All HVect = All id ||| Take the first element. - export + public export head : All p (x :: xs) -> p x head (y :: _) = y ||| Take all but the first element. - export + public export tail : All p (x :: xs) -> All p xs tail (_ :: ys) = ys From 6ff9d92b6e55f6f91bf59e3a7388f1bbc79e4b4a Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Sun, 7 Jan 2024 20:34:47 -0600 Subject: [PATCH 3/3] Add CHANGELOG_NEXT entries --- CHANGELOG_NEXT.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index b61848bed5..dc92a53dee 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -39,9 +39,24 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * Added append `(++)` for `List` version of `All`. +* Moved helpers and theorems from contrib's `Data.HVect` into base's + `Data.Vect.Quantifiers.All` namespace. Some functions were renamed and some + already existed. Others had quantity changes -- in short, there were some + breaking changes here in addition to removing the respective functions from + contrib. If you hit a breaking change, please take a look at + [the PR](https://github.com/idris-lang/Idris2/pull/3191/files) and determine if you + simply need to update a function name or if your use-case requires additional + code changes in the base library. If it's the latter, open a bug ticket or + start a discussion on the Idris Discord to determine the best path forward. + #### Contrib * `Data.List.Lazy` was moved from `contrib` to `base`. * Existing `System.Console.GetOpt` was extended to support errors during options parsing in a backward-compatible way. + +* Moved helpers from `Data.HVect` to base library's `Data.Vect.Quantifiers.All` + and removed `Data.HVect` from contrib. See the additional notes in the + CHANGELOG under the `Library changes`/`Base` section above. +