module Example where

open import Data.List
open import Data.Maybe
open import Data.Product
open import Data.String hiding ( _++_ )
open import Relation.Binary.Core
open import Relation.Nullary.Core
open import Data.Sum
open import Data.Empty

Ident : Set
Ident = String

Env : Set
Env = List Ident

data _≤_ : (Γ₁ : Env) -> (Γ₂ : Env) -> Set where
  trans    : {Γ₁ : Env} {Γ₂ : Env} {Γ₃ : Env} -> Γ₁ ≤ Γ₂ -> Γ₂ ≤ Γ₃ -> Γ₁ ≤ Γ₃
  subLeft  : {Γ₁ : Env} {Γ₂ : Env} -> Γ₁ ≤ (Γ₁ ++ Γ₂)
  subRight : {Γ₁ : Env} {Γ₂ : Env} -> Γ₂ ≤ (Γ₁ ++ Γ₂)

data _∈_ : (nm : Ident) -> (Γ : Env) -> Set where
  here : {nm : Ident} {Γ' : Env} -> nm ∈ (nm ∷ Γ')
  next : {nm : Ident} {nm' : Ident} {Γ : Env} -> nm ∈ Γ -> nm ∈ (nm' ∷ Γ)

data Err : Env -> Set where
  scope : {Γ : Env} (nm : Ident) -> ¬ (nm ∈ Γ) -> Err Γ

Errs : Env -> Set
Errs env = List (Err env)

append : {nm : Ident} {Γ : Env} -> (nm ∈ Γ) -> (Γ' : Env) -> (nm ∈ (Γ ++ Γ'))
append {nm} {.nm ∷ Γ} (here)     Γ' = here {nm} {Γ ++ Γ'}
append {nm} {nm' ∷ Γ} (next inΓ) Γ' = next (append {nm} {Γ} inΓ Γ')
append {_}  {[]}      ()         _

prefix : {nm : Ident} {Γ' : Env} -> (nm ∈ Γ') -> (Γ : Env) -> (nm ∈ (Γ ++ Γ'))
prefix inΓ' []      = inΓ'
prefix inΓ' (x ∷ Γ) = next (prefix inΓ' Γ)

_∈≤_ : {nm : Ident} {Γ : Env} {Γ' : Env} -> (Γ' ≤ Γ) -> nm ∈ Γ' -> nm ∈ Γ
(subLeft  {_} {Γ'}) ∈≤ inΓ' = append inΓ' Γ'
(subRight {Γ})      ∈≤ inΓ' = prefix inΓ' Γ
(trans subL subR)   ∈≤ inΓ' = subR ∈≤ ( subL ∈≤ inΓ')

notFirst : {nm : Ident} {nm' : Ident} {Γ : Env} -> ¬ (nm ≡ nm') -> ¬ (nm' ∈ Γ) -> (nm' ∈ (nm ∷ Γ)) -> ⊥
notFirst prv₁ _ here = prv₁ refl
notFirst _ prv₁ (next prv₂) = prv₁ prv₂

_∈?_ : (nm : Ident) -> (Γ : Env) -> ¬ (nm ∈ Γ) ⊎ (nm ∈ Γ)
nm' ∈? [] = inj₁ (\())
nm' ∈? (nm ∷ Γ) with nm ≟ nm'
nm' ∈? (._  ∷ Γ) | yes refl = inj₂ here
nm' ∈? (nm ∷ Γ)  | no prv' with nm' ∈? Γ
nm' ∈? (nm ∷ Γ)  | no prv' | inj₂ prv = inj₂ (next {nm'} {nm} prv)
nm' ∈? (nm ∷ Γ)  | no prv' | inj₁ prv = inj₁ (notFirst prv' prv)

infixl 5 _◆_
data Target : (Γ : Env) -> Set where
  def   : ∀ {Γ} (nm : Ident) -> (nm ∈ Γ) -> Target Γ
  use   : ∀ {Γ} (nm : Ident) -> (nm ∈ Γ) -> Target Γ
  _◆_   : ∀ {Γ} -> (left : Target Γ) -> (right : Target Γ) -> Target Γ

data Source : Set where
  def   : (nm : Ident) -> Source
  use   : (nm : Ident) -> Source
  _◆_   : (left : Source) -> (right : Source) -> Source

data Outcome : Set where
  outcome : ∀{Γ} -> ((Errs Γ) ⊎ (Target Γ)) -> Outcome

V₂ : Env -> Set
V₂ Γ₁ = (Γ₂ : Env) -> Γ₁ ≤ Γ₂ -> Errs Γ₂ ⊎ Target Γ₂

V₁ : Set
V₁ = Source -> Σ Env V₂

visit : V₁
visit (def nm) = ([ nm ] , k)
               where k : V₂ [ nm ]
                     k Γ prv = inj₂ ((def nm (prv ∈≤ here)))
visit (use nm) = ([] , k)
               where k : V₂ []
                     k Γ prv with nm ∈? Γ
                     ... | inj₁ prv'  = inj₁ [ scope nm prv' ]
                     ... | inj₂ prv' = inj₂ (use nm prv')
visit (left ◆ right) with visit left
... | (Γ₁ , kLeft) with visit right
... | (Γ₂ , kRight) = (Γ₁ ++ Γ₂ , k) 
                    where k : V₂ (Γ₁ ++ Γ₂)
                          k Γ prv with kLeft Γ (trans subLeft prv)
                          k Γ prv | inj₁ es with kRight Γ (trans ((subRight {Γ₁} {Γ₂})) prv)
                          k Γ prv | inj₁ es₁ | inj₁ es₂ = inj₁ (es₁ ++ es₂)
                          k Γ prv | inj₁ es₁ | inj₂ _   = inj₁ es₁
                          k Γ prv | inj₂ t₁ with kRight Γ (trans ((subRight {Γ₁} {Γ₂})) prv)
                          k Γ prv | inj₂ _  | inj₁ es₁  = inj₁ es₁
                          k Γ prv | inj₂ t₁ | inj₂ t₂   = inj₂ (t₁ ◆ t₂)

compile : Env -> Source -> Outcome
compile Γ₀ e with visit e
... | (Γ₁ , k) = outcome (k (Γ₁ ++ Γ₀) subLeft)

i₁ = "i1"
i₂ = "i2"

initEnv : Env
initEnv = [ i₂ ]

test : Outcome
test = compile initEnv ((use i₂) ◆ (use i₁) ◆ (def i₁))