Skip to content

Commit be9ac3a

Browse files
gallaisgallais
authored
[ new ] inductive definition of Infix (#1348)
1 parent e175f89 commit be9ac3a

File tree

7 files changed

+430
-58
lines changed

7 files changed

+430
-58
lines changed

‎CHANGELOG.md

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,9 @@ New modules
102102
* Added `Reflection.Traversal` for generic de Bruijn-aware traversals of reflected terms.
103103
* Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
104104
on reflected terms.
105+
105106
* Added `Relation.Binary.TypeClasses` for type classes to be used with instance search.
107+
106108
* Added various modules containing `instance` declarations:
107109
`Data.Bool.Instances`, `Data.Char.Instances`, `Data.Fin.Instances`,
108110
`Data.Float.Instances`, `Data.Integer.Instances`,
@@ -123,7 +125,23 @@ New modules
123125
Algebra.Properties.CommutativeSemigroup.Divisibility
124126
```
125127

126-
* Added bindings for Haskell's `System.Environment`
128+
* Heterogeneous relation characterising a list as an infix segment of another:
129+
```
130+
Data.List.Relation.Binary.Infix.Heterogeneous
131+
Data.List.Relation.Binary.Infix.Heterogeneous.Properties
132+
```
133+
and added `Properties` file for the homogeneous variants of (pre/in/suf)fix:
134+
```
135+
Data.List.Relation.Binary.Prefix.Homogeneous.Properties
136+
Data.List.Relation.Binary.Infix.Homogeneous.Properties
137+
Data.List.Relation.Binary.Suffix.Homogeneous.Properties
138+
```
139+
140+
* Added bindings for Haskell's `System.Environment`:
141+
```
142+
System.Environment
143+
System.Environment.Primitive
144+
```
127145

128146
Other major changes
129147
-------------------

‎src/Data/List/Relation/Binary/Infix/Heterogeneous.agda

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- An inductive definition of the heterogeneous infix relation
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.List.Relation.Binary.Infix.Heterogeneous where
10+
11+
open import Level
12+
open import Relation.Binary using (REL; _⇒_)
13+
open import Data.List.Base as List using (List; []; _∷_)
14+
open import Data.List.Relation.Binary.Pointwise
15+
using (Pointwise)
16+
open import Data.List.Relation.Binary.Prefix.Heterogeneous
17+
as Prefix using (Prefix; []; _∷_)
18+
19+
private
20+
variable
21+
a b r s : Level
22+
A : Set a
23+
B : Set b
24+
R : REL A B r
25+
S : REL A B s
26+
27+
module _ {A : Set a} {B : Set b} (R : REL A B r) where
28+
29+
data Infix : REL (List A) (List B) (a ⊔ b ⊔ r) where
30+
here : ∀ {as bs} → Prefix R as bs → Infix as bs
31+
there : ∀ {b as bs} → Infix as bs → Infix as (b ∷ bs)
32+
33+
data View (as : List A) : List B → Set (a ⊔ b ⊔ r) where
34+
MkView : ∀ pref {inf} → Pointwise R as inf → ∀ suff →
35+
View as (pref List.++ inf List.++ suff)
36+
37+
map : R ⇒ S → Infix R ⇒ Infix S
38+
map R⇒S (here pref) = here (Prefix.map R⇒S pref)
39+
map R⇒S (there inf) = there (map R⇒S inf)
40+
41+
toView : ∀ {as bs} → Infix R as bs → View R as bs
42+
toView (here p) with Prefix.toView p
43+
...| inf Prefix.++ suff = MkView [] inf suff
44+
toView (there p) with toView p
45+
... | MkView pref inf suff = MkView (_ ∷ pref) inf suff
46+
47+
fromView : ∀ {as bs} → View R as bs → Infix R as bs
48+
fromView (MkView [] inf suff) = here (Prefix.fromView (inf Prefix.++ suff))
49+
fromView (MkView (a ∷ pref) inf suff) = there (fromView (MkView pref inf suff))

‎src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of the heterogeneous infix relation
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.List.Relation.Binary.Infix.Heterogeneous.Properties where
10+
11+
open import Level
12+
open import Data.Bool.Base using (true; false)
13+
open import Data.Empty using (⊥-elim)
14+
open import Data.List.Base as List using (List; []; _∷_; length; map; filter; replicate)
15+
open import Data.Nat.Base using (zero; suc; _≤_; s≤s)
16+
import Data.Nat.Properties as ℕₚ
17+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
18+
open import Function.Base using (case_of_; _$′_)
19+
20+
open import Relation.Nullary using (¬_; yes; no; does)
21+
open import Relation.Nullary.Decidable using (map′)
22+
open import Relation.Nullary.Negation using (contradiction)
23+
open import Relation.Nullary.Sum using (_⊎-dec_)
24+
open import Relation.Unary as U using (Pred)
25+
open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
26+
open import Relation.Binary.PropositionalEquality using (_≢_; refl; cong)
27+
28+
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
29+
open import Data.List.Relation.Binary.Infix.Heterogeneous
30+
open import Data.List.Relation.Binary.Prefix.Heterogeneous
31+
as Prefix using (Prefix; []; _∷_)
32+
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ
33+
open import Data.List.Relation.Binary.Suffix.Heterogeneous
34+
as Suffix using (Suffix; here; there)
35+
36+
private
37+
variable
38+
a b r s : Level
39+
A : Set a
40+
B : Set b
41+
R : REL A B r
42+
S : REL A B s
43+
44+
------------------------------------------------------------------------
45+
-- Conversion functions
46+
47+
fromPointwise : ∀ {as bs} → Pointwise R as bs → Infix R as bs
48+
fromPointwise pw = here (Prefixₚ.fromPointwise pw)
49+
50+
fromSuffix : ∀ {as bs} → Suffix R as bs → Infix R as bs
51+
fromSuffix (here pw) = fromPointwise pw
52+
fromSuffix (there p) = there (fromSuffix p)
53+
54+
module _ {c t} {C : Set c} {T : REL A C t} where
55+
56+
fromPrefixSuffix : Trans R S T → Trans (Prefix R) (Suffix S) (Infix T)
57+
fromPrefixSuffix tr p (here q) = here (Prefixₚ.trans tr p (Prefixₚ.fromPointwise q))
58+
fromPrefixSuffix tr p (there q) = there (fromPrefixSuffix tr p q)
59+
60+
fromSuffixPrefix : Trans R S T → Trans (Suffix R) (Prefix S) (Infix T)
61+
fromSuffixPrefix tr (here p) q = here (Prefixₚ.trans tr (Prefixₚ.fromPointwise p) q)
62+
fromSuffixPrefix tr (there p) (_ ∷ q) = there (fromSuffixPrefix tr p q)
63+
64+
∷⁻ : ∀ {as b bs} → Infix R as (b ∷ bs) → Prefix R as (b ∷ bs) ⊎ Infix R as bs
65+
∷⁻ (here pref) = inj₁ pref
66+
∷⁻ (there inf) = inj₂ inf
67+
68+
------------------------------------------------------------------------
69+
-- length
70+
71+
length-mono : ∀ {as bs} → Infix R as bs → length as ≤ length bs
72+
length-mono (here pref) = Prefixₚ.length-mono pref
73+
length-mono (there p) = ℕₚ.≤-step (length-mono p)
74+
75+
------------------------------------------------------------------------
76+
-- As an order
77+
78+
module _ {c t} {C : Set c} {T : REL A C t} where
79+
80+
Prefix-Infix-trans : Trans R S T → Trans (Prefix R) (Infix S) (Infix T)
81+
Prefix-Infix-trans tr p (here q) = here (Prefixₚ.trans tr p q)
82+
Prefix-Infix-trans tr p (there q) = there (Prefix-Infix-trans tr p q)
83+
84+
Infix-Prefix-trans : Trans R S T → Trans (Infix R) (Prefix S) (Infix T)
85+
Infix-Prefix-trans tr (here p) q = here (Prefixₚ.trans tr p q)
86+
Infix-Prefix-trans tr (there p) (_ ∷ q) = there (Infix-Prefix-trans tr p q)
87+
88+
Suffix-Infix-trans : Trans R S T → Trans (Suffix R) (Infix S) (Infix T)
89+
Suffix-Infix-trans tr p (here q) = fromSuffixPrefix tr p q
90+
Suffix-Infix-trans tr p (there q) = there (Suffix-Infix-trans tr p q)
91+
92+
Infix-Suffix-trans : Trans R S T → Trans (Infix R) (Suffix S) (Infix T)
93+
Infix-Suffix-trans tr p (here q) = Infix-Prefix-trans tr p (Prefixₚ.fromPointwise q)
94+
Infix-Suffix-trans tr p (there q) = there (Infix-Suffix-trans tr p q)
95+
96+
trans : Trans R S T → Trans (Infix R) (Infix S) (Infix T)
97+
trans tr p (here q) = Infix-Prefix-trans tr p q
98+
trans tr p (there q) = there (trans tr p q)
99+
100+
antisym : Antisym R S T → Antisym (Infix R) (Infix S) (Pointwise T)
101+
antisym asym (here p) (here q) = Prefixₚ.antisym asym p q
102+
antisym asym {i = a ∷ as} {j = bs} p@(here _) (there q)
103+
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
104+
length as <⟨ length-mono p ⟩
105+
length bs ≤⟨ length-mono q ⟩
106+
length as ∎ where open ℕₚ.≤-Reasoning
107+
antisym asym {i = as} {j = b ∷ bs} (there p) q@(here _)
108+
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
109+
length bs <⟨ length-mono q ⟩
110+
length as ≤⟨ length-mono p ⟩
111+
length bs ∎ where open ℕₚ.≤-Reasoning
112+
antisym asym {i = a ∷ as} {j = b ∷ bs} (there p) (there q)
113+
= ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
114+
length as <⟨ length-mono p ⟩
115+
length bs <⟨ length-mono q ⟩
116+
length as ∎ where open ℕₚ.≤-Reasoning
117+
118+
------------------------------------------------------------------------
119+
-- map
120+
121+
module _ {c d r} {C : Set c} {D : Set d} {R : REL C D r} where
122+
123+
map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
124+
Infix (λ a b → R (f a) (g b)) as bs →
125+
Infix R (List.map f as) (List.map g bs)
126+
map⁺ f g (here p) = here (Prefixₚ.map⁺ f g p)
127+
map⁺ f g (there p) = there (map⁺ f g p)
128+
129+
map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
130+
Infix R (List.map f as) (List.map g bs) →
131+
Infix (λ a b → R (f a) (g b)) as bs
132+
map⁻ {bs = []} f g (here p) = here (Prefixₚ.map⁻ f g p)
133+
map⁻ {bs = b ∷ bs} f g (here p) = here (Prefixₚ.map⁻ f g p)
134+
map⁻ {bs = b ∷ bs} f g (there p) = there (map⁻ f g p)
135+
136+
------------------------------------------------------------------------
137+
-- filter
138+
139+
module _ {p q} {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q)
140+
(P⇒Q : ∀ {a b} → P a → Q b) (Q⇒P : ∀ {a b} → Q b → P a)
141+
where
142+
143+
filter⁺ : ∀ {as bs} → Infix R as bs → Infix R (filter P? as) (filter Q? bs)
144+
filter⁺ (here p) = here (Prefixₚ.filter⁺ P? Q? (λ _ → P⇒Q) (λ _ → Q⇒P) p)
145+
filter⁺ {bs = b ∷ bs} (there p) with does (Q? b)
146+
... | true = there (filter⁺ p)
147+
... | false = filter⁺ p
148+
149+
------------------------------------------------------------------------
150+
-- replicate
151+
152+
replicate⁺ : ∀ {m n a b} → m ≤ n → R a b →
153+
Infix R (replicate m a) (replicate n b)
154+
replicate⁺ m≤n r = here (Prefixₚ.replicate⁺ m≤n r)
155+
156+
replicate⁻ : ∀ {m n a b} → m ≢ 0 →
157+
Infix R (replicate m a) (replicate n b) → R a b
158+
replicate⁻ {m = m} {n = zero} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p
159+
replicate⁻ {m = m} {n = suc n} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p
160+
replicate⁻ {m = m} {n = suc n} m≢0 (there p) = replicate⁻ m≢0 p
161+
162+
------------------------------------------------------------------------
163+
-- decidability
164+
165+
infix? : Decidable R → Decidable (Infix R)
166+
infix? R? [] [] = yes (here [])
167+
infix? R? (a ∷ as) [] = no (λ where (here ()))
168+
infix? R? as bbs@(_ ∷ bs) =
169+
map′ [ here , there ]′ ∷⁻
170+
(Prefixₚ.prefix? R? as bbs ⊎-dec infix? R? as bs)

‎src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of the homogeneous infix relation
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.List.Relation.Binary.Infix.Homogeneous.Properties where
10+
11+
open import Level
12+
open import Function.Base using (_∘′_)
13+
open import Relation.Binary
14+
15+
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
16+
open import Data.List.Relation.Binary.Infix.Heterogeneous
17+
open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
18+
19+
private
20+
variable
21+
a b r s : Level
22+
A : Set a
23+
B : Set b
24+
R : REL A B r
25+
S : REL A B s
26+
27+
isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Infix S)
28+
isPreorder po = record
29+
{ isEquivalence = Pointwise.isEquivalence PO.isEquivalence
30+
; reflexive = fromPointwise ∘′ Pointwise.map PO.reflexive
31+
; trans = trans PO.trans
32+
} where module PO = IsPreorder po
33+
34+
isPartialOrder : IsPartialOrder R S → IsPartialOrder (Pointwise R) (Infix S)
35+
isPartialOrder po = record
36+
{ isPreorder = isPreorder PO.isPreorder
37+
; antisym = antisym PO.antisym
38+
} where module PO = IsPartialOrder po
39+
40+
isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Infix S)
41+
isDecPartialOrder dpo = record
42+
{ isPartialOrder = isPartialOrder DPO.isPartialOrder
43+
; _≟_ = Pointwise.decidable DPO._≟_
44+
; _≤?_ = infix? DPO._≤?_
45+
} where module DPO = IsDecPartialOrder dpo

0 commit comments

Comments
 (0)