First-order approximation for polymorphic hints.

dev/ci/user-overlays/21164-tabareau-hint-refresh-firstorder-approx.sh

@@ -0,0 +1 @@
+overlay hott https://github.com/jdchristensen/HoTT trunc-universes 21164

proofs/clenv.ml

@@ -135,10 +135,41 @@ let refresh_template_constraints ~metas env sigma ind c =
     let cstrs, _, _ = Inductive.instantiate_template_universes mib univs in
     Evd.add_constraints sigma cstrs
 
-let clenv_refresh env sigma ctx clenv =
+let get_head_ref sigma c =
+  let hd, args = EConstr.decompose_app sigma c in
+  match destRef sigma hd with
+  | (gr, u) -> Some (gr, u, args)
+  | exception DestKO -> None
+
+let is_cumulative env r =  let open GlobRef in match r with
+  | ConstructRef ((mind,_),_) | IndRef (mind,_)  ->
+      let mind = Environ.lookup_mind mind env in
+      Declareops.inductive_is_cumulative mind
+  | _ -> false
+
+let rec first_order_match env sigma bound accu c1 c2 = match get_head_ref sigma c1, get_head_ref sigma c2 with
+| Some (gr1, u1, args1), Some (gr2, u2, args2) ->
+  if QGlobRef.equal env gr1 gr2 && not (is_cumulative env gr1) then
+    let _q1, u1 = UVars.Instance.to_array (EConstr.Unsafe.to_instance u1) in
+    let _q2, u2 = UVars.Instance.to_array (EConstr.Unsafe.to_instance u2) in
+    let accu = Array.fold_left2 (fun accu u u0 -> if Univ.Level.Set.mem u0 bound then Univ.Level.Map.add u0 u accu else accu) accu u1 u2 in
+    Array.fold_left2 (fun accu a1 a2 -> first_order_match env sigma bound accu a1 a2) accu args1 args2
+  else accu
+| None, None | (None, Some _) | (Some _, None) -> accu
+
+let first_order_fresh_instance env sigma ctx ~concl t =
+  let (qvars, uvars), cstrs = ctx in
+  let univ_subst = first_order_match env sigma uvars Univ.Level.Map.empty concl t in
+  let cstrs = Univ.subst_univs_level_constraints univ_subst cstrs in
+  (* TODO: unify qualities too *)
+  let uvars = Univ.Level.Map.fold (fun u _ accu -> Univ.Level.Set.remove u accu) univ_subst uvars in
+  let ((qsubst, usubst), cstrs) = UnivGen.fresh_sort_context_instance ((qvars, uvars), cstrs) in
+  (qsubst, Univ.Level.Map.fold Univ.Level.Map.add univ_subst usubst), cstrs
+
+let clenv_refresh env sigma ~concl ctx clenv =
   match ctx with
   | Some ctx ->
-    let (subst, ctx) = UnivGen.fresh_sort_context_instance ctx in
+    let (subst, ctx) = first_order_fresh_instance env sigma ctx ~concl (fst clenv.templtyp) in
     let emap c = Vars.subst_univs_level_constr subst c in
     let sigma = Evd.merge_sort_context_set Evd.univ_flexible sigma ctx in
     (* Only metas are mentioning the old universes. *)

proofs/clenv.mli

@@ -28,7 +28,7 @@ val clenv_meta_list : clausenv -> Meta.t
 (* Ad-hoc primitives *)
 val update_clenv_evd : clausenv -> evar_map -> Meta.t -> clausenv
 val clenv_strip_proj_params : clausenv -> clausenv
-val clenv_refresh : env -> evar_map -> UnivGen.sort_context_set option -> clausenv -> clausenv
+val clenv_refresh : env -> evar_map -> concl:EConstr.t -> UnivGen.sort_context_set option -> clausenv -> clausenv
 val clenv_arguments : clausenv -> metavariable list
 
 (** subject of clenv (instantiated) *)
@@ -88,3 +88,6 @@ val refiner : clausenv -> unit Proofview.tactic
 [@@ocaml.deprecated]
 
 end
+
+val first_order_fresh_instance : env -> evar_map -> UnivGen.sort_context_set -> concl:types -> types ->
+  UVars.sort_level_subst * UnivGen.sort_context_set

tactics/auto.ml

@@ -69,7 +69,8 @@ let exact h =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let sigma, c = Hints.fresh_hint env sigma h in
+    let concl = Proofview.Goal.concl gl in
+    let sigma, c = Hints.fresh_hint env sigma ~concl h in
     let sigma, t = Typing.type_of env sigma c in
     let concl = Proofview.Goal.concl gl in
     if occur_existential sigma t || occur_existential sigma concl then

tactics/class_tactics.ml

@@ -159,7 +159,8 @@ let e_give_exact flags h =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = project gl in
-  let sigma, c = Hints.fresh_hint env sigma h in
+  let concl = Proofview.Goal.concl gl in
+  let sigma, c = Hints.fresh_hint env sigma ~concl h in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
   Proofview.Unsafe.tclEVARS sigma <*>
   Clenv.unify ~flags ~cv_pb:CUMUL t1 <*> exact_no_check c
@@ -173,7 +174,8 @@ let unify_resolve ~with_evars flags h diff = match diff with
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.project gl in
-  let sigma, c = Hints.fresh_hint env sigma h in
+  let concl = Proofview.Goal.concl gl in
+  let sigma, c = Hints.fresh_hint env sigma ~concl h in
   let clenv = Clenv.mk_clenv_from_n env sigma diff (c, ty) in
   Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv
   end

tactics/eauto.ml

@@ -95,7 +95,8 @@ let e_exact flags h =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let sigma, c = Hints.fresh_hint env sigma h in
+    let concl = Proofview.Goal.concl gl in
+    let sigma, c = Hints.fresh_hint env sigma ~concl h in
     Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c
   end
 

tactics/hints.ml

@@ -1807,15 +1807,19 @@ let connect_hint_clenv h gl =
      below just replaces the metas of sigma by those coming from the clenv. *)
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  Clenv.clenv_refresh env sigma ctx clenv
+  let concl = Proofview.Goal.concl gl in
+  Clenv.clenv_refresh env sigma ~concl ctx clenv
 
-let fresh_hint env sigma h =
-  let { hint_term = c; hint_uctx = ctx } = h in
+let fresh_hint env sigma ?concl h =
+  let { hint_term = c; hint_uctx = ctx; hint_type = ty } = h in
   match h.hint_uctx with
   | None -> sigma, c
   | Some ctx ->
     (* Refresh the instance of the hint *)
-    let (subst, ctx) = UnivGen.fresh_sort_context_instance ctx in
+    let (subst, ctx) = match concl with
+    | None -> UnivGen.fresh_sort_context_instance ctx
+    | Some concl -> Clenv.first_order_fresh_instance env sigma ~concl ctx ty
+    in
     let c = Vars.subst_univs_level_constr subst c in
     let sigma = Evd.merge_sort_context_set Evd.univ_flexible sigma ctx in
     sigma, c

tactics/hints.mli

@@ -222,7 +222,7 @@ val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> de
 
 val make_db_list : hint_db_name list -> hint_db list
 
-val fresh_hint : env -> evar_map -> hint -> evar_map * constr
+val fresh_hint : env -> evar_map -> ?concl:types -> hint -> evar_map * constr
 
 val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
   ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic