allow importing of Bidir without any postulates

6 files changed, 31 insertions, 15 deletions

diff --git a/BFF.agda b/BFF.agda
index 79f3b3d..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)
+  open GetTypes.VecVec public using (Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
diff --git a/Bidir.agda b/Bidir.agda
index 42f8821..e792b3a 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -24,8 +24,8 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ;
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
-import FreeTheorems
-open FreeTheorems.VecVec using (Get ; module Get)
+import GetTypes
+open GetTypes.VecVec using (Get ; module Get)
 open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
 open import FinMap
 import CheckInsert
diff --git a/Everything.agda b/Everything.agda
index 76beef6..7399254 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -4,6 +4,7 @@ module Everything where
 import Generic
 import FinMap
 import CheckInsert
+import GetTypes
 import FreeTheorems
 import BFF
 import Bidir
diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index d2ba3ef..2695491 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -6,14 +6,13 @@ open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality using (_≗_)
 
+import GetTypes
+
 module ListList where
   get-type : Set₁
   get-type = {A : Set} → List A → List A
 
-  record Get : Set₁ where
-    field
-      get : {A : Set} → List A → List A
-      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+  open GetTypes.ListList public
 
   postulate
     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
@@ -25,11 +24,7 @@ module VecVec where
   get-type : (ℕ → ℕ) → Set₁
   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
 
-  record Get : Set₁ where
-    field
-      getlen : ℕ → ℕ
-      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
-      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+  open GetTypes.VecVec public
 
   postulate
     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
diff --git a/GetTypes.agda b/GetTypes.agda
new file mode 100644
index 0000000..99675f9
--- /dev/null
+++ b/GetTypes.agda
@@ -0,0 +1,20 @@
+module GetTypes where
+
+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 (_≗_)
+
+module ListList where
+  record Get : Set₁ where
+    field
+      get : {A : Set} → List A → List A
+      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+
+module VecVec where
+  record Get : Set₁ where
+    field
+      getlen : ℕ → ℕ
+      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
diff --git a/Precond.agda b/Precond.agda
index a1f1081..2be3f3a 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -30,8 +30,8 @@ import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
-import FreeTheorems
-open FreeTheorems.VecVec using (Get ; module Get)
+import GetTypes
+open GetTypes.VecVec using (Get ; module Get)
 open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v)