[refold]: allow rigid unification

src/ecHiGoal.ml

@@ -598,9 +598,10 @@ let process_rewrite1_core ?mode ?(close = true) ?target (s, p, o) pt tc =
           tc_error !!tc "r-pattern does not match the rewriting rule"
 
 (* -------------------------------------------------------------------- *)
-let process_delta ~und_delta ?target (s, o, p) tc =
+let process_delta ~und_delta ?(rigid = false) ?target (s, o, p) tc =
   let env, hyps, concl = FApi.tc1_eflat tc in
   let o = norm_rwocc o in
+  let occmode = if rigid then Some om_rigid else None in
 
   let idtg, target =
     match target with
@@ -668,7 +669,7 @@ let process_delta ~und_delta ?target (s, o, p) tc =
   match s with
   | `LtoR -> begin
     let matches =
-      try  ignore (PT.pf_find_occurence ptenv ~ptn:p target); true
+      try  ignore (PT.pf_find_occurence ptenv ?occmode ~ptn:p target); true
       with PT.FindOccFailure _ -> false
     in
 
@@ -729,23 +730,26 @@ let process_delta ~und_delta ?target (s, o, p) tc =
         with EcEnv.NotReducible -> fp
     in
 
-    let matches =
-      try  ignore (PT.pf_find_occurence ptenv ~ptn:fp target); true
-      with PT.FindOccFailure _ -> false
-    in
+    begin
+      match PT.pf_find_occurence ?occmode ptenv ~ptn:fp target with
+      | (_, occmode) ->
+        let p    = concretize_form ptenv p  in
+        let fp   = concretize_form ptenv fp in
+        let cpos =
+          try
+            FPosition.select_form
+              ?xconv:(if rigid then Some `AlphaEq else None)
+              ?keyed:(if rigid then Some occmode.k_keyed else None)
+              hyps o fp target
+          with InvalidOccurence ->
+            tc_error !!tc "invalid occurences selector" in
 
-    if matches then begin
-      let p    = concretize_form ptenv p  in
-      let fp   = concretize_form ptenv fp in
-      let cpos =
-        try  FPosition.select_form hyps o fp target
-        with InvalidOccurence ->
-          tc_error !!tc "invalid occurences selector"
-      in
+        let target = FPosition.map cpos (fun _ -> p) target in
+        t_change ~ri ?target:idtg target tc 
 
-      let target = FPosition.map cpos (fun _ -> p) target in
-      t_change ~ri ?target:idtg target tc
-    end else t_id tc
+      | exception (PT.FindOccFailure _) ->
+        t_id tc
+  end
 
 (* -------------------------------------------------------------------- *)
 let process_rewrite1_r ttenv ?target ri tc =
@@ -768,11 +772,11 @@ let process_rewrite1_r ttenv ?target ri tc =
       let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
       t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc
 
-  | RWDelta ((s, r, o, px), p) -> begin
+  | RWDelta (rigid, (s, r, o, px), p) -> begin
       if Option.is_some px then
         tc_error !!tc "cannot use pattern selection in delta-rewrite rules";
 
-      let do1 tc = process_delta ~und_delta ?target (s, o, p) tc in
+      let do1 tc = process_delta ~und_delta ~rigid ?target (s, o, p) tc in
 
       match r with
       | None -> do1 tc

src/ecHiGoal.mli

@@ -75,7 +75,7 @@ val process_clear       : clear_info -> backward
 val process_smt         : ?loc:EcLocation.t -> ttenv -> pprover_infos option -> backward
 val process_coq         : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward
 val process_apply       : implicits:bool -> apply_t * prevert option -> backward
-val process_delta       : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward
+val process_delta       : und_delta:bool -> ?rigid:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward
 val process_rewrite     : ttenv -> ?target:psymbol -> rwarg list -> backward
 val process_subst       : pformula list -> backward
 val process_cut         : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward

src/ecParser.mly

@@ -2418,8 +2418,8 @@ rwarg1:
 | s=rwside r=rwrepeat? o=rwocc? p=bracket(form_h)? fp=rwpterms
    { RWRw ((s, r, o, p), fp) }
 
-| s=rwside r=rwrepeat? o=rwocc? SLASH x=sform_h %prec prec_tactic
-   { RWDelta ((s, r, o, None), x); }
+| s=rwside r=rwrepeat? o=rwocc? SLASH rigid=iboption(TILD) x=sform_h %prec prec_tactic
+   { RWDelta (rigid, (s, r, o, None), x); }
 
 | PR s=bracket(rwpr_arg)
    { RWPr s }

src/ecParsetree.ml

@@ -877,7 +877,7 @@ type rwarg = (tfocus located) option * rwarg1 located
 
 and rwarg1 =
   | RWSimpl  of [`Default | `Variant]
-  | RWDelta  of (rwoptions * pformula)
+  | RWDelta  of (bool * rwoptions * pformula)
   | RWRw     of (rwoptions * (rwside * ppterm) list)
   | RWPr     of (psymbol * pformula option)
   | RWDone   of [`Default | `Variant] option