Require Import ssreflect Sint63.
Open Scope sint63_scope.

Inductive expr : Type -> Type :=
  | Int : int -> expr int
  | Add : expr (int -> int -> int)
  | App a b : expr (a -> b) -> expr a -> expr b.
Print expr.

Fixpoint eval (a : Type) (e : expr a) : a :=
  match e in expr a return a with
  | Int n => n
  | Add => Int63.add
  | App b c f x => eval (b -> c) f (eval b x)
  end.

Definition evfun (a b : Type) (e : expr (a -> b)) : a -> b :=
  match e in expr a return a with
  | Int n => n
  | Add => Int63.add
  | App b c f x => eval (b -> c) f (eval b x)
  end.

Inductive eqw (A : Type) : A -> A -> Type := Refl x : eqw A x x.

Definition cast A B (w : eqw Type A B) :=
  match w in eqw _ A B return A -> B with
    Refl _ _ => fun a => a
  end.

Definition trans (A B C : Type) : eqw _ A B -> eqw _ B C -> eqw _ A C :=
  fun w1 =>
    match w1 in eqw _ A B return eqw _ B C -> eqw _ A C
    with Refl _ _ => fun w2 => w2 end.

Definition lem A B C D (x : A * B) : (A * B = C * D)%type -> A = C.
move=> Eq.
move: (fst x).
have y := x.
Abort.

Fail
Definition cast_fst A B (w : eqw _ (A * B)%type (int * bool)%type) : A -> int :=
  match w in eqw _ (A * B)%type (C * D)%type return A -> C with
    Refl => fun a => a
  end.

Inductive empty :=. 

Lemma eqw_eq A x y : eqw A x y -> x = y.
Proof. by elim. Qed.

Definition any_bool_empty A (w : eqw _ bool empty) : A.
set f := fun x : bool => x.
set g := eq_rect bool (fun T => bool -> T) f empty (eqw_eq _ _ _ w).
case: g.
exact true.
Defined.

Inductive zero := Zero.
Inductive succ (n : Type) := Succ of n.
Inductive vec (A : Type) : Type -> Type :=
  | Nil : vec A zero
  | Cons n : A -> vec A n -> vec A (succ n).

Fixpoint map A B n (f : A -> B) (l : vec A n) :=
  match l in vec _ n return vec B n with
  | Nil _ => Nil B
  | Cons _ n a l => Cons B n (f a) (map A B n f l)
  end.

Fail Definition head A n (l : vec A (succ n)) : A :=
  match l with
  | Cons _ n a l => a
  end.

Inductive ty : Type -> Type :=
  | Tbool : ty bool
  | Tint : ty int
  | Tpair A B : ty A -> ty B -> ty (A * B)
  | Tarrow A B : ty A -> ty B ->  ty (A -> B).

Inductive dyn := Dyn T of ty T & T.

Fixpoint sum (h : nat) (d : dyn) : int :=
  if h is S h then
    let: (Dyn T a x) := d in
    match a in ty T return T -> int with
    | Tbool => fun x => if x then 1 else 0
    | Tint => fun x => x
    | Tpair T1 T2 TY1 TY2 =>
        fun x =>
        sum h (Dyn T1 TY1 (fst x)) +
        sum h (Dyn T2 TY2 (snd x))
    | Tarrow _ _ _ _ => fun x => 0
    end x
  else 0.

Reset expr.

Inductive ml_type : Set :=
  | ml_int
  | ml_bool
  | ml_arrow of ml_type & ml_type
  | ml_pair of ml_type & ml_type
  | ml_eqw of ml_type & ml_type
  | ml_expr of ml_type
  | ml_zero
  | ml_succ of ml_type
  | ml_vec of ml_type & ml_type
  | ml_ty of ml_type
  | ml_dyn
  | ml_hlist of ml_type.
Print ml_type.

Inductive eqw (T1 T2 : ml_type) :=
  | Refl of T1 = T2.

Inductive zero := Zero.
Inductive succ n := Succ of n.
Inductive vec (A : Type) (n : ml_type) :=
  | Nil of n = ml_zero
  | Cons m of n = ml_succ m & A & vec A m.

Inductive expr (T : ml_type) :=
  | Int of T = ml_int & int
  | Add of T = ml_arrow ml_int (ml_arrow ml_int ml_int)
  | App T2 of expr (ml_arrow T2 T) & expr T2.

Inductive ty (T : ml_type) :=
  | Tbool of T = ml_bool
  | Tint of T = ml_int
  | Tpair (A B : ml_type) of T = ml_pair A B & ty A & ty B
  | Tarrow (A B : ml_type) of T = ml_arrow A B & ty A & ty B.

Inductive dyn (ct : ml_type -> Type) := Dyn (T : ml_type) of ty T & ct T.

Inductive hlist (ct : ml_type -> Type) (T : ml_type) :=
  | HNil of T = ml_zero
  | HCons T1 T2 of T = ml_pair T1 T2 & ct T1 & hlist ct T2.

#[bypass_check(guard)]
Fixpoint coq_type (T : ml_type) : Type :=
  match T with
  | ml_int => Int63.int
  | ml_bool => bool
  | ml_arrow T1 T2 => coq_type T1 -> coq_type T2
  | ml_pair T1 T2 => coq_type T1 * coq_type T2
  | ml_eqw T1 T2 => eqw T1 T2
  | ml_expr T1 => expr T1
  | ml_zero => zero
  | ml_succ T1 => succ (coq_type T1)
  | ml_vec T1 T2 => vec (coq_type T1) T2
  | ml_ty T1 => ty T1
  | ml_dyn => dyn coq_type
  | ml_hlist T1 => hlist coq_type T1
  end.

Fixpoint map (T1 T2 T3 : ml_type) (f : coq_type T1 -> coq_type T2)
         (l : vec (coq_type T1) T3) :=
  match l with
  | Nil _ _ H => Nil _ _ H
  | Cons _ _ m H a l =>
      Cons _ _ m H (f a) (map T1 T2 _ f l)
  end.

Definition head (T1 T2 : ml_type) (l : vec (coq_type T1) (ml_succ T2))
  : coq_type T1 :=
  match l with
  | Nil _ _ H => match H with end
  | Cons _ _ _ _ a _ => a
  end.

Definition eqw_eq [x y] (w : eqw x y) : x = y :=
  match w with Refl _ _ H => H end.

Definition cast (T1 T2 : ml_type) (w : eqw T1 T2) (x : coq_type T1) :
  coq_type T2 := eq_rect T1 coq_type x T2 (eqw_eq w).

Definition proj_ml_pair_1 defT T :=
  if T is ml_pair T1 _ then T1 else defT.

Definition cast_fst (A B : ml_type)
           (w : eqw (ml_pair A B) (ml_pair ml_int ml_bool))
           (x : coq_type A) : int :=
  eq_rect A coq_type x ml_int (f_equal (proj_ml_pair_1 A) (eqw_eq w)).

Definition proj_ml_succ defT T :=
  if T is ml_succ T1 then T1 else defT.

Definition succ_inj n1 n2 (w : eqw (ml_succ n1) (ml_succ n2)) : eqw n1 n2 :=
  Refl _ _ (f_equal (proj_ml_succ n1) (eqw_eq w)).

Fixpoint eval (T : ml_type) (e : expr T) : coq_type T :=
  match e with
  | Int _ H n => eq_rect ml_int coq_type n T (eq_sym H)
  | Add _ H =>
      eq_rect (ml_arrow ml_int (ml_arrow ml_int ml_int))
              coq_type Int63.add T (eq_sym H)
  | App _ T1 f x => eval _ f (eval T1 x)
  end.
Print eval.

Compute eval _ (App _ _ (App _ _ (Add _ (eq_refl _)) (Int _ (eq_refl _) 3)) (Int _ (eq_refl _) 4)).

(* Unset Guard Checking. *)
#[bypass_check(guard)]
Fixpoint sum (h : nat) (d : dyn coq_type) : int :=
  if h is S h then
    let: (Dyn _ T a x) := d in
    match a with
    | Tbool _ H => if eq_rect _ _ x _ H then 1 else 0
    | Tint _ H => eq_rect _ _ x _ H
    | Tpair _ T1 T2 H TY1 TY2 =>
        sum h (Dyn _ T1 TY1 (fst (eq_rect _ _ x _ H))) +
        sum h (Dyn _ T2 TY2 (snd (eq_rect _ _ x _ H)))
    | Tarrow _ _ _ _ _ _ => 0
    end
  else 0.

Eval compute in
  sum 10 (Dyn _ _ (Tpair _ _ _ eq_refl (Tint _ eq_refl)
                         (Tbool _ eq_refl)) (3, true)).

Definition hhead (T1 T2 : ml_type) (l : hlist coq_type (ml_pair T1 T2))
  : coq_type T1 :=
  match l with
  | HNil _ _ H => match H with end
  | HCons _ _ _ _ H a _ =>
      eq_rect _ _ a _ (f_equal (proj_ml_pair_1 ml_zero) (eq_sym H))
  end.

Eval compute in
  hhead _ _
        (HCons coq_type _ ml_int ml_zero eq_refl 3 (HNil coq_type _ eq_refl)).

Reset eqw.

Inductive eqw : ml_type -> ml_type -> Type :=
  | Refl T : eqw T T.

Inductive zero := Zero.
Inductive succ n := Succ of n.
Inductive vec (A : Type) : ml_type -> Type :=
  | Nil : vec A ml_zero
  | Cons m : A -> vec A m -> vec A (ml_succ m).

Inductive expr : ml_type -> Type :=
  | Int : int -> expr ml_int
  | Add : expr (ml_arrow ml_int (ml_arrow ml_int ml_int))
  | App T T2 : expr (ml_arrow T2 T) -> expr T2 -> expr T.

Inductive ty : ml_type -> Type :=
  | Tbool : ty ml_bool
  | Tint : ty ml_int
  | Tpair (A B : ml_type) : ty A -> ty B -> ty (ml_pair A B)
  | Tarrow (A B : ml_type) : ty A -> ty B ->  ty (ml_arrow A B).

Inductive dyn (ct : ml_type -> Type) := Dyn (T : ml_type) of ty T & ct T.

Inductive hlist (ct : ml_type -> Type) : ml_type -> Type :=
  | HNil : hlist ct ml_zero
  | HCons T1 T2 : ct T1 -> hlist ct T2 -> hlist ct (ml_pair T1 T2).

#[bypass_check(guard)]
Fixpoint coq_type (T : ml_type) : Type :=
  match T with
  | ml_arrow T1 T2 => coq_type T1 -> coq_type T2
  | ml_pair T1 T2 => coq_type T1 * coq_type T2
  | ml_eqw T1 T2 => eqw T1 T2
  | ml_expr T1 => expr T1
  | ml_zero => zero
  | ml_succ T1 => succ (coq_type T1)
  | ml_vec T1 T2 => vec (coq_type T1) T2
  | ml_int => Int63.int
  | ml_bool => bool
  | ml_ty T1 => ty T1
  | ml_dyn => dyn coq_type
  | ml_hlist T1 => hlist coq_type T1
  end.

Fixpoint map (T1 T2 T3 : ml_type) (f : coq_type T1 -> coq_type T2)
         (l : vec (coq_type T1) T3) :=
  match l in vec _ n return vec (coq_type T2) n with
  | Nil _ => Nil _
  | Cons _ m a l =>
      Cons _ m (f a) (map T1 T2 _ f l)
  end.

Definition is_succ T :=
  if T is ml_succ _ then True else False.

Definition head (T1 T2 : ml_type) (l : vec (coq_type T1) (ml_succ T2))
  : coq_type T1 :=
  match l with
  | Cons _ _ a _ => a
  end.

Definition cast T1 T2 (w : eqw T1 T2) :=
  match w in eqw T1 T2 return coq_type T1 -> coq_type T2 with
  | Refl _ => fun x => x
  end.

Definition proj_ml_pair1 defT T :=
  if T is ml_pair T1 _ then T1 else defT.

Definition eqw_eq [T1 T2] (w : eqw T1 T2) : T1 = T2 :=
  match w with Refl _ => eq_refl end.

Definition cast_fst (A B : ml_type)
           (w : eqw (ml_pair A  B) (ml_pair ml_int ml_bool))
           (x : coq_type A) : int :=
  eq_rect A coq_type x ml_int (f_equal (proj_ml_pair1 A) (eqw_eq w)).

Fixpoint eval (T : ml_type) (e : expr T) : coq_type T :=
  match e in expr T return coq_type T with
  | Int n => n
  | Add => Int63.add
  | App _ _ f x => eval _ f (eval _ x)
  end.

Compute eval _ (App _ _ (App _ _ Add (Int 3)) (Int 4)).

#[bypass_check(guard)]
Fixpoint sum (h : nat) (d : dyn coq_type) : int :=
  if h is S h then
    let: (Dyn _ T a x) := d in
    match a in ty T return coq_type T -> int with
    | Tbool => fun x => if x then 1 else 0
    | Tint => fun x => x
    | Tpair T1 T2 TY1 TY2 =>
        fun x =>
        sum h (Dyn _ T1 TY1 (fst x)) +
        sum h (Dyn _ T2 TY2 (snd x))
    | Tarrow _ _ _ _ => fun x => 0
    end x
  else 0.