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 s ⇒ tSort (if Universe.is_level s then s else fresh_universe)
| tProd na b t ⇒ tProd na b (refresh_universes t)
| tLetIn na b t' t ⇒ tLetIn 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 k ⇒ if ge_dec k n then proj1 t else t
| tEvar k ts ⇒ tEvar k (List.map (tsl_rec1 n) ts)
| tCast t c a ⇒ tCast (tsl_rec1 n t) c (tsl_rec1 n a)
| tProd x A B ⇒ tProd x (tsl_rec1 n A) (tsl_rec1 (n+1) B)
| tLambda x A t ⇒ tLambda x (tsl_rec1 n A) (tsl_rec1 (n+1) t)
| tLetIn x a t u ⇒ tLetIn x (tsl_rec1 n a) (tsl_rec1 n t) (tsl_rec1 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec1 n t) (List.map (tsl_rec1 n) lu)
| tCase ik t u brs ⇒ tCase ik
(map_predicate_k id tsl_rec1 n t) (tsl_rec1 n u)
(map_branches_k tsl_rec1 n brs)
| tProj p t ⇒ tProj 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
| O ⇒ raise translation_utils.NotEnoughFuel
| S fuel ⇒
match t with
| tRel n ⇒ ret (proj2 (tRel n))
| tSort s ⇒ ret (tLambda (nNamed "A") (tSort s)
(tProd nAnon (tRel 0) (tSort s)))
| tCast t c A ⇒ let 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 B ⇒ let Π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 t ⇒ A' <- 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 u ⇒ t' <- 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 u ⇒ t' <- 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 t ⇒ t' <- 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
| O ⇒ raise translation_utils.NotEnoughFuel
| S fuel ⇒
match t with
| tRel n ⇒ ret (tRel n)
| tCast t c A ⇒ t' <- tsl_term fuel Σ G E Γ t ;;
A' <- tsl_ty_param fuel Σ G E Γ A ;;
ret (tCast t' c A')
| tConst s univs ⇒ lookup_tsl_table' E (ConstRef s)
| tInd i univs ⇒ lookup_tsl_table' E (IndRef i)
| tConstruct i n univs ⇒ lookup_tsl_table' E (ConstructRef i n)
| t ⇒ match infer Σ G Γ t with
| Checked typ ⇒ let 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 t ⇒ raise (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.Eq ⇒ t
| Datatypes.Gt ⇒ tRel n
| Datatypes.Lt ⇒ tRel n
end
| tEvar ev args ⇒ tEvar ev (List.map (replace t k) args)
| tLambda na T M ⇒ tLambda na (replace t k T) (replace (lift0 1 t) (S k) M)
| tApp u v ⇒ tApp (replace t k u) (List.map (replace t k) v)
| tProd na A B ⇒ tProd na (replace t k A) (replace (lift0 1 t) (S k) B)
| tCast c kind ty ⇒ tCast (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 c ⇒ tProj 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
| x ⇒ x
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
| None ⇒ raise (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_ctx ⇒ Monomorphic_ctx
| Polymorphic_ctx ctx ⇒ Polymorphic_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 u ⇒ replace 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) |}
| None ⇒ raise 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
| None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
| Some ctrs ⇒ tsl_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
| None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
| Some ctrs ⇒ tsl_ty_param fuel (fst (fst ΣE)) (make_graph ctrs) (snd ΣE) [] t
end);
tsl_ind := tsl_mind_body |}.
Notation "'TYPE'" := (sigma Type (fun A ⇒ A → 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)).
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 s ⇒ tSort (if Universe.is_level s then s else fresh_universe)
| tProd na b t ⇒ tProd na b (refresh_universes t)
| tLetIn na b t' t ⇒ tLetIn 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 k ⇒ if ge_dec k n then proj1 t else t
| tEvar k ts ⇒ tEvar k (List.map (tsl_rec1 n) ts)
| tCast t c a ⇒ tCast (tsl_rec1 n t) c (tsl_rec1 n a)
| tProd x A B ⇒ tProd x (tsl_rec1 n A) (tsl_rec1 (n+1) B)
| tLambda x A t ⇒ tLambda x (tsl_rec1 n A) (tsl_rec1 (n+1) t)
| tLetIn x a t u ⇒ tLetIn x (tsl_rec1 n a) (tsl_rec1 n t) (tsl_rec1 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec1 n t) (List.map (tsl_rec1 n) lu)
| tCase ik t u brs ⇒ tCase ik
(map_predicate_k id tsl_rec1 n t) (tsl_rec1 n u)
(map_branches_k tsl_rec1 n brs)
| tProj p t ⇒ tProj 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
| O ⇒ raise translation_utils.NotEnoughFuel
| S fuel ⇒
match t with
| tRel n ⇒ ret (proj2 (tRel n))
| tSort s ⇒ ret (tLambda (nNamed "A") (tSort s)
(tProd nAnon (tRel 0) (tSort s)))
| tCast t c A ⇒ let 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 B ⇒ let Π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 t ⇒ A' <- 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 u ⇒ t' <- 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 u ⇒ t' <- 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 t ⇒ t' <- 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
| O ⇒ raise translation_utils.NotEnoughFuel
| S fuel ⇒
match t with
| tRel n ⇒ ret (tRel n)
| tCast t c A ⇒ t' <- tsl_term fuel Σ G E Γ t ;;
A' <- tsl_ty_param fuel Σ G E Γ A ;;
ret (tCast t' c A')
| tConst s univs ⇒ lookup_tsl_table' E (ConstRef s)
| tInd i univs ⇒ lookup_tsl_table' E (IndRef i)
| tConstruct i n univs ⇒ lookup_tsl_table' E (ConstructRef i n)
| t ⇒ match infer Σ G Γ t with
| Checked typ ⇒ let 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 t ⇒ raise (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.Eq ⇒ t
| Datatypes.Gt ⇒ tRel n
| Datatypes.Lt ⇒ tRel n
end
| tEvar ev args ⇒ tEvar ev (List.map (replace t k) args)
| tLambda na T M ⇒ tLambda na (replace t k T) (replace (lift0 1 t) (S k) M)
| tApp u v ⇒ tApp (replace t k u) (List.map (replace t k) v)
| tProd na A B ⇒ tProd na (replace t k A) (replace (lift0 1 t) (S k) B)
| tCast c kind ty ⇒ tCast (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 c ⇒ tProj 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
| x ⇒ x
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
| None ⇒ raise (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_ctx ⇒ Monomorphic_ctx
| Polymorphic_ctx ctx ⇒ Polymorphic_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 u ⇒ replace 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) |}
| None ⇒ raise 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
| None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
| Some ctrs ⇒ tsl_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
| None ⇒ raise (TypingError (UnsatisfiableConstraints (snd (global_ext_uctx (fst ΣE)))))
| Some ctrs ⇒ tsl_ty_param fuel (fst (fst ΣE)) (make_graph ctrs) (snd ΣE) [] t
end);
tsl_ind := tsl_mind_body |}.
Notation "'TYPE'" := (sigma Type (fun A ⇒ A → 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)).