(*
 * Coq code of the examples in the paper
 *
 *		      A Type System for Certified Binaries
 *			      YALEU/DCS/TR-1211
 *
 *   by Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou
 *
 * (for Coq version 6.3.1)
 *)

(*-------------------------- The type language TL --------------------------*)

(*
 * Sorts
 *
 * We map the TL sorts to Coq's built-in sorts Type and Set.
 * The sorts Ext and Kscm are both mapped to Type.
 * Since Kscm : Ext, this may seem to imply that Type : Type,
 *   but in reality Coq implements the infinite {Type_i} hierarchy of ECC
 *   and silently assigns appropriate levels to Types.
 * In our case this means Ext = Type_1 : Type_2 and Kscm = Type_0 : Type_1.
 *)

Definition Kscm : Type := Type.
Definition Kind : Type := Set.

(*
 * Logical propositions: constants
 *
 * (Coq uses the syntax (X : A) B for product types.)
 *)

Definition  True : Kind := (k : Kind) k -> k.
Definition False : Kind := (k : Kind) k.

(*
 * A proof of True: the polymorphic identity
 *
 * (Coq uses the syntax [X : A] B for abstractions.
 *  Headers of nested abstractions may be merged, e.g.
 *        [X,X' : A; Y : A'] B
 *    for [X : A] [X' : A] [Y : A'] B.)
 *)

Definition id : True := [k : Kind; t : k] t.

(*
 * Logical connectives: negation
 *)

Definition Not : Kind -> Kind := [k : Kind] k -> False.

(*
 * Examples of inductive definitions
 *)

Inductive Bool : Kind := true  : Bool
		       | false : Bool.

Inductive Nat : Kind := zero : Nat
		      | succ : Nat -> Nat.

(*
 * Each definition of an inductive kind also defines implicitly
 *   the corresponding small and large eliminations
 *   and binds them to identifiers obtained by appending "_rec" and "_rect"
 *   to the kind name.
 * E.g. the dependent large elimination on Bool is Bool_rect of kind
 *
 *   (P : Bool -> Type) (P true) -> (P false) -> (b : Bool) (P b),
 *
 * and the dependent small elimination on Nat is Nat_rec of kind
 *
 *   (P : Nat -> Kind)
 *     (P zero) -> ((n : Nat) (P n) -> (P (succ n))) -> (n : Nat) (P n).
 *
 * The syntax Elim[Nat,k](t){tz,ts} in the paper corresponds to
 *
 *   (Nat_rec k tz ts t)
 *
 * Next we define non-dependent versions of these eliminations
 *   which are used in the translation of pattern matching syntax below.
 *)

Definition Bool_LElimND : (u : Type) u -> u -> Bool -> u
 := [u : Type] (Bool_rect ([_ : Bool] u)).

Definition Nat_ElimND : (k : Kind) k -> (Nat -> k -> k) -> Nat -> k
 := [k : Kind] (Nat_rec ([_ : Nat] k)).

(*
 * The examples using pattern matching syntax are translated here
 *   to applications of the corresponding elimination terms.
 * We use "?" for kinds which are implicit in the paper and Coq can infer.
 *)

Definition plus : Nat -> Nat -> Nat
 := (Nat_ElimND ?
      [t : Nat] t
      [t : ?; plus_t : ?; t' : Nat] (succ (plus_t t'))).

Definition ifez : Nat -> ((k : Kind) k -> (Nat -> k) -> k)
 := (Nat_ElimND ?
      [k : Kind; t1 : k; t2 : Nat -> k] t1
      [t : ?; _ifez_t : ?; k : Kind; t1 : k; t2 : Nat -> k] (t2 t)).

Definition le : Nat -> Nat -> Bool
 := (Nat_ElimND ?
      [t : Nat] true
      [t : ?; le_t : ?; t' : Nat] (ifez t' Bool false le_t)).

Definition lt : Nat -> Nat -> Bool
 := [t : Nat] (le (succ t)).

Definition Cond : Bool -> Kind -> Kind -> Kind
 := (Bool_LElimND ?
      [k1,k2 : Kind] k1
      [k1,k2 : Kind] k2).

(*--------------- Types in the computation language lambda-H ----------------*)

Inductive Omega : Kind := snat : Nat -> Omega
			| sbool : Bool -> Omega
			| arrow : Omega -> Omega -> Omega
			| tup : Nat -> (Nat -> Omega) -> Omega
			| allKind : (k : Kind) (k -> Omega) -> Omega
			| exKind : (k : Kind) (k -> Omega) -> Omega
			| allKscm : (z : Kscm) (z -> Omega) -> Omega
			| exKscm : (z : Kscm) (z -> Omega) -> Omega.

(*
 * Syntactic sugar for Omega constructors
 *
 * We use Coq's inference facilities for the shorthand syntax for quantifiers.
 *)

Infix RIGHTA 7 "=>" arrow.
Syntactic Definition allK := (allKind ?).
Syntactic Definition exK := (exKind ?).
Syntactic Definition allKs := (allKscm ?).
Syntactic Definition exKs := (exKscm ?).

Syntactic Definition forall := allK.
Syntactic Definition exists := exK.

(*
 * (Note syntax below: the term is parsed as (forall ([t : Omega] t)).)
 *)

Definition void : Omega := (forall [t : Omega] t).

(*
 * The usual types of natural numbers and booleans.
 *)

Definition nat  : Omega := (exists [t : Nat] (snat t)).
Definition bool : Omega := (exists [t : Bool] (sbool t)).

(*
 * Types for and of tuples.
 *)

Inductive List : Kind := nil  : List
		       | cons : Omega -> List -> List.

Definition List_ElimND : (k : Kind) k -> (Omega -> List -> k -> k) -> List -> k
 := [k : Kind] (List_rec ([_ : List] k)).

Definition nth : List -> Nat -> Omega
 := (List_ElimND ?
      [t : Nat] void
      [t1 : ?; t2 : ?; nth_t2 : ?; t : Nat] (ifez t Omega t1 nth_t2)).

Infix RIGHTA 6 ":::" cons.

Definition pair : Omega -> Omega -> Omega :=
  [t,t' : Omega] (tup (succ (succ zero)) (nth (t ::: t' ::: nil))).
Infix 3 "**" pair.

Definition repeat : Nat -> Omega -> List
 := (Nat_ElimND ?
      [t' : Omega] nil
      [t : ?; repeat_t : ?; t' : Omega] t' ::: (repeat_t t')).

Definition vec : Nat -> Omega -> Omega
 := [t: Nat; t' : Omega] (tup t (nth (repeat t t'))).

Definition vector : Omega -> Omega
 := [t : Omega] (exists [t' : Nat] (snat t') ** (vec t' t)).

(*
 * The inductive kind of proofs of m < n, called here LT_i to avoid name clash.
 * Presented only for illustration of the intention behind LT, defined below.
 *)

Inductive LT_i : Nat -> Nat -> Kind
 := ltzs_i : (t : Nat) (LT_i zero (succ t))
  | ltss_i : (t,t' : Nat) (LT_i t t') -> (LT_i (succ t) (succ t')).

(*
 * The Church encoding LT of LT_i, which we use in the proofs to stay in TL.
 *)

Definition LT : Nat -> Nat -> Kind
 := [t,t' : Nat]
    (R : Nat -> Nat -> Kind)
    ((t : Nat) (R zero (succ t))) ->
    ((t,t' : Nat) (R t t') -> (R (succ t) (succ t'))) ->
    (R t t').

Definition ltzs : (t : Nat) (LT zero (succ t))
 := [t : Nat; R : Nat -> Nat -> Kind;
     z : (t : Nat) (R zero (succ t));
     s : (t,t' : Nat) (R t t') -> (R (succ t) (succ t'))]
    (z t).

Definition ltss : (t,t' : Nat) (LT t t') -> (LT (succ t) (succ t'))
 := [t,t' : Nat; p : (LT t t'); R : Nat -> Nat -> Kind;
     z : (t : Nat) (R zero (succ t));
     s : (t,t' : Nat) (R t t') -> (R (succ t) (succ t'))]
    (s t t' (p R z s)).

(*
 * Dependent if-zero (on Nat) and conditional (on Bool).
 *)

Definition dep_ifez
 : (t : Nat; k : Nat -> Kind) (k zero) -> ((t' : Nat) (k (succ t'))) -> (k t)
 := [t : Nat; k : Nat -> Kind; t1 : (k zero); t2 : ((t' : Nat) (k (succ t')))]
    (Nat_rec k
      t1
      [t' : Nat; _ : (k t')] (t2 t')
      t).

Definition dep_if : (t : Bool; k : Bool -> Kind) (k true) -> (k false) -> (k t)
 := [t : Bool; k : Bool -> Kind; t1 : (k true); t2 : (k false)]
    (Bool_rec k t1 t2 t).

(*
 * The kind LTOrTrue, which appears in the example of
 *   subscript check elimination, and some abbreviations.
 *)

Definition LTOrTrue : Nat -> Nat -> Bool -> Kind
 := [t1,t2 : Nat; t : Bool] (Cond t (LT t1 t2) True).

Definition LTcond : Nat -> Nat -> Kind
 := [t',t : Nat] (LTOrTrue t' t (lt t' t)).

Definition LTimp : Nat -> Nat -> Bool -> Kind
 := [t',t : Nat; t'' : Bool]
    (LTOrTrue t' t t'') -> (LTOrTrue (succ t') (succ t) t'').

(*
 * The generator of proofs used in the subscript check elimination example.
 *)

Definition ltPrf : (t',t : Nat) (LTcond t' t)
 := [t' : Nat]
 (* Note: an extra [t : Nat] appears here in a version of the paper *)
    (Nat_rec ([t1' : Nat] (t1 : Nat) (LTcond t1' t1))
      [t1 : Nat] (dep_ifez t1 (LTcond zero) id ltzs)
      [t1' : Nat; tP : (t1 : Nat) (LTcond t1' t1); t1 : Nat]
        (dep_ifez t1
		  (LTcond (succ t1'))
		  id
		  [t1 : Nat] (dep_if (lt t1' t1)
				     (LTimp t1' t1)
				     (ltss t1' t1)
				     (id True)
				     (tP t1)))
      t').

(*------------------- Types in the CPS language lambda-K --------------------*)

Inductive Omega_K : Kind := snat_K : Nat -> Omega_K
			  | sbool_K : Bool -> Omega_K
			  | arrowBottom : Omega_K -> Omega_K
			  | func : Omega_K -> Omega_K
			  | tup_K : Nat -> (Nat -> Omega_K) -> Omega_K
			  | allKind_K : (k : Kind) (k -> Omega_K) -> Omega_K
			  | exKind_K : (k : Kind) (k -> Omega_K) -> Omega_K
			  | allKscm_K : (z : Kscm) (z -> Omega_K) -> Omega_K
			  | exKscm_K : (z : Kscm) (z -> Omega_K) -> Omega_K.

Definition void_K : Omega_K := (allKind_K Omega_K [t : Omega_K] t).

Inductive List_K : Kind := nil_K  : List_K
			 | cons_K : Omega_K -> List_K -> List_K.

Definition nth_K : List_K -> Nat -> Omega_K
 := (List_K_rec ([_ : List_K] Nat -> Omega_K)
      [t : Nat] void_K
      [t1 : ?; t2 : ?; nth_K_t2 : ?; t : Nat] (ifez t Omega_K t1 nth_K_t2)).

Definition pair_K : Omega_K -> Omega_K -> Omega_K :=
  [t,t' : Omega_K]
  (tup_K (succ (succ zero)) (nth_K (cons_K t (cons_K t' nil_K)))).

(*
 * The type function cont is used here instead of the macro K_c in the paper,
 *   which inside the definition of K expands into inductive invocations.
 *)

Definition cont : Omega_K -> Omega_K
 := [t : Omega_K] (func (arrowBottom t)).

Definition K : Omega -> Omega_K
 := (Omega_rec ([_ : Omega] Omega_K)
  (* snat *)    snat_K
  (* sbool *)   sbool_K
  (* arrow *)   [t1 : Omega; K_t1 : Omega_K; t2 : Omega; K_t2 : Omega_K]
		  (cont (pair_K K_t1 (cont K_t2)))
  (* tup *)     [t1 : Nat; t2 : Nat -> Omega; K_o_t2 : Nat -> Omega_K]
		  (tup_K t1 ([t : Nat] (K_o_t2 t)))
  (* allKind *) [k : Kind; t : k -> Omega; K_o_t : k -> Omega_K]
		  (func (allKind_K k [t1 : k] (arrowBottom (cont (K_o_t t1)))))
  (* exKind *)  [k : Kind; t : k -> Omega; K_o_t : k -> Omega_K]
		  (exKind_K k ([t1 : k] (K_o_t t1)))
  (* allKscm *) [z : Kscm; t : z -> Omega; K_o_t : z -> Omega_K]
		  (func (allKscm_K z [k : z] (arrowBottom (cont (K_o_t k)))))
  (* exKscm *)  [z : Kscm; t : z -> Omega; K_o_t : z -> Omega_K]
		  (exKscm_K z ([k : z] (K_o_t k)))).

(*----------- Closure conversion for types in language lambda-C ------------*)

Definition Cl : Omega_K -> Omega_K -> Omega_K
 := (Omega_K_rec ([_ : Omega_K] Omega_K -> Omega_K)
  (* snat *)    [t : Nat; t' : Omega_K] (snat_K t)
  (* sbool *)   [t : Bool;  t' : Omega_K] (sbool_K t)
  (* arr-bot *) [t : Omega_K; Cl_t : Omega_K -> Omega_K; t' : Omega_K]
		  (arrowBottom (pair_K t' (Cl_t void_K)))
  (* func *)    [t : Omega_K; Cl_t : Omega_K -> Omega_K; t' : Omega_K]
		  (exKind_K Omega_K ([t1 : Omega_K] (pair_K (Cl_t t1) t1)))
  (* tup *)     [t1 : Nat; t2 : Nat -> Omega_K;
		 Cl_o_t2 : Nat -> Omega_K -> Omega_K; t' : Omega_K]
		  (tup_K t1 ([t'' : Nat] (Cl_o_t2 t'' t')))
  (* allKind *) [k : Kind; t : k -> Omega_K;
		 Cl_o_t : k -> Omega_K -> Omega_K; t' : Omega_K]
		  (allKind_K k ([t1 : k] (Cl_o_t t1 t')))
  (* exKind *)  [k : Kind; t : k -> Omega_K;
		 Cl_o_t : k -> Omega_K -> Omega_K; t' : Omega_K]
		  (exKind_K k ([t1 : k] (Cl_o_t t1 t')))
  (* allKscm *) [z : Kscm; t : z -> Omega_K;
		 Cl_o_t : z -> Omega_K -> Omega_K; t' : Omega_K]
		  (allKscm_K z ([k : z] (Cl_o_t k t')))
  (* exKscm *)  [z : Kscm; t : z -> Omega_K;
		 Cl_o_t : z -> Omega_K -> Omega_K; t' : Omega_K]
		  (exKscm_K z ([k : z] (Cl_o_t k t')))).

(*
 * ver 1. July 24, 2001. Valery Trifonov
 *)