port to agda/2.6.0.1 and agda-stdlib/1.1

 * Data.Vec.lookup changed parameter order.
 * A number of symbols were moved from Data.Maybe to submodules.
 * In a number of occasions, agda no longer figures implicit arguments
   and they had to be made explicit.
 * We can no longer use heterogeneous proofs inside equational reasoning
   for propositional equality. Use heterogeneous equational reasoning.
 * Stop importing proof-irrelevance as that would require K.

7 files changed, 29 insertions, 24 deletions

diff --git a/BFF.agda b/BFF.agda
index 06744f6..74380a9 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -35,7 +35,7 @@ module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
     where open Shaped ShapeT
 
   denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α
-  denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c)
+  denumerate ShapeT c = lookupV (Shaped.content ShapeT c)
 
   bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j))
   bff G {i} j s v = let s′ = enumerate SourceShapeT (gl₁ i)
diff --git a/Bidir.agda b/Bidir.agda
index 64f6d1b..e31d844 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -8,8 +8,10 @@ open import Data.Fin using (Fin)
 import Level
 import Category.Monad
 import Category.Functor
-open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just ; just-injective) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
+open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
 import Data.Maybe.Categorical
+open import Data.Maybe.Properties using (just-injective)
+open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing ; drop-just) renaming (setoid to MaybeSetoid ; Pointwise to MaybeEq)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.List using (List)
@@ -100,7 +102,7 @@ lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT
 lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
   fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
     ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
-  fill s (map (flip lookupVec (content c)) (allFin (arity s)))
+  fill s (map (lookupVec (content c)) (allFin (arity s)))
     ≡⟨ P.cong (fill s) (map-lookup-allFin (content c)) ⟩
   fill s (content c)
     ≡⟨ content-fill c ⟩
@@ -275,7 +277,7 @@ module _ (G : Get) where
     contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
       ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
     map (flip lookupM (h↦h′ h)) (contentV (get t))
-      ≡⟨ lemma-exchange-maps (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
+      ≡⟨ lemma-exchange-maps (h↦h′ h) h (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
     map (flip lookupM h) (contentV (get t))
       ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
     map just (contentV v)
diff --git a/CheckInsert.agda b/CheckInsert.agda
index 9447b04..dbba6e6 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -6,7 +6,8 @@ module CheckInsert (A : DecSetoid ℓ₀ ℓ₀) where
 open import Data.Nat using (ℕ)
 open import Data.Fin using (Fin)
 open import Data.Fin.Properties using (_≟_)
-open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
+open import Data.Maybe using (Maybe ; nothing ; just)
+open import Data.Maybe.Relation.Binary.Pointwise using () renaming (setoid to MaybeSetoid)
 open import Data.Vec using (Vec) renaming (_∷_ to _∷V_)
 open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
diff --git a/FinMap.agda b/FinMap.agda
index 6342fc5..051014c 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -2,7 +2,8 @@ module FinMap where
 
 open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ ; zero ; suc)
-open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective)
+open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
+open import Data.Maybe.Properties using (just-injective)
 open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
@@ -40,7 +41,7 @@ FinMapMaybe : ℕ → Set → Set
 FinMapMaybe n A = Vec (Maybe A) n
 
 lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A
-lookupM = lookupVec
+lookupM = flip lookupVec
 
 insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A
 insert f a m = m [ f ]≔ (just a)
@@ -129,6 +130,6 @@ lemma-disjoint-union {n} f t = tabulate-cong inner
             ≡⟨ P.cong (flip (maybe′ just) nothing) (lookup∘tabulate (just ∘ f) x) ⟩
           just (f x) ∎
 
-lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
-lemma-exchange-maps h≈h′ {[]}     All.[]         = P.refl
-lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
+lemma-exchange-maps : {n m : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
+lemma-exchange-maps h h' h≈h′ {[]}     All.[]         = P.refl
+lemma-exchange-maps h h' h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h h' h≈h′ pis)
diff --git a/Generic.agda b/Generic.agda
index 323688a..ed9d4a4 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -3,8 +3,9 @@ module Generic where
 import Category.Functor
 import Category.Monad
 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
-open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq)
+open import Data.Maybe using (Maybe ; just ; nothing)
 import Data.Maybe.Categorical
+open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing) renaming (setoid to MaybeEq)
 open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
 open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
diff --git a/LiftGet.agda b/LiftGet.agda
index 4ddf26f..e0a6932 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -8,7 +8,7 @@ open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
 open import Data.List.Properties using (length-map ; length-replicate)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (_∘_ ; flip ; const)
-open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; proof-irrelevance ; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
 open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable)
 
 import FreeTheorems
@@ -30,16 +30,16 @@ toList∘map f (x ∷V xs) = P.cong (_∷_ (f x)) (toList∘map f xs)
 GetV-to-GetL : GetV → GetL
 GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
   where open GetV getrecord
-        open ≡-Reasoning
+        open ≅-Reasoning
         ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
-        ft f xs = begin
+        ft f xs = ≅-to-≡ (begin
           toList (get (fromList (map f xs)))
             ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (H.reflexive (length-map f xs)) (fromList∘map f xs) ⟩
           toList (get (mapV f (fromList xs)))
             ≡⟨ P.cong toList (free-theorem f (fromList xs)) ⟩
           toList (mapV f (get (fromList xs)))
             ≡⟨ toList∘map f (get (fromList xs)) ⟩
-          map f (toList (get (fromList xs))) ∎
+          map f (toList (get (fromList xs))) ∎)
 
 getList-to-getlen : get-type → ℕ → ℕ
 getList-to-getlen get = length ∘ get ∘ flip replicate tt
diff --git a/Precond.agda b/Precond.agda
index 9b4a66c..9d21022 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -42,28 +42,28 @@ lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.j
 lemma-maybe-just a (just x) = P.refl
 lemma-maybe-just a nothing  = P.refl
 
-lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
-lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (tabulate-cong (λ f → begin
+lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} (h : FinMapMaybe n A) {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
+lemma-union-delete-fromFunc {is = []} h {g = g} p = _ , (tabulate-cong (λ f → begin
       maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
         ≡⟨ P.cong (flip (maybe′ just) (lookupM f h)) (lookup∘tabulate (just ∘ g) f) ⟩
       maybe′ just (just (g f)) (lookupM f h)
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
       just (maybe′ id (g f) (lookupM f h)) ∎))
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
   union h (delete i (delete-many is (fromFunc g)))
     ≡⟨ tabulate-cong inner ⟩
   union h (delete-many is (fromFunc g))
-    ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
+    ≡⟨ proj₂ (lemma-union-delete-fromFunc h ps) ⟩
   _ ∎)
-  where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
+  where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup h f) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup h f)
         inner f with f ≟ i
         inner .i | yes P.refl = begin
-          maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h)
+          maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup h i)
             ≡⟨ P.cong (maybe′ just _) px ⟩
           just x
             ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩
-          maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
-        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lookup∘update′ f≢i (delete-many is (fromFunc g)) nothing)
+          maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup h i) ∎
+        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup h f)) (lookup∘update′ f≢i (delete-many is (fromFunc g)) nothing)
 
 module _ (G : Get) where
   open Get G
@@ -96,7 +96,7 @@ module _ (G : Get) where
           g  = fromFunc (denumerate SourceShapeT s)
           g′ = delete-many (contentV (get s′)) g
           t  = enumerate SourceShapeT (gl₁ i)
-          wp = lemma-union-delete-fromFunc (lemma-assoc-domain (contentV (get t)) (contentV v) p)
+          wp = lemma-union-delete-fromFunc h (lemma-assoc-domain (contentV (get t)) (contentV v) p)
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []