diff --git a/src/shared/convs/holba_convLib.sml b/src/shared/convs/holba_convLib.sml index acfa40e32..5227eb264 100644 --- a/src/shared/convs/holba_convLib.sml +++ b/src/shared/convs/holba_convLib.sml @@ -138,6 +138,21 @@ in (* local *) clean_conv; end + local + val optcase_none_thm = CONJUNCT1 optionTheory.option_case_def; + val optcase_some_thm = CONJUNCT2 optionTheory.option_case_def; + in + fun option_CASE_CONV opt_conv app_conv = + RATOR_CONV (LAND_CONV opt_conv) THENC + (fn tm => ( + if optionSyntax.is_none tm then + REWR_CONV optcase_none_thm + else + REWR_CONV optcase_some_thm THENC + app_conv + ) tm); + end + (* ---------------------------------------------------------------------------------- *) (* generic fast set operations (conversions) *) diff --git a/src/tools/symbexec/bir_vars_ofLib.sml b/src/tools/symbexec/bir_vars_ofLib.sml index 263a19df5..f095be014 100644 --- a/src/tools/symbexec/bir_vars_ofLib.sml +++ b/src/tools/symbexec/bir_vars_ofLib.sml @@ -152,6 +152,70 @@ in (* local *) val birs_freesymbs_CONV = GEN_match_conv is_birs_freesymbs birs_freesymbs_DIRECT_CONV; + +(* ---------------------------------------------------------------------------------- *) +(* birs_env_vars_are_initialised, birs_env_var_is_initialised *) +(* ---------------------------------------------------------------------------------- *) + + local + val birs_update_env_P_CONV = + BETA_CONV THENC + NEG_CONV ( + LHS_CONV ( + REWR_CONV pairTheory.FST + ) THENC + bir_varname_EQ_CONV + ); + in + val birs_gen_env_list_purge_CONV = + listLib.FILTER_CONV birs_update_env_P_CONV; + end + + val birs_update_env_CONV = + REWR_CONV birs_update_env_thm THENC + RAND_CONV (RAND_CONV birs_gen_env_list_purge_CONV); + + local + fun birs_env_var_is_initialised_set_CONV_helper tm = ( + if (listSyntax.is_cons o rand o rand o rator) tm then + REWR_CONV birs_env_var_is_initialised_gen_env_INSERT_thm THENC + LAND_CONV ( + option_CASE_CONV + (bir_exp_typecheckLib.type_of_bir_exp_DIRECT_CONV) + ( + BETA_CONV THENC + ITE_CONV ( + LAND_CONV bir_vars_of_exp_DIRECT_CONV THENC + SUBSET_CONV bir_var_EQ_CONV + ) + ) + ) THENC + RAND_CONV ( + LAND_CONV (RAND_CONV (birs_gen_env_list_purge_CONV)) THENC + birs_env_var_is_initialised_set_CONV_helper + ) THENC + pred_setLib.UNION_CONV bir_var_EQ_CONV + else + REWR_CONV birs_env_var_is_initialised_gen_env_EMPTY_thm + ) tm; + in + val birs_env_var_is_initialised_set_CONV = ( + birs_env_var_is_initialised_set_CONV_helper + ) o (fn tm => + if is_birs_env_var_is_initialised_set tm then tm else + raise ERR "birs_env_var_is_initialised_set_CONV" "cannot handle term" + ); + end + + val birs_env_vars_are_initialised_CONV = ( + REWR_CONV birs_env_vars_are_initialised_SUBSET_thm THENC + RAND_CONV birs_env_var_is_initialised_set_CONV THENC + SUBSET_CONV bir_var_EQ_CONV + ) o (fn tm => + if is_birs_env_vars_are_initialised tm then tm else + raise ERR "birs_env_vars_are_initialised_CONV" "cannot handle term" + ); + end (* local *) end (* struct *) diff --git a/src/tools/symbexec/birsSyntax.sml b/src/tools/symbexec/birsSyntax.sml index 988d0de98..a0dfc0ab2 100644 --- a/src/tools/symbexec/birsSyntax.sml +++ b/src/tools/symbexec/birsSyntax.sml @@ -79,12 +79,18 @@ end; val syntax_fns1_env = syntax_fns 2 HolKernel.dest_monop HolKernel.mk_monop; val syntax_fns1_set = syntax_fns 2 HolKernel.dest_monop HolKernel.mk_monop; val syntax_fns2 = syntax_fns 2 HolKernel.dest_binop HolKernel.mk_binop; + val syntax_fns2_set = syntax_fns 3 HolKernel.dest_binop HolKernel.mk_binop; + val syntax_fns3 = syntax_fns 3 HolKernel.dest_triop HolKernel.mk_triop; in val (birs_gen_env_tm, mk_birs_gen_env, dest_birs_gen_env, is_birs_gen_env) = syntax_fns1_env "birs_gen_env"; val (bir_senv_GEN_list_tm, mk_bir_senv_GEN_list, dest_bir_senv_GEN_list, is_bir_senv_GEN_list) = syntax_fns1_env "bir_senv_GEN_list"; val (birs_exps_of_senv_tm, mk_birs_exps_of_senv, dest_birs_exps_of_senv, is_birs_exps_of_senv) = syntax_fns1_set "birs_exps_of_senv"; val (bir_pc_set_lbls_tm, mk_bir_pc_set_lbls, dest_bir_pc_set_lbls, is_bir_pc_set_lbls) = syntax_fns1_set "bir_pc_set_lbls"; + + val (birs_env_var_is_initialised_tm, mk_birs_env_var_is_initialised, dest_birs_env_var_is_initialised, is_birs_env_var_is_initialised) = syntax_fns3 "birs_env_var_is_initialised"; + val (birs_env_var_is_initialised_set_tm, mk_birs_env_var_is_initialised_set, dest_birs_env_var_is_initialised_set, is_birs_env_var_is_initialised_set) = syntax_fns2_set "birs_env_var_is_initialised"; + val (birs_env_vars_are_initialised_tm, mk_birs_env_vars_are_initialised, dest_birs_env_vars_are_initialised, is_birs_env_vars_are_initialised) = syntax_fns3 "birs_env_vars_are_initialised"; end; local diff --git a/src/tools/symbexec/birs_mergeLib.sml b/src/tools/symbexec/birs_mergeLib.sml index 1652f00e9..0631ad429 100644 --- a/src/tools/symbexec/birs_mergeLib.sml +++ b/src/tools/symbexec/birs_mergeLib.sml @@ -138,7 +138,7 @@ in (* local *) val thm_z = Profile.profile "zzz_5_stateacc" (CONV_RULE (birs_Pi_CONV (LAND_CONV ( birs_state_acc_CONV THENC GEN_match_conv is_birs_update_env ( - birs_stepLib.birs_update_env_CONV + bir_vars_ofLib.birs_update_env_CONV ) )))) thm3; val _ = if not debug then () else print "\nz: \n"; @@ -200,7 +200,7 @@ in (* local *) (* create updated state (pcond and env), and purge previous environment mapping *) val env_mod = mk_birs_update_env (pairSyntax.mk_pair (vn, exp_new), env_old); val _ = if not debug_mode then () else print "created update env exp\n"; - val env_new = (snd o dest_eq o concl o birs_stepLib.birs_update_env_CONV) env_mod; + val env_new = (snd o dest_eq o concl o bir_vars_ofLib.birs_update_env_CONV) env_mod; val _ = if not debug_mode then () else print "purged update env exp\n"; val pcond_new = bslSyntax.band (bslSyntax.beq (bslSyntax.bden symb_tm, exp_tm), pcond_old); val Pi_sys_new_tm = mk_birs_state (pc, env_new, status, pcond_new); diff --git a/src/tools/symbexec/birs_stepLib.sml b/src/tools/symbexec/birs_stepLib.sml index 0e6b398d3..2c3d693a3 100644 --- a/src/tools/symbexec/birs_stepLib.sml +++ b/src/tools/symbexec/birs_stepLib.sml @@ -898,19 +898,6 @@ fun birs_gen_env_CONV eq_thms = ) THENC TRY_CONV (REWR_CONV birs_gen_env_GET_NULL_thm); -val birs_update_env_P_CONV = - BETA_CONV THENC - NEG_CONV ( - LHS_CONV ( - REWR_CONV pairTheory.FST - ) THENC - bir_varname_EQ_CONV - ); - -val birs_update_env_CONV = - REWR_CONV birs_update_env_thm THENC - RAND_CONV (RAND_CONV (FILTER_CONV birs_update_env_P_CONV)); - fun birs_exec_stmtB_CONV eq_thms tm = let (* evaluate to symbolic expression *) @@ -949,7 +936,7 @@ in ( GEN_match_conv is_birs_update_env ( LAND_CONV (LAND_CONV (REWR_CONV bir_envTheory.bir_var_name_def)) THENC RAND_CONV (unabbrev_conv eq_thms) THENC - birs_update_env_CONV + bir_vars_ofLib.birs_update_env_CONV ))) res_b_option_bind; @@ -1271,8 +1258,6 @@ fun birs_exec_step_CONV_fun tm = val birs_symbval_concretizations_oracle_ext_CONV = birs_symbval_concretizations_oracle_ext_CONV; -val birs_update_env_CONV = birs_update_env_CONV; - end (* local *) end (* struct *) diff --git a/src/tools/symbexec/distribute_generic_stuffLib.sml b/src/tools/symbexec/distribute_generic_stuffLib.sml index 35d667334..59e08406f 100644 --- a/src/tools/symbexec/distribute_generic_stuffLib.sml +++ b/src/tools/symbexec/distribute_generic_stuffLib.sml @@ -51,31 +51,14 @@ fun Q_bircont_SOLVE3CONJS_TAC varset_thm = ( (* cleanup proof state *) REPEAT (POP_ASSUM (K ALL_TAC)) >> - (* concretize and normalize *) + (* goal is now a birs_env_vars_are_initialised predicate *) (* --- first the variable set *) REWRITE_TAC [GSYM varset_thm] >> - CONV_TAC (RAND_CONV (EVAL)) >> - (* --- then the symbolic environment *) - FULL_SIMP_TAC (std_ss++holBACore_ss++listSimps.LIST_ss) [birs_gen_env_def, birs_gen_env_fun_def, birs_gen_env_fun_def, bir_envTheory.bir_env_lookup_def] >> - (* --- then the symbol set *) - FULL_SIMP_TAC (std_ss++birs_state_ss) [birs_symb_symbols_thm, birs_auxTheory.birs_exps_of_senv_thm] >> - REPEAT (CHANGED_TAC (fn x => ( - FULL_SIMP_TAC (std_ss++holBACore_ss++listSimps.LIST_ss++pred_setLib.PRED_SET_ss++stringSimps.STRING_ss) [Once birs_auxTheory.birs_exps_of_senv_COMP_thm] - ) x)) >> - CONV_TAC (RATOR_CONV (RAND_CONV (computeLib.RESTR_EVAL_CONV [``bir_vars_of_exp``] THENC SIMP_CONV (std_ss++holBACore_ss) [] THENC EVAL))) >> - - (* finish the proof *) - REPEAT (CHANGED_TAC (fn x => ( - REWRITE_TAC [Once birs_env_vars_are_initialised_INSERT_thm, birs_env_vars_are_initialised_EMPTY_thm, birs_env_var_is_initialised_def] >> - let - val fix_tac = - EVAL_TAC >> - SIMP_TAC (std_ss++holBACore_ss) [bir_valuesTheory.BType_Bool_def] >> - EVAL_TAC; - in - (CONJ_TAC >- fix_tac) ORELSE (fix_tac) - end - ) x)) + CONV_TAC (RAND_CONV (EVAL THENC holba_convLib.LIST_TO_SET_CONV)) >> + (* --- then the symbols of the symbolic state *) + CONV_TAC (LAND_CONV (bir_vars_ofLib.birs_symb_symbols_DIRECT_CONV)) >> + (* --- symbolic environment is already in standard form and now combine the whole thing *) + CONV_TAC (bir_vars_ofLib.birs_env_vars_are_initialised_CONV) ) );