Smarter algorithm to build frozen_and_pending_holes

SkySkimmer · Sep 15, 2023 · 06db5ea · 06db5ea
1 parent c379f20
commit 06db5ea
Showing 1 changed file with 20 additions and 8 deletions.
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
@@ -213,7 +213,7 @@ type frozen =
       but the actual data of the map is not used, only keys matter. All
       functions operating on this type must have the same behaviour on
       [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *)
-| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t
+| FrozenProgress of (undefined evar_info Evar.Map.t * Evar.Set.t) Lazy.t
   (** Proper partition of the evar map as described above. *)
 
 let frozen_and_pending_holes (sigma, sigma') =
@@ -223,18 +223,30 @@ let frozen_and_pending_holes (sigma, sigma') =
     FrozenId undefined0
   else
     let data = lazy begin
-    let add_derivative_of evk evi acc =
-      match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
-    let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in
-    let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
-    let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
-    (frozen, pending)
+      let pending, aliases =
+        Evar.Map.symmetric_diff_fold (fun ev v v' (pending,aliases as acc) -> match v, v' with
+            | None, None -> assert false
+            | Some _, None ->
+              (* ev got defined in sigma', but is it an alias? *)
+              begin match advance sigma' ev with
+              | None -> acc
+              | Some ev -> pending, Evar.Set.add ev aliases
+              end
+            | None, Some _ ->
+              (* ev is new in sigma' *)
+              Evar.Set.add ev pending, aliases
+            | Some _, Some _ -> (* ev is still undefined in sigma' *) acc)
+          undefined0
+          (Evd.undefined_map sigma')
+          (Evar.Set.empty, Evar.Set.empty)
+      in
+      (Evd.undefined_map sigma', Evar.Set.diff pending aliases)
     end in
     FrozenProgress data
 
 let filter_frozen frozen = match frozen with
   | FrozenId map -> fun evk -> Evar.Map.mem evk map
-  | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
+  | FrozenProgress (lazy (undf, pending)) -> fun evk -> not (Evar.Set.mem evk pending) && Evar.Map.mem evk undf
 
 let typeclasses_filter ~program_mode frozen =
   if program_mode