Merge PR coq#18278: Small cleanups around the ssr implementation of a…

…pplyn

Reviewed-by: gares
Co-authored-by: gares <[email protected]>

plugins/ssr/ssrcommon.ml

@@ -460,13 +460,10 @@ let call_on_evar env sigma tac e =
     Exninfo.iraise (e, info)
 
 open Pp
-let pp _ = () (* FIXME *)
 module Intset = Evar.Set
 
 let abs_evars_pirrel env sigma0 (sigma, c0) =
-  pp(lazy(str"==PF_ABS_EVARS_PIRREL=="));
-  pp(lazy(str"c0= " ++ Printer.pr_econstr_env env sigma c0));
-  let c0 = Evarutil.nf_evar sigma0 (Evarutil.nf_evar sigma c0) in
+  let c0 = Evarutil.nf_evar sigma c0 in
   let nenv = env_size env in
   let abs_evar n k =
     let open EConstr in
@@ -477,22 +474,20 @@ let abs_evars_pirrel env sigma0 (sigma, c0) =
     | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn sigma x b t (mkArrow t x.binder_relevance c)
     | NamedDecl.LocalAssum (x,t) -> mkNamedProd sigma x t c in
     let t = Context.Named.fold_inside abs_dc ~init:concl dc in
-    Evarutil.nf_evar sigma0 (Evarutil.nf_evar sigma t) in
+    Evarutil.nf_evar sigma t
+  in
   let rec put evlist c = match EConstr.kind sigma c with
   | Evar (k, a) ->
     if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else
     let n = max 0 (SList.length a - nenv) in
-    let k_ty =
-      Retyping.get_sort_family_of
-        env sigma (Evd.evar_concl (Evd.find_undefined sigma k)) in
+    (* FIXME? this is not the right environment in general *)
+    let k_ty = Retyping.get_sort_family_of env sigma (Evd.evar_concl (Evd.find_undefined sigma k)) in
     let is_prop = k_ty = InProp in
-    let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t
+    let t = abs_evar n k in
+    (k, (n, t, is_prop)) :: put evlist t
   | _ -> EConstr.fold sigma put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
-  let pr_constr t = Printer.pr_econstr_env env sigma (Reductionops.nf_beta env sigma0 t) in
-  pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
-    (fun (k,_) -> Evar.print k) evlist));
   let evplist =
     let depev = List.fold_left (fun evs (_,(_,t,_)) ->
         Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in
@@ -505,11 +500,9 @@ let abs_evars_pirrel env sigma0 (sigma, c0) =
         List.filter (fun (j,_) -> j <> i) ev, evp, sigma
       with e when CErrors.noncritical e -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in
   let c0 = Evarutil.nf_evar sigma c0 in
-  let evlist =
-    List.map (fun (x,(y,t,z)) -> x,(y,Evarutil.nf_evar sigma t,z)) evlist in
-  let evplist =
-    List.map (fun (x,(y,t,z)) -> x,(y,Evarutil.nf_evar sigma t,z)) evplist in
-  pp(lazy(str"c0= " ++ pr_constr c0));
+  let nf (k, (n, t, p)) = (k, (n, Evarutil.nf_evar sigma t, p)) in
+  let evlist = List.map nf evlist in
+  let evplist = List.map nf evplist in
   let rec lookup k i = function
     | [] -> 0, 0
     | (k', (n,_,_)) :: evl -> if k = k' then i,n else lookup k (i + 1) evl in
@@ -526,26 +519,25 @@ let abs_evars_pirrel env sigma0 (sigma, c0) =
       let j = destRel sigma hd in
       mkApp (mkRel j, Array.of_list (List.map (Vars.lift (i-1)) extra_args @ args))
   | _ -> EConstr.map_with_binders sigma ((+) 1) (app extra_args) i c in
-  let rec loopP evlist c i = function
+  let rec loopP evlist accu i = function
+  | [] -> List.rev accu
   | (_, (n, t, _)) :: evl ->
     let t = get evlist (i - 1) t in
     let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in
-    loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl
-  | [] -> c in
+    loopP evlist (RelDecl.LocalAssum (make_annot n Sorts.Relevant, t) :: accu) (i - 1) evl
+  in
   let rec loop c i = function
   | (_, (n, t, _)) :: evl ->
     let evs = Evarutil.undefined_evars_of_term sigma t in
     let t_evplist = List.filter (fun (k,_) -> Intset.mem k evs) evplist in
-    let t = loopP t_evplist (get t_evplist 1 t) 1 t_evplist in
+    let ctx_t = loopP t_evplist [] 1 t_evplist in
+    let t = EConstr.it_mkProd_or_LetIn (get t_evplist 1 t) ctx_t in
     let t = get evlist (i - 1) t in
-    let extra_args =
-      List.map (fun (k,_) -> mkRel (fst (lookup k i evlist)))
-        (List.rev t_evplist) in
+    let extra_args = List.rev_map (fun (k,_) -> mkRel (fst (lookup k i evlist))) t_evplist in
     let c = if extra_args = [] then c else app extra_args 1 c in
     loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl
   | [] -> c in
   let res = loop (get evlist 1 c0) 1 evlist in
-  pp(lazy(str"res= " ++ pr_constr res));
   List.length evlist, res
 
 (* Strip all non-essential dependencies from an abstracted term, generating *)
@@ -811,39 +803,55 @@ let dependent_apply_error =
  * Refine.refine function that handles type classes and evars but fails to
  * handle "dependently typed higher order evars".
  *
+ * Assumes that the type of [t] is a telescope with [n] leading product types.
+ * This is always the case as the only caller of applyn uses it with the output
+ * of abs_evars_pirrel which starts with n lambdas generated by abstraction.
+ * It also assumes [t] starts with [n] Lambda nodes.
+ *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
+let applyn ?(beta=false) ~with_evars ?(first_goes_last=false) n t =
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   if with_evars then
     let refine =
-      Proofview.Goal.enter begin fun gl ->
       Refine.refine ~typecheck:false begin fun sigma ->
-      let env = Proofview.Goal.env gl in
-      let concl = Proofview.Goal.concl gl in
-      let t, ty, args, sigma = saturate ?beta ~bi_types:true env sigma t n in
+      let rec saturate c args sigma n =
+        if n = 0 then args, sigma
+        else match EConstr.kind sigma c with
+        | Lambda (_, argty, c) ->
+          let argty = Reductionops.nf_betaiota env sigma (EConstr.Vars.substl args argty) in
+          let (sigma, x) = Evarutil.new_evar env sigma argty in
+          saturate c (x :: args) sigma (n-1)
+        | _ -> assert false
+      in
+      let _, ty = EConstr.decompose_prod_n_decls sigma n (Retyping.get_type_of env sigma t) in
+      let args, sigma = saturate t [] sigma n in
+      let ty = EConstr.Vars.substl args ty in
+      let args = Array.rev_of_list args in
+      let t = EConstr.mkApp (t, args) in
+      let t = if beta then Reductionops.whd_beta env sigma t else t in
       let sigma = unify_HO env sigma ty concl in
       (* Set our own set of goals. In theory saturate generates them in the
          right order, so we could just return sigma directly, but explicit is
          better than implicit. *)
       let sigma = Evd.push_future_goals (snd @@ Evd.pop_future_goals sigma) in
-      let fold sigma (_, e, _) = match EConstr.kind sigma e with
+      let fold sigma e = match EConstr.kind sigma e with
       | Evar (evk, _) -> Evd.declare_future_goal evk sigma
       | _ -> sigma
       in
-      let sigma = List.fold_left fold sigma args in
+      let sigma = Array.fold_left fold sigma args in
       (sigma, t)
       end
-      end
     in
     Tacticals.tclTHENLIST [
       refine;
-      Proofview.(if with_shelve then shelve_unifiable else tclUNIT ());
+      Proofview.shelve_unifiable;
       Proofview.(if first_goes_last then cycle 1 else tclUNIT ())
     ]
   else
-    Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let env = Proofview.Goal.env gl in
     let sigma = Evd.push_future_goals sigma in
     let hyps = Environ.named_context_val env in
     let inst = EConstr.identity_subst_val hyps in
@@ -855,15 +863,13 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
           | Lambda (_, ty, bo) ->
             let () = if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error in
             let ty = Reductionops.nf_betaiota env sigma ty in
-            let src = Loc.tag Evar_kinds.GoalEvar in
-            let (sigma, evk) = Evarutil.new_pure_evar ~src ~typeclass_candidate:false hyps sigma ty in
+            let (sigma, evk) = Evarutil.new_pure_evar ~typeclass_candidate:false hyps sigma ty in
             loop sigma bo (evk :: args) (n - 1)
           | _ -> assert false
       in
       loop sigma t [] n
     in
     let _, sigma = Evd.pop_future_goals sigma in
-    pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env env sigma t));
 
     let map evk = Proofview.goal_with_state evk (Proofview.Goal.state gl) in
     let sgl = List.rev_map map args in
@@ -889,7 +895,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
   let uct = Evd.evar_universe_context (fst oc) in
   let n, oc = abs_evars_pirrel env sigma oc in
   Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
-  Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n oc)
+  Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ?beta n oc)
     (fun _ -> Proofview.tclZERO dependent_apply_error)
   end
 

plugins/ssr/ssrcommon.mli

@@ -215,13 +215,6 @@ val pf_interp_ty :
 val ssr_n_tac : string -> int -> unit Proofview.tactic
 val donetac : int -> unit Proofview.tactic
 
-val applyn :
-           with_evars:bool ->
-           ?beta:bool ->
-           ?with_shelve:bool ->
-           ?first_goes_last:bool ->
-           int ->
-           EConstr.t -> unit Proofview.tactic
 exception NotEnoughProducts
 val saturate :
            ?beta:bool ->