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