added Everything.agda, cleaned examples

Author: flupe

Everything.agda

@@ -0,0 +1,34 @@
+module Everything where
+
+import Generics.Prelude
+import Generics.Telescope
+import Generics.Telescope.Equality
+import Generics.Desc
+import Generics.All
+import Generics.HasDesc
+import Generics.Accessibility
+import Generics.Helpers
+import Generics.Reflection
+
+import Generics.Mu
+import Generics.Mu.All
+import Generics.Mu.Elim
+import Generics.Mu.Fold
+import Generics.Mu.Conversion
+
+import Generics.Constructions.Case
+import Generics.Constructions.Cong
+import Generics.Constructions.DecEq
+import Generics.Constructions.Elim
+import Generics.Constructions.Fold
+import Generics.Constructions.Mu
+import Generics.Constructions.Recursion
+import Generics.Constructions.Show
+
+import Generics
+
+-- Work In Progress
+---------------------------------
+
+-- import Generics.Mu.NoConfusion
+-- import Generics.Constructions.Injective

examples/Elim.agda

@@ -1,30 +1,22 @@
 {-# OPTIONS --safe #-}
-open import Generics.Prelude hiding (lookup; _≟_)
-open import Generics.HasDesc
-open import Generics.Desc
-open import Generics.Telescope
-open import Generics.Reflection
-
-open import Generics.Constructions.Show as Show
-open import Generics.Constructions.Case
-open import Generics.Constructions.Elim
-open import Generics.Constructions.Fold
-open import Generics.Constructions.Cong
-open import Generics.Helpers
--- open import Generics.Constructions.DecEq
+
+module Parametrized where
+
+open import Generics
+
+open import Agda.Primitive
+open import Function.Base
+open import Data.Nat.Base hiding (pred)
+open import Data.Fin.Base hiding (pred; _+_)
+open import Data.List.Base hiding (sum; length)
 
 open import Relation.Nullary
 open import Relation.Nullary.Decidable as Decidable
 open import Relation.Binary.HeterogeneousEquality.Core using (_≅_; refl)
+open import Relation.Binary.PropositionalEquality
 
 open import Data.String hiding (show; _≟_; length)
 open import Data.Maybe.Base
-open import Data.Nat.Base using (_*_)
-
-
-module Parametrized where
-
-open Show.Show ⦃...⦄
 
 
 module Nat where
@@ -36,11 +28,13 @@ module Nat where
   ---------------------------
   -- Deriving the eliminator
 
+  elimℕ = deriveElim natD
+
   plus : ℕ → ℕ → ℕ
-  plus n = elim (const ℕ) n (const suc)
+  plus n = elimℕ (const ℕ) n suc
 
   mult : ℕ → ℕ → ℕ
-  mult n = elim (const ℕ) 0 (const (plus n))
+  mult n = elimℕ (const ℕ) 0 (plus n)
 
   -- things defined with the eliminator reduce properly on open terms
 
@@ -93,23 +87,23 @@ module Nat where
   congℕ = deriveCong natD
 
   ze≅ze : 0 ≅ 0
-  ze≅ze = congℕ Fin.zero
+  ze≅ze = congℕ zero
 
   su≅su : ∀ {n m} → n ≅ m → suc n ≅ suc m
   su≅su = congℕ (suc zero)
 
-
   -------------------------------
   -- Deriving decidable equality
 
-  -- instance decℕ : DecEq ℕ
-  --          decℕ = deriveDecEq natD
+  instance decℕ : DecEq ℕ
+           decℕ = deriveDecEq natD
 
-  -- _ : 3 ≟ 3 ≡ yes refl
-  -- _ = refl
+  _ : 3 ≟ 3 ≡ yes refl
+  _ = refl
+
+  _ : 3 ≟ 2 ≡ no _
+  _ = refl
 
-  -- _ : 3 ≟ 2 ≡ no _
-  -- _ = refl
 
 module ListDemo where
 
@@ -134,39 +128,40 @@ module ListDemo where
   mul : list ℕ → ℕ
   mul = foldList 1 _*_
 
-module Vek where
+
+module Vec where
   private variable A : Set
                    n : ℕ
 
-  data Vek (A : Set) : ℕ → Set where
-    nil  : Vek A 0
-    cons : ∀ {n} → A → Vek A n → Vek A (suc n)
+  data Vec (A : Set) : ℕ → Set where
+    nil  : Vec A 0
+    cons : ∀ {n} → A → Vec A n → Vec A (suc n)
 
   instance
-    vekD : HasDesc Vek
-    vekD = deriveDesc Vek
+    vekD : HasDesc Vec
+    vekD = deriveDesc Vec
 
   ---------------------------
   -- Deriving the eliminator
 
-  elimVek = deriveElim vekD
+  elimVec = deriveElim vekD
 
-  length : Vek A n → ℕ
-  length = elimVek (const ℕ) 0 (λ x xs n → suc n)
+  length : Vec A n → ℕ
+  length = elimVec (const ℕ) 0 (const suc)
 
-  length0 : length (nil {A = A}) ≡ 0
+  length0 : length (nil {A}) ≡ 0
   length0 = refl
 
-  lengthP : (x : Vek A n) → length x ≡ n
-  lengthP = elimVek (λ {n} x → length x ≡ n) refl λ x xs Pxs → cong suc Pxs
+  lengthP : (x : Vec A n) → length x ≡ n
+  lengthP = elimVec (λ {n} x → length x ≡ n) refl (const (cong suc))
 
   ---------------------------
   -- Deriving fold
 
-  foldVek = deriveFold vekD
+  foldVec = deriveFold vekD
 
-  vekToList : ∀ {A n} → Vek A n → List A
-  vekToList = foldVek [] _∷_
+  vekToList : ∀ {A n} → Vec A n → List A
+  vekToList = foldVec [] _∷_
 
   -----------------------
   -- Deriving congruence
@@ -176,7 +171,7 @@ module Vek where
   []≅[] : ∀ {A} → nil {A} ≅ nil {A}
   []≅[] = congV zero
 
-  cong-cons : ∀ {A n} {x y : A} → x ≅ y → {xs ys : Vek A n} → xs ≅ ys
+  cong-cons : ∀ {A n} {x y : A} → x ≅ y → {xs ys : Vec A n} → xs ≅ ys
             → cons x xs ≅ cons y ys
   cong-cons = congV (suc zero) refl
 
@@ -196,14 +191,15 @@ module WType  where
   -- Deriving the eliminator
 
   elimW : (Pr : W A B → Set c)
-        → (∀ x g → (∀ y → Pr (g y)) → Pr (node x g) )
+        → (∀ x {g} → (∀ y → Pr (g y)) → Pr (node x g) )
         → ∀ x → Pr x
   elimW = deriveElim wD
 
   elimW-node
     : {Pr : W A B → Set c}
-      (M : ∀ x g → (∀ y → Pr (g y)) → Pr (node x g) )
-    → ∀ {x g} → elimW Pr M (node x g) ≡ M x g (λ y → elimW Pr M (g y))
+      (M : ∀ x {g} → (∀ y → Pr (g y)) → Pr (node x g) )
+    → ∀ {x g}
+    → elimW Pr M (node x g) ≡ M x (λ y → elimW Pr M (g y))
   elimW-node M = refl
 
 
@@ -230,6 +226,5 @@ module Irrelevance where
   instance showSquash : ∀ {A} → Show (Squash A)
            showSquash = deriveShow squashD
 
-  -- Indeed, we use the argument name when printing irrelevant args
-  _ : show (squash 3) ≡ "squash (.x)"
+  _ : show (squash 3) ≡ "squash (._)"
   _ = refl

examples/Parametrized.agda

@@ -0,0 +1,16 @@
+{-# OPTIONS --safe #-}
+module Generics where
+
+open import Data.Unit                    public using (⊤; tt)
+open import Generics.Prelude             public using (liftω; liftω-inst)
+open import Generics.HasDesc             public using (HasDesc)
+open import Generics.Reflection          public using (deriveDesc)
+open import Generics.Helpers             public
+
+open import Generics.Constructions.Case       public using (deriveCase)
+open import Generics.Constructions.Cong       public using (deriveCong)
+open import Generics.Constructions.DecEq      public using (DecEq; _≟_; deriveDecEq)
+open import Generics.Constructions.Elim       public using (deriveElim)
+open import Generics.Constructions.Fold       public using (deriveFold)
+open import Generics.Constructions.Recursion  public using (rec; Below)
+open import Generics.Constructions.Show       public using (Show; show; deriveShow)