[ fix #683 ] re-export specialised versions of the constructors (#684)

Author: gallais

CHANGELOG.md

@@ -73,19 +73,16 @@ New modules
   Data.List.Relation.Binary.Suffix.Heterogeneous.Properties
   Data.List.Relation.Binary.Prefix.Heterogeneous
   Data.List.Relation.Binary.Prefix.Heterogeneous.Properties
-  Data.List.Relation.Binary.Sublist.Homogeneous.Properties
-  Data.List.Relation.Binary.Sublist.Homogeneous.Solver
   Data.List.Relation.Binary.Sublist.Heterogeneous
   Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
+  Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
   Data.List.Relation.Binary.Sublist.Setoid
   Data.List.Relation.Binary.Sublist.Setoid.Properties
   Data.List.Relation.Binary.Sublist.DecSetoid
-  Data.List.Relation.Binary.Sublist.DecSetoid.Properties
   Data.List.Relation.Binary.Sublist.DecSetoid.Solver
   Data.List.Relation.Binary.Sublist.Propositional
   Data.List.Relation.Binary.Sublist.Propositional.Properties
   Data.List.Relation.Binary.Sublist.DecPropositional
-  Data.List.Relation.Binary.Sublist.DecPropositional.Properties
   Data.List.Relation.Binary.Sublist.DecPropositional.Solver
   Data.List.Relation.Ternary.Interleaving.Setoid
   Data.List.Relation.Ternary.Interleaving.Setoid.Properties

src/Data/List/Relation/Binary/Sublist/DecPropositional.agda

@@ -1,22 +1,43 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- An inductive definition of the sublist relation for types which have a
--- decidable equality. This is commonly known as Order Preserving Embeddings (OPE).
+-- An inductive definition of the sublist relation for types which have
+-- a decidable equality. This is commonly known as Order Preserving
+-- Embeddings (OPE).
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Decidable)
+open import Relation.Binary
 open import Agda.Builtin.Equality using (_≡_)
 
 module Data.List.Relation.Binary.Sublist.DecPropositional
-       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
-       where
+  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+  where
 
-import Relation.Binary.PropositionalEquality as P
+open import Data.List.Relation.Binary.Equality.DecPropositional _≟_
+  using (_≡?_)
+import Data.List.Relation.Binary.Sublist.DecSetoid as DecSetoidSublist
+import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist
+open import Relation.Binary.PropositionalEquality
 
-open import Data.List.Relation.Binary.Sublist.DecSetoid (P.decSetoid _≟_)
-  hiding (lookup) public
-open import Data.List.Relation.Binary.Sublist.Propositional {A = A}
-  using (lookup) public
+------------------------------------------------------------------------
+-- Re-export core definitions and operations
+
+open PropositionalSublist {A = A} public
+open DecSetoidSublist (decSetoid _≟_) using (_⊆?_) public
+
+------------------------------------------------------------------------
+-- Additional relational properties
+
+⊆-isDecPartialOrder : IsDecPartialOrder _≡_ _⊆_
+⊆-isDecPartialOrder = record
+  { isPartialOrder = ⊆-isPartialOrder
+  ; _≟_            = _≡?_
+  ; _≤?_           = _⊆?_
+  }
+
+⊆-decPoset : DecPoset a a a
+⊆-decPoset = record
+  { isDecPartialOrder = ⊆-isDecPartialOrder
+  }

src/Data/List/Relation/Binary/Sublist/DecPropositional/Properties.agda

@@ -1,18 +1,46 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- An inductive definition of the sublist relation with respect to a setoid
--- which is decidable. This is a generalisation of what is commonly known as
--- Order Preserving Embeddings (OPE).
+-- An inductive definition of the sublist relation with respect to a
+-- setoid which is decidable. This is a generalisation of what is
+-- commonly known as Order Preserving Embeddings (OPE).
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (DecSetoid)
+open import Relation.Binary
 
-module Data.List.Relation.Binary.Sublist.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+module Data.List.Relation.Binary.Sublist.DecSetoid
+  {c ℓ} (S : DecSetoid c ℓ) where
 
-private
-  module S = DecSetoid S
+import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEquality
+import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
+import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
+  as HeterogeneousProperties
+open import Level using (_⊔_)
 
-open import Data.List.Relation.Binary.Sublist.Setoid S.setoid public
+open DecSetoid S
+open DecSetoidEquality S
+
+------------------------------------------------------------------------
+-- Re-export core definitions
+
+open SetoidSublist setoid public
+
+------------------------------------------------------------------------
+-- Additional relational properties
+
+_⊆?_ : Decidable _⊆_
+_⊆?_ = HeterogeneousProperties.sublist? _≟_
+
+⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
+⊆-isDecPartialOrder = record
+  { isPartialOrder = ⊆-isPartialOrder
+  ; _≟_            = _≋?_
+  ; _≤?_           = _⊆?_
+  }
+
+⊆-decPoset : DecPoset c (c ⊔ ℓ) (c ⊔ ℓ)
+⊆-decPoset = record
+  { isDecPartialOrder = ⊆-isDecPartialOrder
+  }

src/Data/List/Relation/Binary/Sublist/DecSetoid.agda

@@ -10,7 +10,7 @@ open import Relation.Binary using (DecSetoid)
 
 module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where
 
-private module S = DecSetoid S
+open DecSetoid S
 
-open import Data.List.Relation.Binary.Sublist.Homogeneous.Solver S._≈_ S.refl S._≟_
+open import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver _≈_ refl _≟_
   using (Item; module Item; TList; module TList; prove) public

src/Data/List/Relation/Binary/Sublist/DecSetoid/Properties.agda

@@ -8,7 +8,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.Relation.Binary.Sublist.Heterogeneous where
+open import Relation.Binary using (REL)
+
+module Data.List.Relation.Binary.Sublist.Heterogeneous
+  {a b r} {A : Set a} {B : Set b} {R : REL A B r}
+  where
 
 open import Level using (_⊔_)
 open import Data.List.Base using (List; []; _∷_; [_])
@@ -19,44 +23,39 @@ open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 ------------------------------------------------------------------------
--- Type and basic combinators
+-- Re-export core definitions
 
-module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
+open import Data.List.Relation.Binary.Sublist.Heterogeneous.Core public
 
-  data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
-    []   : Sublist [] []
-    _∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
-    _∷_  : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)
+------------------------------------------------------------------------
+-- Type and basic combinators
 
-module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
+module _ {s} {S : REL A B s} where
 
   map : R ⇒ S → Sublist R ⇒ Sublist S
   map f []        = []
   map f (y ∷ʳ rs) = y ∷ʳ map f rs
   map f (r ∷ rs)  = f r ∷ map f rs
 
-module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
-
-  minimum : Min (Sublist R) []
-  minimum []       = []
-  minimum (x ∷ xs) = x ∷ʳ minimum xs
+minimum : Min (Sublist R) []
+minimum []       = []
+minimum (x ∷ xs) = x ∷ʳ minimum xs
 
 ------------------------------------------------------------------------
 -- Conversion to and from Any
 
-  toAny : ∀ {a bs} → Sublist R [ a ] bs → Any (R a) bs
-  toAny (y ∷ʳ rs) = there (toAny rs)
-  toAny (r ∷ rs)  = here r
+toAny : ∀ {a bs} → Sublist R [ a ] bs → Any (R a) bs
+toAny (y ∷ʳ rs) = there (toAny rs)
+toAny (r ∷ rs)  = here r
 
-  fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs
-  fromAny (here r)  = r ∷ minimum _
-  fromAny (there p) = _ ∷ʳ fromAny p
+fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs
+fromAny (here r)  = r ∷ minimum _
+fromAny (there p) = _ ∷ʳ fromAny p
 
 ------------------------------------------------------------------------
 -- Generalised lookup based on a proof of Any
 
-module _ {a b p q r} {A : Set a} {B : Set b} {R : REL A B r}
-         {P : Pred A p} {Q : Pred B q} (resp : P ⟶ Q Respects R) where
+module _ {p q} {P : Pred A p} {Q : Pred B q} (resp : P ⟶ Q Respects R) where
 
   lookup : ∀ {xs ys} → Sublist R xs ys → Any P xs → Any Q ys
   lookup []       ()

src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda

@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This file contains some core definitions which are re-exported by
+-- Data.List.Relation.Binary.Sublist.Heterogeneous.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (REL)
+
+module Data.List.Relation.Binary.Sublist.Heterogeneous.Core
+       {a b r} {A : Set a} {B : Set b} (R : REL A B r)
+       where
+
+open import Level using (_⊔_)
+open import Data.List.Base using (List; []; _∷_; [_])
+
+data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
+  []   : Sublist [] []
+  _∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
+  _∷_  : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)