From 8b805be9d3730c67dd75422357d8f9cf35426e78 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 4 Apr 2023 21:08:41 -0700
Subject: [PATCH] Add a map from natural numbers for use as a lattice
 transformer

---
 NatMap.agda | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 NatMap.agda

diff --git a/NatMap.agda b/NatMap.agda
new file mode 100644
index 0000000..9349210
--- /dev/null
+++ b/NatMap.agda
@@ -0,0 +1,48 @@
+module NatMap where
+
+open import Agda.Primitive using (Level)
+open import Data.Nat using (ℕ; _<?_; _≟_)
+open import Data.Nat.Properties using (<-cmp)
+open import Data.String using (String; _++_)
+open import Data.List using (List; []; _∷_)
+open import Data.Product using (_×_; _,_)
+open import Relation.Nullary using (yes; no)
+open import Relation.Binary using (Tri)
+open import Agda.Builtin.Equality using (_≡_; refl)
+
+variable
+    a : Level
+    A : Set a
+
+-- It's easiest to reason about a linear-insertion map.
+
+NatMap : (A : Set a) → Set a
+NatMap A = List (ℕ × A)
+
+insert : ℕ → A → NatMap A -> NatMap A
+insert n a [] = (n , a) ∷ []
+insert n a l@(x@(n' , a') ∷ xs) with n <? n'
+...                             | yes n≡n' = (n , a) ∷ l
+...                             | no n≢n' = x ∷ insert n a xs
+
+
+testInsert₁ : insert 3 "third" [] ≡ (3 , "third") ∷ []
+testInsert₁ = refl
+
+testInsert₂ : insert 4 "fourth" ((3 , "third") ∷ []) ≡ (3 , "third") ∷ (4 , "fourth") ∷ []
+testInsert₂ = refl
+
+testInsert₃ : insert 2 "second" ((3 , "third") ∷ (4 , "fourth") ∷ []) ≡ (2 , "second") ∷ (3 , "third") ∷ (4 , "fourth") ∷ []
+testInsert₃ = refl
+
+{-# TERMINATING #-}
+merge : (A -> A -> A) -> NatMap A -> NatMap A -> NatMap A
+merge _ [] m₂ = m₂
+merge _ m₁ [] = m₁
+merge f m₁@(x₁@(n₁ , a₁) ∷ xs₁) m₂@(x₂@(n₂ , a₂) ∷ xs₂) with <-cmp n₁ n₂
+...                                                     | Tri.tri< _ _ _ = x₁ ∷ merge f xs₁ m₂
+...                                                     | Tri.tri> _ _ _ = x₂ ∷ merge f m₁ xs₂
+...                                                     | Tri.tri≈ _ _ _ = (n₁ , f a₁ a₂) ∷ merge f xs₁ xs₂
+
+testMerge : merge (_++_) ((1 , "one") ∷ (2 , "two") ∷ []) ((2 , "two") ∷ (3 , "three") ∷ []) ≡ (1 , "one") ∷ (2 , "twotwo") ∷ (3 , "three") ∷ []
+testMerge = refl