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