(* binders/ must be a subdirectory in the current working directory. *)  
Add LoadPath "binders".

Require Import Specif.
Require Import Metatheory.
Require Import Metatheory_Var.
Require Import OrderedType OrderedTypeEx.
Require Import Peano_dec.

Module Names : VariablesType := Variables.

Definition kvar := var.

(** Source language - lambda terms with names 
source names are different than free variables in terms!!! *) 
Inductive src_tm : Set :=
| svar : var -> src_tm
| slam : var -> src_tm -> src_tm
| sapp : src_tm -> src_tm -> src_tm
| slet : var -> src_tm -> src_tm -> src_tm.

(* CPS terms *)
Inductive trm : Set :=
| trm_term : exp -> trm
with
exp : Set :=
| cont_app : cont -> val -> exp
| trm_app : trm -> cont -> exp
| val_app : val -> val -> cont -> exp
| elet : var -> val -> exp -> exp
with
val : Set :=
| bvar : nat -> val
| fvar : var -> val
| lam : var -> trm -> val
with
cont : Set :=
| c_bid : nat -> cont
| c_fid : kvar -> cont
| c_lam : exp -> cont.

(*
(** target terms = CPS normal forms (not checked for well-formedness)  *)
Inductive ttrm : trm -> Prop :=
| ttrm_term : forall e, texp e -> ttrm (trm_term e)
with
texp : exp -> Prop :=
| tbcont_app : forall k v, texp (cont_app (c_bid k) v)
| tfcont_app : forall k v, texp (cont_app (c_fid k) v)
| tval_app : forall v0 v1 e, tval v0 ->  
(e)...
tval v1 -> texp (val_app v0 v1 (c_lam e))
| telet : forall, texp (elet x v )
with
tval : val -> Prop :=
| tbvar : forall w, tval (bvar w)
| tfvar : forall x, tval (fvar x)
| tlam : forall x r, ttrm r -> tval (lam x r).
 *)

(* We need two kinds of opening operations: one
for opening with a value and one for opening with a continuations; 
each for a different kind of variable;
we count lambdas together for both kinds of variables *)

(** Opening up abstractions (with a value) - in continuations *)

Fixpoint open_rec (k : nat) (u : val) (r : trm) {struct r} : trm :=
match r with
| trm_term e => trm_term (open_exp (S k) u e)
end
with
open_exp k u e {struct e} : exp :=
match e with
| cont_app c v => cont_app (open_cont k u c) (open_val k u v)
| trm_app r c => trm_app (open_rec k u r) (open_cont k u c)
| val_app v0 v1 c => val_app (open_val k u v0) (open_val k u v1) (open_cont k u c)
| elet x v e => elet x (open_val k u v) (open_exp k u e)
end
with
open_val k u v {struct v} : val :=
match v with
| bvar w => if k === w then u else bvar w
| fvar x => fvar x
| lam x e => lam x (open_rec k u e)
end
with
open_cont k u c {struct c} : cont :=
match c with
| c_bid n => c_bid n
| c_fid n => c_fid n
| c_lam e => c_lam (open_exp (S k) u e)
end.

Definition open t u := open_rec 0 u t.

(** Opening up abstractions (with a continuation) - in terms *)

Fixpoint openc_rec (k : nat) (u : cont) (r : trm) {struct r} : trm :=
match r with
| trm_term e => trm_term (openc_exp (S k) u e)
end
with
openc_exp k u e {struct e} : exp :=
match e with
| cont_app c v => cont_app (openc_cont k u c) (openc_val k u v)
| trm_app r c => trm_app (openc_rec k u r) (openc_cont k u c)
| val_app v0 v1 c => val_app (openc_val k u v0) (openc_val k u v1) (openc_cont k u c)
| elet x v e => elet x (openc_val k u v) (openc_exp k u e)
end
with
openc_val k u v {struct v} : val :=
match v with
| bvar w => bvar w
| fvar x => fvar x
| lam x e => lam x (openc_rec k u e)
end
with
openc_cont k u c {struct c} : cont :=
match c with
| c_bid n => if k === n then u else c_bid n
| c_fid n => c_fid n
| c_lam e => c_lam (openc_exp (S k) u e)
end.

Definition openc t u := openc_rec 0 u t.

(*Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).*)
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (var x)).

(** Well-formed terms are locally closed trms *)

Inductive term : trm -> Prop :=
| term_trm : forall L e,
(forall k:kvar, k \notin L -> term_exp (openc_exp 0 (c_fid k) e)) ->
term (trm_term e)
with
term_exp : exp -> Prop :=
| term_cont_app : forall c v, term_cont c -> term_val v -> term_exp (cont_app c v)
| term_trm_app : forall r c, term r -> term_cont c -> term_exp (trm_app r c)
| term_val_app : forall v0 v1 c, term_val v0 -> term_val v1 ->
term_cont c -> term_exp (val_app v0 v1 c)
| term_elet : forall x v e,
term_val v -> term_exp e -> 
term_exp (elet x v e)
with
term_val : val -> Prop :=
| term_fvar : forall x, term_val (fvar x)
| term_lam : forall x r, term r -> term_val (lam x r)
with
term_cont : cont -> Prop :=
| term_c_fid : forall k, term_cont (c_fid k)
| term_c_lam : forall L e,
(forall w, w \notin L -> term_exp (open_exp 0 (fvar w) e)) ->
term_cont (c_lam e).

Hint Constructors term.

Scheme trmind := Induction for trm Sort Prop
with trmexpind := Induction for exp Sort Prop
with trmvalind := Induction for val Sort Prop
with trmcontind := Induction for cont Sort Prop.

Scheme termind := Induction for term Sort Prop
with termexpind := Induction for term_exp Sort Prop
with termvalind := Induction for term_val Sort Prop
with termcontind := Induction for term_cont Sort Prop.

(* Definition of closed terms, ie, without free continuation variables *)

Inductive closed : trm -> Prop :=
| closed_trm : forall e, closed_exp e -> closed (trm_term e)
with
closed_exp : exp -> Prop :=
| closed_cont_app : forall c v, closed_cont c -> closed_val v -> 
closed_exp (cont_app c v)
| closed_trm_app : forall r c, closed r -> closed_cont c -> 
closed_exp (trm_app r c)
| closed_val_app : forall v0 v1 c, closed_val v0 -> closed_val v1 ->
closed_cont c -> closed_exp (val_app v0 v1 c)
| closed_elet : forall x v e, closed_val v -> closed_exp e ->
closed_exp (elet x v e)
with
closed_val : val -> Prop :=
| closed_bvar : forall x, closed_val (bvar x)
| closed_fvar : forall x, closed_val (fvar x)
| closed_lam : forall x r, closed r -> closed_val (lam x r)
with
closed_cont : cont -> Prop :=
| closed_c_bid : forall n, closed_cont (c_bid n)
| closed_c_lam : forall e,
closed_exp e ->
closed_cont (c_lam e).


(** Definition of the body of a let-expression *)
(*
Definition body t :=
  exists L, forall x:var, x \notin L -> term (open t (fvar x)).
struct
(** Free variables in a term *)
*)

(* Standard CPS CBV translation *)

Fixpoint cps (t:src_tm) : trm :=
match t with
| svar x => trm_term (cont_app (c_bid 0) (fvar x))
| slam x t => trm_term (cont_app (c_bid 0) (lam x (cps t)))
| sapp t0 t1 => trm_term (trm_app (cps t0) (c_lam (trm_app (cps t1) (c_lam (val_app (bvar 1) (bvar 0) (c_bid 2))))))
| slet x t0 t1 => trm_term (trm_app (cps t0) 
(c_lam (elet x (bvar 0) (trm_app (cps t1) (c_bid 1)))))
end.

Fixpoint fv (t : trm) : vars :=
match t with
| trm_term e => fv_exp e
end
with fv_exp (e:exp) : vars :=
match e with
| cont_app c v => fv_cont c \u fv_val v
| trm_app r c => fv r \u fv_cont c
| val_app v0 v1 c => fv_val v0 \u fv_val v1 \u fv_cont c 
| elet x v e => fv_val v \u fv_exp e
end
with
fv_val (v:val) : vars :=
match v with
| bvar i => {}
| fvar x => {{x}}
| lam x r => fv r
end
with
fv_cont (c:cont) : vars :=
match c with
| c_bid k => {}
| c_fid k => {}
| c_lam e => fv_exp e
end.

Fixpoint fvc (t : trm) : vars :=
match t with
| trm_term e => fvc_exp e
end
with fvc_exp (e:exp) : vars :=
match e with
| cont_app c v => fvc_cont c \u fvc_val v
| trm_app r c => fvc r \u fvc_cont c
| val_app v0 v1 c => fvc_val v0 \u fvc_val v1 \u fvc_cont c 
| elet x v e => fvc_val v \u fvc_exp e
end
with
fvc_val (v:val) : vars :=
match v with
| bvar i => {}
| fvar x => {}
| lam x r => fvc r
end
with
fvc_cont (c:cont) : vars :=
match c with
| c_bid k => {}
| c_fid k => {{k}}
| c_lam e => fvc_exp e
end.

(** Inductive definition of normalization, ie. N e e' means that intermediate expression e
 normalizes to target expression e' *)

(** Rd must be defined only on well formed expressions *)
Inductive Rd : exp -> exp -> Prop :=
| ax18 :
forall e c L,
(forall k, k \notin L -> term_exp (openc_exp 0 (c_fid k) e)) ->
term_cont c ->
Rd (trm_app (trm_term e) c) (openc_exp 0 c e)
| ax19 :
forall e v L,
(forall x, x \notin L -> term_exp (open_exp 0 (fvar x) e)) ->
term_val v ->
Rd (cont_app (c_lam e) v) (open_exp 0 v e).

Inductive A : val -> val -> Prop :=
| A_var : forall x, A (fvar x) (fvar x)
| A_lam : forall x r0 r1, N r0 r1 -> A (lam x r0) (lam x r1)
with
N : trm -> trm -> Prop :=
| N_term : forall e0 e1 L,
(forall k, k \notin L -> Ne (openc_exp 0 (c_fid k) e0) (openc_exp 0 (c_fid k) e1)) ->
(* Ne e0 e1 ->*) N (trm_term e0) (trm_term e1)
with 
Ne : exp -> exp -> Prop :=
| Ne_cont_app : forall v0 v1 k,
A v0 v1 ->
Ne (cont_app (c_fid k) v0) (cont_app (c_fid k) v1)
| Ne_val_app : forall v0 w0 c0 v1 w1 c1,
A v0 v1 -> A w0 w1 -> C c0 c1 ->
Ne (val_app v0 w0 c0) (val_app v1 w1 c1)
| Ne_elet : forall x v e v0 e0,
A v v0 -> Ne e e0 ->
Ne (elet x v e) (elet x v0 e0)
| Ne_trans : forall e0 e1 e2,
Rd e0 e1 -> Ne e1 e2 -> Ne e0 e2
with
C : cont -> cont -> Prop :=
| C_fid : forall k, C (c_fid k) (c_fid k)
(* (c_lam (cont_app (c_fid k) (bvar 0))) (* eta expansion!!! *) *)
| C_c_lam : forall e0 e1 L, 
(forall x, x \notin L -> Ne (open_exp 0 (fvar x) e0) (open_exp 0 (fvar x) e1)) ->
(*Ne e0 e1 ->*) C (c_lam e0) (c_lam e1).

Scheme Aind := Induction for A Sort Prop
with Nind := Induction for N Sort Prop
with
Neind := Induction for Ne Sort Prop
with
Cind := Induction for C Sort Prop.


(*
(** Induction schema for mutual induction on terms *)
Lemma dbl_term_ind :
  forall P Q,
  (forall x:var, P (fvar x) * Q (fvar x)) ->
  (forall (n:var) (t:trm), P t -> P (lam n t) * Q (lam n t)) ->
  (forall t:src_tm, P t * Q t -> forall t0, P t0 * Q t0 -> P (app t t0) * Q (app t t0)) ->
  forall t, P t.
Proof.
intros.
assert (P t * Q t).
induction t; auto.
apply X0; auto.
destruct IHt; auto.
destruct X2; trivial.
Defined.

(** Induction schema for mutual induction on terms as suggested by one-pass transformer *)
Lemma ind2 :
  forall P Q,
   (forall n, P (lvar n)) ->
   (forall n t, P t-> P (lam n t)) ->
   (forall t, Q t -> forall t0, Q t0 -> P (app t t0)) ->
   (forall n, Q (lvar n)) ->
   (forall n t, P t -> Q (lam n t)) ->
   (forall t, Q t -> forall t0, Q t0 -> Q (app t t0)) ->
   forall t, P t.
Proof.
intros.
apply dbl_term_ind with (Q:=Q); auto.
intros; split; auto.
apply X1.
destruct X5; auto.
destruct X6; auto.
apply X4.
destruct X5; auto.
destruct X6; auto.
Qed.

*)

Definition Gv v := closed_val v /\ term_val v.
Definition Gc c := closed_cont c /\ term_cont c.

(** Logical relation on contexts, ie. context c satisfies property Rc if - plugged with value -
normalizes *)
(*
Definition Rv (v:val) := prod (closed_val v) { v' : val | A v v'}.
Definition Re (e:exp) := prod (closed_exp e) {e' : exp | Ne e e'}.
Definition Rc (c:cont) := prod (closed_cont c) 
(forall v, Gv v -> Rv v -> Re (cont_app c v)).
(** Goal property on source terms *)
Definition R (r:trm) := prod (closed r) (forall c, Gc c -> Rc c -> Re (trm_app r c)).
*)

Definition Rv (v:val) := { v' : val | A v v'}.
Definition Re (e:exp) := {e' : exp | Ne e e'}.
(*
Fixpoint Rc (c:cont) : Type :=
match c with
| c_bid k => False
| c_fid k => True
| c_lam e => (forall v, Gv v -> Rv v -> Re (cont_app (c_lam e) v))
end.
*)

Definition Rc (c:cont) := (forall v, Gv v -> Rv v -> Re (cont_app c v)).


(** Goal property on source terms *)
Definition R (r:trm) := (forall c, (*Gc c -> *) Rc c -> Re (trm_app r c)).
 
Hint Unfold (*Rc*) Rv Re R.