Require Import List.


Section Polarity.

Inductive polarity : Set :=
  | nonvariant : polarity
  | covariant : polarity
  | contravariant : polarity.


Definition opp_pol (p: polarity) : polarity :=
  match p with
    | nonvariant => nonvariant
    | covariant => contravariant
    | contravariant => covariant
  end.

Definition mul_pol (p1 p2: polarity) : polarity :=
  match p1 with
    | nonvariant => nonvariant
    | covariant => p2
    | contravariant => opp_pol p2
  end.

End Polarity.


Section Types.

Inductive typ : Set :=
  | int : typ
  | arrow : typ -> typ -> polarity -> typ.

End Types.


Notation " t1 '->+' t2 " := (arrow t1 t2 covariant) (at level 60, right associativity).
Notation " t1 '->-' t2 " := (arrow t1 t2 contravariant) (at level 60, right associativity).
Notation " t1 '->o' t2 " := (arrow t1 t2 nonvariant) (at level 60, right associativity).


Section Terms.

Inductive cst : Set :=
  | zero : cst
  | succ : cst
  | add : cst
  | sub : cst
  | rec : cst.


Inductive trm: Set :=
  | Var : nat -> trm
  | Cst : cst -> trm
  | App : trm -> trm -> trm
  | Abs : polarity -> typ -> trm -> trm.


Definition env := list (option (polarity * typ)).

End Terms.


Section Typing.

Definition sigma (c: cst) : typ :=
  match c with
    | zero => int
    | succ => int ->+ int
    | add => int ->+ int ->+ int
    | sub => int ->+ int ->- int
    | rec => int ->o ((int ->o int) ->o int ->o int) ->o int
  end.


Definition inv_pol (p: polarity) (e: env) : env :=
  match p with
    | covariant => e
    | contravariant => map (fun x => match x with
               | Some (p,t) => Some (opp_pol p, t)
               | None => None
             end) e
    | nonvariant => map (fun x => match x with
               | Some (p,t) => match p with
                 | nonvariant => Some (nonvariant,t)
                 | _ => None
               end
               | None => None
             end) e
  end.


Inductive type : env -> trm -> typ -> Prop :=
  | varp : forall (e: env) (n: nat) (t: typ), nth n e None = Some (covariant, t) -> type e (Var n) t
  | varn : forall (e: env) (n: nat) (t: typ), nth n e None = Some (nonvariant, t) -> type e (Var n) t
  | cste : forall (e: env) (c: cst), type e (Cst c) (sigma c)
  | app : forall (e: env) (u v: trm) (t1 t2: typ) (p: polarity), type e u (arrow t1 t2 p) -> type (inv_pol p e) v t1 -> type e (App u v) t2
  | abs : forall (e: env) (m: trm) (t1 t2: typ) (p: polarity), type ((Some (p,t1))::e) m t2 -> type e (Abs p t1 m) (arrow t1 t2 p).

End Typing.