Merge PR #13771: Slightly less stupid algorithm for simpl fixpoint expansion + cleanups

Reviewed-by: mattam82

1 files changed, 74 insertions, 74 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a103699716..430813e874 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -384,11 +384,6 @@ let x = Name default_dependent_ident
    do so that the reduction uses this extra information *)
 
 let dummy = mkProp
-let vfx = Id.of_string "_expanded_fix_"
-let vfun = Id.of_string "_eliminator_function_"
-let venv = let open Context.Named.Declaration in
-  val_of_named_context [LocalAssum (make_annot vfx Sorts.Relevant, dummy);
-                        LocalAssum (make_annot vfun Sorts.Relevant, dummy)]
 
 (* Mark every occurrence of substituted vars (associated to a function)
    as a problem variable: an evar that can be instantiated either by
@@ -403,10 +398,10 @@ let substl_with_function subst sigma constr =
       match v.(i-k-1) with
       | (fx, Some (min, ref)) ->
         let sigma = !evd in
-        let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in
+        let (sigma, evk) = Evarutil.new_pure_evar empty_named_context_val sigma dummy in
         evd := sigma;
-        minargs := Evar.Map.add evk min !minargs;
-        Vars.lift k (mkEvar (evk, [fx; ref]))
+        minargs := Evar.Map.add evk (min, fx, ref) !minargs;
+        mkEvar (evk, [])
       | (fx, None) -> Vars.lift k fx
     else mkRel (i - Array.length v)
   | _ ->
@@ -419,14 +414,14 @@ exception Partial
 (* each problem variable that cannot be made totally applied even by
    reduction is solved by the expanded fix term. *)
 let solve_arity_problem env sigma fxminargs c =
-  let evm = ref sigma in
-  let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
+  let set = ref Evar.Set.empty in
+  let set_fix i = set := Evar.Set.add i !set in
   let rec check strict c =
     let c' = whd_betaiotazeta env sigma c in
     let (h,rcargs) = decompose_app_vect sigma c' in
     match EConstr.kind sigma h with
-        Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
-          let minargs = Evar.Map.find i fxminargs in
+        Evar(i,_) when Evar.Map.mem i fxminargs && not (Evar.Set.mem i !set) ->
+          let minargs, _, _ = Evar.Map.find i fxminargs in
           if Array.length rcargs < minargs then
             if strict then set_fix i
             else raise Partial;
@@ -435,45 +430,95 @@ let solve_arity_problem env sigma fxminargs c =
           (let ev, u = destEvalRefU sigma h in
              match reference_opt_value env sigma ev u with
              | Some h' ->
-                let bak = !evm in
+                let bak = !set in
                 (try Array.iter (check false) rcargs
                 with Partial ->
-                  evm := bak;
+                  set := bak;
                   check strict (mkApp(h',rcargs)))
             | None -> Array.iter (check strict) rcargs)
       | _ -> EConstr.iter sigma (check strict) c' in
   check true c;
-  !evm
+  !set
 
 let substl_checking_arity env subst sigma c =
   (* we initialize the problem: *)
   let body,sigma,minargs = substl_with_function subst sigma c in
   (* we collect arity constraints *)
-  let sigma' = solve_arity_problem env sigma minargs body in
+  let ans = solve_arity_problem env sigma minargs body in
   (* we propagate the constraints: solved problems are substituted;
      the other ones are replaced by the function symbol *)
-  let rec nf_fix c = match EConstr.kind sigma c with
-  | Evar (i,[fx;f]) when Evar.Map.mem i minargs ->
+  let rec nf_fix k c = match EConstr.kind sigma c with
+  | Evar (i, []) ->
     (* FIXME: find a less hackish way of doing this *)
-    begin match EConstr.kind sigma' c with
-    | Evar _ -> f
-    | c -> EConstr.of_kind c
+    begin match Evar.Map.find i minargs with
+    | (_, fx, ref) ->
+      if Evar.Set.mem i ans then Vars.lift k fx
+      else Vars.lift k ref
+    | exception Not_found ->
+      (* An argumentless evar that was not generated by substl_with_function *)
+      c
     end
-  | _ -> EConstr.map sigma nf_fix c
+  | _ -> EConstr.map_with_binders sigma succ nf_fix k c
   in
-  nf_fix body
+  nf_fix 0 body
 
 type fix_reduction_result = NotReducible | Reduced of (constr * constr list)
 
 let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
+  let (names, (nbfix, lv, n)), u, largs = f in
+  let lu = List.firstn n largs in
+  let p = List.length lv in
+  let lyi = List.map fst lv in
+  let la =
+    List.map_i (fun q aq ->
+      (* k from the comment is q+1 *)
+      try mkRel (p+1-(List.index Int.equal (n-q) lyi))
+      with Not_found -> Vars.lift p aq)
+      0 lu
+  in
+  let f i = match names.(i) with
+  | None -> None
+  | Some (minargs,ref) ->
+      let body = applist (mkEvalRef ref u, la) in
+      let g =
+        List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
+          let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in
+          let tij' = Vars.substl (List.rev subst) tij in
+          let x = make_annot x Sorts.Relevant in  (* TODO relevance *)
+          mkLambda (x,tij',c)) 1 body (List.rev lv)
+      in Some (minargs,g)
+  in
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = List.init nbodies make_Fi in
-  substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum))
+  let c = substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) in
+  nf_beta env sigma c
 
 let contract_cofix_use_function env sigma f
-  (bodynum,(_names,_,bodies as typedbodies)) =
+  (bodynum,(names,_,bodies as typedbodies)) args =
+  let f =
+    if isConst sigma f then
+      let minargs = List.length args in
+      fun i ->
+        if Int.equal i bodynum then Some (minargs, f)
+        else match names.(i).binder_name with
+          | Anonymous -> None
+          | Name id ->
+              (* In case of a call to another component of a block of
+                  mutual inductive, try to reuse the global name if
+                  the block was indeed initially built as a global
+                  definition *)
+              let (kn, u) = destConst sigma f in
+              let kn = Constant.change_label kn (Label.of_id id) in
+              let cst = (kn, EInstance.kind sigma u) in
+              try match constant_opt_value_in env cst with
+                | None -> None
+                    (* TODO: check kn is correct *)
+                | Some _ -> Some (minargs,mkConstU (kn, u))
+              with Not_found -> None
+    else
+      fun _ -> None in
   let nbodies = Array.length bodies in
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = List.init nbodies make_Fi in
@@ -503,7 +548,7 @@ let reduce_mind_case env sigma mia =
         mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
-let reduce_mind_case_use_function func env sigma mia =
+let reduce_mind_case_use_function f env sigma mia =
   match EConstr.kind sigma mia.mconstr with
     | Construct ((_, i as cstr),u) ->
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
@@ -512,30 +557,8 @@ let reduce_mind_case_use_function func env sigma mia =
         let br = it_mkLambda_or_LetIn (snd br) ctx in
         applist (br, real_cargs)
     | CoFix (bodynum,(names,_,_) as cofix) ->
-        let build_cofix_name =
-          if isConst sigma func then
-            let minargs = List.length mia.mcargs in
-            fun i ->
-              if Int.equal i bodynum then Some (minargs,func)
-              else match names.(i).binder_name with
-                | Anonymous -> None
-                | Name id ->
-                    (* In case of a call to another component of a block of
-                       mutual inductive, try to reuse the global name if
-                       the block was indeed initially built as a global
-                       definition *)
-                    let (kn, u) = destConst sigma func in
-                    let kn = Constant.change_label kn (Label.of_id id) in
-                    let cst = (kn, EInstance.kind sigma u) in
-                    try match constant_opt_value_in env cst with
-                      | None -> None
-                          (* TODO: check kn is correct *)
-                      | Some _ -> Some (minargs,mkConstU (kn, u))
-                    with Not_found -> None
-          else
-            fun _ -> None in
         let cofix_def =
-          contract_cofix_use_function env sigma build_cofix_name cofix in
+          contract_cofix_use_function env sigma f cofix mia.mcargs in
         mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
@@ -686,7 +709,7 @@ let rec red_elim_const env sigma ref u largs =
         let f = ([|Some (minfxargs,ref)|],infos), u, largs in
         (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
            | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
+           | Reduced (c,rest) -> (c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
         let rec descend (ref,u) args =
           let c = reference_value env sigma ref u in
@@ -700,7 +723,7 @@ let rec red_elim_const env sigma ref u largs =
         let f = refinfos, u, midargs in
         (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
            | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
+           | Reduced (c,rest) -> (c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value env sigma ref u in
            (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
@@ -825,29 +848,6 @@ and reduce_fix_use_function env sigma f fix stack =
         let stack' = List.assign stack recargnum (applist recarg') in
         (match EConstr.kind sigma recarg'hd with
            | Construct _ ->
-              let (names, (nbfix, lv, n)), u, largs = f in
-              let lu = List.firstn n largs in
-              let p = List.length lv in
-              let lyi = List.map fst lv in
-              let la =
-                List.map_i (fun q aq ->
-                  (* k from the comment is q+1 *)
-                  try mkRel (p+1-(List.index Int.equal (n-q) lyi))
-                  with Not_found -> Vars.lift p aq)
-                  0 lu
-              in
-              let f i = match names.(i) with
-              | None -> None
-              | Some (minargs,ref) ->
-                  let body = applist (mkEvalRef ref u, la) in
-                  let g =
-                    List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
-                      let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in
-                      let tij' = Vars.substl (List.rev subst) tij in
-                      let x = make_annot x Sorts.Relevant in  (* TODO relevance *)
-                      mkLambda (x,tij',c)) 1 body (List.rev lv)
-                  in Some (minargs,g)
-              in
                Reduced (contract_fix_use_function env sigma f fix,stack')
            | _ -> NotReducible)