zippertypetheory.v

Global Set Primitive Projections.

Require Import Coq.Unicode.Utf8.
Require Coq.Lists.List.

Import List.ListNotations.

Variant zipper {A} := zip (Γ1: list A) (τ: A) (Γ2: list A).
Arguments zipper: clear implicits.

Inductive ix {A} {τ: A}: list A → Type :=
| O {Γ}: ix (τ :: Γ)
| S {Γ τ2}: ix Γ → ix (τ2 :: Γ)
.

Arguments ix {A}.

Inductive split {A}: list A → zipper A → Type :=
| XO {τ Γ}: split (τ :: Γ) (zip [] τ Γ)
| XS {Γ1 τ1 τ2 Γ2 Γ3}:
  split Γ3 (zip Γ1 τ2 Γ2) →
  split (τ1 :: Γ3) (zip (τ1 :: Γ1) τ2 Γ2)
.

Arguments split {A}.

Inductive value :=
| unit
| prod (τ1 τ2: value)
| U (σ: comp)
with comp :=
| F (τ: value)
| lpow (τ: value) (σ: comp)
| rpow (σ: comp) (τ: value)
.


Implicit Type τ: value.
Implicit Type σ: comp.
Implicit Type Γ: list value.
Implicit Type Δ: zipper value.

Infix "×" := prod (left associativity, at level 50).
Reserved Infix "⊢" (at level 90).
Reserved Infix "⊩" (at level 90).

Infix "\" := lpow (left associativity, at level 50).
Infix "/" := rpow.

Inductive data: list value → value → Set :=
| var {Γ τ}: ix τ Γ → Γ ⊢ τ

| tt {Γ}: Γ ⊢ unit
| fanout {Γ τ1 τ2}: Γ ⊢ τ1 → Γ ⊢ τ2 → Γ ⊢ τ1 × τ2
| π1 {Γ τ1 τ2}: Γ ⊢ τ1 × τ2 → Γ ⊢ τ1
| π2 {Γ τ1 τ2}: Γ ⊢ τ1 × τ2 → Γ ⊢ τ1

| thunk {Γ Δ σ}:
  split Γ Δ →
  Δ ⊩ σ →
  Γ ⊢ U σ
where "Γ ⊢ τ" := (data Γ τ)
with code: zipper value → comp → Set :=
| ret {Γ Δ τ2}:
  split Γ Δ →
  Γ ⊢ τ2 → Δ ⊩ F τ2
| force {Γ Δ σ}:
  split Γ Δ →
  Γ ⊢ U σ → Δ ⊩ σ

(* FIXME? not sure at all here *)
| to {Γ1 τ1 Γ2 τ2 σ}:
  zip Γ1 τ1 Γ2 ⊩ F τ2 →
  zip Γ1 τ2 Γ2 ⊩ σ →
  zip Γ1 τ1 Γ2 ⊩ σ

(* FIXME not sure at all here *)
| lapp {Γ Δ τ σ}:
  Δ ⊩ τ \ σ →
  split Γ Δ →
  Γ ⊢ τ →
  Δ ⊩ σ
| rapp {Γ Δ τ σ}:
  Δ ⊩ σ / τ →
  split Γ Δ →
  Γ ⊢ τ →
  Δ ⊩ σ

| L {Γ1 τ1 Γ2 τ2 σ}:
  zip (τ1 :: Γ1) τ2 Γ2 ⊩ σ →
  zip Γ1 τ2 Γ2 ⊩ τ1 \ σ
| R {Γ1 τ1 Γ2 τ2 σ}:
  zip Γ1 τ2 (τ1 :: Γ2) ⊩ σ →
  zip Γ1 τ2 Γ2 ⊩ σ / τ1
where "Γ ⊩ τ" := (code Γ τ)
.

Infix "#" := fanout (left associativity, at level 20).
Infix "TO" := to (at level 30).

Notation "!" := tt.