From 004f1fd26bf0a4ab7b4df74ee97e8445258457fc Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Wed, 5 Jun 2024 11:51:23 +0100
Subject: [PATCH] [ new ] Data.SnocList.HasLength from compiler libs (#3299)

---
 libs/base/Data/Singleton.idr          |  4 ++
 libs/base/Data/SnocList/HasLength.idr | 70 +++++++++++++++++++++++++++
 libs/base/base.ipkg                   |  1 +
 3 files changed, 75 insertions(+)
 create mode 100644 libs/base/Data/SnocList/HasLength.idr

diff --git a/libs/base/Data/Singleton.idr b/libs/base/Data/Singleton.idr
index ad504c7a32..2eecee8984 100644
--- a/libs/base/Data/Singleton.idr
+++ b/libs/base/Data/Singleton.idr
@@ -6,6 +6,10 @@ public export
 data Singleton : a -> Type where
      Val : (x : a) -> Singleton x
 
+public export %inline
+reindex : (0 _ : x === y) -> Singleton x -> Singleton y
+reindex Refl x = x
+
 public export %inline
 unVal : Singleton {a} x -> a
 unVal $ Val x = x
diff --git a/libs/base/Data/SnocList/HasLength.idr b/libs/base/Data/SnocList/HasLength.idr
new file mode 100644
index 0000000000..dbb771aa2c
--- /dev/null
+++ b/libs/base/Data/SnocList/HasLength.idr
@@ -0,0 +1,70 @@
+module Data.SnocList.HasLength
+
+import Data.Nat
+import Data.SnocList
+
+---------------------------------------
+-- horrible hack
+import Data.List.HasLength as L
+
+public export
+LHasLength : Nat -> List a -> Type
+LHasLength = L.HasLength
+%hide L.HasLength
+---------------------------------------
+
+public export
+data HasLength : Nat -> SnocList a -> Type where
+  Z : HasLength Z [<]
+  S : HasLength n sa -> HasLength (S n) (sa :< a)
+
+export
+hasLength : HasLength n sx -> length sx === n
+hasLength Z = Refl
+hasLength (S p) = cong S (hasLength p)
+
+export
+map : (f : a -> b) -> HasLength n xs -> HasLength n (map f xs)
+map f Z = Z
+map f (S hl) = S (map f hl)
+
+export
+sucL : HasLength n sx -> HasLength (S n) ([<x] ++ sx)
+sucL Z     = S Z
+sucL (S n) = S (sucL n)
+
+export
+hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)
+hlAppend sx Z = sx
+hlAppend sx (S sy) = S (hlAppend sx sy)
+
+export
+hlFish : HasLength m sx -> LHasLength n ys -> HasLength (n + m) (sx <>< ys)
+hlFish x Z = x
+hlFish {n = S n} x (S y) = rewrite plusSuccRightSucc n m in hlFish (S x) y
+
+export
+mkHasLength : (sx : SnocList a) -> HasLength (length sx) sx
+mkHasLength [<] = Z
+mkHasLength (sx :< _) = S (mkHasLength sx)
+
+export
+hlChips : HasLength m sx -> LHasLength n ys -> LHasLength (m + n) (sx <>> ys)
+hlChips Z y = y
+hlChips {m = S m} {n} (S x) y
+  = rewrite plusSuccRightSucc m n in
+    hlChips x (S y)
+
+export
+cast : {sy : _} -> (0 _ : SnocList.length sx = SnocList.length sy) ->
+       HasLength m sx -> HasLength m sy
+cast {sy = [<]} eq Z = Z
+cast {sy = sy :< _} eq (S p) = S (cast (injective eq) p)
+
+hlReverseOnto : HasLength m acc -> HasLength n sx -> HasLength (m + n) (reverseOnto acc sx)
+hlReverseOnto p Z = rewrite plusZeroRightNeutral m in p
+hlReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hlReverseOnto (S p) q
+
+export
+hlReverse : HasLength m acc -> HasLength m (reverse acc)
+hlReverse = hlReverseOnto Z
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index efe2d1472a..603d6c6c55 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -77,6 +77,7 @@ modules = Control.App,
           Data.Singleton,
           Data.SnocList,
           Data.SnocList.Elem,
+          Data.SnocList.HasLength,
           Data.SnocList.Operations,
           Data.SnocList.Quantifiers,
           Data.So,