Warn on useless unfolds by default

Author: oskgo

src/ecHiGoal.ml

@@ -33,7 +33,6 @@ type ttenv = {
   tt_implicits : bool;
   tt_oldip     : bool;
   tt_redlogic  : bool;
-  tt_und_delta : bool;
 }
 
 type engine = ptactic_core -> FApi.backward
@@ -671,7 +670,7 @@ let process_rewrite1_core
           tc_error !!tc "context variable does not appear in the r-pattern"
 
 (* -------------------------------------------------------------------- *)
-let process_delta ~und_delta ?target ((s :rwside), o, p) tc =
+let process_delta ?target ((s :rwside), o, p) tc =
   let env, hyps, concl = FApi.tc1_eflat tc in
   let o = norm_rwocc o in
 
@@ -693,10 +692,8 @@ let process_delta ~und_delta ?target ((s :rwside), o, p) tc =
           EcReduction.delta_h = check_id; } in
     let redform = EcReduction.simplify ri hyps target in
 
-    if und_delta then begin
-      if EcFol.f_equal target redform then
-        EcEnv.notify env `Warning "unused unfold: /%s" x
-    end;
+    if EcFol.f_equal target redform then
+      EcEnv.notify env `Warning "unused unfold: /%s" x;
 
     t_change ~ri:{ ri with eta = true; beta = true; } ?target:idtg redform tc
 
@@ -823,7 +820,6 @@ let process_delta ~und_delta ?target ((s :rwside), o, p) tc =
 (* -------------------------------------------------------------------- *)
 let process_rewrite1_r ttenv ?target ri tc =
   let implicits = ttenv.tt_implicits in
-  let und_delta = ttenv.tt_und_delta in
 
   match unloc ri with
   | RWDone simpl ->
@@ -846,7 +842,7 @@ let process_rewrite1_r ttenv ?target ri tc =
         tc_error !!tc "cannot use pattern selection in delta-rewrite rules";
 
       let do1 tc =
-        process_delta ~und_delta ?target (rwopt.side, rwopt.occurrence, p) tc in
+        process_delta ?target (rwopt.side, rwopt.occurrence, p) tc in
 
       match rwopt.repeat with
       | None -> do1 tc
@@ -1609,7 +1605,7 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
     in t_seqs [t_intros_i [h]; rwt; t_clear h] tc
 
   and intro1_unfold (_ : ST.state) (s, o) p tc =
-    process_delta ~und_delta:ttenv.tt_und_delta (s, o, p) tc
+    process_delta (s, o, p) tc
 
   and intro1_view (_ : ST.state) pe tc =
     process_view1 pe tc

src/ecHiGoal.mli

@@ -14,7 +14,6 @@ type ttenv = {
   tt_implicits : bool;
   tt_oldip     : bool;
   tt_redlogic  : bool;
-  tt_und_delta : bool;
 }
 
 type engine  = ptactic_core -> backward
@@ -80,7 +79,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       : ?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/ecScope.ml

@@ -238,13 +238,11 @@ module KnownFlags = struct
   let implicits = "implicits"
   let oldip     = "oldip"
   let redlogic  = "redlogic"
-  let und_delta = "und_delta"
 
   let flags = [
     (implicits, false);
     (oldip    , false);
     (redlogic , true );
-    (und_delta, false);
   ]
 end
 
@@ -546,12 +544,6 @@ module Options = struct
 
   let set_redlogic scope value =
     set scope KnownFlags.redlogic value
-
-  let get_und_delta scope =
-    get scope KnownFlags.und_delta
-
-  let set_und_delta scope value =
-    set scope KnownFlags.und_delta value
 end
 
 (* -------------------------------------------------------------------- *)
@@ -857,8 +849,7 @@ module Tactics = struct
           EcHiGoal.tt_smtmode    = htmode;
           EcHiGoal.tt_implicits  = Options.get_implicits scope;
           EcHiGoal.tt_oldip      = Options.get_oldip scope;
-          EcHiGoal.tt_redlogic   = Options.get_redlogic scope;
-          EcHiGoal.tt_und_delta  = Options.get_und_delta scope; } in
+          EcHiGoal.tt_redlogic   = Options.get_redlogic scope; } in
 
         let bullets =
           try omap (EcBullets.open_phrase ~bullet juc) pac.puc_bullets

theories/analysis/RealSeries.ec

@@ -1208,7 +1208,7 @@ rewrite -(@eq_sum (G (x :: r) (x :: r))) => /= [sg @/G|].
 rewrite -(@eq_sum (fun sg => F x u * G (x :: r) r sg)).
 - by move=> sg /= @/G; case _: (_ /\ _).
 rewrite sumZ; congr => @/G @/M => {S P M G}.
-rewrite -(@sum_reindex (swap_codom x witness u)) /(\o) /=.
+rewrite -(@sum_reindex (swap_codom x witness u)) 3:/(\o) /=.
 - by apply: bij_swap_codom.
 - by apply/summable_cond_fin/finiteIr/finite_fixfinfun; apply/finite_mem.
 apply: eq_sum=> /= sg; congr; last first.

theories/datatypes/BitEncoding.ec

@@ -815,7 +815,7 @@ move=> s1 s2; rewrite mulzDl /= [_ + n]addrC => szE1 szE2.
 have := size_eqD _ _ _ _ _ szE1; ~-1: move=> //#.
 have := size_eqD _ _ _ _ _ szE2; ~-1: move=> //#.
 case=> [s1a s1b] [# sz1a sz1b ->] [s2a s2b] [# sz2a sz2b ->].
-rewrite !mkseqSr /(\o) //= !drop0 !take_catl ?(sz1a, sz2a) //.
+rewrite !mkseqSr //= /(\o) !drop0 !take_catl ?(sz1a, sz2a) //.
 rewrite !take_oversize ?(sz1a, sz2a) // => -[<-].
 move=> eq_tl; congr; apply: ih => //.
 apply: (eq_trans _ _ (eq_trans _ eq_tl _)).

theories/datatypes/FMap.ec

@@ -547,7 +547,7 @@ qed.
 
 lemma offset_get s (e: 'a): (offset s).[e] = if e \in s then Some () else None.
 proof.
-rewrite getE /ofset ofmapK.
+rewrite getE ofmapK.
 - move: (FSet.finite_mem s).
   apply/eq_ind/fun_ext => y.
   rewrite offunE /#.

theories/structure/Finite.ec

@@ -256,7 +256,7 @@ lemma finite_fixfinfun ['a 'b] dom codom :
   => is_finite<:'b> codom
   => is_finite<: 'a -> 'b> (fixfinfun dom codom).
 proof.
-case=> [sa [uqa @/predT /= ha]] [sb [uqb @/predT /= hb]]; apply/finiteP.
+case=> [sa [uqa /= ha]] [sb [uqb /= hb]]; apply/finiteP.
 pose F (s : ('a * 'b) list) (a : 'a) := odflt witness (assoc s a).
 exists (map F (fingraph sa sb)) => /= f hfix.
 apply/mapP; pose s := map (fun a => (a, f a)) sa.