Merge branch feature-get-record into master

This branch brings three main benefits:
 * Only one explicit parameter is needed to ask for a get function.
 * The postulated free theorems are mostly turned into preconditions,
   i.e. the only use of the postulates is in LiftGet.
 * We can now convert list based get functions to vec based ones and back
   including the (now) accompanying free theorem.

1 files changed, 5 insertions, 5 deletions

diff --git a/BFF.agda b/BFF.agda
index 61eeefd..ddf2307 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -16,10 +16,10 @@ open import Relation.Binary using (DecSetoid ; module DecSetoid)
 open import FinMap
 open import Generic using (mapMV)
 import CheckInsert
-import FreeTheorems
+import GetTypes
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open FreeTheorems.VecVec public using (get-type)
+  open GetTypes.VecVec public using (Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
@@ -33,9 +33,9 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
   denumerate = flip lookupV
 
-  bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
-  bff get s v = let s′ = enumerate s
-                    t′ = get s′
+  bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n))
+  bff G s v = let   s′ = enumerate s
+                    t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
                     h  = assoc t′ v