(*
 * An encoding of "focused lambda-calculus" in Coq using higher-order
 * abstract syntax, done in "Church-style".  Generalized with both
 * positive and negative types.
 * Author: Noam Zeilberger
 *
 * See paper:
 *  "Focusing and Higher-order Abstract Syntax", POPL '08
 *  http://www.cs.cmu.edu/~noam/research/focusing-hoas.pdf
 *)

Set Implicit Arguments.

Require Import List.

Section Debruijn2.

  Variable A : Set.

  Definition frame := list A.
  Definition stack := list frame.

  Inductive InFrame (a : A) : frame -> Set :=
    | f0 : forall F, InFrame a (a :: F)
    | fS : forall F b, InFrame a F -> InFrame a (b :: F).

  Inductive InStack (a : A) : stack -> Set :=
    | s0 : forall S F, InFrame a F -> InStack a (F :: S)
    | sS : forall S F, InStack a S -> InStack a (F :: S).

End Debruijn2.

(* types *)
Parameter atom : Set.

Inductive pos : Set := 
  | One : pos
  | Times : pos -> pos -> pos
  | Zero : pos
  | Plus : pos -> pos -> pos
  | Nat : pos
  | PAtom : atom -> pos
  | Down : neg -> pos

with neg : Set :=
  | Top : neg
  | With : neg -> neg -> neg
  | Arrow : pos -> neg -> neg
  | Stream : neg -> neg
  | NAtom : atom -> neg
  | Up : pos -> neg.

(* hypotheses, conclusions and linear contexts *)
Inductive hyp : Set :=
  | PAtomH : atom -> hyp
  | NegH : neg -> hyp.
Inductive conc : Set :=
  | NAtomC : atom -> conc
  | PosC : pos -> conc.

Definition linctx := frame hyp.

Notation "[ X ]" := (X :: nil).

(* pattern typing, "Delta |= P" *)
Inductive patP : linctx -> pos -> Set :=
  | c_avar : forall X, patP [ PAtomH X ] (PAtom X)
  | c_nvar : forall N, patP [ NegH N ] (Down N)
  | c_unit : patP nil One
  | c_pair : forall Delta1 Delta2 P1 P2,
      patP Delta1 P1 -> patP Delta2 P2 ->
      patP (Delta1 ++ Delta2) (Times P1 P2)
  | c_in1 : forall Delta P1 P2,
      patP Delta P1 ->
      patP Delta (Plus P1 P2)
  | c_in2 : forall Delta P1 P2,
      patP Delta P2 ->
      patP Delta (Plus P1 P2)
  | c_z : patP nil Nat
  | c_s : forall Delta, patP Delta Nat -> patP Delta Nat.

(* destructor-pattern typing, "Delta ; N |= c" *)
Inductive patN : linctx -> neg -> conc -> Set :=
  | d_aid : forall X, patN nil (NAtom X) (NAtomC X)
  | d_pid : forall P, patN nil (Up P) (PosC P)
  | d_app : forall Delta1 Delta2 P N c,
      patP Delta1 P -> patN Delta2 N c ->
      patN (Delta1 ++ Delta2) (Arrow P N) c
  | d_pi1 : forall Delta N1 N2 c,
      patN Delta N1 c ->
      patN Delta (With N1 N2) c
  | d_pi2 : forall Delta N1 N2 c,
      patN Delta N2 c ->
      patN Delta (With N1 N2) c
  | d_hd : forall Delta N c,
      patN Delta N c ->
      patN Delta (Stream N) c
  | d_tl : forall Delta N c,
      patN Delta (Stream N) c ->
      patN Delta (Stream N) c.

(* Intuitionistic focusing judgments

  Translation key:
  rfoc Gamma P         "Gamma |- [P]" 
  linv Gamma c0 c       "Gamma ; c0 |- c"
  unfoc Gamma c         "Gamma |- c"
  rinv Gamma h         "Gamma |- h"
  lfoc Gamma N c       "Gamma ; [N] |- c"
  satctx Gamma Delta    "Gamma |- Delta"
*)

Definition intctx := stack hyp.

Inductive rfoc : intctx -> pos -> Set :=
  | ValP : forall Gamma P Delta,
      patP Delta P -> satctx Gamma Delta -> rfoc Gamma P

with linv : intctx -> conc -> conc -> Set :=
  | IdXN : forall Gamma X, linv Gamma (NAtomC X) (NAtomC X)
  | ConP : forall Gamma P c,
      (forall Delta, patP Delta P -> unfoc (Delta :: Gamma) c) -> 
      linv Gamma (PosC P) c

with unfoc : intctx -> conc -> Set :=
  | Ret : forall Gamma P, rfoc Gamma P -> unfoc Gamma (PosC P)
  | App : forall Gamma N c,
      InStack (NegH N) Gamma -> lfoc Gamma N c ->
      unfoc Gamma c

with lfoc : intctx -> neg -> conc -> Set :=
  | ConN : forall Gamma N c0 c Delta,
      patN Delta N c0 -> satctx Gamma Delta -> linv Gamma c0 c ->
      lfoc Gamma N c

with rinv : intctx -> hyp -> Set :=
  | ValN : forall Gamma N,
      (forall Delta c, patN Delta N c -> unfoc (Delta :: Gamma) c) -> 
      rinv Gamma (NegH N)
  | IdXP : forall Gamma X,
      InStack (PAtomH X) Gamma -> rinv Gamma (PAtomH X)

with satctx : intctx -> linctx -> Set :=
  | Sub : forall Gamma Delta,
      (forall h, InFrame h Delta -> InStack h Gamma -> rinv Gamma h) ->
      satctx Gamma Delta.