From 6125cb1ddc442bf8270bb778a85c4b8d77fe570a Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 28 Aug 2023 12:26:25 +0200 Subject: [PATCH] add `clear *` to clear all unused items in the context recursively --- src/ecHiGoal.ml | 23 ++++++++++++++--------- src/ecHiGoal.mli | 2 +- src/ecParser.mly | 5 ++++- src/ecParsetree.ml | 8 +++++++- 4 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 5d2b68b08..f1563a5f7 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -163,17 +163,22 @@ 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 + | `Some symbols -> ( + try t_clears (List.map toid symbols) tc + with (ClearError _) as err -> tc_error_exn !!tc err) + | `All -> let try_clear tc id = + (try t_clear1 id tc + with (ClearError _) -> tc) in + let hyp_ids = (List.map fst (LDecl.tohyps hyps).h_local) in + FApi.tcenv_of_tcenv1 (List.fold_left try_clear tc hyp_ids) (* -------------------------------------------------------------------- *) let process_algebra mode kind eqs (tc : tcenv1) = @@ -1413,7 +1418,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 (`Some xs) tc and intro1_case (st : ST.state) nointro pis gs = let onsub gs = @@ -1826,7 +1831,7 @@ let rec process_mgenintros ?cf ttenv pis tc = | `Gen gn -> t_onall ( t_seqs [ - process_clear gn.pr_clear; + process_clear (`Some gn.pr_clear); process_generalize gn.pr_genp ]) tc in process_mgenintros ~cf:false ttenv pis tc @@ -1838,7 +1843,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 (`Some pr.pr_clear); process_generalize ?doeq pr.pr_genp; process_view views] tc @@ -2078,7 +2083,7 @@ let process_case ?(doeq = false) gp tc = | _ -> () end; t_seqs - [process_clear gp.pr_rev.pr_clear; t_case f; + [process_clear (`Some gp.pr_rev.pr_clear); t_case f; t_simplify_with_info EcReduction.betaiota_red] tc diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 3b22249c3..317163fd6 100644 --- a/src/ecHiGoal.mli +++ b/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 diff --git a/src/ecParser.mly b/src/ecParser.mly index 82f1ef145..4bc3fabae 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2682,8 +2682,11 @@ logtactic: | MOVE vw=prefix(SLASH, pterm)* gp=prefix(COLON, revert)? { Pmove { pr_rev = odfl prevert0 gp; pr_view = vw; } } +| CLEAR STAR + { Pclear `All } + | CLEAR l=loc(ipcore_name)+ - { Pclear l } + { Pclear (`Some l) } | CONGR { Pcongr } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 19909d4e3..1c5fde285 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -957,6 +957,12 @@ type apply_info = [ | `ExactType of pqsymbol ] +(* -------------------------------------------------------------------- *) +type clear_info = [ + | `All + | `Some 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