Library MetaCoq.Translations.param_generous_unpacked

Reserved Notation "'tsl_ty_param'".

Definition tsl_name n :=
  match n with
  | nAnon ⇒ nAnon
  | nNamed n ⇒ nNamed (tsl_ident n)
  end.

Definition mkApps t us := tApp t us. Definition mkApp t u := mkApps t [u].

Fixpoint subst_app (t : term) (us : list term) : term :=
  match t, us with
  | tLambda _ A t, u :: us ⇒ subst_app (t {0 := u}) us
  | _, [] ⇒ t
  | _, _ ⇒ mkApps t us
  end.

Definition default_term := tRel 0.

Definition up := lift 1 0.

Fixpoint tsl_rec0 (E : tsl_table) (t : term) {struct t} : term :=
  match t with
  | tRel k ⇒ tRel (2*k+1)
  | tEvar k ts ⇒ tEvar k (map (tsl_rec0 E) ts)
  | tCast t c a ⇒ tCast (tsl_rec0 E t) c (tsl_rec0 E a)
  | tProd na A B ⇒ tProd na (tsl_rec0 E A)
                  (tProd (tsl_name na) (mkApp (up (tsl_rec1 E A)) (tRel 0))
                         (tsl_rec0 E B))
  | tLambda na A t ⇒ tLambda na (tsl_rec0 E A)
                    (tLambda (tsl_name na) (mkApp (up (tsl_rec1 E A)) (tRel 0))
                             (tsl_rec0 E t))
  | tLetIn na A t u ⇒ tLetIn na (tsl_rec0 E A) (tsl_rec0 E t)
                     (tLetIn (tsl_name na) (mkApp (up (tsl_rec1 E A)) (tRel 0)) (up (tsl_rec1 E t))
                             (tsl_rec0 E u))

  | tApp t us ⇒ let u' := List.fold_right (fun v l ⇒ tsl_rec0 E v :: tsl_rec1 E v :: l) [] us in
                mkApps (tsl_rec0 E t) u'

  | tCase ik t u br ⇒ tCase ik (tsl_rec0 E t) (tsl_rec0 E u)
                            (map (fun x ⇒ (fst x, tsl_rec0 E (snd x))) br)
  | tProj p t ⇒ tProj p (tsl_rec0 E t)
  
  
  | _ ⇒ t
  end
with tsl_rec1 (E : tsl_table) (t : term) {struct t} : term :=
  match t with
  | tRel k ⇒ tRel (2 × k)
  | tSort s ⇒ tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))

  | tProd na A B ⇒ let A0 := tsl_rec0 E A in
                   let A1 := tsl_rec1 E A in
                   let B0 := tsl_rec0 E B in
                   let B1 := tsl_rec1 E B in
                   let ΠAB0 := tProd na A0 (tProd (tsl_name na) (mkApp (up A1) (tRel 0)) B0) in
                   tLambda (nNamed "f") ΠAB0
                           (tProd na (up A0) (tProd (tsl_name na) (subst_app (lift0 2 A1) [tRel 0])
                                                    (subst_app (lift 1 2 B1)
                                                               [tApp (tRel 2) [tRel 1; tRel 0]])))

  | tLambda na A t ⇒ let A0 := tsl_rec0 E A in
                     let A1 := tsl_rec1 E A in
                     tLambda na A0 (tLambda (tsl_name na) (subst_app (up A1) [tRel 0]) (tsl_rec1 E t))

  | tApp t us ⇒ let u' := List.fold_right (fun v l ⇒ tsl_rec0 E v :: tsl_rec1 E v :: l) [] us in
                mkApps (tsl_rec1 E t) u'

  | tLetIn na t A u ⇒ let t0 := tsl_rec0 E t in
                      let t1 := tsl_rec1 E t in
                      let A0 := tsl_rec0 E A in
                      let A1 := tsl_rec1 E A in
                      let u0 := tsl_rec0 E u in
                      let u1 := tsl_rec1 E u in
                      tLetIn na t0 A0 (tLetIn (tsl_name na) (up t1) (subst_app (up A1) [tRel 0]) u1)

  | tCast t c A ⇒ let t0 := tsl_rec0 E t in
                  let t1 := tsl_rec1 E t in
                  let A0 := tsl_rec0 E A in
                  let A1 := tsl_rec1 E A in
                  tCast t1 c (mkApps A1 [tCast t0 c A0])

  | tConst s univs ⇒
    match lookup_tsl_table E (ConstRef s) with
    | Some t ⇒ t
    | None ⇒ default_term
    end
  | tInd i univs ⇒
    match lookup_tsl_table E (IndRef i) with
    | Some t ⇒ t
    | None ⇒ default_term
    end
  | tConstruct i n univs ⇒
    match lookup_tsl_table E (ConstructRef i n) with
    | Some t ⇒ t
    | None ⇒ default_term
    end

  | _ ⇒ todo
  end.




Goal ((fun f : ∀ (A : Type) (Aᵗ : A → Type) (H : A), Aᵗ H → A ⇒
    ∀ (A : Type) (Aᵗ : A → Type) (H : A) (H0 : Aᵗ H), Aᵗ (f A Aᵗ H H0)) (fun (A : Type) (Aᵗ : A → Type) (x : A) (_ : Aᵗ x) ⇒ x)
       = (∀ (A : Type) (Aᵗ : A → Type) (x : A), Aᵗ x → Aᵗ x)).



Fixpoint fold_left_i_aux {A B} (f : A → nat → B → A) (n0 : nat) (l : list B)
         (a0 : A) {struct l} : A
  := match l with
     | [] ⇒ a0
     | b :: l ⇒ fold_left_i_aux f (S n0) l (f a0 n0 b)
     end.
Definition fold_left_i {A B} f := @fold_left_i_aux A B f 0.

Fixpoint monad_map_i_aux {M} {H : Monad M} {A B} (f : nat → A → M B) (n0 : nat) (l : list A) : M (list B)
  := match l with
     | [] ⇒ ret []
     | x :: l ⇒ x' <- (f n0 x) ;;
                l' <- (monad_map_i_aux f (S n0) l) ;;
                ret (x' :: l')
     end.

Definition monad_map_i {M H A B} f := @monad_map_i_aux M H A B f 0.

Fixpoint map_i_aux {A B} (f : nat → A → B) (n0 : nat) (l : list A) : list B
  := match l with
     | [] ⇒ []
     | x :: l ⇒ (f n0 x) :: (map_i_aux f (S n0) l)
     end.

Definition map_i {A B} f := @map_i_aux A B f 0.

Definition tsl_mind_body (E : tsl_table)
           (id : ident) (mind : mutual_inductive_body)
  : tsl_table × list mutual_inductive_body.
Defined.


Definition tTranslate (ΣE : tsl_context) (id : ident)
  : TemplateMonad (option tsl_context) :=
  gr <- tmAbout id ;;
  id' <- tmEval all (tsl_ident id) ;;
  let E := snd ΣE in
  match gr with
  | ConstructRef ind _ ⇒ tmPrint "todo tTranslate" ;; ret None
  | IndRef (mkInd kn n) ⇒
      d <- tmQuoteInductive id ;;
      let d' := tsl_mind_body E id d in
      d' <- tmEval lazy d' ;;
      tmPrint d' ;;
      let entries := map mind_body_to_entry (snd d') in
      
      monad_fold_left (fun _ e ⇒ tmMkInductive e) entries tt ;;
      let decl := InductiveDecl kn d in
      print_nf (id ++ " has been translated as " ++ id') ;;
      ret (Some (decl :: fst ΣE, E ++ snd ΣE)%list)

  | ConstRef kn ⇒
    e <- tmQuoteConstant kn true ;;
    print_nf ("toto1" ++ id) ;;
    match e with
    | ParameterEntry _ ⇒ print_nf (id ++ "is an axiom, not a definition") ;;
                         ret None
    | DefinitionEntry {| definition_entry_type := A;
                         definition_entry_body := t |} ⇒
      print_nf ("toto2 " ++ id) ;;
      
      t0 <- tmEval lazy (tsl_rec0 E t) ;;
      t1 <- tmEval lazy (tsl_rec1 E t) ;;
      A1 <- tmEval lazy (tsl_rec1 E A) ;;
      print_nf ("toto4 " ++ id) ;;
      tmMkDefinition id' t1 ;;
      print_nf ("toto5 " ++ id) ;;
      let decl := {| cst_universes := [];
                     cst_type := A; cst_body := Some t |} in
      let Σ' := ConstantDecl kn decl :: (fst ΣE) in
      let E' := (ConstRef kn, tConst id' []) :: (snd ΣE) in
      print_nf (id ++ " has been translated as " ++ id') ;;
      tmEval all (Some (Σ', E'))
    end
  end.

Definition Ty := Type.
Definition TyTy := Ty → Type.



Definition map_context_decl (f : term → term) (decl : context_decl): context_decl
  := {| decl_name := decl.(decl_name);
        decl_body := option_map f decl.(decl_body); decl_type := f decl.(decl_type) |}.

Notation " Γ ,, d " := (d :: Γ) (at level 20, d at next level, only parsing).

Fixpoint tsl_ctx (E : tsl_table) (Γ : context) : context :=
  match Γ with
  | [] ⇒ []
  
  
  | Γ ,, decl ⇒ let n := decl.(decl_name) in
                let x := decl.(decl_body) in
                let A := decl.(decl_type) in
    tsl_ctx E Γ ,, Build_context_decl n (omap (tsl_rec0 0) x) (tsl_rec0 0 A)
                ,, Build_context_decl (tsl_name n) (omap (lift 1 0 \o tsl_rec1 E 0) x) (mkApps (lift0 1 (tsl_rec1 E 0 A)) [tRel 0])
  end.


Notation "#| Γ |" := (List.length Γ) (at level 0, Γ at level 99, format "#| Γ |") : term_scope.


Lemma tsl_ctx_length E (Γ : context) : #|tsl_ctx E Γ| = 2 × #|Γ|%term.


Notation "( x ; y )" := (exist _ x y).




Definition tsl_table_correct (Σ : global_context) (E : tsl_table) : Type := todo.

Lemma LmapE : @List.map = @seq.map.

Lemma lebE (m n : nat) : (Nat.leb m n) = (m ≤ n).

Lemma term_eqP : Equality.axiom eq_term.

Definition term_eqMixin := EqMixin term_eqP.
Canonical termT_eqype := EqType term term_eqMixin.

Lemma tsl_rec0_lift m n t :
  tsl_rec0 m (lift n m t) = lift (2 × n) m (tsl_rec0 m t).

Lemma lift_mkApps n k t us
  : lift n k (mkApps t us) = mkApps (lift n k t) (map (lift n k) us).


Lemma tsl_rec1_lift E n t :
  
  tsl_rec1 E 0 (lift0 n t) = lift0 (2 × n) (tsl_rec1 E 0 t).






Record hidden T := Hidden {show : T}.
Notation "'hidden" := (show _ (Hidden _ _)).
Lemma hide T (t : T) : t = show T (Hidden T t).



Lemma eq_safe_nth T (l : list T) n n' p p' : n = n' →
  safe_nth l (n; p) = safe_nth l (n'; p') :> T.

    Lemma tsl_rec0_decl_type (Γ : context) (n : nat) (isdecl : (n < #|Γ|%term)%coq_nat) (E : tsl_table) (isdecl' : (2 × n + 1 < #|tsl_ctx E Γ|%term)%coq_nat)
      : tsl_rec0 0 (decl_type (safe_nth Γ (n; isdecl))) =
        decl_type (safe_nth (tsl_ctx E Γ) (2 × n + 1; isdecl')).

Lemma tsl_rec1_decl_type (Γ : context) (n : nat) (E : tsl_table) p p'
  (Γ' := tsl_ctx E Γ) :
  mkApps (lift0 1 (decl_type (safe_nth Γ' ((2 × n); p)))) [tRel 0] =
  decl_type (safe_nth Γ' (2 × n; p')).


Lemma tsl_correct Σ Γ t T (H : Σ ;;; Γ |-- t : T)
  : ∀ E, tsl_table_correct Σ E →
    let Γ' := tsl_ctx E Γ in
    let t0 := tsl_rec0 0 t in
    let t1 := tsl_rec1 E 0 t in
    let T0 := tsl_rec0 0 T in
    let T1 := tsl_rec1 E 0 T in
    Σ ;;; Γ' |-- t0 : T0 ∧ Σ ;;; Γ' |-- t1 : mkApps T1 [t0].