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