From 87b16a9b85d24ac57425f25057b9ea5282927933 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 16 Apr 2025 22:59:24 +0100 Subject: [PATCH 1/7] =?UTF-8?q?[=20re=20#2684=20]=C2=A0First=20bits?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/SnocList/Base.agda | 702 ++++++++++++++++++++++++++++++++++++ 1 file changed, 702 insertions(+) create mode 100644 src/Data/SnocList/Base.agda diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda new file mode 100644 index 0000000000..961eae6756 --- /dev/null +++ b/src/Data/SnocList/Base.agda @@ -0,0 +1,702 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- SnocLists, basic types and operations +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.SnocList.Base where + +{- +open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) +open import Data.Bool.Base as Bool + using (Bool; false; true; not; _∧_; _∨_; if_then_else_) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) +-} +open import Data.Nat.Base as ℕ using (ℕ; zero; suc) +{- +open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′) +open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) +open import Data.These.Base as These using (These; this; that; these) +open import Function.Base + using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip) +-} +open import Level using (Level) +{- +open import Relation.Unary using (Pred; Decidable) +open import Relation.Binary.Core using (Rel) +import Relation.Binary.Definitions as B +-} +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) +{- +open import Relation.Nullary.Decidable.Core using (T?; does; ¬?) +-} + +private + variable + a b c p ℓ : Level + A : Set a + B : Set b + C : Set c + +------------------------------------------------------------------------ +-- Types + +-- Standard lists grow on the left and are know as `forwards' lists +-- because their elements are traversed left-to-right. For didactic +-- reasons we rename the type and its constructors in this module so +-- that the type constructor (List>) and the data constructors ([>] +-- and _▸_) all explicitly mention the forwards direction. + +open import Data.List.Base as List> + using () + renaming ( List to List> + ; [] to [>] + ; _∷_ to _▸_ + ) + +-- A backwards list (also as snoc list because `snoc' is `cons' backwards) +-- is a list that grows on the right, and that is therefore traversed +-- right-to-left. + +infixl 5 _◂_ + +data List< (A : Set a) : Set a where + [<] : List< A + _◂_ : List< A → A → List< A + +------------------------------------------------------------------------ +-- Operations interacting with lists +-- +-- When representing a position in the middle of list (no matter what its +-- direction is), it is convenient to use a pair of a backwards list on +-- the left of the position and a forwards one on its right. This way we +-- can move the position around either left or right by moving values +-- from one list to the other. +-- +-- E.g. if we want to move the position {HERE} one step to the left in +-- the list [1, 2, {HERE}, 3, 4] then we need to be able to take 2 +-- out of the right end of the list on the left and push it onto the left +-- end of the list on the right to obtain [1, {HERE}, 2, 3, 4]. +-- +-- This can be done efficiently if my representation on the left is +-- right-to-left and so gives me constant time access to its right end +-- and vice-versa for the representation on the right. +-- +-- The following operations describe how to combine [<1, 2] and +-- [> 3, 4] in a position-respecting manner to obtain a forwards +-- or backwards list respectively. +-- +-- These all use the same mnemonic: the symbol used for the operation +-- spells out the direction of the consecutive input lists as well as +-- that of the output. +-- +-- E.g. the string for the fish operator "<><" spells out +-- "backwards forwards backwards" and so it: +-- 1. takes a backwards list as its first argument +-- 2. takes a forwards list as its second argument +-- 3. returns a backwards list + +infixl 5 _<><_ +infixr 6 _<>>_ + +-- Fish +_<><_ : List< A → List> A → List< A +sx <>< [>] = sx +sx <>< (x ▸ xs) = (sx ◂ x) <>< xs + +-- Chips +_<>>_ : List< A → List> A → List> A +[<] <>> xs = xs +(sx ◂ x) <>> xs = sx <>> (x ▸ xs) + +private + + [<1,2] : List< ℕ + [<1,2] = [<] ◂ 1 ◂ 2 + + [>3,4] : List> ℕ + [>3,4] = 3 ▸ 4 ▸ [>] + + [<1,2,3,4] : List< ℕ + [<1,2,3,4] = [<] ◂ 1 ◂ 2 ◂ 3 ◂ 4 + + [>1,2,3,4] : List> ℕ + [>1,2,3,4] = 1 ▸ 2 ▸ 3 ▸ 4 ▸ [>] + + -- Order-preserving combination producing a backwards list + _ : [<1,2] <>< [>3,4] ≡ [<1,2,3,4] + _ = refl + + -- Order-preserving combination producing a forwards list + _ : [<1,2] <>> [>3,4] ≡ [>1,2,3,4] + _ = refl + +------------------------------------------------------------------------ +-- Operations to transform snoc lists + +map : (A → B) → List< A → List< B +map f [<] = [<] +map f (sx ◂ x) = map f sx ◂ f x + +{- +infixr 5 _++_ + +_++_ : List A → List A → List A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ (xs ++ ys) + +intersperse : A → List A → List A +intersperse x [] = [] +intersperse x (y ∷ []) = y ∷ [] +intersperse x (y ∷ ys) = y ∷ x ∷ intersperse x ys + +intercalate : List A → List (List A) → List A +intercalate xs [] = [] +intercalate xs (ys ∷ []) = ys +intercalate xs (ys ∷ yss) = ys ++ xs ++ intercalate xs yss + +cartesianProductWith : (A → B → C) → List A → List B → List C +cartesianProductWith f [] _ = [] +cartesianProductWith f (x ∷ xs) ys = map (f x) ys ++ cartesianProductWith f xs ys + +cartesianProduct : List A → List B → List (A × B) +cartesianProduct = cartesianProductWith _,_ + +------------------------------------------------------------------------ +-- Aligning and zipping + +alignWith : (These A B → C) → List A → List B → List C +alignWith f [] bs = map (f ∘′ that) bs +alignWith f as [] = map (f ∘′ this) as +alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ alignWith f as bs + +zipWith : (A → B → C) → List A → List B → List C +zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys +zipWith f _ _ = [] + +unalignWith : (A → These B C) → List A → List B × List C +unalignWith f [] = [] , [] +unalignWith f (a ∷ as) with f a +... | this b = Product.map₁ (b ∷_) (unalignWith f as) +... | that c = Product.map₂ (c ∷_) (unalignWith f as) +... | these b c = Product.map (b ∷_) (c ∷_) (unalignWith f as) + +unzipWith : (A → B × C) → List A → List B × List C +unzipWith f [] = [] , [] +unzipWith f (xy ∷ xys) = Product.zip _∷_ _∷_ (f xy) (unzipWith f xys) + +partitionSumsWith : (A → B ⊎ C) → List A → List B × List C +partitionSumsWith f = unalignWith (These.fromSum ∘′ f) + +align : List A → List B → List (These A B) +align = alignWith id + +zip : List A → List B → List (A × B) +zip = zipWith (_,_) + +unalign : List (These A B) → List A × List B +unalign = unalignWith id + +unzip : List (A × B) → List A × List B +unzip = unzipWith id + +partitionSums : List (A ⊎ B) → List A × List B +partitionSums = partitionSumsWith id + +merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A +merge R? [] ys = ys +merge R? xs [] = xs +merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y) + then x ∷ merge R? xs y∷ys + else y ∷ merge R? x∷xs ys + +------------------------------------------------------------------------ +-- Operations for reducing lists + +foldr : (A → B → B) → B → List A → B +foldr c n [] = n +foldr c n (x ∷ xs) = c x (foldr c n xs) + +foldl : (A → B → A) → A → List B → A +foldl c n [] = n +foldl c n (x ∷ xs) = foldl c (c n x) xs + +concat : List (List A) → List A +concat = foldr _++_ [] + +concatMap : (A → List B) → List A → List B +concatMap f = concat ∘ map f + +ap : List (A → B) → List A → List B +ap fs as = concatMap (flip map as) fs + +catMaybes : List (Maybe A) → List A +catMaybes = foldr (maybe′ _∷_ id) [] + +mapMaybe : (A → Maybe B) → List A → List B +mapMaybe p = catMaybes ∘ map p + +null : List A → Bool +null [] = true +null (x ∷ xs) = false + +length : List A → ℕ +length = foldr (const suc) 0 + +------------------------------------------------------------------------ +-- Operations for constructing lists + +[_] : A → List A +[ x ] = x ∷ [] + +fromMaybe : Maybe A → List A +fromMaybe (just x) = [ x ] +fromMaybe nothing = [] + +replicate : ℕ → A → List A +replicate zero x = [] +replicate (suc n) x = x ∷ replicate n x + +iterate : (A → A) → A → ℕ → List A +iterate f e zero = [] +iterate f e (suc n) = e ∷ iterate f (f e) n + +inits : List A → List (List A) +inits {A = A} = λ xs → [] ∷ tail xs + module Inits where + tail : List A → List (List A) + tail [] = [] + tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail xs) + +tails : List A → List (List A) +tails {A = A} = λ xs → xs ∷ tail xs + module Tails where + tail : List A → List (List A) + tail [] = [] + tail (_ ∷ xs) = xs ∷ tail xs + +insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A +insertAt xs zero v = v ∷ xs +insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v + +updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A +updateAt (x ∷ xs) zero f = f x ∷ xs +updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f + +-- Tabulation + +applyUpTo : (ℕ → A) → ℕ → List A +applyUpTo f zero = [] +applyUpTo f (suc n) = f zero ∷ applyUpTo (f ∘ suc) n + +applyDownFrom : (ℕ → A) → ℕ → List A +applyDownFrom f zero = [] +applyDownFrom f (suc n) = f n ∷ applyDownFrom f n + +tabulate : ∀ {n} (f : Fin n → A) → List A +tabulate {n = zero} f = [] +tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc) + +lookup : ∀ (xs : List A) → Fin (length xs) → A +lookup (x ∷ xs) zero = x +lookup (x ∷ xs) (suc i) = lookup xs i + +-- Numerical + +upTo : ℕ → List ℕ +upTo = applyUpTo id + +downFrom : ℕ → List ℕ +downFrom = applyDownFrom id + +allFin : ∀ n → List (Fin n) +allFin n = tabulate id + +unfold : ∀ (P : ℕ → Set b) + (f : ∀ {n} → P (suc n) → Maybe (A × P n)) → + ∀ {n} → P n → List A +unfold P f {n = zero} s = [] +unfold P f {n = suc n} s = maybe′ (λ (x , s′) → x ∷ unfold P f s′) [] (f s) + +------------------------------------------------------------------------ +-- Operations for reversing lists + +reverseAcc : List A → List A → List A +reverseAcc = foldl (flip _∷_) + +reverse : List A → List A +reverse = reverseAcc [] + +-- "Reverse append" xs ʳ++ ys = reverse xs ++ ys + +infixr 5 _ʳ++_ + +_ʳ++_ : List A → List A → List A +_ʳ++_ = flip reverseAcc + +-- Snoc: Cons, but from the right. + +infixl 6 _∷ʳ_ + +_∷ʳ_ : List A → A → List A +xs ∷ʳ x = xs ++ [ x ] + + + +-- Backwards initialisation + +infixl 5 _∷ʳ′_ + +data InitLast {A : Set a} : List A → Set a where + [] : InitLast [] + _∷ʳ′_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x) + +initLast : (xs : List A) → InitLast xs +initLast [] = [] +initLast (x ∷ xs) with initLast xs +... | [] = [] ∷ʳ′ x +... | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y + +-- uncons, but from the right +unsnoc : List A → Maybe (List A × A) +unsnoc as with initLast as +... | [] = nothing +... | xs ∷ʳ′ x = just (xs , x) + +------------------------------------------------------------------------ +-- Operations for deconstructing lists + +-- Note that although the following three combinators can be useful for +-- programming, when proving it is often a better idea to manually +-- destruct a list argument as each branch of the pattern-matching will +-- have a refined type. + +uncons : List A → Maybe (A × List A) +uncons [] = nothing +uncons (x ∷ xs) = just (x , xs) + +head : List A → Maybe A +head [] = nothing +head (x ∷ _) = just x + +tail : List A → Maybe (List A) +tail [] = nothing +tail (_ ∷ xs) = just xs + +last : List A → Maybe A +last [] = nothing +last (x ∷ []) = just x +last (_ ∷ xs) = last xs + +take : ℕ → List A → List A +take zero xs = [] +take (suc n) [] = [] +take (suc n) (x ∷ xs) = x ∷ take n xs + +drop : ℕ → List A → List A +drop zero xs = xs +drop (suc n) [] = [] +drop (suc n) (x ∷ xs) = drop n xs + +splitAt : ℕ → List A → List A × List A +splitAt zero xs = ([] , xs) +splitAt (suc n) [] = ([] , []) +splitAt (suc n) (x ∷ xs) = Product.map₁ (x ∷_) (splitAt n xs) + +removeAt : (xs : List A) → Fin (length xs) → List A +removeAt (x ∷ xs) zero = xs +removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i + +------------------------------------------------------------------------ +-- Operations for filtering lists + +-- The following are a variety of functions that can be used to +-- construct sublists using a predicate. +-- +-- Each function has two forms. The first main variant uses a +-- proof-relevant decidable predicate, while the second variant uses +-- a irrelevant boolean predicate and are suffixed with a `ᵇ` character, +-- typed as \^b. +-- +-- The decidable versions have several advantages: 1) easier to prove +-- properties, 2) better meta-variable inference and 3) most of the rest +-- of the library is set-up to work with decidable predicates. However, +-- in rare cases the boolean versions can be useful, mainly when one +-- wants to minimise dependencies. +-- +-- In summary, in most cases you probably want to use the decidable +-- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) xs` +-- rather than `takeWhileᵇ (_≤ᵇ 10) xs`. + +takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +takeWhile P? [] = [] +takeWhile P? (x ∷ xs) with does (P? x) +... | true = x ∷ takeWhile P? xs +... | false = [] + +takeWhileᵇ : (A → Bool) → List A → List A +takeWhileᵇ p = takeWhile (T? ∘ p) + +dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +dropWhile P? [] = [] +dropWhile P? (x ∷ xs) with does (P? x) +... | true = dropWhile P? xs +... | false = x ∷ xs + +dropWhileᵇ : (A → Bool) → List A → List A +dropWhileᵇ p = dropWhile (T? ∘ p) + +filter : ∀ {P : Pred A p} → Decidable P → List A → List A +filter P? [] = [] +filter P? (x ∷ xs) with does (P? x) +... | false = filter P? xs +... | true = x ∷ filter P? xs + +filterᵇ : (A → Bool) → List A → List A +filterᵇ p = filter (T? ∘ p) + +partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +partition P? [] = ([] , []) +partition P? (x ∷ xs) with does (P? x) | partition P? xs +... | true | (ys , zs) = (x ∷ ys , zs) +... | false | (ys , zs) = (ys , x ∷ zs) + +partitionᵇ : (A → Bool) → List A → List A × List A +partitionᵇ p = partition (T? ∘ p) + +span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +span P? [] = ([] , []) +span P? ys@(x ∷ xs) with does (P? x) +... | true = Product.map (x ∷_) id (span P? xs) +... | false = ([] , ys) + + +spanᵇ : (A → Bool) → List A → List A × List A +spanᵇ p = span (T? ∘ p) + +break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +break P? = span (¬? ∘ P?) + +breakᵇ : (A → Bool) → List A → List A × List A +breakᵇ p = break (T? ∘ p) + +-- The predicate `P` represents the notion of newline character for the +-- type `A`. It is used to split the input list into a list of lines. +-- Some lines may be empty if the input contains at least two +-- consecutive newline characters. +linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +linesBy {A = A} P? = go nothing where + + go : Maybe (List A) → List A → List (List A) + go acc [] = maybe′ ([_] ∘′ reverse) [] acc + go acc (c ∷ cs) = if does (P? c) + then reverse acc′ ∷ go nothing cs + else go (just (c ∷ acc′)) cs + where acc′ = Maybe.fromMaybe [] acc + +linesByᵇ : (A → Bool) → List A → List (List A) +linesByᵇ p = linesBy (T? ∘ p) + +-- The predicate `P` represents the notion of space character for the +-- type `A`. It is used to split the input list into a list of words. +-- All the words are non empty and the output does not contain any space +-- characters. +wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +wordsBy {A = A} P? = go [] where + + cons : List A → List (List A) → List (List A) + cons [] ass = ass + cons as ass = reverse as ∷ ass + + go : List A → List A → List (List A) + go acc [] = cons acc [] + go acc (c ∷ cs) = if does (P? c) + then cons acc (go [] cs) + else go (c ∷ acc) cs + +wordsByᵇ : (A → Bool) → List A → List (List A) +wordsByᵇ p = wordsBy (T? ∘ p) + +derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A +derun R? [] = [] +derun R? (x ∷ []) = x ∷ [] +derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs +... | true | ys = ys +... | false | ys = x ∷ ys + +derunᵇ : (A → A → Bool) → List A → List A +derunᵇ r = derun (T? ∘₂ r) + +deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A +deduplicate R? [] = [] +deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs) + +deduplicateᵇ : (A → A → Bool) → List A → List A +deduplicateᵇ r = deduplicate (T? ∘₂ r) + +-- Finds the first element satisfying the boolean predicate +find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A +find P? [] = nothing +find P? (x ∷ xs) = if does (P? x) then just x else find P? xs + +findᵇ : (A → Bool) → List A → Maybe A +findᵇ p = find (T? ∘ p) + +-- Finds the index of the first element satisfying the boolean predicate +findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs) +findIndex P? [] = nothing +findIndex P? (x ∷ xs) = if does (P? x) + then just zero + else Maybe.map suc (findIndex P? xs) + +findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs) +findIndexᵇ p = findIndex (T? ∘ p) + +-- Finds indices of all the elements satisfying the boolean predicate +findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs) +findIndices P? [] = [] +findIndices P? (x ∷ xs) = if does (P? x) + then zero ∷ indices + else indices + where indices = map suc (findIndices P? xs) + +findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs) +findIndicesᵇ p = findIndices (T? ∘ p) + +------------------------------------------------------------------------ +-- Actions on single elements + +infixl 5 _[_]%=_ _[_]∷=_ + +-- xs [ i ]%= f modifies the i-th element of xs according to f + +_[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A +xs [ i ]%= f = updateAt xs i f + +-- xs [ i ]≔ y overwrites the i-th element of xs with y + +_[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A +xs [ k ]∷= v = xs [ k ]%= const v + +------------------------------------------------------------------------ +-- Conditional versions of cons and snoc + +infixr 5 _?∷_ +_?∷_ : Maybe A → List A → List A +_?∷_ = maybe′ _∷_ id + +infixl 6 _∷ʳ?_ +_∷ʳ?_ : List A → Maybe A → List A +xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x + +------------------------------------------------------------------------ +-- Raw algebraic bundles + +module _ (A : Set a) where + ++-rawMagma : RawMagma a _ + ++-rawMagma = record + { Carrier = List A + ; _≈_ = _≡_ + ; _∙_ = _++_ + } + + ++-[]-rawMonoid : RawMonoid a _ + ++-[]-rawMonoid = record + { Carrier = List A + ; _≈_ = _≡_ + ; _∙_ = _++_ + ; ε = [] + } + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 1.4 + +infixl 5 _∷ʳ'_ +_∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x) +_∷ʳ'_ = InitLast._∷ʳ′_ +{-# WARNING_ON_USAGE _∷ʳ'_ +"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. +Please use _∷ʳ′_ (ending in a prime) instead." +#-} + +-- Version 2.0 + +infixl 5 _─_ +_─_ = removeAt +{-# WARNING_ON_USAGE _─_ +"Warning: _─_ was deprecated in v2.0. +Please use removeAt instead." +#-} + +-- Version 2.1 + +scanr : (A → B → B) → B → List A → List B +scanr f e [] = e ∷ [] +scanr f e (x ∷ xs) with scanr f e xs +... | [] = [] -- dead branch +... | ys@(y ∷ _) = f x y ∷ ys +{-# WARNING_ON_USAGE scanr +"Warning: scanr was deprecated in v2.1. +Please use Data.List.Scans.Base.scanr instead." +#-} + +scanl : (A → B → A) → A → List B → List A +scanl f e [] = e ∷ [] +scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs +{-# WARNING_ON_USAGE scanl +"Warning: scanl was deprecated in v2.1. +Please use Data.List.Scans.Base.scanl instead." +#-} + +-- Version 2.3 + +and : List Bool → Bool +and = foldr _∧_ true + +all : (A → Bool) → List A → Bool +all p = and ∘ map p +{-# WARNING_ON_USAGE and +"Warning: and was deprecated in v2.3. +Please use Data.Bool.ListAction.and instead." +#-} +{-# WARNING_ON_USAGE all +"Warning: all was deprecated in v2.3. +Please use Data.Nat.ListAction.all instead." +#-} + +or : List Bool → Bool +or = foldr _∨_ false + +any : (A → Bool) → List A → Bool +any p = or ∘ map p +{-# WARNING_ON_USAGE or +"Warning: or was deprecated in v2.3. +Please use Data.Bool.ListAction.or instead." +#-} +{-# WARNING_ON_USAGE any +"Warning: any was deprecated in v2.3. +Please use Data.Bool.ListAction.any instead." +#-} + +sum : List ℕ → ℕ +sum = foldr ℕ._+_ 0 +{-# WARNING_ON_USAGE sum +"Warning: sum was deprecated in v2.3. +Please use Data.Nat.ListAction.sum instead." +#-} + +product : List ℕ → ℕ +product = foldr ℕ._*_ 1 +{-# WARNING_ON_USAGE product +"Warning: product was deprecated in v2.3. +Please use Data.Nat.ListAction.product instead." +#-} +-} From 360e2c48f9a876433b1e6973a032dcf1200b404b Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Apr 2026 14:29:18 +0100 Subject: [PATCH 2/7] [ more ] content --- src/Data/SnocList/Base.agda | 509 ++++++++++++++++-------------------- 1 file changed, 219 insertions(+), 290 deletions(-) diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda index 961eae6756..18b8fd8b4b 100644 --- a/src/Data/SnocList/Base.agda +++ b/src/Data/SnocList/Base.agda @@ -10,29 +10,26 @@ module Data.SnocList.Base where {- open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) -open import Data.Bool.Base as Bool - using (Bool; false; true; not; _∧_; _∨_; if_then_else_) +-} +open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) --} open import Data.Nat.Base as ℕ using (ℕ; zero; suc) -{- -open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′) -open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) +open import Data.Product.Base as Product using (_×_; _,_) +open import Data.Sum.Base as Sum using (_⊎_) open import Data.These.Base as These using (These; this; that; these) -open import Function.Base - using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip) --} +open import Function.Base using (id; _∘′_; flip; _$′_; const) + +-- using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip) open import Level using (Level) {- open import Relation.Unary using (Pred; Decidable) +-} open import Relation.Binary.Core using (Rel) import Relation.Binary.Definitions as B --} open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -{- -open import Relation.Nullary.Decidable.Core using (T?; does; ¬?) --} +open import Relation.Nullary.Decidable.Core using (does) -- (T?; does; ¬?) + private variable @@ -48,24 +45,28 @@ private -- because their elements are traversed left-to-right. For didactic -- reasons we rename the type and its constructors in this module so -- that the type constructor (List>) and the data constructors ([>] --- and _▸_) all explicitly mention the forwards direction. +-- and _:>_) all explicitly mention the forwards direction. open import Data.List.Base as List> using () renaming ( List to List> ; [] to [>] - ; _∷_ to _▸_ + ; _∷_ to _:>_ ) + public --- A backwards list (also as snoc list because `snoc' is `cons' backwards) --- is a list that grows on the right, and that is therefore traversed --- right-to-left. +-- A backwards list (also known as a snoc list in the literature +-- because `snoc' is `cons' backwards is a list that grows on the +-- right, and that is therefore traversed right-to-left. -infixl 5 _◂_ +-- :> a right-to-left cons +-- <: its mirror image to get a left-to-right cons (aka snoc) + +infixl 5 _<:_ data List< (A : Set a) : Set a where [<] : List< A - _◂_ : List< A → A → List< A + _<:_ : List< A → A → List< A ------------------------------------------------------------------------ -- Operations interacting with lists @@ -73,16 +74,16 @@ data List< (A : Set a) : Set a where -- When representing a position in the middle of list (no matter what its -- direction is), it is convenient to use a pair of a backwards list on -- the left of the position and a forwards one on its right. This way we --- can move the position around either left or right by moving values --- from one list to the other. +-- can move the position around either left or right in contant time +-- by moving values from one list to the other. -- -- E.g. if we want to move the position {HERE} one step to the left in -- the list [1, 2, {HERE}, 3, 4] then we need to be able to take 2 -- out of the right end of the list on the left and push it onto the left -- end of the list on the right to obtain [1, {HERE}, 2, 3, 4]. -- --- This can be done efficiently if my representation on the left is --- right-to-left and so gives me constant time access to its right end +-- This can be done efficiently if the representation on the left is +-- right-to-left and so gives us constant time access to its right end -- and vice-versa for the representation on the right. -- -- The following operations describe how to combine [<1, 2] and @@ -99,32 +100,32 @@ data List< (A : Set a) : Set a where -- 2. takes a forwards list as its second argument -- 3. returns a backwards list -infixl 5 _<><_ -infixr 6 _<>>_ - -- Fish +infixl 5 _<><_ _<><_ : List< A → List> A → List< A sx <>< [>] = sx -sx <>< (x ▸ xs) = (sx ◂ x) <>< xs +sx <>< (x :> xs) = (sx <: x) <>< xs --- Chips +-- Chips (is Fish's best friend) +infixr 6 _<>>_ _<>>_ : List< A → List> A → List> A [<] <>> xs = xs -(sx ◂ x) <>> xs = sx <>> (x ▸ xs) +(sx <: x) <>> xs = sx <>> (x :> xs) +-- Some examples showing that these operations are order-preserving. private [<1,2] : List< ℕ - [<1,2] = [<] ◂ 1 ◂ 2 + [<1,2] = [<] <: 1 <: 2 [>3,4] : List> ℕ - [>3,4] = 3 ▸ 4 ▸ [>] + [>3,4] = 3 :> 4 :> [>] [<1,2,3,4] : List< ℕ - [<1,2,3,4] = [<] ◂ 1 ◂ 2 ◂ 3 ◂ 4 + [<1,2,3,4] = [<] <: 1 <: 2 <: 3 <: 4 [>1,2,3,4] : List> ℕ - [>1,2,3,4] = 1 ▸ 2 ▸ 3 ▸ 4 ▸ [>] + [>1,2,3,4] = 1 :> 2 :> 3 :> 4 :> [>] -- Order-preserving combination producing a backwards list _ : [<1,2] <>< [>3,4] ≡ [<1,2,3,4] @@ -134,214 +135,231 @@ private _ : [<1,2] <>> [>3,4] ≡ [>1,2,3,4] _ = refl +toList> : List< A → List> A +toList> = _<>> [>] + +fromList> : List> A → List< A +fromList> = [<] <><_ + ------------------------------------------------------------------------ -- Operations to transform snoc lists map : (A → B) → List< A → List< B map f [<] = [<] -map f (sx ◂ x) = map f sx ◂ f x - -{- -infixr 5 _++_ +map f (sx <: x) = map f sx <: f x -_++_ : List A → List A → List A -[] ++ ys = ys -(x ∷ xs) ++ ys = x ∷ (xs ++ ys) +infixl 5 _++_ +_++_ : List< A → List< A → List< A +xs ++ [<] = xs +xs ++ (ys <: x) = (xs ++ ys) <: x -intersperse : A → List A → List A -intersperse x [] = [] -intersperse x (y ∷ []) = y ∷ [] -intersperse x (y ∷ ys) = y ∷ x ∷ intersperse x ys +intersperse : A → List< A → List< A +intersperse x [<] = [<] +intersperse x xs@([<] <: _) = xs +intersperse x (ys <: y) = intersperse x ys <: x <: y -intercalate : List A → List (List A) → List A -intercalate xs [] = [] -intercalate xs (ys ∷ []) = ys -intercalate xs (ys ∷ yss) = ys ++ xs ++ intercalate xs yss +intercalate : List< A → List< (List< A) → List< A +intercalate xs [<] = [<] +intercalate xs ([<] <: ys) = ys +intercalate xs (yss <: ys) = intercalate xs yss ++ xs ++ ys -cartesianProductWith : (A → B → C) → List A → List B → List C -cartesianProductWith f [] _ = [] -cartesianProductWith f (x ∷ xs) ys = map (f x) ys ++ cartesianProductWith f xs ys +cartesianProductWith : (A → B → C) → List< A → List< B → List< C +cartesianProductWith f [<] _ = [<] +cartesianProductWith f (xs <: x) ys = cartesianProductWith f xs ys ++ map (f x) ys -cartesianProduct : List A → List B → List (A × B) +cartesianProduct : List< A → List< B → List< (A × B) cartesianProduct = cartesianProductWith _,_ ------------------------------------------------------------------------ -- Aligning and zipping -alignWith : (These A B → C) → List A → List B → List C -alignWith f [] bs = map (f ∘′ that) bs -alignWith f as [] = map (f ∘′ this) as -alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ alignWith f as bs +alignWith : (These A B → C) → List< A → List< B → List< C +alignWith f [<] bs = map (f ∘′ that) bs +alignWith f as [<] = map (f ∘′ this) as +alignWith f (as <: a) (bs <: b) = alignWith f as bs <: f (these a b) -zipWith : (A → B → C) → List A → List B → List C -zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys -zipWith f _ _ = [] +zipWith : (A → B → C) → List< A → List< B → List< C +zipWith f (xs <: x) (ys <: y) = zipWith f xs ys <: f x y +zipWith f _ _ = [<] -unalignWith : (A → These B C) → List A → List B × List C -unalignWith f [] = [] , [] -unalignWith f (a ∷ as) with f a -... | this b = Product.map₁ (b ∷_) (unalignWith f as) -... | that c = Product.map₂ (c ∷_) (unalignWith f as) -... | these b c = Product.map (b ∷_) (c ∷_) (unalignWith f as) +unalignWith : (A → These B C) → List< A → List< B × List< C +unalignWith f [<] = [<] , [<] +unalignWith f (as <: a) with f a +... | this b = Product.map₁ (_<: b) (unalignWith f as) +... | that c = Product.map₂ (_<: c) (unalignWith f as) +... | these b c = Product.map (_<: b) (_<: c) (unalignWith f as) -unzipWith : (A → B × C) → List A → List B × List C -unzipWith f [] = [] , [] -unzipWith f (xy ∷ xys) = Product.zip _∷_ _∷_ (f xy) (unzipWith f xys) +unzipWith : (A → B × C) → List< A → List< B × List< C +unzipWith f [<] = [<] , [<] +unzipWith f (xys <: xy) = Product.zip _<:_ _<:_ (unzipWith f xys) (f xy) -partitionSumsWith : (A → B ⊎ C) → List A → List B × List C +partitionSumsWith : (A → B ⊎ C) → List< A → List< B × List< C partitionSumsWith f = unalignWith (These.fromSum ∘′ f) -align : List A → List B → List (These A B) +align : List< A → List< B → List< (These A B) align = alignWith id -zip : List A → List B → List (A × B) +zip : List< A → List< B → List< (A × B) zip = zipWith (_,_) -unalign : List (These A B) → List A × List B +unalign : List< (These A B) → List< A × List< B unalign = unalignWith id -unzip : List (A × B) → List A × List B +unzip : List< (A × B) → List< A × List< B unzip = unzipWith id -partitionSums : List (A ⊎ B) → List A × List B +partitionSums : List< (A ⊎ B) → List< A × List< B partitionSums = partitionSumsWith id -merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A -merge R? [] ys = ys -merge R? xs [] = xs -merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y) - then x ∷ merge R? xs y∷ys - else y ∷ merge R? x∷xs ys +merge : {R : Rel A ℓ} → B.Decidable R → List< A → List< A → List< A +merge R? [<] ys = ys +merge R? xs [<] = xs +merge R? xsx@(xs <: x) ysy@(ys <: y) = if does (R? x y) + then merge R? xs ysy <: x + else merge R? xsx ys <: y ------------------------------------------------------------------------ -- Operations for reducing lists -foldr : (A → B → B) → B → List A → B -foldr c n [] = n -foldr c n (x ∷ xs) = c x (foldr c n xs) +foldr : (A → B → B) → B → List< A → B +foldr c n [<] = n +foldr c n (xs <: x) = foldr c (c x n) xs -foldl : (A → B → A) → A → List B → A -foldl c n [] = n -foldl c n (x ∷ xs) = foldl c (c n x) xs +foldl : (A → B → A) → A → List< B → A +foldl c n [<] = n +foldl c n (xs <: x) = c (foldl c n xs) x -concat : List (List A) → List A -concat = foldr _++_ [] +concat : List< (List< A) → List< A +concat = foldl _++_ [<] -concatMap : (A → List B) → List A → List B -concatMap f = concat ∘ map f +_ : concat ([<] <: [<1,2] <: (fromList> [>3,4])) ≡ [<1,2,3,4] +_ = refl -ap : List (A → B) → List A → List B +concatMap : (A → List< B) → List< A → List< B +concatMap f = concat ∘′ map f + +-- Both List>.concatMap & List<.concatMap behave the same +_ : (concatMap (λ n → [<] <: n <: suc n) [<1,2,3,4]) <>> [>] + ≡ List>.concatMap (λ n → n :> suc n :> [>]) ([<1,2,3,4] <>> [>]) +_ = refl + +ap : List< (A → B) → List< A → List< B ap fs as = concatMap (flip map as) fs -catMaybes : List (Maybe A) → List A -catMaybes = foldr (maybe′ _∷_ id) [] +catMaybes : List< (Maybe A) → List< A +catMaybes = foldl (flip $′ maybe′ (flip _<:_) id) [<] -mapMaybe : (A → Maybe B) → List A → List B -mapMaybe p = catMaybes ∘ map p +_ : let trash = [<] <: nothing in + catMaybes (trash ++ map just [<1,2,3,4] ++ trash) ≡ [<1,2,3,4] +_ = refl -null : List A → Bool -null [] = true -null (x ∷ xs) = false +mapMaybe : (A → Maybe B) → List< A → List< B +mapMaybe p = catMaybes ∘′ map p -length : List A → ℕ -length = foldr (const suc) 0 +null : List< A → Bool +null [<] = true +null (_ <: _) = false + +length : List< A → ℕ +length = foldl (flip $′ const suc) 0 ------------------------------------------------------------------------ -- Operations for constructing lists -[_] : A → List A -[ x ] = x ∷ [] - -fromMaybe : Maybe A → List A -fromMaybe (just x) = [ x ] -fromMaybe nothing = [] +fromMaybe : Maybe A → List< A +fromMaybe (just x) = [<] <: x +fromMaybe nothing = [<] -replicate : ℕ → A → List A -replicate zero x = [] -replicate (suc n) x = x ∷ replicate n x +replicate : ℕ → A → List< A +replicate zero x = [<] +replicate (suc n) x = replicate n x <: x -iterate : (A → A) → A → ℕ → List A -iterate f e zero = [] -iterate f e (suc n) = e ∷ iterate f (f e) n +iterate : (A → A) → A → ℕ → List< A +iterate f e zero = [<] +iterate f e (suc n) = iterate f (f e) n <: e -inits : List A → List (List A) -inits {A = A} = λ xs → [] ∷ tail xs +inits : List< A → List< (List< A) +inits {A = A} = λ xs → tail xs <: [<] module Inits where - tail : List A → List (List A) - tail [] = [] - tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail xs) + tail : List< A → List< (List< A) + tail [<] = [<] + tail (xs <: x) = map (_<: x) (tail xs) <: ([<] <: x) -tails : List A → List (List A) -tails {A = A} = λ xs → xs ∷ tail xs +tails : List< A → List< (List< A) +tails {A = A} = λ xs → tail xs <: xs module Tails where - tail : List A → List (List A) - tail [] = [] - tail (_ ∷ xs) = xs ∷ tail xs + tail : List< A → List< (List< A) + tail [<] = [<] + tail (xs <: _) = tail xs <: xs -insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A -insertAt xs zero v = v ∷ xs -insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v +insertAt : (xs : List< A) → Fin (suc (length xs)) → A → List< A +insertAt xs zero v = xs <: v +insertAt (xs <: x) (suc i) v = insertAt xs i v <: x -updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A -updateAt (x ∷ xs) zero f = f x ∷ xs -updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f +updateAt : (xs : List< A) → Fin (length xs) → (A → A) → List< A +updateAt (xs <: x) zero f = xs <: f x +updateAt (xs <: x) (suc i) f = updateAt xs i f <: x --- Tabulation +lookup : ∀ (xs : List< A) → Fin (length xs) → A +lookup (xs <: x) zero = x +lookup (xs <: x) (suc i) = lookup xs i -applyUpTo : (ℕ → A) → ℕ → List A -applyUpTo f zero = [] -applyUpTo f (suc n) = f zero ∷ applyUpTo (f ∘ suc) n +-- Tabulation -applyDownFrom : (ℕ → A) → ℕ → List A -applyDownFrom f zero = [] -applyDownFrom f (suc n) = f n ∷ applyDownFrom f n +applyUpTo : (ℕ → A) → ℕ → List< A +applyUpTo f zero = [<] +applyUpTo f (suc n) = applyUpTo (f ∘′ suc) n <: f zero -tabulate : ∀ {n} (f : Fin n → A) → List A -tabulate {n = zero} f = [] -tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc) +applyDownFrom : (ℕ → A) → ℕ → List< A +applyDownFrom f zero = [<] +applyDownFrom f (suc n) = applyDownFrom f n <: f n -lookup : ∀ (xs : List A) → Fin (length xs) → A -lookup (x ∷ xs) zero = x -lookup (x ∷ xs) (suc i) = lookup xs i +tabulate : ∀ {n} (f : Fin n → A) → List< A +tabulate {n = zero} f = [<] +tabulate {n = suc n} f = tabulate (f ∘′ suc) <: f zero -- Numerical -upTo : ℕ → List ℕ +upTo : ℕ → List< ℕ upTo = applyUpTo id -downFrom : ℕ → List ℕ +downFrom : ℕ → List< ℕ downFrom = applyDownFrom id -allFin : ∀ n → List (Fin n) +allFin : ∀ n → List< (Fin n) allFin n = tabulate id unfold : ∀ (P : ℕ → Set b) (f : ∀ {n} → P (suc n) → Maybe (A × P n)) → - ∀ {n} → P n → List A -unfold P f {n = zero} s = [] -unfold P f {n = suc n} s = maybe′ (λ (x , s′) → x ∷ unfold P f s′) [] (f s) + ∀ {n} → P n → List< A +unfold P f {n = zero} s = [<] +unfold P f {n = suc n} s = maybe′ (λ (x , s′) → unfold P f s′ <: x) [<] (f s) ------------------------------------------------------------------------ -- Operations for reversing lists -reverseAcc : List A → List A → List A -reverseAcc = foldl (flip _∷_) +reverseAcc : List< A → List< A → List< A +reverseAcc = foldr (flip _<:_) -reverse : List A → List A -reverse = reverseAcc [] +reverse : List< A → List< A +reverse = reverseAcc [<] +_ : toList> (reverse [<1,2,3,4]) ≡ List>.reverse (toList> [<1,2,3,4]) +_ = refl + +{- -- "Reverse append" xs ʳ++ ys = reverse xs ++ ys infixr 5 _ʳ++_ -_ʳ++_ : List A → List A → List A +_ʳ++_ : List< A → List< A → List< A _ʳ++_ = flip reverseAcc -- Snoc: Cons, but from the right. infixl 6 _∷ʳ_ -_∷ʳ_ : List A → A → List A +_∷ʳ_ : List< A → A → List< A xs ∷ʳ x = xs ++ [ x ] @@ -350,18 +368,18 @@ xs ∷ʳ x = xs ++ [ x ] infixl 5 _∷ʳ′_ -data InitLast {A : Set a} : List A → Set a where +data InitLast {A : Set a} : List< A → Set a where [] : InitLast [] - _∷ʳ′_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x) + _∷ʳ′_ : (xs : List< A) (x : A) → InitLast (xs ∷ʳ x) -initLast : (xs : List A) → InitLast xs +initLast : (xs : List< A) → InitLast xs initLast [] = [] initLast (x ∷ xs) with initLast xs ... | [] = [] ∷ʳ′ x ... | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y -- uncons, but from the right -unsnoc : List A → Maybe (List A × A) +unsnoc : List< A → Maybe (List< A × A) unsnoc as with initLast as ... | [] = nothing ... | xs ∷ʳ′ x = just (xs , x) @@ -374,39 +392,39 @@ unsnoc as with initLast as -- destruct a list argument as each branch of the pattern-matching will -- have a refined type. -uncons : List A → Maybe (A × List A) +uncons : List< A → Maybe (A × List< A) uncons [] = nothing uncons (x ∷ xs) = just (x , xs) -head : List A → Maybe A +head : List< A → Maybe A head [] = nothing head (x ∷ _) = just x -tail : List A → Maybe (List A) +tail : List< A → Maybe (List< A) tail [] = nothing tail (_ ∷ xs) = just xs -last : List A → Maybe A +last : List< A → Maybe A last [] = nothing last (x ∷ []) = just x last (_ ∷ xs) = last xs -take : ℕ → List A → List A +take : ℕ → List< A → List< A take zero xs = [] take (suc n) [] = [] take (suc n) (x ∷ xs) = x ∷ take n xs -drop : ℕ → List A → List A +drop : ℕ → List< A → List< A drop zero xs = xs drop (suc n) [] = [] drop (suc n) (x ∷ xs) = drop n xs -splitAt : ℕ → List A → List A × List A +splitAt : ℕ → List< A → List< A × List< A splitAt zero xs = ([] , xs) splitAt (suc n) [] = ([] , []) splitAt (suc n) (x ∷ xs) = Product.map₁ (x ∷_) (splitAt n xs) -removeAt : (xs : List A) → Fin (length xs) → List A +removeAt : (xs : List< A) → Fin (length xs) → List< A removeAt (x ∷ xs) zero = xs removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i @@ -431,139 +449,139 @@ removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i -- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) xs` -- rather than `takeWhileᵇ (_≤ᵇ 10) xs`. -takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +takeWhile : ∀ {P : Pred A p} → Decidable P → List< A → List< A takeWhile P? [] = [] takeWhile P? (x ∷ xs) with does (P? x) ... | true = x ∷ takeWhile P? xs ... | false = [] -takeWhileᵇ : (A → Bool) → List A → List A +takeWhileᵇ : (A → Bool) → List< A → List< A takeWhileᵇ p = takeWhile (T? ∘ p) -dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +dropWhile : ∀ {P : Pred A p} → Decidable P → List< A → List< A dropWhile P? [] = [] dropWhile P? (x ∷ xs) with does (P? x) ... | true = dropWhile P? xs ... | false = x ∷ xs -dropWhileᵇ : (A → Bool) → List A → List A +dropWhileᵇ : (A → Bool) → List< A → List< A dropWhileᵇ p = dropWhile (T? ∘ p) -filter : ∀ {P : Pred A p} → Decidable P → List A → List A +filter : ∀ {P : Pred A p} → Decidable P → List< A → List< A filter P? [] = [] filter P? (x ∷ xs) with does (P? x) ... | false = filter P? xs ... | true = x ∷ filter P? xs -filterᵇ : (A → Bool) → List A → List A +filterᵇ : (A → Bool) → List< A → List< A filterᵇ p = filter (T? ∘ p) -partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +partition : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) partition P? [] = ([] , []) partition P? (x ∷ xs) with does (P? x) | partition P? xs ... | true | (ys , zs) = (x ∷ ys , zs) ... | false | (ys , zs) = (ys , x ∷ zs) -partitionᵇ : (A → Bool) → List A → List A × List A +partitionᵇ : (A → Bool) → List< A → List< A × List< A partitionᵇ p = partition (T? ∘ p) -span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +span : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) span P? [] = ([] , []) span P? ys@(x ∷ xs) with does (P? x) ... | true = Product.map (x ∷_) id (span P? xs) ... | false = ([] , ys) -spanᵇ : (A → Bool) → List A → List A × List A +spanᵇ : (A → Bool) → List< A → List< A × List< A spanᵇ p = span (T? ∘ p) -break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +break : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) break P? = span (¬? ∘ P?) -breakᵇ : (A → Bool) → List A → List A × List A +breakᵇ : (A → Bool) → List< A → List< A × List< A breakᵇ p = break (T? ∘ p) -- The predicate `P` represents the notion of newline character for the -- type `A`. It is used to split the input list into a list of lines. -- Some lines may be empty if the input contains at least two -- consecutive newline characters. -linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +linesBy : ∀ {P : Pred A p} → Decidable P → List< A → List< (List< A) linesBy {A = A} P? = go nothing where - go : Maybe (List A) → List A → List (List A) + go : Maybe (List< A) → List< A → List< (List< A) go acc [] = maybe′ ([_] ∘′ reverse) [] acc go acc (c ∷ cs) = if does (P? c) then reverse acc′ ∷ go nothing cs else go (just (c ∷ acc′)) cs where acc′ = Maybe.fromMaybe [] acc -linesByᵇ : (A → Bool) → List A → List (List A) +linesByᵇ : (A → Bool) → List< A → List< (List< A) linesByᵇ p = linesBy (T? ∘ p) -- The predicate `P` represents the notion of space character for the -- type `A`. It is used to split the input list into a list of words. -- All the words are non empty and the output does not contain any space -- characters. -wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +wordsBy : ∀ {P : Pred A p} → Decidable P → List< A → List< (List< A) wordsBy {A = A} P? = go [] where - cons : List A → List (List A) → List (List A) + cons : List< A → List< (List< A) → List< (List< A) cons [] ass = ass cons as ass = reverse as ∷ ass - go : List A → List A → List (List A) + go : List< A → List< A → List< (List< A) go acc [] = cons acc [] go acc (c ∷ cs) = if does (P? c) then cons acc (go [] cs) else go (c ∷ acc) cs -wordsByᵇ : (A → Bool) → List A → List (List A) +wordsByᵇ : (A → Bool) → List< A → List< (List< A) wordsByᵇ p = wordsBy (T? ∘ p) -derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A +derun : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A derun R? [] = [] derun R? (x ∷ []) = x ∷ [] derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs ... | true | ys = ys ... | false | ys = x ∷ ys -derunᵇ : (A → A → Bool) → List A → List A +derunᵇ : (A → A → Bool) → List< A → List< A derunᵇ r = derun (T? ∘₂ r) -deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A +deduplicate : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A deduplicate R? [] = [] deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs) -deduplicateᵇ : (A → A → Bool) → List A → List A +deduplicateᵇ : (A → A → Bool) → List< A → List< A deduplicateᵇ r = deduplicate (T? ∘₂ r) -- Finds the first element satisfying the boolean predicate -find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A +find : ∀ {P : Pred A p} → Decidable P → List< A → Maybe A find P? [] = nothing find P? (x ∷ xs) = if does (P? x) then just x else find P? xs -findᵇ : (A → Bool) → List A → Maybe A +findᵇ : (A → Bool) → List< A → Maybe A findᵇ p = find (T? ∘ p) -- Finds the index of the first element satisfying the boolean predicate -findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs) +findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List< A) → Maybe $ Fin (length xs) findIndex P? [] = nothing findIndex P? (x ∷ xs) = if does (P? x) then just zero else Maybe.map suc (findIndex P? xs) -findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs) +findIndexᵇ : (A → Bool) → (xs : List< A) → Maybe $ Fin (length xs) findIndexᵇ p = findIndex (T? ∘ p) -- Finds indices of all the elements satisfying the boolean predicate -findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs) +findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List< A) → List< $ Fin (length xs) findIndices P? [] = [] findIndices P? (x ∷ xs) = if does (P? x) then zero ∷ indices else indices where indices = map suc (findIndices P? xs) -findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs) +findIndicesᵇ : (A → Bool) → (xs : List< A) → List< $ Fin (length xs) findIndicesᵇ p = findIndices (T? ∘ p) ------------------------------------------------------------------------ @@ -573,23 +591,23 @@ infixl 5 _[_]%=_ _[_]∷=_ -- xs [ i ]%= f modifies the i-th element of xs according to f -_[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A +_[_]%=_ : (xs : List< A) → Fin (length xs) → (A → A) → List< A xs [ i ]%= f = updateAt xs i f -- xs [ i ]≔ y overwrites the i-th element of xs with y -_[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A +_[_]∷=_ : (xs : List< A) → Fin (length xs) → A → List< A xs [ k ]∷= v = xs [ k ]%= const v ------------------------------------------------------------------------ -- Conditional versions of cons and snoc infixr 5 _?∷_ -_?∷_ : Maybe A → List A → List A +_?∷_ : Maybe A → List< A → List< A _?∷_ = maybe′ _∷_ id infixl 6 _∷ʳ?_ -_∷ʳ?_ : List A → Maybe A → List A +_∷ʳ?_ : List< A → Maybe A → List< A xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x ------------------------------------------------------------------------ @@ -598,105 +616,16 @@ xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x module _ (A : Set a) where ++-rawMagma : RawMagma a _ ++-rawMagma = record - { Carrier = List A + { Carrier = List< A ; _≈_ = _≡_ ; _∙_ = _++_ } ++-[]-rawMonoid : RawMonoid a _ ++-[]-rawMonoid = record - { Carrier = List A + { Carrier = List< A ; _≈_ = _≡_ ; _∙_ = _++_ ; ε = [] } - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -infixl 5 _∷ʳ'_ -_∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x) -_∷ʳ'_ = InitLast._∷ʳ′_ -{-# WARNING_ON_USAGE _∷ʳ'_ -"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. -Please use _∷ʳ′_ (ending in a prime) instead." -#-} - --- Version 2.0 - -infixl 5 _─_ -_─_ = removeAt -{-# WARNING_ON_USAGE _─_ -"Warning: _─_ was deprecated in v2.0. -Please use removeAt instead." -#-} - --- Version 2.1 - -scanr : (A → B → B) → B → List A → List B -scanr f e [] = e ∷ [] -scanr f e (x ∷ xs) with scanr f e xs -... | [] = [] -- dead branch -... | ys@(y ∷ _) = f x y ∷ ys -{-# WARNING_ON_USAGE scanr -"Warning: scanr was deprecated in v2.1. -Please use Data.List.Scans.Base.scanr instead." -#-} - -scanl : (A → B → A) → A → List B → List A -scanl f e [] = e ∷ [] -scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs -{-# WARNING_ON_USAGE scanl -"Warning: scanl was deprecated in v2.1. -Please use Data.List.Scans.Base.scanl instead." -#-} - --- Version 2.3 - -and : List Bool → Bool -and = foldr _∧_ true - -all : (A → Bool) → List A → Bool -all p = and ∘ map p -{-# WARNING_ON_USAGE and -"Warning: and was deprecated in v2.3. -Please use Data.Bool.ListAction.and instead." -#-} -{-# WARNING_ON_USAGE all -"Warning: all was deprecated in v2.3. -Please use Data.Nat.ListAction.all instead." -#-} - -or : List Bool → Bool -or = foldr _∨_ false - -any : (A → Bool) → List A → Bool -any p = or ∘ map p -{-# WARNING_ON_USAGE or -"Warning: or was deprecated in v2.3. -Please use Data.Bool.ListAction.or instead." -#-} -{-# WARNING_ON_USAGE any -"Warning: any was deprecated in v2.3. -Please use Data.Bool.ListAction.any instead." -#-} - -sum : List ℕ → ℕ -sum = foldr ℕ._+_ 0 -{-# WARNING_ON_USAGE sum -"Warning: sum was deprecated in v2.3. -Please use Data.Nat.ListAction.sum instead." -#-} - -product : List ℕ → ℕ -product = foldr ℕ._*_ 1 -{-# WARNING_ON_USAGE product -"Warning: product was deprecated in v2.3. -Please use Data.Nat.ListAction.product instead." -#-} -} From bc16f53508789d680274a9e9c4085b98173e15fe Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Apr 2026 15:06:23 +0100 Subject: [PATCH 3/7] [ more ] definitions --- src/Data/List/Base.agda | 2 +- src/Data/SnocList/Base.agda | 281 ++++++++++++++++++------------------ 2 files changed, 145 insertions(+), 138 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index e2bb18441b..19561277a2 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -398,7 +398,7 @@ linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) linesBy {A = A} P? = go nothing where go : Maybe (List A) → List A → List (List A) - go acc [] = maybe′ ([_] ∘′ reverse) [] acc + go acc [] = ([_] ∘′ reverse) (Maybe.fromMaybe [] acc) go acc (c ∷ cs) = if does (P? c) then reverse acc′ ∷ go nothing cs else go (just (c ∷ acc′)) cs diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda index 18b8fd8b4b..87e0387d3c 100644 --- a/src/Data/SnocList/Base.agda +++ b/src/Data/SnocList/Base.agda @@ -11,6 +11,7 @@ module Data.SnocList.Base where {- open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) -} + open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) @@ -18,17 +19,15 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product.Base as Product using (_×_; _,_) open import Data.Sum.Base as Sum using (_⊎_) open import Data.These.Base as These using (These; this; that; these) -open import Function.Base using (id; _∘′_; flip; _$′_; const) --- using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip) +open import Function.Base using (id; _∘_; _∘′_; flip; _$′_; const) + open import Level using (Level) -{- -open import Relation.Unary using (Pred; Decidable) --} +open import Relation.Unary as U using (Pred) open import Relation.Binary.Core using (Rel) import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -open import Relation.Nullary.Decidable.Core using (does) -- (T?; does; ¬?) +open import Relation.Nullary.Decidable.Core using (does; T?; ¬?) private @@ -109,7 +108,7 @@ sx <>< (x :> xs) = (sx <: x) <>< xs -- Chips (is Fish's best friend) infixr 6 _<>>_ _<>>_ : List< A → List> A → List> A -[<] <>> xs = xs +[<] <>> xs = xs (sx <: x) <>> xs = sx <>> (x :> xs) -- Some examples showing that these operations are order-preserving. @@ -150,22 +149,22 @@ map f (sx <: x) = map f sx <: f x infixl 5 _++_ _++_ : List< A → List< A → List< A -xs ++ [<] = xs -xs ++ (ys <: x) = (xs ++ ys) <: x +sx ++ [<] = sx +sx ++ (sy <: x) = (sx ++ sy) <: x intersperse : A → List< A → List< A intersperse x [<] = [<] -intersperse x xs@([<] <: _) = xs -intersperse x (ys <: y) = intersperse x ys <: x <: y +intersperse x sx@([<] <: _) = sx +intersperse x (sy <: y) = intersperse x sy <: x <: y intercalate : List< A → List< (List< A) → List< A -intercalate xs [<] = [<] -intercalate xs ([<] <: ys) = ys -intercalate xs (yss <: ys) = intercalate xs yss ++ xs ++ ys +intercalate sx [<] = [<] +intercalate sx ([<] <: sy) = sy +intercalate sx (sys <: sy) = intercalate sx sys ++ sx ++ sy cartesianProductWith : (A → B → C) → List< A → List< B → List< C cartesianProductWith f [<] _ = [<] -cartesianProductWith f (xs <: x) ys = cartesianProductWith f xs ys ++ map (f x) ys +cartesianProductWith f (sx <: x) sy = cartesianProductWith f sx sy ++ map (f x) sy cartesianProduct : List< A → List< B → List< (A × B) cartesianProduct = cartesianProductWith _,_ @@ -179,7 +178,7 @@ alignWith f as [<] = map (f ∘′ this) as alignWith f (as <: a) (bs <: b) = alignWith f as bs <: f (these a b) zipWith : (A → B → C) → List< A → List< B → List< C -zipWith f (xs <: x) (ys <: y) = zipWith f xs ys <: f x y +zipWith f (sx <: x) (sy <: y) = zipWith f sx sy <: f x y zipWith f _ _ = [<] unalignWith : (A → These B C) → List< A → List< B × List< C @@ -191,7 +190,7 @@ unalignWith f (as <: a) with f a unzipWith : (A → B × C) → List< A → List< B × List< C unzipWith f [<] = [<] , [<] -unzipWith f (xys <: xy) = Product.zip _<:_ _<:_ (unzipWith f xys) (f xy) +unzipWith f (xsy <: xy) = Product.zip _<:_ _<:_ (unzipWith f xsy) (f xy) partitionSumsWith : (A → B ⊎ C) → List< A → List< B × List< C partitionSumsWith f = unalignWith (These.fromSum ∘′ f) @@ -212,22 +211,22 @@ partitionSums : List< (A ⊎ B) → List< A × List< B partitionSums = partitionSumsWith id merge : {R : Rel A ℓ} → B.Decidable R → List< A → List< A → List< A -merge R? [<] ys = ys -merge R? xs [<] = xs -merge R? xsx@(xs <: x) ysy@(ys <: y) = if does (R? x y) - then merge R? xs ysy <: x - else merge R? xsx ys <: y +merge R? [<] sy = sy +merge R? sx [<] = sx +merge R? sxx@(sx <: x) syy@(sy <: y) = if does (R? x y) + then merge R? sx syy <: x + else merge R? sxx sy <: y ------------------------------------------------------------------------ -- Operations for reducing lists foldr : (A → B → B) → B → List< A → B foldr c n [<] = n -foldr c n (xs <: x) = foldr c (c x n) xs +foldr c n (sx <: x) = foldr c (c x n) sx foldl : (A → B → A) → A → List< B → A foldl c n [<] = n -foldl c n (xs <: x) = c (foldl c n xs) x +foldl c n (sx <: x) = c (foldl c n sx) x concat : List< (List< A) → List< A concat = foldl _++_ [<] @@ -279,30 +278,30 @@ iterate f e zero = [<] iterate f e (suc n) = iterate f (f e) n <: e inits : List< A → List< (List< A) -inits {A = A} = λ xs → tail xs <: [<] +inits {A = A} = λ sx → tail sx <: [<] module Inits where tail : List< A → List< (List< A) tail [<] = [<] - tail (xs <: x) = map (_<: x) (tail xs) <: ([<] <: x) + tail (sx <: x) = map (_<: x) (tail sx) <: ([<] <: x) tails : List< A → List< (List< A) -tails {A = A} = λ xs → tail xs <: xs +tails {A = A} = λ sx → tail sx <: sx module Tails where tail : List< A → List< (List< A) tail [<] = [<] - tail (xs <: _) = tail xs <: xs + tail (sx <: _) = tail sx <: sx -insertAt : (xs : List< A) → Fin (suc (length xs)) → A → List< A -insertAt xs zero v = xs <: v -insertAt (xs <: x) (suc i) v = insertAt xs i v <: x +insertAt : (sx : List< A) → Fin (suc (length sx)) → A → List< A +insertAt sx zero v = sx <: v +insertAt (sx <: x) (suc i) v = insertAt sx i v <: x -updateAt : (xs : List< A) → Fin (length xs) → (A → A) → List< A -updateAt (xs <: x) zero f = xs <: f x -updateAt (xs <: x) (suc i) f = updateAt xs i f <: x +updateAt : (sx : List< A) → Fin (length sx) → (A → A) → List< A +updateAt (sx <: x) zero f = sx <: f x +updateAt (sx <: x) (suc i) f = updateAt sx i f <: x -lookup : ∀ (xs : List< A) → Fin (length xs) → A -lookup (xs <: x) zero = x -lookup (xs <: x) (suc i) = lookup xs i +lookup : ∀ (sx : List< A) → Fin (length sx) → A +lookup (sx <: x) zero = x +lookup (sx <: x) (suc i) = lookup sx i -- Tabulation @@ -347,42 +346,43 @@ reverse = reverseAcc [<] _ : toList> (reverse [<1,2,3,4]) ≡ List>.reverse (toList> [<1,2,3,4]) _ = refl -{- --- "Reverse append" xs ʳ++ ys = reverse xs ++ ys - -infixr 5 _ʳ++_ +-- "Reverse append" sx ++ʳ sy = sx ++ reverse sy -_ʳ++_ : List< A → List< A → List< A -_ʳ++_ = flip reverseAcc +infixr 5 _++ʳ_ --- Snoc: Cons, but from the right. +_++ʳ_ : List< A → List< A → List< A +_++ʳ_ = reverseAcc -infixl 6 _∷ʳ_ +_ : let [<3,4] = fromList> [>3,4] in + [<1,2] ++ʳ [<3,4] ≡ [<1,2] ++ reverse [<3,4] +_ = refl -_∷ʳ_ : List< A → A → List< A -xs ∷ʳ x = xs ++ [ x ] +-- Cons: Snoc but from the left. +infixr 6 _ˡ∷_ +_ˡ∷_ : A → List< A → List< A +x ˡ∷ sx = ([<] <: x) ++ sx -- Backwards initialisation -infixl 5 _∷ʳ′_ +infixr 5 _ˡ∷′_ data InitLast {A : Set a} : List< A → Set a where - [] : InitLast [] - _∷ʳ′_ : (xs : List< A) (x : A) → InitLast (xs ∷ʳ x) + [] : InitLast [<] + _ˡ∷′_ : (x : A) (sx : List< A) → InitLast (x ˡ∷ sx) -initLast : (xs : List< A) → InitLast xs -initLast [] = [] -initLast (x ∷ xs) with initLast xs -... | [] = [] ∷ʳ′ x -... | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y +initLast : (sx : List< A) → InitLast sx +initLast [<] = [] +initLast (sx <: x) with initLast sx +... | [] = x ˡ∷′ [<] +... | y ˡ∷′ sy = y ˡ∷′ (sy <: x) --- uncons, but from the right -unsnoc : List< A → Maybe (List< A × A) -unsnoc as with initLast as +-- unsnoc, but from the left +uncons : List< A → Maybe (A × List< A) +uncons as with initLast as ... | [] = nothing -... | xs ∷ʳ′ x = just (xs , x) +... | x ˡ∷′ sx = just (x , sx) ------------------------------------------------------------------------ -- Operations for deconstructing lists @@ -392,41 +392,41 @@ unsnoc as with initLast as -- destruct a list argument as each branch of the pattern-matching will -- have a refined type. -uncons : List< A → Maybe (A × List< A) -uncons [] = nothing -uncons (x ∷ xs) = just (x , xs) +unsnoc : List< A → Maybe (List< A × A) +unsnoc [<] = nothing +unsnoc (sx <: x) = just (sx , x) head : List< A → Maybe A -head [] = nothing -head (x ∷ _) = just x +head [<] = nothing +head (_ <: x) = just x tail : List< A → Maybe (List< A) -tail [] = nothing -tail (_ ∷ xs) = just xs +tail [<] = nothing +tail (sx <: _) = just sx last : List< A → Maybe A -last [] = nothing -last (x ∷ []) = just x -last (_ ∷ xs) = last xs +last [<] = nothing +last ([<] <: x) = just x +last (sx <: _) = last sx take : ℕ → List< A → List< A -take zero xs = [] -take (suc n) [] = [] -take (suc n) (x ∷ xs) = x ∷ take n xs +take zero sx = [<] +take (suc n) [<] = [<] +take (suc n) (sx <: x) = take n sx <: x drop : ℕ → List< A → List< A -drop zero xs = xs -drop (suc n) [] = [] -drop (suc n) (x ∷ xs) = drop n xs +drop zero sx = sx +drop (suc n) [<] = [<] +drop (suc n) (sx <: x) = drop n sx splitAt : ℕ → List< A → List< A × List< A -splitAt zero xs = ([] , xs) -splitAt (suc n) [] = ([] , []) -splitAt (suc n) (x ∷ xs) = Product.map₁ (x ∷_) (splitAt n xs) +splitAt zero sx = (sx , [<]) +splitAt (suc n) [<] = ([<] , [<]) +splitAt (suc n) (sx <: x) = Product.map₂ (_<: x) (splitAt n sx) -removeAt : (xs : List< A) → Fin (length xs) → List< A -removeAt (x ∷ xs) zero = xs -removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i +removeAt : (sx : List< A) → Fin (length sx) → List< A +removeAt (sx <: _) zero = sx +removeAt (sx <: x) (suc i) = removeAt sx i <: x ------------------------------------------------------------------------ -- Operations for filtering lists @@ -446,56 +446,53 @@ removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i -- wants to minimise dependencies. -- -- In summary, in most cases you probably want to use the decidable --- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) xs` --- rather than `takeWhileᵇ (_≤ᵇ 10) xs`. +-- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) sx` +-- rather than `takeWhileᵇ (_≤ᵇ 10) sx`. -takeWhile : ∀ {P : Pred A p} → Decidable P → List< A → List< A -takeWhile P? [] = [] -takeWhile P? (x ∷ xs) with does (P? x) -... | true = x ∷ takeWhile P? xs -... | false = [] +takeWhile : ∀ {P : Pred A p} → U.Decidable P → List< A → List< A +takeWhile P? [<] = [<] +takeWhile P? (sx <: x) = + if does (P? x) then takeWhile P? sx <: x else [<] takeWhileᵇ : (A → Bool) → List< A → List< A takeWhileᵇ p = takeWhile (T? ∘ p) -dropWhile : ∀ {P : Pred A p} → Decidable P → List< A → List< A -dropWhile P? [] = [] -dropWhile P? (x ∷ xs) with does (P? x) -... | true = dropWhile P? xs -... | false = x ∷ xs +dropWhile : ∀ {P : Pred A p} → U.Decidable P → List< A → List< A +dropWhile P? [<] = [<] +dropWhile P? sxx@(sx <: x) = + if does (P? x) then dropWhile P? sx else sxx dropWhileᵇ : (A → Bool) → List< A → List< A dropWhileᵇ p = dropWhile (T? ∘ p) -filter : ∀ {P : Pred A p} → Decidable P → List< A → List< A -filter P? [] = [] -filter P? (x ∷ xs) with does (P? x) -... | false = filter P? xs -... | true = x ∷ filter P? xs +filter : ∀ {P : Pred A p} → U.Decidable P → List< A → List< A +filter P? [<] = [<] +filter P? (sx <: x) = + let ih = filter P? sx in + if does (P? x) then ih <: x else ih filterᵇ : (A → Bool) → List< A → List< A filterᵇ p = filter (T? ∘ p) -partition : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) -partition P? [] = ([] , []) -partition P? (x ∷ xs) with does (P? x) | partition P? xs -... | true | (ys , zs) = (x ∷ ys , zs) -... | false | (ys , zs) = (ys , x ∷ zs) +partition : ∀ {P : Pred A p} → U.Decidable P → List< A → (List< A × List< A) +partition P? [<] = ([<] , [<]) +partition P? (sx <: x) with does (P? x) | partition P? sx +... | true | (sy , sz) = (sy <: x , sz) +... | false | (sy , sz) = (sy , sz <: x) partitionᵇ : (A → Bool) → List< A → List< A × List< A partitionᵇ p = partition (T? ∘ p) -span : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) -span P? [] = ([] , []) -span P? ys@(x ∷ xs) with does (P? x) -... | true = Product.map (x ∷_) id (span P? xs) -... | false = ([] , ys) - +span : ∀ {P : Pred A p} → U.Decidable P → List< A → (List< A × List< A) +span P? [<] = ([<] , [<]) +span P? sxx@(sx <: x) with does (P? x) +... | true = Product.map₂ (_<: x) (span P? sx) +... | false = (sxx , [<]) spanᵇ : (A → Bool) → List< A → List< A × List< A spanᵇ p = span (T? ∘ p) -break : ∀ {P : Pred A p} → Decidable P → List< A → (List< A × List< A) +break : ∀ {P : Pred A p} → U.Decidable P → List< A → (List< A × List< A) break P? = span (¬? ∘ P?) breakᵇ : (A → Bool) → List< A → List< A × List< A @@ -505,19 +502,29 @@ breakᵇ p = break (T? ∘ p) -- type `A`. It is used to split the input list into a list of lines. -- Some lines may be empty if the input contains at least two -- consecutive newline characters. -linesBy : ∀ {P : Pred A p} → Decidable P → List< A → List< (List< A) +linesBy : ∀ {P : Pred A p} → U.Decidable P → List< A → List< (List< A) linesBy {A = A} P? = go nothing where - go : Maybe (List< A) → List< A → List< (List< A) - go acc [] = maybe′ ([_] ∘′ reverse) [] acc - go acc (c ∷ cs) = if does (P? c) - then reverse acc′ ∷ go nothing cs - else go (just (c ∷ acc′)) cs - where acc′ = Maybe.fromMaybe [] acc + go : Maybe (List> A) → List< A → List< (List< A) + go acc [<] = (([<] <:_) ∘′ fromList>) (Maybe.fromMaybe [>] acc) + go acc (cs <: c) = if does (P? c) + then go nothing cs <: fromList> acc′ + else go (just (c :> acc′)) cs + where acc′ = Maybe.fromMaybe [>] acc linesByᵇ : (A → Bool) → List< A → List< (List< A) linesByᵇ p = linesBy (T? ∘ p) +_ : linesByᵇ (ℕ._≤ᵇ 0) ([<] <: 0 <: 1 <: 2 <: 0 <: 3 <: 0 <: 0 <: 4) ≡ + [<] <: [<] <: ([<] <: 1 <: 2) <: ([<] <: 3) <: [<] <: ([<] <: 4) +_ = refl + +_ : linesByᵇ (ℕ._≤ᵇ 0) ([<] <: 1 <: 2 <: 0 <: 3 <: 0 <: 0 <: 4) ≡ + [<] <: ([<] <: 1 <: 2) <: ([<] <: 3) <: [<] <: ([<] <: 4) +_ = refl + + +{- -- The predicate `P` represents the notion of space character for the -- type `A`. It is used to split the input list into a list of words. -- All the words are non empty and the output does not contain any space @@ -541,16 +548,16 @@ wordsByᵇ p = wordsBy (T? ∘ p) derun : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A derun R? [] = [] derun R? (x ∷ []) = x ∷ [] -derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs -... | true | ys = ys -... | false | ys = x ∷ ys +derun R? (x ∷ sx@(y ∷ _)) with does (R? x y) | derun R? sx +... | true | sy = sy +... | false | sy = x ∷ sy derunᵇ : (A → A → Bool) → List< A → List< A derunᵇ r = derun (T? ∘₂ r) deduplicate : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A deduplicate R? [] = [] -deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs) +deduplicate R? (x ∷ sx) = x ∷ filter (¬? ∘ R? x) (deduplicate R? sx) deduplicateᵇ : (A → A → Bool) → List< A → List< A deduplicateᵇ r = deduplicate (T? ∘₂ r) @@ -558,30 +565,30 @@ deduplicateᵇ r = deduplicate (T? ∘₂ r) -- Finds the first element satisfying the boolean predicate find : ∀ {P : Pred A p} → Decidable P → List< A → Maybe A find P? [] = nothing -find P? (x ∷ xs) = if does (P? x) then just x else find P? xs +find P? (x ∷ sx) = if does (P? x) then just x else find P? sx findᵇ : (A → Bool) → List< A → Maybe A findᵇ p = find (T? ∘ p) -- Finds the index of the first element satisfying the boolean predicate -findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List< A) → Maybe $ Fin (length xs) +findIndex : ∀ {P : Pred A p} → Decidable P → (sx : List< A) → Maybe $ Fin (length sx) findIndex P? [] = nothing -findIndex P? (x ∷ xs) = if does (P? x) +findIndex P? (x ∷ sx) = if does (P? x) then just zero - else Maybe.map suc (findIndex P? xs) + else Maybe.map suc (findIndex P? sx) -findIndexᵇ : (A → Bool) → (xs : List< A) → Maybe $ Fin (length xs) +findIndexᵇ : (A → Bool) → (sx : List< A) → Maybe $ Fin (length sx) findIndexᵇ p = findIndex (T? ∘ p) -- Finds indices of all the elements satisfying the boolean predicate -findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List< A) → List< $ Fin (length xs) +findIndices : ∀ {P : Pred A p} → Decidable P → (sx : List< A) → List< $ Fin (length sx) findIndices P? [] = [] -findIndices P? (x ∷ xs) = if does (P? x) +findIndices P? (x ∷ sx) = if does (P? x) then zero ∷ indices else indices - where indices = map suc (findIndices P? xs) + where indices = map suc (findIndices P? sx) -findIndicesᵇ : (A → Bool) → (xs : List< A) → List< $ Fin (length xs) +findIndicesᵇ : (A → Bool) → (sx : List< A) → List< $ Fin (length sx) findIndicesᵇ p = findIndices (T? ∘ p) ------------------------------------------------------------------------ @@ -589,15 +596,15 @@ findIndicesᵇ p = findIndices (T? ∘ p) infixl 5 _[_]%=_ _[_]∷=_ --- xs [ i ]%= f modifies the i-th element of xs according to f +-- sx [ i ]%= f modifies the i-th element of sx according to f -_[_]%=_ : (xs : List< A) → Fin (length xs) → (A → A) → List< A -xs [ i ]%= f = updateAt xs i f +_[_]%=_ : (sx : List< A) → Fin (length sx) → (A → A) → List< A +sx [ i ]%= f = updateAt sx i f --- xs [ i ]≔ y overwrites the i-th element of xs with y +-- sx [ i ]≔ y overwrites the i-th element of sx with y -_[_]∷=_ : (xs : List< A) → Fin (length xs) → A → List< A -xs [ k ]∷= v = xs [ k ]%= const v +_[_]∷=_ : (sx : List< A) → Fin (length sx) → A → List< A +sx [ k ]∷= v = sx [ k ]%= const v ------------------------------------------------------------------------ -- Conditional versions of cons and snoc @@ -608,7 +615,7 @@ _?∷_ = maybe′ _∷_ id infixl 6 _∷ʳ?_ _∷ʳ?_ : List< A → Maybe A → List< A -xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x +sx ∷ʳ? x = maybe′ (sx ∷ʳ_) sx x ------------------------------------------------------------------------ -- Raw algebraic bundles From c1c4bafda252252cf2d0df636f22423e037a86dd Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Apr 2026 16:44:10 +0100 Subject: [PATCH 4/7] [ more ] bug fixes --- CHANGELOG.md | 9 ++++++++ src/Data/List/Base.agda | 14 ++++++------ src/Data/SnocList/Base.agda | 43 +++++++++++++++++++------------------ 3 files changed, 39 insertions(+), 27 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 42844d01ef..18ee5e53cc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,8 @@ Bug-fixes * Fix a typo in `Function.Construct.Constant`. +* Fix a bug in `Data.List.Base`'s `linesBy` (the last empty line would be dropped). + Non-backwards compatible changes -------------------------------- @@ -184,6 +186,13 @@ New modules Data.List.NonEmpty.Membership.Setoid ``` +* A new type of lists that grow on the right. + This is typically useful to model contexts of typing rules + or type accumulators that need to be reversed in the base case. + ``` + Data.SnocList.Base + ``` + * Refactoring of `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` as smaller modules: ``` Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 19561277a2..a76c87dd15 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -395,14 +395,16 @@ breakᵇ p = break (T? ∘ p) -- Some lines may be empty if the input contains at least two -- consecutive newline characters. linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) -linesBy {A = A} P? = go nothing where +linesBy {A = A} P? = go [] where - go : Maybe (List A) → List A → List (List A) - go acc [] = ([_] ∘′ reverse) (Maybe.fromMaybe [] acc) + -- ideally this should use a snoclist for the accumulator + -- but unfortunately this is in the dependency graph of + -- Data.SnocList.Base + go : List A → List A → List (List A) + go acc [] = [ reverse acc ] go acc (c ∷ cs) = if does (P? c) - then reverse acc′ ∷ go nothing cs - else go (just (c ∷ acc′)) cs - where acc′ = Maybe.fromMaybe [] acc + then reverse acc ∷ go [] cs + else go (c ∷ acc) cs linesByᵇ : (A → Bool) → List A → List (List A) linesByᵇ p = linesBy (T? ∘ p) diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda index 87e0387d3c..93bc3a0e78 100644 --- a/src/Data/SnocList/Base.agda +++ b/src/Data/SnocList/Base.agda @@ -58,8 +58,9 @@ open import Data.List.Base as List> -- because `snoc' is `cons' backwards is a list that grows on the -- right, and that is therefore traversed right-to-left. --- :> a right-to-left cons --- <: its mirror image to get a left-to-right cons (aka snoc) +-- :> a cons growing the list on the left +-- <: its mirror image to get a cons that grows the list on the right +-- (aka snoc) infixl 5 _<:_ @@ -503,14 +504,13 @@ breakᵇ p = break (T? ∘ p) -- Some lines may be empty if the input contains at least two -- consecutive newline characters. linesBy : ∀ {P : Pred A p} → U.Decidable P → List< A → List< (List< A) -linesBy {A = A} P? = go nothing where +linesBy {A = A} P? cs = go cs [>] where - go : Maybe (List> A) → List< A → List< (List< A) - go acc [<] = (([<] <:_) ∘′ fromList>) (Maybe.fromMaybe [>] acc) - go acc (cs <: c) = if does (P? c) - then go nothing cs <: fromList> acc′ - else go (just (c :> acc′)) cs - where acc′ = Maybe.fromMaybe [>] acc + go : List< A → List> A → List< (List< A) + go [<] l = [<] <: fromList> l + go (cs <: c) l = if does (P? c) + then go cs [>] <: fromList> l + else go cs (c :> l) linesByᵇ : (A → Bool) → List< A → List< (List< A) linesByᵇ p = linesBy (T? ∘ p) @@ -523,25 +523,26 @@ _ : linesByᵇ (ℕ._≤ᵇ 0) ([<] <: 1 <: 2 <: 0 <: 3 <: 0 <: 0 <: 4) ≡ [<] <: ([<] <: 1 <: 2) <: ([<] <: 3) <: [<] <: ([<] <: 4) _ = refl - -{- -- The predicate `P` represents the notion of space character for the -- type `A`. It is used to split the input list into a list of words. -- All the words are non empty and the output does not contain any space -- characters. -wordsBy : ∀ {P : Pred A p} → Decidable P → List< A → List< (List< A) -wordsBy {A = A} P? = go [] where +wordsBy : ∀ {P : Pred A p} → U.Decidable P → List< A → List< (List< A) +wordsBy {A = A} P? cs = go cs [>] where - cons : List< A → List< (List< A) → List< (List< A) - cons [] ass = ass - cons as ass = reverse as ∷ ass + snoc : List< (List< A) → List> A → List< (List< A) + snoc sas [>] = sas + snoc sas as = sas <: fromList> as - go : List< A → List< A → List< (List< A) - go acc [] = cons acc [] - go acc (c ∷ cs) = if does (P? c) - then cons acc (go [] cs) - else go (c ∷ acc) cs + go : List< A → List> A → List< (List< A) + go [<] w = snoc [<] w + go (cs <: c) w = if does (P? c) + then snoc (go cs [>]) w + else go cs (c :> w) + -- notice that the order cs - c - w in go's LHS + -- stays the same in the recursive call +{- wordsByᵇ : (A → Bool) → List< A → List< (List< A) wordsByᵇ p = wordsBy (T? ∘ p) From 9b9a9a501a3383c4bb374057680d39684d314a6e Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Apr 2026 16:49:53 +0100 Subject: [PATCH 5/7] [ done ] feature parity with Data.List.Base --- src/Data/SnocList/Base.agda | 57 +++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 31 deletions(-) diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda index 93bc3a0e78..71d1dd61c2 100644 --- a/src/Data/SnocList/Base.agda +++ b/src/Data/SnocList/Base.agda @@ -8,9 +8,7 @@ module Data.SnocList.Base where -{- open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) --} open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) @@ -20,7 +18,7 @@ open import Data.Product.Base as Product using (_×_; _,_) open import Data.Sum.Base as Sum using (_⊎_) open import Data.These.Base as These using (These; this; that; these) -open import Function.Base using (id; _∘_; _∘′_; flip; _$′_; const) +open import Function.Base using (id; _∘_; _∘′_; _∘₂_; flip; _$′_; const) open import Level using (Level) open import Relation.Unary as U using (Pred) @@ -29,7 +27,6 @@ import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import Relation.Nullary.Decidable.Core using (does; T?; ¬?) - private variable a b c p ℓ : Level @@ -542,54 +539,53 @@ wordsBy {A = A} P? cs = go cs [>] where -- notice that the order cs - c - w in go's LHS -- stays the same in the recursive call -{- wordsByᵇ : (A → Bool) → List< A → List< (List< A) wordsByᵇ p = wordsBy (T? ∘ p) derun : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A -derun R? [] = [] -derun R? (x ∷ []) = x ∷ [] -derun R? (x ∷ sx@(y ∷ _)) with does (R? x y) | derun R? sx +derun R? [<] = [<] +derun R? sx@([<] <: x) = sx +derun R? (sx@(_ <: y) <: x) with does (R? x y) | derun R? sx ... | true | sy = sy -... | false | sy = x ∷ sy +... | false | sy = sy <: x derunᵇ : (A → A → Bool) → List< A → List< A derunᵇ r = derun (T? ∘₂ r) deduplicate : ∀ {R : Rel A p} → B.Decidable R → List< A → List< A -deduplicate R? [] = [] -deduplicate R? (x ∷ sx) = x ∷ filter (¬? ∘ R? x) (deduplicate R? sx) +deduplicate R? [<] = [<] +deduplicate R? (sx <: x) = filter (¬? ∘ R? x) (deduplicate R? sx) <: x deduplicateᵇ : (A → A → Bool) → List< A → List< A deduplicateᵇ r = deduplicate (T? ∘₂ r) -- Finds the first element satisfying the boolean predicate -find : ∀ {P : Pred A p} → Decidable P → List< A → Maybe A -find P? [] = nothing -find P? (x ∷ sx) = if does (P? x) then just x else find P? sx +find : ∀ {P : Pred A p} → U.Decidable P → List< A → Maybe A +find P? [<] = nothing +find P? (sx <: x) = if does (P? x) then just x else find P? sx findᵇ : (A → Bool) → List< A → Maybe A findᵇ p = find (T? ∘ p) -- Finds the index of the first element satisfying the boolean predicate -findIndex : ∀ {P : Pred A p} → Decidable P → (sx : List< A) → Maybe $ Fin (length sx) -findIndex P? [] = nothing -findIndex P? (x ∷ sx) = if does (P? x) +findIndex : ∀ {P : Pred A p} → U.Decidable P → (sx : List< A) → Maybe (Fin (length sx)) +findIndex P? [<] = nothing +findIndex P? (sx <: x) = if does (P? x) then just zero else Maybe.map suc (findIndex P? sx) -findIndexᵇ : (A → Bool) → (sx : List< A) → Maybe $ Fin (length sx) +findIndexᵇ : (A → Bool) → (sx : List< A) → Maybe (Fin (length sx)) findIndexᵇ p = findIndex (T? ∘ p) -- Finds indices of all the elements satisfying the boolean predicate -findIndices : ∀ {P : Pred A p} → Decidable P → (sx : List< A) → List< $ Fin (length sx) -findIndices P? [] = [] -findIndices P? (x ∷ sx) = if does (P? x) - then zero ∷ indices +findIndices : ∀ {P : Pred A p} → U.Decidable P → (sx : List< A) → List< (Fin (length sx)) +findIndices P? [<] = [<] +findIndices P? (sx <: x) = if does (P? x) + then indices <: zero else indices where indices = map suc (findIndices P? sx) -findIndicesᵇ : (A → Bool) → (sx : List< A) → List< $ Fin (length sx) +findIndicesᵇ : (A → Bool) → (sx : List< A) → List< (Fin (length sx)) findIndicesᵇ p = findIndices (T? ∘ p) ------------------------------------------------------------------------ @@ -610,13 +606,13 @@ sx [ k ]∷= v = sx [ k ]%= const v ------------------------------------------------------------------------ -- Conditional versions of cons and snoc -infixr 5 _?∷_ -_?∷_ : Maybe A → List< A → List< A -_?∷_ = maybe′ _∷_ id +infixr 5 _<:?_ +_<:?_ : List< A → Maybe A → List< A +sx <:? mx = maybe′ (sx <:_) sx mx -infixl 6 _∷ʳ?_ -_∷ʳ?_ : List< A → Maybe A → List< A -sx ∷ʳ? x = maybe′ (sx ∷ʳ_) sx x +infixl 6 _?ˡ∷_ +_?ˡ∷_ : Maybe A → List< A → List< A +mx ?ˡ∷ sx = maybe′ (_ˡ∷ sx) sx mx ------------------------------------------------------------------------ -- Raw algebraic bundles @@ -634,6 +630,5 @@ module _ (A : Set a) where { Carrier = List< A ; _≈_ = _≡_ ; _∙_ = _++_ - ; ε = [] + ; ε = [<] } --} From 50a1543eae2bbb9ecaf20d2854f18d2135495a0c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Apr 2026 17:03:49 +0100 Subject: [PATCH 6/7] [ fix ] test case --- src/Data/String/Base.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda index 43ff59c732..d5a48fdb61 100644 --- a/src/Data/String/Base.agda +++ b/src/Data/String/Base.agda @@ -186,7 +186,11 @@ lines : String → List String lines = linesByᵇ ('\n' Char.≈ᵇ_) -- `lines` preserves empty lines -_ : lines "\nabc\n\nb\n\n\n" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ "" ∷ "" ∷ [] +_ : lines "\nabc\n\nb\n\n\n" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ "" ∷ "" ∷ "" ∷ [] +_ = refl + +-- `lines` does not add a trailing newline +_ : lines "\nabc\n\nb" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ [] _ = refl map : (Char → Char) → String → String From 8bf6192b7bba419ee02c492d238302ce41eca169 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Mon, 20 Apr 2026 11:26:02 +0100 Subject: [PATCH 7/7] [ cleanup ] remove spurious lambdas Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/SnocList/Base.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/SnocList/Base.agda b/src/Data/SnocList/Base.agda index 71d1dd61c2..214b1bdafb 100644 --- a/src/Data/SnocList/Base.agda +++ b/src/Data/SnocList/Base.agda @@ -276,14 +276,14 @@ iterate f e zero = [<] iterate f e (suc n) = iterate f (f e) n <: e inits : List< A → List< (List< A) -inits {A = A} = λ sx → tail sx <: [<] +inits {A = A} sx = tail sx <: [<] module Inits where tail : List< A → List< (List< A) tail [<] = [<] tail (sx <: x) = map (_<: x) (tail sx) <: ([<] <: x) tails : List< A → List< (List< A) -tails {A = A} = λ sx → tail sx <: sx +tails {A = A} sx = tail sx <: sx module Tails where tail : List< A → List< (List< A) tail [<] = [<]