From dadcd8f65bd040d81f57279acfb7f9b5c46137c2 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 22 May 2019 12:20:53 +1000 Subject: [PATCH] c-parser: update to cartouches --- tools/c-parser/CProof.thy | 20 +++--- tools/c-parser/PackedTypes.thy | 46 ++++++------- tools/c-parser/StaticFun.thy | 4 +- tools/c-parser/testfiles/attributes.thy | 12 ++-- tools/c-parser/testfiles/codetests.thy | 8 +-- tools/c-parser/testfiles/fncall.thy | 4 +- tools/c-parser/testfiles/fnptr.thy | 4 +- tools/c-parser/testfiles/gcc_attribs.thy | 4 +- .../c-parser/testfiles/initialised_decls.thy | 4 +- tools/c-parser/testfiles/jiraver150.thy | 2 +- tools/c-parser/testfiles/jiraver313.thy | 6 +- tools/c-parser/testfiles/jiraver434.thy | 4 +- tools/c-parser/testfiles/jiraver456.thy | 4 +- tools/c-parser/testfiles/longlong.thy | 2 +- tools/c-parser/testfiles/many_local_vars.thy | 2 +- tools/c-parser/testfiles/modifies_speed.thy | 10 +-- tools/c-parser/testfiles/multi_deref.thy | 8 +-- .../c-parser/testfiles/parse_struct_array.thy | 8 +-- tools/c-parser/testfiles/parse_switch.thy | 8 +-- tools/c-parser/umm_heap/ArrayAssertion.thy | 18 ++--- tools/c-parser/umm_heap/Arrays.thy | 4 +- tools/c-parser/umm_heap/CTypes.thy | 2 +- tools/c-parser/umm_heap/CTypesBase.thy | 10 +-- tools/c-parser/umm_heap/CTypesDefs.thy | 24 +++---- tools/c-parser/umm_heap/CompoundCTypesEx.thy | 2 +- tools/c-parser/umm_heap/MapExtra.thy | 68 +++++++++---------- tools/c-parser/umm_heap/SepCode.thy | 2 +- tools/c-parser/umm_heap/SepFrame.thy | 2 +- tools/c-parser/umm_heap/SepInv.thy | 6 +- tools/c-parser/umm_heap/SepTactic.thy | 22 +++--- tools/c-parser/umm_heap/Separation.thy | 6 +- tools/c-parser/umm_heap/TypHeap.thy | 2 +- 32 files changed, 164 insertions(+), 164 deletions(-) diff --git a/tools/c-parser/CProof.thy b/tools/c-parser/CProof.thy index 82e3017cd..2073b76cb 100644 --- a/tools/c-parser/CProof.thy +++ b/tools/c-parser/CProof.thy @@ -41,9 +41,9 @@ ML_file "name_generation.ML" (* set up hoare package to rewrite state updates more *) -setup {* +setup \ Hoare.add_foldcongsimps [@{thm "update_update"}, @{thm "o_def"}] -*} +\ (* Syntax for apply antiquotation parsing explicitly *) @@ -71,7 +71,7 @@ definition hrs_id :: "heap_raw_state \ heap_raw_state" where declare hrs_id_def [simp add] -parse_translation {* +parse_translation \ let fun ac x = Syntax.const "_antiquoteCur" $ Syntax.const x fun aco x y = Syntax.const y $ (Syntax.const "globals" $ x) @@ -90,11 +90,11 @@ let fun heap_assert_tr [b] = repl b | heap_assert_tr ts = raise TERM ("heap_assert_tr", ts); in [("_heap",K heap_assert_tr)] end; -*} +\ (* Separation logic assertion parse translation *) -parse_translation {* +parse_translation \ let fun ac x = Syntax.const "_antiquoteCur" $ Syntax.const x fun aco x y = Syntax.const y $ (Syntax.const "globals" $ x) @@ -121,7 +121,7 @@ let fun sep_tr [t] = Syntax.const "sep_app" $ (*new_heap *) t $ hd ac | sep_tr ts = raise TERM ("sep_tr", ts); in [("_sep_assert",K sep_tr)] end; -*} +\ definition c_null_guard :: "'a::c_type ptr_guard" where @@ -280,7 +280,7 @@ syntax (output) "_Deref" :: "'b \ 'b" ("*_" [1000] 1000) "_AssignH" :: "'b => 'b => ('a,'p,'f) com" ("(2*_ :==/ _)" [30, 30] 23) -print_translation {* +print_translation \ let fun deref (Const ("_antiquoteCur",_)$Const (h,_)) p = if h=NameGeneration.global_heap then Syntax.const "_Deref" $ p else @@ -301,14 +301,14 @@ let fun assign_tr [l,r] = deref_assign l r | assign_tr ts = raise Match in [("CTypesDefs.lift",K lift_tr),("_Assign",K assign_tr)] end; -*} +\ -print_translation {* +print_translation \ let fun sep_app_tr [l,r] = Syntax.const "_sep_assert" $ l | sep_app_tr ts = raise Match in [("sep_app",K sep_app_tr)] end; -*} +\ syntax "_h_t_valid" :: "'a::c_type ptr \ bool" ("\\<^sub>t _" [99] 100) diff --git a/tools/c-parser/PackedTypes.thy b/tools/c-parser/PackedTypes.thy index 7e7be01b2..bcb425369 100644 --- a/tools/c-parser/PackedTypes.thy +++ b/tools/c-parser/PackedTypes.thy @@ -12,9 +12,9 @@ theory PackedTypes imports "Word_Lib.WordSetup" CProof begin -section {* Underlying definitions for the class axioms *} +section \Underlying definitions for the class axioms\ -text {* field_access / field_update is the identity for packed types *} +text \field_access / field_update is the identity for packed types\ definition "fa_fu_idem fd n \ @@ -39,7 +39,7 @@ where lemmas td_fafu_idem_simps = fai0 fai1 fai2 fai3 fai4 fai5 -text {* field_access is independent of the underlying bytes *} +text \field_access is independent of the underlying bytes\ definition "fa_heap_indep fd n \ @@ -64,7 +64,7 @@ where lemmas td_fa_hi_simps = fahi0 fahi1 fahi2 fahi3 fahi4 fahi5 -section {* Lemmas about td_fafu_idem *} +section \Lemmas about td_fafu_idem\ lemma field_lookup_td_fafu_idem: shows "\(s :: 'a field_desc typ_desc) f m n. \ field_lookup t f m = Some (s, n); td_fafu_idem t \ \ td_fafu_idem s" @@ -225,7 +225,7 @@ next by (rule field_lookup_offset2_list [where m = 0, simplified]) show "access_ti_list ts' (update_ti s bs v) (drop (size_td (dt_fst p')) bs') ! (x - size_td (dt_fst p')) = bs ! (x - n)" - using mlt nlex xln lbs lbs' wf wfts `td_fafu_idem s` `wf_fd s` + using mlt nlex xln lbs lbs' wf wfts \td_fafu_idem s\ \wf_fd s\ by (simp add: Cons_typ_desc.hyps(2) [OF fl'] size_td_pair_dt_fst) qed } @@ -244,13 +244,13 @@ next apply simp done - hence ?case using wf lbs lbs' nlex xln wf wfts `td_fafu_idem s` `wf_fd s` + hence ?case using wf lbs lbs' nlex xln wf wfts \td_fafu_idem s\ \wf_fd s\ by (simp add: nth_append length_fa_ti access_ti_pair_dt_fst size_td_pair_dt_fst ih[OF fl]) } - ultimately show ?case using `field_lookup_list (p' # ts') f 0 = Some (s, n)` by (simp split: option.splits) + ultimately show ?case using \field_lookup_list (p' # ts') f 0 = Some (s, n)\ by (simp split: option.splits) qed (clarsimp split: if_split_asm)+ -subsection {* td_fa_hi *} +subsection \td_fa_hi\ (* \ size_of TYPE('a::mem_type) \ length h; size_of TYPE('a) \ length h' \ \ *) @@ -302,9 +302,9 @@ next by simp (erule (2) DTPair_typ_desc.hyps) qed -section {* Simp rules for deriving packed props from the type combinators *} +section \Simp rules for deriving packed props from the type combinators\ -subsection {* td_fafu_idem *} +subsection \td_fafu_idem\ lemma td_fafu_idem_final_pad: "padup (2 ^ align_td t) (size_td t) = 0 @@ -455,7 +455,7 @@ lemma td_fafu_idem_empty_typ_info: unfolding empty_typ_info_def by simp -subsection {* td_fa_hi *} +subsection \td_fa_hi\ (* These are mostly identical to the above --- surely there is something which implies both? *) @@ -586,11 +586,11 @@ lemma td_fa_hi_empty_typ_info: unfolding empty_typ_info_def by simp -section {* The type class and simp sets *} +section \The type class and simp sets\ -text {* Packed types, with no padding, have the defining property that +text \Packed types, with no padding, have the defining property that access is invariant under substitution of the underlying heap and - access/update is the identity *} + access/update is the identity\ class packed_type = mem_type + assumes td_fafu_idem: "td_fafu_idem (typ_info_t TYPE('a::c_type))" @@ -630,9 +630,9 @@ next case (Cons x xs) thus ?case by (simp add: min_def ac_simps drop_take) qed -section {* Instances *} +section \Instances\ -text {* Words (of multiple of 8 size) are packed *} +text \Words (of multiple of 8 size) are packed\ instantiation word :: (len8) packed_type begin @@ -643,7 +643,7 @@ instance done end -text {* Pointers are always packed *} +text \Pointers are always packed\ instantiation ptr :: (c_type)packed_type begin @@ -654,7 +654,7 @@ instance done end -text {* Arrays of packed types are in turn packed *} +text \Arrays of packed types are in turn packed\ class array_outer_packed = packed_type + array_outer_max_size class array_inner_packed = array_outer_packed + array_inner_max_size @@ -670,9 +670,9 @@ instance array :: (array_outer_packed, array_max_count) packed_type instance array :: (array_inner_packed, array_max_count) array_outer_packed .. -section {* Theorems about packed types *} +section \Theorems about packed types\ -subsection {* td_fa_hi *} +subsection \td_fa_hi\ lemma heap_independence: "\length h = size_of TYPE('a :: packed_type); length h' = size_of TYPE('a) \ @@ -705,7 +705,7 @@ lemma packed_heap_update_collapse_hrs: unfolding hrs_mem_update_def by (simp add: split_def packed_heap_update_collapse) -subsection {* td_fafu_idem *} +subsection \td_fafu_idem\ lemma order_leE: fixes x :: "'a :: order" @@ -771,10 +771,10 @@ next show ?case proof (cases n') - case 0 thus ?thesis using `Suc m' < n'` by simp + case 0 thus ?thesis using \Suc m' < n'\ by simp next case (Suc n'') - hence "m' < n''" using `Suc m' < n'` by simp + hence "m' < n''" using \Suc m' < n'\ by simp thus ?thesis using Suc by (simp add: Suc.hyps ac_simps) qed diff --git a/tools/c-parser/StaticFun.thy b/tools/c-parser/StaticFun.thy index 0a1ac226f..399220809 100644 --- a/tools/c-parser/StaticFun.thy +++ b/tools/c-parser/StaticFun.thy @@ -60,7 +60,7 @@ lemma tree_eq_fun_in_range_split: apply fastforce done -ML {* +ML \ structure StaticFun = struct @@ -137,7 +137,7 @@ fun define_tree_and_thms_with_defs name names key_defs opt_values ord ctxt = let end -*} +\ (* testing diff --git a/tools/c-parser/testfiles/attributes.thy b/tools/c-parser/testfiles/attributes.thy index 37ff791c6..a85cf0e46 100644 --- a/tools/c-parser/testfiles/attributes.thy +++ b/tools/c-parser/testfiles/attributes.thy @@ -14,7 +14,7 @@ begin install_C_file "attributes.c" -ML {* +ML \ local open ProgramAnalysis in @@ -22,18 +22,18 @@ fun global_details vi = (srcname vi, length (get_vi_attrs vi)) val all_global_details = get_globals #> map global_details end -*} +\ -ML {* +ML \ val results = CalculateState.get_csenv @{theory} "attributes.c" |> the |> all_global_details |> sort (prod_ord string_ord int_ord) -*} +\ -ML {* +ML \ val _ = if results = [("u",1), ("v", 1)] then () else error "Test case failure" -*} +\ end diff --git a/tools/c-parser/testfiles/codetests.thy b/tools/c-parser/testfiles/codetests.thy index 7fbcff8d1..86aa665b4 100644 --- a/tools/c-parser/testfiles/codetests.thy +++ b/tools/c-parser/testfiles/codetests.thy @@ -12,20 +12,20 @@ theory codetests imports "CParser.CTranslation" begin -ML {* Context.>> (Context.map_theory ( +ML \Context.>> (Context.map_theory ( TermsTypes.prim_mk_defn "foo" @{term "33::nat"})) -*} +\ thm foo_def -ML {* +ML \ Context.>> (Context.map_theory ( RecursiveRecordPackage.define_record_type [ {record_name = "myrecord", fields = [{fldname = "fld1", fldty = @{typ "nat"}}, {fldname = "myset", fldty = @{typ "nat \ bool"}}]} ])) -*} +\ thm myrecord_accupd_same diff --git a/tools/c-parser/testfiles/fncall.thy b/tools/c-parser/testfiles/fncall.thy index f1febaf80..a944025d3 100644 --- a/tools/c-parser/testfiles/fncall.thy +++ b/tools/c-parser/testfiles/fncall.thy @@ -20,11 +20,11 @@ where "fac 0 = 1" | "fac (Suc n) = (Suc n) * fac n" -ML {* +ML \ val ast = IsarInstall.get_Csyntax @{theory} "fncall.c" -*} +\ external_file "fncall.c" install_C_file "fncall.c" diff --git a/tools/c-parser/testfiles/fnptr.thy b/tools/c-parser/testfiles/fnptr.thy index cfd1fee79..c2cfe29bd 100644 --- a/tools/c-parser/testfiles/fnptr.thy +++ b/tools/c-parser/testfiles/fnptr.thy @@ -12,9 +12,9 @@ theory fnptr imports "CParser.CTranslation" begin -ML {* +ML \ IsarInstall.install_C_file ((((NONE,NONE),NONE),"fnptr.c"),NONE) @{theory} -*} +\ external_file "fnptr.c" install_C_file "fnptr.c" diff --git a/tools/c-parser/testfiles/gcc_attribs.thy b/tools/c-parser/testfiles/gcc_attribs.thy index 02a86b33d..e5dc70519 100644 --- a/tools/c-parser/testfiles/gcc_attribs.thy +++ b/tools/c-parser/testfiles/gcc_attribs.thy @@ -21,10 +21,10 @@ begin thm f_body_def end -ML {* +ML \ val SOME cse = CalculateState.get_csenv @{theory} "gcc_attribs.c" val spec1 = Symtab.lookup (ProgramAnalysis.function_specs cse) "myexit" val spec2 = Symtab.lookup (ProgramAnalysis.function_specs cse) "myexit2" -*} +\ end diff --git a/tools/c-parser/testfiles/initialised_decls.thy b/tools/c-parser/testfiles/initialised_decls.thy index 7728f6e7c..fa9a9b6d4 100644 --- a/tools/c-parser/testfiles/initialised_decls.thy +++ b/tools/c-parser/testfiles/initialised_decls.thy @@ -21,7 +21,7 @@ thm f_body_def thm g_body_def end -text {* +text \ Following proof confirms that we can prove stuff about g without needing to prove that f is side-effect free; which ain't true. The translation doesn't incorrectly reckon that the initialisation of local variable i @@ -29,7 +29,7 @@ text {* This proof still works, but there aren't side-effect-free guards inserted at any point in the current translation so the point is a bit moot. -*} +\ lemma (in initialised_decls_global_addresses) foo: shows "\ \ \ True \ \ret__int :== PROC g() \ \ret__int = 3 \" diff --git a/tools/c-parser/testfiles/jiraver150.thy b/tools/c-parser/testfiles/jiraver150.thy index 47187fdef..3f7934774 100644 --- a/tools/c-parser/testfiles/jiraver150.thy +++ b/tools/c-parser/testfiles/jiraver150.thy @@ -20,7 +20,7 @@ declare [[use_anonymous_local_variables=true]] context jiraver150 begin - ML {* @{const_name "unsigned_char'local0_'"} *} + ML \@{const_name "unsigned_char'local0_'"}\ thm f_body_def thm f2_body_def diff --git a/tools/c-parser/testfiles/jiraver313.thy b/tools/c-parser/testfiles/jiraver313.thy index dd0323d77..dba086ce8 100644 --- a/tools/c-parser/testfiles/jiraver313.thy +++ b/tools/c-parser/testfiles/jiraver313.thy @@ -12,14 +12,14 @@ theory jiraver313 imports "CParser.CTranslation" begin -ML {* Feedback.verbosity_level := 6 *} +ML \Feedback.verbosity_level := 6\ declare [[calculate_modifies_proofs = false ]] external_file "jiraver313.c" install_C_file memsafe "jiraver313.c" -ML {* +ML \ local open Absyn val cpp_record = @@ -31,7 +31,7 @@ in val Decl d = hd decls val VarDecl vd = RegionExtras.node d end -*} +\ context jiraver313 begin diff --git a/tools/c-parser/testfiles/jiraver434.thy b/tools/c-parser/testfiles/jiraver434.thy index c3df190c9..6eb1a202c 100644 --- a/tools/c-parser/testfiles/jiraver434.thy +++ b/tools/c-parser/testfiles/jiraver434.thy @@ -21,14 +21,14 @@ begin thm useContext_body_def term "r2_C_update" -ML {* +ML \ val Const(nm, ty) = @{term "ucptr_'"} val (d, r) = TermsTypes.dom_rng ty val (pointedTo_tyname, []) = dest_Type (TermsTypes.dest_ptr_ty r) val basename = List.last (String.fields (fn c => c = #".") pointedTo_tyname) val _ = basename = NameGeneration.mkAnonStructName 1 orelse raise Fail "anonymous struct has unexpected name" -*} +\ end (* context *) diff --git a/tools/c-parser/testfiles/jiraver456.thy b/tools/c-parser/testfiles/jiraver456.thy index 753d3f43f..0ee39b87c 100644 --- a/tools/c-parser/testfiles/jiraver456.thy +++ b/tools/c-parser/testfiles/jiraver456.thy @@ -23,7 +23,7 @@ thm f0_body_def thm f1_body_def thm f2_body_def -ML {* +ML \ fun count c th = let @@ -37,7 +37,7 @@ val f = count @{const Div_0}; (f @{thm f1_body_def} = 1 andalso f @{thm f2_body_def} = 1 andalso f @{thm f0_body_def} = 1) orelse OS.Process.exit OS.Process.failure -*} +\ end diff --git a/tools/c-parser/testfiles/longlong.thy b/tools/c-parser/testfiles/longlong.thy index 01b8f6c35..ab3bd82ef 100644 --- a/tools/c-parser/testfiles/longlong.thy +++ b/tools/c-parser/testfiles/longlong.thy @@ -15,7 +15,7 @@ begin external_file "longlong.c" install_C_file "longlong.c" -ML {* NameGeneration.return_var_name (Absyn.Signed Absyn.LongLong) *} +ML \NameGeneration.return_var_name (Absyn.Signed Absyn.LongLong)\ context longlong diff --git a/tools/c-parser/testfiles/many_local_vars.thy b/tools/c-parser/testfiles/many_local_vars.thy index 9c48d8d54..e79bc5a6b 100644 --- a/tools/c-parser/testfiles/many_local_vars.thy +++ b/tools/c-parser/testfiles/many_local_vars.thy @@ -23,7 +23,7 @@ install_C_file "many_local_vars.c" context "many_local_vars_global_addresses" begin lemma "\\. \ \\<^bsub>/UNIV\<^esub> {\} Call test_'proc {t. t may_not_modify_globals \}" - apply (tactic {* HoarePackage.vcg_tac "_modifies" "false" [] @{context} 1 *}) + apply (tactic \HoarePackage.vcg_tac "_modifies" "false" [] @{context} 1\) done end diff --git a/tools/c-parser/testfiles/modifies_speed.thy b/tools/c-parser/testfiles/modifies_speed.thy index fb0211e92..42e0dbb06 100644 --- a/tools/c-parser/testfiles/modifies_speed.thy +++ b/tools/c-parser/testfiles/modifies_speed.thy @@ -12,9 +12,9 @@ theory modifies_speed imports "CParser.CTranslation" begin -text {* Speed test for modifies proofs. *} +text \Speed test for modifies proofs.\ -ML {* +ML \ fun filename_relative thy name = Path.append (Resources.master_directory thy) (Path.explode name) @@ -44,11 +44,11 @@ fun write_speed_test_file n_globs n_funcs = let List.app write_func (1 upto n_funcs); TextIO.closeOut f end -*} +\ -ML {* +ML \ write_speed_test_file 10 40 -*} +\ declare [[sorry_modifies_proofs = false]] diff --git a/tools/c-parser/testfiles/multi_deref.thy b/tools/c-parser/testfiles/multi_deref.thy index 758c78bdd..27f96372b 100644 --- a/tools/c-parser/testfiles/multi_deref.thy +++ b/tools/c-parser/testfiles/multi_deref.thy @@ -20,19 +20,19 @@ context multi_deref_global_addresses begin thm f_body_def (* only 1 C_Guard; see JIRA VER-85 *) thm g_body_def (* 2 C_Guards, one per deref; see JIRA VER-152 *) -ML {* +ML \ val th = @{thm g_body_def} val t = Thm.concl_of th fun incifGuard (@{const "C_Guard"}) i = i + 1 | incifGuard _ i = i -*} +\ -ML {* +ML \ fold_aterms incifGuard t 0 = 2 orelse OS.Process.exit OS.Process.failure -*} +\ end diff --git a/tools/c-parser/testfiles/parse_struct_array.thy b/tools/c-parser/testfiles/parse_struct_array.thy index b83499e15..f73efd5d9 100644 --- a/tools/c-parser/testfiles/parse_struct_array.thy +++ b/tools/c-parser/testfiles/parse_struct_array.thy @@ -28,14 +28,14 @@ begin thm ts20110511_1_body_def thm ts20110511_2_body_def -ML {* +ML \ val bthm = @{thm "ts20110511_1_body_def"} val b_t = Thm.concl_of bthm val cs = Term.add_consts b_t [] -*} +\ -ML {* member (=) (map #1 cs) "CProof.strictc_errortype.C_Guard" orelse - OS.Process.exit OS.Process.failure *} +ML \member (=) (map #1 cs) "CProof.strictc_errortype.C_Guard" orelse + OS.Process.exit OS.Process.failure\ end diff --git a/tools/c-parser/testfiles/parse_switch.thy b/tools/c-parser/testfiles/parse_switch.thy index debaef1bd..fe8e0893a 100644 --- a/tools/c-parser/testfiles/parse_switch.thy +++ b/tools/c-parser/testfiles/parse_switch.thy @@ -24,16 +24,16 @@ thm h_body_def thm j_body_def thm k_body_def -ML {* +ML \ val kthm = @{thm k_body_def} val k_t = Thm.concl_of kthm val cs = Term.add_consts k_t [] -*} +\ -ML {* +ML \ member (=) (map #1 cs) "CProof.strictc_errortype.C_Guard" orelse OS.Process.exit OS.Process.failure -*} +\ end diff --git a/tools/c-parser/umm_heap/ArrayAssertion.thy b/tools/c-parser/umm_heap/ArrayAssertion.thy index acfa5b7a2..ca55c8fa4 100644 --- a/tools/c-parser/umm_heap/ArrayAssertion.thy +++ b/tools/c-parser/umm_heap/ArrayAssertion.thy @@ -67,15 +67,15 @@ lemma typ_uinfo_array_tag_n_m_eq: by (simp add: typ_uinfo_t_def typ_info_array array_tag_def uinfo_array_tag_n_m_eq) -text {* Alternative to h_t_valid for arrays. This allows reasoning -about arrays of variable width. *} +text \Alternative to h_t_valid for arrays. This allows reasoning +about arrays of variable width.\ definition h_t_array_valid :: "heap_typ_desc \ ('a :: c_type) ptr \ nat \ bool" where "h_t_array_valid htd ptr n = valid_footprint htd (ptr_val ptr) (uinfo_array_tag_n_m TYPE ('a) n n)" -text {* Assertion that pointer p is within an array that continues -for at least n more elements. *} +text \Assertion that pointer p is within an array that continues +for at least n more elements.\ definition "array_assertion (p :: ('a :: c_type) ptr) n htd = (\q i j. h_t_array_valid htd q j @@ -120,7 +120,7 @@ lemma array_ptr_valid_array_assertionI: by (auto dest: array_ptr_valid_array_assertionD simp: array_assertion_shrink_right) -text {* Derived from array_assertion, an appropriate assertion for performing +text \Derived from array_assertion, an appropriate assertion for performing a pointer addition, or for dereferencing a pointer addition (the strong case). In either case, there must be an array connecting the two ends of the pointer @@ -128,7 +128,7 @@ transition, with the caveat that the last address can be just out of the array if the pointer is not dereferenced, thus the strong/weak distinction. If the pointer doesn't actually move, nothing is learned. -*} +\ definition ptr_add_assertion :: "('a :: c_type) ptr \ int \ bool \ heap_typ_desc \ bool" where @@ -155,8 +155,8 @@ lemma ptr_add_assertion_uint[simp]: by (simp add: ptr_add_assertion_positive uint_0_iff unat_def split: bool.split) -text {* Ignore char and void pointers. The C standard specifies that arithmetic on -char and void pointers doesn't create any special checks. *} +text \Ignore char and void pointers. The C standard specifies that arithmetic on +char and void pointers doesn't create any special checks.\ definition ptr_add_assertion' :: "('a :: c_type) ptr \ int \ bool \ heap_typ_desc \ bool" @@ -176,7 +176,7 @@ lemma typ_name_void: lemmas ptr_add_assertion' = ptr_add_assertion'_def td_diff_from_typ_name typ_name_void -text {* Mechanism for retyping a range of memory to a non-constant array size. *} +text \Mechanism for retyping a range of memory to a non-constant array size.\ definition ptr_arr_retyps :: "nat \ ('a :: c_type) ptr \ heap_typ_desc \ heap_typ_desc" diff --git a/tools/c-parser/umm_heap/Arrays.thy b/tools/c-parser/umm_heap/Arrays.thy index 5a4a139aa..302dadc60 100644 --- a/tools/c-parser/umm_heap/Arrays.thy +++ b/tools/c-parser/umm_heap/Arrays.thy @@ -56,7 +56,7 @@ next then obtain b B where S: "S = insert b B \ b \ B \ card B = n \ (n = 0 \ B = {})" by (auto simp: card_Suc_eq) - with `finite S` Suc.hyps [of B] + with \finite S\ Suc.hyps [of B] obtain f where IH: "(\m B) \ (\x. x \ B \ (\!m. m < n \ f m = x))" by auto define f' where "f' \ \m. if m = card B then b else f m" from Suc.prems S IH @@ -87,7 +87,7 @@ lemma forall_finite_index: by (metis (mono_tags, hide_lams) finite_index_works) -section {* Finite Cartesian Products *} +section \Finite Cartesian Products\ typedef ('a,'n::finite) array ("_[_]" [30,0] 31) = "UNIV :: ('n => 'a) set" by simp diff --git a/tools/c-parser/umm_heap/CTypes.thy b/tools/c-parser/umm_heap/CTypes.thy index 4c7ded059..c97dc7f7a 100644 --- a/tools/c-parser/umm_heap/CTypes.thy +++ b/tools/c-parser/umm_heap/CTypes.thy @@ -80,7 +80,7 @@ lemma update_ti_pair_t_dtpair [simp]: "update_ti_pair_t (DTPair t f) = update_ti_t t" by (rule ext, simp add: update_ti_pair_t_def update_ti_t_def) -text {* --------------------------------------------------------------- *} +text \---------------------------------------------------------------\ lemma field_desc_empty [simp]: "field_desc (TypDesc (TypAggregate []) nm) = \ field_access = \x bs. [], diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy index c22f2de9f..092caef40 100644 --- a/tools/c-parser/umm_heap/CTypesBase.thy +++ b/tools/c-parser/umm_heap/CTypesBase.thy @@ -127,12 +127,12 @@ end subsection "Raw heap" -text {* A raw map from addresses to bytes *} +text \A raw map from addresses to bytes\ type_synonym heap_mem = "addr \ byte" -text {* For heap h, pointer p and nat n, (heap_list h n p) returns the list - of bytes in the heap taken from addresses {p..+n} *} +text \For heap h, pointer p and nat n, (heap_list h n p) returns the list + of bytes in the heap taken from addresses {p..+n}\ primrec heap_list :: "heap_mem \ nat \ addr \ byte list" @@ -143,9 +143,9 @@ where section "Intervals" -text {* +text \ For word a and nat b, {a..+b} is the set of words x, - with unat (x - a) < b. *} + with unat (x - a) < b.\ definition intvl :: "'a::len word \ nat \ 'a::len word set" where diff --git a/tools/c-parser/umm_heap/CTypesDefs.thy b/tools/c-parser/umm_heap/CTypesDefs.thy index a8b21330e..24c5c66b1 100644 --- a/tools/c-parser/umm_heap/CTypesDefs.thy +++ b/tools/c-parser/umm_heap/CTypesDefs.thy @@ -25,11 +25,11 @@ type_synonym qualified_field_name = "field_name list" type_synonym typ_name = string -text {* A typ_desc wraps a typ_struct with a typ name. +text \A typ_desc wraps a typ_struct with a typ name. A typ_struct is either a Scalar, with size, alignment and either a field accessor/updator pair (for typ_info) or a 'normalisor' (for typ_uinfo), or an Aggregate, with a list of typ_desc, - field name pairs.*} + field name pairs.\ datatype 'a typ_desc = TypDesc "'a typ_struct" typ_name @@ -94,8 +94,8 @@ definition fu_commutes :: "('b \ 'a \ 'a) \ "fu_commutes f g \ \v bs bs'. f bs (g bs' v) = g bs' (f bs v)" -text {* size_td returns the sum of the sizes of all Scalar fields - comprising a typ_desc i.e. the overall size of the type *} +text \size_td returns the sum of the sizes of all Scalar fields + comprising a typ_desc i.e. the overall size of the type\ (* Could express this and many other typ_desc primrecs as tree fold/map combos, but the intuition this way is clearer for anything non-trivial *) @@ -116,8 +116,8 @@ where | tz5: "size_td_pair (DTPair t n) = size_td t" -text {* access_ti overlays the byte-wise representation of an object - on a given byte list, given the typ_info (i.e. the layout) *} +text \access_ti overlays the byte-wise representation of an object + on a given byte list, given the typ_info (i.e. the layout)\ primrec access_ti :: "'a typ_info \ ('a \ byte list \ byte list)" and @@ -145,8 +145,8 @@ text \@{text access_ti\<^sub>0} overlays the representation of an object o definition access_ti\<^sub>0 :: "'a typ_info \ ('a \ byte list)" where "access_ti\<^sub>0 t \ \v. access_ti t v (replicate (size_td t) 0)" -text {* update_ti updates an object, given a list of bytes (the - representation of the new value), and the typ_info *} +text \update_ti updates an object, given a list of bytes (the + representation of the new value), and the typ_info\ primrec update_ti :: "'a typ_info \ (byte list \ 'a \ 'a)" and @@ -167,8 +167,8 @@ where | fu5: "update_ti_pair (DTPair t nm) = update_ti t" -text {* update_ti_t updates an object only if the length of the - supplied representation equals the object size *} +text \update_ti_t updates an object only if the length of the + supplied representation equals the object size\ definition update_ti_t :: "'a typ_info \ (byte list \ 'a \ 'a)" where "update_ti_t t \ \bs. if length bs = size_td t then @@ -187,8 +187,8 @@ definition update_ti_pair_t :: "'a typ_info_pair \ (byte list \field_desc generates the access/update pair for a field, + given the field's type_desc\ definition field_desc :: "'a typ_info \ 'a field_desc" where "field_desc t \ \ field_access = access_ti t, diff --git a/tools/c-parser/umm_heap/CompoundCTypesEx.thy b/tools/c-parser/umm_heap/CompoundCTypesEx.thy index 841161958..b5f3f9c3a 100644 --- a/tools/c-parser/umm_heap/CompoundCTypesEx.thy +++ b/tools/c-parser/umm_heap/CompoundCTypesEx.thy @@ -46,7 +46,7 @@ lemma aggregate_x_struct_ex_tag [simp]: lemma "upd_local (x_example_update \ (\x _. x))" apply(auto simp: upd_local_def ) -apply(tactic {* Record.split_tac @{context} 1 *} ) +apply(tactic \Record.split_tac @{context} 1\ ) apply simp done diff --git a/tools/c-parser/umm_heap/MapExtra.thy b/tools/c-parser/umm_heap/MapExtra.thy index a5c4075c7..a867ce0d6 100644 --- a/tools/c-parser/umm_heap/MapExtra.thy +++ b/tools/c-parser/umm_heap/MapExtra.thy @@ -8,31 +8,31 @@ * @TAG(NICTA_BSD) *) -chapter {* More properties of maps plus map disjuction. *} +chapter \More properties of maps plus map disjuction.\ theory MapExtra imports Main begin -text {* +text \ BEWARE: we are not interested in using the @{term "dom x \ dom y = {}"} rules from Map for our separation logic proofs. As such, we overwrite the Map rules where that form of disjointness is in the assumption conflicts - with a name we want to use with @{text "\"}. *} + with a name we want to use with @{text "\"}.\ -text {* +text \ A note on naming: Anything not involving heap disjuction can potentially be incorporated directly into Map.thy, thus uses @{text "m"}. Anything involving heap disjunction is not really mergeable with Map, is destined for use in separation logic, and hence uses @{text "h"} -*} +\ -text {*--------------------------------------- *} -text {* Things that should go into Option Type *} -text {*--------------------------------------- *} +text \---------------------------------------\ +text \Things that should go into Option Type\ +text \---------------------------------------\ -text {* Misc option lemmas *} +text \Misc option lemmas\ lemma None_not_eq: "(None \ x) = (\y. x = Some y)" by (cases x) auto @@ -40,24 +40,24 @@ lemma None_com: "(None = x) = (x = None)" by fast lemma Some_com: "(Some y = x) = (x = Some y)" by fast -text {*--------------------------------------- *} -text {* Things that should go into Map.thy *} -text {*--------------------------------------- *} +text \---------------------------------------\ +text \Things that should go into Map.thy\ +text \---------------------------------------\ -text {* Map intersection: set of all keys for which the maps agree. *} +text \Map intersection: set of all keys for which the maps agree.\ definition map_inter :: "('a \ 'b) \ ('a \ 'b) \ 'a set" (infixl "\\<^sub>m" 70) where "m\<^sub>1 \\<^sub>m m\<^sub>2 \ {x \ dom m\<^sub>1. m\<^sub>1 x = m\<^sub>2 x}" -text {* Map restriction via domain subtraction *} +text \Map restriction via domain subtraction\ definition sub_restrict_map :: "('a \ 'b) => 'a set => ('a \ 'b)" (infixl "`-" 110) where "m `- S \ (\x. if x \ S then None else m x)" -subsection {* Properties of maps not related to restriction *} +subsection \Properties of maps not related to restriction\ lemma empty_forall_equiv: "(m = Map.empty) = (\x. m x = None)" by (rule fun_eq_iff) @@ -116,7 +116,7 @@ lemma map_le_same_dom_eq: "\ m\<^sub>0 \\<^sub>m m\<^sub>1 ; dom m\<^sub>0 = dom m\<^sub>1 \ \ m\<^sub>0 = m\<^sub>1" by (simp add: map_le_antisym map_le_def) -subsection {* Properties of map restriction *} +subsection \Properties of map restriction\ lemma restrict_map_cancel: "(m |` S = m |` T) = (dom m \ S = dom m \ T)" @@ -218,13 +218,13 @@ lemma prod_restrict_map_add: by (auto simp: map_add_def restrict_map_def split: option.splits) -text {*--------------------------------------- *} -text {* Things that should NOT go into Map.thy *} -text {*--------------------------------------- *} +text \---------------------------------------\ +text \Things that should NOT go into Map.thy\ +text \---------------------------------------\ -section {* Definitions *} +section \Definitions\ -text {* Map disjuction *} +text \Map disjuction\ definition map_disj :: "('a \ 'b) \ ('a \ 'b) \ bool" (infix "\" 51) where @@ -232,7 +232,7 @@ definition declare None_not_eq [simp] -text {* Heap monotonicity and the frame property *} +text \Heap monotonicity and the frame property\ definition heap_mono :: "(('a \ 'b) \ 'c option) \ bool" where @@ -257,7 +257,7 @@ lemma heap_frameE: unfolding heap_frame_def by fastforce -section {* Properties of @{term "sub_restrict_map"} *} +section \Properties of @{term "sub_restrict_map"}\ lemma restrict_map_sub_disj: "h |` S \ h `- S" by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def @@ -268,7 +268,7 @@ lemma restrict_map_sub_add: "h |` S ++ h `- S = h" split: option.splits if_split) -section {* Properties of map disjunction *} +section \Properties of map disjunction\ lemma map_disj_empty_right [simp]: "h \ Map.empty" @@ -291,7 +291,7 @@ lemma map_disjI: by (simp add: map_disj_def) -subsection {* Map associativity-commutativity based on map disjuction *} +subsection \Map associativity-commutativity based on map disjuction\ lemma map_add_com: "h\<^sub>0 \ h\<^sub>1 \ h\<^sub>0 ++ h\<^sub>1 = h\<^sub>1 ++ h\<^sub>0" @@ -309,27 +309,27 @@ lemma map_add_disj': "(h\<^sub>1 ++ h\<^sub>2) \ h\<^sub>0 = (h\<^sub>1 \ h\<^sub>0 \ h\<^sub>2 \ h\<^sub>0)" by (simp add: map_disj_def, fast) -text {* +text \ We redefine @{term "map_add"} associativity to bind to the right, which seems to be the more common case. Note that when a theory includes Map again, @{text "map_add_assoc"} will return to the simpset and will cause infinite loops if its symmetric counterpart is added (e.g. via @{text "map_ac_simps"}) - *} +\ declare map_add_assoc [simp del] -text {* +text \ Since the associativity-commutativity of @{term "map_add"} relies on map disjunction, we include some basic rules into the ac set. - *} +\ lemmas map_ac_simps = map_add_assoc[symmetric] map_add_com map_disj_com map_add_left_commute map_add_disj map_add_disj' -subsection {* Basic properties *} +subsection \Basic properties\ lemma map_disj_None_right: "\ h\<^sub>0 \ h\<^sub>1 ; x \ dom h\<^sub>0 \ \ h\<^sub>1 x = None" @@ -352,7 +352,7 @@ lemma map_disj_common: by (frule (1) map_disj_None_left', simp) -subsection {* Map disjunction and addition *} +subsection \Map disjunction and addition\ lemma map_add_eval_left: "\ x \ dom h ; h \ h' \ \ (h ++ h') x = h x" @@ -444,7 +444,7 @@ lemma map_add_lr_disj: (auto split: option.splits) -subsection {* Map disjunction and updates *} +subsection \Map disjunction and updates\ lemma map_disj_update_left [simp]: "p \ dom h\<^sub>1 \ h\<^sub>0 \ h\<^sub>1(p \ v) = h\<^sub>0 \ h\<^sub>1" @@ -470,7 +470,7 @@ lemma map_add3_update: by (auto simp: map_add_update_left[symmetric] map_ac_simps) -subsection {* Map disjunction and @{term "map_le"} *} +subsection \Map disjunction and @{term "map_le"}\ lemma map_le_override [simp]: "\ h \ h' \ \ h \\<^sub>m h ++ h'" @@ -527,7 +527,7 @@ lemma map_le_conv2: by (case_tac "h\<^sub>0'=h\<^sub>0", insert map_le_conv, auto intro: exI[where x=Map.empty]) -subsection {* Map disjunction and restriction *} +subsection \Map disjunction and restriction\ lemma map_disj_comp [simp]: "h\<^sub>0 \ h\<^sub>1 |` (UNIV - dom h\<^sub>0)" diff --git a/tools/c-parser/umm_heap/SepCode.thy b/tools/c-parser/umm_heap/SepCode.thy index d2cdad18d..b4de85af9 100644 --- a/tools/c-parser/umm_heap/SepCode.thy +++ b/tools/c-parser/umm_heap/SepCode.thy @@ -65,7 +65,7 @@ definition where "sep_cut x y \ sep_cut' x (unat y)" -text {* ---- *} +text \----\ (* FIXME MOVE *) lemma heap_list_h_eq: diff --git a/tools/c-parser/umm_heap/SepFrame.thy b/tools/c-parser/umm_heap/SepFrame.thy index fd57da5fc..cfd608005 100644 --- a/tools/c-parser/umm_heap/SepFrame.thy +++ b/tools/c-parser/umm_heap/SepFrame.thy @@ -168,7 +168,7 @@ where "x \ intra_deps C \ x \ proc_deps C \" | "\ x \ proc_deps C \; \ x = Some D; y \ intra_deps D \ \ y \ proc_deps C \" -text {* ---- *} +text \----\ lemma point_eq_mod_refl [simp]: "point_eq_mod f f X" diff --git a/tools/c-parser/umm_heap/SepInv.thy b/tools/c-parser/umm_heap/SepInv.thy index 10dacf99e..702e7fd82 100644 --- a/tools/c-parser/umm_heap/SepInv.thy +++ b/tools/c-parser/umm_heap/SepInv.thy @@ -21,11 +21,11 @@ definition inv_footprint :: "'a::c_type ptr \ heap_assert" where "inv_footprint p \ \s. dom s = {(x,y). x \ {ptr_val p..+size_of TYPE('a)}} - s_footprint p" -text {* +text \ Like in Separation.thy, these arrows are defined using bsub and esub but have an \emph{input} syntax abbreviation with just sub. See original comment there for justification. -*} +\ definition sep_map_inv :: "'a::c_type ptr \ 'a ptr_guard \ 'a \ heap_assert" @@ -68,7 +68,7 @@ definition where "g \\<^sub>s\<^sup>i p \ g \\<^sub>s p \\<^sup>* inv_footprint p" -text {* ---- *} +text \----\ lemma sep_map'_g: "(p \\<^sup>i\<^sub>g v) s \ g p" diff --git a/tools/c-parser/umm_heap/SepTactic.thy b/tools/c-parser/umm_heap/SepTactic.thy index 411a1e32f..8976e5dab 100644 --- a/tools/c-parser/umm_heap/SepTactic.thy +++ b/tools/c-parser/umm_heap/SepTactic.thy @@ -65,7 +65,7 @@ lemma sep_point_otherD: "sep_points P s \ True" by (rule TrueI) -ML {* +ML \ val sep_point_ds = [@{thm sep_point_mapD}, @{thm sep_point_map_excD}] @@ -85,7 +85,7 @@ fun sep_point_tacs ds ctxt = [ ] fun sep_point_tac ds ctxt = EVERY (sep_point_tacs ds ctxt) -*} +\ method_setup sep_point_tac = "Attrib.thms >> (fn thms => Method.SIMPLE_METHOD o sep_point_tac thms)" @@ -97,10 +97,10 @@ lemma "(P \\<^sup>* p \\<^sub>g v \\<^sup>* Q) s \ fun sep_exists_tac ctxt = full_simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm "sep_conj_exists1"}, @{thm "sep_conj_exists2"}]) -*} +\ method_setup sep_exists_tac = "Scan.succeed (Method.SIMPLE_METHOD' o sep_exists_tac)" @@ -153,7 +153,7 @@ lemma sep_mark2_left2: "(P \\<^sup>* sep_mark2 Q) = (sep_mark2 Q \\<^sup>* P)" by (rule sep_conj_com) -ML {* +ML \ (* Replace all occurrences of an underscore that does not have an alphanumeric on either side of it *) @@ -185,9 +185,9 @@ rusc "(_ +\<^sub>p _) \ _"; rusc "_ \\<^sub>_ _"; rusc "_"; rusc "_ O_o _" -*} +\ -ML{* +ML\ fun sep_select_tacs s ctxt = let val (str, vars) = rusc s @@ -214,10 +214,10 @@ fun sep_select_tac s ctxt = SELECT_GOAL (EVERY (sep_select_tacs s ctxt)) fun lift_parser p (ctxt,ts) = let val (r, ts') = p ts in (r, (ctxt,ts')) end -*} +\ method_setup sep_select_tac = - {* lift_parser Args.name >> (fn s => Method.SIMPLE_METHOD' o sep_select_tac s) *} + \lift_parser Args.name >> (fn s => Method.SIMPLE_METHOD' o sep_select_tac s)\ "takes a target conjunct in the goal and reorders it to the front" lemma @@ -259,7 +259,7 @@ lemma ptr_retyp_sep_cut'_wp_hrs: by (case_tac s) (simp add: hrs_htd_update_def, erule (1) ptr_retyp_sep_cut'_wp) -ML {* +ML \ fun destruct bs (Bound n) = Free (List.nth (bs,n)) | destruct bs (Abs (s,ty,t)) = destruct ((s,ty)::bs) t @@ -330,7 +330,7 @@ end fun sep_wp_tac ctxt = (REPEAT (sep_wp_step_tac ctxt false)) THEN sep_wp_step_tac ctxt true -*} +\ method_setup sep_wp_tac = "Scan.succeed (Method.SIMPLE_METHOD o sep_wp_tac)" diff --git a/tools/c-parser/umm_heap/Separation.thy b/tools/c-parser/umm_heap/Separation.thy index fee3a8c29..8cf8fa42b 100644 --- a/tools/c-parser/umm_heap/Separation.thy +++ b/tools/c-parser/umm_heap/Separation.thy @@ -46,13 +46,13 @@ definition where "singleton p v h d \ lift_state (heap_update p v h,d) |` s_footprint p" -text {* +text \ Like in Separation.thy, these arrows are defined using bsub and esub but have an \emph{input} syntax abbreviation with just sub. Why? Because if sub is the only way, people write things like @{text "p \\<^sup>i\<^sub>(f x y) v"} instead of @{text "p \\<^sup>i\<^bsub>(f x y)\<^esub> v"}. We preserve the sub syntax though, because esub and bsub are a pain to type. -*} +\ definition sep_map :: "'a::c_type ptr \ 'a ptr_guard \ 'a \ heap_assert" @@ -91,7 +91,7 @@ syntax "_sep_assert" :: "bool \ heap_state \ bool" ("'(_')\<^bsup>sep\<^esup>" [0] 100) -text {* ---- *} +text \----\ lemma sep_empD: "\ s \ s = Map.empty" diff --git a/tools/c-parser/umm_heap/TypHeap.thy b/tools/c-parser/umm_heap/TypHeap.thy index 0e160ca0b..b2af18d1b 100644 --- a/tools/c-parser/umm_heap/TypHeap.thy +++ b/tools/c-parser/umm_heap/TypHeap.thy @@ -299,7 +299,7 @@ definition where "s \\<^sub>\ t \ typ_uinfo_t s \\<^sub>t typ_uinfo_t t" -text {* ---- *} +text \----\ lemma wf_heap_val_SIndexVal_STyp_simp [simp]: "wf_heap_val s \ s (x,SIndexVal) \ Some (STyp t)"