[refold]: allow rigid unification

Syntax: `rewrite -/~(pattern)`

Author: strub

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 `AlphaEq else `Conv)
+              ~keyed:occmode.k_keyed
+              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/ecLexer.mll

@@ -422,6 +422,7 @@ rule main = parse
   | "<@"  { [LEAT      ] }
   | ":~"  { [COLONTILD ] }
 
+  | "/~"   { [SLASHTILD       ] }
   | "/~="  { [SLASHTILDEQ     ] }
   | "//~=" { [SLASHSLASHTILDEQ] }
 

src/ecParser.mly

@@ -563,6 +563,7 @@
 %token SLASHGT
 %token SLASHSHARP
 %token SLASHSLASHGT
+%token SLASHTILD
 %token SLASHTILDEQ
 %token SLASHSLASH
 %token SLASHSLASHEQ
@@ -2390,7 +2391,10 @@ rwarg1:
    { 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); }
+   { RWDelta (false, (s, r, o, None), x); }
+
+| s=rwside r=rwrepeat? o=rwocc? SLASHTILD x=sform_h %prec prec_tactic
+   { RWDelta (true, (s, r, o, None), x); }
 
 | PR s=bracket(rwpr_arg)
    { RWPr s }

src/ecParsetree.ml

@@ -860,7 +860,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