Slightly less stupid algorithm for simpl fixpoint expansion.

Instead of storing the bare fixpoint and its unfolded body in the term,
incurring a cost for their lifts under contexts, we simply store them
in the side map used to track the relation between a fresh problem evar
and its minimal arity. We also replace the hacky evarmap used to track
instantiation with a mere set.

1 files changed, 22 insertions, 23 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2a612b4737..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,33 +430,37 @@ 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)