Updated to Agda-2.6.1

Author: effectfully

readme.md

@@ -2,6 +2,8 @@
 
 It's a library for doing generic programming in Agda.
 
+The library is tested with Agda-2.6.1 and likely does not work with other versions of Agda.
+
 # A quick taste
 
 Deriving decidable equality for vectors:
@@ -32,8 +34,6 @@ instance StarEq : ∀ {i t} {I : Set i} {T : Rel I t} {i j}
 unquoteDef StarEq = deriveEqTo StarEq (quote Star)
 ```
 
-(For this to type check you need the recent development version of Agda (as of 09.08.16))
-
 # Internally
 
 Descriptions of constructors are defined as follows:
@@ -216,7 +216,9 @@ There are also generic `elim` in [`Function/Elim.agda`](Function/Elim.agda) (the
 
 # Limitations
 
-- No inductive-inductive or inductive-recursive data types. The latter [can be done](https://github.com/effectfully/random-stuff/blob/master/Desc/IRDesc.agda) at the cost of complicating the encoding.
+- No support for mutually recursive data types. They can be supported, I just haven't implemented that.
+
+- No support for inductive-inductive or inductive-recursive data types. The latter [can be done](https://github.com/effectfully/random-stuff/blob/master/Desc/IRDesc.agda) at the cost of complicating the encoding.
 
 - No coinduction.
 
@@ -226,4 +228,4 @@ There are also generic `elim` in [`Function/Elim.agda`](Function/Elim.agda) (the
 
 - Ornaments may or may not appear later (in the way described in [Unbiased ornaments](http://effectfully.blogspot.com/2016/07/unbiased-ornaments.html)). I don't find them very vital currently.
 
-- No forcing of indices. [`Lift`](Examples/Data/Lift.agda) can be described, though.
+- No forcing of indices. [`Lift`](Examples/Data/Lift.agda) can be described, though.

src/Generic/Core.agda

@@ -12,7 +12,7 @@ _≤ℓ_ : Level -> Level -> Set
 α ≤ℓ β = α ⊔ β ≡ β
 
 mutual
-  Binder : ∀ {ι} α β γ -> Arg-info -> ι ⊔ lsuc (α ⊔ β) ≡ γ -> Set ι -> Set γ
+  Binder : ∀ {ι} α β γ -> ArgInfo -> ι ⊔ lsuc (α ⊔ β) ≡ γ -> Set ι -> Set γ
   Binder α β γ i q I = Coerce q (∃ λ (A : Set α) -> < relevance i > A -> Desc I β)
 
   data Desc {ι} (I : Set ι) β : Set (ι ⊔ lsuc β) where

src/Generic/Examples/Data/Product.agda

@@ -1,6 +1,6 @@
 module Generic.Examples.Data.Product where
 
-open import Generic.Main as Main hiding (Σ; proj₁; proj₂) renaming (_,_ to _,′_)
+open import Generic.Main as Main hiding (Σ; proj₁; proj₂; _,′_) renaming (_,_ to _,′_)
 
 infixr 4 _,_
 

src/Generic/Examples/DeriveEq.agda

@@ -6,7 +6,7 @@ open import Data.Vec using (Vec) renaming ([] to []ᵥ; _∷_ to _∷ᵥ_)
 
 module DeriveEqStar where
   open import Relation.Binary
-  open import Data.Star
+  open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
   instance StarEq : ∀ {i t} {I : Set i} {T : Rel I t} {i j}
                       {{iEq : Eq I}} {{tEq : ∀ {i j} -> Eq (T i j)}} -> Eq (Star T i j)

src/Generic/Lib/Reflection/Core.agda

@@ -1,13 +1,16 @@
 module Generic.Lib.Reflection.Core where
 
+open import Agda.Builtin.Reflection using (withNormalisation; Relevance; Visibility; clause) public
 open import Reflection
   renaming (visible to expl; hidden to impl; instance′ to inst;
     relevant to rel; irrelevant to irr; pi to absPi; lam to absLam; def to appDef)
-  hiding (var; con; meta; _≟_; return; _>>=_; _>>_) public
-open import Agda.Builtin.Reflection using (withNormalisation) public
+  hiding (Arg-info; var; con; meta; visibility; relevance; _≟_; return; _>>=_; _>>_) public
+open import Reflection.Argument.Information using (ArgInfo; visibility; relevance) public
+import Reflection.Name
 open Term    using () renaming (var to appVar; con to appCon; meta to appMeta) public
 open Pattern using () renaming (var to patVar; con to patCon) public
 open Literal using () renaming (meta to litMeta) public
+open Sort public
 
 open import Generic.Lib.Intro
 open import Generic.Lib.Equality.Propositional
@@ -238,7 +241,7 @@ open Data public
 
 instance
   NameEq : Eq Name
-  NameEq = viaBase _≟-Name_
+  NameEq = viaBase Reflection.Name._≟_
 
   EqRelValue : ∀ {α r} {A : Set α} {{aEq : RelEq r A}} -> Eq (< r > A)
   EqRelValue {A = A} {{aEq}} = record
@@ -286,7 +289,7 @@ mutual
   ren ι (lam v s t)     = lam v s (ren (keep ι) t)
   ren ι (pat-lam cs xs) = undefined where postulate undefined : _
   ren ι (pi s a b)      = pi s (ren ι <$> a) (ren (keep ι) b)
-  ren ι (sort s)        = sort (renSort ι s)
+  ren ι (agda-sort s)   = agda-sort (renSort ι s)
   ren ι (lit l)         = lit l
   ren ι (appMeta x xs)  = appMeta x (rens ι xs)
   ren ι  unknown        = unknown
@@ -322,7 +325,7 @@ mutual
   mapName f n (lam v s t)     = lam v s (mapName (f ∘ suc) n t)
   mapName f n (pat-lam cs xs) = undefined where postulate undefined : _
   mapName f n (pi s a b)      = pi s (mapName f n <$> a) (mapName (f ∘ suc) n b)
-  mapName f n (sort s)        = sort (mapNameSort f n s)
+  mapName f n (agda-sort s)   = agda-sort (mapNameSort f n s)
   mapName f n (lit l)         = lit l
   mapName f n (appMeta x xs)  = appMeta x (mapNames f n xs)
   mapName f n  unknown        = unknown
@@ -424,8 +427,8 @@ macro
     getType f >>= λ a ->
     let res = λ app -> quoteTC (vis# (countExplPis a) app f) >>= unify ?r in
     getDefinition f >>= λ
-      { (constructor′ _) -> res appCon
-      ;  _               -> res appDef
+      { (data-cons _) -> res appCon
+      ;  _            -> res appDef
       }
 
   sateMacro : Name -> Term -> TC _
@@ -442,9 +445,9 @@ unshift′ t = explLam "_" t · sate tt₀
 -- A note for myself: `foldℕ (sate lsuc) (sate lzero) n` is not `reify n`:
 -- it's damn `lsuc` -- not `suc`.
 termLevelOf : Term -> Maybe Term
-termLevelOf (sort (set t)) = just t
-termLevelOf (sort (lit n)) = just (foldℕ (sate lsuc) (sate lzero) n)
-termLevelOf (sort unknown) = just unknown
+termLevelOf (agda-sort (set t)) = just t
+termLevelOf (agda-sort (lit n)) = just (foldℕ (sate lsuc) (sate lzero) n)
+termLevelOf (agda-sort unknown) = just unknown
 termLevelOf _ = nothing
 
 instance
@@ -475,7 +478,7 @@ instance
         }
     }
 
-  ArgInfoReify : Reify Arg-info
+  ArgInfoReify : Reify ArgInfo
   ArgInfoReify = record
     { reify = λ{ (arg-info v r) -> sate arg-info (reify v) (reify r) }
     }
@@ -547,11 +550,11 @@ getData d = getNormType d >>= λ ab -> getDefinition d >>= λ
            {  nothing             -> panic "getData: data"
            ; (just (a , b , acs)) -> return ∘ uncurry (packData d a b) $ splitList acs
            }
-  ; (record′ c _)    -> getNormType c >>= dropPis (countPis ab) >>> λ
+  ; (record-type c _) -> getNormType c >>= dropPis (countPis ab) >>> λ
        {  nothing  -> panic "getData: record"
        ; (just a′) -> return $ packData d (initType ab) (lastType ab) (a′ ∷ []) (c , tt)
        }
-  ;  _               -> throw "not a data"
+  ;  _ -> throw "not a data"
   }
 
 macro

src/Generic/Lib/Reflection/Fold.agda

@@ -17,7 +17,7 @@ foldTypeOf (packData d a b cs ns) = appendType iab ∘ pi "π" π ∘ pi "P" P $
   ab   = appendType a b
   iab  = implicitize ab
   π    = implRelArg (quoteTerm Level)
-  P    = explRelArg ∘ appendType (shiftBy (suc j) b) ∘ sort ∘ set $ pureVar j
+  P    = explRelArg ∘ appendType (shiftBy (suc j) b) ∘ agda-sort ∘ set $ pureVar j
   hyp  = mapName (λ p -> appVar p ∘ drop i) d ∘ shiftBy (2 + j)
   _ʰ→_ = flip $ foldr (λ c r -> hyp c ‵→ shift r)
   from = appDef d (pisToArgVars (2 + i + j) ab)

src/Generic/Reflection/ReadData.agda

@@ -3,7 +3,7 @@ module Generic.Reflection.ReadData where
 open import Generic.Core
 open import Generic.Function.FoldMono
 
-‵π : Arg-info -> String -> Term -> Term -> Term
+‵π : ArgInfo -> String -> Term -> Term -> Term
 ‵π i s a b = sate π (reify i) (sate refl) ∘ sate coerce ∘ sate _,_ a $
   appDef (quote appRel) (implRelArg (reify (relevance i)) ∷ explRelArg (explLam s b) ∷ [])