Set Implicit Arguments.

Require Import List.
Require Import String.

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 := 
  | PAtom : atom -> pos
  | One : pos
  | Times : pos -> pos -> pos
  | Zero : pos
  | Plus : pos -> pos -> pos
  | Nat : pos
  | Down : neg -> pos
  | LFArrow : rule -> pos -> pos
  | Def : string -> pos

with rule : Set :=
  | Ax : string -> rule
  | HO : pos -> rule -> rule

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

(* parameter contexts *)  
Definition parctx := list rule.

Definition cpos : Set := prod parctx pos.
Definition cneg := prod parctx neg.

(* hypotheses and linear contexts *)
Inductive hyp : Set :=
  | PAtomH : atom -> hyp
  | NegH : cneg -> hyp.

Definition linctx := frame hyp.

(* pattern typing, "Delta |= [Psi]A+" *)
Inductive tp_pat : linctx -> cpos -> Set :=
  | p_avar : forall Psi X, tp_pat (PAtomH X :: nil) (Psi,PAtom X)
  | p_fvar : forall Psi N, tp_pat (NegH (Psi,N) :: nil) (Psi,Down N)
  | p_unit : forall Psi, tp_pat nil (Psi, One)
  | p_pair : forall Delta1 Delta2 Psi P1 P2,
      tp_pat Delta1 (Psi,P1) -> tp_pat Delta2 (Psi,P2) ->
      tp_pat (Delta1 ++ Delta2) (Psi,Times P1 P2)
  | p_in1 : forall Delta Psi P1 P2,
      tp_pat Delta (Psi,P1) ->
      tp_pat Delta (Psi,Plus P1 P2)
  | p_in2 : forall Delta Psi P1 P2,
      tp_pat Delta (Psi,P2) ->
      tp_pat Delta (Psi,Plus P1 P2)
  | p_z : forall Psi, tp_pat nil (Psi,Nat)
  | p_s : forall Delta Psi, tp_pat Delta (Psi,Nat) -> tp_pat Delta (Psi,Nat)
  | p_lam : forall Delta Psi R P,
      tp_pat Delta (R::Psi,P) ->
      tp_pat Delta (Psi,LFArrow R P)
  | p_rule : forall Delta Psi P,
      tp_rule Delta (Psi,Ax P) -> tp_pat Delta (Psi,Def P)

with tp_rule : linctx -> parctx * rule -> Set :=
  | p_ax : forall Psi R, In R Psi -> tp_rule nil (Psi,R)
  | p_mp : forall Delta1 Delta2 Psi R A,
      tp_rule Delta1 (Psi,HO A R) -> tp_pat Delta2 (Psi,A) ->
      tp_rule (Delta1 ++ Delta2) (Psi,R).

(* conclusions *)
Inductive conc : Set :=
  | NAtomC : atom -> conc
  | PosC : cpos -> conc.

(* spine typing, "Delta | [Psi]A- |= gamma" *)
Inductive tp_skel : linctx -> cneg -> conc -> Set :=
  | s_aid : forall Psi X, tp_skel nil (Psi,NAtom X) (NAtomC X)
  | s_pid : forall Psi P, tp_skel nil (Psi,Up P) (PosC (Psi,P))
  | s_app : forall Delta1 Delta2 Psi P N gamma,
      tp_pat Delta1 (Psi,P) -> tp_skel Delta2 (Psi,N) gamma ->
      tp_skel (Delta1 ++ Delta2) (Psi,Arrow P N) gamma
  | s_pi1 : forall Delta Psi N1 N2 gamma,
      tp_skel Delta (Psi,N1) gamma ->
      tp_skel Delta (Psi,With N1 N2) gamma
  | s_pi2 : forall Delta Psi N1 N2 gamma,
      tp_skel Delta (Psi,N2) gamma ->
      tp_skel Delta (Psi,With N1 N2) gamma
  | s_unpack : forall Delta Psi R N gamma,
      tp_skel Delta (R::Psi,N) gamma ->
      tp_skel Delta (Psi,LFWedge R N) gamma.

(* Intuitionistic focusing judgments

  Translation key:
  rfoc Gamma C+         "Gamma |- [C+]" 
  active Gamma g0 g     "Gamma ; g0 |- g" 
  unfoc Gamma g         "Gamma |- g"
  inv Gamma C-          "Gamma |- C-"
  lfoc Gamma C- g       "Gamma ; [C-] |- g"
  satctx Gamma Delta    "Gamma |- Delta"
*)

Definition intctx := stack hyp.

Inductive rfoc : intctx -> cpos -> Set :=
  | Val : forall Gamma Cp Delta,
      tp_pat Delta Cp -> satctx Gamma Delta -> rfoc Gamma Cp

with active : intctx -> conc -> conc -> Set :=
  | Id : forall Gamma X, active Gamma (NAtomC X) (NAtomC X)
  | Ctx : forall Gamma Cp g,
      (forall Delta, tp_pat Delta Cp -> unfoc (Delta :: Gamma) g) -> 
      active Gamma (PosC Cp) g

with unfoc : intctx -> conc -> Set :=
  | Return : forall Gamma Cp, rfoc Gamma Cp -> unfoc Gamma (PosC Cp)
  | EComp : forall Gamma Cn g,
      InStack (NegH Cn) Gamma -> lfoc Gamma Cn g ->
      unfoc Gamma g

with lfoc : intctx -> cneg -> conc -> Set :=
  | Spine : forall Gamma Cn g0 g Delta,
      tp_skel Delta Cn g0 -> satctx Gamma Delta -> active Gamma g0 g ->
      lfoc Gamma Cn g

with inv : intctx -> cneg -> Set :=
  | Term : forall Gamma Cn,
      (forall Delta g, tp_skel Delta Cn g -> unfoc (Delta :: Gamma) g) -> 
      inv Gamma Cn

with satctx : intctx -> linctx -> Set :=
  | SubNil : forall Gamma, satctx Gamma nil
  | SubConsX : forall Gamma X Delta,
      InStack (PAtomH X) Gamma -> satctx Gamma Delta ->
      satctx Gamma (PAtomH X::Delta)
  | SubConsF : forall Gamma Cn Delta,
      inv Gamma Cn -> satctx Gamma Delta -> 
      satctx Gamma (NegH Cn::Delta).

Hint Constructors tp_pat tp_rule tp_skel : focus.
Hint Constructors rfoc active unfoc inv lfoc satctx : focus.

Definition Psi_nat := (Ax "nat") :: HO (Def "nat") (Ax "nat") :: nil.

Definition emp : frame hyp := nil.

Lemma one_is_a_nat :
  rfoc nil (Psi_nat,Def "nat").
eapply Val with (Delta := emp).
eapply p_rule.
eapply p_mp with (Delta1 := emp) (Delta2 := emp).
eapply p_ax.
compute; auto.
eapply p_rule.
eapply p_ax.
compute; auto.
eauto with focus.
Qed.

Print one_is_a_nat.

Lemma pred_fnc :
  inv nil (Psi_nat, Arrow (Def "nat") (Up (Def "nat"))).
eapply Term.
intros.
inversion H.
inversion H6.
eapply Return.
eapply Val.
apply H5.
(* identity substitution *)