-
Notifications
You must be signed in to change notification settings - Fork 0
/
Crunch_Instances_NonDet.thy
152 lines (139 loc) · 5.38 KB
/
Crunch_Instances_NonDet.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
152
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory Crunch_Instances_NonDet
imports
Crunch
"Monad_WP/wp/WPEx"
"Monad_WP/NonDetMonadVCG"
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_nondet_monad_state_type
(Type ("Product_Type.prod",
[Type ("Set.set", [Type ("Product_Type.prod", [_,v])]),
Type ("HOL.bool",[])]))
= SOME v
| get_nondet_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;
val wps_tactic = wps_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_nondet_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_nondet_monad_state_type;
end;
structure CrunchNoFail : CRUNCH = Crunch(CrunchNoFailInstance);
structure CrunchEmptyFailInstance : CrunchInstance =
struct
val name = "empty_fail";
type extra = unit;
val eq_extra = op =;
fun parse_extra ctxt extra
= case extra of
"" => (Syntax.parse_term ctxt "%_. True", ())
| _ => error "empty_fail does not need a precondition";
val has_preconds = false;
fun mk_term _ body _ =
(Syntax.parse_term @{context} "empty_fail") $ body;
fun dest_term (Const (@{const_name empty_fail}, _) $ b)
= SOME (Term.dummy, b, ())
| dest_term _ = NONE;
fun put_precond _ _ = error "crunch empty_fail 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. empty_fail mapp_lambda_ignore";
val get_monad_state_type = get_nondet_monad_state_type;
end;
structure CrunchEmptyFail : CRUNCH = Crunch(CrunchEmptyFailInstance);
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;
val wps_tactic = wps_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_nondet_monad_state_type;
end;
structure CrunchValidE : CRUNCH = Crunch(CrunchValidEInstance);
\<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 "empty_fail" (CrunchEmptyFail.crunch_x, CrunchEmptyFail.crunch_ignore_add_del)
\<close>
end