(*
 * An encoding of "focused lambda-calculus" in Coq using higher-order
 * abstract syntax, done in "Church-style".
 * Author: Noam Zeilberger
 *
 * 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 tp : Set := 
  | Atom : atom -> tp
  | One : tp
  | Times : tp -> tp -> tp
  | Zero : tp
  | Plus : tp -> tp -> tp
  | Arrow : tp -> tp -> tp
  | Nat : tp.

(* hypotheses and linear contexts *)
Inductive hyp : Set :=
  | AtomH : atom -> hyp
  | ArrowH : tp -> tp -> hyp.

Definition linctx := frame hyp.
  
(* linear entailment, "Delta ==> P" *)
Inductive lin_entail : linctx -> tp -> Set :=
  | p_avar : forall X, lin_entail (AtomH X :: nil) (Atom X)
  | p_fvar : forall P Q, lin_entail (ArrowH P Q :: nil) (Arrow P Q)
  | p_unit : lin_entail nil One
  | p_pair : forall Delta1 Delta2 P1 P2,
      lin_entail Delta1 P1 -> lin_entail Delta2 P2 ->
      lin_entail (Delta1 ++ Delta2) (Times P1 P2)
  | p_in1 : forall Delta P1 P2,
      lin_entail Delta P1 ->
      lin_entail Delta (Plus P1 P2)
  | p_in2 : forall Delta P1 P2,
      lin_entail Delta P2 ->
      lin_entail Delta (Plus P1 P2)
  | p_zero : lin_entail nil Nat
  | p_succ : forall Delta, lin_entail Delta Nat -> lin_entail Delta Nat.

(* Intuitionistic focusing judgments

  Translation key:
  rfoc Gamma P          "Gamma |- [P]" 
  linv Gamma P Q        "Gamma ; P |- Q" 
  unfoc Gamma P         "Gamma |- P"
  satctx Gamma Delta    "Gamma |- Delta"
*)

Definition intctx := stack hyp.

Inductive rfoc : intctx -> tp -> Set :=
  | Val : forall Gamma P Delta,
      lin_entail Delta P -> satctx Gamma Delta -> rfoc Gamma P

with linv : intctx -> tp -> tp -> Set :=
  | Lam : forall Gamma P Q,
      (forall Delta, lin_entail Delta P -> unfoc (Delta :: Gamma) Q) -> 
      linv Gamma P Q

with unfoc : intctx -> tp -> Set :=
  | Return : forall Gamma P, rfoc Gamma P -> unfoc Gamma P
  | EComp : forall Gamma P Q R,
      InStack (ArrowH P Q) Gamma -> rfoc Gamma P -> linv Gamma Q R ->
      unfoc Gamma R

with satctx : intctx -> linctx -> Set :=
  | SubNil : forall Gamma, satctx Gamma nil
  | SubConsX : forall Gamma X Delta,
      InStack (AtomH X) Gamma -> satctx Gamma Delta ->
      satctx Gamma (AtomH X::Delta)
  | SubConsF : forall Gamma P Q Delta,
      linv Gamma P Q -> satctx Gamma Delta -> 
      satctx Gamma (ArrowH P Q::Delta).