add clear to clear all unused items in the context recursively

add exclude filters and test

Author: oskgo

src/ecHiGoal.ml

@@ -163,17 +163,23 @@ let process_coq ~loc ~name (ttenv : ttenv) coqmode  pi (tc : tcenv1) =
     t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode:(`Report (Some loc)) coqmode pi) tc
 
 (* -------------------------------------------------------------------- *)
-let process_clear symbols tc =
+let process_clear (info : clear_info) tc =
   let hyps = FApi.tc1_hyps tc in
-
   let toid s =
     if not (LDecl.has_name (unloc s) hyps) then
       tc_lookup_error !!tc ~loc:s.pl_loc `Local ([], unloc s);
     fst (LDecl.by_name (unloc s) hyps)
   in
-
-  try  t_clears (List.map toid symbols) tc
-  with (ClearError _) as err -> tc_error_exn !!tc err
+  match info with
+  | `Include symbols -> begin
+    try  t_clears (List.map toid symbols) tc
+    with (ClearError _) as err -> tc_error_exn !!tc err
+  end
+  | `Exclude symbols -> 
+    let excluded = List.map toid symbols in
+    let hyp_ids = List.map fst (LDecl.tohyps hyps).h_local in
+    let clear_list = List.filter (fun x -> not (List.mem x excluded)) hyp_ids in
+    t_clears ~leniant:true clear_list tc
 
 (* -------------------------------------------------------------------- *)
 let process_algebra mode kind eqs (tc : tcenv1) =
@@ -1413,7 +1419,7 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
     t_simplify_lg ~delta:`IfApplied (ttenv, logic) tc
 
   and intro1_clear (_ : ST.state) xs tc =
-    process_clear xs tc
+    process_clear (`Include xs) tc
 
   and intro1_case (st : ST.state) nointro pis gs =
     let onsub gs =
@@ -1826,7 +1832,7 @@ let rec process_mgenintros ?cf ttenv pis tc =
       | `Gen gn ->
          t_onall (
            t_seqs [
-               process_clear gn.pr_clear;
+               process_clear (`Include gn.pr_clear);
                process_generalize gn.pr_genp
            ]) tc
     in process_mgenintros ~cf:false ttenv pis tc
@@ -1838,7 +1844,7 @@ let process_genintros ?cf ttenv pis tc =
 (* -------------------------------------------------------------------- *)
 let process_move ?doeq views pr (tc : tcenv1) =
   t_seqs
-    [process_clear pr.pr_clear;
+    [process_clear (`Include pr.pr_clear);
      process_generalize ?doeq pr.pr_genp;
      process_view views]
     tc
@@ -2078,7 +2084,7 @@ let process_case ?(doeq = false) gp tc =
             | _ -> ()
           end;
           t_seqs
-            [process_clear gp.pr_rev.pr_clear; t_case f;
+            [process_clear (`Include gp.pr_rev.pr_clear); t_case f;
              t_simplify_with_info EcReduction.betaiota_red]
             tc
 

src/ecHiGoal.mli

@@ -71,7 +71,7 @@ val process_mgenintros  : ?cf:bool -> ttenv -> introgenpattern list -> tactical
 val process_genintros   : ?cf:bool -> ttenv -> introgenpattern list -> backward
 val process_generalize  : ?doeq:bool -> genpattern list -> backward
 val process_move        : ?doeq:bool -> ppterm list -> prevert -> backward
-val process_clear       : psymbol list -> backward
+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

src/ecParser.mly

@@ -2682,8 +2682,14 @@ logtactic:
 | MOVE vw=prefix(SLASH, pterm)* gp=prefix(COLON, revert)?
    { Pmove { pr_rev = odfl prevert0 gp; pr_view = vw; } }
 
+| CLEAR
+   { Pclear (`Exclude []) }
+
+| CLEAR MINUS l=loc(ipcore_name)+
+   { Pclear (`Exclude l) }
+
 | CLEAR l=loc(ipcore_name)+
-   { Pclear l }
+   { Pclear (`Include l) }
 
 | CONGR
    { Pcongr }

src/ecParsetree.ml

@@ -957,6 +957,12 @@ type apply_info = [
   | `ExactType of pqsymbol
 ]
 
+(* -------------------------------------------------------------------- *)
+type clear_info = [
+  | `Exclude of psymbol list
+  | `Include of psymbol list
+]
+
 (* -------------------------------------------------------------------- *)
 type pgenhave = psymbol * intropattern option * psymbol list * pformula
 
@@ -979,7 +985,7 @@ type logtactic =
   | Pcut        of pcut
   | Pcutdef     of (intropattern * pcutdef)
   | Pmove       of prevertv
-  | Pclear      of psymbol list
+  | Pclear      of clear_info
   | Prewrite    of (rwarg list * osymbol_r)
   | Prwnormal   of pformula * pqsymbol list
   | Psubst      of pformula list

tests/clear.ec

@@ -0,0 +1,21 @@
+lemma L: true.
+pose x:=false.
+clear x.
+(* `x` is now unbound *)
+pose x:=false.
+pose y:=x.
+pose z:=y.
+clear -y. 
+(* `z` is unbound, but `x` is not, since `y` depends on it *)
+pose z:=x.
+clear y.
+pose y:=z.
+clear. 
+(* everything is unbound, since nothing is in the goal *)
+pose x:=true.
+pose y:=false.
+clear. 
+(* we cannot clear `x` since it is in the goal,
+   but `y` is not used so it becomes unbound *)
+pose y:= x.
+abort.