Skip to content

normalize the result of case_rwlist and cache it. #1662

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
+17 −5
Open

normalize the result of case_rwlist and cache it. #1662

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 17 additions & 5 deletions src/basicProof/BasicProvers.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -693,17 +693,29 @@ fun PURE_FULL_CASE_TAC (g as (asl,w)) =
in Cases_on `^t` end g;

local
fun tot f x = f x handle HOL_ERR _ => NONE
in

fun tot f x = f x handle HOL_ERR _ => NONE

fun case_rws tyi =
List.mapPartial I
[Lib.total TypeBasePure.case_def_of tyi,
tot TypeBasePure.distinct_of tyi,
tot TypeBasePure.one_one_of tyi]
|> map BODY_CONJUNCTS
|> List.concat

val cache = ref (List.concat (map case_rws (TypeBase.elts ())))

fun update_cache tyinfo =
let val thms = (case_rws tyinfo)
in
cache := List.revAppend (thms,!cache)
end
in

val _ = TypeBase.register_update_fn (fn tyinfo => (update_cache tyinfo;tyinfo))

fun case_rwlist () =
itlist (fn tyi => fn rws => case_rws tyi @ rws)
(TypeBase.elts()) [];
fun case_rwlist () = !cache

(* Add the rewrites into a simpset to avoid re-processing them when
* (PURE_CASE_SIMP_CONV rws) is called multiple times by EVERY_CASE_TAC. This
Expand Down