Update to stdlib 2.1.1 and other changes.main

I don't fully know what has changed because the changes are so old.

Doesn't yet compile due to not finishing proofs in `CBPV.Frex.Comp`.

1 files changed, 27 insertions, 8 deletions

diff --git a/src/CBPV/Context.agda b/src/CBPV/Context.agda
index d1aafc4..0ab5093 100644
--- a/src/CBPV/Context.agda
+++ b/src/CBPV/Context.agda
@@ -1,6 +1,7 @@
 module CBPV.Context where
 
 open import Data.Bool using (Bool)
+open import Data.List using (List; []; _∷_)
 open import Data.String using (String)
 import Data.String.Properties as String
 
@@ -15,23 +16,41 @@ abstract
   𝔪 : Name
   𝔪 = "𝔪"
 
-record Named : Set where
+record GenNamed (A : Set) : Set where
   constructor _:-_
   field
     name   : Name
-    ofType : ValType
+    ofType : A
 
-open Named public
+open GenNamed public
 
-infixl 5 _:<_ _++_
+Named : Set
+Named = GenNamed ValType
 
-data Context : Set where
-  [<]  : Context
-  _:<_ : Context → (ex : Named) → Context
+infixl 5 _:<_ _++_ _<><_
+
+data GenContext (A : Set) : Set where
+  [<]  : GenContext A
+  _:<_ : GenContext A → (ex : GenNamed A) → GenContext A
+
+Context : Set
+Context = GenContext ValType
+
+map : {A B : Set} → (A → B) → GenContext A → GenContext B
+map f [<] = [<]
+map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty)
+
+foldr : {A B : Set} → (A → B → B) → B → GenContext A → B
+foldr f z [<] = z
+foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ
 
 pattern [<_:-_] x A = [<] :< (x :- A)
 pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
 
-_++_ : Context → Context → Context
+_++_ : {A : Set} → GenContext A → GenContext A → GenContext A
 Γ ++ [<] = Γ
 Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
+
+_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A
+Γ <>< [] = Γ
+Γ <>< (x ∷ xs) = Γ :< x <>< xs