Merge branch 'coq-8.8' into coq-8.9

translations/param_cheap_packed.v

@@ -9,6 +9,7 @@ Open Scope list_scope.
 Open Scope sigma_scope.
 
 Local Existing Instance config.default_checker_flags.
+Local Existing Instance Checker.default_fuel.
 
 
 Fixpoint refresh_universes (t : term) {struct t} :=
@@ -131,11 +132,11 @@ Fixpoint replace t k u {struct u} :=
   | 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')) mfix 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')) mfix in
+    let mfix' := List.map (map_def (replace t k) (replace t k')) mfix in
     tCoFix mfix' idx
   | x => x
   end.
@@ -194,6 +195,7 @@ Definition tsl_mind_body (ΣE : tsl_context) (mp : string)
       (* refine (fold_left_i (fun E k _ => _ :: E) ind.(ind_ctors) []). *)
       (* exact (ConstructRef (mkInd id i) k, tConstruct (mkInd id' i) k []). *)
       refine [].
+  - (* FIXME don't know what to do *) refine (mind.(ind_params)).
 Defined.
 
 

translations/param_generous_packed.v

@@ -36,6 +36,7 @@ Fixpoint refresh_universes (t : term) {struct t} :=
 
 Local Instance tit : config.checker_flags
   := {| config.check_univs := false |}.
+Existing Instance Checker.default_fuel.
 
 (* if b it is the first translation, else the second *)
 Fixpoint tsl_rec (fuel : nat) (Σ : global_context) (E : tsl_table) (Γ : context)

translations/param_original.v

@@ -27,6 +27,13 @@ Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term :=
   | _ => t
   end.
 
+Fixpoint subst_app (t : term) (us : list term) : term :=
+  match t, us with
+  | tLambda _ A t, u :: us => subst_app (t {0 := u}) us
+  | _, [] => t
+  | _, _ => mkApps t us
+  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 :=
@@ -114,6 +121,7 @@ Definition tsl_rec1 := tsl_rec1_app None.
 Definition tsl_mind_body (E : tsl_table) (mp : string) (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)|}]).  (* FIXME always ok? *)
   - refine (let kn' := tsl_kn tsl_ident kn mp in
@@ -123,6 +131,8 @@ Definition tsl_mind_body (E : tsl_table) (mp : string) (kn : kername)
     + (* ctors *)
       refine (fold_left_i (fun E k _ => _ :: E) ind.(ind_ctors) []).
       exact (ConstructRef (mkInd kn i) k, tConstruct (mkInd kn' i) k []).
+  - (* params: 2 times the same parameters? Probably wrong *)
+    refine (mind.(ind_params) ++ mind.(ind_params))%list.
   - refine (map_i _ mind.(ind_bodies)).
     intros i ind.
     refine {| ind_name := tsl_ident ind.(ind_name);
@@ -176,7 +186,10 @@ Run TemplateProgram (Translate emptyTC "tm").
 Run TemplateProgram (TC <- Translate emptyTC "nat" ;;
                      tmDefinition "nat_TC" TC ).
 
-Run TemplateProgram (Translate nat_TC "pred").
+Run TemplateProgram (TC <- Translate nat_TC "bool" ;;
+                     tmDefinition "bool_TC" TC ).
+
+Run TemplateProgram (Translate bool_TC "pred").
 
 
 Module Id1.

translations/times_bool_fun.v

@@ -34,6 +34,7 @@ Definition pairTrue typ tm := tApp tpair [typ; tbool; tm; ttrue].
 
 
 Local Instance tit : config.checker_flags := {| config.check_univs := false |}.
+Existing Instance Checker.default_fuel.
 
 Fixpoint tsl_rec (fuel : nat) (Σ : global_context) (E : tsl_table) (Γ : context) (t : term) {struct fuel}
   : tsl_result term :=
@@ -115,6 +116,12 @@ Fixpoint replace pat u t {struct t} :=
     | _ => t (* todo *)
     end.
 
+Fixpoint subst_app (t : term) (us : list term) : term :=
+  match t, us with
+  | tLambda _ A t, u :: us => subst_app (t {0 := u}) us
+  | _, [] => t
+  | _, _ => mkApps t us
+  end.
 
 (* If tm of type typ = Π [A0] [A1] ... . [B], returns *)
 (* a term of type [Π A0 A1 ... . B] *)
@@ -140,9 +147,10 @@ Definition tsl_mind_body (ΣE : tsl_context) (mp : string) (kn : kername)
                              | Error _ => todo
                              end in
           let kn' := tsl_kn tsl_ident kn mp in _).
-  refine (let LI := List.split (map_i _ mind.(ind_bodies)) in
+  unshelve refine (let LI := List.split (map_i _ mind.(ind_bodies)) in
           ret (List.concat (fst LI),
                [{| ind_npars := mind.(ind_npars);
+                   ind_params := _;
                    ind_bodies := snd LI;
                    ind_universes := mind.(ind_universes)|}])). (* FIXME always ok? *)
   intros i ind.
@@ -182,6 +190,9 @@ Definition tsl_mind_body (ΣE : tsl_context) (mp : string) (kn : kername)
                           mind.(ind_bodies) ctor_type').
   + (* table *)
     refine (IndRef (mkInd kn i), pouet (tInd (mkInd kn' i) []) ind_type').
+  + (* parameters *)
+    simple refine (List.fold_left _ (mind.(ind_params)) []).
+    exact (fun Γ' A => Γ' ,, vass (decl_name A) (tsl Γ' (decl_type A))).
 Defined.
 
 

translations/translation_utils.v

@@ -258,7 +258,7 @@ Definition ImplementExisting {tsl : Translation} (ΣE : tsl_context) (id : ident
                           ++ id ++ " has not enough constructors. This is a bug.")
       | Some (_, ty, _) =>  (* keep id? *)
         tmDebug "plop3" ;;
-        let A := substl (inds kn [] (* FIXME uctx *) (ind_bodies d)) ty in
+        let A := subst0 (inds kn [] (* FIXME uctx *) (ind_bodies d)) ty in
         tmDebug "plop4" ;;
         tA' <- tmEval lazy (tsl_ty ΣE A) ;;
         tmDebug "plop5" ;;