[ new ] add rose trees (#1035)

Author: gallais

CHANGELOG.md

@@ -133,7 +133,7 @@ warnings are attached to all deprecated names to discourage their use.
 Other major additions
 ---------------------
 
-* New modules
+* Added new modules:
   ```agda
   Codata.Cowriter.Bisimilarity
 
@@ -145,16 +145,19 @@ Other major additions
   Data.Tree.Binary.Properties
   Data.Tree.Binary.Relation.Unary.All
   Data.Tree.Binary.Relation.Unary.All.Properties
+  Data.Tree.Rose
+  Data.Tree.Rose.Properties
 
   Text.Pretty.Core
   Text.Pretty
-
   Text.Tabular.Base
   Text.Tabular.List
   Text.Tabular.Vec
+  Text.Tree.Linear
 
   README.Text.Pretty
   README.Text.Tabular
+  README.Text.Tree
   ```
 
 * Added induction over subsets to `Data.Fin.Subset.Induction`.

README.agda

@@ -294,13 +294,18 @@ import README.Inspect
 
 import README.Text.Printf
 
+-- Showcasing the pretty printing module
+
+import README.Text.Pretty
+
 -- Explaining how to display tables of strings:
 
 import README.Text.Tabular
 
--- Showcasing the pretty printing module
+-- Explaining how to display a tree:
+
+import README.Text.Tree
 
-import README.Text.Pretty
 
 ------------------------------------------------------------------------
 -- Core modules

README/Text/Tree.agda

@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Examples of pretty printing of rose trees
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe --sized-types #-}
+
+module README.Text.Tree where
+
+open import Data.List.Base
+open import Data.String.Base
+open import Data.Tree.Rose
+open import Function.Base
+open import Agda.Builtin.Equality
+
+------------------------------------------------------------------------
+-- We import the module defining the pretty printer for rose trees
+
+open import Text.Tree.Linear
+
+------------------------------------------------------------------------
+-- Example
+
+_ : unlines (display
+  $ node [ "one" ]
+      (node [ "two" ] []
+     ∷ node ("three" ∷ "and" ∷ "four" ∷ [])
+         (node [ "five" ] []
+        ∷ node [ "six" ] (node [ "seven" ] [] ∷ [])
+        ∷ node [ "eight" ] []
+        ∷ [])
+     ∷ node [ "nine" ]
+         (node [ "ten" ] []
+        ∷ node [ "eleven" ] [] ∷ [])
+        ∷ []))
+  ≡ "one
+\   \ ├ two
+\   \ ├ three
+\   \ │ and
+\   \ │ four
+\   \ │  ├ five
+\   \ │  ├ six
+\   \ │  │  └ seven
+\   \ │  └ eight
+\   \ └ nine
+\   \    ├ ten
+\   \    └ eleven"
+_ = refl

src/Data/List/Base.agda

@@ -13,13 +13,13 @@ module Data.List.Base where
 
 open import Data.Bool.Base as Bool
   using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
-open import Data.Fin using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe)
+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; _+_; _*_ ; _≤_ ; s≤s)
 open import Data.Product as Prod using (_×_; _,_)
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+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 using (id; _∘_ ; _∘′_; const; flip)
+open import Function.Base using (id; _∘_ ; _∘′_; const; flip)
 open import Level using (Level)
 open import Relation.Nullary using (does)
 open import Relation.Unary using (Pred; Decidable)
@@ -335,11 +335,11 @@ xs ∷ʳ x = xs ++ [ x ]
 
 infixr 5 _?∷_
 _?∷_ : Maybe A → List A → List A
-_?∷_ = maybe _∷_ id
+_?∷_ = maybe′ _∷_ id
 
 infixl 6 _∷ʳ?_
 _∷ʳ?_ : List A → Maybe A → List A
-xs ∷ʳ? x = maybe (xs ∷ʳ_) xs x
+xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x
 
 
 -- Backwards initialisation

src/Data/Tree/Rose.agda

@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Rose trees
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe --sized-types #-}
+
+module Data.Tree.Rose where
+
+open import Level using (Level)
+open import Size
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.List.Extrema.Nat
+open import Function.Base using (_∘_)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+    i : Size
+
+------------------------------------------------------------------------
+-- Type and basic constructions
+
+data Rose (A : Set a) : Size → Set a where
+  node : (a : A) (ts : List (Rose A i)) → Rose A (↑ i)
+
+leaf : A → Rose A ∞
+leaf a = node a []
+
+------------------------------------------------------------------------
+-- Transforming rose trees
+
+map : (A → B) → Rose A i → Rose B i
+map f (node a ts) = node (f a) (List.map (map f) ts)
+
+------------------------------------------------------------------------
+-- Reducing rose trees
+
+foldr : (A → List B → B) → Rose A i → B
+foldr n (node a ts) = n a (List.map (foldr n) ts)
+
+depth : Rose A i → ℕ
+depth (node a ts) = suc (max 0 (List.map depth ts))

src/Data/Tree/Rose/Properties.agda

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of rose trees
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe --sized-types #-}
+
+module Data.Tree.Rose.Properties where
+
+open import Level using (Level)
+open import Size
+open import Data.List.Base as List using (List)
+open import Data.List.Extrema.Nat
+import Data.List.Properties as Listₚ
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Tree.Rose
+open import Function.Base
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    i : Size
+
+------------------------------------------------------------------------
+-- map properties
+
+map-compose : (f : A → B) (g : B → C) →
+              map {i = i} (g ∘′ f) ≗ map {i = i} g ∘′ map {i = i} f
+map-compose f g (node a ts) = cong (node (g (f a))) $ begin
+  List.map (map (g ∘′ f)) ts             ≡⟨ Listₚ.map-cong (map-compose f g) ts ⟩
+  List.map (map g ∘ map f) ts            ≡⟨ Listₚ.map-compose ts ⟩
+  List.map (map g) (List.map (map f) ts) ∎
+
+depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t
+depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin
+  List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩
+  List.map (depth ∘′ map f) ts         ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩
+  List.map depth ts ∎
+
+------------------------------------------------------------------------
+-- foldr properties
+
+foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) →
+            foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts
+foldr-map f n (node a ts) = cong (n (f a)) $ begin
+  List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩
+  List.map (foldr n ∘′ map f) ts           ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩
+  List.map (foldr (n ∘′ f)) ts             ∎

src/Text/Tree/Linear.agda

@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- 1 dimensional pretty printing of rose trees
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe --sized-types #-}
+
+module Text.Tree.Linear where
+
+open import Level using (Level)
+open import Size
+open import Data.Bool.Base using (Bool; true; false; if_then_else_; _∧_)
+open import Data.DifferenceList as DList renaming (DiffList to DList) using ()
+open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_)
+open import Data.Nat.Base using (ℕ; _∸_)
+open import Data.Product using (_×_; _,_)
+open import Data.String.Base
+open import Data.Tree.Rose using (Rose; node)
+open import Function.Base using (flip)
+
+private
+  variable
+    a : Level
+    A : Set a
+    i : Size
+
+display : Rose (List String) i → List String
+display t = DList.toList (go (([] , t) ∷ [])) where
+
+  padding : Bool → List Bool → String → String
+  padding dir? []       str = str
+  padding dir? (b ∷ bs) str =
+    (if dir? ∧ List.null bs
+     then if b then " ├ " else " └ "
+     else if b then " │ "  else "   ")
+    ++ padding dir? bs str
+
+  nodePrefixes : List A → List Bool
+  nodePrefixes as = true ∷ List.replicate (List.length as ∸ 1) false
+
+  childrenPrefixes : List A → List Bool
+  childrenPrefixes as = List.replicate (List.length as ∸ 1) true ∷ʳ false
+
+  go : List (List Bool × Rose (List String) i) → DList String
+  go []                       = DList.[]
+  go ((bs , node a ts₁) ∷ ts) =
+    let bs′ = List.reverse bs in
+    DList.fromList (List.zipWith (flip padding bs′) (nodePrefixes a) a)
+    DList.++ go (List.zip (List.map (_∷ bs) (childrenPrefixes ts₁)) ts₁)
+    DList.++ go ts