-- An encoding of focused intuitionistic logic, simultaneously an intrinsic encoding
-- of focused lambda calculus

open import Data.List
open import Data.String renaming (_++_ to concat) 

module Main where

  module Types where
    Atom : Set 
    Atom = String

    mutual
      data Pos : Set where
        X⁺  : Atom -> Pos
        ↓   : Neg -> Pos
        1⁺  : Pos
        _*_ : Pos -> Pos -> Pos
        0⁺  : Pos
        _+_ : Pos -> Pos -> Pos
        2⁺ : Pos
        ℕ  : Pos

      data Neg : Set where
        X⁻ : Atom -> Neg
        ↑ : Pos -> Neg
        ⊤ : Neg
        _→_ : Pos -> Neg -> Neg
        _&_ : Neg -> Neg -> Neg

      infixr 14 _→_
      infixr 15 _&_
      infixr 15 _+_
      infixr 16 _*_

  module Contexts where
    open Types public

    data Hyp : Set where
      HP : Atom -> Hyp
      HN : Neg -> Hyp

    data Conc : Set where
      CP : Pos -> Conc
      CN : Atom -> Conc

    LCtx : Set
    LCtx = List Hyp

    UCtx : Set
    UCtx = List LCtx

    data _∈_ : Hyp -> LCtx -> Set where
      f0 : {h : Hyp}   {Δ : LCtx} -> h ∈ (h :: Δ )
      fS : {h h' : Hyp} {Δ : LCtx} -> h' ∈ Δ -> h' ∈ (h :: Δ)

    data _∈∈_ : Hyp -> UCtx -> Set where
      s0 : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈ Δ -> h ∈∈ (Δ :: Γ)
      sS : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈∈ Γ -> h ∈∈ (Δ :: Γ)

  module Patterns where
    open Contexts public
   
    [_] : {A : Set} -> A -> List A
    [_] x  = x :: []

    -- Pat⁺ Δ A⁺ = linear entailment "Δ ⇒ A⁺"
    data Pat⁺ : LCtx -> Pos -> Set where
      Px  : {x : Atom} -> Pat⁺ [ HP x ] (X⁺ x)
      Pu  : {A⁻ : Neg} -> Pat⁺ [ HN A⁻ ] (↓ A⁻)
      P<> : Pat⁺ [] 1⁺
      Ppair : {Δ1 : LCtx} { Δ2 : LCtx } {A : Pos} {B : Pos}
                -> Pat⁺ Δ1 A -> Pat⁺ Δ2 B -> Pat⁺ (Δ1 ++ Δ2) (A * B)
                
      Pinl : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ A -> Pat⁺ Δ (A + B)
      Pinr : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ B -> Pat⁺ Δ (A + B)
      Ptt  : Pat⁺ [] 2⁺
      Pff  : Pat⁺ [] 2⁺
      Pz   : Pat⁺ [] ℕ
      Ps   : {Δ : LCtx } -> Pat⁺ Δ ℕ -> Pat⁺ Δ ℕ

    -- Pat⁻ Δ A⁻ c = linear entailment "Δ ; A⁻ ⇒ c"
    data Pat⁻ : LCtx -> Neg -> Conc -> Set where
      Dx  : forall {x} -> Pat⁻ [] (X⁻ x) (CN x)
      Dp  : forall {A⁺} -> Pat⁻ [] (↑ A⁺) (CP A⁺)
      Dapp : {Δ1 : LCtx } {Δ2 : LCtx} {A⁺ : Pos} {B⁻ : Neg} {c : Conc}
               -> Pat⁺ Δ1 A⁺ -> Pat⁻ Δ2 B⁻ c -> Pat⁻ (Δ2 ++ Δ1) (A⁺ → B⁻) c
      Dfst   : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc}
                -> Pat⁻ Δ A⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c
      Dsnd   : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc}
                -> Pat⁻ Δ B⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c

  module Logic where
    open Patterns public

    mutual
       -- RFoc Γ A⁺ = right-focus "Γ ⊢ [A⁺]"
       data RFoc : UCtx -> Pos -> Set where
         Val : forall {Γ A⁺ Δ} -> Pat⁺ Δ A⁺ -> SatCtx Γ Δ -> RFoc Γ A⁺ 

       -- LInv Γ c₀ c = left-inversion "Γ ; c₀ ⊢ c"
       data LInv : UCtx -> Conc -> Conc -> Set where
         Id- : forall {Γ X⁻ } -> LInv Γ (CN X⁻) (CN X⁻)
         Fn   : forall {Γ A⁺ c}
                 -> ({Δ : LCtx} -> Pat⁺ Δ A⁺ -> UnFoc (Δ :: Γ) c)
                 -> LInv Γ (CP A⁺) c

       -- RInv Γ h = right-inversion "Γ ⊢ h;"
       data RInv : UCtx -> Hyp -> Set where
         Susp : forall {Γ A⁻ }
                -> ({Δ : LCtx} {c : Conc} -> Pat⁻ Δ A⁻ c -> UnFoc (Δ :: Γ) c)
                -> RInv Γ (HN A⁻)
         Id+ : forall {Γ X⁺ } -> ((HP X⁺) ∈∈ Γ) -> RInv Γ (HP X⁺)
    
       -- LFoc Γ A⁻ c = left-focus "Γ ; [A⁻] ⊢ c"
       data LFoc : UCtx -> Neg -> Conc -> Set where
         Spine : forall {Δ A⁻ c0 c Γ} -> Pat⁻ Δ A⁻ c0  ->  SatCtx Γ Δ  ->  LInv Γ c0 c
                 -> LFoc Γ A⁻ c

       -- UnFoc Γ c = unfocused "Γ ⊢ c"
       data UnFoc : UCtx -> Conc -> Set where
         Ret : forall {Γ A⁺ } -> RFoc Γ A⁺ -> UnFoc Γ (CP A⁺)
         App : forall {Γ A⁻ c} -> ((HN A⁻) ∈∈ Γ) -> LFoc Γ A⁻ c -> UnFoc Γ c

       -- SatCtx Γ Δ = conjoined inversion "Γ ⊢ Δ;"
       data SatCtx : UCtx -> LCtx -> Set where
         Sub : forall {Γ Δ} ->
               ({h : Hyp} -> (h ∈ Δ) -> (RInv Γ h))
               -> SatCtx Γ Δ

  module Examples where
    open Logic
    NilCtx : {Γ : UCtx} -> SatCtx Γ []
    NilCtx = Sub f
     where f : forall {h} -> h ∈ [] -> RInv _ h
           f ()

    ⌊_⌋ : {Δ : LCtx} -> Pat⁺ Δ 2⁺ -> Pat⁺ [] 2⁺
    ⌊_⌋ Ptt = Ptt
    ⌊_⌋ Pff = Pff

    tt : {Γ : UCtx} -> RFoc Γ 2⁺
    tt = Val Ptt NilCtx
    ff : {Γ : UCtx} -> RFoc Γ 2⁺
    ff = Val Pff NilCtx

    not : (Γ : UCtx) -> RInv Γ (HN (2⁺ → ↑ 2⁺))
    not Γ = Susp not*
      where
        not* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c
        not* (Dapp Ptt Dp) = Ret ff
        not* (Dapp Pff Dp) = Ret tt

    and : (Γ : UCtx) -> RInv Γ (HN (2⁺ → 2⁺ → ↑ 2⁺))
    and Γ = Susp and*
      where
        and* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (2⁺ → 2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c
        and* (Dapp Ptt (Dapp Ptt Dp)) = Ret tt
        and* (Dapp Ptt (Dapp Pff Dp)) = Ret ff
        and* (Dapp Pff (Dapp Ptt Dp)) = Ret ff
        and* (Dapp Pff (Dapp Pff Dp)) = Ret ff

    App' : {Γ : UCtx} {A⁺ B⁺ : Pos} {c : Conc} -> 
           (HN (A⁺ → ↑ B⁺) ∈∈ Γ) -> (RFoc Γ A⁺) -> (LInv Γ (CP B⁺) c) ->
           UnFoc Γ c
    App' u (Val p σ) F = App u (Spine (Dapp p Dp) σ F)

    table1 : (Γ : UCtx) -> RInv Γ (HN (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺)))
    table1 Γ = Susp table1*
      where
        table1* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺)) c -> UnFoc (Δ :: Γ) c
        table1* (Dapp Pu Dp) = App' (s0 f0) tt (Fn (\b1 -> 
                               App' (sS (s0 f0)) ff (Fn (\b2 -> 
                                     Ret (Val (Ppair ⌊ b1 ⌋ ⌊ b2 ⌋) NilCtx)))))