Adapt to agda/agda#5289 (#1453)

* Adapt to agda/agda#5289

* [ admin ] exclude more of the modules from the safe index

* [ fix ] add --rewriting option to index.agda

Author: jespercockx

.travis.yml

@@ -56,7 +56,7 @@ matrix:
              cd ../ &&
              git clone https://github.com/agda/agda &&
              cd agda &&
-             git checkout fec60970117acab3aeee56bea88bc38136db6c1b &&
+             git checkout 63218e5924df4e1a23ce9cb65e10a679c0cee0ce &&
              cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
           fi
 

CHANGELOG.md

@@ -37,6 +37,9 @@ Non-backwards compatible changes
   * The types of the `clause` and `absurd-clause` constructors of the
     `Clause` datatype now take an extra argument `(tel : Telescope)`,
     where `Telescope = List (String × Arg Type)`.
+  * The following constructors have been added to the `Sort` datatype:
+    `prop : (t : Term) → Sort`, `propLit : (n : Nat) → Sort`, and
+    `inf : (n : Nat) → Sort`.
 
   See the release notes of Agda 2.6.2 for more information.
 

src/Reflection/Annotated.agda

@@ -131,6 +131,9 @@ mutual
   data Sortₐ′ {ℓ} : Typeₐ ℓ ⟨sort⟩ where
     set     : ∀ {t} → Termₐ Ann t → Sortₐ′ Ann (set t)
     lit     : ∀ n → Sortₐ′ Ann (lit n)
+    prop    : ∀ {t} → Termₐ Ann t → Sortₐ′ Ann (prop t)
+    propLit : ∀ n → Sortₐ′ Ann (propLit n)
+    inf     : ∀ n → Sortₐ′ Ann (inf n)
     unknown : Sortₐ′ Ann unknown
 
   data Patternₐ′ {ℓ} : Typeₐ ℓ ⟨pat⟩ where
@@ -197,6 +200,9 @@ module _ (annFun : AnnotationFun Ann) where
     annotate′ {⟨pat⟩}     (absurd x)             = absurd x
     annotate′ {⟨sort⟩}    (set t)                = set (annotate t)
     annotate′ {⟨sort⟩}    (lit n)                = lit n
+    annotate′ {⟨sort⟩}    (prop t)               = prop (annotate t)
+    annotate′ {⟨sort⟩}    (propLit n)            = propLit n
+    annotate′ {⟨sort⟩}    (inf n)                = inf n
     annotate′ {⟨sort⟩}    unknown                = unknown
     annotate′ {⟨clause⟩}  (clause tel ps t)      = clause (annotate tel) (annotate ps) (annotate t)
     annotate′ {⟨clause⟩}  (absurd-clause tel ps) = absurd-clause (annotate tel) (annotate ps)
@@ -234,6 +240,9 @@ mutual
   map′ ⟨pat⟩       f (absurd x)           = absurd x
   map′ ⟨sort⟩      f (set t)              = set (map f t)
   map′ ⟨sort⟩      f (lit n)              = lit n
+  map′ ⟨sort⟩      f (prop t)             = prop (map f t)
+  map′ ⟨sort⟩      f (propLit n)          = propLit n
+  map′ ⟨sort⟩      f (inf n)              = inf n
   map′ ⟨sort⟩      f unknown              = unknown
   map′ ⟨clause⟩    f (clause Γ ps args)   = clause (map f Γ) (map f ps) (map f args)
   map′ ⟨clause⟩    f (absurd-clause Γ ps) = absurd-clause (map f Γ) (map f ps)
@@ -271,6 +280,9 @@ module _ {W : Set ℓ} (ε : W) (_∪_ : W → W → W) where
   defaultAnn ⟨pat⟩       (absurd x)           = ε
   defaultAnn ⟨sort⟩      (set t)              = ann t
   defaultAnn ⟨sort⟩      (lit n)              = ε
+  defaultAnn ⟨sort⟩      (prop t)             = ann t
+  defaultAnn ⟨sort⟩      (propLit n)          = ε
+  defaultAnn ⟨sort⟩      (inf n)              = ε
   defaultAnn ⟨sort⟩      unknown              = ε
   defaultAnn ⟨clause⟩    (clause Γ ps t)      = ann Γ ∪ (ann ps ∪ ann t)
   defaultAnn ⟨clause⟩    (absurd-clause Γ ps) = ann Γ ∪ ann ps
@@ -321,6 +333,9 @@ module Traverse {M : Set → Set} (appl : RawApplicative M) where
       traverse′ {⟨pat⟩}     (absurd x)           = pure (absurd x)
       traverse′ {⟨sort⟩}    (set t)              = set <$> traverse t
       traverse′ {⟨sort⟩}    (lit n)              = pure (lit n)
+      traverse′ {⟨sort⟩}    (prop t)             = prop <$> traverse t
+      traverse′ {⟨sort⟩}    (propLit n)          = pure (propLit n)
+      traverse′ {⟨sort⟩}    (inf n)              = pure (inf n)
       traverse′ {⟨sort⟩}    unknown              = pure unknown
       traverse′ {⟨clause⟩}  (clause Γ ps t)      = clause <$> traverse Γ <*> traverse ps <*> traverse t
       traverse′ {⟨clause⟩}  (absurd-clause Γ ps) = absurd-clause <$> traverse Γ <*> traverse ps

src/Reflection/Show.agda

@@ -97,6 +97,9 @@ mutual
   showSort : Sort → String
   showSort (set t) = "Set" <+> parensIfSpace (showTerm t)
   showSort (lit n) = "Set" ++ ℕ.show n -- no space to disambiguate from set t
+  showSort (prop t) = "Prop" <+> parensIfSpace (showTerm t)
+  showSort (propLit n) = "Prop" ++ ℕ.show n -- no space to disambiguate from prop t
+  showSort (inf n) = "Setω" ++ ℕ.show n
   showSort unknown = "unknown"
 
   showPatterns : List (Arg Pattern) → String

src/Reflection/Term.agda

@@ -237,6 +237,14 @@ set-injective refl = refl
 slit-injective : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y
 slit-injective refl = refl
 
+prop-injective : ∀ {x y} → prop x ≡ prop y → x ≡ y
+prop-injective refl = refl
+
+propLit-injective : ∀ {x y} → propLit x ≡ propLit y → x ≡ y
+propLit-injective refl = refl
+
+inf-injective : ∀ {x y} → inf x ≡ inf y → x ≡ y
+inf-injective refl = refl
 
 var x args ≟ var x′ args′ =
   Dec.map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×-dec args ≟-Args args′)
@@ -349,13 +357,40 @@ unknown     ≟ pat-lam _ _ = no λ()
 
 set t   ≟-Sort set t′  = Dec.map′ (cong set) set-injective (t ≟ t′)
 lit n   ≟-Sort lit n′  = Dec.map′ (cong lit) slit-injective (n ℕ.≟ n′)
+prop t   ≟-Sort prop t′  = Dec.map′ (cong prop) prop-injective (t ≟ t′)
+propLit n   ≟-Sort propLit n′  = Dec.map′ (cong propLit) propLit-injective (n ℕ.≟ n′)
+inf n   ≟-Sort inf n′  = Dec.map′ (cong inf) inf-injective (n ℕ.≟ n′)
 unknown ≟-Sort unknown = yes refl
 set _   ≟-Sort lit _   = no λ()
+set _   ≟-Sort prop _   = no λ()
+set _   ≟-Sort propLit _   = no λ()
+set _   ≟-Sort inf _   = no λ()
 set _   ≟-Sort unknown = no λ()
 lit _   ≟-Sort set _   = no λ()
+lit _   ≟-Sort prop _   = no λ()
+lit _   ≟-Sort propLit _   = no λ()
+lit _   ≟-Sort inf _   = no λ()
 lit _   ≟-Sort unknown = no λ()
+prop _  ≟-Sort set _   = no λ()
+prop _  ≟-Sort lit _   = no λ()
+prop _  ≟-Sort propLit _   = no λ()
+prop _  ≟-Sort inf _   = no λ()
+prop _  ≟-Sort unknown   = no λ()
+propLit _  ≟-Sort set _   = no λ()
+propLit _  ≟-Sort lit _   = no λ()
+propLit _  ≟-Sort prop _   = no λ()
+propLit _  ≟-Sort inf _   = no λ()
+propLit _  ≟-Sort unknown   = no λ()
+inf _  ≟-Sort set _   = no λ()
+inf _  ≟-Sort lit _   = no λ()
+inf _  ≟-Sort prop _   = no λ()
+inf _  ≟-Sort propLit _   = no λ()
+inf _  ≟-Sort unknown   = no λ()
 unknown ≟-Sort set _   = no λ()
 unknown ≟-Sort lit _   = no λ()
+unknown ≟-Sort prop _   = no λ()
+unknown ≟-Sort propLit _   = no λ()
+unknown ≟-Sort inf _   = no λ()
 
 
 pat-con-injective₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′

src/Reflection/Traversal.agda

@@ -111,9 +111,12 @@ module _ (actions : Actions) where
   traverseTel Γ ((x , ty) ∷ tel) =
     _∷_ ∘ (x ,_) <$> traverseArg Γ ty ⊛ traverseTel ((x , ty) ∷cxt Γ) tel
 
-  traverseSort Γ (Sort.set t)   = Sort.set <$> traverseTerm Γ t
-  traverseSort Γ t@(Sort.lit _) = pure t
-  traverseSort Γ [email protected] = pure t
+  traverseSort Γ (Sort.set t)       = Sort.set <$> traverseTerm Γ t
+  traverseSort Γ t@(Sort.lit _)     = pure t
+  traverseSort Γ (Sort.prop t)      = Sort.prop <$> traverseTerm Γ t
+  traverseSort Γ t@(Sort.propLit _) = pure t
+  traverseSort Γ t@(Sort.inf _)     = pure t
+  traverseSort Γ [email protected]     = pure t
 
   traversePattern Γ (Pattern.con c ps) = Pattern.con <$> onCon Γ c ⊛ traversePats Γ ps
   traversePattern Γ (Pattern.dot t)    = Pattern.dot <$> traverseTerm Γ t

travis/index.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module index where
 
 -- You probably want to start with this module:

travis/index.sh

@@ -7,6 +7,12 @@ for file in $( find src -name "*.agda" | sort ); do
     if [[ ! $i == *Unsafe \
        && ! $i == Reflection \
        && ! $i == IO* \
-       && ! $i == *TrustMe ]]; then echo "import $i" >> safe.agda; fi
+       && ! $i == *TrustMe \
+       && ! $i == Debug* \
+       && ! $i == Codata.Musical* \
+       && ! $i == Foreign* \
+       && ! $i == System* \
+       && ! $i == Text.Pretty* \
+       ]]; then echo "import $i" >> safe.agda; fi
   fi
 done