Library MetaCoq.Translations.param_generous_unpacked
From MetaCoq.Template Require Import utils All.
From MetaCoq.Translations Require Import translation_utils.
Require Import ssreflect.
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].
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.
MetaCoq Run (tm <- tmQuote (∀ A, A → A) ;;
let tm' := tsl_rec1 [] tm in
tmUnquote tm' >>= tmPrint).
MetaCoq Run (tm <- tmQuote (fun A (x : A) ⇒ x) ;;
let tm' := tsl_rec0 [] tm in
tmUnquote tm' >>= tmPrint).
MetaCoq Run (tm <- tmQuote (fun A (x : A) ⇒ x) ;;
let tm' := tsl_rec1 [] tm in
tmUnquote tm' >>= tmPrint).
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)).
reflexivity.
Defined.
MetaCoq Quote Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
Unset MetaCoq Strict Unquote Universe Mode.
MetaCoq Run (let tm' := tsl_rec1 [] tm in
print_nf tm' ;;
tmUnquote tm' >>= tmPrint).
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.
refine (_, [{| ind_npars := 2 × mind.(ind_npars);
ind_bodies := _ |}]).
- refine (let id' := tsl_ident id in
fold_left_i (fun E i ind ⇒ _ :: _ ++ E) mind.(ind_bodies) []).
+
exact (IndRef (mkInd id i), tInd (mkInd id' i) []).
+
refine (fold_left_i (fun E k _ ⇒ _ :: E) ind.(ind_ctors) []).
exact (ConstructRef (mkInd id i) k, tConstruct (mkInd id' i) k []).
- refine (map_i _ mind.(ind_bodies)).
intros i ind.
refine {| ind_name := tsl_ident ind.(ind_name);
ind_type := _;
ind_kelim := ind.(ind_kelim);
ind_ctors := _;
ind_projs := [] |}. +
refine (let ar := subst_app (tsl_rec1 E ind.(ind_type))
[tInd (mkInd id i) []] in
ar).
+
refine (map_i _ ind.(ind_ctors)).
intros k ((name, typ), nargs).
refine (tsl_ident name, _, 2 × nargs).
refine (subst_app _ [tConstruct (mkInd id i) k []]).
refine (fold_left_i (fun t0 i u ⇒ t0 {S i := u}) _ (tsl_rec1 E typ)).
refine (List.rev (map_i (fun i _ ⇒ tInd (mkInd id i) [])
mind.(ind_bodies))).
Defined.
Definition tTranslate (ΣE : tsl_context) (id : ident)
: TemplateMonad (option tsl_context) :=
gr <- tmLocate 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 true 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))
| 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.
MetaCoq Run (ΣE <- tTranslate ([],[]) "Ty" ;;
let ΣE := option_get todo ΣE in
tTranslate ΣE "TyTy" >>= tmPrint).
Fail MetaCoq Run (tTranslate ([],[]) "nat").
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.
Delimit Scope term_scope with term.
Notation "#| Γ |" := (List.length Γ) (at level 0, Γ at level 99, format "#| Γ |") : term_scope.
Lemma tsl_ctx_length E (Γ : context) : #|tsl_ctx E Γ| = 2 × #|Γ|%term.
Proof.
induction Γ.
reflexivity.
destruct a, decl_body; simpl;
by rewrite IHΓ mulnS.
Qed.
Notation "( x ; y )" := (exist _ x y).
Definition tsl_table_correct (Σ : global_context) (E : tsl_table) : Type := todo.
Lemma LmapE : @List.map = @seq.map.
reflexivity.
Qed.
Lemma lebE (m n : nat) : (Nat.leb m n) = (m ≤ n).
Admitted.
Lemma term_eqP : Equality.axiom eq_term.
Admitted.
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).
Proof.
elim/term_forall_list_ind : t m n ⇒ //=; rewrite ?plusE.
- move⇒ n m k.
rewrite lebE.
case: leqP ⇒ /= mn; rewrite lebE plusE.
rewrite !ifT ?mulnDr ?addnA //.
admit.
admit.
by rewrite leqNgt mn.
- admit.
- by move⇒ t IHt c t0 IHt0 m n; rewrite IHt IHt0.
- by move⇒ n0 t -IHt t0 IHt0 m n /=; rewrite IHt addn1 IHt0.
- by move⇒ n t IHt t0 IHt0 m n0; rewrite IHt addn1 IHt0.
- by move⇒ n t IHt t0 IHt0 t1 IHt1 m n0; rewrite !addn1 IHt IHt0 IHt1.
- move⇒ t IHt l IHl m n; rewrite IHt.
rewrite LmapE.
rewrite -!map_comp.
congr (tApp _ _).
apply/eq_in_map ⇒ i /=.
admit.
- move⇒ p t IHt t0 IHt0 l IHl m n.
rewrite IHt IHt0.
admit.
- by move⇒ s t IHt m n; rewrite IHt.
- admit.
- admit.
Admitted.
Lemma lift_mkApps n k t us
: lift n k (mkApps t us) = mkApps (lift n k t) (map (lift n k) us).
Proof.
done.
Qed.
Arguments subst_app : simpl nomatch.
Lemma tsl_rec1_lift E n t :
tsl_rec1 E 0 (lift0 n t) = lift0 (2 × n) (tsl_rec1 E 0 t).
Proof.
elim/term_forall_list_ind : t n ⇒ //; rewrite ?plusE.
- move⇒ n k.
by rewrite /= mulnDr.
- admit.
- admit.
- admit.
- move⇒ t IHt c t0 IHt0 n /=; rewrite IHt IHt0 ?lift_mkApps.
congr (tCast _ _ (mkApps _ _)).
by rewrite !tsl_rec0_lift.
- move⇒ n t IHt t0 IHt0 n0.
rewrite /=.
rewrite !IHt.
rewrite !tsl_rec0_lift.
Admitted.
Record hidden T := Hidden {show : T}.
Arguments show : simpl never.
Notation "'hidden" := (show _ (Hidden _ _)).
Lemma hide T (t : T) : t = show T (Hidden T t).
Proof. by []. Qed.
Arguments safe_nth : simpl nomatch.
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.
Proof.
move⇒ eq_n; case: _ / eq_n in p p' ×.
elim: l ⇒ [|x l IHl] in n p p' ×.
by inversion p.
by case: n ⇒ [//|n] in p p' *; apply: IHl.
Qed.
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')).
Proof.
elim: Γ ⇒ [|a Γ IHΓ] in n isdecl isdecl' ×.
by inversion isdecl.
simpl.
case: n ⇒ [//|n] in isdecl isdecl' ×.
rewrite addn1 /= in isdecl' ×.
rewrite IHΓ addn1 //.
apply/leP; move/leP : isdecl'.
by rewrite !mul2n doubleS.
move⇒ isdecl''.
congr (decl_type _); apply: eq_safe_nth.
by rewrite plusE addn0 mul2n -addnn addnS.
Qed.
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')).
Proof.
subst Γ'; elim: Γ ⇒ [|a Γ IHΓ] in n p p' ×.
by inversion p.
Admitted.
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].
Proof.
elim/typing_ind: H ⇒ {Γ t T} Γ.
- move⇒ n isdecl E X Γ' /=.
rewrite tsl_rec0_lift mulnS add2n (tsl_rec0_decl_type _ _ _ E).
rewrite tsl_ctx_length.
apply/leP.
by rewrite addn1 mul2n -doubleS -mul2n leq_mul2l; apply/leP.
rewrite !addn1; move⇒ isdecl'.
split; first exact: type_Rel.
have := type_Rel Σ Γ' (2 × n) _.
evar (l : (2 × n < #|Γ'|%term)%coq_nat).
move⇒ /(_ l).
rewrite -tsl_rec1_decl_type /=.
admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- rewrite /= ⇒ t l t' t'' tt' IHt' spine E ΣE_correct; rewrite /mkApps; split.
apply: type_App.
have [] := IHt' _ ΣE_correct.
by move⇒ t0_ty ?; exact: t0_ty.
admit.
apply: type_App.
have [] := IHt' _ ΣE_correct.
by move⇒ ? t1_ty; exact: t1_ty.
admit.
rewrite /Γ' ⇒ isdecl'; clear.
case: Γ isdecl isdecl'.
Require Import Vector.
From MetaCoq.Translations Require Import translation_utils.
Require Import ssreflect.
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].
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.
MetaCoq Run (tm <- tmQuote (∀ A, A → A) ;;
let tm' := tsl_rec1 [] tm in
tmUnquote tm' >>= tmPrint).
MetaCoq Run (tm <- tmQuote (fun A (x : A) ⇒ x) ;;
let tm' := tsl_rec0 [] tm in
tmUnquote tm' >>= tmPrint).
MetaCoq Run (tm <- tmQuote (fun A (x : A) ⇒ x) ;;
let tm' := tsl_rec1 [] tm in
tmUnquote tm' >>= tmPrint).
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)).
reflexivity.
Defined.
MetaCoq Quote Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
Unset MetaCoq Strict Unquote Universe Mode.
MetaCoq Run (let tm' := tsl_rec1 [] tm in
print_nf tm' ;;
tmUnquote tm' >>= tmPrint).
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.
refine (_, [{| ind_npars := 2 × mind.(ind_npars);
ind_bodies := _ |}]).
- refine (let id' := tsl_ident id in
fold_left_i (fun E i ind ⇒ _ :: _ ++ E) mind.(ind_bodies) []).
+
exact (IndRef (mkInd id i), tInd (mkInd id' i) []).
+
refine (fold_left_i (fun E k _ ⇒ _ :: E) ind.(ind_ctors) []).
exact (ConstructRef (mkInd id i) k, tConstruct (mkInd id' i) k []).
- refine (map_i _ mind.(ind_bodies)).
intros i ind.
refine {| ind_name := tsl_ident ind.(ind_name);
ind_type := _;
ind_kelim := ind.(ind_kelim);
ind_ctors := _;
ind_projs := [] |}. +
refine (let ar := subst_app (tsl_rec1 E ind.(ind_type))
[tInd (mkInd id i) []] in
ar).
+
refine (map_i _ ind.(ind_ctors)).
intros k ((name, typ), nargs).
refine (tsl_ident name, _, 2 × nargs).
refine (subst_app _ [tConstruct (mkInd id i) k []]).
refine (fold_left_i (fun t0 i u ⇒ t0 {S i := u}) _ (tsl_rec1 E typ)).
refine (List.rev (map_i (fun i _ ⇒ tInd (mkInd id i) [])
mind.(ind_bodies))).
Defined.
Definition tTranslate (ΣE : tsl_context) (id : ident)
: TemplateMonad (option tsl_context) :=
gr <- tmLocate 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 true 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))
| 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.
MetaCoq Run (ΣE <- tTranslate ([],[]) "Ty" ;;
let ΣE := option_get todo ΣE in
tTranslate ΣE "TyTy" >>= tmPrint).
Fail MetaCoq Run (tTranslate ([],[]) "nat").
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.
Delimit Scope term_scope with term.
Notation "#| Γ |" := (List.length Γ) (at level 0, Γ at level 99, format "#| Γ |") : term_scope.
Lemma tsl_ctx_length E (Γ : context) : #|tsl_ctx E Γ| = 2 × #|Γ|%term.
Proof.
induction Γ.
reflexivity.
destruct a, decl_body; simpl;
by rewrite IHΓ mulnS.
Qed.
Notation "( x ; y )" := (exist _ x y).
Definition tsl_table_correct (Σ : global_context) (E : tsl_table) : Type := todo.
Lemma LmapE : @List.map = @seq.map.
reflexivity.
Qed.
Lemma lebE (m n : nat) : (Nat.leb m n) = (m ≤ n).
Admitted.
Lemma term_eqP : Equality.axiom eq_term.
Admitted.
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).
Proof.
elim/term_forall_list_ind : t m n ⇒ //=; rewrite ?plusE.
- move⇒ n m k.
rewrite lebE.
case: leqP ⇒ /= mn; rewrite lebE plusE.
rewrite !ifT ?mulnDr ?addnA //.
admit.
admit.
by rewrite leqNgt mn.
- admit.
- by move⇒ t IHt c t0 IHt0 m n; rewrite IHt IHt0.
- by move⇒ n0 t -IHt t0 IHt0 m n /=; rewrite IHt addn1 IHt0.
- by move⇒ n t IHt t0 IHt0 m n0; rewrite IHt addn1 IHt0.
- by move⇒ n t IHt t0 IHt0 t1 IHt1 m n0; rewrite !addn1 IHt IHt0 IHt1.
- move⇒ t IHt l IHl m n; rewrite IHt.
rewrite LmapE.
rewrite -!map_comp.
congr (tApp _ _).
apply/eq_in_map ⇒ i /=.
admit.
- move⇒ p t IHt t0 IHt0 l IHl m n.
rewrite IHt IHt0.
admit.
- by move⇒ s t IHt m n; rewrite IHt.
- admit.
- admit.
Admitted.
Lemma lift_mkApps n k t us
: lift n k (mkApps t us) = mkApps (lift n k t) (map (lift n k) us).
Proof.
done.
Qed.
Arguments subst_app : simpl nomatch.
Lemma tsl_rec1_lift E n t :
tsl_rec1 E 0 (lift0 n t) = lift0 (2 × n) (tsl_rec1 E 0 t).
Proof.
elim/term_forall_list_ind : t n ⇒ //; rewrite ?plusE.
- move⇒ n k.
by rewrite /= mulnDr.
- admit.
- admit.
- admit.
- move⇒ t IHt c t0 IHt0 n /=; rewrite IHt IHt0 ?lift_mkApps.
congr (tCast _ _ (mkApps _ _)).
by rewrite !tsl_rec0_lift.
- move⇒ n t IHt t0 IHt0 n0.
rewrite /=.
rewrite !IHt.
rewrite !tsl_rec0_lift.
Admitted.
Record hidden T := Hidden {show : T}.
Arguments show : simpl never.
Notation "'hidden" := (show _ (Hidden _ _)).
Lemma hide T (t : T) : t = show T (Hidden T t).
Proof. by []. Qed.
Arguments safe_nth : simpl nomatch.
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.
Proof.
move⇒ eq_n; case: _ / eq_n in p p' ×.
elim: l ⇒ [|x l IHl] in n p p' ×.
by inversion p.
by case: n ⇒ [//|n] in p p' *; apply: IHl.
Qed.
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')).
Proof.
elim: Γ ⇒ [|a Γ IHΓ] in n isdecl isdecl' ×.
by inversion isdecl.
simpl.
case: n ⇒ [//|n] in isdecl isdecl' ×.
rewrite addn1 /= in isdecl' ×.
rewrite IHΓ addn1 //.
apply/leP; move/leP : isdecl'.
by rewrite !mul2n doubleS.
move⇒ isdecl''.
congr (decl_type _); apply: eq_safe_nth.
by rewrite plusE addn0 mul2n -addnn addnS.
Qed.
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')).
Proof.
subst Γ'; elim: Γ ⇒ [|a Γ IHΓ] in n p p' ×.
by inversion p.
Admitted.
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].
Proof.
elim/typing_ind: H ⇒ {Γ t T} Γ.
- move⇒ n isdecl E X Γ' /=.
rewrite tsl_rec0_lift mulnS add2n (tsl_rec0_decl_type _ _ _ E).
rewrite tsl_ctx_length.
apply/leP.
by rewrite addn1 mul2n -doubleS -mul2n leq_mul2l; apply/leP.
rewrite !addn1; move⇒ isdecl'.
split; first exact: type_Rel.
have := type_Rel Σ Γ' (2 × n) _.
evar (l : (2 × n < #|Γ'|%term)%coq_nat).
move⇒ /(_ l).
rewrite -tsl_rec1_decl_type /=.
admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- rewrite /= ⇒ t l t' t'' tt' IHt' spine E ΣE_correct; rewrite /mkApps; split.
apply: type_App.
have [] := IHt' _ ΣE_correct.
by move⇒ t0_ty ?; exact: t0_ty.
admit.
apply: type_App.
have [] := IHt' _ ΣE_correct.
by move⇒ ? t1_ty; exact: t1_ty.
admit.
rewrite /Γ' ⇒ isdecl'; clear.
case: Γ isdecl isdecl'.
Require Import Vector.