Library MetaCoq.Translations.param_cheap_packed

From MetaCoq.Template Require Import utils All Checker.
From MetaCoq.Translations Require Import translation_utils sigma.

Import MCMonadNotation.
Local Existing Instance config.default_checker_flags.
Local Existing Instance default_fuel.

Fixpoint refresh_universes (t : term) {struct t} :=
  match t with
  | tSort stSort (if Universe.is_level s then s else fresh_universe)
  | tProd na b ttProd na b (refresh_universes t)
  | tLetIn na b t' ttLetIn 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 kif ge_dec k n then proj1 t else t
  | tEvar k tstEvar k (List.map (tsl_rec1 n) ts)
  | tCast t c atCast (tsl_rec1 n t) c (tsl_rec1 n a)
  | tProd x A BtProd x (tsl_rec1 n A) (tsl_rec1 (n+1) B)
  | tLambda x A ttLambda x (tsl_rec1 n A) (tsl_rec1 (n+1) t)
  | tLetIn x a t utLetIn x (tsl_rec1 n a) (tsl_rec1 n t) (tsl_rec1 (n+1) u)
  | tApp t lutApp (tsl_rec1 n t) (List.map (tsl_rec1 n) lu)
  | tCase ik t u brstCase ik
      (map_predicate_k id tsl_rec1 n t) (tsl_rec1 n u)
      (map_branches_k tsl_rec1 n brs)
  | tProj p ttProj 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
  | Oraise translation_utils.NotEnoughFuel
  | S fuel
  match t with
  | tRel nret (proj2 (tRel n))
  | tSort sret (tLambda (nNamed "A") (tSort s)
                           (tProd nAnon (tRel 0) (tSort s)))
  | tCast t c Alet 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 Blet Π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 tA' <- 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 ut' <- 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 ut' <- 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 tt' <- 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
  | Oraise translation_utils.NotEnoughFuel
  | S fuel
  match t with
  | tRel nret (tRel n)
  | tCast t c At' <- tsl_term fuel Σ G E Γ t ;;
                  A' <- tsl_ty_param fuel Σ G E Γ A ;;
                  ret (tCast t' c A')
  | tConst s univslookup_tsl_table' E (ConstRef s)
  | tInd i univslookup_tsl_table' E (IndRef i)
  | tConstruct i n univslookup_tsl_table' E (ConstructRef i n)
  | tmatch infer Σ G Γ t with
        | Checked typlet 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 traise (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.Eqt
    | Datatypes.GttRel n
    | Datatypes.LttRel n
    end
  | tEvar ev argstEvar ev (List.map (replace t k) args)
  | tLambda na T MtLambda na (replace t k T) (replace (lift0 1 t) (S k) M)
  | tApp u vtApp (replace t k u) (List.map (replace t k) v)
  | tProd na A BtProd na (replace t k A) (replace (lift0 1 t) (S k) B)
  | tCast c kind tytCast (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 p' := map_predicate_k id (replace t) k p in
    let brs' := map_branches_k (replace t) k brs in
    tCase ind p' (replace t k c) brs'
  | tProj p ctProj 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
  | xx
  end.

Definition tsl_mind_body (ΣE : tsl_context) (mp : modpath)
           (kn : kername) (mind : mutual_inductive_body)
  : tsl_result (tsl_table × list mutual_inductive_body).
  refine (
      let Σ := fst (fst ΣE) in
      match gc_of_uctx (global_ext_uctx (fst ΣE)) with
      | Noneraise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
      | Some ctrs
        let G := make_graph ctrs in
        let E := snd ΣE in
        let tsl_ty' := tsl_ty_param fuel Σ G E [] in
        let tsl2' := tsl_rec2 fuel Σ G E [] in
        let kn' : kername := (mp, tsl_ident (snd kn)) in _ end).
  simple refine (let arities := List.map ind_type mind.(ind_bodies) in
                 arities2 <- monad_map tsl2' arities ;;
                 bodies <- _ ;;
                 ret (_, [{| ind_npars := mind.(ind_npars);
                             ind_bodies := bodies ;
                 ind_universes := match mind.(ind_universes) with
                  | Monomorphic_ctxMonomorphic_ctx
                  | Polymorphic_ctx ctxPolymorphic_ctx ctx
                 end;
                 ind_variance := mind.(ind_variance) |}])).   simple refine (let L : list term := _ in _).

  - refine (let n := List.length arities - 1 in
            let L := List.combine arities arities2 in
            List.rev (mapi (fun i '(a,a2)pair a a2 (tInd (mkInd kn i) []) (tRel (n-i))) L)).

  -
    refine (monad_map_i _ mind.(ind_bodies)).
    intros i ind.
    refine (A <- _ ;; ctors <- _ ;;
            ret {| ind_name := tsl_ident ind.(ind_name);
                   ind_sort := ind.(ind_sort);
                   ind_indices := ind.(ind_indices);
                   ind_type := A;
                   ind_kelim := ind.(ind_kelim);
                   ind_ctors := ctors;
                   ind_projs := [];
                   ind_relevance := ind.(ind_relevance) |}).     +
      refine (t2 <- tsl2' ind.(ind_type) ;;
              let i1 := tsl_rec1 0 (tInd (mkInd kn i) []) in
              ret (try_reduce (fst (fst ΣE)) [] fuel (mkApp t2 i1))).
    +
      refine (monad_map_i _ ind.(ind_ctors)).
      intros k c.
      refine (t2 <- tsl2' c.(cstr_type) ;;
              let t2 := fold_left_i (fun t i ureplace u i t) L t2 in
              let c1 := tsl_rec1 0 (tConstruct (mkInd kn i) k []) in
              match reduce_opt RedFlags.default (fst (fst ΣE)) []
                               fuel (mkApp t2 c1) with
              | Some t'ret
                {| cstr_name := tsl_ident c.(cstr_name);
                   cstr_type := t';
                   cstr_args := c.(cstr_args);
                   cstr_indices := c.(cstr_indices);
                   cstr_arity := c.(cstr_arity) |}
              | Noneraise TranslationNotHandeled
              end).

  - refine (let L := List.combine mind.(ind_bodies) arities2 in
            fold_left_i (fun E i '(ind,a2)_ :: _ ++ E) L []).
    +
      refine (IndRef (mkInd kn i), pair ind.(ind_type) a2 (tInd (mkInd kn i) []) (tInd (mkInd kn' i) [])).
    +
      refine (fold_left_i (fun E k __ :: E) ind.(ind_ctors) []).
      exact (ConstructRef (mkInd kn i) k, tConstruct (mkInd kn' i) k []).
  - exact mind.(ind_finite).
  - refine (mind.(ind_params)).
Defined.

#[export] Instance tsl_param : Translation
  := {| tsl_id := tsl_ident ;
        tsl_tm := fun ΣE t
      match gc_of_uctx (global_ext_uctx (fst ΣE)) with
      | Noneraise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
      | Some ctrstsl_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
      | Noneraise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
      | Some ctrstsl_ty_param fuel (fst (fst ΣE)) (make_graph ctrs) (snd ΣE) [] t
      end);
        tsl_ind := tsl_mind_body |}.

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

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

MetaCoq Run (Translate emptyTC "nat" >>= tmDebug).

Require Vector.
Require Even.
Unset Universe Checking.
MetaCoq Run (Translate emptyTC "list" >>= tmDebug).
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)).