Library MetaCoq.Translations.param_cheap_packed

Fixpoint refresh_universes (t : term) {struct t} :=
  match t with
  | tSort s ⇒ tSort (if Universe.is_level s then s else fresh_universe)
  | tProd na b t ⇒ tProd na b (refresh_universes t)
  | tLetIn na b t' t ⇒ tLetIn na b t' (refresh_universes t)
  | _ ⇒ t
  end.

Reserved Notation "'tsl_ty_param'".

Fixpoint tsl_rec1 (n : nat) (t : term) {struct t} : term :=
  match t with
  | tRel k ⇒ if ge_dec k n then proj1 t else t
  | tEvar k ts ⇒ tEvar k (List.map (tsl_rec1 n) ts)
  | tCast t c a ⇒ tCast (tsl_rec1 n t) c (tsl_rec1 n a)
  | tProd x A B ⇒ tProd x (tsl_rec1 n A) (tsl_rec1 (n+1) B)
  | tLambda x A t ⇒ tLambda x (tsl_rec1 n A) (tsl_rec1 (n+1) t)
  | tLetIn x a t u ⇒ tLetIn x (tsl_rec1 n a) (tsl_rec1 n t) (tsl_rec1 (n+1) u)
  | tApp t lu ⇒ tApp (tsl_rec1 n t) (List.map (tsl_rec1 n) lu)
  | tCase ik t u br ⇒ tCase ik (tsl_rec1 n t) (tsl_rec1 n u)
                            (List.map (fun x ⇒ (fst x, tsl_rec1 n (snd x))) br)
  | tProj p t ⇒ tProj p (tsl_rec1 n t)
  
  
  | _ ⇒ t
  end.

Fixpoint tsl_rec2 (fuel : nat) (Σ : global_env) (G : universes_graph) (E : tsl_table) (Γ : context) (t : term) {struct fuel}
  : tsl_result term :=
  match fuel with
  | O ⇒ raise translation_utils.NotEnoughFuel
  | S fuel ⇒
  match t with
  | tRel n ⇒ ret (proj2 (tRel n))
  | tSort s ⇒ ret (tLambda (nNamed "A") (tSort s)
                           (tProd nAnon (tRel 0) (tSort s)))
  | tCast t c A ⇒ let t1 := tsl_rec1 0 t in
                  t2 <- tsl_rec2 fuel Σ G E Γ t ;;
                  A2 <- tsl_rec2 fuel Σ G E Γ A ;;
                  ret (tCast t2 c (tApp A2 [t1]))
  | tProd n A B ⇒ let ΠAB' := tsl_rec1 0 (tProd n A B) in
                  let B1 := tsl_rec1 0 B in
                  A' <- tsl_ty_param fuel Σ G E Γ A ;;
                  B2 <- tsl_rec2 fuel Σ G E (Γ ,, vass n A) B ;;
                  ret (tLambda (nNamed "f") ΠAB'
                               (tProd n (lift 1 0 A')
                                      (tApp (lift 1 1 B2)
                                            [tApp (tRel 1) [proj1 (tRel 0)]])))
  | tLambda n A t ⇒ A' <- tsl_ty_param fuel Σ G E Γ A ;;
                    t' <- tsl_rec2 fuel Σ G E (Γ ,, vass n A) t ;;
                    ret (tLambda n A' t')
  | tLetIn n t A u ⇒ t' <- tsl_term fuel Σ G E Γ t ;;
                     A' <- tsl_ty_param fuel Σ G E Γ A ;;
                     u' <- tsl_rec2 fuel Σ G E (Γ ,, vdef n t A) u ;;
                     ret (tLetIn n t' A' u')
  | tApp t u ⇒ t' <- tsl_rec2 fuel Σ G E Γ t ;;
               u' <- monad_map (tsl_term fuel Σ G E Γ) u ;;
               ret (tApp t' u')
  | tConst _ _ as t
  | tInd _ _ as t
  | tConstruct _ _ _ as t ⇒ t' <- tsl_term fuel Σ G E Γ t ;;
                            ret (proj2 t')
  | _ ⇒ raise TranslationNotHandeled
  end
  end
with tsl_term (fuel : nat) (Σ : global_env) (G : universes_graph) (E : tsl_table) (Γ : context) (t : term) {struct fuel}
  : tsl_result term :=
  match fuel with
  | O ⇒ raise translation_utils.NotEnoughFuel
  | S fuel ⇒
  match t with
  | tRel n ⇒ ret (tRel n)
  | tCast t c A ⇒ t' <- tsl_term fuel Σ G E Γ t ;;
                  A' <- tsl_ty_param fuel Σ G E Γ A ;;
                  ret (tCast t' c A')
  | tConst s univs ⇒ lookup_tsl_table' E (ConstRef s)
  | tInd i univs ⇒ lookup_tsl_table' E (IndRef i)
  | tConstruct i n univs ⇒ lookup_tsl_table' E (ConstructRef i n)
  | t ⇒ match infer Σ G Γ t with
        | Checked typ ⇒ let typ := refresh_universes typ in
                        let t1 := tsl_rec1 0 t in
                        t2 <- tsl_rec2 fuel Σ G E Γ t ;;
                        let typ1 := tsl_rec1 0 typ in
                        typ2 <- tsl_rec2 fuel Σ G E Γ typ ;;
                        ret (pair typ1 typ2 t1 t2)
        | TypeError t ⇒ raise (TypingError t)
        end
  end
  end
where "'tsl_ty_param'" := (fun fuel Σ G E Γ t ⇒
                        let t1 := tsl_rec1 0 t in
                        t2 <- tsl_rec2 fuel Σ G E Γ t ;;
                        ret (pack t1 t2)).

Fixpoint replace t k u {struct u} :=
  match u with
  | tRel n ⇒
    match Nat.compare k n with
    | Datatypes.Eq ⇒ t
    | Datatypes.Gt ⇒ tRel n
    | Datatypes.Lt ⇒ tRel n
    end
  | tEvar ev args ⇒ tEvar ev (List.map (replace t k) args)
  | tLambda na T M ⇒ tLambda na (replace t k T) (replace (lift0 1 t) (S k) M)
  | tApp u v ⇒ tApp (replace t k u) (List.map (replace t k) v)
  | tProd na A B ⇒ tProd na (replace t k A) (replace (lift0 1 t) (S k) B)
  | tCast c kind ty ⇒ tCast (replace t k c) kind (replace t k ty)
  | tLetIn na b ty b' ⇒ tLetIn na (replace t k b) (replace t k ty) (replace (lift0 1 t) (S k) b')
  | tCase ind p c brs ⇒
    let brs' := List.map (on_snd (replace t k)) brs in
    tCase ind (replace t k p) (replace t k c) brs'
  | tProj p c ⇒ tProj p (replace t k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (replace t k) (replace t k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (replace t k) (replace t k')) mfix in
    tCoFix mfix' idx
  | x ⇒ x
  end.

Definition tsl_mind_body (ΣE : tsl_context) (mp : string)
           (kn : kername) (mind : mutual_inductive_body)
  : tsl_result (tsl_table × list mutual_inductive_body).



Defined.

Instance tsl_param : Translation
  := {| tsl_id := tsl_ident ;
        tsl_tm := fun ΣE t ⇒
      match gc_of_uctx (global_ext_uctx (fst ΣE)) with
      | None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
      | Some ctrs ⇒ tsl_term fuel (fst (fst ΣE)) (make_graph ctrs) (snd ΣE) [] t
      end;
        tsl_ty := Some (fun ΣE t ⇒
      match gc_of_uctx (global_ext_uctx (fst ΣE)) with
      | None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
      | Some ctrs ⇒ tsl_ty_param fuel (fst (fst ΣE)) (make_graph ctrs) (snd ΣE) [] t
      end);
        tsl_ind := tsl_mind_body |}.

Notation "'TYPE'" := (sigma Type (fun A ⇒ A → Type)).
Notation "'El' A" := (sigma (π1 A) (π2 A)) (at level 20).

Definition ty := nat → nat.
Definition to := Type.


Check (listᵗ : ∀ (A : TYPE), list A.1 → Type).
Check (nilᵗ : ∀ (A : TYPE), listᵗ A nil).
Check (consᵗ : ∀ (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l),
          listᵗ A (x.1 :: lH.1)).