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, 18 insertions, 1 deletions

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index 2695491..d4eb174 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -1,10 +1,15 @@
 module FreeTheorems 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 _↪_)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
+open import Relation.Binary using (Setoid)
+open Injection using (to)
 
 import GetTypes
 
@@ -31,3 +36,15 @@ module VecVec where
 
   assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
+
+module PartialVecVec where
+  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
+  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
+
+  open GetTypes.PartialVecVec public
+
+  postulate
+    free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
+
+  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
+  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }