Library MetaRocq.Translations.param_original
From MetaRocq.Utils Require Import utils.
From MetaRocq.Template Require Import All.
From MetaRocq.Translations Require Import translation_utils.
Import MRMonadNotation.
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 k ⇒ if n ≤ k then tRel (2*k-n+1) else t
| tEvar k ts ⇒ tEvar k (map (tsl_rec0 n) ts)
| tCast t c a ⇒ tCast (tsl_rec0 n t) c (tsl_rec0 n a)
| tProd na A B ⇒ tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
| tLambda na A t ⇒ tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
| tLetIn na t A u ⇒ tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
| tCase ik t u br ⇒ tCase ik (map_predicate_k id tsl_rec0 n t) (tsl_rec0 n u)
(map_branches_k tsl_rec0 n br)
| tProj p t ⇒ tProj 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))
| t ⇒ let t1 :=
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 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 A ⇒ 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
tCast t1 c (mkApps A1 [tCast t0 c A0])
| tConst s univs ⇒
match lookup_tsl_table E (ConstRef s) with
| Some t ⇒ t
| None ⇒ debug "tConst" (string_of_kername s)
end
| tInd i univs ⇒
match lookup_tsl_table E (IndRef i) with
| Some t ⇒ t
| None ⇒ debug "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 t ⇒ t
| None ⇒ debug "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 x ⇒ lift x 0) 1 t in
let brs' := map_branches_k (fun x ⇒ lift 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 k ⇒ tsl_rec1_app (Some (tsl_rec0 0 case1)) E) 0 t)
(tsl_rec1 E u)
(map_branches_k (fun k ⇒ tsl_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"
| tInt _ | tFloat _ | tArray _ _ _ _ | tString _ ⇒ todo "tsl"
end in
match app with Some t' ⇒ mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
| None ⇒ t1 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 u ⇒ t0 {S i := u}) _ (tsl_rec1 E c.(cstr_type))).
refine (rev (mapi (fun i _ ⇒ tInd (mkInd kn i) [])
mind.(ind_bodies))).
Defined.
MetaRocq 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 t ⇒ ret (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.
MetaRocq Run (Translate emptyTC "T").
Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
MetaRocq Run (Translate emptyTC "tm").
MetaRocq Run (TC <- Translate emptyTC "nat" ;;
tmDefinition "nat_TC" TC ).
MetaRocq Run (TC <- Translate nat_TC "bool" ;;
tmDefinition "bool_TC" TC ).
Import Init.Nat.
From MetaRocq.Template Require Import All.
From MetaRocq.Translations Require Import translation_utils.
Import MRMonadNotation.
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 k ⇒ if n ≤ k then tRel (2*k-n+1) else t
| tEvar k ts ⇒ tEvar k (map (tsl_rec0 n) ts)
| tCast t c a ⇒ tCast (tsl_rec0 n t) c (tsl_rec0 n a)
| tProd na A B ⇒ tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
| tLambda na A t ⇒ tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
| tLetIn na t A u ⇒ tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
| tCase ik t u br ⇒ tCase ik (map_predicate_k id tsl_rec0 n t) (tsl_rec0 n u)
(map_branches_k tsl_rec0 n br)
| tProj p t ⇒ tProj 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))
| t ⇒ let t1 :=
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 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 A ⇒ 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
tCast t1 c (mkApps A1 [tCast t0 c A0])
| tConst s univs ⇒
match lookup_tsl_table E (ConstRef s) with
| Some t ⇒ t
| None ⇒ debug "tConst" (string_of_kername s)
end
| tInd i univs ⇒
match lookup_tsl_table E (IndRef i) with
| Some t ⇒ t
| None ⇒ debug "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 t ⇒ t
| None ⇒ debug "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 x ⇒ lift x 0) 1 t in
let brs' := map_branches_k (fun x ⇒ lift 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 k ⇒ tsl_rec1_app (Some (tsl_rec0 0 case1)) E) 0 t)
(tsl_rec1 E u)
(map_branches_k (fun k ⇒ tsl_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"
| tInt _ | tFloat _ | tArray _ _ _ _ | tString _ ⇒ todo "tsl"
end in
match app with Some t' ⇒ mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
| None ⇒ t1 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 u ⇒ t0 {S i := u}) _ (tsl_rec1 E c.(cstr_type))).
refine (rev (mapi (fun i _ ⇒ tInd (mkInd kn i) [])
mind.(ind_bodies))).
Defined.
MetaRocq 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 t ⇒ ret (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.
MetaRocq Run (Translate emptyTC "T").
Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
MetaRocq Run (Translate emptyTC "tm").
MetaRocq Run (TC <- Translate emptyTC "nat" ;;
tmDefinition "nat_TC" TC ).
MetaRocq Run (TC <- Translate nat_TC "bool" ;;
tmDefinition "bool_TC" TC ).
Import Init.Nat.