Make proof-local simplify hint databases visible to conversion

The named/local hint-database mechanism records the set of active
databases per goal (g_simpl), but several tactics consulted user
reduction rules through static reduction_info values (full_compat /
full_red with an empty user_local), so rules activated with
`hint +db.` were invisible to them.

With this, `hint simplify in db : ...` + a proof-local `hint +db.`
behaves exactly like the former global default-database hints.

Author: strub

src/ecCoreGoal.ml

@@ -420,6 +420,8 @@ module FApi = struct
   let tc_goal   (tc : tcenv) = tc1_goal   tc.tce_tcenv
   let tc_env    (tc : tcenv) = tc1_env    tc.tce_tcenv
 
+  let tc_simplify_context (tc : tcenv) = tc1_simplify_context tc.tce_tcenv
+
   let tc_flat   ?target (tc : tcenv) = tc1_flat  ?target tc.tce_tcenv
   let tc_eflat  ?target (tc : tcenv) = tc1_eflat ?target tc.tce_tcenv
   let tc_hyps   ?target (tc : tcenv) = tc1_hyps  ?target tc.tce_tcenv

src/ecCoreGoal.mli

@@ -315,6 +315,7 @@ module FApi : sig
   val tc_flat    : ?target:ident -> tcenv -> LDecl.hyps * form
   val tc_eflat   : ?target:ident -> tcenv -> env * LDecl.hyps * form
   val tc_hyps    : ?target:ident -> tcenv -> LDecl.hyps
+  val tc_simplify_context : tcenv -> EcEnv.simplify_context
 
   (* Accessors for focused goal parts (tcenv1) *)
   val tc1_handle : tcenv1 -> handle

src/ecHiGoal.ml

@@ -986,15 +986,17 @@ let process_rewrite1_r ttenv ?target ri tc =
         let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
         let hyps   = FApi.tc1_hyps ?target tc in
 
+        let simpl = FApi.tc1_simplify_context tc in
+
         let ptenv, prw =
           match rwopt.match_ with
           | None ->
-              PT.ptenv_of_penv hyps !!tc, None
+              PT.ptenv_of_penv ~simpl hyps !!tc, None
 
           | Some (RWM_Plain p) ->
               let (ps, ue), p = TTC.tc1_process_pattern tc p in
               let ev = MEV.of_idents (Mid.keys ps) `Form in
-              (PT.ptenv !!tc hyps (ue, ev), Some (p, None))
+              (PT.ptenv ~simpl !!tc hyps (ue, ev), Some (p, None))
 
           | Some (RWM_Context (x, p)) ->
               let ps   = ref Mid.empty in
@@ -1005,7 +1007,7 @@ let process_rewrite1_r ttenv ?target ri tc =
               let hyps = LDecl.add_local x (LD_var (xty, None)) hyps in
               let p    = EcTyping.trans_pattern (LDecl.toenv hyps) ps ue p in
               let ev   = MEV.of_idents (x :: Mid.keys !ps) `Form in
-              (PT.ptenv !!tc hyps (ue, ev), Some (p, Some (x, xty))) in
+              (PT.ptenv ~simpl !!tc hyps (ue, ev), Some (p, Some (x, xty))) in
 
         let theside =
           match rwopt.side, subs with

src/ecLowGoal.ml

@@ -387,6 +387,9 @@ let t_cbv_with_info ?target (ri : reduction_info) (tc : tcenv1) =
 let t_cbv ?target ?(delta = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) =
   let ri = { nodelta with delta_p = fun _ -> delta } in
   let ri = { ri with logic } in
+  (* thread the proof-local simplify overlay (hint +db, local rules) so
+     that tactics built on [t_cbv] (done, progress, ...) see it *)
+  let ri = { ri with user_local = FApi.tc1_simplify_context tc } in
   t_cbv_with_info ?target ri tc
 
 (* -------------------------------------------------------------------- *)
@@ -398,6 +401,9 @@ let t_cbn_with_info ?target (ri : reduction_info) (tc : tcenv1) =
 let t_cbn ?target ?(delta = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) =
   let ri = { nodelta with delta_p = fun _ -> delta } in
   let ri = { ri with logic } in
+  (* thread the proof-local simplify overlay (hint +db, local rules) so
+     that tactics built on [t_cbn] (done, progress, ...) see it *)
+  let ri = { ri with user_local = FApi.tc1_simplify_context tc } in
   t_cbn_with_info ?target ri tc
 
 (* -------------------------------------------------------------------- *)
@@ -676,7 +682,12 @@ let tt_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv) =
   let tc, (pt, ax, subgoals)  =
     RApi.to_pure (fun tc -> LowApply.check_with_cutsolve `Elim pt (`Tc (tc, None))) tc in
 
-  if not (EcReduction.is_conv hyps ax concl) then begin
+  (* conversion sees the proof-local simplify context (hint +db) *)
+  let conv_ri =
+    { EcReduction.full_red with
+        EcReduction.user_local = FApi.tc_simplify_context tc } in
+
+  if not (EcReduction.is_conv ~ri:conv_ri hyps ax concl) then begin
     (*
     let env = FApi.tc_env tc in
     let ppe = EcPrinting.PPEnv.ofenv env in
@@ -757,7 +768,11 @@ module Apply = struct
 
   exception NoInstance of (bool * reason * PT.pt_env * (form * form))
 
-  let t_apply_bwd_r ?(ri = EcReduction.full_compat) ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) =
+  let t_apply_bwd_r ?ri ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) =
+    (* by default, conversion sees the proof-local simplify context *)
+    let ri = ri |> odfl
+      { EcReduction.full_compat with
+          EcReduction.user_local = pt.PT.ptev_env.PT.pte_lc } in
     let ((hyps, concl), pterr) = (FApi.tc1_flat tc, PT.copy pt.ptev_env) in
 
     let noinstance ?(dpe = false) reason =
@@ -834,7 +849,7 @@ module Apply = struct
   let t_apply_bwd ?(ri : EcReduction.reduction_info option) ?mode ?canview pt (tc : tcenv1) =
     let hyps   = FApi.tc1_hyps tc in
     let pt, ax = LowApply.check `Elim pt (`Hyps (hyps, !!tc)) in
-    let ptenv  = ptenv_of_penv hyps !!tc in
+    let ptenv  = ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps !!tc in
     let pt     = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = ax; } in
     t_apply_bwd_r ?ri ?mode ?canview pt tc
 
@@ -1728,6 +1743,10 @@ let t_rewrite
    ?xconv ?keyed ?target ?(mode : rwmode option) ?(donot=false)
    (pt : proofterm) (s, pos) (tc : tcenv1)
 =
+  (* conversion checks below see the proof-local simplify context *)
+  let conv_ri =
+    { EcReduction.full_compat with
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
   let tc           = RApi.rtcenv_of_tcenv1 tc in
   let (hyps, tgfp) = RApi.tc_flat ?target tc in
   let env          = LDecl.toenv hyps in
@@ -1763,7 +1782,7 @@ let t_rewrite
   in
 
   let change f =
-    if not (EcReduction.is_conv hyps f left) then
+    if not (EcReduction.is_conv ~ri:conv_ri hyps f left) then
       raise InvalidGoalShape;
     right in
 

src/ecMatching.ml

@@ -880,7 +880,7 @@ let fmnotation = {
 
 (* -------------------------------------------------------------------- *)
 (* Rigid unification *)
-let f_match_core opts hyps (ue, ev) f1 f2 =
+let f_match_core ?(conv_ri = EcReduction.full_compat) opts hyps (ue, ev) f1 f2 =
   let ue  = EcUnify.UniEnv.copy ue in
   let ev  = ref ev in
 
@@ -891,7 +891,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
 
   let conv =
     match opts.fm_conv with
-    | true  -> EcReduction.is_conv ~ri:EcReduction.full_compat hyps
+    | true  -> EcReduction.is_conv ~ri:conv_ri hyps
     | false -> EcReduction.is_alpha_eq hyps
   in
 
@@ -1286,8 +1286,8 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
     doit (EcEnv.LDecl.toenv hyps) (Fsubst.f_subst_id, Mid.empty) f1 f2;
     (ue, !ev)
 
-let f_match opts hyps (ue, ev) f1 f2 =
-  let (ue, ev) = f_match_core opts hyps (ue, ev) f1 f2 in
+let f_match ?conv_ri opts hyps (ue, ev) f1 f2 =
+  let (ue, ev) = f_match_core ?conv_ri opts hyps (ue, ev) f1 f2 in
     if not (MEV.filled ev) then
       raise MatchFailure;
     let clue =

src/ecMatching.mli

@@ -371,15 +371,17 @@ val fmdelta    : fmoptions
 val fmnotation : fmoptions
 
 val f_match_core :
-     fmoptions
+     ?conv_ri:EcReduction.reduction_info
+  -> fmoptions
   -> EcEnv.LDecl.hyps
   -> unienv * mevmap
   -> form
   -> form
   -> unienv * mevmap
 
 val f_match :
-     fmoptions
+     ?conv_ri:EcReduction.reduction_info
+  -> fmoptions
   -> EcEnv.LDecl.hyps
   -> unienv * mevmap
   -> form

src/ecProofTerm.ml

@@ -19,6 +19,7 @@ type pt_env = {
   pte_hy : LDecl.hyps;
   pte_ue : EcUnify.unienv;
   pte_ev : EcMatching.mevmap ref;
+  pte_lc : EcEnv.simplify_context;  (* proof-local simplify context *)
 }
 
 type pt_ev = {
@@ -78,22 +79,24 @@ let argkind_of_ptarg arg : argkind =
   | PVASub     _ -> `PTerm
 
 (* -------------------------------------------------------------------- *)
-let ptenv pe hyps (ue, ev) =
+let ptenv ?(simpl = EcEnv.SimplifyContext.empty) pe hyps (ue, ev) =
   { pte_pe = pe;
     pte_hy = hyps;
     pte_ue = EcUnify.UniEnv.copy ue;
-    pte_ev = ref ev; }
+    pte_ev = ref ev;
+    pte_lc = simpl; }
 
 (* -------------------------------------------------------------------- *)
 let copy pe =
-  ptenv pe.pte_pe pe.pte_hy (pe.pte_ue, !(pe.pte_ev))
+  ptenv ~simpl:pe.pte_lc pe.pte_pe pe.pte_hy (pe.pte_ue, !(pe.pte_ev))
 
 (* -------------------------------------------------------------------- *)
-let ptenv_of_penv (hyps : LDecl.hyps) (pe : proofenv) =
+let ptenv_of_penv ?(simpl = EcEnv.SimplifyContext.empty) (hyps : LDecl.hyps) (pe : proofenv) =
   { pte_pe = pe;
     pte_hy = hyps;
     pte_ue = PT.unienv_of_hyps hyps;
-    pte_ev = ref EcMatching.MEV.empty; }
+    pte_ev = ref EcMatching.MEV.empty;
+    pte_lc = simpl; }
 
 (* -------------------------------------------------------------------- *)
 let rec get_head_symbol (pt : pt_env) (f : form) =
@@ -272,17 +275,21 @@ let pattern_form ?name hyps ~ptn subject =
 let pf_form_match (pt : pt_env) ?mode ~ptn subject =
   let mode = mode |> odfl EcMatching.fmrigid in
 
+  (* conversion during matching sees the proof-local simplify context *)
+  let conv_ri =
+    { EcReduction.full_compat with EcReduction.user_local = pt.pte_lc } in
+
   try
     let (ue, ev) =
-      EcMatching.f_match_core mode pt.pte_hy
+      EcMatching.f_match_core ~conv_ri mode pt.pte_hy
         (pt.pte_ue, !(pt.pte_ev)) ptn subject
     in
       EcUnify.UniEnv.restore ~dst:pt.pte_ue ~src:ue;
       pt.pte_ev := ev
   with EcMatching.MatchFailure as exn ->
     (* FIXME: should we check for empty inters. with ecmap? *)
     if not mode.fm_conv ||
-       not (EcReduction.is_conv ~ri:EcReduction.full_compat pt.pte_hy ptn subject) then
+       not (EcReduction.is_conv ~ri:conv_ri pt.pte_hy ptn subject) then
       raise exn
 
 (* -------------------------------------------------------------------- *)
@@ -883,37 +890,37 @@ let process_full_closed_pterm pe pf =
 let tc1_process_pterm_cut ~prcut tc ff =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff
+  process_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 let tc1_process_pterm tc ff =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_pterm (ptenv_of_penv hyps pe) ff
+  process_pterm (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 let tc1_process_full_pterm_cut ~prcut (tc : tcenv1) (ff : 'a gppterm) =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_full_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff
+  process_full_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 let tc1_process_full_pterm ?implicits (tc : tcenv1) (ff : ppterm) =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_full_pterm ?implicits (ptenv_of_penv hyps pe) ff
+  process_full_pterm ?implicits (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 let tc1_process_full_closed_pterm_cut ~prcut (tc : tcenv1) (ff : 'a gppterm) =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_full_closed_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff
+  process_full_closed_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 let tc1_process_full_closed_pterm (tc : tcenv1) (ff : ppterm) =
   let pe   = FApi.tc1_penv tc in
   let hyps = FApi.tc1_hyps tc in
-  process_full_closed_pterm (ptenv_of_penv hyps pe) ff
+  process_full_closed_pterm (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff
 
 (* -------------------------------------------------------------------- *)
 type prept = [

src/ecProofTerm.mli

@@ -35,6 +35,7 @@ type pt_env = {
   pte_hy : LDecl.hyps;       (* local context *)
   pte_ue : EcUnify.unienv;   (* unification env. *)
   pte_ev : mevmap ref;       (* metavar env. *)
+  pte_lc : EcEnv.simplify_context; (* proof-local simplify context *)
 }
 
 type pt_ev = {
@@ -148,9 +149,9 @@ val concretize_e_form_gen : cptenv -> bindings -> form -> form
 val concretize_e_arg      : cptenv -> pt_arg -> pt_arg
 
 (* PTEnv constructor *)
-val ptenv_of_penv : LDecl.hyps -> proofenv -> pt_env
+val ptenv_of_penv : ?simpl:EcEnv.simplify_context -> LDecl.hyps -> proofenv -> pt_env
 
-val ptenv : proofenv -> LDecl.hyps -> (EcUnify.unienv * mevmap) -> pt_env
+val ptenv : ?simpl:EcEnv.simplify_context -> proofenv -> LDecl.hyps -> (EcUnify.unienv * mevmap) -> pt_env
 val copy  : pt_env -> pt_env
 
 (* Proof-terms construction from components *)