implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.

1 files changed, 18 insertions, 0 deletions

diff --git a/Instances.agda b/Instances.agda
new file mode 100644
index 0000000..faff6f8
--- /dev/null
+++ b/Instances.agda
@@ -0,0 +1,18 @@
+module Instances where
+
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import Structures using (Shaped)
+
+VecShaped : Shaped ℕ Vec
+VecShaped = record
+  { arity = id
+  ; content = id
+  ; fill = λ _ → id
+  ; isShaped = record
+    { content-fill = λ _ → refl
+    ; fill-content = λ _ _ → refl
+    } }