1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8 * Configuring type strengthen rules.
9 * Based on type_strengthen.thy.
10 *)
11theory type_strengthen_tricks imports
12  "AutoCorres.AutoCorres"
13begin
14
15external_file "type_strengthen.c"
16install_C_file "type_strengthen.c"
17
18(* We can configure the type strengthen rules individually.
19   For example, suppose that we do not want to lift loops to the option monad: *)
20declare gets_theE_L2_while [ts_rule option del]
21
22(* We can also specify which monads are used for type strengthening.
23   Here, we exclude the read-only monad completely, and specify
24   rules for some individual functions. *)
25autocorres [
26  ts_rules = pure option nondet,
27  ts_force option = pure_f
28  ] "type_strengthen.c"
29
30context type_strengthen begin
31
32(* pure_f (and indirectly, pure_f2) are now lifted to the option monad. *)
33thm pure_f'_def pure_f2'_def
34thm pure_g'_def pure_h'_def
35    pure_i'_def pure_j'_def pure_k'_def pure_div_roundup'_def
36(* gets_f and gets_g are now lifted to the option monad. *)
37thm gets_f'_def gets_g'_def
38thm opt_f'_def opt_g'_def opt_h'.simps opt_i'_def
39    opt_j'_def opt_a'.simps opt_a2'_def
40(* opt_l is now lifted to the state monad. *)
41thm opt_l'_def
42thm st_f'_def st_g'_def st_h'_def st_i'.simps (* hax'_def *)
43thm exc_f'_def
44
45(* Check the above claims. *)
46term "pure_f' :: lifted_globals \<Rightarrow> unit option"
47term "pure_f2' :: lifted_globals \<Rightarrow> unit option"
48term "pure_g' :: ure_C ptr \<Rightarrow> ure_C ptr"
49term "pure_h' :: ure_C ptr \<Rightarrow> int"
50term "pure_i' :: int \<Rightarrow> int"
51term "pure_j' :: ure_C \<Rightarrow> int"
52term "pure_k' :: ure_C \<Rightarrow> int"
53term "pure_div_roundup' :: word32 \<Rightarrow> word32 \<Rightarrow> word32"
54term "gets_f' :: lifted_globals \<Rightarrow> word32 option"
55term "gets_g' :: lifted_globals \<Rightarrow> word32 option"
56term "opt_f' :: word32 ptr \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
57term "opt_g' :: int \<Rightarrow> lifted_globals \<Rightarrow> int option"
58term "opt_h' :: nat \<Rightarrow> ure_C ptr \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
59term "opt_i' :: (lifted_globals, int) nondet_monad"
60term "opt_j' :: ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> lifted_globals \<Rightarrow> int option"
61term "opt_a' :: nat \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> lifted_globals \<Rightarrow> word32 option"
62term "opt_a2' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
63term "opt_l' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
64term "st_f' :: ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> (lifted_globals, unit) nondet_monad"
65term "st_g' :: word32 ptr \<Rightarrow> (lifted_globals, word32) nondet_monad"
66term "st_h' :: word32 \<Rightarrow> (lifted_globals, word32) nondet_monad"
67term "st_i' :: nat \<Rightarrow> ure_C ptr \<Rightarrow> ure_C ptr \<Rightarrow> (lifted_globals, ure_C ptr) nondet_monad"
68term "exc_f' :: word8 ptr \<Rightarrow> 32 signed word ptr \<Rightarrow> (lifted_globals, int) nondet_monad"
69end
70
71end
72