1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Crunch_Instances_NonDet 8imports 9 Crunch 10 WPEx 11 NonDetMonadVCG 12begin 13 14lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE 15 K_bind_def split_def bind_assoc bindE_assoc 16 trans[OF liftE_bindE return_bind] 17 18ML \<open> 19fun get_nondet_monad_state_type 20 (Type ("Product_Type.prod", 21 [Type ("Set.set", [Type ("Product_Type.prod", [_,v])]), 22 Type ("HOL.bool",[])])) 23 = SOME v 24 | get_nondet_monad_state_type _ = NONE 25 26structure CrunchValidInstance : CrunchInstance = 27struct 28 val name = "valid"; 29 type extra = term; 30 val eq_extra = ae_conv; 31 fun parse_extra ctxt extra 32 = case extra of 33 "" => error "A post condition is required" 34 | extra => let val pre = Syntax.parse_term ctxt extra 35 in (pre, Abs ("_", dummyT, pre)) end; 36 val has_preconds = true; 37 fun mk_term pre body post = 38 (Syntax.parse_term @{context} "valid") $ pre $ body $ post; 39 fun dest_term ((Const (@{const_name "valid"}, _)) $ pre $ body $ post) 40 = SOME (pre, body, post) 41 | dest_term _ = NONE; 42 fun put_precond pre ((v as Const (@{const_name "valid"}, _)) $ _ $ body $ post) 43 = v $ pre $ body $ post 44 | put_precond _ _ = error "put_precond: not a hoare triple"; 45 val pre_thms = @{thms "hoare_pre"}; 46 val wpc_tactic = wp_cases_tactic_weak; 47 val wps_tactic = wps_tac; 48 val magic = Syntax.parse_term @{context} 49 "\<lambda>mapp_lambda_ignore. valid P_free_ignore mapp_lambda_ignore Q_free_ignore"; 50 val get_monad_state_type = get_nondet_monad_state_type; 51end; 52 53structure CrunchValid : CRUNCH = Crunch(CrunchValidInstance); 54 55structure CrunchNoFailInstance : CrunchInstance = 56struct 57 val name = "no_fail"; 58 type extra = unit; 59 val eq_extra = op =; 60 fun parse_extra ctxt extra 61 = case extra of 62 "" => (Syntax.parse_term ctxt "%_. True", ()) 63 | _ => (Syntax.parse_term ctxt extra, ()); 64 val has_preconds = true; 65 fun mk_term pre body _ = 66 (Syntax.parse_term @{context} "no_fail") $ pre $ body; 67 fun dest_term ((Const (@{const_name "no_fail"}, _)) $ pre $ body) 68 = SOME (pre, body, ()) 69 | dest_term _ = NONE; 70 fun put_precond pre ((v as Const (@{const_name "no_fail"}, _)) $ _ $ body) 71 = v $ pre $ body 72 | put_precond _ _ = error "put_precond: not a no_fail term"; 73 val pre_thms = @{thms "no_fail_pre"}; 74 val wpc_tactic = wp_cases_tactic_weak; 75 fun wps_tactic _ _ _ = no_tac; 76 val magic = Syntax.parse_term @{context} 77 "\<lambda>mapp_lambda_ignore. no_fail P_free_ignore mapp_lambda_ignore"; 78 val get_monad_state_type = get_nondet_monad_state_type; 79end; 80 81structure CrunchNoFail : CRUNCH = Crunch(CrunchNoFailInstance); 82 83structure CrunchEmptyFailInstance : CrunchInstance = 84struct 85 val name = "empty_fail"; 86 type extra = unit; 87 val eq_extra = op =; 88 fun parse_extra ctxt extra 89 = case extra of 90 "" => (Syntax.parse_term ctxt "%_. True", ()) 91 | _ => error "empty_fail does not need a precondition"; 92 val has_preconds = false; 93 fun mk_term _ body _ = 94 (Syntax.parse_term @{context} "empty_fail") $ body; 95 fun dest_term (Const (@{const_name empty_fail}, _) $ b) 96 = SOME (Term.dummy, b, ()) 97 | dest_term _ = NONE; 98 fun put_precond _ _ = error "crunch empty_fail should not be calling put_precond"; 99 val pre_thms = []; 100 val wpc_tactic = wp_cases_tactic_weak; 101 fun wps_tactic _ _ _ = no_tac; 102 val magic = Syntax.parse_term @{context} 103 "\<lambda>mapp_lambda_ignore. empty_fail mapp_lambda_ignore"; 104 val get_monad_state_type = get_nondet_monad_state_type; 105end; 106 107structure CrunchEmptyFail : CRUNCH = Crunch(CrunchEmptyFailInstance); 108 109structure CrunchValidEInstance : CrunchInstance = 110struct 111 val name = "valid_E"; 112 type extra = term * term; 113 fun eq_extra ((a, b), (c, d)) = (ae_conv (a, c) andalso ae_conv (b, d)); 114 fun parse_extra ctxt extra 115 = case extra of 116 "" => error "A post condition is required" 117 | extra => let val pre = Syntax.parse_term ctxt extra 118 in (pre, (Abs ("_", dummyT, pre), Abs ("_", dummyT, pre))) end; 119 val has_preconds = true; 120 fun mk_term pre body extra = 121 (Syntax.parse_term @{context} "validE") $ pre $ body $ fst extra $ snd extra; 122 fun dest_term (Const (@{const_name "validE"}, _) $ pre $ body $ p1 $ p2) 123 = SOME (pre, body, (p1, p2)) 124 | dest_term _ = NONE; 125 fun put_precond pre ((v as Const (@{const_name "validE"}, _)) $ _ $ body $ post $ post') 126 = v $ pre $ body $ post $ post' 127 | put_precond _ _ = error "put_precond: not a validE term"; 128 val pre_thms = @{thms "hoare_pre"}; 129 val wpc_tactic = wp_cases_tactic_weak; 130 val wps_tactic = wps_tac; 131 val magic = Syntax.parse_term @{context} 132 "\<lambda>mapp_lambda_ignore. validE P_free_ignore mapp_lambda_ignore Q_free_ignore Q_free_ignore"; 133 val get_monad_state_type = get_nondet_monad_state_type; 134end; 135 136structure CrunchValidE : CRUNCH = Crunch(CrunchValidEInstance); 137\<close> 138 139setup \<open> 140 add_crunch_instance "" (CrunchValid.crunch_x, CrunchValid.crunch_ignore_add_del) 141\<close> 142setup \<open> 143 add_crunch_instance "valid" (CrunchValid.crunch_x, CrunchValid.crunch_ignore_add_del) 144\<close> 145setup \<open> 146 add_crunch_instance "no_fail" (CrunchNoFail.crunch_x, CrunchNoFail.crunch_ignore_add_del) 147\<close> 148setup \<open> 149 add_crunch_instance "empty_fail" (CrunchEmptyFail.crunch_x, CrunchEmptyFail.crunch_ignore_add_del) 150\<close> 151 152end