module infiniteSK where
open import Coinduction
open import Relation.Binary.PropositionalEquality

infixl 5 _$_

-- coinductive terms
data CL : Set where
  S : CL
  K : CL
  _$_ : ∞ CL → ∞ CL → CL

-- inductive prefixes
data CL' : Set where
  inj : CL → CL'
  S K : CL'
  _$_ : CL' → CL' → CL'

data Match : CL' → CL → Set where
  S : Match S S
  K : Match K K
  _$_ : ∀ {y y' l r} →
        Match y (♭ l) → Match y' (♭ r) → Match (y $ y') (l $ r)
  inj : ∀ {x y} → x ≡ y → Match (inj x) y

build : CL' → CL
build (inj y) = y
build S = S
build K = K
build (y $ y') = ♯ build y $ ♯ build y'

Match-build : ∀ x → Match x (build x)
Match-build (inj y) = inj refl
Match-build S = S
Match-build K = K
Match-build (y $ y') = Match-build y $ Match-build y'

-- an example
I : CL
I = ♯ (♯ S $ ♯ K) $ ♯ K

I' : CL'
I' = S $ K $ K

mutual
  _⟶_ : CL' → CL' → Set
  x ⟶ y = {l r : CL} → Match x l → Match y r → l ⇒ r

  data _⇒_ : CL → CL → Set where
    K⇒ : ∀ x y → (K $ x $ y) ⟶ x
    S⇒ : ∀ x y z → (S $ x $ y $ z) ⟶ ((x $ z) $ (y $ z))
    trans⇒ : ∀ {t} t' {t''} → t ⇒ t' → t' ⇒ t'' → t ⇒ t''
    left⇒ : ∀ l1 l2 r → l1 ⟶ l2 → (l1 $ r) ⟶ (l2 $ r)

iid' : ∀ x → (I' $ x) ⟶ x
iid' x pl pr
  = trans⇒ (build (K $ x $ (K $ x)))
      (S⇒ K K x
          pl
          ((K $ Match-build x) $ (K $ Match-build x)))
      (K⇒ x (K $ x)
          ((K $ Match-build x) $ (K $ Match-build x))
          pr)

SIω : CL
SIω = ♯ (♯ S $ ♯ I) $ ♯ SIω

fixd' : ∀ x → (inj SIω $ x) ⟶ (x $ (inj SIω $ x))
fixd' x (inj ?≡♭l $ px) pr =
  trans⇒ (build (I' $ x $ (inj SIω $ x)))
    (S⇒ I' (inj SIω) x
        (subst (Match _) ?≡♭l (S $ (S $ K $ K) $ inj refl) $ px)
        (S $ K $ K $ Match-build x $ (inj refl $ Match-build x)))
    (left⇒ (I' $ x) x (inj SIω $ x) (iid' x)
        (S $ K $ K $ Match-build x $ (inj refl $ Match-build x))
        pr)