Library ExtLib.Generic.Data

Require Import Coq.Lists.List.
Require Import ExtLib.Data.Member.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Generic.Func.

Set Implicit Arguments.
Set Strict Implicit.

Fixpoint hlist_to_tuple ps (h : hlist (fun x : Type => x) ps) : asTuple ps :=
  match h in hlist _ ps return asTuple ps with
    | Hnil => tt
    | Hcons x h => (x,hlist_to_tuple h)
  end.

Inductive itype (ps : list Type) : Type :=
| Inj : Type -> itype ps
| Rec : hlist (fun x => x) ps -> itype ps
| Sum : itype ps -> itype ps -> itype ps
| Prod : itype ps -> itype ps -> itype ps
| Sig : forall T : Type, (T -> itype ps) -> itype ps
| Pi : forall T : Type, (T -> itype ps) -> itype ps
| Get : forall T : Type, member T ps -> (T -> itype ps) -> itype ps
| Unf : forall T : Type, member T ps -> T -> itype ps -> itype ps.

Definition Unit {ps} := @Inj ps unit.

Section denote.
  Variable (ps : list Type).

  Fixpoint itypeD (i : itype ps) {struct i}
  : asFunc ps Type -> asFunc ps Type :=
    match i return asFunc ps Type -> asFunc ps Type with
      | Get pf f => fun F => @get ps _ _ pf (fun x => itypeD (f x) F)
      | Inj _ T => fun _ => const T
      | Rec h => fun F => const (applyF F (hlist_to_tuple h))
      | @Sig _ t f => fun F =>
                     @under _ _ (fun App => @sigT t (fun x' => App _ (itypeD (f x') F)))
      | @Pi _ t f => fun F =>
                     @under _ _ (fun App => forall x' : t, App _ (itypeD (f x') F))
      | Sum a b => fun F => combine sum ps (itypeD a F) (itypeD b F)
      | Prod a b => fun F => combine prod ps (itypeD a F) (itypeD b F)
      | @Unf _ T pf v i => fun F =>
                          @get ps _ _ pf (fun x => combine prod _ (const (x = v : Type)) (replace pf v (itypeD i F)))
    end%type.
End denote.

Section _match.
  Variable ps : list Type.
  Variable RecT : asFunc ps Type.

  Fixpoint cases (i : itype ps) (k : asFunc ps Type -> asFunc ps Type)
           {struct i} : asFunc ps Type :=
    match i with
      | Inj _ T => k (const T)
      | Sum a b => combine prod ps (cases a k) (cases b k)
      | Prod a b =>
        cases a (fun A => cases b (fun B =>
                                       under _ _ (fun App => App _ A -> App _ (k B))))
      | Rec ps => k (const (applyF RecT (hlist_to_tuple ps)))
      | @Get _ T m f => @get _ _ _ m (fun x => cases (f x) k)
      | @Sig _ t f => @under _ _ (fun App => forall x' : t, (App _ (cases (f x') k)))
      | @Pi _ t f => @under _ _ (fun App => @sigT t (fun x' => App _ (cases (f x') k)))
      | @Unf _ T pf v i => replace pf v (cases i k)
    end.

End _match.

Fixpoint asPiE ps {struct ps}
: forall (F : _)
         (G : forall x : (forall U, asFunc ps U -> U), F x),
         asPi ps F :=
  match ps as ps
        return forall F : (forall U : Type, asFunc ps U -> U) -> Type,
                 (forall x : forall U : Type, asFunc ps U -> U, F x) -> asPi ps F
  with
    | nil => fun _ G => G _
    | p :: ps => fun _ G => fun x => asPiE _ _ (fun x' => G _)
  end.

Fixpoint asPi_combine ps {struct ps}
: forall (F G : _),
    asPi ps (fun App => F App -> G App) ->
    asPi ps F -> asPi ps G :=
  match ps as ps
        return forall F G : (forall U : Type, asFunc ps U -> U) -> Type,
                 asPi ps (fun App : forall U : Type, asFunc ps U -> U => F App -> G App) ->
                 asPi ps F -> asPi ps G
  with
    | nil => fun _ _ a b => a b
    | p :: ps => fun _ _ a b x => asPi_combine _ _ _ (a x) (b x)
  end.