module Example2 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 : Set where
  scope : (nm : Ident) -> Err

Errs : Set
Errs = List Err

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₂) = {!!}

_∈?_ : (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 Source : Set where
  def   : (nm : Ident) -> Source
  use   : (nm : Ident) -> Source
  _◆_   : (left : Source) -> (right : Source) -> Source

Target : Set
Target = Source

V₂ : Set
V₂ = (Γ₂ : Env) -> Errs × Target

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

visit : V₁
visit (def nm) = ([ nm ] , k)
               where k : V₂
                     k Γ = [] , (def nm)
visit (use nm) = ([] , k)
               where k : V₂
                     k Γ with nm ∈? Γ | use nm
                     ... | inj₁ _ | t = [ scope nm  ] , t
                     ... | inj₂ _ | t = [] , t
visit (left ◆ right) with visit left
... | (Γ₁ , kLeft) with visit right
... | (Γ₂ , kRight) = (Γ₁ ++ Γ₂ , k) 
                    where k : V₂
                          k Γ with kLeft Γ
                          k Γ | es₁ , t₁ with kRight Γ
                          k Γ | es₁ , t₁ | es₂ , t₂ = es₁ ++ es₂ , t₁ ◆ t₂

compile : Env -> Source -> Errs × Target
compile Γ₀ e with visit e
... | (Γ₁ , k) = k (Γ₁ ++ Γ₀)

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

initEnv : Env
initEnv = [ i₂ ]

test : Errs × Target
test = compile initEnv ((use i₂) ◆ (use i₁) ◆ (def i₁))


{-
mutual
  f : Set -> (Set × Set)
  f x = (Env , x)

  z : (Set × Set)
  z = f (proj₁ z)
-}