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