Library MetaCoq.Translations.param_original

From MetaCoq.Template Require Import utils All.
From MetaCoq.Translations Require Import translation_utils.
Import MCMonadNotation.

Local Infix "<=" := Nat.leb.

Definition default_term := tVar "constant_not_found".
Definition debug_term msg:= tVar ("debug: " ^ msg).

Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term :=
  match t with
  | tRel kif n k then tRel (2×k-n+1) else t
  | tEvar k tstEvar k (map (tsl_rec0 n) ts)
  | tCast t c atCast (tsl_rec0 n t) c (tsl_rec0 n a)
  | tProd na A BtProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
  | tLambda na A ttLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
  | tLetIn na t A utLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
  | tApp t lutApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
  | tCase ik t u brtCase ik (map_predicate_k id tsl_rec0 n t) (tsl_rec0 n u)
                            (map_branches_k tsl_rec0 n br)
  | tProj p ttProj p (tsl_rec0 n t)
  
  
  | _t
  end.

Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
  let tsl_rec1 := tsl_rec1_app None in
  let debug case symbol :=
      debug_term ("tsl_rec1: " ^ case ^ " " ^ symbol ^ " not found") in
  match t with
  | tLambda na A t
    let A0 := tsl_rec0 0 A in
    let A1 := tsl_rec1_app None E A in
    tLambda na A0 (tLambda (tsl_name tsl_ident na)
                           (subst_app (lift0 1 A1) [tRel 0])
                           (tsl_rec1_app (option_map (lift 2 2) app) E t))
  | tlet t1 :=
  match t with
  | tRel ktRel (2 × k)
  | tSort stLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))

  | tProd na A B
    let A0 := tsl_rec0 0 A in
    let A1 := tsl_rec1 E A in
    let B0 := tsl_rec0 1 B in
    let B1 := tsl_rec1 E B in
    let ΠAB0 := tProd na A0 B0 in
    tLambda (nNamed "f") ΠAB0
      (tProd na (lift0 1 A0)
             (tProd (tsl_name tsl_ident na)
                    (subst_app (lift0 2 A1) [tRel 0])
                    (subst_app (lift 1 2 B1)
                               [tApp (tRel 2) [tRel 1]])))
  | tApp t us
    let us' := concat (map (fun v[tsl_rec0 0 v; tsl_rec1 E v]) us) in
    mkApps (tsl_rec1 E t) us'

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

  | tCast t c Alet t0 := tsl_rec0 0 t in
                  let t1 := tsl_rec1 E t in
                  let A0 := tsl_rec0 0 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 tt
    | Nonedebug "tConst" (string_of_kername s)
    end
  | tInd i univs
    match lookup_tsl_table E (IndRef i) with
    | Some tt
    | Nonedebug "tInd" (match i with mkInd s _string_of_kername s end)
    end
  | tConstruct i n univs
    match lookup_tsl_table E (ConstructRef i n) with
    | Some tt
    | Nonedebug "tConstruct" (match i with mkInd s _string_of_kername s end)
    end
  | tCase ik t u brs as case
    let t' := map_predicate_k id (fun xlift x 0) 1 t in
    let brs' := map_branches_k (fun xlift x 0) 1 brs in
    let case1 := tCase ik t' (tRel 0) brs' in
    match lookup_tsl_table E (IndRef ik.(ci_ind)) with
    | Some (tInd i _univ) ⇒
      let ci' := {| ci_ind := ik.(ci_ind); ci_npar := ik.(ci_npar) × 2; ci_relevance := ik.(ci_relevance) |} in
      tCase ci'
            (map_predicate_k id (fun ktsl_rec1_app (Some (tsl_rec0 0 case1)) E) 0 t)
            (tsl_rec1 E u)
            (map_branches_k (fun ktsl_rec1 E) 0 brs)
    | _debug "tCase" (match ik.(ci_ind) with mkInd s _string_of_kername s end)
    end
  | tProj _ _todo "tsl"
  | tFix _ _ | tCoFix _ _todo "tsl"
  | tVar _ | tEvar _ _todo "tsl"
  | tLambda _ _ _tVar "impossible"
  
  end in
  match app with Some t'mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
               | Nonet1 end
  end.
Definition tsl_rec1 := tsl_rec1_app None.

Definition tsl_mind_body (E : tsl_table) (mp : modpath) (kn : kername)
           (mind : mutual_inductive_body) : tsl_table × list mutual_inductive_body.
  refine (_, [{| ind_npars := 2 × mind.(ind_npars);
                 ind_params := _;
                 ind_bodies := _;
                 ind_universes := mind.(ind_universes);
                 ind_variance := mind.(ind_variance)|}]).   - refine (let kn' : kername := (mp, tsl_ident kn.2) in
            fold_left_i (fun E i ind_ :: _ ++ E) mind.(ind_bodies) []).
    +
      exact (IndRef (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) ++ mind.(ind_params)).
  - refine (mapi _ mind.(ind_bodies)).
    intros i ind.
    refine {| ind_name := tsl_ident ind.(ind_name);
              ind_indices := ind.(ind_indices);
              ind_sort := ind.(ind_sort);
              ind_type := _;
              ind_kelim := ind.(ind_kelim);
              ind_ctors := _;
              ind_projs := [];
              ind_relevance := ind.(ind_relevance) |}.     +
      refine (let ar := subst_app (tsl_rec1 E ind.(ind_type))
                                  [tInd (mkInd kn i) []] in
              ar).
    +
      refine (mapi _ ind.(ind_ctors)).
      intros k c.
      refine {| cstr_name := tsl_ident c.(cstr_name); cstr_arity := 2 × c.(cstr_arity) |}%nat.
      exact c.(cstr_args).       exact c.(cstr_indices).
      refine (subst_app _ [tConstruct (mkInd kn i) k []]).
      refine (fold_left_i (fun t0 i ut0 {S i := u}) _ (tsl_rec1 E c.(cstr_type))).
      refine (rev (mapi (fun i _tInd (mkInd kn i) [])
                              mind.(ind_bodies))).
Defined.

MetaCoq Run (typ <- tmQuote ( A, A A) ;;
                     typ' <- tmEval all (tsl_rec1 [] typ) ;;
                     tm <- tmQuote (fun A (x : A) ⇒ x) ;;
                     tm' <- tmEval all (tsl_rec1 [] tm) ;;
                     tmUnquote (tApp typ' [tm]) >>= tmDebug).

#[export] Instance param : Translation :=
  {| tsl_id := tsl_ident ;
     tsl_tm := fun ΣE tret (tsl_rec1 (snd ΣE) t) ;
     
     tsl_ty := None ;
     tsl_ind := fun ΣE mp kn mind
     ret (tsl_mind_body (snd ΣE) mp kn mind) |}.

Definition T := A, A A.
MetaCoq Run (Translate emptyTC "T").

Definition tm := ((fun A (x:A) ⇒ x) (Type Type) (fun xx)).
MetaCoq Run (Translate emptyTC "tm").

MetaCoq Run (TC <- Translate emptyTC "nat" ;;
                     tmDefinition "nat_TC" TC ).

MetaCoq Run (TC <- Translate nat_TC "bool" ;;
                     tmDefinition "bool_TC" TC ).
Import Init.Nat.