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