Merge PR coq#18260: Cache set of undefined impossible case evars in e…

…var_flags

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

engine/evarutil.ml

@@ -497,12 +497,12 @@ let filter_effective_candidates evd evi filter candidates =
   let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
   List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates
 
-let restrict_evar evd evk filter ?src candidates =
+let restrict_evar evd evk filter candidates =
   let evar_info = Evd.find_undefined evd evk in
   let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in
   match candidates with
   | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
-  | _ -> Evd.restrict evk filter ?candidates ?src evd
+  | _ -> Evd.restrict evk filter ?candidates evd
 
 let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~global c =
   (* returns a new constr where all the evars have been 'cleaned'

engine/evarutil.mli

@@ -225,7 +225,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t opti
     into an empty list. *)
 
 val restrict_evar : evar_map -> Evar.t -> Filter.t ->
-  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
+  constr list option -> evar_map * Evar.t
 
 val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types ->
   Id.Set.t -> evar_map * named_context_val * types

engine/evd.ml

@@ -489,6 +489,7 @@ type evar_flags =
   { obligation_evars : Evar.Set.t;
     aliased_evars : Evar.t Evar.Map.t;
     typeclass_evars : Evar.Set.t;
+    impossible_case_evars : Evar.Set.t;
   }
 
 type side_effect_role =
@@ -752,6 +753,11 @@ let add_with_name (type a) ?name ?(typeclass_candidate = true) d e (i : a evar_i
       { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
     else d.evar_flags
   in
+  let evar_flags = match i.evar_source with
+    | _, ImpossibleCase ->
+      { evar_flags with impossible_case_evars = Evar.Set.add e evar_flags.impossible_case_evars }
+    | _ -> evar_flags
+  in
   let candidate_evars = match i.evar_candidates with
   | Undefined None -> Evar.Set.remove e d.candidate_evars
   | Undefined (Some _) -> Evar.Set.add e d.candidate_evars
@@ -788,11 +794,14 @@ let is_obligation_evar evd evk =
   let flags = evd.evar_flags in
   Evar.Set.mem evk flags.obligation_evars
 
+let get_impossible_case_evars evd = evd.evar_flags.impossible_case_evars
+
 (** Inheritance of flags: for evar-evar and restriction cases *)
 
 let inherit_evar_flags evar_flags evk evk' =
   let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
   let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+  let evk_impossible = Evar.Set.mem evk evar_flags.impossible_case_evars in
   let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in
   let typeclass_evars =
     if evk_typeclass then
@@ -806,15 +815,23 @@ let inherit_evar_flags evar_flags evk evk' =
       Evar.Set.add evk' obligation_evars
     else evar_flags.obligation_evars
   in
-  { obligation_evars; aliased_evars; typeclass_evars;  }
+  let impossible_case_evars =
+    if evk_impossible then
+      let impossible_case_evars = Evar.Set.remove evk evar_flags.impossible_case_evars in
+      Evar.Set.add evk' impossible_case_evars
+    else evar_flags.impossible_case_evars
+  in
+  { obligation_evars; aliased_evars; typeclass_evars; impossible_case_evars; }
 
 (** Removal: in all other cases of definition *)
 
 let remove_evar_flags evk evar_flags =
   { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
+    impossible_case_evars = Evar.Set.remove evk evar_flags.impossible_case_evars;
     (* Aliasing information is kept. *)
-    aliased_evars = evar_flags.aliased_evars }
+    aliased_evars = evar_flags.aliased_evars;
+  }
 
 (** New evars *)
 
@@ -971,7 +988,9 @@ let create_evar_defs sigma = { sigma with
 let empty_evar_flags =
   { obligation_evars = Evar.Set.empty;
     aliased_evars = Evar.Map.empty;
-    typeclass_evars = Evar.Set.empty }
+    typeclass_evars = Evar.Set.empty;
+    impossible_case_evars = Evar.Set.empty;
+  }
 
 let empty_side_effects = {
   seff_private = Safe_typing.empty_private_constants;
@@ -1422,6 +1441,11 @@ let restrict evk filter ?candidates ?src evd =
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  let evar_flags = match src with
+    | Some (_,Evar_kinds.ImpossibleCase) ->
+      { evar_flags with impossible_case_evars = Evar.Set.add evk' evar_flags.impossible_case_evars }
+    | _ -> evar_flags
+  in
   let candidate_evars = Evar.Set.remove evk evd.candidate_evars in
   let candidate_evars = match candidates with
   | None -> candidate_evars
@@ -1438,9 +1462,8 @@ let restrict evk filter ?candidates ?src evd =
   (evd, evk')
 
 let update_source evd evk src =
-  let evar_info = EvMap.find evk evd.undf_evars in
-  let evar_info' = { evar_info with evar_source = src } in
-  { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+  let modify _ info = { info with evar_source = src } in
+  { evd with undf_evars = EvMap.modify evk modify evd.undf_evars }
 
 (**********************************************************)
 (* Accessing metas *)

engine/evd.mli

@@ -359,6 +359,9 @@ val set_obligation_evar : evar_map -> Evar.t -> evar_map
 val is_obligation_evar : evar_map -> Evar.t -> bool
 (** Is the evar declared as an obligation *)
 
+val get_impossible_case_evars : evar_map -> Evar.Set.t
+(** Set of undefined evars with ImpossibleCase evar source. *)
+
 val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)

pretyping/evarconv.ml

@@ -1818,14 +1818,14 @@ let rec solve_unconstrained_evars_with_candidates flags env evd =
       solve_unconstrained_evars_with_candidates flags env evd
 
 let solve_unconstrained_impossible_cases env evd =
-  Evd.fold_undefined (fun evk ev_info evd' ->
-    match Evd.evar_source ev_info with
-    | loc,Evar_kinds.ImpossibleCase ->
+  Evar.Set.fold (fun evk evd' ->
       let evd', j = coq_unit_judge env evd' in
       let ty = j_type j in
       let flags = default_flags env in
       instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *)
-    | _ -> evd') evd evd
+    )
+    (Evd.get_impossible_case_evars evd)
+    evd
 
 let solve_unif_constraints_with_heuristics env
     ?(flags=default_flags env) ?(with_ho=false) evd =

pretyping/pretyping.ml

@@ -407,20 +407,13 @@ let process_inference_flags flags env initial (sigma,c,cty) =
 let adjust_evar_source sigma na c =
   match na, kind sigma c with
   | Name id, Evar (evk,args) ->
-     let EvarInfo evi = Evd.find sigma evk in
+     let evi = Evd.find_undefined sigma evk in
      begin match Evd.evar_source evi with
-     | loc, Evar_kinds.QuestionMark {
-         Evar_kinds.qm_obligation=b;
-         Evar_kinds.qm_name=Anonymous;
-         Evar_kinds.qm_record_field=recfieldname;
-        } ->
-        let src = (loc,Evar_kinds.QuestionMark {
-            Evar_kinds.qm_obligation=b;
-            Evar_kinds.qm_name=na;
-            Evar_kinds.qm_record_field=recfieldname;
-        }) in
-        let (sigma, evk') = restrict_evar sigma evk (evar_filter evi) ~src None in
-        sigma, mkEvar (evk',args)
+     | loc, Evar_kinds.QuestionMark ({ Evar_kinds.qm_name=Anonymous } as qm) ->
+       let src = (loc,Evar_kinds.QuestionMark { qm with Evar_kinds.qm_name=na }) in
+       (* Evd.update_source doesn't work for some reason, cf test bug_18260_1.v *)
+       let (sigma, evk') = Evd.restrict evk (evar_filter evi) ~src sigma in
+       sigma, mkEvar (evk',args)
      | _ -> sigma, c
      end
   | _, _ -> sigma, c

test-suite/bugs/bug_18260_1.v

@@ -0,0 +1,106 @@
+Require Coq.Init.Byte Coq.Strings.Byte Coq.ZArith.ZArith.
+
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+
+Import Byte.
+
+Module Export word.
+  Class word {width : BinInt.Z} := {
+      rep : Type;
+    }.
+  Arguments word : clear implicits.
+
+End word.
+Notation word := word.word.
+Global Coercion word.rep : word >-> Sortclass.
+
+
+
+Module map.
+  Class map {key value:Type} := mk {
+                                    rep : Type;
+                                  }.
+  Arguments map : clear implicits.
+  Global Coercion rep : map >-> Sortclass.
+
+End map.
+Local Notation map := map.map.
+Global Coercion map.rep : map >-> Sortclass.
+
+Definition SuchThat(R: Type)(P: R -> Prop) := R.
+Existing Class SuchThat.
+
+Notation "'annotate!' x T" := (match x return T with b => b end)
+                                (at level 10, x at level 0, T at level 0, only parsing).
+
+Notation "'infer!' P" :=
+  (match _ as ResType return ResType with
+   | ResType =>
+       match P with
+       | Fun => annotate! (annotate! _ (SuchThat ResType Fun)) ResType
+       end
+   end)
+    (at level 0, P at level 100, only parsing).
+
+Global Hint Extern 1 (SuchThat ?RRef ?FRef) =>
+         let R := eval cbv delta [RRef] in RRef in
+           let r := open_constr:(_ : R) in
+           let G := eval cbv beta delta [RRef FRef] in (FRef r) in
+             let t := open_constr:(ltac:(cbv beta; typeclasses eauto) : G) in
+             match r with
+             | ?y => exact y
+             end
+               : typeclass_instances.
+
+Class Multiplication{A B R: Type}(a: A)(b: B)(r: R) := {}.
+Notation "a * b" := (infer! Multiplication a b) (only parsing) : oo_scope.
+
+
+Import map.
+
+Section Sep.
+  Context  {map : Type}.
+  Definition sep (p q : map -> Prop) (m:map) : Prop. Admitted.
+
+End Sep.
+
+Import Coq.ZArith.ZArith.
+
+Section Scalars.
+  Context {width : Z} {word : word width}.
+
+  Context {mem : map.map word byte}.
+  Definition scalar : word -> word -> mem -> Prop. Admitted.
+
+End Scalars.
+
+#[export] Instance MulSepClause{K V: Type}{M: map.map K V}(a b: @map.rep K V M -> Prop)
+  : Multiplication a b (sep a b) | 10 := {}.
+
+
+Class PointsTo{width: Z}{word: word.word width}{mem: map.map word Byte.byte}{V: Type}
+  (addr: word)(val: V)(pred: mem -> Prop) := {}.
+Global Hint Mode PointsTo + + + + + + - : typeclass_instances.
+
+Class PointsToPredicate{width}{word: word.word width}{mem: Type}
+  (V: Type)(pred: word -> V -> mem -> Prop) := {}.
+
+#[export] Instance PointsToPredicate_to_PointsTo
+  {width}{word: word.word width}{mem: map.map word Byte.byte}{V: Type}
+  (pred: word -> V -> mem -> Prop){p: PointsToPredicate V pred}
+  (a: word)(v: V): PointsTo a v (pred a v) := {}.
+
+#[export] Instance PointsToScalarPredicate
+  {width}{word: word.word width}{mem: map.map word Byte.byte}:
+  PointsToPredicate word scalar := {}.
+
+Section TestNotations.
+  Context {width: Z} {word: word.word width} {mem: map.map word Byte.byte}.
+  Local Open Scope oo_scope.
+  Set Printing All.
+  Typeclasses eauto := debug.
+  Goal forall (a1 a2 ofs sz v1 v2: word) (R: mem -> Prop) (m: mem),
+      (infer! Multiplication R (infer! PointsTo a1 v1)) m.
+  Abort.
+End TestNotations.