{-# OPTIONS --universe-polymorphism #-}
module OAOAOO where
open import Function using (_∘_; id)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; false; true)
open import Data.Product using (Σ; _,_; proj₁; proj₂; _×_; map)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; _≢_)
curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
((p : Σ A B) → C p) →
((x : A) → (y : B x) → C (x , y))
curry f = λ x y → f (x , y)
false↦_true↦_ : ∀ {a} {P : Bool → Set a} → P false → P true → (b : Bool) → P b
(false↦ p true↦ q) false = p
(false↦ p true↦ q) true = q
! : ∀ {a} {A : Set a} → A → ⊤
! = λ _ → tt
data Desc (I : Set) : Set₁ where
say : (i : I) -> Desc I
σ : (S : Set) (D : S -> Desc I) -> Desc I
ask_*_ : (i : I) (D : Desc I) -> Desc I
⟦_⟧ : ∀ {I} → Desc I → (I → Set) → (I → Set)
⟦ say i' ⟧ X i = i' ≡ i
⟦ σ S D ⟧ X i = Σ S λ s → ⟦ D s ⟧ X i
⟦ ask i' * D ⟧ X i = X i' × ⟦ D ⟧ X i
data μ {I : Set} (D : Desc I) (i : I) : Set where
<_> : ⟦ D ⟧ (μ D) i → μ D i
infix 1 <_>
_⇒_ : ∀ {I} → (I → Set) → (I → Set) → Set
X ⇒ Y = ∀ {i} → X i → Y i
infixr 4 _⇒_
mutual
fold : ∀ {I X} {D : Desc I} → (⟦ D ⟧ X ⇒ X) → μ D ⇒ X
fold {D = D} phi < ds > = phi (mapFold D D phi ds)
mapFold : ∀ {I X} (D E : Desc I) → (⟦ D ⟧ X ⇒ X) → ⟦ E ⟧ (μ D) ⇒ ⟦ E ⟧ X
mapFold D (say i) phi q = q
mapFold D (σ S E) phi (s , xs) = s , mapFold D (E s) phi xs
mapFold D (ask i * E) phi (x , xs) = fold phi x , mapFold D E phi xs
fmap : ∀ {I} (D : Desc I) {X Y} → (X ⇒ Y) → ⟦ D ⟧ X ⇒ ⟦ D ⟧ Y
fmap (say i) f refl = refl
fmap (σ S D) f (s , xs) = s , fmap (D s) f xs
fmap (ask i * D) f (x , xs) = f x , fmap D f xs
mapFold-as-fmap : ∀ {I} (D E : Desc I) {X} (f : ⟦ D ⟧ X ⇒ X) {i} (xs : ⟦ E ⟧ (μ D) i) →
mapFold D E f xs ≡ fmap E (fold f) xs
mapFold-as-fmap D (say i) f refl = refl
mapFold-as-fmap D (σ S E) f (s , xs) = cong (_,_ s) (mapFold-as-fmap D (E s) f xs)
mapFold-as-fmap D (ask i * E) f (x , xs) = cong (_,_ (fold f x)) (mapFold-as-fmap D E f xs)
All : {I : Set} (E : Desc I) {D : I → Set}
(P : {i : I} → D i → Set) {i : I} → ⟦ E ⟧ D i → Set
All (say i) P x = ⊤
All (σ S E) P (s , e) = All (E s) P e
All (ask i * E) P (d , e) = P d × All E P e
mutual
induction : {I : Set} (D : Desc I) (P : {i : I} → μ D i → Set) →
({i : I} (ds : ⟦ D ⟧ (μ D) i) → All D P ds → P < ds >) →
{i : I} (x : μ D i) → P x
induction D P p < ds > = p ds (everywhereInduction D D P p ds)
everywhereInduction :
{I : Set} (D E : Desc I)
(P : {i : I} → μ D i → Set) →
({i : I} (d : ⟦ D ⟧ (μ D) i) → All D P d → P < d >) →
{i : I} (d : ⟦ E ⟧ (μ D) i) → All E P d
everywhereInduction D (say i) P p _ = tt
everywhereInduction D (σ S E) P p (s , e) = everywhereInduction D (E s) P p e
everywhereInduction D (ask i * E) P p (d , e) = induction D P p d ,
everywhereInduction D E P p e
fusion : ∀ {I} (D : Desc I) {X Y} →
(h : X ⇒ Y) (f : ⟦ D ⟧ X ⇒ X) (g : ⟦ D ⟧ Y ⇒ Y) →
(∀ {i} (xs : ⟦ D ⟧ X i) → h (f xs) ≡ g (fmap D h xs)) →
∀ {i} (x : μ D i) → h (fold f x) ≡ fold g x
fusion {I} D {X} {Y} h f g fc x =
induction D (λ y → h (fold f y) ≡ fold g y) (λ ds hs → aux D f g ds hs fc) x
where
aux : (E : Desc I) (f' : ⟦ E ⟧ X ⇒ X) (g' : ⟦ E ⟧ Y ⇒ Y) →
∀ {i} (es : ⟦ E ⟧ (μ D) i) → All E (λ y → h (fold f y) ≡ fold g y) es →
(∀ {i} (xs : ⟦ E ⟧ X i) → h (f' xs) ≡ g' (fmap E h xs)) →
h (f' (mapFold D E f es)) ≡ g' (mapFold D E g es)
aux (say i) f' g' refl hs fc = fc refl
aux (σ S E) f' g' (s , es) hs fc =
aux (E s) (curry f' s) (curry g' s) es hs (curry fc s)
aux (ask i * E) f' g' (d , es) (eq , hs) fc rewrite sym eq =
aux E (curry f' (fold f d)) (curry g' (h (fold f d))) es hs (curry fc (fold f d))
reflection : ∀ {I} {D : Desc I} {i} (x : μ D i) → fold <_> x ≡ x
reflection {I} {D} x = induction D (λ y → fold <_> y ≡ y) (λ ds hs → cong <_> (aux D ds hs)) x
where aux : ∀ (E : Desc I) {i} (es : ⟦ E ⟧ (μ D) i) →
All E (λ y → fold {X = μ D} <_> y ≡ y) es → mapFold D E <_> es ≡ es
aux (say i) refl hs = refl
aux (σ S E) (s , es) hs = cong (_,_ s) (aux (E s) es hs)
aux (ask i * E) (x , es) (eq , hs) rewrite eq = cong (_,_ x) (aux E es hs)
data _⁻¹_ {I J : Set} (e : J → I) : I → Set where
ok : (j : J) → e ⁻¹ (e j)
data Orn {I} (J : Set) (e : J → I) : Desc I → Set₁ where
say : {i : I} → e ⁻¹ i → Orn J e (say i)
σ : (S : Set) → ∀ {D} → ((s : S) → Orn J e (D s)) → Orn J e (σ S D)
ask_*_ : {i : I} → e ⁻¹ i → ∀ {D} → Orn J e D → Orn J e (ask i * D)
Δ : (S : Set) → ∀ {D} → (S → Orn J e D) → Orn J e D
⌊_⌋ : ∀ {I J e} {D : Desc I} → Orn J e D → Desc J
⌊ say (ok j) ⌋ = say j
⌊ σ S O ⌋ = σ S λ s → ⌊ O s ⌋
⌊ ask (ok j) * O ⌋ = ask j * ⌊ O ⌋
⌊ Δ S O ⌋ = σ S λ s → ⌊ O s ⌋
idOrn : ∀ {I} → (D : Desc I) → Orn I id D
idOrn (say i) = say (ok i)
idOrn (σ S D) = σ S λ s → idOrn (D s)
idOrn (ask i * D) = ask ok i * idOrn D
erase : ∀ {I J e} {D : Desc I} {X : I → Set} →
(O : Orn J e D) → ⟦ ⌊ O ⌋ ⟧ (X ∘ e) ⇒ ⟦ D ⟧ X ∘ e
erase (say (ok j)) refl = refl
erase (σ S O) (s , rs) = s , erase (O s) rs
erase (ask (ok j) * O) (r , rs) = r , erase O rs
erase (Δ S O) (s , rs) = erase (O s) rs
erase-parametric :
∀ {I J e} {D : Desc I} (O : Orn J e D) {X Y} (f : X ⇒ Y) {j} (xs : ⟦ ⌊ O ⌋ ⟧ (X ∘ e) j) →
fmap D {X} {Y} f (erase O xs) ≡ erase O (fmap ⌊ O ⌋ {X ∘ e} {Y ∘ e} f xs)
erase-parametric (say (ok j)) f refl = refl
erase-parametric (σ S O) f (s , xs) = cong (_,_ s) (erase-parametric (O s) f xs)
erase-parametric (ask (ok j) * O) f (x , xs) = cong (_,_ (f x)) (erase-parametric O f xs)
erase-parametric (Δ S O) f (s , xs) = erase-parametric (O s) f xs
ornAlg : ∀ {I J e} {D : Desc I} (O : Orn J e D) → ⟦ ⌊ O ⌋ ⟧ (μ D ∘ e) ⇒ μ D ∘ e
ornAlg O ds = < erase O ds >
forget : ∀ {I J e} {D : Desc I} (O : Orn J e D) → (μ ⌊ O ⌋) ⇒ μ D ∘ e
forget O = fold (ornAlg O)
algOrn : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) → Orn (Σ I J) proj₁ D
algOrn (say i) φ = say (ok (i , φ refl))
algOrn (σ S D) φ = σ S λ s → algOrn (D s) (curry φ s)
algOrn {J = J} (ask i * D) φ = Δ (J i) λ j → ask (ok (i , j)) * algOrn D (curry φ j)
meld : ∀{I J} (D E : Desc I) (φ : ⟦ D ⟧ J ⇒ J) (ψ : ⟦ E ⟧ J ⇒ J) {i} (z : ⟦ E ⟧ (μ D) i) →
All E (λ y' → μ ⌊ algOrn D φ ⌋ (_ , fold φ y')) z →
⟦ ⌊ algOrn E ψ ⌋ ⟧ (μ ⌊ algOrn D φ ⌋) (i , ψ (mapFold D E φ z))
meld D (say j) φ ψ refl hs = refl
meld D (σ S E) φ ψ (s , z) hs = s , meld D (E s) φ (curry ψ s) z hs
meld D (ask j * E) φ ψ (d , z) (h , hs) = fold φ d , h ,
meld D E φ (curry ψ (fold φ d)) z hs
remember : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J)
{i} (x' : μ D i) → μ ⌊ algOrn D φ ⌋ (i , fold φ x')
remember {I} {J} D φ x' =
induction D (λ y' → μ ⌊ algOrn D φ ⌋ (_ , fold φ y')) (λ ds hs → < meld D D φ φ ds hs >) x'
forget-remember-inverse : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) {i} (x' : μ D i) →
forget (algOrn D φ) (remember D φ x') ≡ x'
forget-remember-inverse {I} {J} D φ x' =
induction D (λ y' → forget (algOrn D φ) (remember D φ y') ≡ y') (λ ds hs → cong <_> (aux D φ ds hs)) x'
where
aux : (E : Desc I) (ψ : ⟦ E ⟧ J ⇒ J) {i : I} (es : ⟦ E ⟧ (μ D) i) →
All E (λ y' → forget (algOrn D φ) (remember D φ y') ≡ y') es →
erase (algOrn E ψ)
(mapFold ⌊ algOrn D φ ⌋ ⌊ algOrn E ψ ⌋ (ornAlg (algOrn D φ))
(meld D E φ ψ es (everywhereInduction D E
(λ y' → μ ⌊ algOrn D φ ⌋ (_ , fold φ y'))
(λ ds' hs' → < meld D D φ φ ds' hs' >) es))) ≡ es
aux (say i) ψ refl hs = refl
aux (σ S E) ψ (s , es) hs = cong (_,_ s) (aux (E s) (curry ψ s) es hs)
aux (ask i * E) ψ (d , es) (h , hs) rewrite h = cong (_,_ d) (aux E (curry ψ (fold φ d)) es hs)
recomputation : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) {ij} (x : μ ⌊ algOrn D φ ⌋ ij) →
fold φ (forget (algOrn D φ) x) ≡ proj₂ ij
recomputation {I} {J} D φ x =
induction ⌊ algOrn D φ ⌋ (λ {ij} x → fold φ (forget (algOrn D φ) x) ≡ proj₂ ij) (fuse D φ) x
where
fuse : (E : Desc I) (ψ : ⟦ E ⟧ J ⇒ J) →
{ij : Σ I J} (e : ⟦ ⌊ algOrn E ψ ⌋ ⟧ (μ ⌊ algOrn D φ ⌋) ij) →
All ⌊ algOrn E ψ ⌋ (λ {ij} x → fold φ (forget (algOrn D φ) x) ≡ proj₂ ij) e →
ψ (mapFold D E φ (erase (algOrn E ψ)
(mapFold ⌊ algOrn D φ ⌋ ⌊ algOrn E ψ ⌋ (ornAlg (algOrn D φ)) e))) ≡ proj₂ ij
fuse (say i) ψ refl hs = refl
fuse (σ S E) ψ (s , e) hs = fuse (E s) (curry ψ s) e hs
fuse (ask i * E) ψ (j , x , e) (h , hs) rewrite h = fuse E (curry ψ j) e hs
rpOrn : ∀ {I J e} {D : Desc I} (O : Orn J e D) → Orn (Σ J (μ D ∘ e)) proj₁ ⌊ O ⌋
rpOrn O = algOrn ⌊ O ⌋ (ornAlg O)
[_]_⊩_ : ∀ {I J e} {D : Desc I} (j : J) (x' : μ D (e j)) (O : Orn J e D) → Set
[ j ] x' ⊩ O = μ ⌊ rpOrn O ⌋ (j , x')
_⊩_ : ∀ {I J e} {D : Desc I} {j : J} (x' : μ D (e j)) (O : Orn J e D) → Set
x' ⊩ O = [ _ ] x' ⊩ O
infix 2 [_]_⊩_ _⊩_
ℜ : ∀ {I J e} {D : Desc I} (O : Orn J e D) {j} (x : μ ⌊ O ⌋ j) → forget O x ⊩ O
ℜ O = remember ⌊ O ⌋ (ornAlg O)
ℜ⁻¹ : ∀ {I J e} {D : Desc I} (O : Orn J e D) {j} →
(x' : μ D (e j)) (r : x' ⊩ O) → μ ⌊ O ⌋ j
ℜ⁻¹ O x' = forget (rpOrn O)
realiser-recovery : ∀ {I J e} {D : Desc I} (O : Orn J e D) {j} →
(x' : μ D (e j)) (r : x' ⊩ O) → forget O (ℜ⁻¹ O x' r) ≡ x'
realiser-recovery O x' r = recomputation ⌊ O ⌋ (ornAlg O) r
AOE : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) {ij} {x' : μ D (proj₁ ij)} →
[ ij ] x' ⊩ algOrn D φ → fold φ x' ≡ proj₂ ij
AOE D φ {ij} {x'} r with recomputation D φ (ℜ⁻¹ (algOrn D φ) x' r)
... | eq rewrite realiser-recovery (algOrn D φ) x' r = eq
AOE⁻¹ : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) {ij} {x' : μ D (proj₁ ij)} →
fold φ x' ≡ proj₂ ij → [ ij ] x' ⊩ algOrn D φ
AOE⁻¹ D φ {x' = x'} eq with ℜ (algOrn D φ) (remember D φ x')
... | r rewrite forget-remember-inverse D φ x' | eq = r
remember' : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J)
{i} (x' : μ D i) → μ ⌊ algOrn D φ ⌋ (i , fold φ x')
remember' D φ x' = ℜ⁻¹ (algOrn D φ) x' (AOE⁻¹ D φ refl)
recomputation' : ∀ {I J} (D : Desc I) (φ : ⟦ D ⟧ J ⇒ J) {ij} (x : μ ⌊ algOrn D φ ⌋ ij) →
fold φ (forget (algOrn D φ) x) ≡ proj₂ ij
recomputation' D φ x = AOE D φ (ℜ (algOrn D φ) x)
algOrn' : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
Orn (Σ J (K ∘ e)) (e ∘ proj₁) D
algOrn' (say (ok j)) φ = say (ok (j , φ refl))
algOrn' (σ S O) φ = σ S λ s → algOrn' (O s) (curry φ s)
algOrn' {K = K} {e} (ask (ok j) * O) φ = Δ (K (e j)) λ k →
ask (ok (j , k)) * algOrn' O (curry φ k)
algOrn' (Δ S O) φ = Δ S λ s → algOrn' (O s) φ
diffOrn-l : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
Orn (Σ J (K ∘ e)) proj₁ ⌊ O ⌋
diffOrn-l O φ = algOrn ⌊ O ⌋ (φ ∘ erase O)
iso₁-cast : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X} →
⟦ ⌊ algOrn' O φ ⌋ ⟧ X ⇒ ⟦ ⌊ diffOrn-l O φ ⌋ ⟧ X
iso₁-cast (say (ok j)) φ refl = refl
iso₁-cast (σ S O) φ (s , xs) = s , iso₁-cast (O s) (curry φ s) xs
iso₁-cast (ask (ok j) * O) φ (k , x , xs) = k , x , iso₁-cast O (curry φ k) xs
iso₁-cast (Δ S O) φ (s , xs) = s , iso₁-cast (O s) φ xs
iso₁ : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
μ ⌊ algOrn' O φ ⌋ ⇒ μ ⌊ diffOrn-l O φ ⌋
iso₁ O φ = fold (<_> ∘ iso₁-cast O φ)
iso₁-cast-parametric :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X Y}
(f : X ⇒ Y) {i} (x : ⟦ ⌊ algOrn' O φ ⌋ ⟧ X i) →
fmap ⌊ diffOrn-l O φ ⌋ f (iso₁-cast O φ x) ≡ iso₁-cast O φ (fmap ⌊ algOrn' O φ ⌋ f x)
iso₁-cast-parametric (say (ok i)) φ f refl = refl
iso₁-cast-parametric (σ S O) φ f (s , xs) =
cong (_,_ s) (iso₁-cast-parametric (O s) (curry φ s) f xs)
iso₁-cast-parametric (ask (ok i) * O) φ f (k , x , xs) =
cong (_,_ k) (cong (_,_ (f x)) (iso₁-cast-parametric O (curry φ k) f xs))
iso₁-cast-parametric (Δ S O) φ f (s , xs) =
cong (_,_ s) (iso₁-cast-parametric (O s) φ f xs)
forget-after-forget-l-1st-fusion-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (μ ⌊ diffOrn-l O φ ⌋) jk) →
forget (diffOrn-l O φ) ((<_> ∘ iso₁-cast O φ) xs)
≡ < (erase (diffOrn-l O φ) ∘ iso₁-cast O φ) (fmap ⌊ algOrn' O φ ⌋ (forget (diffOrn-l O φ)) xs) >
forget-after-forget-l-1st-fusion-condition O φ xs
rewrite mapFold-as-fmap ⌊ diffOrn-l O φ ⌋ ⌊ diffOrn-l O φ ⌋ (ornAlg (diffOrn-l O φ)) (iso₁-cast O φ xs)
| iso₁-cast-parametric O φ (forget (diffOrn-l O φ)) xs = refl
erase-after-erase-l :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{X} {jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (X ∘ e ∘ proj₁) jk) →
erase {X = X} O (erase (diffOrn-l O φ) (iso₁-cast O φ xs)) ≡ erase (algOrn' O φ) xs
erase-after-erase-l (say (ok j)) φ refl = refl
erase-after-erase-l (σ S O) φ (s , xs) = cong (_,_ s) (erase-after-erase-l (O s) (curry φ s) xs)
erase-after-erase-l (ask (ok j) * O) φ (k , x , xs) = cong (_,_ x) (erase-after-erase-l O (curry φ k) xs)
erase-after-erase-l (Δ S O) φ (s , xs) = erase-after-erase-l (O s) φ xs
forget-after-forget-l-2nd-fusion-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (μ ⌊ O ⌋ ∘ proj₁) jk) →
forget O < (erase (diffOrn-l O φ) ∘ iso₁-cast O φ) xs >
≡ < erase (algOrn' O φ) (fmap ⌊ algOrn' O φ ⌋ (forget O) xs) >
forget-after-forget-l-2nd-fusion-condition {D = D} O φ xs
rewrite mapFold-as-fmap ⌊ O ⌋ ⌊ O ⌋ (ornAlg O) (erase (diffOrn-l O φ) (iso₁-cast O φ xs))
| erase-parametric (diffOrn-l O φ) {μ ⌊ O ⌋} (forget O) (iso₁-cast O φ xs)
| iso₁-cast-parametric O φ (forget O) xs
| erase-after-erase-l O φ {μ D} (fmap ⌊ algOrn' O φ ⌋ (forget O) xs) = refl
forget-after-forget-l :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (x : μ ⌊ algOrn' O φ ⌋ jk) →
forget O (forget (diffOrn-l O φ) (iso₁ O φ x)) ≡ forget (algOrn' O φ) x
forget-after-forget-l O φ x
rewrite fusion ⌊ algOrn' O φ ⌋ (forget (diffOrn-l O φ)) (<_> ∘ iso₁-cast O φ)
(<_> ∘ erase (diffOrn-l O φ) ∘ iso₁-cast O φ) (forget-after-forget-l-1st-fusion-condition O φ) x
| fusion ⌊ algOrn' O φ ⌋ (forget O) (<_> ∘ erase (diffOrn-l O φ) ∘ iso₁-cast O φ)
(<_> ∘ erase (algOrn' O φ)) (forget-after-forget-l-2nd-fusion-condition O φ) x = refl
project-l : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} {x' : μ D (e (proj₁ jk))} → [ jk ] x' ⊩ algOrn' O φ → x' ⊩ O
project-l O φ {jk} {x'} r
with ℜ O (forget (diffOrn-l O φ) (iso₁ O φ (ℜ⁻¹ (algOrn' O φ) x' r)))
... | result rewrite forget-after-forget-l O φ (ℜ⁻¹ (algOrn' O φ) x' r)
| realiser-recovery (algOrn' O φ) x' r = result
diffOrn-r : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
Orn (Σ J (K ∘ e)) (map e id) ⌊ algOrn D φ ⌋
diffOrn-r (say (ok j)) φ = say (ok (j , φ refl))
diffOrn-r (σ S O) φ = σ S λ s → diffOrn-r (O s) (curry φ s)
diffOrn-r {K = K} {e} (ask (ok j) * O) φ =
σ (K (e j)) λ k → ask (ok (j , k)) * diffOrn-r O (curry φ k)
diffOrn-r (Δ S O) φ = Δ S λ s → diffOrn-r (O s) φ
iso₃-cast : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X} →
⟦ ⌊ algOrn' O φ ⌋ ⟧ X ⇒ ⟦ ⌊ diffOrn-r O φ ⌋ ⟧ X
iso₃-cast (say (ok j)) φ refl = refl
iso₃-cast (σ S O) φ (s , xs) = s , iso₃-cast (O s) (curry φ s) xs
iso₃-cast (ask (ok j) * O) φ (k , x , xs) = k , x , iso₃-cast O (curry φ k) xs
iso₃-cast (Δ S O) φ (s , xs) = s , iso₃-cast (O s) φ xs
iso₃ : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
μ ⌊ algOrn' O φ ⌋ ⇒ μ ⌊ diffOrn-r O φ ⌋
iso₃ O φ = fold (<_> ∘ iso₃-cast O φ)
iso₃-cast-parametric :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X Y}
(f : X ⇒ Y) {i} (x : ⟦ ⌊ algOrn' O φ ⌋ ⟧ X i) →
fmap ⌊ diffOrn-r O φ ⌋ f (iso₃-cast O φ x) ≡ iso₃-cast O φ (fmap ⌊ algOrn' O φ ⌋ f x)
iso₃-cast-parametric (say (ok i)) φ f refl = refl
iso₃-cast-parametric (σ S O) φ f (s , xs) =
cong (_,_ s) (iso₃-cast-parametric (O s) (curry φ s) f xs)
iso₃-cast-parametric (ask (ok i) * O) φ f (k , x , xs) =
cong (_,_ k) (cong (_,_ (f x)) (iso₃-cast-parametric O (curry φ k) f xs))
iso₃-cast-parametric (Δ S O) φ f (s , xs) =
cong (_,_ s) (iso₃-cast-parametric (O s) φ f xs)
forget-after-forget-r-1st-fusion-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (μ ⌊ diffOrn-r O φ ⌋) jk) →
forget (diffOrn-r O φ) ((<_> ∘ iso₃-cast O φ) xs)
≡ < (erase (diffOrn-r O φ) ∘ iso₃-cast O φ) (fmap ⌊ algOrn' O φ ⌋ (forget (diffOrn-r O φ)) xs) >
forget-after-forget-r-1st-fusion-condition O φ xs
rewrite mapFold-as-fmap ⌊ diffOrn-r O φ ⌋ ⌊ diffOrn-r O φ ⌋ (ornAlg (diffOrn-r O φ)) (iso₃-cast O φ xs)
| iso₃-cast-parametric O φ (forget (diffOrn-r O φ)) xs = refl
erase-after-erase-r :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{X} {jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (X ∘ e ∘ proj₁) jk) →
erase {X = X} (algOrn D φ) (erase (diffOrn-r O φ) (iso₃-cast O φ xs)) ≡ erase (algOrn' O φ) xs
erase-after-erase-r (say (ok j)) φ refl = refl
erase-after-erase-r (σ S O) φ (s , xs) = cong (_,_ s) (erase-after-erase-r (O s) (curry φ s) xs)
erase-after-erase-r (ask (ok j) * O) φ (k , x , xs) = cong (_,_ x) (erase-after-erase-r O (curry φ k) xs)
erase-after-erase-r (Δ S O) φ (s , xs) = erase-after-erase-r (O s) φ xs
forget-after-forget-r-2nd-fusion-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (xs : ⟦ ⌊ algOrn' O φ ⌋ ⟧ (μ ⌊ algOrn D φ ⌋ ∘ map e id) jk) →
forget (algOrn D φ) < (erase (diffOrn-r O φ) ∘ iso₃-cast O φ) xs >
≡ < erase (algOrn' O φ) (fmap ⌊ algOrn' O φ ⌋ (forget (algOrn D φ)) xs) >
forget-after-forget-r-2nd-fusion-condition {D = D} O φ xs
rewrite mapFold-as-fmap ⌊ algOrn D φ ⌋ ⌊ algOrn D φ ⌋ (ornAlg (algOrn D φ)) (erase (diffOrn-r O φ) (iso₃-cast O φ xs))
| erase-parametric (diffOrn-r O φ) {μ ⌊ algOrn D φ ⌋} (forget (algOrn D φ)) (iso₃-cast O φ xs)
| iso₃-cast-parametric O φ (forget (algOrn D φ)) xs
| erase-after-erase-r O φ {μ D} (fmap ⌊ algOrn' O φ ⌋ (forget (algOrn D φ)) xs) = refl
forget-after-forget-r :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (x : μ ⌊ algOrn' O φ ⌋ jk) →
forget (algOrn D φ) (forget (diffOrn-r O φ) (iso₃ O φ x)) ≡ forget (algOrn' O φ) x
forget-after-forget-r {D = D} O φ x
rewrite fusion ⌊ algOrn' O φ ⌋ (forget (diffOrn-r O φ)) (<_> ∘ iso₃-cast O φ)
(<_> ∘ erase (diffOrn-r O φ) ∘ iso₃-cast O φ) (forget-after-forget-r-1st-fusion-condition O φ) x
| fusion ⌊ algOrn' O φ ⌋ (forget (algOrn D φ)) (<_> ∘ erase (diffOrn-r O φ) ∘ iso₃-cast O φ)
(<_> ∘ erase (algOrn' O φ)) (forget-after-forget-r-2nd-fusion-condition O φ) x = refl
project-r : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} {x' : μ D (e (proj₁ jk))} →
[ jk ] x' ⊩ algOrn' O φ → [ map e id jk ] x' ⊩ algOrn D φ
project-r {D = D} O φ {jk} {x'} r
with ℜ (algOrn D φ) (forget (diffOrn-r O φ) (iso₃ O φ (ℜ⁻¹ (algOrn' O φ) x' r)))
... | result rewrite forget-after-forget-r O φ (ℜ⁻¹ (algOrn' O φ) x' r)
| realiser-recovery (algOrn' O φ) x' r = result
iso₂-cast : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X} →
⟦ ⌊ diffOrn-l O φ ⌋ ⟧ X ⇒ ⟦ ⌊ algOrn' O φ ⌋ ⟧ X
iso₂-cast (say (ok jk)) φ refl = refl
iso₂-cast (σ S O) φ (s , xs) = s , iso₂-cast (O s) (curry φ s) xs
iso₂-cast (ask (ok jk) * O) φ (k , x , xs) = k , x , iso₂-cast O (curry φ k) xs
iso₂-cast (Δ S O) φ (s , xs) = s , iso₂-cast (O s) φ xs
iso₂ : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) →
μ ⌊ diffOrn-l O φ ⌋ ⇒ μ ⌊ algOrn' O φ ⌋
iso₂ O φ = fold (<_> ∘ iso₂-cast O φ)
iso₁-iso₂-cast-inverse :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K) {X}
{jk} (xs : ⟦ ⌊ diffOrn-l O φ ⌋ ⟧ X jk) → iso₁-cast O φ (iso₂-cast O φ xs) ≡ xs
iso₁-iso₂-cast-inverse (say (ok j)) φ refl = refl
iso₁-iso₂-cast-inverse (σ S O) φ (s , xs) = cong (_,_ s) (iso₁-iso₂-cast-inverse (O s) (curry φ s) xs)
iso₁-iso₂-cast-inverse (ask (ok j) * O) φ (k , x , xs) = cong (_,_ k) (cong (_,_ x) (iso₁-iso₂-cast-inverse O (curry φ k) xs))
iso₁-iso₂-cast-inverse (Δ S O) φ (s , xs) = cong (_,_ s) (iso₁-iso₂-cast-inverse (O s) φ xs)
iso₁-iso₂-inverse-fusion-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (xs : ⟦ ⌊ diffOrn-l O φ ⌋ ⟧ (μ ⌊ algOrn' O φ ⌋) jk) →
iso₁ O φ < iso₂-cast O φ xs > ≡ < fmap ⌊ diffOrn-l O φ ⌋ (iso₁ O φ) xs >
iso₁-iso₂-inverse-fusion-condition O φ xs
rewrite mapFold-as-fmap ⌊ algOrn' O φ ⌋ ⌊ algOrn' O φ ⌋ {μ ⌊ diffOrn-l O φ ⌋} (<_> ∘ iso₁-cast O φ) (iso₂-cast O φ xs)
| sym (iso₁-cast-parametric O φ (iso₁ O φ) (iso₂-cast O φ xs))
| iso₁-iso₂-cast-inverse O φ xs = refl
iso₁-iso₂-inverse : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (x : μ ⌊ diffOrn-l O φ ⌋ jk) → iso₁ O φ (iso₂ O φ x) ≡ x
iso₁-iso₂-inverse O φ x =
trans (fusion ⌊ diffOrn-l O φ ⌋ (iso₁ O φ) (<_> ∘ iso₂-cast O φ) <_>
(iso₁-iso₂-inverse-fusion-condition O φ) x)
(reflection x)
forget-after-forget-l' :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} (x : μ ⌊ diffOrn-l O φ ⌋ jk) →
forget (algOrn' O φ) (iso₂ O φ x) ≡ forget O (forget (diffOrn-l O φ) x)
forget-after-forget-l' O φ x with forget-after-forget-l O φ (iso₂ O φ x)
... | eq rewrite iso₁-iso₂-inverse O φ x = sym eq
fission-condition :
∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{j} (xs : ⟦ ⌊ O ⌋ ⟧ (μ D ∘ e) j) → fold φ (ornAlg O xs) ≡ φ (erase O (fmap ⌊ O ⌋ (fold φ) xs))
fission-condition {D = D} O φ xs rewrite mapFold-as-fmap D D φ (erase O xs)
| erase-parametric O {μ D} (fold φ) xs = refl
fission : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{j} (x : μ ⌊ O ⌋ j) → fold (φ ∘ erase O) x ≡ fold φ (forget O x)
fission O φ x = sym (fusion ⌊ O ⌋ (fold φ) (ornAlg O) (φ ∘ erase O) (fission-condition O φ) x)
integrate : ∀ {I J K e} {D : Desc I} (O : Orn J e D) (φ : ⟦ D ⟧ K ⇒ K)
{jk} {x' : μ D (e (proj₁ jk))} →
x' ⊩ O → [ map e id jk ] x' ⊩ algOrn D φ → [ jk ] x' ⊩ algOrn' O φ
integrate {D = D} O φ {jk} {x'} r₁ r₂
with ℜ (algOrn' O φ) (iso₂ O φ (remember ⌊ O ⌋ (φ ∘ erase O) (ℜ⁻¹ O x' r₁)))
... | result rewrite forget-after-forget-l' O φ (remember ⌊ O ⌋ (φ ∘ erase O) (ℜ⁻¹ O x' r₁))
| forget-remember-inverse ⌊ O ⌋ (φ ∘ erase O) (ℜ⁻¹ O x' r₁)
| fission O φ (forget (rpOrn O) r₁)
| realiser-recovery O x' r₁
| AOE D φ r₂ = result
NatD : Desc ⊤
NatD = σ Bool (false↦ say tt
true↦ ask tt * say tt)
Nat : Set
Nat = μ NatD tt
zero : Nat
zero = < false , refl >
suc : Nat → Nat
suc n = < true , n , refl >
suc≢zero : ∀ {m} → suc m ≢ zero
suc≢zero ()
Fin'O : Orn Nat ! NatD
Fin'O = σ Bool (false↦ Δ Nat {say tt} (λ n → say (ok n))
true↦ Δ Nat {ask tt * say tt} (λ n → ask (ok n) * say (ok (suc n))))
_≤_ : Nat → Nat → Set
m ≤ n = μ ⌊ algOrn ⌊ Fin'O ⌋ (ornAlg Fin'O) ⌋ (n , m)
_≰_ : Nat → Nat → Set
m ≰ n = ¬ (m ≤ n)
infix 3 _≤_ _≰_
≤-base : ∀ {n} → zero ≤ n
≤-base {n} = < false , n , refl >
≤-step : ∀ {m n} → m ≤ n → suc m ≤ suc n
≤-step {m} {n} m≤n = < true , n , m , m≤n , refl >
≤-squeeze : ∀ {n} → n ≤ zero → n ≡ zero
≤-squeeze < false , ._ , refl > = refl
≤-squeeze < true , _ , _ , _ , () >
≤-step⁻¹ : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-step⁻¹ < false , n , () >
≤-step⁻¹ < true , n , m , m≤n , refl > = m≤n
≤-refl : ∀ {n} → n ≤ n
≤-refl {< false , refl >} = ≤-base
≤-refl {< true , n , refl >} = ≤-step (≤-refl {n})
≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
≤-trans < false , _ , refl > y≤z = ≤-base
≤-trans < true , _ , _ , x≤y , refl > < false , _ , () >
≤-trans < true , _ , _ , x≤y , refl > < true , _ , ._ , y≤z , refl > = ≤-step (≤-trans x≤y y≤z)
≰-invert : ∀ {x y} → x ≰ y → y ≤ x
≰-invert {x} {< false , refl >} x≰y = ≤-base
≰-invert {< false , refl >} {< true , y , refl >} x≰y with x≰y ≤-base
≰-invert {< false , refl >} {< true , y , refl >} x≰y | ()
≰-invert {< true , x , refl >} {< true , y , refl >} x≰y = ≤-step (≰-invert (x≰y ∘ ≤-step))
_⊓_ : Nat → Nat → Nat
< false , refl > ⊓ n = zero
< true , m , refl > ⊓ < false , refl > = zero
< true , m , refl > ⊓ < true , n , refl > = suc (m ⊓ n)
infixl 5 _⊓_
⊓-universal-⇒ : ∀ z x y → z ≤ x ⊓ y → z ≤ x × z ≤ y
⊓-universal-⇒ < false , refl > x y le = ≤-base , ≤-base
⊓-universal-⇒ < true , z , refl > < false , refl > y < false , _ , () >
⊓-universal-⇒ < true , z , refl > < false , refl > y < true , _ , _ , _ , () >
⊓-universal-⇒ < true , z , refl > < true , x , refl > < false , refl > < false , _ , () >
⊓-universal-⇒ < true , z , refl > < true , x , refl > < false , refl > < true , _ , _ , _ , () >
⊓-universal-⇒ < true , z , refl > < true , x , refl > < true , y , refl > < false , _ , () >
⊓-universal-⇒ < true , z , refl > < true , x , refl > < true , y , refl > < true , ._ , ._ , le , refl > = map ≤-step ≤-step (⊓-universal-⇒ z x y le)
⊓-universal-⇐ : ∀ {z x y} → z ≤ x → z ≤ y → z ≤ x ⊓ y
⊓-universal-⇐ < false , ._ , refl > z≤y = ≤-base
⊓-universal-⇐ < true , _ , _ , z≤x , refl > < false , _ , () >
⊓-universal-⇐ < true , _ , _ , z≤x , refl > < true , _ , ._ , z≤y , refl > = ≤-step (⊓-universal-⇐ z≤x z≤y)
ListO : Set → Orn ⊤ id NatD
ListO A = σ Bool (false↦ say (ok tt)
true↦ Δ A (λ x → ask (ok tt) * say (ok tt)))
List : Set → Set
List A = μ ⌊ ListO A ⌋ tt
[] : ∀ {A} → List A
[] = < false , refl >
_∷_ : ∀ {A} → A → List A → List A
x ∷ xs = < true , x , xs , refl >
infixr 5 _∷_
length : ∀ {A} → List A → Nat
length = forget (ListO _)
SListO : Orn Nat ! ⌊ ListO Nat ⌋
SListO = σ Bool (false↦ Δ Nat {say tt} (λ n → say (ok n))
true↦ σ Nat (λ x → Δ Nat (λ b →
Δ (b ≤ x) {ask tt * say tt} (λ _ →
ask (ok x) * say (ok b)))))
SList : Nat → Set
SList = μ ⌊ SListO ⌋
snil : ∀ {b} → SList b
snil {b} = < false , b , refl >
scons : (x : Nat) → ∀ {b} → b ≤ x → SList x → SList b
scons x {b} b≤x xs = < true , x , b , b≤x , xs , refl >
VecO : (A : Set) → Orn (⊤ × Nat) proj₁ ⌊ ListO A ⌋
VecO A = rpOrn (ListO A)
Vec : Set → Nat → Set
Vec A n = μ ⌊ VecO A ⌋ (tt , n)
vnil : ∀ {A} → Vec A zero
vnil = < false , refl >
vcons : ∀ {A} → A → ∀ {n} → Vec A n → Vec A (suc n)
vcons x {n} xs = < true , x , n , xs , refl >
_+_ : Nat → Nat → Nat
< false , refl > + n = n
< true , m , refl > + n = suc (m + n)
_++_ : ∀ {A} → List A → List A → List A
< false , refl > ++ ys = ys
< true , x , xs , refl > ++ ys = x ∷ (xs ++ ys)
length-hom : ∀ {A} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-hom < false , refl > ys = refl
length-hom < true , x , xs , refl > ys = cong suc (length-hom xs ys)
append-length : ∀ {A} (xs ys : List A) {m n} →
length xs ≡ m → length ys ≡ n → length (xs ++ ys) ≡ m + n
append-length xs ys refl refl = length-hom xs ys
vecToList : ∀ {A} → ∀ {n} → Vec A n → List A
vecToList = forget (rpOrn (ListO _))
vappend : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
vappend {A} xs ys = ℜ⁻¹ (VecO A) (xs' ++ ys')
(AOE⁻¹ ⌊ ListO A ⌋ φ (append-length xs' ys' eq₁ eq₂))
where
xs' = forget (VecO A) xs
ys' = forget (VecO A) ys
φ = ornAlg (ListO A)
eq₁ = AOE ⌊ ListO A ⌋ φ (ℜ (VecO A) xs)
eq₂ = AOE ⌊ ListO A ⌋ φ (ℜ (VecO A) ys)
SVecO : Orn (Nat × Nat) ! ⌊ ListO Nat ⌋
SVecO = algOrn' SListO (ornAlg (ListO Nat))
SVec : Nat → Nat → Set
SVec b n = μ ⌊ SVecO ⌋ (b , n)
svnil : ∀ {b} → SVec b zero
svnil {b} = < false , b , refl >
svcons : (x : Nat) → ∀ {b} → b ≤ x → ∀ {n} → SVec x n → SVec b (suc n)
svcons x {b} b≤x {n} xs = < true , x , b , b≤x , n , xs , refl >
_≤?_ : (m n : Nat) → Dec (m ≤ n)
< false , refl > ≤? n = yes ≤-base
< true , m , refl > ≤? < false , refl > = no (suc≢zero ∘ ≤-squeeze)
< true , m , refl > ≤? < true , n , refl > with m ≤? n
... | yes m≤n = yes (≤-step m≤n)
... | no m≰n = no (m≰n ∘ ≤-step⁻¹)
insert : Nat → List Nat → List Nat
insert y < false , refl > = y ∷ []
insert y < true , x , xs , refl > with y ≤? x
... | yes _ = y ∷ x ∷ xs
... | no _ = x ∷ insert y xs
insert-length : ∀ y xs {n} → length xs ≡ n → length (insert y xs) ≡ suc n
insert-length y < false , refl > refl = refl
insert-length y < true , x , xs , refl > refl
with y ≤? x
... | yes _ = refl
... | no _ = cong suc (insert-length y xs refl)
vinsert : Nat → ∀ {n} → Vec Nat n → Vec Nat (suc n)
vinsert y {n} xs = ℜ⁻¹ (VecO Nat) (insert y xs')
(AOE⁻¹ ⌊ ListO Nat ⌋ (ornAlg (ListO Nat))
(insert-length y xs' (AOE ⌊ ListO Nat ⌋ (ornAlg (ListO Nat)) r)))
where xs' = forget (VecO Nat) xs
r = ℜ (VecO Nat) xs
Sorted : Nat → List Nat → Set
Sorted b xs = [ b ] xs ⊩ SListO
sorted-nil : ∀ {b} → Sorted b []
sorted-nil {b} = < false , b , refl >
sorted-cons : ∀ x → ∀ {b} → b ≤ x → ∀ {xs} → Sorted x xs → Sorted b (x ∷ xs)
sorted-cons x {b} b≤x {xs} s = < true , x , b , b≤x , xs , s , refl >
sorted-relax : ∀ {b b' xs} → b' ≤ b → Sorted b xs → Sorted b' xs
sorted-relax b'≤b < false , _ , refl > = sorted-nil
sorted-relax b'≤b < true , x , _ , b≤x , _ , s , refl > = sorted-cons x (≤-trans b'≤b b≤x) s
insert-sorted : ∀ y xs {b} → Sorted b xs → Sorted (b ⊓ y) (insert y xs)
insert-sorted y ._ < false , b , refl > = sorted-cons y (proj₂ (⊓-universal-⇒ (b ⊓ y) b y ≤-refl)) sorted-nil
insert-sorted y ._ < true , x , b , b≤x , xs , s , refl >
with y ≤? x
... | yes y≤x = sorted-cons y (proj₂ (⊓-universal-⇒ (b ⊓ y) b y ≤-refl)) (sorted-cons x y≤x s)
... | no y≰x = sorted-cons x (≤-trans (proj₁ (⊓-universal-⇒ (b ⊓ y) b y ≤-refl)) b≤x)
(sorted-relax (⊓-universal-⇐ ≤-refl (≰-invert y≰x)) (insert-sorted y xs s))
sinsert : (y : Nat) → ∀ {b} → SList b → SList (b ⊓ y)
sinsert y xs = let xs' = forget SListO xs
in ℜ⁻¹ SListO (insert y xs') (insert-sorted y xs' (ℜ SListO xs))
svinsert : (y : Nat) → ∀ {b n} → SVec b n → SVec (b ⊓ y) (suc n)
svinsert y {b} {n} xs = ℜ⁻¹ SVecO (insert y xs')
(integrate SListO φ
(insert-sorted y xs' r₁)
(AOE⁻¹ ⌊ ListO Nat ⌋ φ (insert-length y xs' (AOE ⌊ ListO Nat ⌋ φ r₂))))
where xs' = forget SVecO xs
φ = ornAlg (ListO Nat)
r = ℜ SVecO xs
r₁ = project-l SListO φ r
r₂ = project-r SListO φ r
isort : (xs : List Nat) → SVec zero (length xs)
isort < false , refl > = svnil
isort < true , x , xs , refl > = svinsert x (isort xs)