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