drop PartialShapeVec
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 3 Apr 2014 06:45:19 +0000 (08:45 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 3 Apr 2014 06:45:19 +0000 (08:45 +0200)
One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.

BFF.agda
GetTypes.agda

index 12524ca..26d1d5e 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -18,7 +18,7 @@ open import Generic using (sequenceV ; ≡-to-Π)
 open import Structures using (Shaped ; module Shaped)
 open import Instances using (VecShaped)
 import CheckInsert
 open import Structures using (Shaped ; module Shaped)
 open import Instances using (VecShaped)
 import CheckInsert
-open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec ; PartialShapeVec-to-PartialShapeShape)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeShape)
 
 module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.PartialShapeShape public using (Get ; module Get)
 
 module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.PartialShapeShape public using (Get ; module Get)
@@ -67,10 +67,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate = PartialShapeBFF.denumerate A VecShaped
 
   bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
   denumerate = PartialShapeBFF.denumerate A VecShaped
 
   bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
-  bff G j s v = PartialShapeBFF.bff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+  bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeShape G) j s v
 
   sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
 
   sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
-  sbff  G j s v = PartialShapeBFF.sbff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+  sbff  G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
index 2812e2b..f23d154 100644 (file)
@@ -52,39 +52,6 @@ VecVec-to-PartialVecVec G = record
   ; free-theorem = free-theorem
   } where open VecVec.Get G
 
   ; free-theorem = free-theorem
   } where open VecVec.Get G
 
-module PartialShapeVec where
-  record Get : Set₁ where
-    field
-      Shape : Set
-      Container : Set → Shape → Set
-      ShapeT : Shaped Shape Container
-
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ↪ EqSetoid Shape
-      gl₂ : I ⟶ EqSetoid ℕ
-
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ (to gl₁)
-    |gl₂| = _⟨$⟩_ gl₂
-
-    open Shaped ShapeT using (fmap)
-
-    field
-      get : {A : Set} {i : |I|} → Container A (|gl₁| i) → Vec A (|gl₂| i)
-      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmap f ≗ mapV f ∘ get
-
-    open Shaped ShapeT public
-
-PartialVecVec-to-PartialShapeVec : PartialVecVec.Get → PartialShapeVec.Get
-PartialVecVec-to-PartialShapeVec G = record
-  { ShapeT       = VecShaped
-  ; I            = I
-  ; gl₁          = gl₁
-  ; gl₂          = gl₂
-  ; get          = get
-  ; free-theorem = free-theorem
-  } where open PartialVecVec.Get G
-
 module PartialShapeShape where
   record Get : Set₁ where
     field
 module PartialShapeShape where
   record Get : Set₁ where
     field
@@ -114,13 +81,13 @@ module PartialShapeShape where
     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
 
     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
 
-PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get
-PartialShapeVec-to-PartialShapeShape G = record
-  { SourceShapeT = ShapeT
+PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
+PartialVecVec-to-PartialShapeShape G = record
+  { SourceShapeT = VecShaped
   ; ViewShapeT   = VecShaped
   ; I            = I
   ; gl₁          = gl₁
   ; gl₂          = gl₂
   ; get          = get
   ; free-theorem = free-theorem
   ; ViewShapeT   = VecShaped
   ; I            = I
   ; gl₁          = gl₁
   ; gl₂          = gl₂
   ; get          = get
   ; free-theorem = free-theorem
-  } where open PartialShapeVec.Get G
+  } where open PartialVecVec.Get G