text:
module Types.IND where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Product

open import Function

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

open import Types.Direction
open import Auxiliary.Extensionality

open import Auxiliary.RewriteLemmas

private
  variable
    m n : ℕ

----------------------------------------------------------------------
-- session type inductively with explicit rec

data Polarity : Set where
  POS NEG : Polarity

mutual
  data Type n : Set where
    TUnit TInt : Type n
    TPair : (T₁ : Type n) (T₂ : Type n) → Type n
    TChan : (S : SType n) → Type n

  data SType n : Set where
    gdd : (G : GType n) → SType n
    rec : (G : GType (suc n) ) → SType n
    var : (p : Polarity) → (x : Fin n) → SType n

  data GType n : Set where
    transmit : (d : Dir) (T : Type n) (S : SType n) → GType n
    choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
    end : GType n

TType = Type

-- weakening

weakenS : (n : ℕ) → SType m → SType (m + n)
weakenG : (n : ℕ) → GType m → GType (m + n)
weakenT : (n : ℕ) → TType m → TType (m + n)

weakenS n (gdd gst) = gdd (weakenG n gst)
weakenS n (rec gst) = rec (weakenG n gst)
weakenS n (var p x) = var p (inject+ n x)

weakenG n (transmit d t s) = transmit d (weakenT n t) (weakenS n s)
weakenG n (choice d m alt) = choice d m (weakenS n ∘ alt)
weakenG n end = end

weakenT n TUnit = TUnit
weakenT n TInt = TInt
weakenT n (TPair ty ty₁) = TPair (weakenT n ty) (weakenT n ty₁)
weakenT n (TChan x) = TChan (weakenS n x)

weaken1 : SType m → SType (suc m)
weaken1{m} stm with weakenS 1 stm
... | r rewrite n+1=suc-n {m} = r

module CheckWeaken where
  s0 : SType 0
  s0 = rec (transmit SND TUnit (var POS zero))
  s1 : SType 1
  s1 = rec (transmit SND TUnit (var POS zero))
  s2 : SType 2
  s2 = rec (transmit SND TUnit (var POS zero))

  check-weakenS1 : weakenS 1 s0 ≡ s1
  check-weakenS1 = cong rec (cong (transmit SND TUnit) refl)

  check-weakenS2 : weakenS 2 s0 ≡ s2
  check-weakenS2 = cong rec (cong (transmit SND TUnit) refl)

weaken1'N : Fin (suc n) → Fin n → Fin (suc n)
weaken1'N zero x = suc x
weaken1'N (suc i) zero = zero
weaken1'N (suc i) (suc x) = suc (weaken1'N i x)

weaken1'S : Fin (suc n) → SType n → SType (suc n)
weaken1'G : Fin (suc n) → GType n → GType (suc n)
weaken1'T : Fin (suc n) → TType n → TType (suc n)

weaken1'S i (gdd gst) = gdd (weaken1'G i gst)
weaken1'S i (rec gst) = rec (weaken1'G (suc i) gst)
weaken1'S i (var p x) = var p (weaken1'N i x)

weaken1'G i (transmit d t s) = transmit d (weaken1'T i t) (weaken1'S i s)
weaken1'G i (choice d m alt) = choice d m (weaken1'S i ∘ alt)
weaken1'G i end = end

weaken1'T i TUnit = TUnit
weaken1'T i TInt = TInt
weaken1'T i (TPair t₁ t₂) = TPair (weaken1'T i t₁) (weaken1'T i t₂)
weaken1'T i (TChan x) = TChan (weaken1'S i x)

weaken1S : SType n → SType (suc n)
weaken1G : GType n → GType (suc n)
weaken1T : Type n → Type (suc n)

weaken1S = weaken1'S zero
weaken1G = weaken1'G zero
weaken1T = weaken1'T zero

module CheckWeaken1' where
  sxy : ∀ n → Fin (suc n) → SType n
  sxy n x = rec (transmit SND TUnit (var POS x))

  s00 : SType 0
  s00 = sxy 0 zero
  s10 : SType 1
  s10 = sxy 1 zero
  s11 : SType 1
  s11 = sxy 1 (suc zero)
  s22 : SType 2
  s22 = sxy 2 (suc (suc zero))

  check-weaken-s01 : weaken1'S zero s00 ≡ s10
  check-weaken-s01 = refl

  check-weaken-s1-s2 : weaken1'S zero s11 ≡ s22
  check-weaken-s1-s2 = refl

  check-weaken-s21 : weaken1'S (suc zero) (sxy 2 (suc zero)) ≡ sxy 3 (suc zero)
  check-weaken-s21 = refl
--------------------------------------------------------------------

dual-pol : Polarity → Polarity
dual-pol POS = NEG
dual-pol NEG = POS

dual-pol-inv : ∀ p → dual-pol (dual-pol p) ≡ p
dual-pol-inv POS = refl
dual-pol-inv NEG = refl

swap-polS : (i : Fin (suc n)) → SType (suc n) → SType (suc n)
swap-polG : (i : Fin (suc n)) → GType (suc n) → GType (suc n)
swap-polT : (i : Fin (suc n)) → Type (suc n) → Type (suc n)

swap-polG i (transmit d t st) = transmit d (swap-polT i t) (swap-polS i st)
swap-polG i (choice d m alt) = choice d m (swap-polS i ∘ alt)
swap-polG i end = end

swap-polS i (gdd gst) = gdd (swap-polG i gst)
swap-polS i (rec st) = rec (swap-polG (suc i) st)
swap-polS zero (var p zero) = var (dual-pol p) zero
swap-polS (suc i) (var p zero) = var p zero
swap-polS zero (var p (suc x)) = var p (suc x)
swap-polS {suc n} (suc i) (var p (suc x)) = weaken1S (swap-polS i (var p x))

swap-polT i TUnit = TUnit
swap-polT i TInt = TInt
swap-polT i (TPair t₁ t₂) = TPair (swap-polT i t₁) (swap-polT i t₂)
swap-polT i (TChan x) = TChan (swap-polS i x)

--------------------------------------------------------------------

weak-weakN : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (x : Fin n)
  → weaken1'N (suc i) (weaken1'N j x) ≡ weaken1'N (inject₁ j) (weaken1'N i x)
weak-weakG : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (g : GType n)
  → weaken1'G (suc i) (weaken1'G j g) ≡ weaken1'G (inject₁ j) (weaken1'G i g)
weak-weakS : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s : SType n)
  → weaken1'S (suc i) (weaken1'S j s) ≡ weaken1'S (inject₁ j) (weaken1'S i s)
weak-weakT : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (t : Type n)
  → weaken1'T (suc i) (weaken1'T j t) ≡ weaken1'T (inject₁ j) (weaken1'T i t)

weak-weakN zero zero le x                              = refl
weak-weakN (suc i) zero le x                         = refl
weak-weakN (suc i) (suc j) (s≤s le) zero           = refl
weak-weakN{suc n} (suc i) (suc j) (s≤s le) (suc x) = cong suc (weak-weakN i j le x)

weak-weakG i j le (transmit d t s) = cong₂ (transmit d) (weak-weakT i j le t) (weak-weakS i j le s)
weak-weakG i j le (choice d m alt) = cong (choice d m) (ext (weak-weakS i j le ∘ alt))
weak-weakG i j le end              = refl

weak-weakS i j le (gdd gst) = cong gdd (weak-weakG i j le gst)
weak-weakS i j le (rec gst) = cong rec (weak-weakG (suc i) (suc j) (s≤s le) gst)
weak-weakS i j le (var p x) = cong (var p) (weak-weakN i j le x)

weak-weakT i j le TUnit        = refl
weak-weakT i j le TInt         = refl
weak-weakT i j le (TPair t t₁) = cong₂ TPair (weak-weakT i j le t) (weak-weakT i j le t₁)
weak-weakT i j le (TChan s)    = cong TChan (weak-weakS i j le s)

weaken1-weakenN : (m : ℕ) (j : Fin (suc n)) (x : Fin n)
  → inject+ m (weaken1'N j x) ≡ weaken1'N (inject+ m j) (inject+ m x)
weaken1-weakenN m zero zero           = refl
weaken1-weakenN m zero (suc x)      = refl
weaken1-weakenN m (suc j) zero      = refl
weaken1-weakenN m (suc j) (suc x) = cong suc (weaken1-weakenN m j x)

weaken1-weakenS : (m : ℕ) (j : Fin (suc n)) (s : SType n)
  → weakenS m (weaken1'S j s) ≡ weaken1'S (inject+ m j) (weakenS m s)
weaken1-weakenG : (m : ℕ) (j : Fin (suc n)) (g : GType n)
  → weakenG m (weaken1'G j g) ≡ weaken1'G (inject+ m j) (weakenG m g)
weaken1-weakenT : (m : ℕ) (j : Fin (suc n)) (t : Type n)
  → weakenT m (weaken1'T j t) ≡ weaken1'T (inject+ m j) (weakenT m t)
weaken1-weakenS m j (gdd gst) = cong gdd (weaken1-weakenG m j gst)
weaken1-weakenS m j (rec gst) = cong rec (weaken1-weakenG m (suc j) gst)
weaken1-weakenS m zero (var p zero)      = refl
weaken1-weakenS m zero (var p (suc x)) = refl
weaken1-weakenS {suc n} m (suc j) (var p zero)      = refl
weaken1-weakenS {suc n} m (suc j) (var p (suc x)) = cong (var p) (cong suc (weaken1-weakenN m j x))

weaken1-weakenG m j (transmit d t s)  = cong₂ (transmit d) (weaken1-weakenT m j t) (weaken1-weakenS m j s)
weaken1-weakenG m j (choice d m₁ alt) = cong (choice d m₁) (ext (weaken1-weakenS m j ∘ alt))
weaken1-weakenG m j end = refl

weaken1-weakenT m j TUnit = refl
weaken1-weakenT m j TInt = refl
weaken1-weakenT m j (TPair t t₁) = cong₂ TPair (weaken1-weakenT m j t) (weaken1-weakenT m j t₁)
weaken1-weakenT m j (TChan x) = cong TChan (weaken1-weakenS m j x)

--------------------------------------------------------------------

-- weakening of later index
{-# TERMINATING #-}
swap-weaken1'G : (i : Fin (suc (suc n))) (j : Fin′ i) (gst : GType (suc n)) →
  swap-polG (inject j) (weaken1'G i gst) ≡ weaken1'G i (swap-polG (inject! j) gst)
swap-weaken1'S : (i : Fin (suc (suc n))) (j : Fin′ i) (sst : SType (suc n)) →
  swap-polS (inject j) (weaken1'S i sst) ≡ weaken1'S i (swap-polS (inject! j) sst)
swap-weaken1'T : (i : Fin (suc (suc n))) (j : Fin′ i) (t : Type (suc n)) →
  swap-polT (inject j) (weaken1'T i t) ≡ weaken1'T i (swap-polT (inject! j) t)

swap-weaken1'G i j (transmit d t s) = cong₂ (transmit d) (swap-weaken1'T i j t) (swap-weaken1'S i j s)
swap-weaken1'G i j (choice d m alt) = cong (choice d m) (ext (swap-weaken1'S i j ∘ alt))
swap-weaken1'G i j end = refl

swap-weaken1'S i j (gdd gst) = cong gdd (swap-weaken1'G i j gst)
swap-weaken1'S i j (rec gst) = cong rec (swap-weaken1'G (suc i) (suc j) gst)
swap-weaken1'S zero () (var p x)
swap-weaken1'S (suc i) zero (var p zero) = refl
swap-weaken1'S (suc i) zero (var p (suc x)) = refl
swap-weaken1'S (suc i) (suc j) (var p zero) = refl
swap-weaken1'S{suc n} (suc i) (suc j) (var p (suc x)) rewrite (weak-weakS i zero z≤n (swap-polS (inject! j) (var p x))) =
  let sws = swap-weaken1'S{n} i j (var p x) in cong (weaken1'S zero) sws

swap-weaken1'T i j TUnit         = refl
swap-weaken1'T i j TInt          = refl
swap-weaken1'T i j (TPair t₁ t₂) = cong₂ TPair (swap-weaken1'T i j t₁) (swap-weaken1'T i j t₂)
swap-weaken1'T i j (TChan s)     = cong TChan (swap-weaken1'S i j s)

--------------------------------------------------------------------

-- weakening of earlier index
{-# TERMINATING #-}
swap-weaken1'S< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (s : SType (suc n)) →
  swap-polS (suc i) (weaken1'S (inject₁ j) s) ≡ weaken1'S (inject₁ j) (swap-polS i s)
swap-weaken1'G< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (g : GType (suc n)) →
  swap-polG (suc i) (weaken1'G (inject₁ j) g) ≡ weaken1'G (inject₁ j) (swap-polG i g)
swap-weaken1'T< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (t : Type (suc n)) →
  swap-polT (suc i) (weaken1'T (inject₁ j) t) ≡ weaken1'T (inject₁ j) (swap-polT i t)

swap-weaken1'S< i j le (gdd gst)       = cong gdd (swap-weaken1'G< i j le gst)
swap-weaken1'S< i j le (rec gst)       = cong rec (swap-weaken1'G< (suc i) (suc j) (s≤s le) gst)
swap-weaken1'S< zero zero le (var p x)     = refl
swap-weaken1'S< (suc i) zero le (var p x) = refl
swap-weaken1'S<{suc n} (suc i) (suc j) le (var p zero) = refl
swap-weaken1'S<{suc n} (suc i) (suc j) (s≤s le) (var p (suc x)) rewrite (weak-weakS (inject₁ j) zero z≤n (swap-polS i (var p x))) =
  let sws = swap-weaken1'S<{n} i j le (var p x) in cong (weaken1'S zero) sws

swap-weaken1'G< i j le (transmit d t s) = cong₂ (transmit d) (swap-weaken1'T< i j le t) (swap-weaken1'S< i j le s)
swap-weaken1'G< i j le (choice d m alt) = cong (choice d m) (ext ((swap-weaken1'S< i j le) ∘ alt))
swap-weaken1'G< i j le end = refl

swap-weaken1'T< i j le TUnit = refl
swap-weaken1'T< i j le TInt = refl
swap-weaken1'T< i j le (TPair t t₁) = cong₂ (TPair) (swap-weaken1'T< i j le t) (swap-weaken1'T< i j le t₁)
swap-weaken1'T< i j le (TChan s) = cong (TChan) (swap-weaken1'S< i j le s)

swap-weakenS : (i : Fin (suc n)) → (s : SType (suc n)) →
  swap-polS (suc i) (weaken1S s) ≡ weaken1S (swap-polS i s)
swap-weakenG : (i : Fin (suc n)) → (g : GType (suc n)) →
  swap-polG (suc i) (weaken1G g) ≡ weaken1G (swap-polG i g)
swap-weakenT : (i : Fin (suc n)) → (t : Type (suc n)) →
  swap-polT (suc i) (weaken1T t) ≡ weaken1T (swap-polT i t)

swap-weakenS i s = swap-weaken1'S< i zero z≤n s
swap-weakenG i g = swap-weaken1'G< i zero z≤n g
swap-weakenT i t = swap-weaken1'T< i zero z≤n t

--------------------------------------------------------------------

-- swapping of general weakening
{-# TERMINATING #-}
swap-weakenG' : (m : ℕ) (j : Fin (suc n)) (gst : GType (suc n))
  → swap-polG (inject+ m j) (weakenG m gst) ≡ weakenG m (swap-polG j gst)
swap-weakenS' : (m : ℕ) (j : Fin (suc n)) (s : SType (suc n))
  → swap-polS (inject+ m j) (weakenS m s) ≡ weakenS m (swap-polS j s)
swap-weakenT' : (m : ℕ) (j : Fin (suc n)) (t : Type (suc n))
  → swap-polT (inject+ m j) (weakenT m t) ≡ weakenT m (swap-polT j t)

swap-weakenG' m j (transmit d t s) = cong₂ (transmit d) (swap-weakenT' m j t) (swap-weakenS' m j s)
swap-weakenG' m j (choice d m₁ alt) = cong (choice d m₁) (ext (swap-weakenS' m j ∘ alt))
swap-weakenG' m j end = refl

swap-weakenS' m j (gdd gst) = cong gdd (swap-weakenG' m j gst)
swap-weakenS' m j (rec gst) = cong rec (swap-weakenG' m (suc j) gst)
swap-weakenS' m zero (var p zero)      = refl
swap-weakenS' m (suc j) (var p zero) = refl
swap-weakenS' m zero (var p (suc zero))      = refl
swap-weakenS' m zero (var p (suc (suc x))) = refl
swap-weakenS' {suc n} m (suc j) (var p (suc x)) rewrite (weaken1-weakenS m zero (swap-polS j (var p x))) =
   let rst = swap-weakenS'{n} m j (var p x) in cong weaken1S rst

swap-weakenT' m j TUnit = refl
swap-weakenT' m j TInt = refl
swap-weakenT' m j (TPair t t₁) = cong₂ TPair (swap-weakenT' m j t) (swap-weakenT' m j t₁)
swap-weakenT' m j (TChan x) = cong TChan (swap-weakenS' m j x)

--------------------------------------------------------------------

{-# TERMINATING #-}
swap-pol-invS : (i : Fin (suc n)) → (st : SType (suc n)) →
  swap-polS i (swap-polS i st) ≡ st
swap-pol-invG : (i : Fin (suc n)) → (st : GType (suc n)) →
  swap-polG i (swap-polG i st) ≡ st
swap-pol-invT : (i : Fin (suc n)) → (ty : Type (suc n)) →
  swap-polT i (swap-polT i ty) ≡ ty

swap-pol-invS i (gdd gst) = cong gdd (swap-pol-invG i gst)
swap-pol-invS i (rec gst) = cong rec (swap-pol-invG (suc i) gst)
swap-pol-invS zero (var p zero) rewrite dual-pol-inv p = refl
swap-pol-invS (suc i) (var p zero) = refl
swap-pol-invS zero (var p (suc x)) rewrite dual-pol-inv p = refl
swap-pol-invS {suc n} (suc i) (var p (suc x))
  rewrite swap-weakenS i (swap-polS i (var p x)) | swap-pol-invS i (var p x) = refl

-- extensionality needed
swap-pol-invG i (transmit d t s) = cong₂ (transmit d) (swap-pol-invT i t) (swap-pol-invS i s)
swap-pol-invG i (choice d m alt) = cong (choice d m) (ext R)
  where R : ∀ x → swap-polS i (swap-polS i (alt x)) ≡ alt x
        R x rewrite swap-pol-invS i (alt x) = refl
swap-pol-invG i end = refl

swap-pol-invT i TUnit = refl
swap-pol-invT i TInt = refl
swap-pol-invT i (TPair ty ty₁) = cong₂ TPair (swap-pol-invT i ty) (swap-pol-invT i ty₁)
swap-pol-invT i (TChan x) = cong TChan (swap-pol-invS i x)

--------------------------------------------------------------------
-- LM duality
dualS : SType n → SType n
dualG : GType n → GType n

dualG (transmit d t st) = transmit (dual-dir d) t (dualS st)
dualG (choice d m alt) = choice (dual-dir d) m (dualS ∘ alt)
dualG end = end

dualS (gdd gst) = gdd (dualG gst)
dualS (rec gst) = rec (swap-polG zero (dualG gst))
dualS (var p x) = var (dual-pol p) x

--------------------------------------------------------------------

dual-weakenS : (i : Fin (suc n)) (s : SType n) → dualS (weaken1'S i s) ≡ weaken1'S i (dualS s)
dual-weakenG : (i : Fin (suc n)) (g : GType n) → dualG (weaken1'G i g) ≡ weaken1'G i (dualG g)

dual-weakenS i (gdd gst) = cong gdd (dual-weakenG i gst)
dual-weakenS i (rec gst) rewrite (sym (swap-weaken1'G (suc i) zero (dualG gst))) = cong rec (cong (swap-polG zero) (dual-weakenG (suc i) gst))
dual-weakenS i (var p x) = refl

dual-weakenG i (transmit d t s) = cong₂ (transmit (dual-dir d)) refl (dual-weakenS i s)
dual-weakenG i (choice d m alt) = cong (choice (dual-dir d) m) (ext (dual-weakenS i ∘ alt))
dual-weakenG i end = refl

dual-weakenS' : (m : ℕ) (s : SType n) → dualS (weakenS m s) ≡ weakenS m (dualS s)
dual-weakenG' : (m : ℕ) (g : GType n) → dualG (weakenG m g) ≡ weakenG m (dualG g)

dual-weakenS' n (gdd gst) = cong gdd (dual-weakenG' n gst)
dual-weakenS' n (rec gst) rewrite (sym (swap-weakenG' n zero (dualG gst))) = cong rec (cong (swap-polG zero) (dual-weakenG' n gst))
dual-weakenS' n (var p x) = refl

dual-weakenG' n (transmit d t s) = cong₂ (transmit (dual-dir d)) refl (dual-weakenS' n s)
dual-weakenG' n (choice d m alt) = cong (choice (dual-dir d) m) (ext (dual-weakenS' n ∘ alt))
dual-weakenG' n end = refl

--------------------------------------------------------------------

aux : (i : Fin n) (x : Fin n) (p' : Polarity) →
  var p' (suc (suc x)) ≡ weaken1S (var p' (suc x))
aux i x p = refl

var-suc : (i : Fin n) (x : Fin n) (p : Polarity) →
  ∃ λ p' → swap-polS (suc i) (var p (suc x)) ≡ var p' (suc x)
var-suc zero zero p = dual-pol p , refl
var-suc (suc i) zero p = p , refl
var-suc zero (suc x) p = p , refl
var-suc (suc i) (suc x) p
  with var-suc i x p
... | p' , snd
  rewrite sym (aux i x p') = p' , cong weaken1S snd

--------------------------------------------------------------------

{-# TERMINATING #-}
swap-swapG : (gst : GType (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
  swap-polG i (swap-polG (inject j) gst) ≡ swap-polG (inject j) (swap-polG i gst)
swap-swapT : (t : Type (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
  swap-polT i (swap-polT (inject j) t) ≡ swap-polT (inject j) (swap-polT i t)
swap-swapS : (st : SType (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
  swap-polS i (swap-polS (inject j) st) ≡ swap-polS (inject j) (swap-polS i st)

swap-swapG (transmit d t s) i j = cong₂ (transmit d) (swap-swapT t i j) (swap-swapS s i j)
swap-swapG (choice d m alt) i j = cong (choice d m) (ext (λ x → swap-swapS (alt x) i j))
swap-swapG end i j = refl

swap-swapT TUnit i j = refl
swap-swapT TInt i j = refl
swap-swapT (TPair t t₁) i j = cong₂ TPair (swap-swapT t i j) (swap-swapT t₁ i j)
swap-swapT (TChan x) i j = cong TChan (swap-swapS x i j)

swap-swapS (gdd gst) i j = cong gdd (swap-swapG gst i j)
swap-swapS (rec gst) i j = cong rec (swap-swapG gst (suc i) (suc j))
swap-swapS (var p zero) zero ()
swap-swapS (var p zero) (suc i) zero = refl
swap-swapS (var p zero) (suc i) (suc j) = refl
swap-swapS (var p (suc x)) zero ()
swap-swapS (var p (suc x)) (suc i) zero
  with var-suc i x p
... | p' , snd rewrite snd = refl
swap-swapS {suc n} (var p (suc x)) (suc i) (suc j)
  rewrite swap-weakenS i (swap-polS (inject j) (var p x))
  with swap-swapS (var p x) i j
... | pxij rewrite swap-weakenS (inject j) (swap-polS i (var p x))
  = cong weaken1S pxij

{-# TERMINATING #-}
swap-pol-dualG : (i : Fin (suc n)) (gst : GType (suc n)) →
  swap-polG i (dualG gst) ≡ dualG (swap-polG i gst)
swap-pol-dualS : (i : Fin (suc n)) (st : SType (suc n)) →
  swap-polS i (dualS st) ≡ dualS (swap-polS i st)

swap-pol-dualG i (transmit d t s) = cong (transmit _ (swap-polT i t)) (swap-pol-dualS i s)
swap-pol-dualG i (choice d m alt) = cong (choice _ _) (ext (swap-pol-dualS i ∘ alt))
swap-pol-dualG i end = refl

swap-pol-dualS i (gdd gst) = cong gdd (swap-pol-dualG i gst)
swap-pol-dualS i (rec gst) rewrite sym (swap-pol-dualG (suc i) gst) =
  cong rec (swap-swapG (dualG gst) (suc i) zero)
swap-pol-dualS zero (var p zero) = refl
swap-pol-dualS (suc i) (var p zero) = refl
swap-pol-dualS zero (var p (suc x)) = refl
swap-pol-dualS {suc n} (suc i) (var p (suc x))
   rewrite (dual-weakenS zero (swap-polS i (var p x))) =  cong weaken1S (swap-pol-dualS i (var p x))

--------------------------------------------------------------------

dual-invS : (st : SType n) → st ≡ dualS (dualS st)
dual-invG : (gst : GType n) → gst ≡ dualG (dualG gst)

dual-invS (gdd gst) = cong gdd (dual-invG gst)
dual-invS (rec gst) rewrite sym (swap-pol-dualG zero (dualG gst)) | swap-pol-invG zero (dualG (dualG gst)) = cong rec (dual-invG gst)
dual-invS (var p x) rewrite dual-pol-inv p = refl

dual-invG (transmit d t s) rewrite dual-dir-inv d = cong₂ (transmit d) refl (dual-invS s)
dual-invG (choice d m alt) rewrite dual-dir-inv d = cong (choice d m) (ext R)
  where R : (x : Fin m) → alt x ≡ dualS (dualS (alt x))
        R x rewrite sym (dual-invS (alt x)) = refl
dual-invG end = refl

dual-if : Polarity → SType n → SType n
dual-if POS s = s
dual-if NEG s = dualS s

dual-if-dual : (p : Polarity) (ist : SType 0) → dual-if p ist ≡ dual-if (dual-pol p) (dualS ist)
dual-if-dual POS ist = (dual-invS ist)
dual-if-dual NEG ist = refl

--------------------------------------------------------------------
-- substitution

st-substS : SType (suc n) → Fin (suc n) → SType 0 → SType n
st-substG : GType (suc n) → Fin (suc n) → SType 0 → GType n
st-substT : Type (suc n) → Fin (suc n) → SType 0 → Type n

st-substS (gdd gst) i st0 = gdd (st-substG gst i st0)
st-substS (rec gst) i st0 = rec (st-substG gst (suc i) st0)
st-substS {n} (var p zero) zero st0 = weakenS n (dual-if p st0)
st-substS {suc n} (var p zero) (suc i) st0 = var p zero
st-substS {suc n} (var p (suc x)) zero st0 = var p x
st-substS {suc n} (var p (suc x)) (suc i) st0 = weaken1S (st-substS (var p x) i st0)

st-substG (transmit d t s) i st0 = transmit d (st-substT t i st0) (st-substS s i st0)
st-substG (choice d m alt) i st0 = choice d m (λ j → st-substS (alt j) i st0)
st-substG end i st0 = end

st-substT TUnit i st0 = TUnit
st-substT TInt i st0 = TInt
st-substT (TPair ty ty₁) i st0 = TPair (st-substT ty i st0) (st-substT ty₁ i st0)
st-substT (TChan st) i st0 = TChan (st-substS st i st0)

--------------------------------------------------------------------

trivial-subst-var : (p : Polarity) (x : Fin n) (ist₁ ist₂ : SType 0)
  → st-substS (var p (suc x)) zero ist₁ ≡ st-substS (var p (suc x)) zero ist₂
trivial-subst-var p zero ist1 ist2 = refl
trivial-subst-var p (suc x) ist1 ist2 = refl

trivial-subst-var' : (p : Polarity) (i : Fin n) (ist₁ ist₂ : SType 0)
  → st-substS (var p zero) (suc i) ist₁ ≡ st-substS (var p zero) (suc i) ist₂
trivial-subst-var' p zero ist1 ist2 = refl
trivial-subst-var' p (suc x) ist1 ist2 = refl

--------------------------------------------------------------------
-- equivalence
variable
  t t₁ t₂ t₁' t₂' : Type n
  s s₁ s₂ : SType n
  g g₁ g₂ : GType n

unfold : SType 0 → GType 0
unfold (gdd gst) = gst
unfold (rec gst) = st-substG gst zero (rec gst)

-- type equivalence
data EquivT (R : SType n → SType n → Set) : Type n → Type n → Set where
  eq-unit : EquivT R TUnit TUnit
  eq-int  : EquivT R TInt TInt
  eq-pair : EquivT R t₁ t₁' → EquivT R t₂ t₂' → EquivT R (TPair t₁ t₂) (TPair t₁' t₂')
  eq-chan : R s₁ s₂ → EquivT R (TChan s₁) (TChan s₂)

-- session type equivalence
data EquivG (R : SType n → SType n → Set) : GType n → GType n → Set where
  eq-transmit : (d : Dir) → EquivT R t₁ t₂ → R s₁ s₂ → EquivG R (transmit d t₁ s₁) (transmit d t₂ s₂)
  eq-choice : ∀ {alt alt'} → (d : Dir) → ((i : Fin m) → R (alt i) (alt' i)) → EquivG R (choice d m alt) (choice d m alt')
  eq-end : EquivG R end end

record Equiv (s₁ s₂ : SType 0) : Set where
  coinductive
  field force : EquivG Equiv (unfold s₁) (unfold s₂)

open Equiv

_≈_ = Equiv
_≈'_ = EquivG Equiv
_≈ᵗ_ = EquivT Equiv

-- reflexive

≈-refl : s ≈ s
≈'-refl : g ≈' g
≈ᵗ-refl : t ≈ᵗ t

force (≈-refl {s}) = ≈'-refl

≈'-refl {transmit d t s} = eq-transmit d ≈ᵗ-refl ≈-refl
≈'-refl {choice d m alt} = eq-choice d (λ i → ≈-refl)
≈'-refl {end} = eq-end

≈ᵗ-refl {TUnit} = eq-unit
≈ᵗ-refl {TInt} = eq-int
≈ᵗ-refl {TPair t t₁} = eq-pair ≈ᵗ-refl ≈ᵗ-refl
≈ᵗ-refl {TChan x} = eq-chan ≈-refl

-- symmetric

≈-symm : s₁ ≈ s₂ → s₂ ≈ s₁
≈'-symm : g₁ ≈' g₂ → g₂ ≈' g₁
≈ᵗ-symm : t₁ ≈ᵗ t₂ → t₂ ≈ᵗ t₁

force (≈-symm s₁≈s₂) = ≈'-symm (force s₁≈s₂)

≈'-symm (eq-transmit d x x₁) = eq-transmit d (≈ᵗ-symm x) (≈-symm x₁)
≈'-symm (eq-choice d x) = eq-choice d (≈-symm ∘ x)
≈'-symm eq-end = eq-end

≈ᵗ-symm eq-unit = eq-unit
≈ᵗ-symm eq-int = eq-int
≈ᵗ-symm (eq-pair t₁≈ᵗt₂ t₁≈ᵗt₃) = eq-pair (≈ᵗ-symm t₁≈ᵗt₂) (≈ᵗ-symm t₁≈ᵗt₃)
≈ᵗ-symm (eq-chan x) = eq-chan (≈-symm x)

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Pointwise
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where

open import Data.Fin.Base
open import Data.Fin.Properties
  hiding (isDecEquivalence; setoid; decSetoid)
open import Data.Nat.Base
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
  using () renaming (Pointwise to ×-Pointwise)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Functional as VF hiding (map)
open import Data.Vec.Functional.Relation.Binary.Pointwise
open import Function
open import Level using (Level)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

private
  variable
    a a′ a″ b b′ b″ r s t ℓ : Level
    A : Set a
    B : Set b
    A′ : Set a′
    B′ : Set b′
    A″ : Set a″
    B″ : Set b″

------------------------------------------------------------------------
-- Relational properties

module _ {R : Rel A ℓ} where

  refl : Reflexive R → ∀ {n} → Reflexive (Pointwise R {n})
  refl r i = r

  sym : Symmetric R → ∀ {n} → Symmetric (Pointwise R {n})
  sym s xsys i = s (xsys i)

  trans : Transitive R → ∀ {n} → Transitive (Pointwise R {n})
  trans t xsys yszs i = t (xsys i) (yszs i)

  decidable : Decidable R → ∀ {n} → Decidable (Pointwise R {n})
  decidable r? xs ys = all? λ i → r? (xs i) (ys i)

------------------------------------------------------------------------
-- Structures

  isEquivalence : IsEquivalence R → ∀ n → IsEquivalence (Pointwise R {n})
  isEquivalence isEq n = record
    { refl  = refl  Eq.refl
    ; sym   = sym   Eq.sym
    ; trans = trans Eq.trans
    } where module Eq = IsEquivalence isEq

  isDecEquivalence : IsDecEquivalence R →
                     ∀ n → IsDecEquivalence (Pointwise R {n})
  isDecEquivalence isDecEq n = record
    { isEquivalence = isEquivalence Eq.isEquivalence n
    ; _≟_           = decidable Eq._≟_
    } where module Eq = IsDecEquivalence isDecEq

------------------------------------------------------------------------
-- Bundles

setoid : Setoid a ℓ → ℕ → Setoid a ℓ
setoid S n = record
  { isEquivalence = isEquivalence S.isEquivalence n
  } where module S = Setoid S

decSetoid : DecSetoid a ℓ → ℕ → DecSetoid a ℓ
decSetoid S n = record
  { isDecEquivalence = isDecEquivalence S.isDecEquivalence n
  } where module S = DecSetoid S

------------------------------------------------------------------------
-- map

module _ {R : REL A B r} {S : REL A′ B′ s} {f : A → A′} {g : B → B′} where

  map⁺ : (∀ {x y} → R x y → S (f x) (g y)) →
         ∀ {n} {xs : Vector A n} {ys : Vector B n} →
         Pointwise R xs ys → Pointwise S (VF.map f xs) (VF.map g ys)
  map⁺ f rs i = f (rs i)

------------------------------------------------------------------------
-- head

module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where

  head⁺ : Pointwise R xs ys → R (head xs) (head ys)
  head⁺ rs = rs zero

------------------------------------------------------------------------
-- tail

module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where

  tail⁺ : Pointwise R xs ys → Pointwise R (tail xs) (tail ys)
  tail⁺ rs = rs ∘ suc

------------------------------------------------------------------------
-- _++_

module _ (R : REL A B r) where

  ++⁺ : ∀ {m n xs ys xs′ ys′} →
        Pointwise R {n = m} xs ys → Pointwise R {n = n} xs′ ys′ →
        Pointwise R (xs ++ xs′) (ys ++ ys′)
  ++⁺ {m} rs rs′ i with splitAt m i
  ... | inj₁ i′ = rs i′
  ... | inj₂ j′ = rs′ j′

  ++⁻ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
         Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs ys
  ++⁻ˡ {m} {n} _ _ rs i with rs (inject+ n i)
  ... | r rewrite splitAt-inject+ m n i = r

  ++⁻ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
         Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs′ ys′
  ++⁻ʳ {m} {n} _ _ rs i with rs (raise m i)
  ... | r rewrite splitAt-raise m n i = r

  ++⁻ : ∀ {m n} xs ys {xs′ ys′} →
        Pointwise R (xs ++ xs′) (ys ++ ys′) →
        Pointwise R {n = m} xs ys × Pointwise R {n = n} xs′ ys′
  ++⁻ _ _ rs = ++⁻ˡ _ _ rs , ++⁻ʳ _ _ rs

------------------------------------------------------------------------
-- replicate

module _ {R : REL A B r} {x y n} where

  replicate⁺ : R x y → Pointwise R {n = n} (replicate x) (replicate y)
  replicate⁺ = const

------------------------------------------------------------------------
-- _⊛_

module _ {R : REL A B r} {S : REL A′ B′ s} {n} where

  ⊛⁺ : ∀ {fs : Vector (A → A′) n} {gs : Vector (B → B′) n} →
       Pointwise (λ f g → ∀ {x y} → R x y → S (f x) (g y)) fs gs →
       ∀ {xs ys} → Pointwise R xs ys → Pointwise S (fs ⊛ xs) (gs ⊛ ys)
  ⊛⁺ rss rs i = (rss i) (rs i)

------------------------------------------------------------------------
-- zipWith

module _ {R : REL A B r} {S : REL A′ B′ s} {T : REL A″ B″ t} where

  zipWith⁺ : ∀ {n xs ys xs′ ys′ f f′} →
             (∀ {x y x′ y′} → R x y → S x′ y′ → T (f x x′) (f′ y y′)) →
             Pointwise R xs ys → Pointwise S xs′ ys′ →
             Pointwise T (zipWith f xs xs′) (zipWith f′ {n = n} ys ys′)
  zipWith⁺ t rs ss i = t (rs i) (ss i)

------------------------------------------------------------------------
-- zip

module _ {R : REL A B r} {S : REL A′ B′ s} {n xs ys xs′ ys′} where

  zip⁺ : Pointwise R xs ys → Pointwise S xs′ ys′ →
         Pointwise (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
                   (zip xs xs′) (zip {n = n} ys ys′)
  zip⁺ rs ss i = rs i , ss i

  zip⁻ : Pointwise (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
                   (zip xs xs′) (zip {n = n} ys ys′) →
         Pointwise R xs ys × Pointwise S xs′ ys′
  zip⁻ rss = proj₁ ∘ rss , proj₂ ∘ rss

------------------------------------------------------------------------
-- foldr

module _ {R : REL A B r} {S : REL A′ B′ s}
         {f : A → A′ → A′} {g : B → B′ → B′}
         where

  foldr-cong : (∀ {w x y z} → R w x → S y z → S (f w y) (g x z)) →
               ∀ {d : A′} {e : B′} → S d e →
               ∀ {n} {xs : Vector A n} {ys : Vector B n} →
               Pointwise R xs ys → S (foldr f d xs) (foldr g e ys)
  foldr-cong fg-cong d~e {zero}  rss = d~e
  foldr-cong fg-cong d~e {suc n} rss =
    fg-cong (rss zero) (foldr-cong fg-cong d~e (rss ∘ suc))

ext: agda


text:
-- Syntax: Types, terms and contexts.
module Syntax where

open import Library

infixr 6 _⇒_
infixr 4 _,_

-- Types and contexts.

data Ty : Set where
  ★   : Ty
  _⇒_ : (a b : Ty) → Ty

data Cxt : Set where
  ε   : Cxt
  _,_ : (Γ : Cxt) (a : Ty) → Cxt

-- Variables and terms.

data Var : (Γ : Cxt) (a : Ty) → Set where
  zero : ∀ {Γ a}                 → Var (Γ , a) a
  suc  : ∀ {Γ a b} (x : Var Γ a) → Var (Γ , b) a

data Tm (Γ : Cxt) : (a : Ty) → Set where
  var : ∀ {a}   (x : Var Γ a)                   → Tm Γ a
  abs : ∀ {a b} (t : Tm (Γ , a) b)              → Tm Γ (a ⇒ b)
  app : ∀ {a b} (t : Tm Γ (a ⇒ b)) (u : Tm Γ a) → Tm Γ b

-- Generalized neutral terms.

data GNe (Arg : Cxt → Ty → Set) (Γ : Cxt) : Ty → Set where
  var : ∀{a}    (x : Var Γ a)                         → GNe Arg Γ a
  app : ∀{a b}  (n : GNe Arg Γ (a ⇒ b)) (o : Arg Γ a) → GNe Arg Γ b

-- βη-normal forms.

mutual

  Ne = GNe Nf

  data Nf (Γ : Cxt) : Ty → Set where
    abs : ∀{a b}  (o : Nf (Γ , a) b)  → Nf Γ (a ⇒ b)
    ne  :         (n : Ne Γ ★)        → Nf Γ ★

mutual

  embNe : ∀{Γ a} → Ne Γ a → Tm Γ a
  embNe (var x) = var x
  embNe (app t u) = app (embNe t) (embNf u)

  embNf : ∀{Γ a} → Nf Γ a → Tm Γ a
  embNf (ne t) = embNe t
  embNf (abs t) = abs (embNf t)

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
open import Data.Nat using ( ℕ ) renaming ( zero to zero' ; suc to suc' )
open import Data.Nat.GeneralisedArithmetic using ( fold )
open import Data.String using ( String )

module Data.Natural.Primitive where

infixl 6 _+_

postulate
  Natural : Set
  zero : Natural
  suc : Natural → Natural
  _+_ : Natural → Natural → Natural
  show : Natural → String
  foldl : {A : Set} → (A → A) → A → Natural → A
  foldl' : {A : Set} → (A → A) → A → Natural → A
  foldr : {A : Set} → (A → A) → A → Natural → A

{-# FOREIGN GHC import qualified Data.Natural.AgdaFFI #-}
{-# COMPILE GHC Natural = type Data.Natural.AgdaFFI.Natural #-}
{-# COMPILE GHC zero = 0 #-}
{-# COMPILE GHC suc = succ #-}
{-# COMPILE GHC _+_ = (+) #-}
{-# COMPILE GHC show = show #-}
{-# COMPILE GHC foldl = (\ _ -> Data.Natural.AgdaFFI.nfoldl) #-}
{-# COMPILE GHC foldl' = (\ _ -> Data.Natural.AgdaFFI.nfoldl') #-}
{-# COMPILE GHC foldr = (\ _ -> Data.Natural.AgdaFFI.nfoldr) #-}

private
  postulate
    # : ∀ {i} {A : Set i} → A → Natural
{-# COMPILE GHC # = (\ _ _ -> Data.Natural.AgdaFFI.convert MAlonzo.Data.Nat.mazNatToInteger) #-}

fromℕ : ℕ → Natural
fromℕ = #

max_stars_repo_name: agda/agda-system-io

max_issues_repo_name: agda/agda-system-io

max_forks_repo_name: agda/agda-system-io


text:
-- Mutual Recursion.

module MutRec where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data Odd : Set

data Even : Set where
  e0 : Even
  eS : Odd → Even

data Odd where
  oS : Even → Odd

addEO : Even → Odd → Odd

addOO : Odd → Odd → Even
addOO (oS m) n = eS (addEO m n)

addEO e0 n = n
addEO (eS m) n = oS (addOO m n)

_ : addEO (eS (oS e0)) (oS e0) ≡ oS (eS (oS e0))
_ = refl

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
module Esterel.Lang.Binding where

open import utility
open import Data.List
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Esterel.Lang
open import Esterel.Environment as Env
  using (Env ; VarList ; Dom ; Θ ; _←_)
open import Esterel.Context
  using (Context1 ; EvaluationContext1 ; _≐_⟦_⟧e ; _⟦_⟧e ; _≐_⟦_⟧c ; _⟦_⟧c)
open import Esterel.Context.Properties
  using (plug)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ) renaming (_≟ₛₜ_ to _≟ₛₜₛ_ ; unwrap to Sunwrap)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ) renaming (_≟ₛₜ_ to _≟ₛₜₛₕ_ ; unwrap to sunwrap)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ) renaming (unwrap to vunwrap)
open import Data.Product
  using (_×_ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; ∃ ; Σ)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; _≟_ ; zero ; suc)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)

open import Function
  using (_∘_ ; id ; _∋_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; setoid)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.Bool
  using (not)
open import Data.List.Any as ListAny
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties using (∷↔)
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)

open ListSet Data.Nat._≟_
open _≐_⟦_⟧e
open _≐_⟦_⟧c
open Context1
open EvaluationContext1

base : VarList
base = [] ,′ [] ,′ []

+S : Signal -> VarList -> VarList
+S S' (S , s , v) =  ((Sunwrap S') ∷ S , s , v)

+s : SharedVar -> VarList ->  VarList
+s s' (S , s , v) =  (S , sunwrap s' ∷ s , v)

+x : SeqVar -> VarList -> VarList
+x x' (S , s , v) =  (S , s , vunwrap x' ∷ v)

Xs : VarList -> List ℕ
Xs (_ , _ , v) = v
Ss : VarList -> List ℕ
Ss (S , _ , _) = S
FVₑ : Expr -> VarList
FVₑ (plus []) = base
FVₑ (plus (num x ∷ x₁)) = FVₑ (plus x₁)
FVₑ (plus (seq-ref x ∷ x₁)) = +x x (FVₑ (plus x₁))
FVₑ (plus (shr-ref s ∷ x₁)) = +s s (FVₑ (plus x₁))

dist++ˡ : ∀{VL1 VL2 VL3} → (distinct VL1 (VL2 U̬ VL3)) → (distinct VL1 VL2)
dist++ˡ (a , b , c) =  (dist'++ˡ a) ,(dist'++ˡ b) ,(dist'++ˡ c)

dist++ʳ : ∀{VL1 VL2 VL3} → (distinct VL1 (VL2 U̬ VL3)) → (distinct VL1 VL3)
dist++ʳ{VL1}{VL2 = (v1 , v2 , v3)}{VL3 = (V1 , V2 , V3)} (a , b , c)
   =  (dist'++ʳ{V2 = v1}{V3 = V1} a)  , (dist'++ʳ{V2 = v2}{V3 = V2} b) , (dist'++ʳ{V2 = v3}{V3 = V3} c)

dist++b : ∀{VL1 VL2 VL3 VL4} → (distinct (VL1 U̬ VL2) (VL3 U̬ VL4)) → (distinct VL1 VL3)
dist++b (a , b , c) =  (dist'++b a) , (dist'++b b) , (dist'++b c)

dist:: : ∀{VL1 VL2 S} → (distinct VL1 (+S S VL2)) → (distinct VL1 VL2)
dist::{VL1}{(Ss , s , v)}{S} (a , b , c) = dist':: a  , b , c

{- This definition of CorrectBinding accumulates the bound
   and free variables to make it easier to work with.
   The definition of `CB` (below) matches the one in the paper. -}
data CorrectBinding : Term → (BV : VarList) → (FV : VarList) → Set where
  CBnothing : CorrectBinding nothin base base
  CBpause   : CorrectBinding pause base base
  CBsig     : ∀{p S BV FV} → CorrectBinding p BV FV
                         → CorrectBinding (signl S p) (+S S BV) (FV |̌ (+S S base))
  CBpresent : ∀{S p q BVp FVp BVq FVq}
               → (cbp : CorrectBinding p BVp FVp)
               → (cbq : CorrectBinding q BVq FVq)
               → CorrectBinding (present S ∣⇒ p ∣⇒ q) (BVp U̬ BVq) (+S S (FVp U̬ FVq))
  CBemit    : ∀{S} → CorrectBinding (emit S) base (+S S base)
  CBpar     : ∀{p q BVp FVp BVq FVq}
                → (cbp : CorrectBinding p BVp FVp)
                → (cbq : CorrectBinding q BVq FVq)
                → (BVp≠BVq : distinct BVp BVq)
                → (FVp≠BVq : distinct FVp BVq)
                → (BVp≠FVq : distinct BVp FVq)
                → (Xp≠Xq : distinct' (Xs FVp) (Xs FVq))
                → CorrectBinding (p ∥ q) (BVp U̬ BVq) (FVp U̬ FVq)
  CBloop    : ∀{p BV FV}
               → CorrectBinding p BV FV
               → (BV≠FV : distinct BV FV)
               → CorrectBinding (loop p) BV FV
  CBloopˢ   : ∀{p q BVp FVp BVq FVq}
               → CorrectBinding p BVp FVp
               → CorrectBinding q BVq FVq
               → (BVp≠FVq : distinct BVp FVq)
               → (BVq≠FVq : distinct BVq FVq)
               → CorrectBinding (loopˢ p q) (BVp U̬ BVq) (FVp U̬ FVq)
  CBseq     : ∀{p q BVp BVq FVp FVq}
                → (cbp : CorrectBinding p BVp FVp)
                → (cbq : CorrectBinding q BVq FVq)
                → (BVp≠FVq : distinct BVp FVq)
                → CorrectBinding (p >> q) (BVp U̬ BVq) (FVp U̬ FVq)
  CBsusp    : ∀{S p BV FV}
                → (cbp : CorrectBinding p BV FV)
                → ([S]≠BVp : distinct' [ (Sunwrap S) ] (Ss BV))
                → CorrectBinding (suspend p S) BV (+S S FV)
  CBexit    : ∀{n} → CorrectBinding (exit n) base base
  CBtrap    : ∀{p BV FV} → CorrectBinding p BV FV → CorrectBinding (trap p) BV FV
  CBshared  : ∀{s e p BV FV} → CorrectBinding p BV FV
                             → CorrectBinding (shared s ≔ e in: p)
                                              (+s s BV) ((FVₑ e) U̬ (FV |̌ (+s s base)))
  CBsset    : ∀{s e} → CorrectBinding (s ⇐ e) base (+s s (FVₑ e))
  CBvar     : ∀{x e p BV FV} → CorrectBinding p BV FV
                             → CorrectBinding (var x ≔ e in: p)
                                              (+x x BV) ((FVₑ e) U̬ (FV |̌ (+x x base)))
  CBvset    : ∀{x e} → CorrectBinding (x ≔ e) base (+x x (FVₑ e))
  CBif      : ∀{x p q BVp BVq FVp FVq}
              → (cbp : CorrectBinding p BVp FVp)
              → (cbq : CorrectBinding q BVq FVq)
              → CorrectBinding (if x ∣⇒ p ∣⇒ q) (BVp U̬ BVq) (+x x (FVp U̬ FVq))
  CBρ       : ∀{θ A p BV FV} → CorrectBinding p BV FV
                             → CorrectBinding (ρ⟨ θ , A ⟩· p) (((Dom θ) U̬ BV)) (FV |̌ (Dom θ))

binding-is-function : ∀{p BV₁ FV₁ BV₂ FV₂} →
  CorrectBinding p BV₁ FV₁ →
  CorrectBinding p BV₂ FV₂ →
  BV₁ ≡ BV₂ × FV₁ ≡ FV₂
binding-is-function CBnothing CBnothing = refl , refl
binding-is-function CBpause CBpause = refl , refl
binding-is-function (CBsig cb₁) (CBsig cb₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function (CBpresent cbp₁ cbq₁) (CBpresent cbp₂ cbq₂)
  with binding-is-function cbp₁ cbp₂ | binding-is-function cbq₁ cbq₂
... | (refl , refl) | (refl , refl) = refl , refl
binding-is-function CBemit CBemit = refl , refl
binding-is-function (CBpar cbp₁ cbq₁ BVp≠BVq₁ FVp≠BVq₁ BVp≠FVq₁ Xp≠Xq₁)
                    (CBpar cbp₂ cbq₂ BVp≠BVq₂ FVp≠BVq₂ BVp≠FVq₂ Xp≠Xq₂)
  with binding-is-function cbp₁ cbp₂ | binding-is-function cbq₁ cbq₂
... | (refl , refl) | (refl , refl) = refl , refl
binding-is-function (CBloop cb₁ BV≠FV₁)
                    (CBloop cb₂ BV≠FVV₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function (CBloopˢ cbp₁ cbq₁ BVp≠FVq₁ BVq≠FVq₁)
                    (CBloopˢ cbp₂ cbq₂ BVp≠FVq₂ BVq≠FVq₂)
  with binding-is-function cbp₁ cbp₂ | binding-is-function cbq₁ cbq₂
... | (refl , refl) | (refl , refl) = refl , refl
binding-is-function (CBseq cbp₁ cbq₁ BV≠FV₁) (CBseq cbp₂ cbq₂ BV≠FV₂)
  with binding-is-function cbp₁ cbp₂ | binding-is-function cbq₁ cbq₂
... | (refl , refl) | (refl , refl) = refl , refl
binding-is-function (CBsusp cb₁ S∉BV₁) (CBsusp cb₂ S∉BV₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function CBexit CBexit = refl , refl
binding-is-function (CBtrap cb₁) (CBtrap cb₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function (CBshared cb₁) (CBshared cb₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function CBsset CBsset = refl , refl
binding-is-function (CBvar cb₁) (CBvar cb₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl
binding-is-function CBvset CBvset = refl , refl
binding-is-function (CBif cbp₁ cbq₁) (CBif cbp₂ cbq₂)
  with binding-is-function cbp₁ cbp₂ | binding-is-function cbq₁ cbq₂
... | (refl , refl) | (refl , refl) = refl , refl
binding-is-function (CBρ cb₁) (CBρ cb₂)
  with binding-is-function cb₁ cb₂
... | (refl , refl) = refl , refl

binding-dec : ∀ p → Dec (∃ \ BV -> ∃ \ FV -> CorrectBinding p BV FV)

binding-dec nothin = yes (base , base , CBnothing)

binding-dec pause = yes (base , base , CBpause)

binding-dec (signl S p) with binding-dec p
binding-dec (signl S p) | yes (BV , FV , CBp) =
  yes (+S S BV , (FV |̌ (+S S base)) , CBsig CBp)
binding-dec (signl S p) | no ¬p = no (\ { (BV , FV , CBsig proj₃) → ¬p (_ , _ , proj₃) })

binding-dec (present S ∣⇒ p ∣⇒ q) with binding-dec p
binding-dec (present S ∣⇒ p ∣⇒ q) | yes p₂ with binding-dec q
binding-dec (present S ∣⇒ p ∣⇒ q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) =
  yes (BVp U̬ BVq , +S S (FVp U̬ FVq) , CBpresent CBp CBq)
binding-dec (present S ∣⇒ p ∣⇒ p₁) | yes p₂ | (no ¬p) =
  no (\ { (BV , FV , CBpresent BD BD₁) → ¬p (_ , _ , BD₁) } )
binding-dec (present S ∣⇒ p ∣⇒ p₁) | no ¬p =
  no (\ { (BV , FV , CBpresent BD BD₁) → ¬p (_ , _ , BD) } )

binding-dec (emit S) = yes (base , (Sunwrap S ∷ [] , [] , []) , CBemit)

binding-dec (p ∥ q) with binding-dec p
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) with binding-dec q
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) with distinct-dec BVp BVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | yes BVp≠BVq  = no ¬CB
 where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (p ∥ q) BV FV)
   ¬CB (BV₂ , FV₂ , CBpar CBp₂ CBq₂ BVp≠BVq' FVp≠BVq' BVp≠FVq' Xp≠Xq') with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
   ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec BVp≠BVq' BVp≠BVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | no ¬BVp≠BVq with distinct-dec FVp BVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (yes FVp≠BVq) = no ¬CB
 where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (p ∥ q) BV FV)
   ¬CB (BV₂ , FV₂ , CBpar CBp₂ CBq₂ BVp≠BVq' FVp≠BVq' BVp≠FVq' Xp≠Xq') with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
   ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec FVp≠BVq' FVp≠BVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (no ¬FVp≠BVq) with distinct-dec BVp FVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (no ¬FVp≠BVq) | (yes BVp≠FVq) = no ¬CB
 where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (p ∥ q) BV FV)
   ¬CB (BV₂ , FV₂ , CBpar CBp₂ CBq₂ BVp≠BVq' FVp≠BVq' BVp≠FVq' Xp≠Xq') with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
   ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec BVp≠FVq' BVp≠FVq
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (no ¬FVp≠BVq) | (no ¬BVp≠FVq) with distinct'-dec (Xs FVp) (Xs FVq)
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (no ¬FVp≠BVq) | (no ¬BVp≠FVq) | (yes Xp≠Xq) = no ¬CB
 where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (p ∥ q) BV FV)
   ¬CB (BV₂ , FV₂ , CBpar CBp₂ CBq₂ BVp≠BVq' FVp≠BVq' BVp≠FVq' Xp≠Xq') with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
   ... | ((refl , refl) , (refl , refl)) = Xp≠Xq' (proj₁ Xp≠Xq) (proj₁ (proj₂ Xp≠Xq)) (proj₂ (proj₂ Xp≠Xq))
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (no ¬BVp≠BVq) | (no ¬FVp≠BVq) | (no ¬BVp≠FVq) | (no ¬Xp≠Xq) =
  yes (BVp U̬ BVq , FVp U̬ FVq , CBpar CBp CBq (distinct-dec-is-distinct  ¬BVp≠BVq)
                                           (distinct-dec-is-distinct  ¬FVp≠BVq)
                                           (distinct-dec-is-distinct  ¬BVp≠FVq)
                                           (λ z z∈xs z∈ys → ¬Xp≠Xq (z , z∈xs , z∈ys)))
binding-dec (p ∥ q) | yes (BVp , FVp , CBp) | no ¬p =
  no (\ { (BV , FV , CBpar X X₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) → ¬p (_ , _ , X₁ ) } )
binding-dec (p ∥ q) | no ¬p =
  no (\ { (BV , FV , CBpar X X₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) → ¬p (_ , _ , X) } )

binding-dec (loop p) with binding-dec p
binding-dec (loop p) | yes (BV , FV , CB) with distinct-dec BV FV
binding-dec (loop p) | yes (BV , FV , CB) | yes dec = no ¬CB
  where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (loop p) BV FV)
   ¬CB (BV₂ , FV₂ , CBloop CB₂  BV≠FV') with binding-is-function CB CB₂
   ... | (refl , refl) = distinct-not-distinct-dec BV≠FV' dec
binding-dec (loop p) | yes (BV , FV , CB) | no dec = yes (BV , (FV , (CBloop CB (distinct-dec-is-distinct dec))))
binding-dec (loop p) | no ¬p =
  no (\ { (BV , FV , CBloop CB BV≠FV) -> ¬p (_ , _ , CB) } )

binding-dec (loopˢ p q) with binding-dec p
binding-dec (loopˢ p q) | yes (BVp , FVq , CBp ) with binding-dec q
binding-dec (loopˢ p q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) with distinct-dec BVp FVq
binding-dec (loopˢ p q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | yes BVp≠FVq = no ¬CB
 where
  ¬CB :  ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (loopˢ p q) BV FV)
  ¬CB (BV₂ , FV₂ , CBloopˢ CBp₂ CBq₂ BVp≠FVq₂ BVq≠FVq₂) with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
  ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec BVp≠FVq₂ BVp≠FVq
binding-dec (loopˢ p q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | no ¬BVp≠FVq with distinct-dec BVq FVq
binding-dec (loopˢ p q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | no ¬BVp≠FVq | yes ¬BVq≠FVq = no ¬CB where
  ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (loopˢ p q) BV FV)
  ¬CB (BV₂ , FV₂ , CBloopˢ CBp₂ CBq₂ BVp≠FVq₂ BVq≠FVq₂)  with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
  ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec BVq≠FVq₂ ¬BVq≠FVq
binding-dec (loopˢ p q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | no BVp≠FVq | no BVq≠FVq =
   yes (BVp U̬ BVq , FVp U̬ FVq , CBloopˢ CBp CBq (distinct-dec-is-distinct BVp≠FVq) (distinct-dec-is-distinct BVq≠FVq))
binding-dec (loopˢ p q) | yes (BVp , FVq , CBp) | (no ¬CBq) =
  no (\ { (BV , FV , CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) -> ¬CBq (_ , _ , CBq) } )
binding-dec (loopˢ p q) | no ¬CBp =
  no (\ { (BV , FV , CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) -> ¬CBp (_ , _ , CBp) })

binding-dec (p >> q) with binding-dec p
binding-dec (p >> q) | yes (BVp , FVq , CBp ) with binding-dec q
binding-dec (p >> q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) with distinct-dec BVp FVq
binding-dec (p >> q) | yes (BVp , FVp , CBp) | (yes (BVq , FVq , CBq)) | (yes BVp≠FVq) = no ¬CB
 where
  ¬CB :  ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (p >> q) BV FV)
  ¬CB (BV₂ , FV₂ , CBseq CBp₂ CBq₂ BVp≠FVq') with (binding-is-function CBp CBp₂ , binding-is-function CBq CBq₂)
  ... | ((refl , refl) , (refl , refl)) = distinct-not-distinct-dec BVp≠FVq' BVp≠FVq
binding-dec (p >> q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) | no ¬BVp≠FVq =
  yes  (BVp U̬ BVq , FVp U̬ FVq , CBseq CBp CBq (distinct-dec-is-distinct ¬BVp≠FVq))
binding-dec (p >> q) | yes (BVp , FVq , CBp) | (no ¬CBq) =
  no (\ { (BV , FV , CBseq CBp CBq BVp≠FVq) -> ¬CBq (_ , _ , CBq) } )
binding-dec (p >> q) | no ¬CBp =
  no (\ { (BV , FV , CBseq CBp CBq BVp≠FVq) -> ¬CBp (_ , _ , CBp) })

binding-dec (suspend p S) with binding-dec p
binding-dec (suspend p S) | yes (BV , FV , CB) with distinct'-dec [ (Sunwrap S) ] (Ss BV)
binding-dec (suspend p S) | yes (BV₁ , FV₁ , CB₁) | yes ([S]≠BVp₁ , [S]≠BVp₂ , [S]≠BVp₃) = no ¬CB
 where
   ¬CB : ¬ (∃ \ BV -> ∃ \ FV -> CorrectBinding (suspend p S) BV FV)
   ¬CB (BV₂ , FV₂ , CBsusp CB₃ [S]≠BVp') with (binding-is-function CB₁ CB₃)
   ... | refl , refl = [S]≠BVp' [S]≠BVp₁ [S]≠BVp₂ [S]≠BVp₃
binding-dec (suspend p S) | yes (BV , FV , CB) | (no ¬[S]≠BVp) =
  yes (BV , +S S FV , CBsusp CB (λ z z∈xs z∈ys → ¬[S]≠BVp (z , z∈xs , z∈ys)))
binding-dec (suspend p S) | no ¬p =
  no (\ { (BV , FV , CBsusp CB [S]≠BVp) -> ¬p (_ , _ , CB)})

binding-dec (trap p) with binding-dec p
binding-dec (trap p) | yes (BV , FV , CB) = yes (BV , FV , CBtrap CB)
binding-dec (trap p) | no ¬p =
  no (\ { (BV , FV , CBtrap CB ) -> ¬p (BV , FV , CB) })

binding-dec (exit x) = yes (base , base , CBexit)

binding-dec (shared s ≔ e in: p) with binding-dec p
binding-dec (shared s ≔ e in: p) | yes (BV , FV , CB) =
  yes (+s s BV , (FVₑ e) U̬ (FV |̌ (+s s base)) , CBshared CB)
binding-dec (shared s ≔ e in: p) | no ¬p =
  no (\ { (BV , FV , CBshared CB) -> ¬p (_ , _ , CB) })

binding-dec (s ⇐ e) = yes (base , +s s (FVₑ e) , CBsset)

binding-dec (var x ≔ e in: p) with binding-dec p
binding-dec (var x ≔ e in: p) | yes (BV , FV , CB) =
  yes (+x x BV , (FVₑ e) U̬ (FV |̌ (+x x base)) , CBvar CB)
binding-dec (var x ≔ e in: p) | no ¬p =
  no (\ { (BV , FV , CBvar CB) -> ¬p (_ , _ , CB) } )

binding-dec (x ≔ e) = yes (base , (+x x (FVₑ e)) , CBvset)

binding-dec (if x ∣⇒ p ∣⇒ q) with binding-dec p
binding-dec (if x ∣⇒ p ∣⇒ q) | yes p₁ with binding-dec q
binding-dec (if x ∣⇒ p₁ ∣⇒ q) | yes (BVp , FVp , CBp) | yes (BVq , FVq , CBq) =
  yes (BVp U̬ BVq , +x x (FVp U̬ FVq) , CBif CBp CBq)
binding-dec (if x ∣⇒ p ∣⇒ q) | yes p₁ | (no ¬p) =
  no (\ { (BV , FV , CBif CBp CBq) -> ¬p (_ , _ , CBq) })
binding-dec (if x ∣⇒ p ∣⇒ q) | no ¬p =
  no (\ { (BV , FV , CBif CBp CBq) -> ¬p (_ , _ , CBp) })

binding-dec (ρ⟨ θ , A ⟩· p) with binding-dec p
binding-dec (ρ⟨ θ , A ⟩· p) | yes (BV , FV , BP) =
  yes (((Dom θ) U̬ BV)  , FV |̌ (Dom θ) , CBρ BP)
binding-dec (ρ⟨ θ , A ⟩· p) | no ¬p = no (\ { (BV , FV , CBρ p ) -> ¬p (_ , _ , p) } )

binding-extract : ∀{p BV FV p' E} →
  CorrectBinding p BV FV →
  p ≐ E ⟦ p' ⟧e →
  Σ (VarList × VarList) λ { (BV' , FV') → (BV' ⊆ BV × FV' ⊆ FV) × CorrectBinding p' BV' FV' }
binding-extract cb                      dehole =
  _ , (⊆-refl , ⊆-refl) , cb
binding-extract (CBpar cbp cbq _ _ _ _) (depar₁ p≐E⟦p'⟧)
  with binding-extract cbp p≐E⟦p'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (∪ˡ BV'⊆BV , ∪ˡ FV'⊆FV) , cb*
binding-extract {_} (CBpar {BVp = BVp} {FVp = FVp} cbp cbq _ _ _ _) (depar₂ q≐E⟦q'⟧)
  with binding-extract cbq q≐E⟦q'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (∪ʳ BVp BV'⊆BV , ∪ʳ FVp FV'⊆FV) , cb*
binding-extract (CBseq cbp cbq _)       (deseq p≐E⟦p'⟧)
  with binding-extract cbp p≐E⟦p'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (∪ˡ BV'⊆BV , ∪ˡ FV'⊆FV) , cb*
binding-extract (CBloopˢ cbp cbq _ _)   (deloopˢ p≐E⟦p'⟧)
  with binding-extract cbp p≐E⟦p'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (∪ˡ BV'⊆BV , ∪ˡ FV'⊆FV) , cb*
binding-extract (CBsusp {S = S} cb _)   (desuspend p≐E⟦p'⟧)
  with binding-extract cb  p≐E⟦p'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (BV'⊆BV , ∪ʳ (+S S base) FV'⊆FV) , cb*
binding-extract (CBtrap cb)             (detrap p≐E⟦p'⟧)
  with binding-extract cb  p≐E⟦p'⟧
... | (BV' , FV') , (BV'⊆BV , FV'⊆FV) , cb* = _ , (BV'⊆BV , FV'⊆FV) , cb*

binding-subst : ∀{p BVp FVp q BVq FVq r BVr FVr E} →
  CorrectBinding p BVp FVp →
  p ≐ E ⟦ q ⟧e →
  CorrectBinding q BVq FVq →
  BVr ⊆ BVq →
  FVr ⊆ FVq →
  CorrectBinding r BVr FVr →
  Σ (VarList × VarList) λ { (BV' , FV') → (BV' ⊆ BVp × FV' ⊆ FVp) × CorrectBinding (E ⟦ r ⟧e) BV' FV' }
binding-subst (CBpar {BVq = BVq'} {FVq = FVq'} cbp' cbq' BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq')
              (depar₁ p'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbp' p'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVp'' , FVp'') , (BVp''⊆BVp' , FVp''⊆FVp') , cbp'' =
  _ , (∪-respect-⊆-left BVp''⊆BVp' , ∪-respect-⊆-left FVp''⊆FVp') ,
  CBpar cbp'' cbq'
        (⊆-respect-distinct-left BVp''⊆BVp' BVp'≠BVq')
        (⊆-respect-distinct-left FVp''⊆FVp' FVp'≠BVq')
        (⊆-respect-distinct-left BVp''⊆BVp' BVp'≠FVq')
        (⊆¹-respect-distinct'-left (proj₂ (proj₂ FVp''⊆FVp')) Xp'≠Xq')
binding-subst (CBpar {BVp = BVp'} {FVp = FVp'} cbp' cbq' BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq')
              (depar₂ q'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbq' q'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVq'' , FVq'') , (BVq''⊆BVq' , FVq''⊆FVq') , cbq'' =
  _ , (∪-respect-⊆-right BVp' BVq''⊆BVq' , ∪-respect-⊆-right FVp' FVq''⊆FVq') ,
  CBpar cbp' cbq''
        (⊆-respect-distinct-right BVq''⊆BVq' BVp'≠BVq')
        (⊆-respect-distinct-right BVq''⊆BVq' FVp'≠BVq')
        (⊆-respect-distinct-right FVq''⊆FVq' BVp'≠FVq')
        (⊆¹-respect-distinct'-right (proj₂ (proj₂ FVq''⊆FVq')) Xp'≠Xq')
binding-subst (CBseq {BVq = BVq'} {FVq = FVq'} cbp' cbq' BV≠FV)
              (deseq p'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbp' p'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVp'' , FVp'') , (BVp''⊆BVp' , FVp''⊆FVp') , cbp'' =
  _ , (∪-respect-⊆-left BVp''⊆BVp' , ∪-respect-⊆-left FVp''⊆FVp') ,
  CBseq cbp'' cbq' (⊆-respect-distinct-left BVp''⊆BVp' BV≠FV)
binding-subst (CBloopˢ {BVq = BVq'} {FVq = FVq'} cbp' cbq' BVp≠FVq BVq≠FVq)
              (deloopˢ p'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbp' p'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVp'' , FVp'') , (BVp''⊆BVp' , FVp''⊆FVp') , cbp'' =
  _ , (∪-respect-⊆-left BVp''⊆BVp' , ∪-respect-⊆-left FVp''⊆FVp') ,
  CBloopˢ cbp'' cbq' (⊆-respect-distinct-left BVp''⊆BVp' BVp≠FVq) BVq≠FVq
binding-subst (CBsusp {S} {FV = FVp'} cbp' S∉BVp') (desuspend p'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbp' p'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVp'' , FVP'') , (BVp''⊆BVp' , FVp''⊆FVp') , cbp'' =
  _ , (BVp''⊆BVp' , (∪¹-respect-⊆¹-right [ Signal.unwrap S ] ,′ id ,′ id # FVp''⊆FVp')) ,
  CBsusp cbp'' (⊆¹-respect-distinct'-right (proj₁ BVp''⊆BVp') S∉BVp')
binding-subst (CBtrap cbp') (detrap p'≐E⟦q⟧) cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-subst cbp' p'≐E⟦q⟧ cbq BVr⊆BVq FVr⊆FVq cbr
... | (BVp'' , FVp'') , ⟨BVp''⊆BVp'⟩×⟨FVp''⊆FVp'⟩ , cbp'' =
  _ , ⟨BVp''⊆BVp'⟩×⟨FVp''⊆FVp'⟩ , CBtrap cbp''
binding-subst cbp dehole cbq BVr⊆BVq FVr⊆FVq cbr
  with binding-is-function cbp cbq
... | (refl , refl) = _ , (BVr⊆BVq , FVr⊆FVq) , cbr

binding-extractc' : ∀{p BV FV p' C} →
  CorrectBinding p BV FV →
  p ≐ C ⟦ p' ⟧c →
  Σ (VarList × VarList) λ { (BV' , FV') → CorrectBinding p' BV' FV' }
binding-extractc' cbp dchole =
  _ , cbp
binding-extractc' (CBsig cbp) (dcsignl p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBpresent cbp cbp₁) (dcpresent₁ p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBpresent cbp cbp₁) (dcpresent₂ p≐C⟦p'⟧) =
  binding-extractc' cbp₁ p≐C⟦p'⟧
binding-extractc' (CBpar cbp cbp₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (dcpar₁ p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBpar cbp cbp₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) (dcpar₂ p≐C⟦p'⟧) =
  binding-extractc' cbp₁ p≐C⟦p'⟧
binding-extractc' (CBloop cbp BV≠FV) (dcloop p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) (dcloopˢ₁ p≐C⟦p'⟧) =
  binding-extractc' CBp p≐C⟦p'⟧
binding-extractc' (CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) (dcloopˢ₂ q≐C⟦q'⟧) =
  binding-extractc' CBq q≐C⟦q'⟧
binding-extractc' (CBseq cbp cbp₁ BVp≠FVq) (dcseq₁ p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBseq cbp cbp₁ BVp≠FVq) (dcseq₂ p≐C⟦p'⟧) =
  binding-extractc' cbp₁ p≐C⟦p'⟧
binding-extractc' (CBsusp cbp [S]≠BVp) (dcsuspend p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBtrap cbp) (dctrap p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBshared cbp) (dcshared p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBvar cbp) (dcvar p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBif cbp cbp₁) (dcif₁ p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧
binding-extractc' (CBif cbp cbp₁) (dcif₂ p≐C⟦p'⟧) =
  binding-extractc' cbp₁ p≐C⟦p'⟧
binding-extractc' (CBρ cbp) (dcenv p≐C⟦p'⟧) =
  binding-extractc' cbp p≐C⟦p'⟧

binding-substc' : ∀{p BVp FVp q BVq FVq r BVr FVr C} →
  CorrectBinding p BVp FVp →
  p ≐ C ⟦ q ⟧c →
  CorrectBinding q BVq FVq →
  BVr ⊆ BVq →
  FVr ⊆ FVq →
  CorrectBinding r BVr FVr →
  Σ (VarList × VarList) λ { (BV' , FV') → (BV' ⊆ BVp × FV' ⊆ FVp) × CorrectBinding (C ⟦ r ⟧c) BV' FV' }
binding-substc' CBp dchole CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-is-function CBp CBq
... | refl , refl = _ , (BVr⊆BVq , FVr⊆FVq) , CBr

binding-substc' (CBpar  cbp cbp₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq)
                (dcpar₁ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-left bvsub , ∪-respect-⊆-left fvsub) ,
  CBpar  cb1 cbp₁ (⊆-respect-distinct-left bvsub BVp≠BVq)
                  (⊆-respect-distinct-left fvsub FVp≠BVq)
                  (⊆-respect-distinct-left bvsub BVp≠FVq)
                  (⊆¹-respect-distinct'-left (thd fvsub) Xp≠Xq)

binding-substc' (CBpar{BVp = BVp}{FVp = FVp} cbp cbp₁ BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq)
                (dcpar₂ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp₁ dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub ,  fvsub) , cb1 =
  _ , (∪-respect-⊆-right BVp bvsub , ∪-respect-⊆-right FVp fvsub) ,
  CBpar cbp cb1 (⊆-respect-distinct-right bvsub BVp≠BVq)
                (⊆-respect-distinct-right bvsub FVp≠BVq)
                (⊆-respect-distinct-right fvsub BVp≠FVq)
                (⊆¹-respect-distinct'-right (thd fvsub) Xp≠Xq)

binding-substc' (CBseq cbp cbp₁ BVp≠FVq)
                (dcseq₁ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-left bvsub , ∪-respect-⊆-left fvsub) ,
  CBseq cb1 cbp₁ (⊆-respect-distinct-left bvsub BVp≠FVq)

binding-substc' (CBseq{BVp = BVp}{FVp = FVp} cbp cbp₁ BVp≠FVq)
                (dcseq₂ dc) CBq BVr⊆BVq FVr⊆FVq CBr
   with  binding-substc' cbp₁ dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
   _ , (∪-respect-⊆-right BVp bvsub , ∪-respect-⊆-right FVp fvsub) ,
   CBseq cbp cb1 (⊆-respect-distinct-right fvsub  BVp≠FVq)

binding-substc' (CBsusp{S = S} cbp [S]≠BVp)
                (dcsuspend dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
   _ ,  (bvsub , ((∷-respect-⊆¹ (Signal.unwrap S)) , id , id # fvsub)) ,
   CBsusp cb1 (⊆¹-respect-distinct'-right (fst bvsub) [S]≠BVp)

binding-substc' (CBtrap CBp) (dctrap dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' CBp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (bvsub , fvsub) , CBtrap cb1

binding-substc' (CBsig{S = S ₛ} cbp) (dcsignl dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (((∷-respect-⊆¹ S) , id , id # bvsub) ,
       ⊆-respect-|̌ (+S (S ₛ) base) fvsub),
  CBsig cb1

binding-substc' (CBpresent{S = S ₛ} cbp cbp₁)
                (dcpresent₁ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-left bvsub ,
       ((∷-respect-⊆¹ S) , id , id # (∪-respect-⊆-left fvsub))) ,
  CBpresent cb1 cbp₁

binding-substc' (CBpresent{S = S ₛ}{BVp = BVp}{FVp = FVp} cbp cbp₁)
                (dcpresent₂ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp₁ dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-right BVp bvsub ,
       ((∷-respect-⊆¹ S) , id , id # (∪-respect-⊆-right FVp fvsub))) ,
  CBpresent cbp cb1

binding-substc' (CBloop cbp BV≠FV)
                (dcloop dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-right base bvsub , fvsub) ,
  CBloop cb1 (⊆-respect-distinct-left bvsub
              (⊆-respect-distinct-right fvsub BV≠FV))

binding-substc' (CBloopˢ cbp cbp₁ BVp≠FVq BVq≠FVq)
                (dcloopˢ₁ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-left bvsub , ∪-respect-⊆-left fvsub) ,
  CBloopˢ cb1 cbp₁ (⊆-respect-distinct-left bvsub BVp≠FVq) BVq≠FVq

binding-substc' (CBloopˢ{BVp = BVp}{FVp = FVp} cbp cbp₁ BVp≠FVq BVq≠FVq)
                (dcloopˢ₂ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp₁ dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-right BVp bvsub , ∪-respect-⊆-right FVp fvsub) ,
  CBloopˢ cbp cb1 (⊆-respect-distinct-right fvsub  BVp≠FVq)
                  (⊆-respect-distinct-left bvsub
                   (⊆-respect-distinct-right fvsub BVq≠FVq))

binding-substc' (CBshared{s = s}{e = e} cbp)
                (dcshared dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
 _ , (((id , (∷-respect-⊆¹ (SharedVar.unwrap s)) , id # bvsub)) ,
      ∪-respect-⊆-right (FVₑ e) (⊆-respect-|̌ (+s s base) fvsub)) ,
 CBshared cb1

binding-substc' (CBvar{x = x}{e = e} cbp) (dcvar dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (((id , id , (∷-respect-⊆¹ (SeqVar.unwrap x)) # bvsub)) ,
        ∪-respect-⊆-right (FVₑ e) (⊆-respect-|̌ (+x x base) fvsub)) ,
  CBvar cb1

binding-substc' (CBif{x = x ᵥ} cbp cbp₁) (dcif₁ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-left bvsub , (id , id , (∷-respect-⊆¹ x) # (∪-respect-⊆-left fvsub))) ,
  CBif cb1 cbp₁

binding-substc' (CBif{x = x ᵥ}{BVp = BVp}{FVp = FVp} cbp cbp₁)
                (dcif₂ dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp₁ dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
  _ , (∪-respect-⊆-right BVp bvsub ,
       (id , id , (∷-respect-⊆¹ x) # (∪-respect-⊆-right FVp fvsub))) ,
  CBif cbp cb1

binding-substc' (CBρ{θ = θ} cbp) (dcenv dc) CBq BVr⊆BVq FVr⊆FVq CBr
  with binding-substc' cbp dc CBq BVr⊆BVq FVr⊆FVq CBr
... | _ , (bvsub , fvsub) , cb1 =
 _ , (∪-respect-⊆-right (Dom θ) bvsub , ⊆-respect-|̌ (Dom θ) fvsub) ,
 CBρ cb1

-- In the decomposition E ⟦ p ⟧e, the bound variables in p and the free
-- variables in E must be disjoint.
distinct-term-context-help : ∀ {BV FV BVp FVp BVnothin FVnothin} p E →
  CorrectBinding (E ⟦ p ⟧e) BV FV →
  CorrectBinding p BVp FVp →
  (BVp ⊆ BV) →
  CorrectBinding (E ⟦ nothin ⟧e) BVnothin FVnothin →
  distinct BVp FVnothin
distinct-term-context-help p [] cb cbp BVp⊆BV CBnothing =
  (λ _ _ ()) ,′ (λ _ _ ()) ,′ (λ _ _ ())
distinct-term-context-help p (epar₁ q ∷ E)
  (CBpar cbp' cbq' BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq') cbp BVp⊆BV
  (CBpar cbnothinp cbnothinq BVp≠BVq₁ FVp≠BVq₁ BVp≠FVq₁ Xp≠Xq₁)
  with binding-extract cbp' (((E ⟦ p ⟧e) ≐ E ⟦ p ⟧e) ∋ plug refl)
... | (BV' , FV') , (BV'⊆BVE⟦p⟧ , FV'⊆FVE⟦p⟧) , cbp*
  with binding-is-function cbp cbp* | binding-is-function cbq' cbnothinq
... | refl , refl | refl , refl =
  distinct-union-right
    (distinct-term-context-help p E cbp' cbp BV'⊆BVE⟦p⟧ cbnothinp)
    (⊆-respect-distinct-left BV'⊆BVE⟦p⟧ BVp'≠FVq')
distinct-term-context-help p (epar₂ p₁ ∷ E)
  (CBpar cbp' cbq' BVp'≠BVq' FVp'≠BVq' BVp'≠FVq' Xp'≠Xq') cbp BVp⊆BV
  (CBpar {FVq = FVnothinq} cbnothinp cbnothinq BVp≠BVq₁ FVp≠BVq₁ BVp≠FVq₁ Xp≠Xq₁)
  with binding-extract cbq' (((E ⟦ p ⟧e) ≐ E ⟦ p ⟧e) ∋ plug refl)
... | (BV' , FV') , (BV'⊆BVE⟦p⟧ , FV'⊆FVE⟦p⟧) , cbp*
  with binding-is-function cbp cbp* | binding-is-function cbp' cbnothinp
... | refl , refl | refl , refl =
  ⊆-respect-distinct-right
    (∪-comm-⊆-right FVnothinq ⊆-refl)
    (distinct-union-right
      (distinct-term-context-help p E cbq' cbp BV'⊆BVE⟦p⟧ cbnothinq)
      (⊆-respect-distinct-left BV'⊆BVE⟦p⟧ (distinct-sym FVp'≠BVq')))

distinct-term-context-help p (eseq q ∷ E)
  (CBseq {BVp = BVE⟦p⟧p} {FVp = FVE⟦p⟧p} cbp' cbq' BVp'≠FVq') cbp BVp⊆BV
  (CBseq {BVp = BVnothinp} {BVq = BVnothinq} {FVp = FVnothinp} {FVq = FVnothinq}
         cbnothinp cbnothinq BVp≠FVq)
  with binding-extract cbp' (((E ⟦ p ⟧e) ≐ E ⟦ p ⟧e) ∋ plug refl)
... | (BV' , FV') , (BV'⊆BVE⟦p⟧ , FV'⊆FVE⟦p⟧) , cbp*
  with binding-is-function cbp cbp* | binding-is-function cbq' cbnothinq
... | refl , refl | refl , refl =
  distinct-union-right
    (distinct-term-context-help p E cbp' cbp BV'⊆BVE⟦p⟧ cbnothinp)
    (⊆-respect-distinct-left
     BV'⊆BVE⟦p⟧
     (distinct-sym (dist++ˡ (distinct-sym (distinct-union-left BVp'≠FVq' BVp≠FVq)))))

distinct-term-context-help p (eloopˢ q ∷ E)
  (CBloopˢ {BVp = BVE⟦p⟧p} {FVp = FVE⟦p⟧p} cbp' cbq' BVp'≠FVq' BVq'≠FVq') cbp BVp⊆BV
  (CBloopˢ {BVp = BVnothinp} {FVp = FVnothinp} {BVq = BVnothinq} {FVq = FVnothinq}
           cbnothinp cbnothinq BVp≠FVq BVq≠FVq)
  with binding-extract cbp' (((E ⟦ p ⟧e) ≐ E ⟦ p ⟧e) ∋ plug refl)
... | (BV' , FV') , (BV'⊆BVE⟦p⟧ , FV'⊆FVE⟦p⟧) , cbp*
  with binding-is-function cbp cbp* | binding-is-function cbq' cbnothinq
... | refl , refl | refl , refl =
   distinct-union-right
    (distinct-term-context-help p E cbp' cbp BV'⊆BVE⟦p⟧ cbnothinp)
    (⊆-respect-distinct-left
     BV'⊆BVE⟦p⟧
     (distinct-sym (dist++ˡ (distinct-sym (distinct-union-left BVp'≠FVq' BVp≠FVq)))))

distinct-term-context-help {BVp = BVp} p (esuspend S ∷ E)
  (CBsusp cb [S]≠BVp) cbp BVp⊆BV
  (CBsusp {FV = FV} cbnothin [S]≠BVp₁) = BVp≠S∷FV ,′ id ,′ id # dist
  where dist = distinct-term-context-help p E cb cbp BVp⊆BV cbnothin
        BVp≠S∷FV : (typeof (proj₁ dist)) → ∀ S' → S' ∈ (proj₁ BVp) → S' ∈ (Signal.unwrap S ∷ proj₁ FV) → ⊥
        BVp≠S∷FV BVp≠FV S' S'∈BVp (here refl) = [S]≠BVp S' (here refl) (proj₁ BVp⊆BV S' S'∈BVp)
        BVp≠S∷FV BVp≠FV S' S'∈BVp (there S'∈FV) = BVp≠FV S' S'∈BVp S'∈FV
distinct-term-context-help p (etrap ∷ E)
  (CBtrap cb) cbp BVp⊆BV
  (CBtrap cbnothin) =
  distinct-term-context-help p E cb cbp BVp⊆BV cbnothin

BVars : ∀ (p : Term) -> VarList
BVars nothin = base
BVars pause = base
BVars (signl S p) = +S S (BVars p)
BVars (present S ∣⇒ p ∣⇒ q) = BVp U̬ BVq where
  BVp = BVars p
  BVq = BVars q
BVars (emit S) = base
BVars (p ∥ q) = BVp U̬ BVq where
  BVp = BVars p
  BVq = BVars q
BVars (loop p) = BV where
  BV = BVars p
BVars (loopˢ p q) = BVp U̬ BVq where
  BVp = BVars p
  BVq = BVars q
BVars (p >> q) = BVp U̬ BVq where
  BVp = BVars p
  BVq = BVars q
BVars (suspend p S) = BVars p
BVars (trap p) = BVars p
BVars (exit x) = base
BVars (shared s ≔ e in: p) = +s s (BVars p)
BVars (s ⇐ e) = base
BVars (var x ≔ e in: p) =  +x x (BVars p)
BVars (x ≔ e) = base
BVars (if x ∣⇒ p ∣⇒ q) =  BVp U̬ BVq where
  BVp = BVars p
  BVq = BVars q
BVars (ρ⟨ θ , A ⟩· p) = (Dom θ) U̬ BV where
  BV = BVars p

FVars : ∀ (p : Term) -> VarList
FVars nothin = base
FVars pause = base
FVars (signl S p) =  FV |̌ (+S S base) where
  FV = FVars p
FVars (present S ∣⇒ p ∣⇒ q) =  +S S (FVp U̬ FVq) where
  FVp = FVars p
  FVq = FVars q
FVars (emit S) =  +S S base
FVars (p ∥ q) = FVp U̬ FVq where
  FVp = FVars p
  FVq = FVars q
FVars (loop p) = FVars p
FVars (loopˢ p q) = FVp U̬ FVq where
  FVp = FVars p
  FVq = FVars q
FVars (p >> q) =  FVp U̬ FVq where
  FVp = FVars p
  FVq = FVars q
FVars (suspend p S) = +S S (FVars p)
FVars (trap p) = FVars p
FVars (exit x) = base
FVars (shared s ≔ e in: p) = (FVₑ e) U̬ (FV |̌ (+s s base)) where
  FV = FVars p
FVars (s ⇐ e) = +s s (FVₑ e) where
FVars (var x ≔ e in: p) = (FVₑ e) U̬ (FV |̌ (+x x base)) where
  FV = FVars p
FVars (x ≔ e) = +x x (FVₑ e)
FVars (if x ∣⇒ p ∣⇒ q) = +x x (FVp U̬ FVq) where
  FVp = FVars p
  FVq = FVars q
FVars (ρ⟨ θ , A ⟩· p) = FV |̌ (Dom θ) where
  FV = FVars p

CB : Term -> Set
CB p = CorrectBinding p (BVars p) (FVars p)

BVFVcorrect : ∀ p BV FV -> CorrectBinding p BV FV -> BVars p ≡ BV × FVars p ≡ FV
BVFVcorrect .nothin .([] , [] , []) .([] , [] , []) CBnothing = refl , refl
BVFVcorrect .pause .([] , [] , []) .([] , [] , []) CBpause = refl , refl
BVFVcorrect .(signl _ _) .(+S S BV) .(FV |̌ (+S S base))
            (CBsig{p}{S}{BV}{FV} CB) with BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(present _ ∣⇒ _ ∣⇒ _) .(BVp U̬ BVq) .(+S S (FVp U̬ FVq))
            (CBpresent{S}{p}{q}{BVp}{FVp}{BVq}{FVq} CBp CBq) with
            BVFVcorrect p BVp FVp CBp | BVFVcorrect q BVq FVq CBq
... | refl , refl | refl , refl = refl , refl
BVFVcorrect .(emit _) _ _ CBemit = refl , refl
BVFVcorrect .(_ ∥ _) .(BVp U̬ BVq) .(FVp U̬ FVq)
            (CBpar{p}{q}{BVp}{FVp}{BVq}{FVq} CBp CBq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) with
            BVFVcorrect p BVp FVp CBp | BVFVcorrect q BVq FVq CBq
... | refl , refl | refl , refl = refl , refl
BVFVcorrect .(loop _) .BV .FV
            (CBloop{p}{BV}{FV} CB BV≠FV) with
            BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(loopˢ _ _) .(BVp U̬ BVq) .(FVp U̬ FVq)
            (CBloopˢ{p}{q}{BVp}{FVp}{BVq}{FVq} CBp CBq BVp≠FVq BVq≠FVq) with
            BVFVcorrect p BVp FVp CBp | BVFVcorrect q BVq FVq CBq
... | refl , refl | refl , refl = refl , refl
BVFVcorrect .(_ >> _) .(BVp U̬ BVq) .(FVp U̬ FVq)
            (CBseq{p}{q}{BVp}{BVq}{FVp}{FVq} CBp CBq BVp≠FVq) with
            BVFVcorrect p BVp FVp CBp | BVFVcorrect q BVq FVq CBq
... | refl , refl | refl , refl = refl , refl
BVFVcorrect .(suspend _ _) .BV .(+S S FV)
            (CBsusp{S}{p}{BV}{FV} CB [S]≠BVp) with
            BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(trap _) .BV .FV (CBtrap{p}{BV}{FV} CB) with
             BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(exit _) .([] , [] , []) .([] , [] , []) CBexit = refl , refl
BVFVcorrect .(shared _ ≔ _ in: _) .(+s s BV) .((FVₑ e) U̬ (FV |̌ (+s s base)))
            (CBshared{s}{e}{p}{BV}{FV} CB) with
            BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(_ ⇐ _) .([] , [] , []) .(+s s (FVₑ e)) (CBsset{s}{e}) = refl , refl
BVFVcorrect .(var _ ≔ _ in: _) .(+x x BV) .((FVₑ e) U̬ (FV |̌ (+x x base)))
            (CBvar{x}{e}{p}{BV}{FV} CB) with
            BVFVcorrect p BV FV CB
... | refl , refl = refl , refl
BVFVcorrect .(_ ≔ _) .([] , [] , []) .(+x x (FVₑ e)) (CBvset{x}{e}) = refl , refl
BVFVcorrect .(if _ ∣⇒ _ ∣⇒ _) .(BVp U̬ BVq) .(+x x (FVp U̬ FVq))
            (CBif{x}{p}{q}{BVp}{BVq}{FVp}{FVq} CBp CBq) with
            BVFVcorrect p BVp FVp CBp | BVFVcorrect q BVq FVq CBq
... | refl , refl | refl , refl = refl , refl
BVFVcorrect .(ρ⟨ _ , _ ⟩· _) .(((Dom θ) U̬ BV)) .(FV |̌ (Dom θ))
            (CBρ{θ}{A}{p}{BV}{FV} CB) with BVFVcorrect p BV FV CB
... | refl , refl = refl , refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --prop --rewriting #-}

module Examples.Id where

open import Calf.CostMonoid
open import Calf.CostMonoids using (ℕ-CostMonoid)

costMonoid = ℕ-CostMonoid
open CostMonoid costMonoid

open import Calf costMonoid
open import Calf.Types.Nat
open import Calf.Types.Bounded costMonoid
open import Calf.Types.BigO costMonoid

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)

module Easy where
  id : cmp (Π nat λ _ → F nat)
  id n = ret n

  id/correct : ∀ n → ◯ (id n ≡ ret n)
  id/correct n u = refl

  id/cost : cmp (Π nat λ _ → cost)
  id/cost n = 0

  id≤id/cost : ∀ n → IsBounded nat (id n) (id/cost n)
  id≤id/cost n = bound/ret

  id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → 0)
  id/asymptotic = 0 ≤n⇒f[n]≤ 0 g[n]via λ n _ → id≤id/cost n

module Hard where
  id : cmp (Π nat λ _ → F nat)
  id zero = ret 0
  id (suc n) =
    step (F nat) 1 (
      bind (F nat) (id n) λ n' →
        ret (suc n')
    )

  id/correct : ∀ n → ◯ (id n ≡ ret n)
  id/correct zero    u = refl
  id/correct (suc n) u =
    begin
      id (suc n)
    ≡⟨⟩
      step (F nat) 1 (
        bind (F nat) (id n) λ n' →
          ret (suc n')
      )
    ≡⟨ step/ext (F nat) _ 1 u ⟩
      (bind (F nat) (id n) λ n' →
        ret (suc n'))
    ≡⟨ Eq.cong (λ e → bind (F nat) e _) (id/correct n u) ⟩
      ret (suc n)
    ∎
      where open ≡-Reasoning

  id/cost : cmp (Π nat λ _ → cost)
  id/cost zero    = 0
  id/cost (suc n) =
    1 + (
      bind cost (id n) λ n' → id/cost n +
        0
    )

  id/cost/closed : cmp (Π nat λ _ → cost)
  id/cost/closed n = n

  id/cost≤id/cost/closed : ∀ n → ◯ (id/cost n ≤ id/cost/closed n)
  id/cost≤id/cost/closed zero    u = ≤-refl
  id/cost≤id/cost/closed (suc n) u =
    begin
      id/cost (suc n)
    ≡⟨⟩
      1 + (
        bind cost (id n) λ n' → id/cost n +
          0
      )
    ≡⟨ Eq.cong (λ e → 1 + bind cost e λ n' → id/cost n + 0) (id/correct n u) ⟩
      1 + (id/cost n + 0)
    ≡⟨ Eq.cong suc (+-identityʳ _) ⟩
      1 + id/cost n
    ≤⟨ +-monoʳ-≤ 1 (id/cost≤id/cost/closed n u) ⟩
      1 + id/cost/closed n
    ≡⟨⟩
      suc n
    ≡⟨⟩
      id/cost/closed (suc n)
    ∎
      where open ≤-Reasoning

  id≤id/cost : ∀ n → IsBounded nat (id n) (id/cost n)
  id≤id/cost zero    = bound/ret
  id≤id/cost (suc n) =
    bound/step 1 _ (
      bound/bind (id/cost n) _ (id≤id/cost n) λ n →
        bound/ret
    )

  id≤id/cost/closed : ∀ n → IsBounded nat (id n) (id/cost/closed n)
  id≤id/cost/closed n = bound/relax (id/cost≤id/cost/closed n) (id≤id/cost n)

  id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → n)
  id/asymptotic = 0 ≤n⇒f[n]≤g[n]via λ n _ → id≤id/cost/closed n

easy≡hard : ◯ (Easy.id ≡ Hard.id)
easy≡hard u =
  funext λ n →
    begin
      Easy.id n
    ≡⟨ Easy.id/correct n u ⟩
      ret n
    ≡˘⟨ Hard.id/correct n u ⟩
      Hard.id n
    ∎
      where open ≡-Reasoning

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
-- Andreas, 2016-07-28 issue 2120, reported by guillaume

-- {-# OPTIONS -v tc.term.exlam:50 #-}

open import Common.Product

data Nat : Set where
  zero : Nat

data Eq {A : Set}(a : A) : A → Set where
  refl : Eq a a

postulate _<∣_ : ∀ {X Y : Set} → (X → Y) → X → Y

test : Nat
test = ( λ { (zero , refl) → zero } ) <∣ (zero , zero)

-- WAS: Internal error in Reduce

-- EXPECTED: Proper error, like
--
-- Type mismatch
-- when checking that the pattern refl has type _15 zero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module PathStructure.Empty where

open import Equivalence
open import Types

split-path : {x y : ⊥} → x ≡ y → ⊥
split-path = J (λ _ _ _ → ⊥) id _ _

merge-path : {x y : ⊥} → ⊥ → x ≡ y
merge-path = 0-elim

split-merge-eq : {x y : ⊥} → (x ≡ y) ≃ ⊥
split-merge-eq
  = split-path
  , (merge-path , λ b → 0-elim b)
  , (merge-path , J
      (λ _ _ p → merge-path (split-path p) ≡ p)
      (λ b → 0-elim b) _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module Interpreter where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Int using (pos)
open import Agda.Builtin.Unit using (⊤)

open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
open import FFI.Data.Aeson using (Value; eitherDecode)
open import FFI.Data.Either using (Left; Right)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Text.Encoding using (encodeUtf8)
open import FFI.System.Exit using (exitWith; ExitFailure)

open import Luau.Syntax using (Block)
open import Luau.Syntax.FromJSON using (blockFromJSON)
open import Luau.Syntax.ToString using (blockToString)
open import Luau.Run using (run; return; done; error)
open import Luau.RuntimeError.ToString using (errToStringᴮ)
open import Luau.Value.ToString using (valueToString)

runBlock : ∀ {a} → Block a → IO ⊤
runBlock block with run block
runBlock block | return V D = putStrLn (valueToString V)
runBlock block | done D = putStrLn "nil"
runBlock block | error E D = putStrLn (errToStringᴮ E)

runJSON : Value → IO ⊤
runJSON value with blockFromJSON(value)
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Right block) = runBlock block

runString : String → IO ⊤
runString txt with eitherDecode (encodeUtf8 txt)
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Right value) = runJSON value

main : IO ⊤
main = getContents >>= runString