{-
  An implementation of the (typed) SKI-calculus.

  References:
  [0] Lectures on the Curry-Howard-Isomorphism -- Sørensen, Urzyczyin
  [1] To Mock a Mockingbird -- Smullyan
-}

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Nullary.Decidable using (yes ; no)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary using (¬_)

{-
  The implementation is parametric over a set 𝓥 of variables (on which propositional equality is decidable)
-}
module ski (𝓥 : Set) (_≈_ : DecidableEquality 𝓥) where

-- Syntax of terms as an inductive type
infixl 5 _∙_
data CL : Set where
  `_  : 𝓥 → CL
  K   : CL
  S   : CL
  _∙_ : CL → CL → CL

-- one-step reduction relation
infix 4 _⟶_
data _⟶_ : CL → CL → Set where
  k : ∀ {F G : CL} →
      K ∙ F ∙ G ⟶ F

  s : ∀ {F G H : CL} →
    S ∙ F ∙ G ∙ H ⟶ F ∙ H ∙ (G ∙ H)

  appₗ : ∀ {F F' G : CL} →
    F ⟶ F' →
    ----------------
    F ∙ G ⟶ F' ∙ G

  appᵣ : ∀ {F G G' : CL} →
    G ⟶ G' →
    -------------
    F ∙ G ⟶ F ∙ G'

module mstep where
  infix 4 _↠_
  -- reflexive transitive closure of _⟶_
  infix  3 _∎
  infixr 2 _⟶⟨_⟩_
  data _↠_ : CL → CL → Set where
    _∎ : ∀ (F : CL) →
      F ↠ F
    cons : ∀ {F G H : CL} →
      F ⟶ G →
      G ↠ H →
      F ↠ H

  {-
    The following definitions are some syntax sugar for proofs on the step relation
  -}
  -- one step
  pattern _⟶⟨_⟩_ F F⟶G G↠H = cons {F} F⟶G G↠H

  infix 1 begin_
  begin_ : ∀ {F G : CL} →
    F ↠ G →
    F ↠ G
  begin step = step

  -- injection of a singular step into the multi-step relation
  once : ∀ {F G : CL} →
    F ⟶ G →
    F ↠ G
  once {G = G} step = cons step (G ∎)

  -- multi step
  infixr 2 _↠⟨_⟩_
  _↠⟨_⟩_ : ∀ (F : CL) {G H : CL} →
    F ↠ G →
    G ↠ H →
    F ↠ H
  _↠⟨_⟩_ F (_ ∎) step' = step'
  _↠⟨_⟩_ F (cons {G = G} x step) step' = cons x (_↠⟨_⟩_ G step step')


  -- left and right congruence of the multi-step relation
  mappₗ : ∀ {F G H : CL} →
    F ↠ H →
    (F ∙ G) ↠ (H ∙ G)
  mappₗ {F} {G} (_ ∎) = F ∙ G ∎
  mappₗ (cons F⟶H' G↠H) = cons (appₗ F⟶H') (mappₗ G↠H)

  mappᵣ : ∀ {F G H : CL} →
    G ↠ H →
    (F ∙ G) ↠ (F ∙ H)
  mappᵣ {F} {_} {H} (_ ∎) = F ∙ H ∎
  mappᵣ (cons G⟶H' H'↠H) = cons (appᵣ G⟶H') (mappᵣ H'↠H)

open mstep

{-
  Let's define some of the combinator birds from [1]:
-}
module birds where
  -- Identity (Idiot) bird
  I : CL
  I = S ∙ K ∙ K

  I-step : ∀ {F : CL} → I ∙ F ↠ F
  I-step {F} = begin
    I ∙ F
      ⟶⟨ s ⟩
    K ∙ F ∙ (K ∙ F)
      ⟶⟨ k ⟩
    F ∎

  -- Bluebird
  B : CL
  B = S ∙ (K ∙ S) ∙ K

  B-step : ∀ {F G X : CL} → B ∙ F ∙ G ∙ X ↠ F ∙ (G ∙ X)
  B-step {F} {G} {X} = begin
    B ∙ F ∙ G ∙ X
      ⟶⟨ appₗ (appₗ s) ⟩
    K ∙ S ∙ F ∙ (K ∙ F) ∙ G ∙ X
      ⟶⟨ appₗ (appₗ (appₗ k)) ⟩
    S ∙ (K ∙ F) ∙ G ∙ X
      ⟶⟨ s ⟩
    K ∙ F ∙ X ∙ (G ∙ X)
      ⟶⟨ appₗ k ⟩
    F ∙ (G ∙ X) ∎

  -- Warbler
  W : CL
  W = S ∙ S ∙ (K ∙ I)

  W-step : ∀ {F G : CL} → W ∙ F ∙ G ↠ F ∙ G ∙ G
  W-step {F} {G} = begin
    W ∙ F ∙ G
      ⟶⟨ appₗ s ⟩
    S ∙ F ∙ (K ∙ I ∙ F) ∙ G
      ⟶⟨ s ⟩
    F ∙ G ∙ (K ∙ I ∙ F ∙ G)
      ⟶⟨ appᵣ (appₗ k) ⟩
    F ∙ G ∙ (I ∙ G)
      ↠⟨ mappᵣ I-step ⟩
    F ∙ G ∙ G ∎

  -- Cardinal
  C : CL
  C = S ∙ (B ∙ B ∙ S) ∙ (K ∙ K)

  C-step : ∀ {F G H : CL} → C ∙ F ∙ G ∙ H ↠ F ∙ H ∙ G
  C-step {F} {G} {H} = begin
    C ∙ F ∙ G ∙ H
      ⟶⟨ appₗ (appₗ s) ⟩
    B ∙ B ∙ S ∙ F ∙ (K ∙ K ∙ F) ∙ G ∙ H
      ↠⟨ mappₗ (mappₗ (mappₗ B-step)) ⟩
    B ∙ (S ∙ F) ∙ (K ∙ K ∙ F) ∙ G ∙ H
      ↠⟨ mappₗ B-step ⟩
    S ∙ F ∙ (K ∙ K ∙ F ∙ G) ∙ H
      ⟶⟨ s ⟩
    F ∙ H ∙ (K ∙ K ∙ F ∙ G ∙ H)
      ⟶⟨ appᵣ (appₗ (appₗ k)) ⟩
    F ∙ H ∙ (K ∙ G ∙ H)
      ⟶⟨ appᵣ k ⟩
    F ∙ H ∙ G ∎

  -- Mockingbird
  M : CL
  M = S ∙ I ∙ I

  M-step : ∀ {F : CL} → M ∙ F ↠ F ∙ F
  M-step {F} = begin
    M ∙ F
      ⟶⟨ s ⟩
    I ∙ F ∙ (I ∙ F)
      ↠⟨ mappₗ I-step ⟩
    F ∙ (I ∙ F)
      ↠⟨ mappᵣ I-step ⟩
    F ∙ F ∎

  -- Applying the mockingbird to itself yields a term that reduces to itself
  loop : M ∙ M ↠ M ∙ M
  loop = M-step

open birds

{-
  Relating the SKI-calculus to the λ-calculus. Taken from chapter 5.4 in [0]
-}
module combinatory-abstraction where

  -- Substituting a variable for a term
  _[_/_] : CL → CL → 𝓥 → CL
  (` y) [ B / x ] with x ≈ y
  ... | yes p = B
  ... | no ¬p = ` y
  K [ B / x ] = K
  S [ B / x ] = S
  (A ∙ C) [ B / x ] = (A [ B / x ]) ∙ (C [ B / x ])

  -- combinary abstraction
  ƛ⋆_↦_ : 𝓥 → CL → CL
  ƛ⋆ v ↦ (` x) with v ≈ x
  ... | yes _ = I
  ... | no _ = K ∙ (` x)
  ƛ⋆ v ↦ K = K ∙ K
  ƛ⋆ v ↦ S = K ∙ S
  ƛ⋆ v ↦ (B ∙ C) = S ∙ (ƛ⋆ v ↦ B) ∙ (ƛ⋆ v ↦ C)

  -- combinary abstraction is beta reductive
  beta : ∀ {x : 𝓥} {B : CL} → (A : CL) → (ƛ⋆ x ↦ A) ∙ B ↠ A [ B / x ]
  beta {x} (` y) with x ≈ y
  ... | yes p = I-step
  ... | no ¬p = once k
  beta K = once k
  beta S = once k
  beta {x} {G} (B ∙ C) = begin
    (ƛ⋆ x ↦ (B ∙ C)) ∙ G
      ⟶⟨ s ⟩
    (ƛ⋆ x ↦ B) ∙ G ∙ ((ƛ⋆ x ↦ C) ∙ G)
      ↠⟨ mappₗ (beta B) ⟩
    (B [ G / x ]) ∙ ((ƛ⋆ x ↦ C) ∙ G)
      ↠⟨ mappᵣ (beta C) ⟩
    ((B ∙ C) [ G / x ]) ∎

  infix 5 _∈_
  data _∈_ : 𝓥 → CL → Set where
    in-here : ∀ {x : 𝓥} →
      x ∈ ` x

    in-left : ∀ {x : 𝓥} {F G : CL} →
      x ∈ F →
      x ∈ (F ∙ G)

    in-right : ∀ {x : 𝓥} {F G : CL} →
      x ∈ G →
      x ∈ (F ∙ G)

  open import Data.Empty
  
  no-intro : ∀ {x : 𝓥} (F : CL) →
    ¬ (x ∈ F) →
    ∀ (v : 𝓥) → ¬ (x ∈ (ƛ⋆ v ↦ F))
  no-intro {x} (` y) x∉F v x∈λ⋆F with v ≈ y
  ... | yes p with x∈λ⋆F
  no-intro {x} (` y) x∉F v x∈λ⋆F | yes p | in-left (in-left ())
  no-intro {x} (` y) x∉F v x∈λ⋆F | yes p | in-left (in-right ())
  no-intro {x} (` y) x∉F v x∈λ⋆F | no ¬p with x∈λ⋆F
  no-intro {x} (` y) x∉F v x∈λ⋆F | no ¬p | in-right p = ⊥-elim (x∉F p)
  no-intro K x∉F v (in-left x∈λ⋆F) = x∉F x∈λ⋆F
  no-intro K x∉F v (in-right x∈λ⋆F) = x∉F x∈λ⋆F
  no-intro S x∉F v (in-left ())
  no-intro S x∉F v (in-right x∈λ⋆F) = x∉F x∈λ⋆F
  no-intro (F ∙ G) x∉F v (in-left (in-right x∈λ⋆F)) = no-intro F (λ z → x∉F (in-left z)) v x∈λ⋆F
  no-intro (F ∙ G) x∉F v (in-right x∈λ⋆F) = no-intro G (λ z → x∉F (in-right z)) v x∈λ⋆F

  module cl-lambda (x y z : 𝓥) (x≢y : x ≢ y) (x≢z : x ≢ z) (y≢z : y ≢ z) where

    open import lambda 𝓥 _≈_ renaming (mappₗ to lmappₗ ; mappᵣ to lmappᵣ)

    ⟨_⟩Λ : CL → Λ
    ⟨ ` v ⟩Λ = ` v
    ⟨ K ⟩Λ = ƛ x  ↦ ƛ y ↦ ` x
    ⟨ S ⟩Λ = ƛ x ↦ ƛ y ↦ ƛ z ↦ (` x ∙ ` z) ∙ (` y ∙ ` z)
    ⟨ F ∙ G ⟩Λ = ⟨ F ⟩Λ ∙ ⟨ G ⟩Λ

    ⟨_⟩CL : Λ → CL
    ⟨ ` v ⟩CL = ` v
    ⟨ m ∙ n ⟩CL = ⟨ m ⟩CL ∙ ⟨ n ⟩CL
    ⟨ ƛ v ↦ m ⟩CL = ƛ⋆ v ↦ ⟨ m ⟩CL

    lemma : ∀ (t : Λ) → ⟨ ⟨ t ⟩CL ⟩Λ ↠β t
    lemma (` x) = ` x ∎
    lemma (t ∙ h) = βegin _ ↠β⟨ lmappₗ (lemma t) ⟩ _ ↠β⟨ lmappᵣ (lemma h) ⟩ _ ∎
    lemma (ƛ x ↦ t) = {!!}

    foo : ⟨ ƛ y ↦ ` y ∙ ` y ⟩CL ≡ S ∙ I ∙ I
    foo with y ≈ y
    ... | yes _ = refl
    ... | no ¬p = ⊥-elim (¬p refl)

    _ : ⟨ S ∙ I ∙ I ⟩Λ ≢ (ƛ y ↦ ` y ∙ ` y)
    _ = λ ()

    _ : ⟨ ⟨ S ∙ K ∙ K ⟩Λ ⟩CL ≢ S ∙ K ∙ K
    _ = λ ()
    
    -- lemma : ∀ {F G : CL} →
    --   F ⟶ G →
    --   ⟨ F ⟩Λ ↠β ⟨ G ⟩Λ
    -- lemma {F} {G} (k {G = H}) = βegin
    --   ⟨ K ∙ G ∙ H ⟩Λ ↠β⟨ lmappₗ (β-once (β {!!})) ⟩
    --   {!!} ↠β⟨ {!!} ⟩
    --   ⟨ G ⟩Λ ∎
    -- lemma s = {!!}
    -- lemma (appₗ x) = {!!}
    -- lemma (appᵣ x) = {!!}

module typing where
  open import Data.List
  open import Data.List.Membership.Propositional using (_∈_)
  open import Data.List.Relation.Unary.Any using (here ; there)

  infixr 5 _⇒_
  data type : Set where
    ⋆ : type
    _⇒_ : type → type → type

  context : Set
  context = List (𝓥 × type)

  _∈ₐ_ : 𝓥 → context → Set
  v ∈ₐ Γ = v ∈ (Data.List.map proj₁ Γ)

  _!!_ : {v : 𝓥} → (Γ : context) → (v ∈ₐ Γ) → type
  [] !! ()
  (x ∷ Γ) !! here px = proj₂ x
  (x ∷ Γ) !! there p = Γ !! p

  infix 3 _⊢_∶_
  data _⊢_∶_ : context → CL → type → Set where
    ctx : ∀ {v : 𝓥} {Γ : context} →
      (p : v ∈ₐ Γ) →
      --------------------
      Γ ⊢ ` v ∶ (Γ !! p)

    k : ∀ {Γ : context} {σ τ : type} →
      --------------------
      Γ ⊢ K ∶ σ ⇒ τ ⇒ σ

    s : ∀ {Γ : context} {σ τ ρ : type} →
      --------------------
      Γ ⊢ S ∶ (σ ⇒ τ ⇒ ρ) ⇒ (σ ⇒ τ) ⇒ σ ⇒ ρ

    app : ∀ {Γ : context} {M N : CL} {σ τ : type} →
      Γ ⊢ M ∶ σ ⇒ τ →
      Γ ⊢ N ∶ σ →
      --------------------
      Γ ⊢ M ∙ N ∶ τ

  I-types : ∀ {σ : type} → [] ⊢ I ∶ σ ⇒ σ
  I-types = app (app s k) (k {τ = ⋆})

  B-types : ∀ {σ τ ρ : type} → [] ⊢ B ∶ (τ ⇒ ρ) ⇒ (σ ⇒ τ) ⇒ (σ ⇒ ρ)
  B-types = app (app s (app k s)) k

  W-types : ∀ {σ τ : type} → [] ⊢ W ∶ (σ ⇒ σ ⇒ τ) ⇒ σ ⇒ τ
  W-types = app (app s s) (app k I-types)

  C-types : ∀ {σ τ ρ : type} → [] ⊢ C ∶ (σ ⇒ τ ⇒ ρ) ⇒ τ ⇒ σ ⇒ ρ
  C-types = app (app s (app (app B-types B-types) s)) (app k k)

  M-does-not-type : ∀ {σ : type} → ¬ ([] ⊢ M ∶ σ)
  M-does-not-type (app (app s (app (app s k) k)) (app (app s ()) k))