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