From 7e6bf7318b9cc20a423efe3f5a0ad4ae9de98e67 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 add exclude filters and test --- src/ecHiGoal.ml | 24 +++++++++++++++--------- src/ecHiGoal.mli | 2 +- src/ecParser.mly | 8 +++++++- src/ecParsetree.ml | 8 +++++++- tests/clear.ec | 21 +++++++++++++++++++++ 5 files changed, 51 insertions(+), 12 deletions(-) create mode 100644 tests/clear.ec diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 5d2b68b08..2ca2e691b 100644 --- a/src/ecHiGoal.ml +++ b/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 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..305a6175e 100644 --- a/src/ecParser.mly +++ b/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 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 19909d4e3..14db94e18 100644 --- a/src/ecParsetree.ml +++ b/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 diff --git a/tests/clear.ec b/tests/clear.ec new file mode 100644 index 000000000..bcfeb4bee --- /dev/null +++ b/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.