Operations over Binary random access lists #4
Conversation
| @@ -3,9 +3,12 @@ | |||
| open import Data.Nat | |||
| open import Data.Unit | |||
| open import Data.Empty | |||
| open import Data.Product | |||
| open import Data.Product | |||
| _O : ∀ {n} (bs : DBin-g A (suc n)) → DBin-g A n | ||
| _[_]I : ∀ {n} (bs : DBin-g A (suc n)) (t : T A n) → DBin-g A n |
There was a problem hiding this comment.
Stylistic change, postpone to another PR performing a global and uniform update.
| data Bin : Set where | ||
| ϵ : Bin | ||
| _O : Bin → Bin | ||
| _I : Bin → Bin |
| Bin⇒ℕ-g (bs O) k = {- 0 * 2 ^ k + -} Bin⇒ℕ-g bs (suc k) | ||
| Bin⇒ℕ-g (bs I) k = {- 1 * -} 2 ^ k + Bin⇒ℕ-g bs (suc k) |
|
|
||
| Bin⇒Nat : Bin → ℕ | ||
| Bin⇒Nat b = Bin⇒Nat-g b 0 | ||
| Bin⇒ℕ-g : Bin → ℕ → ℕ |
|
|
||
| private | ||
| -- Appends a new Tree in a structure of trees | ||
| consTree : ∀ {A n} → Tree A n → RAL-g A n → RAL-g A n |
There was a problem hiding this comment.
Add a lemma relating the size of the underlying containers: something like
forget (consTree l t) = BintoNat (size l) +Bin forget t
(Catherine will explicit need this)
| consTree l (t [ l₁ ]I) = consTree (Node l l₁) t O | ||
|
|
||
| -- Removes (and returns) the first tree of the list of trees if not empty | ||
| unconsTree : ∀ {A n} → RAL-g A n → Maybe $ Tree A n × RAL-g A n |
There was a problem hiding this comment.
Same as above, lemma about underlying sizes / binary representations.
| unconsTree (e [ t ]I) = just (t , e O) | ||
|
|
||
| -- Retrieves an element in a list of trees | ||
| lookup-trees : ∀ {A n} → RAL-g A n → ℕ → Maybe A |
There was a problem hiding this comment.
Nasty. Would it be easier if we were indexing by a Bin instead of ℕ?
There was a problem hiding this comment.
I took the implementations from the document without putting too much though in whether they could be optimized or not. There's a section after that which tries to improve the runtime of the functions which might introduce changes like that but I still have not looked into that. Now that my understanding of the structure is better, I could make such attempts.
| (no _) → lookup-trees s (i ∸ pow)} | ||
|
|
||
| -- Replaces an element inside the structure | ||
| update-trees : ∀ {A n} → RAL-g A n → ℕ → A → RAL-g A n |
| -- To be improved, we are working with binary trees after all | ||
| -- It is sad to transform to vectors to lookup, but it's late | ||
| -- and I don't want to handle decidability cases with 2^k-1 | ||
| lookup-tree : ∀ {A k} → Tree A k → Fin (2 ^ k) → A |
There was a problem hiding this comment.
Would it be easier if we were not using a Fin (2 ^ k) but an inductive family indexed by k : Nat that represent numbers between 0 and 2^k:
data Finᵇ : Nat → Set where
here : ∀ {k} → Finᵇ k
left : ∀ {k} → Finᵇ k → Finᵇ (suc k)
right : ∀ {k} → Finᵇ k → Finᵇ (suc k)
Going left means + 0 * 2 ^ k while going right means + 1 * 2 ^ k.
WARNING: untested thought.
|
Thanks for these comments @pedagand |
|
I think so, yes. |
|
Thanks, I will fill these blanks and come up with less nasty implementations. |
This PR proposes an implementations for the primitives on binary random access lists.
It includes the following changes:
lookupandupdatefor treesA question: what is the semantics of the remaining primitives, namely
snoc,rearandfront. My guess:snocadds a tree of size k+1 at the end of the structurerearreturns the last tree of the structurefrontreturns the first tree of the structure