Merge branch feature-partial-getlen into master

It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.

Conflicts: heavy
	BFF.agda (imports, bff type clash)
	Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
                    lemma-get-mapMV)
	Generic.agda (imports)
	Precond.agda (imports, bff type clash in assoc-enough)

1 files changed, 32 insertions, 1 deletions

diff --git a/GetTypes.agda b/GetTypes.agda
index 99675f9..eb72cea 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -1,10 +1,17 @@
 module GetTypes where
 
+open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ)
 open import Data.List using (List ; map)
 open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality using (_≗_)
+open import Function.Equality using (_⟶_ ; _⟨$⟩_)
+open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
+open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
+open import Relation.Binary using (Setoid)
+open Injection using (to)
+
+open import Generic using (≡-to-Π)
 
 module ListList where
   record Get : Set₁ where
@@ -18,3 +25,27 @@ module VecVec where
       getlen : ℕ → ℕ
       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+
+module PartialVecVec where
+  record Get : Set₁ where
+    field
+      I : Setoid ℓ₀ ℓ₀
+      gl₁ : I ↪ EqSetoid ℕ
+      gl₂ : I ⟶ EqSetoid ℕ
+
+    |I|   = Setoid.Carrier I
+    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₂| = _⟨$⟩_ gl₂
+
+    field
+      get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
+      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
+
+VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
+VecVec-to-PartialVecVec G = record
+  { I = EqSetoid ℕ
+  ; gl₁ = id↪
+  ; gl₂ = ≡-to-Π getlen
+  ; get = get
+  ; free-theorem = free-theorem
+  } where open VecVec.Get G