diff --git a/thys/BTree/Array_SBlit.thy b/thys/BTree/Array_SBlit.thy --- a/thys/BTree/Array_SBlit.thy +++ b/thys/BTree/Array_SBlit.thy @@ -1,305 +1,305 @@ theory Array_SBlit imports "Separation_Logic_Imperative_HOL.Array_Blit" begin (* Resolves TODO by Peter Lammich *) (* OCaml handles the case of len=0 correctly (i.e. as specified by the Hoare Triple in Array_Blit not generating an exception if si+len \ array length and such) *) code_printing code_module "array_blit" \ (OCaml) \ let array_blit src si dst di len = ( if src=dst then raise (Invalid_argument "array_blit: Same arrays") else Array.blit src (Z.to_int si) dst (Z.to_int di) (Z.to_int len) );; \ code_printing constant blit' \ (OCaml) "(fun () -> /array'_blit _ _ _ _ _)" export_code blit checking OCaml section "Same array Blit" text "The standard framework already provides a function to copy array elements." term blit thm blit_rule thm blit.simps (* Same array BLIT *) definition "sblit a s d l \ blit a s a d l" text "When copying values within arrays, blit only works for moving elements to the left." lemma sblit_rule[sep_heap_rules]: assumes LEN: "si+len \ length lsrc" and DST_SM: "di \ si" shows "< src \\<^sub>a lsrc > sblit src si di len <\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc) >" unfolding sblit_def using LEN DST_SM proof (induction len arbitrary: lsrc si di) case 0 thus ?case by sep_auto next case (Suc len) note [sep_heap_rules] = Suc.IH have [simp]: "\x. lsrc ! si # take len (drop (Suc si) lsrc) @ x = take (Suc len) (drop si lsrc) @ x" apply simp by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc less_Suc_eq_le add.commute not_less_eq take_Suc_Cons Nat.trans_le_add2) from Suc.prems show ?case by (sep_auto simp: take_update_last drop_upd_irrelevant) qed subsection "A reverse blit" text "The function rblit may be used to copy elements a defined offset to the right" (* Right BLIT or Reverse BLIT *) primrec rblit :: "_ array \ nat \ _ array \ nat \ nat \ unit Heap" where "rblit _ _ _ _ 0 = return ()" | "rblit src si dst di (Suc l) = do { x \ Array.nth src (si+l); Array.upd (di+l) x dst; rblit src si dst di l }" text "For separated arrays it is equivalent to normal blit. The proof follows similarly to the corresponding proof for blit." lemma rblit_rule[sep_heap_rules]: assumes LEN: "si+len \ length lsrc" "di+len \ length ldst" shows "< src \\<^sub>a lsrc * dst \\<^sub>a ldst > rblit src si dst di len <\_. src \\<^sub>a lsrc * dst \\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst) >" using LEN proof (induction len arbitrary: ldst) case 0 thus ?case by sep_auto next case (Suc len) note [sep_heap_rules] = Suc.IH have [simp]: "drop (di + len) (ldst[di + len := lsrc ! (si + len)]) = lsrc ! (si + len) # drop (Suc (di + len)) ldst" by (metis Cons_nth_drop_Suc Suc.prems(2) Suc_le_eq add_Suc_right drop_upd_irrelevant length_list_update lessI nth_list_update_eq) have "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)" proof - have "len < length (drop si lsrc)" using Suc.prems(1) by force then show "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)" by (metis (no_types) Suc.prems(1) add_leD1 nth_drop take_Suc_conv_app_nth) qed then have [simp]: "\x. take len (drop si lsrc) @ lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x" by simp from Suc.prems show ?case by (sep_auto simp: take_update_last drop_upd_irrelevant) qed definition "srblit a s d l \ rblit a s a d l" text "However, within arrays we can now copy to the right." lemma srblit_rule[sep_heap_rules]: assumes LEN: "di+len \ length lsrc" and DST_GR: "di \ si" shows "< src \\<^sub>a lsrc > srblit src si di len <\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc) >" unfolding srblit_def using LEN DST_GR proof (induction len arbitrary: lsrc si di) case 0 thus ?case by sep_auto next case (Suc len) note [sep_heap_rules] = Suc.IH have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)])) = take len (drop si lsrc)" by (metis Suc.prems(2) ab_semigroup_add_class.add.commute add_le_cancel_right take_drop take_update_cancel) have [simp]: "drop (di + len) (lsrc[di + len := lsrc ! (si + len)]) = lsrc ! (si+len) # drop (Suc di + len) lsrc" by (metis Suc.prems(1) add_Suc_right add_Suc_shift add_less_cancel_left append_take_drop_id le_imp_less_Suc le_refl plus_1_eq_Suc same_append_eq take_update_cancel upd_conv_take_nth_drop) have "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)" proof - have "len < length lsrc - si" using Suc.prems(1) Suc.prems(2) by linarith then show ?thesis by (metis (no_types) Suc.prems(1) Suc.prems(2) add_leD1 le_add_diff_inverse length_drop nth_drop take_Suc_conv_app_nth) qed then have [simp]: "\x. take len (drop si lsrc) @ lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x" by simp from Suc.prems show ?case by (sep_auto simp: take_update_last drop_upd_irrelevant) qed subsection "Modeling target language blit" text "For convenience, a function that is oblivious to the direction of the shift is defined." definition "safe_sblit a s d l \ if s > d then sblit a s d l else srblit a s d l " text "We obtain a heap rule similar to the one of blit, but for copying within one array." lemma safe_sblit_rule[sep_heap_rules]: assumes LEN: "len > 0 \ di+len \ length lsrc \ si+len \ length lsrc" shows "< src \\<^sub>a lsrc > safe_sblit src si di len <\_. src \\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc) >" unfolding safe_sblit_def using LEN apply(cases len) apply(sep_auto simp add: sblit_def srblit_def)[] apply sep_auto done (* Compare this to blit_rule *) thm blit_rule thm safe_sblit_rule subsection "Code Generator Setup" text "Note that the requirement for correctness is even weaker here than in SML/OCaml. In particular, if the length of the slice to copy is equal to 0, we will never throw an exception. We therefore manually handle this case, where nothing happens at all." code_printing code_module "array_sblit" \ (SML) \ fun array_sblit src si di len = ( if len > 0 then ArraySlice.copy { di = IntInf.toInt di, src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)), dst = src} else () ) \ code_printing code_module "array_sblit" \ (OCaml) \ let array_sblit src si di len = ( if len > Z.zero then (Array.blit src (Z.to_int si) src (Z.to_int di) (Z.to_int len)) else () );; \ definition safe_sblit' where [code del]: "safe_sblit' src si di len = safe_sblit src (nat_of_integer si) (nat_of_integer di) (nat_of_integer len)" lemma [code]: "safe_sblit src si di len = safe_sblit' src (integer_of_nat si) (integer_of_nat di) (integer_of_nat len)" by (simp add: safe_sblit'_def) (* TODO: Export to other languages: Haskell *) code_printing constant safe_sblit' \ (SML) "(fn/ ()/ => /array'_sblit _ _ _ _)" and (Scala) "{ ('_: Unit)/=>/ def safescopy(src: Array['_], srci: Int, dsti: Int, len: Int) = { - if (len > 0) - System.arraycopy(src, srci, src, dsti, len) - else - () + len > 0 match { + case true => System.arraycopy(src, srci, src, dsti, len) + case false => () + } } safescopy(_.array,_.toInt,_.toInt,_.toInt) }" code_printing constant safe_sblit' \ (OCaml) "(fun () -> /array'_sblit _ _ _ _)" export_code safe_sblit checking SML Scala OCaml subsection "Derived operations" definition array_shr where "array_shr a i k \ do { l \ Array.len a; safe_sblit a i (i+k) (l-(i+k)) }" find_theorems "Array.len" lemma array_shr_rule[sep_heap_rules]: "< src \\<^sub>a lsrc > array_shr src i k <\_. src \\<^sub>a (take (i+k) lsrc @ take (length lsrc - (i+k)) (drop i lsrc)) >" unfolding array_shr_def by sep_auto lemma array_shr_rule_alt: "< src \\<^sub>a lsrc > array_shr src i k <\_. src \\<^sub>a (take (length lsrc) (take (i+k) lsrc @ (drop i lsrc))) >" by (sep_auto simp add: min_def) definition array_shl where "array_shl a i k \ do { l \ Array.len a; safe_sblit a i (i-k) (l-i) } " lemma array_shl_rule[sep_heap_rules]: " < src \\<^sub>a lsrc > array_shl src i k <\_. src \\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (i - k + (length lsrc - i)) lsrc) >" unfolding array_shl_def by sep_auto lemma array_shl_rule_alt: " \i \ length lsrc; k \ i\ \ < src \\<^sub>a lsrc > array_shl src i k <\_. src \\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (length lsrc - k) lsrc) >" by sep_auto end \ No newline at end of file diff --git a/thys/Collections/Lib/Diff_Array.thy b/thys/Collections/Lib/Diff_Array.thy --- a/thys/Collections/Lib/Diff_Array.thy +++ b/thys/Collections/Lib/Diff_Array.thy @@ -1,1097 +1,1098 @@ section \Arrays with in-place updates\ theory Diff_Array imports Assoc_List Automatic_Refinement.Parametricity "HOL-Library.Code_Target_Numeral" begin datatype 'a array = Array "'a list" subsection \primitive operations\ definition new_array :: "'a \ nat \ 'a array" where "new_array a n = Array (replicate n a)" primrec array_length :: "'a array \ nat" where "array_length (Array a) = length a" primrec array_get :: "'a array \ nat \ 'a" where "array_get (Array a) n = a ! n" primrec array_set :: "'a array \ nat \ 'a \ 'a array" where "array_set (Array A) n a = Array (A[n := a])" definition array_of_list :: "'a list \ 'a array" where "array_of_list = Array" \ \Grows array by @{text inc} elements initialized to value @{text x}.\ primrec array_grow :: "'a array \ nat \ 'a \ 'a array" where "array_grow (Array A) inc x = Array (A @ replicate inc x)" \ \Shrinks array to new size @{text sz}. Undefined if @{text "sz > array_length"}\ primrec array_shrink :: "'a array \ nat \ 'a array" where "array_shrink (Array A) sz = ( if (sz > length A) then undefined else Array (take sz A) )" subsection \Derived operations\ text \The following operations are total versions of \array_get\ and \array_set\, which return a default value in case the index is out of bounds. They can be efficiently implemented in the target language by catching exceptions. \ definition "array_get_oo x a i \ if i if i 'a list" where "list_of_array (Array a) = a" primrec assoc_list_of_array :: "'a array \ (nat \ 'a) list" where "assoc_list_of_array (Array a) = zip [0.. nat \ (nat \ 'a) list" where [simp del]: "assoc_list_of_array_code a n = (if array_length a \ n then [] else (n, array_get a n) # assoc_list_of_array_code a (n + 1))" by pat_completeness auto termination assoc_list_of_array_code by(relation "measure (\p. (array_length (fst p) - snd p))") auto definition array_map :: "(nat \ 'a \ 'b) \ 'a array \ 'b array" where "array_map f a = array_of_list (map (\(i, v). f i v) (assoc_list_of_array a))" definition array_foldr :: "(nat \ 'a \ 'b \ 'b) \ 'a array \ 'b \ 'b" where "array_foldr f a b = foldr (\(k, v). f k v) (assoc_list_of_array a) b" definition array_foldl :: "(nat \ 'b \ 'a \ 'b) \ 'b \ 'a array \ 'b" where "array_foldl f b a = foldl (\b (k, v). f k b v) b (assoc_list_of_array a)" subsection \Lemmas\ lemma array_length_new_array [simp]: "array_length (new_array a n) = n" by(simp add: new_array_def) lemma array_length_array_set [simp]: "array_length (array_set a i e) = array_length a" by(cases a) simp lemma array_get_new_array [simp]: "i < n \ array_get (new_array a n) i = a" by(simp add: new_array_def) lemma array_get_array_set_same [simp]: "n < array_length A \ array_get (array_set A n a) n = a" by(cases A) simp lemma array_get_array_set_other: "n \ n' \ array_get (array_set A n a) n' = array_get A n'" by(cases A) simp lemma list_of_array_grow [simp]: "list_of_array (array_grow a inc x) = list_of_array a @ replicate inc x" by (cases a) (simp) lemma array_grow_length [simp]: "array_length (array_grow a inc x) = array_length a + inc" by (cases a)(simp add: array_of_list_def) lemma array_grow_get [simp]: "i < array_length a \ array_get (array_grow a inc x) i = array_get a i" "\ i \ array_length a; i < array_length a + inc\ \ array_get (array_grow a inc x) i = x" by (cases a, simp add: nth_append)+ lemma list_of_array_shrink [simp]: "\ s \ array_length a\ \ list_of_array (array_shrink a s) = take s (list_of_array a)" by (cases a) simp lemma array_shrink_get [simp]: "\ i < s; s \ array_length a \ \ array_get (array_shrink a s) i = array_get a i" by (cases a) (simp) lemma list_of_array_id [simp]: "list_of_array (array_of_list l) = l" by (cases l)(simp_all add: array_of_list_def) lemma map_of_assoc_list_of_array: "map_of (assoc_list_of_array a) k = (if k < array_length a then Some (array_get a k) else None)" by(cases a, cases "k < array_length a")(force simp add: set_zip)+ lemma length_assoc_list_of_array [simp]: "length (assoc_list_of_array a) = array_length a" by(cases a) simp lemma distinct_assoc_list_of_array: "distinct (map fst (assoc_list_of_array a))" by(cases a)(auto) lemma array_length_array_map [simp]: "array_length (array_map f a) = array_length a" by(simp add: array_map_def array_of_list_def) lemma array_get_array_map [simp]: "i < array_length a \ array_get (array_map f a) i = f i (array_get a i)" by(cases a)(simp add: array_map_def map_ran_conv_map array_of_list_def) lemma array_foldr_foldr: "array_foldr (\n. f) (Array a) b = foldr f a b" by(simp add: array_foldr_def foldr_snd_zip) lemma assoc_list_of_array_code_induct: assumes IH: "\n. (n < array_length a \ P (Suc n)) \ P n" shows "P n" proof - have "a = a \ P n" by(rule assoc_list_of_array_code.induct[where P="\a' n. a = a' \ P n"])(auto intro: IH) thus ?thesis by simp qed lemma assoc_list_of_array_code [code]: "assoc_list_of_array a = assoc_list_of_array_code a 0" proof(cases a) case (Array A) { fix n have "zip [n..n < length A\ have [simp]: "a = A ! n" by(subst append_take_drop_id[symmetric, where n=n])(simp add: nth_append min_def) moreover from A have "drop (Suc n) A = A'" by(induct A arbitrary: n)(simp_all add: drop_Cons split: nat.split_asm) ultimately show ?thesis by(subst upt_rec)(simp add: assoc_list_of_array_code.simps) qed qed } note this[of 0] with Array show ?thesis by simp qed lemma list_of_array_code [code]: "list_of_array a = array_foldr (\n. Cons) a []" by(cases a)(simp add: array_foldr_foldr foldr_Cons) lemma array_foldr_cong [fundef_cong]: "\ a = a'; b = b'; \i b. i < array_length a \ f i (array_get a i) b = g i (array_get a i) b \ \ array_foldr f a b = array_foldr g a' b'" by(cases a)(auto simp add: array_foldr_def set_zip intro!: foldr_cong) lemma array_foldl_foldl: "array_foldl (\n. f) b (Array a) = foldl f b a" by(simp add: array_foldl_def foldl_snd_zip) lemma array_map_conv_foldl_array_set: assumes len: "array_length A = array_length a" shows "array_map f a = foldl (\A (k, v). array_set A k (f k v)) A (assoc_list_of_array a)" proof(cases a) case (Array xs) obtain ys where [simp]: "A = Array ys" by(cases A) with Array len have "length xs \ length ys" by simp hence "foldr (\x y. array_set y (fst x) (f (fst x) (snd x))) (rev (zip [0..x. f (fst x) (snd x)) (zip [0..length (xs @ [x]) \ length ys\ have "length xs \ length ys" by simp hence "foldr (\x y. array_set y (fst x) (f (fst x) (snd x))) (rev (zip [0..x. f (fst x) (snd x)) (zip [0..length (xs @ [x]) \ length ys\ obtain y ys' where ys: "drop (length xs) ys = y # ys'" by(cases "drop (length xs) ys") auto moreover hence "drop (Suc (length xs)) ys = ys'" by(auto dest: drop_eq_ConsD) ultimately show ?case by(simp add: list_update_append) qed thus ?thesis using Array len by(simp add: array_map_def split_beta array_of_list_def foldl_conv_foldr) qed subsection \Lemmas about empty arrays\ lemma array_length_eq_0 [simp]: "array_length a = 0 \ a = Array []" by(cases a) simp lemma new_array_0 [simp]: "new_array v 0 = Array []" by(simp add: new_array_def) lemma array_of_list_Nil [simp]: "array_of_list [] = Array []" by(simp add: array_of_list_def) lemma array_map_Nil [simp]: "array_map f (Array []) = Array []" by(simp add: array_map_def) lemma array_foldl_Nil [simp]: "array_foldl f b (Array []) = b" by(simp add: array_foldl_def) lemma array_foldr_Nil [simp]: "array_foldr f (Array []) b = b" by(simp add: array_foldr_def) lemma prod_foldl_conv: "(foldl f a xs, foldl g b xs) = foldl (\(a, b) x. (f a x, g b x)) (a, b) xs" by(induct xs arbitrary: a b) simp_all lemma prod_array_foldl_conv: "(array_foldl f b a, array_foldl g c a) = array_foldl (\h (b, c) v. (f h b v, g h c v)) (b, c) a" by(cases a)(simp add: array_foldl_def foldl_map prod_foldl_conv split_def) lemma array_foldl_array_foldr_comm: "comp_fun_commute (\(h, v) b. f h b v) \ array_foldl f b a = array_foldr (\h v b. f h b v) a b" by(cases a)(simp add: array_foldl_def array_foldr_def split_def comp_fun_commute.foldr_conv_foldl) lemma array_map_conv_array_foldl: "array_map f a = array_foldl (\h a v. array_set a h (f h v)) a a" proof(cases a) case (Array xs) define a where "a = xs" hence "length xs \ length a" by simp hence "foldl (\a (k, v). array_set a k (f k v)) (Array a) (zip [0..(k, v). f k v) (zip [0..a (k, v). array_set a k (f k v)) (Array a) (zip [0..a (k, v). array_set a k (f k v)) (Array a) (zip [0..length (xs @ [x]) \ length a\ have "length xs \ length a" by simp hence "foldl (\a (k, v). array_set a k (f k v)) (Array a) (zip [0..(k, v). f k v) (zip [0..(k, v). f k v) (zip [0..(k, v). f k v) (zip [0..length (xs @ [x]) \ length a\ have "(drop (length xs) a)[0 := f (length xs) x] = f (length xs) x # drop (Suc (length xs)) a" by(simp add: upd_conv_take_nth_drop) also have "map (\(k, v). f k v) (zip [0..(k, v). f k v) (zip [0.. = map (\(k, v). f k v) (zip [0..b (k, v). f k b v) b (zip [0..Parametricity lemmas\ lemma rec_array_is_case[simp]: "rec_array = case_array" apply (intro ext) apply (auto split: array.split) done definition array_rel_def_internal: "array_rel R \ {(Array xs, Array ys)|xs ys. (xs,ys) \ \R\list_rel}" lemma array_rel_def: "\R\array_rel \ {(Array xs, Array ys)|xs ys. (xs,ys) \ \R\list_rel}" unfolding array_rel_def_internal relAPP_def . lemma array_relD: "(Array l, Array l') \ \R\array_rel \ (l,l') \ \R\list_rel" by (simp add: array_rel_def) lemma array_rel_alt: "\R\array_rel = { (Array l, l) | l. True } O \R\list_rel O {(l,Array l) | l. True}" by (auto simp: array_rel_def) lemma array_rel_sv[relator_props]: shows "single_valued R \ single_valued (\R\array_rel)" unfolding array_rel_alt apply (intro relator_props ) apply (auto intro: single_valuedI) done lemma param_Array[param]: "(Array,Array) \ \R\ list_rel \ \R\ array_rel" apply (intro fun_relI) apply (simp add: array_rel_def) done lemma param_rec_array[param]: "(rec_array,rec_array) \ (\Ra\list_rel \ Rb) \ \Ra\array_rel \ Rb" apply (intro fun_relI) apply (rename_tac f f' a a', case_tac a, case_tac a') apply (auto dest: fun_relD array_relD) done lemma param_case_array[param]: "(case_array,case_array) \ (\Ra\list_rel \ Rb) \ \Ra\array_rel \ Rb" apply (clarsimp split: array.split) apply (drule array_relD) by parametricity lemma param_case_array1': assumes "(a,a')\\Ra\array_rel" assumes "\l l'. \ a=Array l; a'=Array l'; (l,l')\\Ra\list_rel \ \ (f l,f' l') \ Rb" shows "(case_array f a,case_array f' a') \ Rb" using assms apply (clarsimp split: array.split) apply (drule array_relD) apply parametricity by (rule refl)+ lemmas param_case_array2' = param_case_array1'[folded rec_array_is_case] lemmas param_case_array' = param_case_array1' param_case_array2' lemma param_array_length[param]: "(array_length,array_length) \ \Rb\array_rel \ nat_rel" unfolding array_length_def by parametricity lemma param_array_grow[param]: "(array_grow,array_grow) \ \R\array_rel \ nat_rel \ R \ \R\array_rel" unfolding array_grow_def by parametricity lemma array_rel_imp_same_length: "(a, a') \ \R\array_rel \ array_length a = array_length a'" apply (cases a, cases a') apply (auto simp add: list_rel_imp_same_length dest!: array_relD) done lemma param_array_get[param]: assumes I: "inat_rel" assumes AR: "(a,a')\\R\array_rel" shows "(array_get a i, array_get a' i') \ R" proof - obtain l l' where [simp]: "a = Array l" "a' = Array l'" by (cases a, cases a', simp_all) from AR have LR: "(l,l') \ \R\list_rel" by (force dest!: array_relD) thus ?thesis using assms unfolding array_get_def apply (auto intro!: param_nth[param_fo] dest: list_rel_imp_same_length) done qed lemma param_array_set[param]: "(array_set,array_set)\\R\array_rel\nat_rel\R\\R\array_rel" unfolding array_set_def by parametricity lemma param_array_of_list[param]: "(array_of_list, array_of_list) \ \R\ list_rel \ \R\ array_rel" unfolding array_of_list_def by parametricity lemma param_array_shrink[param]: assumes N: "array_length a \ n" assumes NR: "(n,n')\nat_rel" assumes AR: "(a,a')\\R\array_rel" shows "(array_shrink a n, array_shrink a' n') \ \R\ array_rel" proof- obtain l l' where [simp]: "a = Array l" "a' = Array l'" by (cases a, cases a', simp_all) from AR have LR: "(l,l') \ \R\list_rel" by (auto dest: array_relD) with assms show ?thesis by (auto intro: param_Array[param_fo] param_take[param_fo] dest: array_rel_imp_same_length ) qed lemma param_assoc_list_of_array[param]: "(assoc_list_of_array, assoc_list_of_array) \ \R\ array_rel \ \\nat_rel,R\prod_rel\list_rel" unfolding assoc_list_of_array_def[abs_def] by parametricity lemma param_array_map[param]: "(array_map, array_map) \ (nat_rel \ Ra \ Rb) \ \Ra\array_rel \ \Rb\array_rel" unfolding array_map_def[abs_def] by parametricity lemma param_array_foldr[param]: "(array_foldr, array_foldr) \ (nat_rel \ Ra \ Rb \ Rb) \ \Ra\array_rel \ Rb \ Rb" unfolding array_foldr_def[abs_def] by parametricity lemma param_array_foldl[param]: "(array_foldl, array_foldl) \ (nat_rel \ Rb \ Ra \ Rb) \ Rb \ \Ra\array_rel \ Rb" unfolding array_foldl_def[abs_def] by parametricity subsection \Code Generator Setup\ subsubsection \Code-Numeral Preparation\ definition [code del]: "new_array' v == new_array v o nat_of_integer" definition [code del]: "array_length' == integer_of_nat o array_length" definition [code del]: "array_get' a == array_get a o nat_of_integer" definition [code del]: "array_set' a == array_set a o nat_of_integer" definition [code del]: "array_grow' a == array_grow a o nat_of_integer" definition [code del]: "array_shrink' a == array_shrink a o nat_of_integer" definition [code del]: "array_get_oo' x a == array_get_oo x a o nat_of_integer" definition [code del]: "array_set_oo' f a == array_set_oo f a o nat_of_integer" lemma [code]: "new_array v == new_array' v o integer_of_nat" "array_length == nat_of_integer o array_length'" "array_get a == array_get' a o integer_of_nat" "array_set a == array_set' a o integer_of_nat" "array_grow a == array_grow' a o integer_of_nat" "array_shrink a == array_shrink' a o integer_of_nat" "array_get_oo x a == array_get_oo' x a o integer_of_nat" "array_set_oo f a == array_set_oo' f a o integer_of_nat" by (simp_all add: o_def add: new_array'_def array_length'_def array_get'_def array_set'_def array_grow'_def array_shrink'_def array_get_oo'_def array_set_oo'_def) text \Fallbacks\ lemmas [code] = array_get_oo'_def[unfolded array_get_oo_def[abs_def]] lemmas [code] = array_set_oo'_def[unfolded array_set_oo_def[abs_def]] subsubsection \Code generator setup for Haskell\ code_printing type_constructor array \ (Haskell) "Array.ArrayType/ _" code_reserved Haskell array_of_list (* code_printing code_module "Array" \ (Haskell) {* --import qualified Data.Array.Diff as Arr; import qualified Data.Array as Arr; import Data.Array.IArray; import Nat; instance Ix Nat where { range (Nat a, Nat b) = map Nat (range (a, b)); index (Nat a, Nat b) (Nat c) = index (a,b) c; inRange (Nat a, Nat b) (Nat c) = inRange (a, b) c; rangeSize (Nat a, Nat b) = rangeSize (a, b); }; type ArrayType = Arr.DiffArray Nat; --type ArrayType = Arr.Array Nat; -- we need to start at 1 and not 0, because the empty array -- is modelled by having s > e for (s,e) = bounds -- and as we are in Nat, 0 is the smallest number array_of_size :: Nat -> [e] -> ArrayType e; array_of_size n = Arr.listArray (1, n); new_array :: e -> Nat -> ArrayType e; new_array a n = array_of_size n (repeat a); array_length :: ArrayType e -> Nat; array_length a = let (s, e) = bounds a in if s > e then 0 else e - s + 1; -- the `if` is actually needed, because in Nat we have s > e --> e - s + 1 = 1 array_get :: ArrayType e -> Nat -> e; array_get a i = a ! (i + 1); array_set :: ArrayType e -> Nat -> e -> ArrayType e; array_set a i e = a // [(i + 1, e)]; array_of_list :: [e] -> ArrayType e; array_of_list xs = array_of_size (fromInteger (toInteger (length xs - 1))) xs; array_grow :: ArrayType e -> Nat -> e -> ArrayType e; array_grow a i x = let (s, e) = bounds a in Arr.listArray (s, e+i) (Arr.elems a ++ repeat x); array_shrink :: ArrayType e -> Nat -> ArrayType e; array_shrink a sz = if sz > array_length a then undefined else array_of_size sz (Arr.elems a); *} *) (* TODO/FIXME: Using standard functional arrays here, as DiffArray seems to be discontinued in Haskell! *) code_printing code_module "Array" \ (Haskell) \module Array where { --import qualified Data.Array.Diff as Arr; import qualified Data.Array as Arr; type ArrayType = Arr.Array Integer; array_of_size :: Integer -> [e] -> ArrayType e; array_of_size n = Arr.listArray (0, n-1); new_array :: e -> Integer -> ArrayType e; new_array a n = array_of_size n (repeat a); array_length :: ArrayType e -> Integer; array_length a = let (s, e) = Arr.bounds a in e; array_get :: ArrayType e -> Integer -> e; array_get a i = a Arr.! i; array_set :: ArrayType e -> Integer -> e -> ArrayType e; array_set a i e = a Arr.// [(i, e)]; array_of_list :: [e] -> ArrayType e; array_of_list xs = array_of_size (toInteger (length xs)) xs; array_grow :: ArrayType e -> Integer -> e -> ArrayType e; array_grow a i x = let (s, e) = Arr.bounds a in Arr.listArray (s, e+i) (Arr.elems a ++ repeat x); array_shrink :: ArrayType e -> Integer -> ArrayType e; array_shrink a sz = if sz > array_length a then undefined else array_of_size sz (Arr.elems a); }\ code_printing constant Array \ (Haskell) "Array.array'_of'_list" code_printing constant new_array' \ (Haskell) "Array.new'_array" code_printing constant array_length' \ (Haskell) "Array.array'_length" code_printing constant array_get' \ (Haskell) "Array.array'_get" code_printing constant array_set' \ (Haskell) "Array.array'_set" code_printing constant array_of_list \ (Haskell) "Array.array'_of'_list" code_printing constant array_grow' \ (Haskell) "Array.array'_grow" code_printing constant array_shrink' \ (Haskell) "Array.array'_shrink" subsubsection \Code Generator Setup For SML\ text \ We have the choice between single-threaded arrays, that raise an exception if an old version is accessed, and truly functional arrays, that update the array in place, but store undo-information to restore old versions. \ code_printing code_module "STArray" \ (SML) \ structure STArray = struct datatype 'a Cell = Invalid | Value of 'a array; exception AccessedOldVersion; type 'a array = 'a Cell Unsynchronized.ref; fun fromList l = Unsynchronized.ref (Value (Array.fromList l)); fun array (size, v) = Unsynchronized.ref (Value (Array.array (size,v))); fun tabulate (size, f) = Unsynchronized.ref (Value (Array.tabulate(size, f))); fun sub (Unsynchronized.ref Invalid, idx) = raise AccessedOldVersion | sub (Unsynchronized.ref (Value a), idx) = Array.sub (a,idx); fun update (aref,idx,v) = case aref of (Unsynchronized.ref Invalid) => raise AccessedOldVersion | (Unsynchronized.ref (Value a)) => ( aref := Invalid; Array.update (a,idx,v); Unsynchronized.ref (Value a) ); fun length (Unsynchronized.ref Invalid) = raise AccessedOldVersion | length (Unsynchronized.ref (Value a)) = Array.length a fun grow (aref, i, x) = case aref of (Unsynchronized.ref Invalid) => raise AccessedOldVersion | (Unsynchronized.ref (Value a)) => ( let val len=Array.length a; val na = Array.array (len+i,x) in aref := Invalid; Array.copy {src=a, dst=na, di=0}; Unsynchronized.ref (Value na) end ); fun shrink (aref, sz) = case aref of (Unsynchronized.ref Invalid) => raise AccessedOldVersion | (Unsynchronized.ref (Value a)) => ( if sz > Array.length a then raise Size else ( aref:=Invalid; Unsynchronized.ref (Value (Array.tabulate (sz,fn i => Array.sub (a,i)))) ) ); structure IsabelleMapping = struct type 'a ArrayType = 'a array; fun new_array (a:'a) (n:IntInf.int) = array (IntInf.toInt n, a); fun array_length (a:'a ArrayType) = IntInf.fromInt (length a); fun array_get (a:'a ArrayType) (i:IntInf.int) = sub (a, IntInf.toInt i); fun array_set (a:'a ArrayType) (i:IntInf.int) (e:'a) = update (a, IntInf.toInt i, e); fun array_of_list (xs:'a list) = fromList xs; fun array_grow (a:'a ArrayType) (i:IntInf.int) (x:'a) = grow (a, IntInf.toInt i, x); fun array_shrink (a:'a ArrayType) (sz:IntInf.int) = shrink (a,IntInf.toInt sz); end; end; structure FArray = struct datatype 'a Cell = Value of 'a Array.array | Upd of (int*'a*'a Cell Unsynchronized.ref); type 'a array = 'a Cell Unsynchronized.ref; fun array (size,v) = Unsynchronized.ref (Value (Array.array (size,v))); fun tabulate (size, f) = Unsynchronized.ref (Value (Array.tabulate(size, f))); fun fromList l = Unsynchronized.ref (Value (Array.fromList l)); fun sub (Unsynchronized.ref (Value a), idx) = Array.sub (a,idx) | sub (Unsynchronized.ref (Upd (i,v,cr)),idx) = if i=idx then v else sub (cr,idx); fun length (Unsynchronized.ref (Value a)) = Array.length a | length (Unsynchronized.ref (Upd (i,v,cr))) = length cr; fun realize_aux (aref, v) = case aref of (Unsynchronized.ref (Value a)) => ( let val len = Array.length a; val a' = Array.array (len,v); in Array.copy {src=a, dst=a', di=0}; Unsynchronized.ref (Value a') end ) | (Unsynchronized.ref (Upd (i,v,cr))) => ( let val res=realize_aux (cr,v) in case res of (Unsynchronized.ref (Value a)) => (Array.update (a,i,v); res) end ); fun realize aref = case aref of (Unsynchronized.ref (Value _)) => aref | (Unsynchronized.ref (Upd (i,v,cr))) => realize_aux(aref,v); fun update (aref,idx,v) = case aref of (Unsynchronized.ref (Value a)) => ( let val nref=Unsynchronized.ref (Value a) in aref := Upd (idx,Array.sub(a,idx),nref); Array.update (a,idx,v); nref end ) | (Unsynchronized.ref (Upd _)) => let val ra = realize_aux(aref,v) in case ra of (Unsynchronized.ref (Value a)) => Array.update (a,idx,v); ra end ; fun grow (aref, inc, x) = case aref of (Unsynchronized.ref (Value a)) => ( let val len=Array.length a; val na = Array.array (len+inc,x) in Array.copy {src=a, dst=na, di=0}; Unsynchronized.ref (Value na) end ) | (Unsynchronized.ref (Upd _)) => ( grow (realize aref, inc, x) ); fun shrink (aref, sz) = case aref of (Unsynchronized.ref (Value a)) => ( if sz > Array.length a then raise Size else ( Unsynchronized.ref (Value (Array.tabulate (sz,fn i => Array.sub (a,i)))) ) ) | (Unsynchronized.ref (Upd _)) => ( shrink (realize aref,sz) ); structure IsabelleMapping = struct type 'a ArrayType = 'a array; fun new_array (a:'a) (n:IntInf.int) = array (IntInf.toInt n, a); fun array_length (a:'a ArrayType) = IntInf.fromInt (length a); fun array_get (a:'a ArrayType) (i:IntInf.int) = sub (a, IntInf.toInt i); fun array_set (a:'a ArrayType) (i:IntInf.int) (e:'a) = update (a, IntInf.toInt i, e); fun array_of_list (xs:'a list) = fromList xs; fun array_grow (a:'a ArrayType) (i:IntInf.int) (x:'a) = grow (a, IntInf.toInt i, x); fun array_shrink (a:'a ArrayType) (sz:IntInf.int) = shrink (a,IntInf.toInt sz); fun array_get_oo (d:'a) (a:'a ArrayType) (i:IntInf.int) = sub (a,IntInf.toInt i) handle Subscript => d fun array_set_oo (d:(unit->'a ArrayType)) (a:'a ArrayType) (i:IntInf.int) (e:'a) = update (a, IntInf.toInt i, e) handle Subscript => d () end; end; \ code_printing type_constructor array \ (SML) "_/ FArray.IsabelleMapping.ArrayType" | constant Array \ (SML) "FArray.IsabelleMapping.array'_of'_list" | constant new_array' \ (SML) "FArray.IsabelleMapping.new'_array" | constant array_length' \ (SML) "FArray.IsabelleMapping.array'_length" | constant array_get' \ (SML) "FArray.IsabelleMapping.array'_get" | constant array_set' \ (SML) "FArray.IsabelleMapping.array'_set" | constant array_grow' \ (SML) "FArray.IsabelleMapping.array'_grow" | constant array_shrink' \ (SML) "FArray.IsabelleMapping.array'_shrink" | constant array_of_list \ (SML) "FArray.IsabelleMapping.array'_of'_list" | constant array_get_oo' \ (SML) "FArray.IsabelleMapping.array'_get'_oo" | constant array_set_oo' \ (SML) "FArray.IsabelleMapping.array'_set'_oo" subsection \Code Generator Setup for Scala\ text \ We use a DiffArray-Implementation in Scala. \ code_printing code_module "DiffArray" \ (Scala) \ object Array { class T[A](n: Int) { val array: Array[AnyRef] = new Array[AnyRef](n) def apply(i: Int): A = array(i).asInstanceOf[A] def update(i: Int, x: A): Unit = array(i) = x.asInstanceOf[AnyRef] def length: Int = array.length def toList: List[A] = array.toList.asInstanceOf[List[A]] override def toString: String = array.mkString("Array.T(", ",", ")") } def init[A](n: Int)(f: Int => A): T[A] = { val a = new T[A](n) for (i <- 0 until n) a(i) = f(i) a } def init_list[A](list: List[A]): T[A] = { val n = list.length val a = new T[A](n) var i = 0 for (x <- list) { a(i) = x i += 1 } a } def make[A](n: BigInt)(f: BigInt => A): T[A] = init(n.toInt)((i: Int) => f(BigInt(i))) def copy[A](a: T[A]): T[A] = init(a.length)(i => a(i)) def alloc[A](n: BigInt)(x: A): T[A] = init(n.toInt)(_ => x) def len[A](a: T[A]): BigInt = BigInt(a.length) def nth[A](a: T[A], n: BigInt): A = a(n.toInt) def upd[A](a: T[A], n: BigInt, x: A): Unit = a.update(n.toInt, x) def freeze[A](a: T[A]): List[A] = a.toList } object DiffArray { protected abstract sealed class DiffArray_D[A] final case class Current[A] (a:Array.T[AnyRef]) extends DiffArray_D[A] final case class Upd[A] (i:Int, v:A, n:DiffArray_D[A]) extends DiffArray_D[A] object DiffArray_Realizer { def realize[A](a:DiffArray_D[A]): Array.T[AnyRef] = a match { case Current(a) => Array.copy(a) case Upd(j,v,n) => {val a = realize(n); a.update(j, v.asInstanceOf[AnyRef]); a} } } class T[A] (var d:DiffArray_D[A]) { def realize (): Array.T[AnyRef] = { val a=DiffArray_Realizer.realize(d); d = Current(a); a } override def toString() = Array.freeze(realize()).toString override def equals(obj:Any) = - if (obj.isInstanceOf[T[A]]) obj.asInstanceOf[T[A]].realize().equals(realize()) - else false - + obj.isInstanceOf[T[A]] match { + case true => obj.asInstanceOf[T[A]].realize().equals(realize()) + case false => false + } } def array_of_list[A](l : List[A]) : T[A] = new T(Current(Array.init_list(l.asInstanceOf[List[AnyRef]]))) def new_array[A](v: A, sz: BigInt) = new T[A](Current[A](Array.alloc[AnyRef](sz.intValue)(v.asInstanceOf[AnyRef]))) private def length[A](a:DiffArray_D[A]) : BigInt = a match { case Current(a) => a.length case Upd(_,_,n) => length(n) } def length[A](a : T[A]) : BigInt = length(a.d) private def sub[A](a:DiffArray_D[A], i:Int) : A = a match { case Current(a) => a(i).asInstanceOf[A] - case Upd(j,v,n) => if (i==j) v else sub(n,i) + case Upd(j,v,n) => i==j match { case true => v case false => sub(n,i) } } def get[A](a:T[A], i:BigInt) : A = sub(a.d,i.intValue) private def realize[A](a:DiffArray_D[A]): Array.T[AnyRef] = DiffArray_Realizer.realize[A](a) def set[A](a:T[A], i:BigInt,v:A) : T[A] = a.d match { case Current(ad) => { val ii = i.intValue; a.d = Upd(ii,ad(ii).asInstanceOf[A],a.d); //ad.update(ii,v); ad(ii)=v.asInstanceOf[AnyRef] new T[A](Current(ad)) } case Upd(_,_,_) => set(new T[A](Current(realize(a.d))), i.intValue,v) } def grow[A](a:T[A], sz:BigInt, v:A) : T[A] = a.d match { case Current(ad) => { val n = ad.length - val adt = Array.init[AnyRef](sz.intValue)(i => if (i < n) ad(i) else v.asInstanceOf[AnyRef]) + val adt = Array.init[AnyRef](sz.intValue)(i => i < n match { case true => ad(i) case false => v.asInstanceOf[AnyRef] }) new T[A](Current[A](adt)) } case Upd (_,_,_) => { val ad = realize(a.d) val n = ad.length - val adt = Array.init[AnyRef](sz.intValue)(i => if (i < n) ad(i) else v.asInstanceOf[AnyRef]) + val adt = Array.init[AnyRef](sz.intValue)(i => i < n match { case true => ad(i) case false => v.asInstanceOf[AnyRef] }) new T[A](Current[A](adt)) } } def shrink[A](a:T[A], sz:BigInt) : T[A] = - if (sz==0) { - array_of_list(Nil) - } else { - a.d match { - case Current(ad) => { - val adt = Array.init[AnyRef](sz.intValue)(i => ad(i)); - new T[A](Current[A](adt)) + sz==0 match { + case true => array_of_list(Nil) + case false => + a.d match { + case Current(ad) => { + val adt = Array.init[AnyRef](sz.intValue)(i => ad(i)); + new T[A](Current[A](adt)) + } + case Upd (_,_,_) => { + val ad = realize(a.d); + val adt = Array.init[AnyRef](sz.intValue)(i => ad(i)); + new T[A](Current[A](adt)) + } } - case Upd (_,_,_) => { - val ad = realize(a.d); - val adt = Array.init[AnyRef](sz.intValue)(i => ad(i)); - new T[A](Current[A](adt)) - } - } } def get_oo[A](d: => A, a:T[A], i:BigInt):A = try get(a,i) catch { case _:scala.IndexOutOfBoundsException => d } def set_oo[A](d: Unit => T[A], a:T[A], i:BigInt, v:A) : T[A] = try set(a,i,v) catch { case _:scala.IndexOutOfBoundsException => d(()) } } /* object Test { - def assert (b : Boolean) : Unit = if (b) () else throw new java.lang.AssertionError("Assertion Failed") + def assert (b : Boolean) : Unit = b match { case true => () case false => throw new java.lang.AssertionError("Assertion Failed") } def eql[A] (a:DiffArray.T[A], b:List[A]) = assert (a.realize.corresponds(b)((x,y) => x.equals(y))) def tests1(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Another update val c = DiffArray.set(b,3,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::9::Nil) // Update of old version (forces realize) val d = DiffArray.set(b,2,8) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::9::Nil) eql(d,1::2::8::4::Nil) } def tests2(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Grow of current version val c = DiffArray.grow(b,6,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::4::9::9::Nil) // Grow of old version val d = DiffArray.grow(a,6,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::4::9::9::Nil) eql(d,1::2::3::4::9::9::Nil) } def tests3(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Shrink of current version val c = DiffArray.shrink(b,3) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::Nil) // Shrink of old version val d = DiffArray.shrink(a,3) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::Nil) eql(d,1::2::3::Nil) } def tests4(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Update _oo (succeeds) val b = DiffArray.set_oo((_) => a,a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Update _oo (current version,fails) val c = DiffArray.set_oo((_) => a,b,5,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::3::4::Nil) // Update _oo (old version,fails) val d = DiffArray.set_oo((_) => b,a,5,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::3::4::Nil) eql(d,1::2::9::4::Nil) } def tests5(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Get_oo (current version, succeeds) assert (DiffArray.get_oo(0,b,2)==9) // Get_oo (current version, fails) assert (DiffArray.get_oo(0,b,5)==0) // Get_oo (old version, succeeds) assert (DiffArray.get_oo(0,a,2)==3) // Get_oo (old version, fails) assert (DiffArray.get_oo(0,a,5)==0) } def main(args: Array[String]): Unit = { tests1 () tests2 () tests3 () tests4 () tests5 () Console.println("Tests passed") } }*/ \ code_printing type_constructor array \ (Scala) "DiffArray.T[_]" | constant Array \ (Scala) "DiffArray.array'_of'_list" | constant new_array' \ (Scala) "DiffArray.new'_array((_),(_).toInt)" | constant array_length' \ (Scala) "DiffArray.length((_)).toInt" | constant array_get' \ (Scala) "DiffArray.get((_),(_).toInt)" | constant array_set' \ (Scala) "DiffArray.set((_),(_).toInt,(_))" | constant array_grow' \ (Scala) "DiffArray.grow((_),(_).toInt,(_))" | constant array_shrink' \ (Scala) "DiffArray.shrink((_),(_).toInt)" | constant array_of_list \ (Scala) "DiffArray.array'_of'_list" | constant array_get_oo' \ (Scala) "DiffArray.get'_oo((_),(_),(_).toInt)" | constant array_set_oo' \ (Scala) "DiffArray.set'_oo((_),(_),(_).toInt,(_))" context begin (*private*) definition "test_diffarray_setup \ (Array,new_array',array_length',array_get', array_set', array_grow', array_shrink',array_of_list,array_get_oo',array_set_oo')" export_code test_diffarray_setup checking Scala SML OCaml? Haskell? end end diff --git a/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy b/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy --- a/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy +++ b/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy @@ -1,438 +1,438 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Initializing the Printer\ theory Printer_init imports "../Init" "../isabelle_home/src/HOL/Isabelle_Main1" begin text\At the time of writing, the following target languages supported by Isabelle are also supported by the meta-compiler: Haskell, OCaml, Scala, SML.\ subsection\Kernel Code for Target Languages\ (* We put in 'CodeConst' functions using characters not allowed in a Isabelle 'code_const' expr (e.g. '_', '"', ...) *) lazy_code_printing code_module "CodeType" \ (Haskell) \ module CodeType where { type MlInt = Integer ; type MlMonad a = IO a }\ | code_module "CodeConst" \ (Haskell) \ module CodeConst where { import System.Directory ; import System.IO ; import qualified CodeConst.Printf ; outFile1 f file = (do fileExists <- doesFileExist file if fileExists then error ("File exists " ++ file ++ "\n") else do h <- openFile file WriteMode f (\pat -> hPutStr h . CodeConst.Printf.sprintf1 pat) hClose h) ; outStand1 :: ((String -> String -> IO ()) -> IO ()) -> IO () ; outStand1 f = f (\pat -> putStr . CodeConst.Printf.sprintf1 pat) }\ | code_module "CodeConst.Monad" \ (Haskell) \ module CodeConst.Monad where { bind a = (>>=) a ; return :: a -> IO a ; return = Prelude.return }\ | code_module "CodeConst.Printf" \ (Haskell) \ module CodeConst.Printf where { import Text.Printf ; sprintf0 = id ; sprintf1 :: PrintfArg a => String -> a -> String ; sprintf1 = printf ; sprintf2 :: PrintfArg a => PrintfArg b => String -> a -> b -> String ; sprintf2 = printf ; sprintf3 :: PrintfArg a => PrintfArg b => PrintfArg c => String -> a -> b -> c -> String ; sprintf3 = printf ; sprintf4 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => String -> a -> b -> c -> d -> String ; sprintf4 = printf ; sprintf5 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => PrintfArg e => String -> a -> b -> c -> d -> e -> String ; sprintf5 = printf }\ | code_module "CodeConst.String" \ (Haskell) \ module CodeConst.String where { concat s [] = [] ; concat s (x : xs) = x ++ concatMap ((++) s) xs }\ | code_module "CodeConst.Sys" \ (Haskell) \ module CodeConst.Sys where { import System.Directory ; isDirectory2 = doesDirectoryExist }\ | code_module "CodeConst.To" \ (Haskell) \ module CodeConst.To where { nat = id }\ | code_module "" \ (OCaml) \ module CodeType = struct type mlInt = int type 'a mlMonad = 'a option end module CodeConst = struct let outFile1 f file = try let () = if Sys.file_exists file then Printf.eprintf "File exists \"%S\"\n" file else () in let oc = open_out file in let b = f (fun s a -> try Some (Printf.fprintf oc s a) with _ -> None) in let () = close_out oc in b with _ -> None let outStand1 f = f (fun s a -> try Some (Printf.fprintf stdout s a) with _ -> None) module Monad = struct let bind = function None -> fun _ -> None | Some a -> fun f -> f a let return a = Some a end module Printf = struct include Printf let sprintf0 = sprintf let sprintf1 = sprintf let sprintf2 = sprintf let sprintf3 = sprintf let sprintf4 = sprintf let sprintf5 = sprintf end module String = String module Sys = struct open Sys let isDirectory2 s = try Some (is_directory s) with _ -> None end module To = struct let nat big_int x = Big_int.int_of_big_int (big_int x) end end \ | code_module "" \ (Scala) \ object CodeType { type mlMonad [A] = Option [A] type mlInt = Int } object CodeConst { def outFile1 [A] (f : (String => A => Option [Unit]) => Option [Unit], file0 : String) : Option [Unit] = { val file = new java.io.File (file0) - if (file .isFile) { - None - } else { - val writer = new java.io.PrintWriter (file) - f ((fmt : String) => (s : A) => Some (writer .write (fmt .format (s)))) - Some (writer .close ()) + file .isFile match { + case true => None + case false => + val writer = new java.io.PrintWriter (file) + f ((fmt : String) => (s : A) => Some (writer .write (fmt .format (s)))) + Some (writer .close ()) } } def outStand1 [A] (f : (String => A => Option [Unit]) => Option [Unit]) : Option[Unit] = { f ((fmt : String) => (s : A) => Some (print (fmt .format (s)))) } object Monad { def bind [A, B] (x : Option [A], f : A => Option [B]) : Option [B] = x match { case None => None case Some (a) => f (a) } def Return [A] (a : A) = Some (a) } object Printf { def sprintf0 (x0 : String) = x0 def sprintf1 [A1] (fmt : String, x1 : A1) = fmt .format (x1) def sprintf2 [A1, A2] (fmt : String, x1 : A1, x2 : A2) = fmt .format (x1, x2) def sprintf3 [A1, A2, A3] (fmt : String, x1 : A1, x2 : A2, x3 : A3) = fmt .format (x1, x2, x3) def sprintf4 [A1, A2, A3, A4] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4) = fmt .format (x1, x2, x3, x4) def sprintf5 [A1, A2, A3, A4, A5] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4, x5 : A5) = fmt .format (x1, x2, x3, x4, x5) } object String { def concat (s : String, l : List [String]) = l filter (_ .nonEmpty) mkString s } object Sys { def isDirectory2 (s : String) = Some (new java.io.File (s) .isDirectory) } object To { def nat [A] (f : A => BigInt, x : A) = f (x) .intValue () } } \ | code_module "" \ (SML) \ structure CodeType = struct type mlInt = string type 'a mlMonad = 'a option end structure CodeConst = struct structure Monad = struct val bind = fn NONE => (fn _ => NONE) | SOME a => fn f => f a val return = SOME end structure Printf = struct local fun sprintf s l = case String.fields (fn #"%" => true | _ => false) s of [] => "" | [x] => x | x :: xs => let fun aux acc l_pat l_s = case l_pat of [] => rev acc | x :: xs => aux (String.extract (x, 1, NONE) :: hd l_s :: acc) xs (tl l_s) in String.concat (x :: aux [] xs l) end in fun sprintf0 s_pat = s_pat fun sprintf1 s_pat s1 = sprintf s_pat [s1] fun sprintf2 s_pat s1 s2 = sprintf s_pat [s1, s2] fun sprintf3 s_pat s1 s2 s3 = sprintf s_pat [s1, s2, s3] fun sprintf4 s_pat s1 s2 s3 s4 = sprintf s_pat [s1, s2, s3, s4] fun sprintf5 s_pat s1 s2 s3 s4 s5 = sprintf s_pat [s1, s2, s3, s4, s5] end end structure String = struct val concat = String.concatWith end structure Sys = struct val isDirectory2 = SOME o File.is_dir o Path.explode handle ERROR _ => K NONE end structure To = struct fun nat f = Int.toString o f end fun outFile1 f file = let val pfile = Path.explode file val () = if File.exists pfile then error ("File exists \"" ^ file ^ "\"\n") else () val oc = Unsynchronized.ref [] val _ = f (fn a => fn b => SOME (oc := Printf.sprintf1 a b :: (Unsynchronized.! oc))) in try (fn () => File.write_list pfile (rev (Unsynchronized.! oc))) () end fun outStand1 f = outFile1 f (Unsynchronized.! stdout_file) end \ subsection\Interface with Types\ datatype ml_int = ML_int code_printing type_constructor ml_int \ (Haskell) "CodeType.MlInt" \ \syntax!\ | type_constructor ml_int \ (OCaml) "CodeType.mlInt" | type_constructor ml_int \ (Scala) "CodeType.mlInt" | type_constructor ml_int \ (SML) "CodeType.mlInt" datatype 'a ml_monad = ML_monad 'a code_printing type_constructor ml_monad \ (Haskell) "CodeType.MlMonad _" \ \syntax!\ | type_constructor ml_monad \ (OCaml) "_ CodeType.mlMonad" | type_constructor ml_monad \ (Scala) "CodeType.mlMonad [_]" | type_constructor ml_monad \ (SML) "_ CodeType.mlMonad" type_synonym ml_string = String.literal subsection\Interface with Constants\ text\module CodeConst\ consts out_file1 :: "((ml_string \ '\1 \ unit ml_monad) \ \fprintf\ \ unit ml_monad) \ ml_string \ unit ml_monad" code_printing constant out_file1 \ (Haskell) "CodeConst.outFile1" | constant out_file1 \ (OCaml) "CodeConst.outFile1" | constant out_file1 \ (Scala) "CodeConst.outFile1" | constant out_file1 \ (SML) "CodeConst.outFile1" consts out_stand1 :: "((ml_string \ '\1 \ unit ml_monad) \ \fprintf\ \ unit ml_monad) \ unit ml_monad" code_printing constant out_stand1 \ (Haskell) "CodeConst.outStand1" | constant out_stand1 \ (OCaml) "CodeConst.outStand1" | constant out_stand1 \ (Scala) "CodeConst.outStand1" | constant out_stand1 \ (SML) "CodeConst.outStand1" text\module Monad\ consts bind :: "'a ml_monad \ ('a \ 'b ml_monad) \ 'b ml_monad" code_printing constant bind \ (Haskell) "CodeConst.Monad.bind" | constant bind \ (OCaml) "CodeConst.Monad.bind" | constant bind \ (Scala) "CodeConst.Monad.bind" | constant bind \ (SML) "CodeConst.Monad.bind" consts return :: "'a \ 'a ml_monad" code_printing constant return \ (Haskell) "CodeConst.Monad.return" | constant return \ (OCaml) "CodeConst.Monad.return" | constant return \ (Scala) "CodeConst.Monad.Return" \ \syntax!\ | constant return \ (SML) "CodeConst.Monad.return" text\module Printf\ consts sprintf0 :: "ml_string \ ml_string" code_printing constant sprintf0 \ (Haskell) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (OCaml) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (Scala) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (SML) "CodeConst.Printf.sprintf0" consts sprintf1 :: "ml_string \ '\1 \ ml_string" code_printing constant sprintf1 \ (Haskell) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (OCaml) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (Scala) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (SML) "CodeConst.Printf.sprintf1" consts sprintf2 :: "ml_string \ '\1 \ '\2 \ ml_string" code_printing constant sprintf2 \ (Haskell) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (OCaml) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (Scala) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (SML) "CodeConst.Printf.sprintf2" consts sprintf3 :: "ml_string \ '\1 \ '\2 \ '\3 \ ml_string" code_printing constant sprintf3 \ (Haskell) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (OCaml) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (Scala) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (SML) "CodeConst.Printf.sprintf3" consts sprintf4 :: "ml_string \ '\1 \ '\2 \ '\3 \ '\4 \ ml_string" code_printing constant sprintf4 \ (Haskell) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (OCaml) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (Scala) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (SML) "CodeConst.Printf.sprintf4" consts sprintf5 :: "ml_string \ '\1 \ '\2 \ '\3 \ '\4 \ '\5 \ ml_string" code_printing constant sprintf5 \ (Haskell) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (OCaml) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (Scala) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (SML) "CodeConst.Printf.sprintf5" text\module String\ consts String_concat :: "ml_string \ ml_string list \ ml_string" code_printing constant String_concat \ (Haskell) "CodeConst.String.concat" | constant String_concat \ (OCaml) "CodeConst.String.concat" | constant String_concat \ (Scala) "CodeConst.String.concat" | constant String_concat \ (SML) "CodeConst.String.concat" text\module Sys\ consts Sys_is_directory2 :: "ml_string \ bool ml_monad" code_printing constant Sys_is_directory2 \ (Haskell) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (OCaml) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (Scala) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (SML) "CodeConst.Sys.isDirectory2" text\module To\ consts ToNat :: "(nat \ integer) \ nat \ ml_int" code_printing constant ToNat \ (Haskell) "CodeConst.To.nat" | constant ToNat \ (OCaml) "CodeConst.To.nat" | constant ToNat \ (Scala) "CodeConst.To.nat" | constant ToNat \ (SML) "CodeConst.To.nat" subsection\Some Notations (I): Raw Translations\ syntax "_sprint0" :: "_ \ ml_string" ("sprint0 (_)\") translations "sprint0 x\" \ "CONST sprintf0 x" syntax "_sprint1" :: "_ \ _ \ ml_string" ("sprint1 (_)\") translations "sprint1 x\" \ "CONST sprintf1 x" syntax "_sprint2" :: "_ \ _ \ ml_string" ("sprint2 (_)\") translations "sprint2 x\" \ "CONST sprintf2 x" syntax "_sprint3" :: "_ \ _ \ ml_string" ("sprint3 (_)\") translations "sprint3 x\" \ "CONST sprintf3 x" syntax "_sprint4" :: "_ \ _ \ ml_string" ("sprint4 (_)\") translations "sprint4 x\" \ "CONST sprintf4 x" syntax "_sprint5" :: "_ \ _ \ ml_string" ("sprint5 (_)\") translations "sprint5 x\" \ "CONST sprintf5 x" subsection\Some Notations (II): Polymorphic Cartouches\ syntax "_cartouche_string'" :: String.literal translations "_cartouche_string" \ "_cartouche_string'" parse_translation \ [( @{syntax_const "_cartouche_string'"} , parse_translation_cartouche @{binding cartouche_type'} (( "fun\<^sub>p\<^sub>r\<^sub>i\<^sub>n\<^sub>t\<^sub>f" , ( Cartouche_Grammar.nil1 , Cartouche_Grammar.cons1 , let fun f c x = Syntax.const c $ x in fn (0, x) => x | (1, x) => f @{const_syntax sprintf1} x | (2, x) => f @{const_syntax sprintf2} x | (3, x) => f @{const_syntax sprintf3} x | (4, x) => f @{const_syntax sprintf4} x | (5, x) => f @{const_syntax sprintf5} x end)) :: Cartouche_Grammar.default) (fn 37 \ \\<^verbatim>\#"%"\\ => (fn x => x + 1) | _ => I) 0)] \ subsection\Generic Locale for Printing\ locale Print = fixes To_string :: "string \ ml_string" fixes To_nat :: "nat \ ml_int" begin declare[[cartouche_type' = "fun\<^sub>p\<^sub>r\<^sub>i\<^sub>n\<^sub>t\<^sub>f"]] end text\As remark, printing functions (like @{term sprintf5}...) are currently weakly typed in Isabelle, we will continue the typing using the type system of target languages.\ end diff --git a/thys/MDP-Algorithms/code/lib/DiffArray_Base.thy b/thys/MDP-Algorithms/code/lib/DiffArray_Base.thy --- a/thys/MDP-Algorithms/code/lib/DiffArray_Base.thy +++ b/thys/MDP-Algorithms/code/lib/DiffArray_Base.thy @@ -1,830 +1,831 @@ (* Author: Peter Lammich *) theory DiffArray_Base imports Main "HOL-Library.Code_Target_Numeral" begin subsection \Additional List Operations\ definition "tabulate n f = map f [0.._. c) = replicate n c" by (auto simp: map_replicate_trivial) lemma length_tabulate[simp]: "length (tabulate n f) = n" by simp lemma nth_tabulate[simp]: "i tabulate n f ! i = f i" by simp lemma upd_tabulate: "(tabulate n f)[i:=x] = tabulate n (f(i:=x))" apply (induction n) by (auto simp: list_update_append split: nat.split) lemma take_tabulate: "take n (tabulate m f) = tabulate (min n m) f" by (simp add: min_def take_map) lemma hd_tabulate[simp]: "n\0 \ hd (tabulate n f) = f 0" by (cases n) (simp add: map_upt_Suc del: upt_Suc)+ lemma tl_tabulate: "tl (tabulate n f) = tabulate (n-1) (f o Suc)" apply (simp add: map_upt_Suc map_Suc_upt del: upt_Suc flip: map_tl map_map) by (cases n; simp) lemma tabulate_cong[fundef_cong]: "n=n' \ (\i. i f i = f' i) \ tabulate n f = tabulate n' f'" by simp lemma tabulate_nth_take: "n \ length xs \ tabulate n ((!) xs) = take n xs" by (rule nth_equalityI, auto) end lemma drop_tabulate: "drop n (tabulate m f) = tabulate (m-n) (f o (+)n)" apply (induction n arbitrary: m f) apply (auto simp: drop_Suc drop_tl tl_tabulate comp_def) done subsection \Primitive Operations\ typedef 'a array = "UNIV :: 'a list set" morphisms array_\ Array by blast setup_lifting type_definition_array lift_definition array_new :: "nat \ 'a \ 'a array" is "\n a. replicate n a" . lift_definition array_tabulate :: "nat \ (nat \ 'a) \ 'a array" is "\n f. Array (tabulate n f)" . lift_definition array_length :: "'a array \ nat" is length . lift_definition array_get :: "'a array \ nat \ 'a" is nth . lift_definition array_set :: "'a array \ nat \ 'a \ 'a array" is list_update . lift_definition array_of_list :: "'a list \ 'a array" is \\x. x\ . subsubsection \Refinement Lemmas\ named_theorems array_refine context notes [simp] = Array_inverse begin lemma array_\_inj: "array_\ a = array_\ b \ a=b" by transfer auto lemma array_eq_iff: "a=b \ array_\ a = array_\ b" by transfer auto lemma array_new_refine[simp,array_refine]: "array_\ (array_new n a) = replicate n a" by transfer auto lemma array_tabulate_refine[simp,array_refine]: "array_\ (array_tabulate n f) = tabulate n f" by transfer auto lemma array_length_refine[simp,array_refine]: "array_length a = length (array_\ a)" by transfer auto lemma array_get_refine[simp,array_refine]: "array_get a i = array_\ a ! i" by transfer auto lemma array_set_refine[simp,array_refine]: "array_\ (array_set a i x) = (array_\ a)[i := x]" by transfer auto lemma array_of_list_refine[simp,array_refine]: "array_\ (array_of_list xs) = xs" by transfer auto end lifting_update array.lifting lifting_forget array.lifting subsection \Basic Derived Operations\ text \These operations may have direct implementations in target language\ definition "array_grow a n dflt = ( let la = array_length a in array_tabulate n (\i. if ii. if i < length xs then xs!i else d) = take n xs @ (replicate (n-length xs) d)" apply (induction n) apply (auto simp: tabulate_Suc take_Suc_conv_app_nth replicate_append_same Suc_diff_le) done lemma array_grow_refine[simp,array_refine]: "array_\ (array_grow a n d) = take n (array_\ a) @ replicate (n-length (array_\ a)) d" by (auto simp: array_grow_def tabulate_grow cong: if_cong) definition "array_take a n = ( let n = min (array_length a) n in array_tabulate n (array_get a) )" lemma tabulate_take: "tabulate (min (length xs) n) ((!) xs) = take n xs" by (auto simp: min_def tabulate_nth_take) lemma array_take_refine[simp,array_refine]: "array_\ (array_take a n) = take n (array_\ a)" by (auto simp: array_take_def tabulate_take cong: tabulate_cong) text \The following is a total version of \array_get\, which returns a default value in case the index is out of bounds. This can be efficiently implemented in the target language by catching exceptions. \ definition "array_get_oo x a i \ if i a) then array_\ a!i else x)" by (simp add: array_get_oo_def) definition "array_set_oo f a i x \ if i (array_set_oo f a i x) = (if i a) then (array_\ a)[i:=x] else array_\ (f ()))" by (simp add: array_set_oo_def) text \ Map array. No old versions for intermediate results need to be tracked, which allows more efficient in-place implementation in case access to old versions is forbidden. \ definition "array_map f a \ array_tabulate (array_length a) (f o array_get a)" lemma array_map_refine[simp,array_refine]: "array_\ (array_map f a) = map f (array_\ a)" unfolding array_map_def apply (auto simp: tabulate_def simp flip: map_map cong: map_cong) by (smt (z3) atLeastLessThan_iff length_map map_eq_conv map_nth nth_map set_upt) lemma array_map_cong[fundef_cong]: "a=a' \ (\x. x\set (array_\ a) \ f x = f' x) \ array_map f a = array_map f' a'" by (simp add: array_eq_iff) context fixes f :: "'a \ 's \ 's" and xs :: "'a list" begin function foldl_idx where "foldl_idx i s = (if i(i,_). length xs - i)") apply auto done lemmas [simp del] = foldl_idx.simps lemma foldl_idx_eq: "foldl_idx i s = fold f (drop i xs) s" apply (induction i s rule: foldl_idx.induct) apply (subst foldl_idx.simps) apply (auto simp flip: Cons_nth_drop_Suc) done lemma fold_by_idx: "fold f xs s = foldl_idx 0 s" using foldl_idx_eq by simp end fun foldr_idx where "foldr_idx f xs 0 s = s" | "foldr_idx f xs (Suc i) s = foldr_idx f xs i (f (xs!i) s)" lemma foldr_idx_eq: "i\length xs \ foldr_idx f xs i s = foldr f (take i xs) s" apply (induction i arbitrary: s) apply (auto simp: take_Suc_conv_app_nth) done lemma foldr_by_idx: "foldr f xs s = foldr_idx f xs (length xs) s" apply (subst foldr_idx_eq) by auto context fixes f :: "'a \ 's \ 's" and a :: "'a array" begin function array_foldl_idx where "array_foldl_idx i s = (if i(i,_). array_length a - i)") apply auto done lemmas [simp del] = array_foldl_idx.simps end lemma array_foldl_idx_refine[simp, array_refine]: "array_foldl_idx f a i s = foldl_idx f (array_\ a) i s" apply (induction i s rule: foldl_idx.induct) apply (subst array_foldl_idx.simps) apply (subst foldl_idx.simps) by fastforce definition "array_fold f a s \ array_foldl_idx f a 0 s" lemma array_fold_refine[simp, array_refine]: "array_fold f a s = fold f (array_\ a) s" unfolding array_fold_def by (simp add: fold_by_idx) fun array_foldr_idx where "array_foldr_idx f xs 0 s = s" | "array_foldr_idx f xs (Suc i) s = array_foldr_idx f xs i (f (array_get xs i) s)" lemma array_foldr_idx_refine[simp, array_refine]: "array_foldr_idx f xs i s = foldr_idx f (array_\ xs) i s" apply (induction i arbitrary: s) by auto definition "array_foldr f xs s \ array_foldr_idx f xs (array_length xs) s" lemma array_foldr_refine[simp, array_refine]: "array_foldr f xs s = foldr f (array_\ xs) s" by (simp add: array_foldr_def foldr_by_idx) subsection \Code Generator Setup\ subsubsection \Code-Numeral Preparation\ definition [code del]: "array_new' == array_new o nat_of_integer" definition [code del]: "array_tabulate' n f \ array_tabulate (nat_of_integer n) (f o integer_of_nat)" definition [code del]: "array_length' == integer_of_nat o array_length" definition [code del]: "array_get' a == array_get a o nat_of_integer" definition [code del]: "array_set' a == array_set a o nat_of_integer" definition [code del]: "array_get_oo' x a == array_get_oo x a o nat_of_integer" definition [code del]: "array_set_oo' f a == array_set_oo f a o nat_of_integer" lemma [code]: "array_new == array_new' o integer_of_nat" "array_tabulate n f == array_tabulate' (integer_of_nat n) (f o nat_of_integer)" "array_length == nat_of_integer o array_length'" "array_get a == array_get' a o integer_of_nat" "array_set a == array_set' a o integer_of_nat" "array_get_oo x a == array_get_oo' x a o integer_of_nat" "array_set_oo g a == array_set_oo' g a o integer_of_nat" by (simp_all del: array_refine add: o_def add: array_new'_def array_tabulate'_def array_length'_def array_get'_def array_set'_def array_get_oo'_def array_set_oo'_def) text \Fallbacks\ lemmas array_get_oo'_fallback[code] = array_get_oo'_def[unfolded array_get_oo_def[abs_def]] lemmas array_set_oo'_fallback[code] = array_set_oo'_def[unfolded array_set_oo_def[abs_def]] lemma array_tabulate'_fallback[code]: "array_tabulate' n f = array_of_list (map (f o integer_of_nat) [0..Haskell\ code_printing type_constructor array \ (Haskell) "Array.ArrayType/ _" code_reserved Haskell array_of_list (* code_printing code_module "Array" \ (Haskell) {* --import qualified Data.Array.Diff as Arr; import qualified Data.Array as Arr; import Data.Array.IArray; import Nat; instance Ix Nat where { range (Nat a, Nat b) = map Nat (range (a, b)); index (Nat a, Nat b) (Nat c) = index (a,b) c; inRange (Nat a, Nat b) (Nat c) = inRange (a, b) c; rangeSize (Nat a, Nat b) = rangeSize (a, b); }; type ArrayType = Arr.DiffArray Nat; --type ArrayType = Arr.Array Nat; -- we need to start at 1 and not 0, because the empty array -- is modelled by having s > e for (s,e) = bounds -- and as we are in Nat, 0 is the smallest number array_of_size :: Nat -> [e] -> ArrayType e; array_of_size n = Arr.listArray (1, n); array_new :: e -> Nat -> ArrayType e; array_new a n = array_of_size n (repeat a); array_length :: ArrayType e -> Nat; array_length a = let (s, e) = bounds a in if s > e then 0 else e - s + 1; -- the `if` is actually needed, because in Nat we have s > e --> e - s + 1 = 1 array_get :: ArrayType e -> Nat -> e; array_get a i = a ! (i + 1); array_set :: ArrayType e -> Nat -> e -> ArrayType e; array_set a i e = a // [(i + 1, e)]; array_of_list :: [e] -> ArrayType e; array_of_list xs = array_of_size (fromInteger (toInteger (length xs - 1))) xs; array_grow :: ArrayType e -> Nat -> e -> ArrayType e; array_grow a i x = let (s, e) = bounds a in Arr.listArray (s, e+i) (Arr.elems a ++ repeat x); array_shrink :: ArrayType e -> Nat -> ArrayType e; array_shrink a sz = if sz > array_length a then undefined else array_of_size sz (Arr.elems a); *} *) (* TODO/FIXME: Using standard functional arrays here, as DiffArray seems to be discontinued in Haskell! *) code_printing code_module "Array" \ (Haskell) \module Array where { --import qualified Data.Array.Diff as Arr; import qualified Data.Array as Arr; type ArrayType = Arr.Array Integer; array_of_size :: Integer -> [e] -> ArrayType e; array_of_size n = Arr.listArray (0, n-1); array_new :: Integer -> e -> ArrayType e; array_new n a = array_of_size n (repeat a); array_length :: ArrayType e -> Integer; array_length a = let (s, e) = Arr.bounds a in e; array_get :: ArrayType e -> Integer -> e; array_get a i = a Arr.! i; array_set :: ArrayType e -> Integer -> e -> ArrayType e; array_set a i e = a Arr.// [(i, e)]; array_of_list :: [e] -> ArrayType e; array_of_list xs = array_of_size (toInteger (length xs)) xs; }\ code_printing constant Array \ (Haskell) "Array.array'_of'_list" code_printing constant array_new' \ (Haskell) "Array.array'_new" code_printing constant array_length' \ (Haskell) "Array.array'_length" code_printing constant array_get' \ (Haskell) "Array.array'_get" code_printing constant array_set' \ (Haskell) "Array.array'_set" code_printing constant array_of_list \ (Haskell) "Array.array'_of'_list" subsubsection \SML\ text \ We have the choice between single-threaded arrays, that raise an exception if an old version is accessed, and truly functional arrays, that update the array in place, but store undo-information to restore old versions. \ code_printing code_module "FArray" \ (SML) \ structure FArray = struct datatype 'a Cell = Value of 'a Array.array | Upd of (int*'a*'a Cell Unsynchronized.ref); type 'a array = 'a Cell Unsynchronized.ref; fun array (size,v) = Unsynchronized.ref (Value (Array.array (size,v))); fun tabulate (size, f) = Unsynchronized.ref (Value (Array.tabulate(size, f))); fun fromList l = Unsynchronized.ref (Value (Array.fromList l)); fun sub (Unsynchronized.ref (Value a), idx) = Array.sub (a,idx) | sub (Unsynchronized.ref (Upd (i,v,cr)),idx) = if i=idx then v else sub (cr,idx); fun length (Unsynchronized.ref (Value a)) = Array.length a | length (Unsynchronized.ref (Upd (i,v,cr))) = length cr; fun realize_aux (aref, v) = case aref of (Unsynchronized.ref (Value a)) => ( let val len = Array.length a; val a' = Array.array (len,v); in Array.copy {src=a, dst=a', di=0}; Unsynchronized.ref (Value a') end ) | (Unsynchronized.ref (Upd (i,v,cr))) => ( let val res=realize_aux (cr,v) in case res of (Unsynchronized.ref (Value a)) => (Array.update (a,i,v); res) end ); fun realize aref = case aref of (Unsynchronized.ref (Value _)) => aref | (Unsynchronized.ref (Upd (i,v,cr))) => realize_aux(aref,v); fun update (aref,idx,v) = case aref of (Unsynchronized.ref (Value a)) => ( let val nref=Unsynchronized.ref (Value a) in aref := Upd (idx,Array.sub(a,idx),nref); Array.update (a,idx,v); nref end ) | (Unsynchronized.ref (Upd _)) => let val ra = realize_aux(aref,v) in case ra of (Unsynchronized.ref (Value a)) => Array.update (a,idx,v); ra end ; structure IsabelleMapping = struct type 'a ArrayType = 'a array; fun array_new (n:IntInf.int) (a:'a) = array (IntInf.toInt n, a); fun array_of_list (xs:'a list) = fromList xs; fun array_tabulate (n:IntInf.int) (f:IntInf.int -> 'a) = tabulate (IntInf.toInt n, f o IntInf.fromInt) fun array_length (a:'a ArrayType) = IntInf.fromInt (length a); fun array_get (a:'a ArrayType) (i:IntInf.int) = sub (a, IntInf.toInt i); fun array_set (a:'a ArrayType) (i:IntInf.int) (e:'a) = update (a, IntInf.toInt i, e); fun array_get_oo (d:'a) (a:'a ArrayType) (i:IntInf.int) = sub (a,IntInf.toInt i) handle Subscript => d fun array_set_oo (d:(unit->'a ArrayType)) (a:'a ArrayType) (i:IntInf.int) (e:'a) = update (a, IntInf.toInt i, e) handle Subscript => d () end; end; \ code_printing type_constructor array \ (SML) "_/ FArray.IsabelleMapping.ArrayType" | constant Array \ (SML) "FArray.IsabelleMapping.array'_of'_list" | constant array_new' \ (SML) "FArray.IsabelleMapping.array'_new" | constant array_tabulate' \ (SML) "FArray.IsabelleMapping.array'_tabulate" | constant array_length' \ (SML) "FArray.IsabelleMapping.array'_length" | constant array_get' \ (SML) "FArray.IsabelleMapping.array'_get" | constant array_set' \ (SML) "FArray.IsabelleMapping.array'_set" | constant array_of_list \ (SML) "FArray.IsabelleMapping.array'_of'_list" | constant array_get_oo' \ (SML) "FArray.IsabelleMapping.array'_get'_oo" | constant array_set_oo' \ (SML) "FArray.IsabelleMapping.array'_set'_oo" subsubsection \Scala\ text \ We use a DiffArray-Implementation in Scala. \ code_printing code_module "DiffArray" \ (Scala) \ object DiffArray { import scala.collection.mutable.ArraySeq protected abstract sealed class DiffArray_D[A] final case class Current[A] (a:ArraySeq[AnyRef]) extends DiffArray_D[A] final case class Upd[A] (i:Int, v:A, n:DiffArray_D[A]) extends DiffArray_D[A] object DiffArray_Realizer { def realize[A](a:DiffArray_D[A]) : ArraySeq[AnyRef] = a match { case Current(a) => ArraySeq.empty ++ a case Upd(j,v,n) => {val a = realize(n); a.update(j, v.asInstanceOf[AnyRef]); a} } } class T[A] (var d:DiffArray_D[A]) { def realize (): ArraySeq[AnyRef] = { val a=DiffArray_Realizer.realize(d); d = Current(a); a } override def toString() = realize().toSeq.toString override def equals(obj:Any) = - if (obj.isInstanceOf[T[A]]) obj.asInstanceOf[T[A]].realize().equals(realize()) - else false - + obj.isInstanceOf[T[A]] match { + case true => obj.asInstanceOf[T[A]].realize().equals(realize()) + case false => false + } } def array_of_list[A](l : List[A]) : T[A] = new T(Current(ArraySeq.empty ++ l.asInstanceOf[List[AnyRef]])) def array_new[A](sz : BigInt, v:A) = new T[A](Current[A](ArraySeq.fill[AnyRef](sz.intValue)(v.asInstanceOf[AnyRef]))) private def length[A](a:DiffArray_D[A]) : BigInt = a match { case Current(a) => a.length case Upd(_,_,n) => length(n) } def length[A](a : T[A]) : BigInt = length(a.d) private def sub[A](a:DiffArray_D[A], i:Int) : A = a match { case Current(a) => a(i).asInstanceOf[A] case Upd(j,v,n) => if (i==j) v else sub(n,i) } def get[A](a:T[A], i:BigInt) : A = sub(a.d,i.intValue) private def realize[A](a:DiffArray_D[A]): ArraySeq[AnyRef] = DiffArray_Realizer.realize[A](a) def set[A](a:T[A], i:BigInt,v:A) : T[A] = a.d match { case Current(ad) => { val ii = i.intValue; a.d = Upd(ii,ad(ii).asInstanceOf[A],a.d); //ad.update(ii,v); ad(ii)=v.asInstanceOf[AnyRef] new T[A](Current(ad)) } case Upd(_,_,_) => set(new T[A](Current(realize(a.d))), i.intValue,v) } def get_oo[A](d: => A, a:T[A], i:BigInt):A = try get(a,i) catch { case _:scala.IndexOutOfBoundsException => d } def set_oo[A](d: Unit => T[A], a:T[A], i:BigInt, v:A) : T[A] = try set(a,i,v) catch { case _:scala.IndexOutOfBoundsException => d(()) } } object Test { def assert (b : Boolean) : Unit = if (b) () else throw new java.lang.AssertionError("Assertion Failed") def eql[A] (a:DiffArray.T[A], b:List[A]) = assert (a.realize.corresponds(b)((x,y) => x.equals(y))) def tests1(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Another update val c = DiffArray.set(b,3,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::9::Nil) // Update of old version (forces realize) val d = DiffArray.set(b,2,8) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::9::Nil) eql(d,1::2::8::4::Nil) } def tests2(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Grow of current version /* val c = DiffArray.grow(b,6,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::4::9::9::Nil) // Grow of old version val d = DiffArray.grow(a,6,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::4::9::9::Nil) eql(d,1::2::3::4::9::9::Nil) */ } def tests3(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Simple update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) /* // Shrink of current version val c = DiffArray.shrink(b,3) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::Nil) // Shrink of old version val d = DiffArray.shrink(a,3) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::9::Nil) eql(d,1::2::3::Nil) */ } def tests4(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Update _oo (succeeds) val b = DiffArray.set_oo((_) => a,a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Update _oo (current version,fails) val c = DiffArray.set_oo((_) => a,b,5,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::3::4::Nil) // Update _oo (old version,fails) val d = DiffArray.set_oo((_) => b,a,5,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) eql(c,1::2::3::4::Nil) eql(d,1::2::9::4::Nil) } def tests5(): Unit = { val a = DiffArray.array_of_list(1::2::3::4::Nil) eql(a,1::2::3::4::Nil) // Update val b = DiffArray.set(a,2,9) eql(a,1::2::3::4::Nil) eql(b,1::2::9::4::Nil) // Get_oo (current version, succeeds) assert (DiffArray.get_oo(0,b,2)==9) // Get_oo (current version, fails) assert (DiffArray.get_oo(0,b,5)==0) // Get_oo (old version, succeeds) assert (DiffArray.get_oo(0,a,2)==3) // Get_oo (old version, fails) assert (DiffArray.get_oo(0,a,5)==0) } def main(args: Array[String]): Unit = { tests1 () tests2 () tests3 () tests4 () tests5 () Console.println("Tests passed") } } \ code_printing type_constructor array \ (Scala) "DiffArray.T[_]" | constant Array \ (Scala) "DiffArray.array'_of'_list" | constant array_new' \ (Scala) "DiffArray.array'_new((_).toInt,(_))" | constant array_length' \ (Scala) "DiffArray.length((_)).toInt" | constant array_get' \ (Scala) "DiffArray.get((_),(_).toInt)" | constant array_set' \ (Scala) "DiffArray.set((_),(_).toInt,(_))" | constant array_of_list \ (Scala) "DiffArray.array'_of'_list" | constant array_get_oo' \ (Scala) "DiffArray.get'_oo((_),(_),(_).toInt)" | constant array_set_oo' \ (Scala) "DiffArray.set'_oo((_),(_),(_).toInt,(_))" context begin (*private*) definition "test_diffarray_setup \ (Array,array_new',array_length',array_get', array_set', array_of_list,array_get_oo',array_set_oo')" export_code test_diffarray_setup checking SML OCaml? Haskell? end subsection \Tests\ (* TODO: Add more systematic tests! *) definition "test1 \ let a=array_of_list [1,2,3,4,5,6]; b=array_tabulate 6 (Suc); a'=array_set a 3 42; b'=array_set b 3 42; c=array_new 6 0 in \i\{0..<6}. array_get a i = i+1 \ array_get b i = i+1 \ array_get a' i = (if i=3 then 42 else i+1) \ array_get b' i = (if i=3 then 42 else i+1) \ array_get c i = (0::nat) " lemma enum_rangeE: assumes "i\{l..{Suc l.. P i" shows "P i" using assms by (metis atLeastLessThan_iff less_eq_Suc_le nat_less_le) lemma "test1" unfolding test1_def Let_def apply (intro ballI conjI) apply (erule enum_rangeE, (simp; fail))+ apply simp apply (erule enum_rangeE, (simp; fail))+ apply simp apply (erule enum_rangeE, (simp; fail))+ apply simp apply (erule enum_rangeE, (simp; fail))+ apply simp apply (erule enum_rangeE, (simp; fail))+ apply simp done ML_val \ if not @{code test1} then error "ERROR" else () \ export_code test1 checking OCaml? Haskell? SML hide_const test1 hide_fact test1_def experiment begin fun allTrue :: "bool list \ nat \ bool list" where "allTrue a 0 = a" | "allTrue a (Suc i) = (allTrue a i)[i := True]" lemma length_allTrue: "n \ length a \ length(allTrue a n) = length a" by(induction n) (auto) lemma "n \ length a \ \i < n. (allTrue a n) ! i" by(induction n) (auto simp: nth_list_update length_allTrue) fun allTrue' :: "bool array \ nat \ bool array" where "allTrue' a 0 = a" | "allTrue' a (Suc i) = array_set (allTrue' a i) i True" lemma "array_\ (allTrue' xs i) = allTrue (array_\ xs) i" apply (induction xs i rule: allTrue'.induct) apply auto done end end diff --git a/thys/Native_Word/Code_Target_Integer_Bit.thy b/thys/Native_Word/Code_Target_Integer_Bit.thy --- a/thys/Native_Word/Code_Target_Integer_Bit.thy +++ b/thys/Native_Word/Code_Target_Integer_Bit.thy @@ -1,635 +1,633 @@ (* Title: Code_Target_Integer_Bit.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Bit operations for target language integers\ theory Code_Target_Integer_Bit imports "HOL-Library.Word" "Code_Int_Integer_Conversion" "Word_Lib.Most_significant_bit" "Word_Lib.Least_significant_bit" "Word_Lib.Generic_set_bit" "Word_Lib.Bit_Comprehension" begin text \TODO: separate\ lemmas [transfer_rule] = identity_quotient fun_quotient Quotient_integer[folded integer.pcr_cr_eq] lemma undefined_transfer: assumes "Quotient R Abs Rep T" shows "T (Rep undefined) undefined" using assms unfolding Quotient_alt_def by blast bundle undefined_transfer = undefined_transfer[transfer_rule] section \More lemmas about @{typ integer}s\ context includes integer.lifting begin lemma integer_of_nat_less_0_conv [simp]: "\ integer_of_nat n < 0" by transfer simp lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n" by transfer rule lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0 \ False" by transfer (simp add: sub_negative) lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n" by transfer simp lemma nat_of_integer_sub1_conv_pred_numeral [simp]: "nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n" by transfer (simp only: pred_numeral_def int_nat_eq numeral_One int_minus flip: int_int_eq, simp) lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1" by transfer simp lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2" by transfer simp lift_definition bin_rest_integer :: "integer \ integer" is \\k . k div 2\ . lift_definition bin_last_integer :: "integer \ bool" is odd . lift_definition Bit_integer :: "integer \ bool \ integer" is \\k b. of_bool b + 2 * k\ . end section \Target language implementations\ text \ Unfortunately, this is not straightforward, because these API functions have different signatures and preconditions on the parameters: \begin{description} \item[Standard ML] Shifts in IntInf are given as word, but not IntInf. \item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer. \end{description} Additional constants take only parameters of type @{typ integer} rather than @{typ nat} and check the preconditions as far as possible (e.g., being non-negative) in a portable way. Manual implementations inside code\_printing perform the remaining range checks and convert these @{typ integer}s into the right type. For normalisation by evaluation, we derive custom code equations, because NBE does not know these code\_printing serialisations and would otherwise loop. \ code_printing code_module Integer_Bit \ (SML) \structure Integer_Bit : sig val test_bit : IntInf.int -> IntInf.int -> bool val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int val shiftl : IntInf.int -> IntInf.int -> IntInf.int val shiftr : IntInf.int -> IntInf.int -> IntInf.int end = struct val maxWord = IntInf.pow (2, Word.wordSize); fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else raise (Fail ("Bit index too large: " ^ IntInf.toString n)); fun set_bit x n b = if n < maxWord then if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))) else raise (Fail ("Bit index too large: " ^ IntInf.toString n)); fun shiftl x n = if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)) else raise (Fail ("Shift operand too large: " ^ IntInf.toString n)); fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else raise (Fail ("Shift operand too large: " ^ IntInf.toString n)); end; (*struct Integer_Bit*)\ code_reserved SML Integer_Bit code_printing code_module Integer_Bit \ (OCaml) \module Integer_Bit : sig val test_bit : Z.t -> Z.t -> bool val shiftl : Z.t -> Z.t -> Z.t val shiftr : Z.t -> Z.t -> Z.t end = struct (* We do not need an explicit range checks here, because Big_int.int_of_big_int raises Failure if the argument does not fit into an int. *) let test_bit x n = Z.testbit x (Z.to_int n);; let shiftl x n = Z.shift_left x (Z.to_int n);; let shiftr x n = Z.shift_right x (Z.to_int n);; end;; (*struct Integer_Bit*)\ code_reserved OCaml Integer_Bit code_printing code_module Data_Bits \ (Haskell) \ module Data_Bits where { import qualified Data.Bits; {- The ...Bounded functions assume that the Integer argument for the shift or bit index fits into an Int, is non-negative and (for types of fixed bit width) less than bitSize -} infixl 7 .&.; infixl 6 `xor`; infixl 5 .|.; (.&.) :: Data.Bits.Bits a => a -> a -> a; (.&.) = (Data.Bits..&.); xor :: Data.Bits.Bits a => a -> a -> a; xor = Data.Bits.xor; (.|.) :: Data.Bits.Bits a => a -> a -> a; (.|.) = (Data.Bits..|.); complement :: Data.Bits.Bits a => a -> a; complement = Data.Bits.complement; testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool; testBitUnbounded x b | b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b) | otherwise = error ("Bit index too large: " ++ show b) ; testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool; testBitBounded x b = Data.Bits.testBit x (fromInteger b); setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a; setBitUnbounded x n b | n <= toInteger (Prelude.maxBound :: Int) = if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n) | otherwise = error ("Bit index too large: " ++ show n) ; setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a; setBitBounded x n True = Data.Bits.setBit x (fromInteger n); setBitBounded x n False = Data.Bits.clearBit x (fromInteger n); shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a; shiftlUnbounded x n | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n) | otherwise = error ("Shift operand too large: " ++ show n) ; shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a; shiftlBounded x n = Data.Bits.shiftL x (fromInteger n); shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a; shiftrUnbounded x n | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n) | otherwise = error ("Shift operand too large: " ++ show n) ; shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a; shiftrBounded x n = Data.Bits.shiftR x (fromInteger n); }\ and \ \@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to Haskell's Prelude.Int type instead of Integer. For compatibility with the Haskell target, we nevertheless provide bounded and unbounded functions.\ (Haskell_Quickcheck) \ module Data_Bits where { import qualified Data.Bits; {- The functions assume that the Int argument for the shift or bit index is non-negative and (for types of fixed bit width) less than bitSize -} infixl 7 .&.; infixl 6 `xor`; infixl 5 .|.; (.&.) :: Data.Bits.Bits a => a -> a -> a; (.&.) = (Data.Bits..&.); xor :: Data.Bits.Bits a => a -> a -> a; xor = Data.Bits.xor; (.|.) :: Data.Bits.Bits a => a -> a -> a; (.|.) = (Data.Bits..|.); complement :: Data.Bits.Bits a => a -> a; complement = Data.Bits.complement; testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool; testBitUnbounded = Data.Bits.testBit; testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool; testBitBounded = Data.Bits.testBit; setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a; setBitUnbounded x n True = Data.Bits.setBit x n; setBitUnbounded x n False = Data.Bits.clearBit x n; setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a; setBitBounded x n True = Data.Bits.setBit x n; setBitBounded x n False = Data.Bits.clearBit x n; shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftlUnbounded = Data.Bits.shiftL; shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftlBounded = Data.Bits.shiftL; shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftrUnbounded = Data.Bits.shiftR; shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a; shiftrBounded = Data.Bits.shiftR; }\ code_reserved Haskell Data_Bits code_printing code_module Integer_Bit \ (Scala) \object Integer_Bit { def testBit(x: BigInt, n: BigInt) : Boolean = - if (n.isValidInt) - x.testBit(n.toInt) - else - sys.error("Bit index too large: " + n.toString) + n.isValidInt match { + case true => x.testBit(n.toInt) + case false => sys.error("Bit index too large: " + n.toString) + } def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt = - if (n.isValidInt) - if (b) - x.setBit(n.toInt) - else - x.clearBit(n.toInt) - else - sys.error("Bit index too large: " + n.toString) + n.isValidInt match { + case true if b => x.setBit(n.toInt) + case true => x.clearBit(n.toInt) + case false => sys.error("Bit index too large: " + n.toString) + } def shiftl(x: BigInt, n: BigInt) : BigInt = - if (n.isValidInt) - x << n.toInt - else - sys.error("Shift index too large: " + n.toString) + n.isValidInt match { + case true => x << n.toInt + case false => sys.error("Shift index too large: " + n.toString) + } def shiftr(x: BigInt, n: BigInt) : BigInt = - if (n.isValidInt) - x << n.toInt - else - sys.error("Shift index too large: " + n.toString) + n.isValidInt match { + case true => x << n.toInt + case false => sys.error("Shift index too large: " + n.toString) + } } /* object Integer_Bit */\ code_printing constant "Bit_Operations.and :: integer \ integer \ integer" \ (SML) "IntInf.andb ((_),/ (_))" and (OCaml) "Z.logand" and (Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: integer \ integer \ integer" \ (SML) "IntInf.orb ((_),/ (_))" and (OCaml) "Z.logor" and (Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: integer \ integer \ integer" \ (SML) "IntInf.xorb ((_),/ (_))" and (OCaml) "Z.logxor" and (Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 2 "^" | constant "Bit_Operations.not :: integer \ integer" \ (SML) "IntInf.notb" and (OCaml) "Z.lognot" and (Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and (Scala) "_.unary'_~" code_printing constant bin_rest_integer \ (SML) "IntInf.div ((_), 2)" and (OCaml) "Z.shift'_right/ _/ 1" and (Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and (Scala) "_ >> 1" context includes integer.lifting bit_operations_syntax begin lemma bitNOT_integer_code [code]: fixes i :: integer shows "NOT i = - i - 1" by transfer (simp add: not_int_def) lemma bin_rest_integer_code [code nbe]: "bin_rest_integer i = i div 2" by transfer rule lemma bin_last_integer_code [code]: "bin_last_integer i \ i AND 1 \ 0" by transfer (simp add: and_one_eq odd_iff_mod_2_eq_one) lemma bin_last_integer_nbe [code nbe]: "bin_last_integer i \ i mod 2 \ 0" by transfer (simp add: odd_iff_mod_2_eq_one) lemma bitval_bin_last_integer [code_unfold]: "of_bool (bin_last_integer i) = i AND 1" by transfer (simp add: and_one_eq mod_2_eq_odd) end definition integer_test_bit :: "integer \ integer \ bool" where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))" declare [[code drop: \bit :: integer \ nat \ bool\]] lemma bit_integer_code [code]: "bit x n \ integer_test_bit x (integer_of_nat n)" by (simp add: integer_test_bit_def) lemma integer_test_bit_code [code]: "integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_test_bit 0 0 = False" "integer_test_bit 0 (Code_Numeral.Pos n) = False" "integer_test_bit (Code_Numeral.Pos num.One) 0 = True" "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False" "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True" "integer_test_bit (Code_Numeral.Pos num.One) (Code_Numeral.Pos n') = False" "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Neg num.One) 0 = True" "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False" "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True" "integer_test_bit (Code_Numeral.Neg num.One) (Code_Numeral.Pos n') = True" "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)" by (simp_all add: integer_test_bit_def bit_integer_def bit_0 flip: bit_not_int_iff') code_printing constant integer_test_bit \ (SML) "Integer'_Bit.test'_bit" and (OCaml) "Integer'_Bit.test'_bit" and (Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and (Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and (Scala) "Integer'_Bit.testBit" context includes integer.lifting bit_operations_syntax begin lemma lsb_integer_code [code]: fixes x :: integer shows "lsb x = bit x 0" by transfer(simp add: lsb_int_def) definition integer_set_bit :: "integer \ integer \ bool \ integer" where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_integer_code [code]: "set_bit x i b = integer_set_bit x (integer_of_nat i) b" by(simp add: integer_set_bit_def) lemma set_bit_integer_conv_masks: fixes x :: integer shows "set_bit x i b = (if b then x OR (push_bit i 1) else x AND NOT (push_bit i 1))" by (transfer; rule bit_eqI) (simp add: bit_simps) end code_printing constant integer_set_bit \ (SML) "Integer'_Bit.set'_bit" and (Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and (Scala) "Integer'_Bit.setBit" text \ OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks. We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR. \ context includes bit_operations_syntax begin lemma integer_set_bit_code [code]: "integer_set_bit x n b = (if n < 0 then undefined x n b else if b then x OR (push_bit (nat_of_integer n) 1) else x AND NOT (push_bit (nat_of_integer n) 1))" by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def) end definition integer_shiftl :: "integer \ integer \ integer" where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)" declare [[code drop: \push_bit :: nat \ integer \ integer\]] lemma shiftl_integer_code [code]: fixes x :: integer shows "push_bit n x = integer_shiftl x (integer_of_nat n)" by(auto simp add: integer_shiftl_def) context includes integer.lifting begin lemma shiftl_integer_conv_mult_pow2: fixes x :: integer shows "push_bit n x = x * 2 ^ n" by (fact push_bit_eq_mult) lemma integer_shiftl_code [code]: "integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_shiftl x 0 = x" "integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)" "integer_shiftl 0 (Code_Numeral.Pos n) = 0" apply (simp_all add: integer_shiftl_def numeral_eq_Suc) apply transfer apply (simp add: ac_simps) done end code_printing constant integer_shiftl \ (SML) "Integer'_Bit.shiftl" and (OCaml) "Integer'_Bit.shiftl" and (Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) "Integer'_Bit.shiftl" definition integer_shiftr :: "integer \ integer \ integer" where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)" declare [[code drop: \drop_bit :: nat \ integer \ integer\]] lemma shiftr_integer_conv_div_pow2: includes integer.lifting fixes x :: integer shows "drop_bit n x = x div 2 ^ n" by (fact drop_bit_eq_div) lemma shiftr_integer_code [code]: fixes x :: integer shows "drop_bit n x = integer_shiftr x (integer_of_nat n)" by(auto simp add: integer_shiftr_def) code_printing constant integer_shiftr \ (SML) "Integer'_Bit.shiftr" and (OCaml) "Integer'_Bit.shiftr" and (Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) "Integer'_Bit.shiftr" lemma integer_shiftr_code [code]: includes integer.lifting shows "integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_shiftr x 0 = x" "integer_shiftr 0 (Code_Numeral.Pos n) = 0" "integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0" "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1" "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)" apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc) apply transfer apply simp apply transfer apply simp apply transfer apply (simp add: add_One) done context includes integer.lifting begin lemma Bit_integer_code [code]: "Bit_integer i False = push_bit 1 i" "Bit_integer i True = push_bit 1 i + 1" by (transfer; simp)+ lemma msb_integer_code [code]: "msb (x :: integer) \ x < 0" by transfer (simp add: msb_int_def) end context includes integer.lifting bit_operations_syntax begin lemma bitAND_integer_unfold [code]: "x AND y = (if x = 0 then 0 else if x = - 1 then y else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps and_int_rec [of _ \_ * 2\] and_int_rec [of \_ * 2\] and_int_rec [of \1 + _ * 2\] elim!: evenE oddE) lemma bitOR_integer_unfold [code]: "x OR y = (if x = 0 then y else if x = - 1 then - 1 else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps or_int_rec [of _ \_ * 2\] or_int_rec [of _ \1 + _ * 2\] or_int_rec [of \1 + _ * 2\] elim!: evenE oddE) lemma bitXOR_integer_unfold [code]: "x XOR y = (if x = 0 then y else if x = - 1 then NOT y else Bit_integer (bin_rest_integer x XOR bin_rest_integer y) (\ bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps xor_int_rec [of _ \_ * 2\] xor_int_rec [of \_ * 2\] xor_int_rec [of \1 + _ * 2\] elim!: evenE oddE) end section \Test code generator setup\ context includes bit_operations_syntax begin definition bit_integer_test :: "bool" where "bit_integer_test = (([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5) , -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5) , NOT 1, NOT (- 3) , -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3) , set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False , push_bit 2 1, push_bit 3 (- 1) , drop_bit 3 100, drop_bit 3 (- 100)] :: integer list) = [ 3, 1, 1, -7 , -3, -3, 7, -1 , -2, 2 , -4, -4, 6, 6 , 21, -1, 4, -7 , 4, -8 , 12, -13] \ [ bit (5 :: integer) 4, bit (5 :: integer) 2, bit (-5 :: integer) 4, bit (-5 :: integer) 2 , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer), msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)] = [ False, True, True, False, True, False, True, False, False, False, True, True])" export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala notepad begin have bit_integer_test by eval have bit_integer_test by normalization have bit_integer_test by code_simp end ML_val \val true = @{code bit_integer_test}\ lemma "x AND y = x OR (y :: integer)" quickcheck[random, expect=counterexample] quickcheck[exhaustive, expect=counterexample] oops lemma "(x :: integer) AND x = x OR x" quickcheck[narrowing, expect=no_counterexample] oops lemma "(f :: integer \ unit) = g" quickcheck[narrowing, size=3, expect=no_counterexample] by(simp add: fun_eq_iff) end hide_const bit_integer_test hide_fact bit_integer_test_def end diff --git a/thys/Native_Word/Uint.thy b/thys/Native_Word/Uint.thy --- a/thys/Native_Word/Uint.thy +++ b/thys/Native_Word/Uint.thy @@ -1,824 +1,828 @@ (* Title: Uint.thy Author: Peter Lammich, TU Munich Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of default size\ theory Uint imports Word_Type_Copies Code_Target_Integer_Bit begin text \ This theory provides access to words in the target languages of the code generator whose bit width is the default of the target language. To that end, the type \uint\ models words of width \dflt_size\, but \dflt_size\ is known only to be positive. Usage restrictions: Default-size words (type \uint\) cannot be used for evaluation, because the results depend on the particular choice of word size in the target language and implementation. Symbolic evaluation has not yet been set up for \uint\. \ text \The default size type\ typedecl dflt_size instantiation dflt_size :: typerep begin definition "typerep_class.typerep \ \_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []" instance .. end consts dflt_size_aux :: "nat" specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0" by auto hide_fact dflt_size_aux_def instantiation dflt_size :: len begin definition "len_of_dflt_size (_ :: dflt_size itself) \ dflt_size_aux" instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0) end abbreviation "dflt_size \ len_of (TYPE (dflt_size))" context includes integer.lifting begin lift_definition dflt_size_integer :: integer is "int dflt_size" . declare dflt_size_integer_def[code del] \ \The code generator will substitute a machine-dependent value for this constant\ lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer" by transfer simp lemma dflt_size[simp]: "dflt_size > 0" "dflt_size \ Suc 0" "\ dflt_size < Suc 0" using len_gt_0[where 'a=dflt_size] by (simp_all del: len_gt_0) end section \Type definition and primitive operations\ typedef uint = \UNIV :: dflt_size word set\ .. global_interpretation uint: word_type_copy Abs_uint Rep_uint using type_definition_uint by (rule word_type_copy.intro) setup_lifting type_definition_uint declare uint.of_word_of [code abstype] declare Quotient_uint [transfer_rule] instantiation uint :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint :: uint is 0 . lift_definition one_uint :: uint is 1 . lift_definition plus_uint :: \uint \ uint \ uint\ is \(+)\ . lift_definition uminus_uint :: \uint \ uint\ is uminus . lift_definition minus_uint :: \uint \ uint \ uint\ is \(-)\ . lift_definition times_uint :: \uint \ uint \ uint\ is \(*)\ . lift_definition divide_uint :: \uint \ uint \ uint\ is \(div)\ . lift_definition modulo_uint :: \uint \ uint \ uint\ is \(mod)\ . lift_definition equal_uint :: \uint \ uint \ bool\ is \HOL.equal\ . lift_definition less_eq_uint :: \uint \ uint \ bool\ is \(\)\ . lift_definition less_uint :: \uint \ uint \ bool\ is \(<)\ . global_interpretation uint: word_type_copy_ring Abs_uint Rep_uint by standard (fact zero_uint.rep_eq one_uint.rep_eq plus_uint.rep_eq uminus_uint.rep_eq minus_uint.rep_eq times_uint.rep_eq divide_uint.rep_eq modulo_uint.rep_eq equal_uint.rep_eq less_eq_uint.rep_eq less_uint.rep_eq)+ instance proof - show \OFCLASS(uint, comm_ring_1_class)\ by (rule uint.of_class_comm_ring_1) show \OFCLASS(uint, semiring_modulo_class)\ by (fact uint.of_class_semiring_modulo) show \OFCLASS(uint, equal_class)\ by (fact uint.of_class_equal) show \OFCLASS(uint, linorder_class)\ by (fact uint.of_class_linorder) qed end instantiation uint :: ring_bit_operations begin lift_definition bit_uint :: \uint \ nat \ bool\ is bit . lift_definition not_uint :: \uint \ uint\ is \Bit_Operations.not\ . lift_definition and_uint :: \uint \ uint \ uint\ is \Bit_Operations.and\ . lift_definition or_uint :: \uint \ uint \ uint\ is \Bit_Operations.or\ . lift_definition xor_uint :: \uint \ uint \ uint\ is \Bit_Operations.xor\ . lift_definition mask_uint :: \nat \ uint\ is mask . lift_definition push_bit_uint :: \nat \ uint \ uint\ is push_bit . lift_definition drop_bit_uint :: \nat \ uint \ uint\ is drop_bit . lift_definition signed_drop_bit_uint :: \nat \ uint \ uint\ is signed_drop_bit . lift_definition take_bit_uint :: \nat \ uint \ uint\ is take_bit . lift_definition set_bit_uint :: \nat \ uint \ uint\ is Bit_Operations.set_bit . lift_definition unset_bit_uint :: \nat \ uint \ uint\ is unset_bit . lift_definition flip_bit_uint :: \nat \ uint \ uint\ is flip_bit . global_interpretation uint: word_type_copy_bits Abs_uint Rep_uint signed_drop_bit_uint by standard (fact bit_uint.rep_eq not_uint.rep_eq and_uint.rep_eq or_uint.rep_eq xor_uint.rep_eq mask_uint.rep_eq push_bit_uint.rep_eq drop_bit_uint.rep_eq signed_drop_bit_uint.rep_eq take_bit_uint.rep_eq set_bit_uint.rep_eq unset_bit_uint.rep_eq flip_bit_uint.rep_eq)+ instance by (fact uint.of_class_ring_bit_operations) end lift_definition uint_of_nat :: \nat \ uint\ is word_of_nat . lift_definition nat_of_uint :: \uint \ nat\ is unat . lift_definition uint_of_int :: \int \ uint\ is word_of_int . lift_definition int_of_uint :: \uint \ int\ is uint . context includes integer.lifting begin lift_definition Uint :: \integer \ uint\ is word_of_int . lift_definition integer_of_uint :: \uint \ integer\ is uint . end global_interpretation uint: word_type_copy_more Abs_uint Rep_uint signed_drop_bit_uint uint_of_nat nat_of_uint uint_of_int int_of_uint Uint integer_of_uint apply standard apply (simp_all add: uint_of_nat.rep_eq nat_of_uint.rep_eq uint_of_int.rep_eq int_of_uint.rep_eq Uint.rep_eq integer_of_uint.rep_eq integer_eq_iff) done instantiation uint :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint :: \uint \ nat\ is size . lift_definition msb_uint :: \uint \ bool\ is msb . lift_definition lsb_uint :: \uint \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint :: \uint \ nat \ bool \ uint\ where set_bit_uint_eq: \set_bit_uint a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint_transfer [transfer_rule]: \(cr_uint ===> (=) ===> (\) ===> cr_uint) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint_eq [abs_def]) transfer_prover end lift_definition set_bits_uint :: \(nat \ bool) \ uint\ is set_bits . lift_definition set_bits_aux_uint :: \(nat \ bool) \ nat \ uint \ uint\ is set_bits_aux . global_interpretation uint: word_type_copy_misc Abs_uint Rep_uint signed_drop_bit_uint uint_of_nat nat_of_uint uint_of_int int_of_uint Uint integer_of_uint dflt_size set_bits_aux_uint by (standard; transfer) simp_all instance using uint.of_class_bit_comprehension uint.of_class_set_bit uint.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint \ (SML) \ structure Uint : sig val set_bit : Word.word -> IntInf.int -> bool -> Word.word val shiftl : Word.word -> IntInf.int -> Word.word val shiftr : Word.word -> IntInf.int -> Word.word val shiftr_signed : Word.word -> IntInf.int -> Word.word val test_bit : Word.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word.orb (x, mask) else Word.andb (x, Word.notb mask) end fun shiftl x n = Word.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0 end; (* struct Uint *)\ code_reserved SML Uint code_printing code_module Uint \ (Haskell) \module Uint(Int, Word, dflt_size) where import qualified Prelude import Data.Int(Int) import Data.Word(Word) import qualified Data.Bits dflt_size :: Prelude.Integer dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int bitSize_aux = Data.Bits.bitSize\ and (Haskell_Quickcheck) \module Uint(Int, Word, dflt_size) where import qualified Prelude import Data.Int(Int) import Data.Word(Word) import qualified Data.Bits dflt_size :: Prelude.Int dflt_size = bitSize_aux (0::Word) where bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int bitSize_aux = Data.Bits.bitSize \ code_reserved Haskell Uint dflt_size text \ OCaml and Scala provide only signed bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint" \ (OCaml) \module Uint : sig type t = int val dflt_size : Z.t val less : t -> t -> bool val less_eq : t -> t -> bool val set_bit : t -> Z.t -> bool -> t val shiftl : t -> Z.t -> t val shiftr : t -> Z.t -> t val shiftr_signed : t -> Z.t -> t val test_bit : t -> Z.t -> bool val int_mask : int val int32_mask : int32 val int64_mask : int64 end = struct type t = int let dflt_size = Z.of_int Sys.int_size;; (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if x<0 then y<0 && x 0;; let int_mask = if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;; let int32_mask = if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size) else Int32.of_string "0xFFFFFFFF";; let int64_mask = if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size) else Int64.of_string "0xFFFFFFFFFFFFFFFF";; end;; (*struct Uint*)\ code_reserved OCaml Uint code_printing code_module Uint \ (Scala) \object Uint { def dflt_size : BigInt = BigInt(32) def less(x: Int, y: Int) : Boolean = - if (x < 0) y < 0 && x < y - else y < 0 || x < y + x < 0 match { + case true => y < 0 && x < y + case false => y < 0 || x < y + } def less_eq(x: Int, y: Int) : Boolean = - if (x < 0) y < 0 && x <= y - else y < 0 || x <= y + x < 0 match { + case true => y < 0 && x <= y + case false => y < 0 || x <= y + } def set_bit(x: Int, n: BigInt, b: Boolean) : Int = - if (b) - x | (1 << n.intValue) - else - x & (1 << n.intValue).unary_~ + b match { + case true => x | (1 << n.intValue) + case false => x & (1 << n.intValue).unary_~ + } def shiftl(x: Int, n: BigInt) : Int = x << n.intValue def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue def test_bit(x: Int, n: BigInt) : Boolean = (x & (1 << n.intValue)) != 0 } /* object Uint */\ code_reserved Scala Uint text \ OCaml's conversion from Big\_int to int demands that the value fits into a signed integer. The following justifies the implementation. \ context includes integer.lifting bit_operations_syntax begin definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1" lift_definition wivs_mask_integer :: integer is wivs_mask . lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1" by transfer (simp add: wivs_mask_def) definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size" lift_definition wivs_shift_integer :: integer is wivs_shift . lemma [code]: "wivs_shift_integer = 2 ^ dflt_size" by transfer (simp add: wivs_shift_def) definition wivs_index :: nat where "wivs_index == dflt_size - 1" lift_definition wivs_index_integer :: integer is "int wivs_index". lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1" by transfer (simp add: wivs_index_def of_nat_diff) definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)" lift_definition wivs_overflow_integer :: integer is wivs_overflow . lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)" by transfer (simp add: wivs_overflow_def) definition wivs_least :: int where "wivs_least == - wivs_overflow" lift_definition wivs_least_integer :: integer is wivs_least . lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))" by transfer (simp add: wivs_overflow_def wivs_least_def) definition Uint_signed :: "integer \ uint" where "Uint_signed i = (if i < wivs_least_integer \ wivs_overflow_integer \ i then undefined Uint i else Uint i)" lemma Uint_code [code]: "Uint i = (let i' = i AND wivs_mask_integer in if bit i' wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')" including undefined_transfer unfolding Uint_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed wivs_mask_def wivs_index_def wivs_overflow_def wivs_least_def wivs_shift_def) done lemma Uint_signed_code [code]: "Rep_uint (Uint_signed i) = (if i < wivs_least_integer \ i \ wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))" unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def by(simp add: Abs_uint_inverse) end text \ Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead. The symbolic implementations for code\_simp use @{term Rep_uint}. The new destructor @{term Rep_uint'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint} ([code abstract] equations for @{typ uint} may use @{term Rep_uint} because these instances will be folded away.) \ definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint" lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. bit x n)" unfolding Rep_uint'_def by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint' :: "dflt_size word \ uint" is "\x :: dflt_size word. x" . lemma Abs_uint'_code [code]: "Abs_uint' x = Uint (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint \ _"]] lemma term_of_uint_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []])) (term_of_class.term_of (Rep_uint' x))" by(simp add: term_of_anything) text \Important: We must prevent the reflection oracle (eval-tac) to use our machine-dependent type. \ code_printing type_constructor uint \ (SML) "Word.word" and (Haskell) "Uint.Word" and (OCaml) "Uint.t" and (Scala) "Int" and (Eval) "*** \"Error: Machine dependent type\" ***" and (Quickcheck) "Word.word" | constant dflt_size_integer \ (SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.wordSize" and (Haskell) "Uint.dflt'_size" and (OCaml) "Uint.dflt'_size" and (Scala) "Uint.dflt'_size" | constant Uint \ (SML) "Word.fromLargeInt (IntInf.toLarge _)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and (Scala) "_.intValue" | constant Uint_signed \ (OCaml) "Z.to'_int" | constant "0 :: uint" \ (SML) "(Word.fromInt 0)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "(Word.fromInt 0)" and (Haskell) "(0 :: Uint.Word)" and (OCaml) "0" and (Scala) "0" | constant "1 :: uint" \ (SML) "(Word.fromInt 1)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "(Word.fromInt 1)" and (Haskell) "(1 :: Uint.Word)" and (OCaml) "1" and (Scala) "1" | constant "plus :: uint \ _ " \ (SML) "Word.+ ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.+ ((_), (_))" and (Haskell) infixl 6 "+" and (OCaml) "Pervasives.(+)" and (Scala) infixl 7 "+" | constant "uminus :: uint \ _" \ (SML) "Word.~" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.~" and (Haskell) "negate" and (OCaml) "Pervasives.(~-)" and (Scala) "!(- _)" | constant "minus :: uint \ _" \ (SML) "Word.- ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.- ((_), (_))" and (Haskell) infixl 6 "-" and (OCaml) "Pervasives.(-)" and (Scala) infixl 7 "-" | constant "times :: uint \ _ \ _" \ (SML) "Word.* ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.* ((_), (_))" and (Haskell) infixl 7 "*" and (OCaml) "Pervasives.( * )" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint \ _ \ bool" \ (SML) "!((_ : Word.word) = _)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "!((_ : Word.word) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and (Scala) infixl 5 "==" | class_instance uint :: equal \ (Haskell) - | constant "less_eq :: uint \ _ \ bool" \ (SML) "Word.<= ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.<= ((_), (_))" and (Haskell) infix 4 "<=" and (OCaml) "Uint.less'_eq" and (Scala) "Uint.less'_eq" | constant "less :: uint \ _ \ bool" \ (SML) "Word.< ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.< ((_), (_))" and (Haskell) infix 4 "<" and (OCaml) "Uint.less" and (Scala) "Uint.less" | constant "Bit_Operations.not :: uint \ _" \ (SML) "Word.notb" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Pervasives.lnot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint \ _" \ (SML) "Word.andb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Pervasives.(land)" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint \ _" \ (SML) "Word.orb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Pervasives.(lor)" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint \ _" \ (SML) "Word.xorb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (OCaml) "Pervasives.(lxor)" and (Scala) infixl 2 "^" definition uint_divmod :: "uint \ uint \ uint \ uint" where "uint_divmod x y = (if y = 0 then (undefined ((div) :: uint \ _) x (0 :: uint), undefined ((mod) :: uint \ _) x (0 :: uint)) else (x div y, x mod y))" definition uint_div :: "uint \ uint \ uint" where "uint_div x y = fst (uint_divmod x y)" definition uint_mod :: "uint \ uint \ uint" where "uint_mod x y = snd (uint_divmod x y)" lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)" including undefined_transfer unfolding uint_divmod_def uint_div_def by transfer(simp add: word_div_def) lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)" including undefined_transfer unfolding uint_mod_def uint_divmod_def by transfer(simp add: word_mod_def) definition uint_sdiv :: "uint \ uint \ uint" where [code del]: "uint_sdiv x y = (if y = 0 then undefined ((div) :: uint \ _) x (0 :: uint) else Abs_uint (Rep_uint x sdiv Rep_uint y))" definition div0_uint :: "uint \ uint" where [code del]: "div0_uint x = undefined ((div) :: uint \ _) x (0 :: uint)" declare [[code abort: div0_uint]] definition mod0_uint :: "uint \ uint" where [code del]: "mod0_uint x = undefined ((mod) :: uint \ _) x (0 :: uint)" declare [[code abort: mod0_uint]] definition wivs_overflow_uint :: uint where "wivs_overflow_uint \ push_bit (dflt_size - 1) 1" lemma Rep_uint_wivs_overflow_uint_eq: \Rep_uint wivs_overflow_uint = 2 ^ (dflt_size - Suc 0)\ by (simp add: wivs_overflow_uint_def one_uint.rep_eq push_bit_uint.rep_eq uint.word_of_power push_bit_eq_mult) lemma wivs_overflow_uint_greater_eq_0: \wivs_overflow_uint > 0\ apply (simp add: less_uint.rep_eq zero_uint.rep_eq Rep_uint_wivs_overflow_uint_eq) apply transfer apply (simp add: take_bit_push_bit push_bit_eq_mult) done lemma uint_divmod_code [code]: "uint_divmod x y = (if wivs_overflow_uint \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint x, mod0_uint x) else let q = push_bit 1 (uint_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" proof (cases \y = 0\) case True moreover have \x \ 0\ by transfer simp moreover note wivs_overflow_uint_greater_eq_0 ultimately show ?thesis by (auto simp add: uint_divmod_def div0_uint_def mod0_uint_def not_less) next case False then show ?thesis including undefined_transfer unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def wivs_overflow_uint_def apply transfer apply (simp add: divmod_via_sdivmod push_bit_of_1) done qed lemma uint_sdiv_code [code]: "Rep_uint (uint_sdiv x y) = (if y = 0 then Rep_uint (undefined ((div) :: uint \ _) x (0 :: uint)) else Rep_uint x sdiv Rep_uint y)" unfolding uint_sdiv_def by(simp add: Abs_uint_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint_divmod_code} computes both with division only. \ code_printing constant uint_div \ (SML) "Word.div ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.div ((_), (_))" and (Haskell) "Prelude.div" | constant uint_mod \ (SML) "Word.mod ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.mod ((_), (_))" and (Haskell) "Prelude.mod" | constant uint_divmod \ (Haskell) "divmod" | constant uint_sdiv \ (OCaml) "Pervasives.('/)" and (Scala) "_ '/ _" definition uint_test_bit :: "uint \ integer \ bool" where [code del]: "uint_test_bit x n = (if n < 0 \ dflt_size_integer \ n then undefined (bit :: uint \ _) x n else bit x (nat_of_integer n))" lemma test_bit_uint_code [code]: "bit x n \ n < dflt_size \ uint_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint_test_bit_def by (transfer, simp, transfer, simp) lemma uint_test_bit_code [code]: "uint_test_bit w n = (if n < 0 \ dflt_size_integer \ n then undefined (bit :: uint \ _) w n else bit (Rep_uint w) (nat_of_integer n))" unfolding uint_test_bit_def by(simp add: bit_uint.rep_eq) code_printing constant uint_test_bit \ (SML) "Uint.test'_bit" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint.test'_bit" and (Scala) "Uint.test'_bit" definition uint_set_bit :: "uint \ integer \ bool \ uint" where [code del]: "uint_set_bit x n b = (if n < 0 \ dflt_size_integer \ n then undefined (set_bit :: uint \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint_code [code]: "set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint_set_bit_def by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint_set_bit_code [code]: "Rep_uint (uint_set_bit w n b) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (set_bit :: uint \ _) w n b) else set_bit (Rep_uint w) (nat_of_integer n) b)" including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp code_printing constant uint_set_bit \ (SML) "Uint.set'_bit" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint.set'_bit" and (Scala) "Uint.set'_bit" definition uint_shiftl :: "uint \ integer \ uint" where [code del]: "uint_shiftl x n = (if n < 0 \ dflt_size_integer \ n then undefined (push_bit :: nat \ uint \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint_code [code]: "push_bit n x = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint_shiftl_def by (transfer fixing: n) simp lemma uint_shiftl_code [code]: "Rep_uint (uint_shiftl w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (push_bit :: nat \ uint \ _) w n) else push_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp code_printing constant uint_shiftl \ (SML) "Uint.shiftl" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint.shiftl" and (Scala) "Uint.shiftl" definition uint_shiftr :: "uint \ integer \ uint" where [code del]: "uint_shiftr x n = (if n < 0 \ dflt_size_integer \ n then undefined (drop_bit :: nat \ uint \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint_code [code]: "drop_bit n x = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint_shiftr_def by (transfer fixing: n) simp lemma uint_shiftr_code [code]: "Rep_uint (uint_shiftr w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (drop_bit :: nat \ uint \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_shiftr_def by transfer simp code_printing constant uint_shiftr \ (SML) "Uint.shiftr" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint.shiftr" and (Scala) "Uint.shiftr" definition uint_sshiftr :: "uint \ integer \ uint" where [code del]: "uint_sshiftr x n = (if n < 0 \ dflt_size_integer \ n then undefined signed_drop_bit_uint n x else signed_drop_bit_uint (nat_of_integer n) x)" lemma sshiftr_uint_code [code]: "signed_drop_bit_uint n x = (if n < dflt_size then uint_sshiftr x (integer_of_nat n) else if bit x wivs_index then -1 else 0)" including undefined_transfer integer.lifting unfolding uint_sshiftr_def by transfer(simp add: not_less signed_drop_bit_beyond word_size wivs_index_def) lemma uint_sshiftr_code [code]: "Rep_uint (uint_sshiftr w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined signed_drop_bit_uint n w) else signed_drop_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_sshiftr_def by transfer simp code_printing constant uint_sshiftr \ (SML) "Uint.shiftr'_signed" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and (OCaml) "Uint.shiftr'_signed" and (Scala) "Uint.shiftr'_signed" lemma uint_msb_test_bit: "msb x \ bit (x :: uint) wivs_index" by transfer (simp add: msb_word_iff_bit wivs_index_def) lemma msb_uint_code [code]: "msb x \ uint_test_bit x wivs_index_integer" apply(simp add: uint_test_bit_def uint_msb_test_bit wivs_index_integer_code dflt_size_integer_def wivs_index_def) by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0 nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def) lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. bit i n)" by transfer (simp add: word_of_int_conv_set_bits) section \Quickcheck setup\ definition uint_of_natural :: "natural \ uint" where "uint_of_natural x \ Uint (integer_of_natural x)" instantiation uint :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint \ qc_random_cnv uint_of_natural" definition "exhaustive_uint \ qc_exhaustive_cnv uint_of_natural" definition "full_exhaustive_uint \ qc_full_exhaustive_cnv uint_of_natural" instance .. end instantiation uint :: narrowing begin interpretation quickcheck_narrowing_samples "\i. (Uint i, Uint (- i))" "0" "Typerep.Typerep (STR ''Uint.uint'') []" . definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint itself \ _"]] lemmas partial_term_of_uint [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint16.thy b/thys/Native_Word/Uint16.thy --- a/thys/Native_Word/Uint16.thy +++ b/thys/Native_Word/Uint16.thy @@ -1,537 +1,537 @@ (* Title: Uint16.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 16 bits\ theory Uint16 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ Restriction for ML code generation: This theory assumes that the ML system provides a Word16 implementation (mlton does, but PolyML 5.5 does not). Therefore, the code setup lives in the target \SML_word\ rather than \SML\. This ensures that code generation still works as long as \uint16\ is not involved. For the target \SML\ itself, no special code generation for this type is set up. Nevertheless, it should work by emulation via \<^typ>\16 word\ if the theory \<^text>\Code_Target_Int_Bit\ is imported. Restriction for OCaml code generation: OCaml does not provide an int16 type, so no special code generation for this type is set up. \ section \Type definition and primitive operations\ typedef uint16 = \UNIV :: 16 word set\ .. global_interpretation uint16: word_type_copy Abs_uint16 Rep_uint16 using type_definition_uint16 by (rule word_type_copy.intro) setup_lifting type_definition_uint16 declare uint16.of_word_of [code abstype] declare Quotient_uint16 [transfer_rule] instantiation uint16 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint16 :: uint16 is 0 . lift_definition one_uint16 :: uint16 is 1 . lift_definition plus_uint16 :: \uint16 \ uint16 \ uint16\ is \(+)\ . lift_definition uminus_uint16 :: \uint16 \ uint16\ is uminus . lift_definition minus_uint16 :: \uint16 \ uint16 \ uint16\ is \(-)\ . lift_definition times_uint16 :: \uint16 \ uint16 \ uint16\ is \(*)\ . lift_definition divide_uint16 :: \uint16 \ uint16 \ uint16\ is \(div)\ . lift_definition modulo_uint16 :: \uint16 \ uint16 \ uint16\ is \(mod)\ . lift_definition equal_uint16 :: \uint16 \ uint16 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint16 :: \uint16 \ uint16 \ bool\ is \(\)\ . lift_definition less_uint16 :: \uint16 \ uint16 \ bool\ is \(<)\ . global_interpretation uint16: word_type_copy_ring Abs_uint16 Rep_uint16 by standard (fact zero_uint16.rep_eq one_uint16.rep_eq plus_uint16.rep_eq uminus_uint16.rep_eq minus_uint16.rep_eq times_uint16.rep_eq divide_uint16.rep_eq modulo_uint16.rep_eq equal_uint16.rep_eq less_eq_uint16.rep_eq less_uint16.rep_eq)+ instance proof - show \OFCLASS(uint16, comm_ring_1_class)\ by (rule uint16.of_class_comm_ring_1) show \OFCLASS(uint16, semiring_modulo_class)\ by (fact uint16.of_class_semiring_modulo) show \OFCLASS(uint16, equal_class)\ by (fact uint16.of_class_equal) show \OFCLASS(uint16, linorder_class)\ by (fact uint16.of_class_linorder) qed end instantiation uint16 :: ring_bit_operations begin lift_definition bit_uint16 :: \uint16 \ nat \ bool\ is bit . lift_definition not_uint16 :: \uint16 \ uint16\ is \Bit_Operations.not\ . lift_definition and_uint16 :: \uint16 \ uint16 \ uint16\ is \Bit_Operations.and\ . lift_definition or_uint16 :: \uint16 \ uint16 \ uint16\ is \Bit_Operations.or\ . lift_definition xor_uint16 :: \uint16 \ uint16 \ uint16\ is \Bit_Operations.xor\ . lift_definition mask_uint16 :: \nat \ uint16\ is mask . lift_definition push_bit_uint16 :: \nat \ uint16 \ uint16\ is push_bit . lift_definition drop_bit_uint16 :: \nat \ uint16 \ uint16\ is drop_bit . lift_definition signed_drop_bit_uint16 :: \nat \ uint16 \ uint16\ is signed_drop_bit . lift_definition take_bit_uint16 :: \nat \ uint16 \ uint16\ is take_bit . lift_definition set_bit_uint16 :: \nat \ uint16 \ uint16\ is Bit_Operations.set_bit . lift_definition unset_bit_uint16 :: \nat \ uint16 \ uint16\ is unset_bit . lift_definition flip_bit_uint16 :: \nat \ uint16 \ uint16\ is flip_bit . global_interpretation uint16: word_type_copy_bits Abs_uint16 Rep_uint16 signed_drop_bit_uint16 by standard (fact bit_uint16.rep_eq not_uint16.rep_eq and_uint16.rep_eq or_uint16.rep_eq xor_uint16.rep_eq mask_uint16.rep_eq push_bit_uint16.rep_eq drop_bit_uint16.rep_eq signed_drop_bit_uint16.rep_eq take_bit_uint16.rep_eq set_bit_uint16.rep_eq unset_bit_uint16.rep_eq flip_bit_uint16.rep_eq)+ instance by (fact uint16.of_class_ring_bit_operations) end lift_definition uint16_of_nat :: \nat \ uint16\ is word_of_nat . lift_definition nat_of_uint16 :: \uint16 \ nat\ is unat . lift_definition uint16_of_int :: \int \ uint16\ is word_of_int . lift_definition int_of_uint16 :: \uint16 \ int\ is uint . context includes integer.lifting begin lift_definition Uint16 :: \integer \ uint16\ is word_of_int . lift_definition integer_of_uint16 :: \uint16 \ integer\ is uint . end global_interpretation uint16: word_type_copy_more Abs_uint16 Rep_uint16 signed_drop_bit_uint16 uint16_of_nat nat_of_uint16 uint16_of_int int_of_uint16 Uint16 integer_of_uint16 apply standard apply (simp_all add: uint16_of_nat.rep_eq nat_of_uint16.rep_eq uint16_of_int.rep_eq int_of_uint16.rep_eq Uint16.rep_eq integer_of_uint16.rep_eq integer_eq_iff) done instantiation uint16 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint16 :: \uint16 \ nat\ is size . lift_definition msb_uint16 :: \uint16 \ bool\ is msb . lift_definition lsb_uint16 :: \uint16 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint16 :: \uint16 \ nat \ bool \ uint16\ where set_bit_uint16_eq: \set_bit_uint16 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint16_transfer [transfer_rule]: \(cr_uint16 ===> (=) ===> (\) ===> cr_uint16) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint16_eq [abs_def]) transfer_prover end lift_definition set_bits_uint16 :: \(nat \ bool) \ uint16\ is set_bits . lift_definition set_bits_aux_uint16 :: \(nat \ bool) \ nat \ uint16 \ uint16\ is set_bits_aux . global_interpretation uint16: word_type_copy_misc Abs_uint16 Rep_uint16 signed_drop_bit_uint16 uint16_of_nat nat_of_uint16 uint16_of_int int_of_uint16 Uint16 integer_of_uint16 16 set_bits_aux_uint16 by (standard; transfer) simp_all instance using uint16.of_class_bit_comprehension uint16.of_class_set_bit uint16.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint16 \ (SML_word) \(* Test that words can handle numbers between 0 and 15 *) val _ = if 4 <= Word.wordSize then () else raise (Fail ("wordSize less than 4")); structure Uint16 : sig val set_bit : Word16.word -> IntInf.int -> bool -> Word16.word val shiftl : Word16.word -> IntInf.int -> Word16.word val shiftr : Word16.word -> IntInf.int -> Word16.word val shiftr_signed : Word16.word -> IntInf.int -> Word16.word val test_bit : Word16.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word16.orb (x, mask) else Word16.andb (x, Word16.notb mask) end fun shiftl x n = Word16.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word16.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word16.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word16.andb (x, Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word16.fromInt 0 end; (* struct Uint16 *)\ code_reserved SML_word Uint16 code_printing code_module Uint16 \ (Haskell) \module Uint16(Int16, Word16) where import Data.Int(Int16) import Data.Word(Word16)\ code_reserved Haskell Uint16 text \Scala provides unsigned 16-bit numbers as Char.\ code_printing code_module Uint16 \ (Scala) \object Uint16 { def set_bit(x: scala.Char, n: BigInt, b: Boolean) : scala.Char = - if (b) - (x | (1.toChar << n.intValue)).toChar - else - (x & (1.toChar << n.intValue).unary_~).toChar + b match { + case true => (x | (1.toChar << n.intValue)).toChar + case false => (x & (1.toChar << n.intValue).unary_~).toChar + } def shiftl(x: scala.Char, n: BigInt) : scala.Char = (x << n.intValue).toChar def shiftr(x: scala.Char, n: BigInt) : scala.Char = (x >>> n.intValue).toChar def shiftr_signed(x: scala.Char, n: BigInt) : scala.Char = (x.toShort >> n.intValue).toChar def test_bit(x: scala.Char, n: BigInt) : Boolean = (x & (1.toChar << n.intValue)) != 0 } /* object Uint16 */\ code_reserved Scala Uint16 text \ Avoid @{term Abs_uint16} in generated code, use @{term Rep_uint16'} instead. The symbolic implementations for code\_simp use @{term Rep_uint16}. The new destructor @{term Rep_uint16'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint16} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint16} ([code abstract] equations for @{typ uint16} may use @{term Rep_uint16} because these instances will be folded away.) To convert @{typ "16 word"} values into @{typ uint16}, use @{term "Abs_uint16'"}. \ definition Rep_uint16' where [simp]: "Rep_uint16' = Rep_uint16" lemma Rep_uint16'_transfer [transfer_rule]: "rel_fun cr_uint16 (=) (\x. x) Rep_uint16'" unfolding Rep_uint16'_def by(rule uint16.rep_transfer) lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint16' :: "16 word \ uint16" is "\x :: 16 word. x" . lemma Abs_uint16'_code [code]: "Abs_uint16' x = Uint16 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint16 \ _"]] lemma term_of_uint16_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint16.uint16.Abs_uint16'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]], TR (STR ''Uint16.uint16'') []])) (term_of_class.term_of (Rep_uint16' x))" by(simp add: term_of_anything) lemma Uint16_code [code]: "Rep_uint16 (Uint16 i) = word_of_int (int_of_integer_symbolic i)" unfolding Uint16_def int_of_integer_symbolic_def by(simp add: Abs_uint16_inverse) code_printing type_constructor uint16 \ (SML_word) "Word16.word" and (Haskell) "Uint16.Word16" and (Scala) "scala.Char" | constant Uint16 \ (SML_word) "Word16.fromLargeInt (IntInf.toLarge _)" and (Haskell) "(Prelude.fromInteger _ :: Uint16.Word16)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Word16)" and (Scala) "_.charValue" | constant "0 :: uint16" \ (SML_word) "(Word16.fromInt 0)" and (Haskell) "(0 :: Uint16.Word16)" and (Scala) "0" | constant "1 :: uint16" \ (SML_word) "(Word16.fromInt 1)" and (Haskell) "(1 :: Uint16.Word16)" and (Scala) "1" | constant "plus :: uint16 \ _ \ _" \ (SML_word) "Word16.+ ((_), (_))" and (Haskell) infixl 6 "+" and (Scala) "(_ +/ _).toChar" | constant "uminus :: uint16 \ _" \ (SML_word) "Word16.~" and (Haskell) "negate" and (Scala) "(- _).toChar" | constant "minus :: uint16 \ _" \ (SML_word) "Word16.- ((_), (_))" and (Haskell) infixl 6 "-" and (Scala) "(_ -/ _).toChar" | constant "times :: uint16 \ _ \ _" \ (SML_word) "Word16.* ((_), (_))" and (Haskell) infixl 7 "*" and (Scala) "(_ */ _).toChar" | constant "HOL.equal :: uint16 \ _ \ bool" \ (SML_word) "!((_ : Word16.word) = _)" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" | class_instance uint16 :: equal \ (Haskell) - | constant "less_eq :: uint16 \ _ \ bool" \ (SML_word) "Word16.<= ((_), (_))" and (Haskell) infix 4 "<=" and (Scala) infixl 4 "<=" | constant "less :: uint16 \ _ \ bool" \ (SML_word) "Word16.< ((_), (_))" and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" | constant "Bit_Operations.not :: uint16 \ _" \ (SML_word) "Word16.notb" and (Haskell) "Data'_Bits.complement" and (Scala) "_.unary'_~.toChar" | constant "Bit_Operations.and :: uint16 \ _" \ (SML_word) "Word16.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (Scala) "(_ & _).toChar" | constant "Bit_Operations.or :: uint16 \ _" \ (SML_word) "Word16.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (Scala) "(_ | _).toChar" | constant "Bit_Operations.xor :: uint16 \ _" \ (SML_word) "Word16.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (Scala) "(_ ^ _).toChar" definition uint16_div :: "uint16 \ uint16 \ uint16" where "uint16_div x y = (if y = 0 then undefined ((div) :: uint16 \ _) x (0 :: uint16) else x div y)" definition uint16_mod :: "uint16 \ uint16 \ uint16" where "uint16_mod x y = (if y = 0 then undefined ((mod) :: uint16 \ _) x (0 :: uint16) else x mod y)" context includes undefined_transfer begin lemma div_uint16_code [code]: "x div y = (if y = 0 then 0 else uint16_div x y)" unfolding uint16_div_def by transfer (simp add: word_div_def) lemma mod_uint16_code [code]: "x mod y = (if y = 0 then x else uint16_mod x y)" unfolding uint16_mod_def by transfer (simp add: word_mod_def) lemma uint16_div_code [code]: "Rep_uint16 (uint16_div x y) = (if y = 0 then Rep_uint16 (undefined ((div) :: uint16 \ _) x (0 :: uint16)) else Rep_uint16 x div Rep_uint16 y)" unfolding uint16_div_def by transfer simp lemma uint16_mod_code [code]: "Rep_uint16 (uint16_mod x y) = (if y = 0 then Rep_uint16 (undefined ((mod) :: uint16 \ _) x (0 :: uint16)) else Rep_uint16 x mod Rep_uint16 y)" unfolding uint16_mod_def by transfer simp end code_printing constant uint16_div \ (SML_word) "Word16.div ((_), (_))" and (Haskell) "Prelude.div" and (Scala) "(_ '/ _).toChar" | constant uint16_mod \ (SML_word) "Word16.mod ((_), (_))" and (Haskell) "Prelude.mod" and (Scala) "(_ % _).toChar" definition uint16_test_bit :: "uint16 \ integer \ bool" where [code del]: "uint16_test_bit x n = (if n < 0 \ 15 < n then undefined (bit :: uint16 \ _) x n else bit x (nat_of_integer n))" lemma test_bit_uint16_code [code]: "bit x n \ n < 16 \ uint16_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint16_test_bit_def by (transfer, simp, transfer, simp) lemma uint16_test_bit_code [code]: "uint16_test_bit w n = (if n < 0 \ 15 < n then undefined (bit :: uint16 \ _) w n else bit (Rep_uint16 w) (nat_of_integer n))" unfolding uint16_test_bit_def by (simp add: bit_uint16.rep_eq) code_printing constant uint16_test_bit \ (SML_word) "Uint16.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (Scala) "Uint16.test'_bit" definition uint16_set_bit :: "uint16 \ integer \ bool \ uint16" where [code del]: "uint16_set_bit x n b = (if n < 0 \ 15 < n then undefined (set_bit :: uint16 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint16_code [code]: "set_bit x n b = (if n < 16 then uint16_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint16_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint16_set_bit_code [code]: "Rep_uint16 (uint16_set_bit w n b) = (if n < 0 \ 15 < n then Rep_uint16 (undefined (set_bit :: uint16 \ _) w n b) else set_bit (Rep_uint16 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint16_set_bit_def by transfer simp code_printing constant uint16_set_bit \ (SML_word) "Uint16.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (Scala) "Uint16.set'_bit" definition uint16_shiftl :: "uint16 \ integer \ uint16" where [code del]: "uint16_shiftl x n = (if n < 0 \ 16 \ n then undefined (push_bit :: nat \ uint16 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint16_code [code]: "push_bit n x = (if n < 16 then uint16_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint16_shiftl_def by transfer simp lemma uint16_shiftl_code [code]: "Rep_uint16 (uint16_shiftl w n) = (if n < 0 \ 16 \ n then Rep_uint16 (undefined (push_bit :: nat \ uint16 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint16 w))" including undefined_transfer unfolding uint16_shiftl_def by transfer simp code_printing constant uint16_shiftl \ (SML_word) "Uint16.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (Scala) "Uint16.shiftl" definition uint16_shiftr :: "uint16 \ integer \ uint16" where [code del]: "uint16_shiftr x n = (if n < 0 \ 16 \ n then undefined (drop_bit :: nat \ uint16 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint16_code [code]: "drop_bit n x = (if n < 16 then uint16_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint16_shiftr_def by transfer simp lemma uint16_shiftr_code [code]: "Rep_uint16 (uint16_shiftr w n) = (if n < 0 \ 16 \ n then Rep_uint16 (undefined (drop_bit :: nat \ uint16 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint16 w))" including undefined_transfer unfolding uint16_shiftr_def by transfer simp code_printing constant uint16_shiftr \ (SML_word) "Uint16.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (Scala) "Uint16.shiftr" definition uint16_sshiftr :: "uint16 \ integer \ uint16" where [code del]: "uint16_sshiftr x n = (if n < 0 \ 16 \ n then undefined signed_drop_bit_uint16 n x else signed_drop_bit_uint16 (nat_of_integer n) x)" lemma sshiftr_uint16_code [code]: "signed_drop_bit_uint16 n x = (if n < 16 then uint16_sshiftr x (integer_of_nat n) else if bit x 15 then -1 else 0)" including undefined_transfer integer.lifting unfolding uint16_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond word_size) lemma uint16_sshiftr_code [code]: "Rep_uint16 (uint16_sshiftr w n) = (if n < 0 \ 16 \ n then Rep_uint16 (undefined signed_drop_bit_uint16 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint16 w))" including undefined_transfer unfolding uint16_sshiftr_def by transfer simp code_printing constant uint16_sshiftr \ (SML_word) "Uint16.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Int16) _)) :: Uint16.Word16)" and (Scala) "Uint16.shiftr'_signed" lemma uint16_msb_test_bit: "msb x \ bit (x :: uint16) 15" by transfer (simp add: msb_word_iff_bit) lemma msb_uint16_code [code]: "msb x \ uint16_test_bit x 15" by (simp add: uint16_test_bit_def uint16_msb_test_bit) lemma uint16_of_int_code [code]: "uint16_of_int i = Uint16 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint16_code [code]: "int_of_uint16 x = int_of_integer (integer_of_uint16 x)" by (simp add: int_of_uint16.rep_eq integer_of_uint16_def) lemma uint16_of_nat_code [code]: "uint16_of_nat = uint16_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint16_code [code]: "nat_of_uint16 x = nat_of_integer (integer_of_uint16 x)" unfolding integer_of_uint16_def including integer.lifting by transfer simp lemma integer_of_uint16_code [code]: "integer_of_uint16 n = integer_of_int (uint (Rep_uint16' n))" unfolding integer_of_uint16_def by transfer auto code_printing constant "integer_of_uint16" \ (SML_word) "Word16.toInt _ : IntInf.int" and (Haskell) "Prelude.toInteger" and (Scala) "BigInt" section \Quickcheck setup\ definition uint16_of_natural :: "natural \ uint16" where "uint16_of_natural x \ Uint16 (integer_of_natural x)" instantiation uint16 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint16 \ qc_random_cnv uint16_of_natural" definition "exhaustive_uint16 \ qc_exhaustive_cnv uint16_of_natural" definition "full_exhaustive_uint16 \ qc_full_exhaustive_cnv uint16_of_natural" instance .. end instantiation uint16 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint16 i in (x, 0xFFFF - x)" "0" "Typerep.Typerep (STR ''Uint16.uint16'') []" . definition "narrowing_uint16 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint16 itself \ _"]] lemmas partial_term_of_uint16 [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint32.thy b/thys/Native_Word/Uint32.thy --- a/thys/Native_Word/Uint32.thy +++ b/thys/Native_Word/Uint32.thy @@ -1,692 +1,696 @@ (* Title: Uint32.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 32 bits\ theory Uint32 imports Word_Type_Copies Code_Target_Integer_Bit begin section \Type definition and primitive operations\ typedef uint32 = \UNIV :: 32 word set\ .. global_interpretation uint32: word_type_copy Abs_uint32 Rep_uint32 using type_definition_uint32 by (rule word_type_copy.intro) setup_lifting type_definition_uint32 declare uint32.of_word_of [code abstype] declare Quotient_uint32 [transfer_rule] instantiation uint32 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint32 :: uint32 is 0 . lift_definition one_uint32 :: uint32 is 1 . lift_definition plus_uint32 :: \uint32 \ uint32 \ uint32\ is \(+)\ . lift_definition uminus_uint32 :: \uint32 \ uint32\ is uminus . lift_definition minus_uint32 :: \uint32 \ uint32 \ uint32\ is \(-)\ . lift_definition times_uint32 :: \uint32 \ uint32 \ uint32\ is \(*)\ . lift_definition divide_uint32 :: \uint32 \ uint32 \ uint32\ is \(div)\ . lift_definition modulo_uint32 :: \uint32 \ uint32 \ uint32\ is \(mod)\ . lift_definition equal_uint32 :: \uint32 \ uint32 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint32 :: \uint32 \ uint32 \ bool\ is \(\)\ . lift_definition less_uint32 :: \uint32 \ uint32 \ bool\ is \(<)\ . global_interpretation uint32: word_type_copy_ring Abs_uint32 Rep_uint32 by standard (fact zero_uint32.rep_eq one_uint32.rep_eq plus_uint32.rep_eq uminus_uint32.rep_eq minus_uint32.rep_eq times_uint32.rep_eq divide_uint32.rep_eq modulo_uint32.rep_eq equal_uint32.rep_eq less_eq_uint32.rep_eq less_uint32.rep_eq)+ instance proof - show \OFCLASS(uint32, comm_ring_1_class)\ by (rule uint32.of_class_comm_ring_1) show \OFCLASS(uint32, semiring_modulo_class)\ by (fact uint32.of_class_semiring_modulo) show \OFCLASS(uint32, equal_class)\ by (fact uint32.of_class_equal) show \OFCLASS(uint32, linorder_class)\ by (fact uint32.of_class_linorder) qed end instantiation uint32 :: ring_bit_operations begin lift_definition bit_uint32 :: \uint32 \ nat \ bool\ is bit . lift_definition not_uint32 :: \uint32 \ uint32\ is \Bit_Operations.not\ . lift_definition and_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.and\ . lift_definition or_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.or\ . lift_definition xor_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.xor\ . lift_definition mask_uint32 :: \nat \ uint32\ is mask . lift_definition push_bit_uint32 :: \nat \ uint32 \ uint32\ is push_bit . lift_definition drop_bit_uint32 :: \nat \ uint32 \ uint32\ is drop_bit . lift_definition signed_drop_bit_uint32 :: \nat \ uint32 \ uint32\ is signed_drop_bit . lift_definition take_bit_uint32 :: \nat \ uint32 \ uint32\ is take_bit . lift_definition set_bit_uint32 :: \nat \ uint32 \ uint32\ is Bit_Operations.set_bit . lift_definition unset_bit_uint32 :: \nat \ uint32 \ uint32\ is unset_bit . lift_definition flip_bit_uint32 :: \nat \ uint32 \ uint32\ is flip_bit . global_interpretation uint32: word_type_copy_bits Abs_uint32 Rep_uint32 signed_drop_bit_uint32 by standard (fact bit_uint32.rep_eq not_uint32.rep_eq and_uint32.rep_eq or_uint32.rep_eq xor_uint32.rep_eq mask_uint32.rep_eq push_bit_uint32.rep_eq drop_bit_uint32.rep_eq signed_drop_bit_uint32.rep_eq take_bit_uint32.rep_eq set_bit_uint32.rep_eq unset_bit_uint32.rep_eq flip_bit_uint32.rep_eq)+ instance by (fact uint32.of_class_ring_bit_operations) end lift_definition uint32_of_nat :: \nat \ uint32\ is word_of_nat . lift_definition nat_of_uint32 :: \uint32 \ nat\ is unat . lift_definition uint32_of_int :: \int \ uint32\ is word_of_int . lift_definition int_of_uint32 :: \uint32 \ int\ is uint . context includes integer.lifting begin lift_definition Uint32 :: \integer \ uint32\ is word_of_int . lift_definition integer_of_uint32 :: \uint32 \ integer\ is uint . end global_interpretation uint32: word_type_copy_more Abs_uint32 Rep_uint32 signed_drop_bit_uint32 uint32_of_nat nat_of_uint32 uint32_of_int int_of_uint32 Uint32 integer_of_uint32 apply standard apply (simp_all add: uint32_of_nat.rep_eq nat_of_uint32.rep_eq uint32_of_int.rep_eq int_of_uint32.rep_eq Uint32.rep_eq integer_of_uint32.rep_eq integer_eq_iff) done instantiation uint32 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint32 :: \uint32 \ nat\ is size . lift_definition msb_uint32 :: \uint32 \ bool\ is msb . lift_definition lsb_uint32 :: \uint32 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint32 :: \uint32 \ nat \ bool \ uint32\ where set_bit_uint32_eq: \set_bit_uint32 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint32_transfer [transfer_rule]: \(cr_uint32 ===> (=) ===> (\) ===> cr_uint32) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint32_eq [abs_def]) transfer_prover end lift_definition set_bits_uint32 :: \(nat \ bool) \ uint32\ is set_bits . lift_definition set_bits_aux_uint32 :: \(nat \ bool) \ nat \ uint32 \ uint32\ is set_bits_aux . global_interpretation uint32: word_type_copy_misc Abs_uint32 Rep_uint32 signed_drop_bit_uint32 uint32_of_nat nat_of_uint32 uint32_of_int int_of_uint32 Uint32 integer_of_uint32 32 set_bits_aux_uint32 by (standard; transfer) simp_all instance using uint32.of_class_bit_comprehension uint32.of_class_set_bit uint32.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint32 \ (SML) \(* Test that words can handle numbers between 0 and 31 *) val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5")); structure Uint32 : sig val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word val shiftl : Word32.word -> IntInf.int -> Word32.word val shiftr : Word32.word -> IntInf.int -> Word32.word val shiftr_signed : Word32.word -> IntInf.int -> Word32.word val test_bit : Word32.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word32.orb (x, mask) else Word32.andb (x, Word32.notb mask) end fun shiftl x n = Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0 end; (* struct Uint32 *)\ code_reserved SML Uint32 code_printing code_module Uint32 \ (Haskell) \module Uint32(Int32, Word32) where import Data.Int(Int32) import Data.Word(Word32)\ code_reserved Haskell Uint32 text \ OCaml and Scala provide only signed 32bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint32" \ (OCaml) \module Uint32 : sig val less : int32 -> int32 -> bool val less_eq : int32 -> int32 -> bool val set_bit : int32 -> Z.t -> bool -> int32 val shiftl : int32 -> Z.t -> int32 val shiftr : int32 -> Z.t -> int32 val shiftr_signed : int32 -> Z.t -> int32 val test_bit : int32 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int32.compare x Int32.zero < 0 then Int32.compare y Int32.zero < 0 && Int32.compare x y < 0 else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;; let less_eq x y = if Int32.compare x Int32.zero < 0 then Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0 else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;; let set_bit x n b = let mask = Int32.shift_left Int32.one (Z.to_int n) in if b then Int32.logor x mask else Int32.logand x (Int32.lognot mask);; let shiftl x n = Int32.shift_left x (Z.to_int n);; let shiftr x n = Int32.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int32.shift_right x (Z.to_int n);; let test_bit x n = Int32.compare (Int32.logand x (Int32.shift_left Int32.one (Z.to_int n))) Int32.zero <> 0;; end;; (*struct Uint32*)\ code_reserved OCaml Uint32 code_printing code_module Uint32 \ (Scala) \object Uint32 { def less(x: Int, y: Int) : Boolean = - if (x < 0) y < 0 && x < y - else y < 0 || x < y + x < 0 match { + case true => y < 0 && x < y + case false => y < 0 || x < y + } def less_eq(x: Int, y: Int) : Boolean = - if (x < 0) y < 0 && x <= y - else y < 0 || x <= y + x < 0 match { + case true => y < 0 && x <= y + case false => y < 0 || x <= y + } def set_bit(x: Int, n: BigInt, b: Boolean) : Int = - if (b) - x | (1 << n.intValue) - else - x & (1 << n.intValue).unary_~ + b match { + case true => x | (1 << n.intValue) + case false => x & (1 << n.intValue).unary_~ + } def shiftl(x: Int, n: BigInt) : Int = x << n.intValue def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue def test_bit(x: Int, n: BigInt) : Boolean = (x & (1 << n.intValue)) != 0 } /* object Uint32 */\ code_reserved Scala Uint32 text \ OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint32_signed :: "integer \ uint32" where "Uint32_signed i = (if i < -(0x80000000) \ i \ 0x80000000 then undefined Uint32 i else Uint32 i)" lemma Uint32_code [code]: "Uint32 i = (let i' = i AND 0xFFFFFFFF in if bit i' 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')" including undefined_transfer integer.lifting unfolding Uint32_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint32_signed_code [code]: "Rep_uint32 (Uint32_signed i) = (if i < -(0x80000000) \ i \ 0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))" unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def by(simp add: Abs_uint32_inverse) end text \ Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead. The symbolic implementations for code\_simp use @{term Rep_uint32}. The new destructor @{term Rep_uint32'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint32} ([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because these instances will be folded away.) To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}. \ definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32" lemma Rep_uint32'_transfer [transfer_rule]: "rel_fun cr_uint32 (=) (\x. x) Rep_uint32'" unfolding Rep_uint32'_def by(rule uint32.rep_transfer) lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint32' :: "32 word \ uint32" is "\x :: 32 word. x" . lemma Abs_uint32'_code [code]: "Abs_uint32' x = Uint32 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint32 \ _"]] lemma term_of_uint32_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []])) (term_of_class.term_of (Rep_uint32' x))" by(simp add: term_of_anything) code_printing type_constructor uint32 \ (SML) "Word32.word" and (Haskell) "Uint32.Word32" and (OCaml) "int32" and (Scala) "Int" and (Eval) "Word32.word" | constant Uint32 \ (SML) "Word32.fromLargeInt (IntInf.toLarge _)" and (Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and (Scala) "_.intValue" | constant Uint32_signed \ (OCaml) "Z.to'_int32" | constant "0 :: uint32" \ (SML) "(Word32.fromInt 0)" and (Haskell) "(0 :: Uint32.Word32)" and (OCaml) "Int32.zero" and (Scala) "0" | constant "1 :: uint32" \ (SML) "(Word32.fromInt 1)" and (Haskell) "(1 :: Uint32.Word32)" and (OCaml) "Int32.one" and (Scala) "1" | constant "plus :: uint32 \ _ " \ (SML) "Word32.+ ((_), (_))" and (Haskell) infixl 6 "+" and (OCaml) "Int32.add" and (Scala) infixl 7 "+" | constant "uminus :: uint32 \ _" \ (SML) "Word32.~" and (Haskell) "negate" and (OCaml) "Int32.neg" and (Scala) "!(- _)" | constant "minus :: uint32 \ _" \ (SML) "Word32.- ((_), (_))" and (Haskell) infixl 6 "-" and (OCaml) "Int32.sub" and (Scala) infixl 7 "-" | constant "times :: uint32 \ _ \ _" \ (SML) "Word32.* ((_), (_))" and (Haskell) infixl 7 "*" and (OCaml) "Int32.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint32 \ _ \ bool" \ (SML) "!((_ : Word32.word) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int32.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint32 :: equal \ (Haskell) - | constant "less_eq :: uint32 \ _ \ bool" \ (SML) "Word32.<= ((_), (_))" and (Haskell) infix 4 "<=" and (OCaml) "Uint32.less'_eq" and (Scala) "Uint32.less'_eq" | constant "less :: uint32 \ _ \ bool" \ (SML) "Word32.< ((_), (_))" and (Haskell) infix 4 "<" and (OCaml) "Uint32.less" and (Scala) "Uint32.less" | constant "Bit_Operations.not :: uint32 \ _" \ (SML) "Word32.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int32.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint32 \ _" \ (SML) "Word32.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int32.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint32 \ _" \ (SML) "Word32.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int32.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint32 \ _" \ (SML) "Word32.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int32.logxor" and (Scala) infixl 2 "^" definition uint32_divmod :: "uint32 \ uint32 \ uint32 \ uint32" where "uint32_divmod x y = (if y = 0 then (undefined ((div) :: uint32 \ _) x (0 :: uint32), undefined ((mod) :: uint32 \ _) x (0 :: uint32)) else (x div y, x mod y))" definition uint32_div :: "uint32 \ uint32 \ uint32" where "uint32_div x y = fst (uint32_divmod x y)" definition uint32_mod :: "uint32 \ uint32 \ uint32" where "uint32_mod x y = snd (uint32_divmod x y)" lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)" including undefined_transfer unfolding uint32_divmod_def uint32_div_def by transfer (simp add: word_div_def) lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)" including undefined_transfer unfolding uint32_mod_def uint32_divmod_def by transfer (simp add: word_mod_def) definition uint32_sdiv :: "uint32 \ uint32 \ uint32" where [code del]: "uint32_sdiv x y = (if y = 0 then undefined ((div) :: uint32 \ _) x (0 :: uint32) else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))" definition div0_uint32 :: "uint32 \ uint32" where [code del]: "div0_uint32 x = undefined ((div) :: uint32 \ _) x (0 :: uint32)" declare [[code abort: div0_uint32]] definition mod0_uint32 :: "uint32 \ uint32" where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32 \ _) x (0 :: uint32)" declare [[code abort: mod0_uint32]] lemma uint32_divmod_code [code]: "uint32_divmod x y = (if 0x80000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint32 x, mod0_uint32 x) else let q = push_bit 1 (uint32_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def less_eq_uint32.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint32_sdiv_code [code]: "Rep_uint32 (uint32_sdiv x y) = (if y = 0 then Rep_uint32 (undefined ((div) :: uint32 \ _) x (0 :: uint32)) else Rep_uint32 x sdiv Rep_uint32 y)" unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint32_divmod_code} computes both with division only. \ code_printing constant uint32_div \ (SML) "Word32.div ((_), (_))" and (Haskell) "Prelude.div" | constant uint32_mod \ (SML) "Word32.mod ((_), (_))" and (Haskell) "Prelude.mod" | constant uint32_divmod \ (Haskell) "divmod" | constant uint32_sdiv \ (OCaml) "Int32.div" and (Scala) "_ '/ _" definition uint32_test_bit :: "uint32 \ integer \ bool" where [code del]: "uint32_test_bit x n = (if n < 0 \ 31 < n then undefined (bit :: uint32 \ _) x n else bit x (nat_of_integer n))" lemma test_bit_uint32_code [code]: "bit x n \ n < 32 \ uint32_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint32_test_bit_def by (transfer, simp, transfer, simp) lemma uint32_test_bit_code [code]: "uint32_test_bit w n = (if n < 0 \ 31 < n then undefined (bit :: uint32 \ _) w n else bit (Rep_uint32 w) (nat_of_integer n))" unfolding uint32_test_bit_def by(simp add: bit_uint32.rep_eq) code_printing constant uint32_test_bit \ (SML) "Uint32.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint32.test'_bit" and (Scala) "Uint32.test'_bit" and (Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)" definition uint32_set_bit :: "uint32 \ integer \ bool \ uint32" where [code del]: "uint32_set_bit x n b = (if n < 0 \ 31 < n then undefined (set_bit :: uint32 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint32_code [code]: "set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint32_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint32_set_bit_code [code]: "Rep_uint32 (uint32_set_bit w n b) = (if n < 0 \ 31 < n then Rep_uint32 (undefined (set_bit :: uint32 \ _) w n b) else set_bit (Rep_uint32 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint32_set_bit_def by transfer simp code_printing constant uint32_set_bit \ (SML) "Uint32.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint32.set'_bit" and (Scala) "Uint32.set'_bit" and (Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)" definition uint32_shiftl :: "uint32 \ integer \ uint32" where [code del]: "uint32_shiftl x n = (if n < 0 \ 32 \ n then undefined (push_bit :: nat \ uint32 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint32_code [code]: "push_bit n x = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint32_shiftl_def by transfer simp lemma uint32_shiftl_code [code]: "Rep_uint32 (uint32_shiftl w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined (push_bit :: nat \ uint32 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_shiftl_def by transfer simp code_printing constant uint32_shiftl \ (SML) "Uint32.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint32.shiftl" and (Scala) "Uint32.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)" definition uint32_shiftr :: "uint32 \ integer \ uint32" where [code del]: "uint32_shiftr x n = (if n < 0 \ 32 \ n then undefined (drop_bit :: nat \ uint32 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint32_code [code]: "drop_bit n x = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint32_shiftr_def by transfer simp lemma uint32_shiftr_code [code]: "Rep_uint32 (uint32_shiftr w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined (drop_bit :: nat \ uint32 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_shiftr_def by transfer simp code_printing constant uint32_shiftr \ (SML) "Uint32.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint32.shiftr" and (Scala) "Uint32.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)" definition uint32_sshiftr :: "uint32 \ integer \ uint32" where [code del]: "uint32_sshiftr x n = (if n < 0 \ 32 \ n then undefined signed_drop_bit_uint32 n x else signed_drop_bit_uint32 (nat_of_integer n) x)" lemma sshiftr_uint32_code [code]: "signed_drop_bit_uint32 n x = (if n < 32 then uint32_sshiftr x (integer_of_nat n) else if bit x 31 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint32_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint32_sshiftr_code [code]: "Rep_uint32 (uint32_sshiftr w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined signed_drop_bit_uint32 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_sshiftr_def by transfer simp code_printing constant uint32_sshiftr \ (SML) "Uint32.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and (OCaml) "Uint32.shiftr'_signed" and (Scala) "Uint32.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint32_msb_test_bit: "msb x \ bit (x :: uint32) 31" by transfer (simp add: msb_word_iff_bit) lemma msb_uint32_code [code]: "msb x \ uint32_test_bit x 31" by (simp add: uint32_test_bit_def uint32_msb_test_bit) lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint32_code [code]: "int_of_uint32 x = int_of_integer (integer_of_uint32 x)" including integer.lifting by transfer simp lemma uint32_of_nat_code [code]: "uint32_of_nat = uint32_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint32_code [code]: "nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)" unfolding integer_of_uint32_def including integer.lifting by transfer simp definition integer_of_uint32_signed :: "uint32 \ integer" where "integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_uint32 n)" lemma integer_of_uint32_signed_code [code]: "integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))" by (simp add: integer_of_uint32_signed_def integer_of_uint32_def) lemma integer_of_uint32_code [code]: "integer_of_uint32 n = (if bit n 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)" proof - have \integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 = Bit_Operations.set_bit 31 (integer_of_uint32_signed (take_bit 31 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint32 n = Bit_Operations.set_bit 31 (integer_of_uint32 (take_bit 31 n))\ if \bit n 31\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint32 n) m = bit (Bit_Operations.set_bit 31 (integer_of_uint32 (take_bit 31 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint32_signed_def bit_simps) qed end code_printing constant "integer_of_uint32" \ (SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint32_signed" \ (OCaml) "Z.of'_int32" and (Scala) "BigInt" section \Quickcheck setup\ definition uint32_of_natural :: "natural \ uint32" where "uint32_of_natural x \ Uint32 (integer_of_natural x)" instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint32 \ qc_random_cnv uint32_of_natural" definition "exhaustive_uint32 \ qc_exhaustive_cnv uint32_of_natural" definition "full_exhaustive_uint32 \ qc_full_exhaustive_cnv uint32_of_natural" instance .. end instantiation uint32 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint32.uint32'') []" . definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint32 itself \ _"]] lemmas partial_term_of_uint32 [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy --- a/thys/Native_Word/Uint64.thy +++ b/thys/Native_Word/Uint64.thy @@ -1,889 +1,893 @@ (* Title: Uint64.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 64 bits\ theory Uint64 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode. Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations directly to the \verb$Word64$ structure provided by the Standard ML implementations. The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit version which does not suffer from a division bug found in PolyML 5.6. \ section \Type definition and primitive operations\ typedef uint64 = \UNIV :: 64 word set\ .. global_interpretation uint64: word_type_copy Abs_uint64 Rep_uint64 using type_definition_uint64 by (rule word_type_copy.intro) setup_lifting type_definition_uint64 declare uint64.of_word_of [code abstype] declare Quotient_uint64 [transfer_rule] instantiation uint64 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint64 :: uint64 is 0 . lift_definition one_uint64 :: uint64 is 1 . lift_definition plus_uint64 :: \uint64 \ uint64 \ uint64\ is \(+)\ . lift_definition uminus_uint64 :: \uint64 \ uint64\ is uminus . lift_definition minus_uint64 :: \uint64 \ uint64 \ uint64\ is \(-)\ . lift_definition times_uint64 :: \uint64 \ uint64 \ uint64\ is \(*)\ . lift_definition divide_uint64 :: \uint64 \ uint64 \ uint64\ is \(div)\ . lift_definition modulo_uint64 :: \uint64 \ uint64 \ uint64\ is \(mod)\ . lift_definition equal_uint64 :: \uint64 \ uint64 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint64 :: \uint64 \ uint64 \ bool\ is \(\)\ . lift_definition less_uint64 :: \uint64 \ uint64 \ bool\ is \(<)\ . global_interpretation uint64: word_type_copy_ring Abs_uint64 Rep_uint64 by standard (fact zero_uint64.rep_eq one_uint64.rep_eq plus_uint64.rep_eq uminus_uint64.rep_eq minus_uint64.rep_eq times_uint64.rep_eq divide_uint64.rep_eq modulo_uint64.rep_eq equal_uint64.rep_eq less_eq_uint64.rep_eq less_uint64.rep_eq)+ instance proof - show \OFCLASS(uint64, comm_ring_1_class)\ by (rule uint64.of_class_comm_ring_1) show \OFCLASS(uint64, semiring_modulo_class)\ by (fact uint64.of_class_semiring_modulo) show \OFCLASS(uint64, equal_class)\ by (fact uint64.of_class_equal) show \OFCLASS(uint64, linorder_class)\ by (fact uint64.of_class_linorder) qed end instantiation uint64 :: ring_bit_operations begin lift_definition bit_uint64 :: \uint64 \ nat \ bool\ is bit . lift_definition not_uint64 :: \uint64 \ uint64\ is \Bit_Operations.not\ . lift_definition and_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.and\ . lift_definition or_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.or\ . lift_definition xor_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.xor\ . lift_definition mask_uint64 :: \nat \ uint64\ is mask . lift_definition push_bit_uint64 :: \nat \ uint64 \ uint64\ is push_bit . lift_definition drop_bit_uint64 :: \nat \ uint64 \ uint64\ is drop_bit . lift_definition signed_drop_bit_uint64 :: \nat \ uint64 \ uint64\ is signed_drop_bit . lift_definition take_bit_uint64 :: \nat \ uint64 \ uint64\ is take_bit . lift_definition set_bit_uint64 :: \nat \ uint64 \ uint64\ is Bit_Operations.set_bit . lift_definition unset_bit_uint64 :: \nat \ uint64 \ uint64\ is unset_bit . lift_definition flip_bit_uint64 :: \nat \ uint64 \ uint64\ is flip_bit . global_interpretation uint64: word_type_copy_bits Abs_uint64 Rep_uint64 signed_drop_bit_uint64 by standard (fact bit_uint64.rep_eq not_uint64.rep_eq and_uint64.rep_eq or_uint64.rep_eq xor_uint64.rep_eq mask_uint64.rep_eq push_bit_uint64.rep_eq drop_bit_uint64.rep_eq signed_drop_bit_uint64.rep_eq take_bit_uint64.rep_eq set_bit_uint64.rep_eq unset_bit_uint64.rep_eq flip_bit_uint64.rep_eq)+ instance by (fact uint64.of_class_ring_bit_operations) end lift_definition uint64_of_nat :: \nat \ uint64\ is word_of_nat . lift_definition nat_of_uint64 :: \uint64 \ nat\ is unat . lift_definition uint64_of_int :: \int \ uint64\ is word_of_int . lift_definition int_of_uint64 :: \uint64 \ int\ is uint . context includes integer.lifting begin lift_definition Uint64 :: \integer \ uint64\ is word_of_int . lift_definition integer_of_uint64 :: \uint64 \ integer\ is uint . end global_interpretation uint64: word_type_copy_more Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 apply standard apply (simp_all add: uint64_of_nat.rep_eq nat_of_uint64.rep_eq uint64_of_int.rep_eq int_of_uint64.rep_eq Uint64.rep_eq integer_of_uint64.rep_eq integer_eq_iff) done instantiation uint64 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint64 :: \uint64 \ nat\ is size . lift_definition msb_uint64 :: \uint64 \ bool\ is msb . lift_definition lsb_uint64 :: \uint64 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint64 :: \uint64 \ nat \ bool \ uint64\ where set_bit_uint64_eq: \set_bit_uint64 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint64_transfer [transfer_rule]: \(cr_uint64 ===> (=) ===> (\) ===> cr_uint64) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint64_eq [abs_def]) transfer_prover end lift_definition set_bits_uint64 :: \(nat \ bool) \ uint64\ is set_bits . lift_definition set_bits_aux_uint64 :: \(nat \ bool) \ nat \ uint64 \ uint64\ is set_bits_aux . global_interpretation uint64: word_type_copy_misc Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 64 set_bits_aux_uint64 by (standard; transfer) simp_all instance using uint64.of_class_bit_comprehension uint64.of_class_set_bit uint64.of_class_lsb by simp_all standard end section \Code setup\ text \ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$. If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume that there is also a \Word64\ structure available and accordingly replace the implementation for the target \verb$Eval$. \ code_printing code_module "Uint64" \ (SML) \(* Test that words can handle numbers between 0 and 63 *) val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6")); structure Uint64 : sig eqtype uint64; val zero : uint64; val one : uint64; val fromInt : IntInf.int -> uint64; val toInt : uint64 -> IntInf.int; val toLarge : uint64 -> LargeWord.word; val fromLarge : LargeWord.word -> uint64 val plus : uint64 -> uint64 -> uint64; val minus : uint64 -> uint64 -> uint64; val times : uint64 -> uint64 -> uint64; val divide : uint64 -> uint64 -> uint64; val modulus : uint64 -> uint64 -> uint64; val negate : uint64 -> uint64; val less_eq : uint64 -> uint64 -> bool; val less : uint64 -> uint64 -> bool; val notb : uint64 -> uint64; val andb : uint64 -> uint64 -> uint64; val orb : uint64 -> uint64 -> uint64; val xorb : uint64 -> uint64 -> uint64; val shiftl : uint64 -> IntInf.int -> uint64; val shiftr : uint64 -> IntInf.int -> uint64; val shiftr_signed : uint64 -> IntInf.int -> uint64; val set_bit : uint64 -> IntInf.int -> bool -> uint64; val test_bit : uint64 -> IntInf.int -> bool; end = struct type uint64 = IntInf.int; val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int; val zero = 0 : IntInf.int; val one = 1 : IntInf.int; fun fromInt x = IntInf.andb(x, mask); fun toInt x = x fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x); fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x); fun plus x y = IntInf.andb(IntInf.+(x, y), mask); fun minus x y = IntInf.andb(IntInf.-(x, y), mask); fun negate x = IntInf.andb(IntInf.~(x), mask); fun times x y = IntInf.andb(IntInf.*(x, y), mask); fun divide x y = IntInf.div(x, y); fun modulus x y = IntInf.mod(x, y); fun less_eq x y = IntInf.<=(x, y); fun less x y = IntInf.<(x, y); fun notb x = IntInf.andb(IntInf.notb(x), mask); fun orb x y = IntInf.orb(x, y); fun andb x y = IntInf.andb(x, y); fun xorb x y = IntInf.xorb(x, y); val maxWord = IntInf.pow (2, Word.wordSize); fun shiftl x n = if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask) else 0; fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else 0; val msb_mask = 0x8000000000000000 : IntInf.int; fun shiftr_signed x i = if IntInf.andb(x, msb_mask) = 0 then shiftr x i else if i >= 64 then 0xFFFFFFFFFFFFFFFF else let val x' = shiftr x i val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask) in IntInf.orb(x', m') end; fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else false; fun set_bit x n b = if n < 64 then if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))) else x; end \ code_reserved SML Uint64 setup \ let val polyml64 = LargeWord.wordSize > 63; (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain from using Word64 in that case. Testing is done with dynamic code evaluation such that the compiler does not choke on the Word64 structure, which need not be present in a 32bit environment. *) val error_msg = "Buggy Word64 structure"; val test_code = "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^ "else raise (Fail \"" ^ error_msg ^ "\");"; val f = Exn.result (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) val use_Word64 = polyml64 andalso (case f () of Exn.Res _ => true | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e | Exn.Exn e => Exn.reraise e) ; val newline = "\n"; val content = "structure Uint64 : sig" ^ newline ^ " eqtype uint64;" ^ newline ^ " val zero : uint64;" ^ newline ^ " val one : uint64;" ^ newline ^ " val fromInt : IntInf.int -> uint64;" ^ newline ^ " val toInt : uint64 -> IntInf.int;" ^ newline ^ " val toLarge : uint64 -> LargeWord.word;" ^ newline ^ " val fromLarge : LargeWord.word -> uint64" ^ newline ^ " val plus : uint64 -> uint64 -> uint64;" ^ newline ^ " val minus : uint64 -> uint64 -> uint64;" ^ newline ^ " val times : uint64 -> uint64 -> uint64;" ^ newline ^ " val divide : uint64 -> uint64 -> uint64;" ^ newline ^ " val modulus : uint64 -> uint64 -> uint64;" ^ newline ^ " val negate : uint64 -> uint64;" ^ newline ^ " val less_eq : uint64 -> uint64 -> bool;" ^ newline ^ " val less : uint64 -> uint64 -> bool;" ^ newline ^ " val notb : uint64 -> uint64;" ^ newline ^ " val andb : uint64 -> uint64 -> uint64;" ^ newline ^ " val orb : uint64 -> uint64 -> uint64;" ^ newline ^ " val xorb : uint64 -> uint64 -> uint64;" ^ newline ^ " val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^ " val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^ "end = struct" ^ newline ^ "" ^ newline ^ "type uint64 = Word64.word;" ^ newline ^ "" ^ newline ^ "val zero = (0wx0 : uint64);" ^ newline ^ "" ^ newline ^ "val one = (0wx1 : uint64);" ^ newline ^ "" ^ newline ^ "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^ "" ^ newline ^ "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);" ^ newline ^ "" ^ newline ^ "fun fromLarge x = Word64.fromLarge x;" ^ newline ^ "" ^ newline ^ "fun toLarge x = Word64.toLarge x;" ^ newline ^ "" ^ newline ^ "fun plus x y = Word64.+(x, y);" ^ newline ^ "" ^ newline ^ "fun minus x y = Word64.-(x, y);" ^ newline ^ "" ^ newline ^ "fun negate x = Word64.~(x);" ^ newline ^ "" ^ newline ^ "fun times x y = Word64.*(x, y);" ^ newline ^ "" ^ newline ^ "fun divide x y = Word64.div(x, y);" ^ newline ^ "" ^ newline ^ "fun modulus x y = Word64.mod(x, y);" ^ newline ^ "" ^ newline ^ "fun less_eq x y = Word64.<=(x, y);" ^ newline ^ "" ^ newline ^ "fun less x y = Word64.<(x, y);" ^ newline ^ "" ^ newline ^ "fun set_bit x n b =" ^ newline ^ " let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ " in if b then Word64.orb (x, mask)" ^ newline ^ " else Word64.andb (x, Word64.notb mask)" ^ newline ^ " end" ^ newline ^ "" ^ newline ^ "fun shiftl x n =" ^ newline ^ " Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr x n =" ^ newline ^ " Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr_signed x n =" ^ newline ^ " Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun test_bit x n =" ^ newline ^ " Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^ "" ^ newline ^ "val notb = Word64.notb" ^ newline ^ "" ^ newline ^ "fun andb x y = Word64.andb(x, y);" ^ newline ^ "" ^ newline ^ "fun orb x y = Word64.orb(x, y);" ^ newline ^ "" ^ newline ^ "fun xorb x y = Word64.xorb(x, y);" ^ newline ^ "" ^ newline ^ "end (*struct Uint64*)" val target_SML64 = "SML_word"; in (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I) #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))])) end \ code_printing code_module Uint64 \ (Haskell) \module Uint64(Int64, Word64) where import Data.Int(Int64) import Data.Word(Word64)\ code_reserved Haskell Uint64 text \ OCaml and Scala provide only signed 64bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint64" \ (OCaml) \module Uint64 : sig val less : int64 -> int64 -> bool val less_eq : int64 -> int64 -> bool val set_bit : int64 -> Z.t -> bool -> int64 val shiftl : int64 -> Z.t -> int64 val shiftr : int64 -> Z.t -> int64 val shiftr_signed : int64 -> Z.t -> int64 val test_bit : int64 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y < 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;; let less_eq x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;; let set_bit x n b = let mask = Int64.shift_left Int64.one (Z.to_int n) in if b then Int64.logor x mask else Int64.logand x (Int64.lognot mask);; let shiftl x n = Int64.shift_left x (Z.to_int n);; let shiftr x n = Int64.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int64.shift_right x (Z.to_int n);; let test_bit x n = Int64.compare (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n))) Int64.zero <> 0;; end;; (*struct Uint64*)\ code_reserved OCaml Uint64 code_printing code_module Uint64 \ (Scala) \object Uint64 { def less(x: Long, y: Long) : Boolean = - if (x < 0) y < 0 && x < y - else y < 0 || x < y + x < 0 match { + case true => y < 0 && x < y + case false => y < 0 || x < y + } def less_eq(x: Long, y: Long) : Boolean = - if (x < 0) y < 0 && x <= y - else y < 0 || x <= y + x < 0 match { + case true => y < 0 && x <= y + case false => y < 0 || x <= y + } def set_bit(x: Long, n: BigInt, b: Boolean) : Long = - if (b) - x | (1L << n.intValue) - else - x & (1L << n.intValue).unary_~ + b match { + case true => x | (1L << n.intValue) + case false => x & (1L << n.intValue).unary_~ + } def shiftl(x: Long, n: BigInt) : Long = x << n.intValue def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue def test_bit(x: Long, n: BigInt) : Boolean = (x & (1L << n.intValue)) != 0 } /* object Uint64 */\ code_reserved Scala Uint64 text \ OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint64_signed :: "integer \ uint64" where "Uint64_signed i = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then undefined Uint64 i else Uint64 i)" lemma Uint64_code [code]: "Uint64 i = (let i' = i AND 0xFFFFFFFFFFFFFFFF in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')" including undefined_transfer integer.lifting unfolding Uint64_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint64_signed_code [code]: "Rep_uint64 (Uint64_signed i) = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))" unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def by(simp add: Abs_uint64_inverse) end text \ Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. The symbolic implementations for code\_simp use @{term Rep_uint64}. The new destructor @{term Rep_uint64'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint64} ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because these instances will be folded away.) To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}. \ definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64" lemma Rep_uint64'_transfer [transfer_rule]: "rel_fun cr_uint64 (=) (\x. x) Rep_uint64'" unfolding Rep_uint64'_def by(rule uint64.rep_transfer) lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint64' :: "64 word \ uint64" is "\x :: 64 word. x" . lemma Abs_uint64'_code [code]: "Abs_uint64' x = Uint64 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint64 \ _"]] lemma term_of_uint64_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []])) (term_of_class.term_of (Rep_uint64' x))" by(simp add: term_of_anything) code_printing type_constructor uint64 \ (SML) "Uint64.uint64" and (Haskell) "Uint64.Word64" and (OCaml) "int64" and (Scala) "Long" | constant Uint64 \ (SML) "Uint64.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and (Scala) "_.longValue" | constant Uint64_signed \ (OCaml) "Z.to'_int64" | constant "0 :: uint64" \ (SML) "Uint64.zero" and (Haskell) "(0 :: Uint64.Word64)" and (OCaml) "Int64.zero" and (Scala) "0" | constant "1 :: uint64" \ (SML) "Uint64.one" and (Haskell) "(1 :: Uint64.Word64)" and (OCaml) "Int64.one" and (Scala) "1" | constant "plus :: uint64 \ _ " \ (SML) "Uint64.plus" and (Haskell) infixl 6 "+" and (OCaml) "Int64.add" and (Scala) infixl 7 "+" | constant "uminus :: uint64 \ _" \ (SML) "Uint64.negate" and (Haskell) "negate" and (OCaml) "Int64.neg" and (Scala) "!(- _)" | constant "minus :: uint64 \ _" \ (SML) "Uint64.minus" and (Haskell) infixl 6 "-" and (OCaml) "Int64.sub" and (Scala) infixl 7 "-" | constant "times :: uint64 \ _ \ _" \ (SML) "Uint64.times" and (Haskell) infixl 7 "*" and (OCaml) "Int64.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint64 \ _ \ bool" \ (SML) "!((_ : Uint64.uint64) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int64.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint64 :: equal \ (Haskell) - | constant "less_eq :: uint64 \ _ \ bool" \ (SML) "Uint64.less'_eq" and (Haskell) infix 4 "<=" and (OCaml) "Uint64.less'_eq" and (Scala) "Uint64.less'_eq" | constant "less :: uint64 \ _ \ bool" \ (SML) "Uint64.less" and (Haskell) infix 4 "<" and (OCaml) "Uint64.less" and (Scala) "Uint64.less" | constant "Bit_Operations.not :: uint64 \ _" \ (SML) "Uint64.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int64.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint64 \ _" \ (SML) "Uint64.andb" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int64.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint64 \ _" \ (SML) "Uint64.orb" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int64.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint64 \ _" \ (SML) "Uint64.xorb" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int64.logxor" and (Scala) infixl 2 "^" definition uint64_divmod :: "uint64 \ uint64 \ uint64 \ uint64" where "uint64_divmod x y = (if y = 0 then (undefined ((div) :: uint64 \ _) x (0 :: uint64), undefined ((mod) :: uint64 \ _) x (0 :: uint64)) else (x div y, x mod y))" definition uint64_div :: "uint64 \ uint64 \ uint64" where "uint64_div x y = fst (uint64_divmod x y)" definition uint64_mod :: "uint64 \ uint64 \ uint64" where "uint64_mod x y = snd (uint64_divmod x y)" lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)" including undefined_transfer unfolding uint64_divmod_def uint64_div_def by transfer (simp add: word_div_def) lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)" including undefined_transfer unfolding uint64_mod_def uint64_divmod_def by transfer (simp add: word_mod_def) definition uint64_sdiv :: "uint64 \ uint64 \ uint64" where [code del]: "uint64_sdiv x y = (if y = 0 then undefined ((div) :: uint64 \ _) x (0 :: uint64) else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))" definition div0_uint64 :: "uint64 \ uint64" where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: div0_uint64]] definition mod0_uint64 :: "uint64 \ uint64" where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: mod0_uint64]] lemma uint64_divmod_code [code]: "uint64_divmod x y = (if 0x8000000000000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint64 x, mod0_uint64 x) else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def less_eq_uint64.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint64_sdiv_code [code]: "Rep_uint64 (uint64_sdiv x y) = (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \ _) x (0 :: uint64)) else Rep_uint64 x sdiv Rep_uint64 y)" unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint64_divmod_code} computes both with division only. \ code_printing constant uint64_div \ (SML) "Uint64.divide" and (Haskell) "Prelude.div" | constant uint64_mod \ (SML) "Uint64.modulus" and (Haskell) "Prelude.mod" | constant uint64_divmod \ (Haskell) "divmod" | constant uint64_sdiv \ (OCaml) "Int64.div" and (Scala) "_ '/ _" definition uint64_test_bit :: "uint64 \ integer \ bool" where [code del]: "uint64_test_bit x n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) x n else bit x (nat_of_integer n))" lemma bit_uint64_code [code]: "bit x n \ n < 64 \ uint64_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint64_test_bit_def by transfer (auto dest: bit_imp_le_length) lemma uint64_test_bit_code [code]: "uint64_test_bit w n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) w n else bit (Rep_uint64 w) (nat_of_integer n))" unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq) code_printing constant uint64_test_bit \ (SML) "Uint64.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint64.test'_bit" and (Scala) "Uint64.test'_bit" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)" definition uint64_set_bit :: "uint64 \ integer \ bool \ uint64" where [code del]: "uint64_set_bit x n b = (if n < 0 \ 63 < n then undefined (set_bit :: uint64 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint64_code [code]: "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint64_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint64_set_bit_code [code]: "Rep_uint64 (uint64_set_bit w n b) = (if n < 0 \ 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \ _) w n b) else set_bit (Rep_uint64 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint64_set_bit_def by transfer simp code_printing constant uint64_set_bit \ (SML) "Uint64.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint64.set'_bit" and (Scala) "Uint64.set'_bit" and (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)" definition uint64_shiftl :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftl x n = (if n < 0 \ 64 \ n then undefined (push_bit :: nat \ uint64 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftl_def by transfer simp lemma uint64_shiftl_code [code]: "Rep_uint64 (uint64_shiftl w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (push_bit :: nat \ uint64 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftl_def by transfer simp code_printing constant uint64_shiftl \ (SML) "Uint64.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint64.shiftl" and (Scala) "Uint64.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)" definition uint64_shiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftr x n = (if n < 0 \ 64 \ n then undefined (drop_bit :: nat \ uint64 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftr_def by transfer simp lemma uint64_shiftr_code [code]: "Rep_uint64 (uint64_shiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (drop_bit :: nat \ uint64 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftr_def by transfer simp code_printing constant uint64_shiftr \ (SML) "Uint64.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint64.shiftr" and (Scala) "Uint64.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)" definition uint64_sshiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_sshiftr x n = (if n < 0 \ 64 \ n then undefined signed_drop_bit_uint64 n x else signed_drop_bit_uint64 (nat_of_integer n) x)" lemma sshiftr_uint64_code [code]: "signed_drop_bit_uint64 n x = (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint64_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint64_sshiftr_code [code]: "Rep_uint64 (uint64_sshiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined signed_drop_bit_uint64 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_sshiftr_def by transfer simp code_printing constant uint64_sshiftr \ (SML) "Uint64.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and (OCaml) "Uint64.shiftr'_signed" and (Scala) "Uint64.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint64_msb_test_bit: "msb x \ bit (x :: uint64) 63" by transfer (simp add: msb_word_iff_bit) lemma msb_uint64_code [code]: "msb x \ uint64_test_bit x 63" by (simp add: uint64_test_bit_def uint64_msb_test_bit) lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint64_code [code]: "int_of_uint64 x = int_of_integer (integer_of_uint64 x)" including integer.lifting by transfer simp lemma uint64_of_nat_code [code]: "uint64_of_nat = uint64_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint64_code [code]: "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)" unfolding integer_of_uint64_def including integer.lifting by transfer simp definition integer_of_uint64_signed :: "uint64 \ integer" where "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)" lemma integer_of_uint64_signed_code [code]: "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))" by (simp add: integer_of_uint64_signed_def integer_of_uint64_def) lemma integer_of_uint64_code [code]: "integer_of_uint64 n = (if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)" proof - have \integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 = Bit_Operations.set_bit 63 (integer_of_uint64_signed (take_bit 63 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint64 n = Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))\ if \bit n 63\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint64 n) m = bit (Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint64_signed_def bit_simps) qed end code_printing constant "integer_of_uint64" \ (SML) "Uint64.toInt" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint64_signed" \ (OCaml) "Z.of'_int64" and (Scala) "BigInt" section \Quickcheck setup\ definition uint64_of_natural :: "natural \ uint64" where "uint64_of_natural x \ Uint64 (integer_of_natural x)" instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint64 \ qc_random_cnv uint64_of_natural" definition "exhaustive_uint64 \ qc_exhaustive_cnv uint64_of_natural" definition "full_exhaustive_uint64 \ qc_full_exhaustive_cnv uint64_of_natural" instance .. end instantiation uint64 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint64.uint64'') []" . definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint64 itself \ _"]] lemmas partial_term_of_uint64 [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint8.thy b/thys/Native_Word/Uint8.thy --- a/thys/Native_Word/Uint8.thy +++ b/thys/Native_Word/Uint8.thy @@ -1,611 +1,615 @@ (* Title: Uint8.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 8 bits\ theory Uint8 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ Restriction for OCaml code generation: OCaml does not provide an int8 type, so no special code generation for this type is set up. If the theory \<^text>\Code_Target_Int_Bit\ is imported, the type \uint8\ is emulated via \<^typ>\8 word\. \ section \Type definition and primitive operations\ typedef uint8 = \UNIV :: 8 word set\ .. global_interpretation uint8: word_type_copy Abs_uint8 Rep_uint8 using type_definition_uint8 by (rule word_type_copy.intro) setup_lifting type_definition_uint8 declare uint8.of_word_of [code abstype] declare Quotient_uint8 [transfer_rule] instantiation uint8 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint8 :: uint8 is 0 . lift_definition one_uint8 :: uint8 is 1 . lift_definition plus_uint8 :: \uint8 \ uint8 \ uint8\ is \(+)\ . lift_definition uminus_uint8 :: \uint8 \ uint8\ is uminus . lift_definition minus_uint8 :: \uint8 \ uint8 \ uint8\ is \(-)\ . lift_definition times_uint8 :: \uint8 \ uint8 \ uint8\ is \(*)\ . lift_definition divide_uint8 :: \uint8 \ uint8 \ uint8\ is \(div)\ . lift_definition modulo_uint8 :: \uint8 \ uint8 \ uint8\ is \(mod)\ . lift_definition equal_uint8 :: \uint8 \ uint8 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint8 :: \uint8 \ uint8 \ bool\ is \(\)\ . lift_definition less_uint8 :: \uint8 \ uint8 \ bool\ is \(<)\ . global_interpretation uint8: word_type_copy_ring Abs_uint8 Rep_uint8 by standard (fact zero_uint8.rep_eq one_uint8.rep_eq plus_uint8.rep_eq uminus_uint8.rep_eq minus_uint8.rep_eq times_uint8.rep_eq divide_uint8.rep_eq modulo_uint8.rep_eq equal_uint8.rep_eq less_eq_uint8.rep_eq less_uint8.rep_eq)+ instance proof - show \OFCLASS(uint8, comm_ring_1_class)\ by (rule uint8.of_class_comm_ring_1) show \OFCLASS(uint8, semiring_modulo_class)\ by (fact uint8.of_class_semiring_modulo) show \OFCLASS(uint8, equal_class)\ by (fact uint8.of_class_equal) show \OFCLASS(uint8, linorder_class)\ by (fact uint8.of_class_linorder) qed end instantiation uint8 :: ring_bit_operations begin lift_definition bit_uint8 :: \uint8 \ nat \ bool\ is bit . lift_definition not_uint8 :: \uint8 \ uint8\ is \Bit_Operations.not\ . lift_definition and_uint8 :: \uint8 \ uint8 \ uint8\ is \Bit_Operations.and\ . lift_definition or_uint8 :: \uint8 \ uint8 \ uint8\ is \Bit_Operations.or\ . lift_definition xor_uint8 :: \uint8 \ uint8 \ uint8\ is \Bit_Operations.xor\ . lift_definition mask_uint8 :: \nat \ uint8\ is mask . lift_definition push_bit_uint8 :: \nat \ uint8 \ uint8\ is push_bit . lift_definition drop_bit_uint8 :: \nat \ uint8 \ uint8\ is drop_bit . lift_definition signed_drop_bit_uint8 :: \nat \ uint8 \ uint8\ is signed_drop_bit . lift_definition take_bit_uint8 :: \nat \ uint8 \ uint8\ is take_bit . lift_definition set_bit_uint8 :: \nat \ uint8 \ uint8\ is Bit_Operations.set_bit . lift_definition unset_bit_uint8 :: \nat \ uint8 \ uint8\ is unset_bit . lift_definition flip_bit_uint8 :: \nat \ uint8 \ uint8\ is flip_bit . global_interpretation uint8: word_type_copy_bits Abs_uint8 Rep_uint8 signed_drop_bit_uint8 by standard (fact bit_uint8.rep_eq not_uint8.rep_eq and_uint8.rep_eq or_uint8.rep_eq xor_uint8.rep_eq mask_uint8.rep_eq push_bit_uint8.rep_eq drop_bit_uint8.rep_eq signed_drop_bit_uint8.rep_eq take_bit_uint8.rep_eq set_bit_uint8.rep_eq unset_bit_uint8.rep_eq flip_bit_uint8.rep_eq)+ instance by (fact uint8.of_class_ring_bit_operations) end lift_definition uint8_of_nat :: \nat \ uint8\ is word_of_nat . lift_definition nat_of_uint8 :: \uint8 \ nat\ is unat . lift_definition uint8_of_int :: \int \ uint8\ is word_of_int . lift_definition int_of_uint8 :: \uint8 \ int\ is uint . context includes integer.lifting begin lift_definition Uint8 :: \integer \ uint8\ is word_of_int . lift_definition integer_of_uint8 :: \uint8 \ integer\ is uint . end global_interpretation uint8: word_type_copy_more Abs_uint8 Rep_uint8 signed_drop_bit_uint8 uint8_of_nat nat_of_uint8 uint8_of_int int_of_uint8 Uint8 integer_of_uint8 apply standard apply (simp_all add: uint8_of_nat.rep_eq nat_of_uint8.rep_eq uint8_of_int.rep_eq int_of_uint8.rep_eq Uint8.rep_eq integer_of_uint8.rep_eq integer_eq_iff) done instantiation uint8 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint8 :: \uint8 \ nat\ is size . lift_definition msb_uint8 :: \uint8 \ bool\ is msb . lift_definition lsb_uint8 :: \uint8 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint8 :: \uint8 \ nat \ bool \ uint8\ where set_bit_uint8_eq: \set_bit_uint8 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint8_transfer [transfer_rule]: \(cr_uint8 ===> (=) ===> (\) ===> cr_uint8) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint8_eq [abs_def]) transfer_prover end lift_definition set_bits_uint8 :: \(nat \ bool) \ uint8\ is set_bits . lift_definition set_bits_aux_uint8 :: \(nat \ bool) \ nat \ uint8 \ uint8\ is set_bits_aux . global_interpretation uint8: word_type_copy_misc Abs_uint8 Rep_uint8 signed_drop_bit_uint8 uint8_of_nat nat_of_uint8 uint8_of_int int_of_uint8 Uint8 integer_of_uint8 8 set_bits_aux_uint8 by (standard; transfer) simp_all instance using uint8.of_class_bit_comprehension uint8.of_class_set_bit uint8.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint8 \ (SML) \(* Test that words can handle numbers between 0 and 3 *) val _ = if 3 <= Word.wordSize then () else raise (Fail ("wordSize less than 3")); structure Uint8 : sig val set_bit : Word8.word -> IntInf.int -> bool -> Word8.word val shiftl : Word8.word -> IntInf.int -> Word8.word val shiftr : Word8.word -> IntInf.int -> Word8.word val shiftr_signed : Word8.word -> IntInf.int -> Word8.word val test_bit : Word8.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word8.orb (x, mask) else Word8.andb (x, Word8.notb mask) end fun shiftl x n = Word8.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word8.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word8.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word8.andb (x, Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word8.fromInt 0 end; (* struct Uint8 *)\ code_reserved SML Uint8 code_printing code_module Uint8 \ (Haskell) \module Uint8(Int8, Word8) where import Data.Int(Int8) import Data.Word(Word8)\ code_reserved Haskell Uint8 text \ Scala provides only signed 8bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module Uint8 \ (Scala) \object Uint8 { def less(x: Byte, y: Byte) : Boolean = - if (x < 0) y < 0 && x < y - else y < 0 || x < y + x < 0 match { + case true => y < 0 && x < y + case false => y < 0 || x < y + } def less_eq(x: Byte, y: Byte) : Boolean = - if (x < 0) y < 0 && x <= y - else y < 0 || x <= y + x < 0 match { + case true => y < 0 && x <= y + case false => y < 0 || x <= y + } def set_bit(x: Byte, n: BigInt, b: Boolean) : Byte = - if (b) - (x | (1 << n.intValue)).toByte - else - (x & (1 << n.intValue).unary_~).toByte + b match { + case true => (x | (1 << n.intValue)).toByte + case false => (x & (1 << n.intValue).unary_~).toByte + } def shiftl(x: Byte, n: BigInt) : Byte = (x << n.intValue).toByte def shiftr(x: Byte, n: BigInt) : Byte = ((x & 255) >>> n.intValue).toByte def shiftr_signed(x: Byte, n: BigInt) : Byte = (x >> n.intValue).toByte def test_bit(x: Byte, n: BigInt) : Boolean = (x & (1 << n.intValue)) != 0 } /* object Uint8 */\ code_reserved Scala Uint8 text \ Avoid @{term Abs_uint8} in generated code, use @{term Rep_uint8'} instead. The symbolic implementations for code\_simp use @{term Rep_uint8}. The new destructor @{term Rep_uint8'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint8} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint8} ([code abstract] equations for @{typ uint8} may use @{term Rep_uint8} because these instances will be folded away.) To convert @{typ "8 word"} values into @{typ uint8}, use @{term "Abs_uint8'"}. \ definition Rep_uint8' where [simp]: "Rep_uint8' = Rep_uint8" lemma Rep_uint8'_transfer [transfer_rule]: "rel_fun cr_uint8 (=) (\x. x) Rep_uint8'" unfolding Rep_uint8'_def by(rule uint8.rep_transfer) lemma Rep_uint8'_code [code]: "Rep_uint8' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint8' :: "8 word \ uint8" is "\x :: 8 word. x" . lemma Abs_uint8'_code [code]: "Abs_uint8' x = Uint8 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint8 \ _"]] lemma term_of_uint8_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint8.uint8.Abs_uint8'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]], TR (STR ''Uint8.uint8'') []])) (term_of_class.term_of (Rep_uint8' x))" by(simp add: term_of_anything) lemma Uin8_code [code]: "Rep_uint8 (Uint8 i) = word_of_int (int_of_integer_symbolic i)" unfolding Uint8_def int_of_integer_symbolic_def by(simp add: Abs_uint8_inverse) code_printing type_constructor uint8 \ (SML) "Word8.word" and (Haskell) "Uint8.Word8" and (Scala) "Byte" | constant Uint8 \ (SML) "Word8.fromLargeInt (IntInf.toLarge _)" and (Haskell) "(Prelude.fromInteger _ :: Uint8.Word8)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Word8)" and (Scala) "_.byteValue" | constant "0 :: uint8" \ (SML) "(Word8.fromInt 0)" and (Haskell) "(0 :: Uint8.Word8)" and (Scala) "0.toByte" | constant "1 :: uint8" \ (SML) "(Word8.fromInt 1)" and (Haskell) "(1 :: Uint8.Word8)" and (Scala) "1.toByte" | constant "plus :: uint8 \ _ \ _" \ (SML) "Word8.+ ((_), (_))" and (Haskell) infixl 6 "+" and (Scala) "(_ +/ _).toByte" | constant "uminus :: uint8 \ _" \ (SML) "Word8.~" and (Haskell) "negate" and (Scala) "(- _).toByte" | constant "minus :: uint8 \ _" \ (SML) "Word8.- ((_), (_))" and (Haskell) infixl 6 "-" and (Scala) "(_ -/ _).toByte" | constant "times :: uint8 \ _ \ _" \ (SML) "Word8.* ((_), (_))" and (Haskell) infixl 7 "*" and (Scala) "(_ */ _).toByte" | constant "HOL.equal :: uint8 \ _ \ bool" \ (SML) "!((_ : Word8.word) = _)" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" | class_instance uint8 :: equal \ (Haskell) - | constant "less_eq :: uint8 \ _ \ bool" \ (SML) "Word8.<= ((_), (_))" and (Haskell) infix 4 "<=" and (Scala) "Uint8.less'_eq" | constant "less :: uint8 \ _ \ bool" \ (SML) "Word8.< ((_), (_))" and (Haskell) infix 4 "<" and (Scala) "Uint8.less" | constant "Bit_Operations.not :: uint8 \ _" \ (SML) "Word8.notb" and (Haskell) "Data'_Bits.complement" and (Scala) "_.unary'_~.toByte" | constant "Bit_Operations.and :: uint8 \ _" \ (SML) "Word8.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (Scala) "(_ & _).toByte" | constant "Bit_Operations.or :: uint8 \ _" \ (SML) "Word8.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (Scala) "(_ | _).toByte" | constant "Bit_Operations.xor :: uint8 \ _" \ (SML) "Word8.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (Scala) "(_ ^ _).toByte" definition uint8_divmod :: "uint8 \ uint8 \ uint8 \ uint8" where "uint8_divmod x y = (if y = 0 then (undefined ((div) :: uint8 \ _) x (0 :: uint8), undefined ((mod) :: uint8 \ _) x (0 :: uint8)) else (x div y, x mod y))" definition uint8_div :: "uint8 \ uint8 \ uint8" where "uint8_div x y = fst (uint8_divmod x y)" definition uint8_mod :: "uint8 \ uint8 \ uint8" where "uint8_mod x y = snd (uint8_divmod x y)" lemma div_uint8_code [code]: "x div y = (if y = 0 then 0 else uint8_div x y)" including undefined_transfer unfolding uint8_divmod_def uint8_div_def by transfer (simp add: word_div_def) lemma mod_uint8_code [code]: "x mod y = (if y = 0 then x else uint8_mod x y)" including undefined_transfer unfolding uint8_mod_def uint8_divmod_def by transfer (simp add: word_mod_def) definition uint8_sdiv :: "uint8 \ uint8 \ uint8" where "uint8_sdiv x y = (if y = 0 then undefined ((div) :: uint8 \ _) x (0 :: uint8) else Abs_uint8 (Rep_uint8 x sdiv Rep_uint8 y))" definition div0_uint8 :: "uint8 \ uint8" where [code del]: "div0_uint8 x = undefined ((div) :: uint8 \ _) x (0 :: uint8)" declare [[code abort: div0_uint8]] definition mod0_uint8 :: "uint8 \ uint8" where [code del]: "mod0_uint8 x = undefined ((mod) :: uint8 \ _) x (0 :: uint8)" declare [[code abort: mod0_uint8]] lemma uint8_divmod_code [code]: "uint8_divmod x y = (if 0x80 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint8 x, mod0_uint8 x) else let q = push_bit 1 (uint8_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint8_divmod_def uint8_sdiv_def div0_uint8_def mod0_uint8_def less_eq_uint8.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint8_sdiv_code [code]: "Rep_uint8 (uint8_sdiv x y) = (if y = 0 then Rep_uint8 (undefined ((div) :: uint8 \ _) x (0 :: uint8)) else Rep_uint8 x sdiv Rep_uint8 y)" unfolding uint8_sdiv_def by(simp add: Abs_uint8_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint8_divmod_code} computes both with division only. \ code_printing constant uint8_div \ (SML) "Word8.div ((_), (_))" and (Haskell) "Prelude.div" | constant uint8_mod \ (SML) "Word8.mod ((_), (_))" and (Haskell) "Prelude.mod" | constant uint8_divmod \ (Haskell) "divmod" | constant uint8_sdiv \ (Scala) "(_ '/ _).toByte" definition uint8_test_bit :: "uint8 \ integer \ bool" where [code del]: "uint8_test_bit x n = (if n < 0 \ 7 < n then undefined (bit :: uint8 \ _) x n else bit x (nat_of_integer n))" lemma bit_uint8_code [code]: "bit x n \ n < 8 \ uint8_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint8_test_bit_def by (transfer, simp, transfer, simp) lemma uint8_test_bit_code [code]: "uint8_test_bit w n = (if n < 0 \ 7 < n then undefined (bit :: uint8 \ _) w n else bit (Rep_uint8 w) (nat_of_integer n))" unfolding uint8_test_bit_def by (simp add: bit_uint8.rep_eq) code_printing constant uint8_test_bit \ (SML) "Uint8.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (Scala) "Uint8.test'_bit" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_test'_bit out of bounds\") else Uint8.test'_bit x i)" definition uint8_set_bit :: "uint8 \ integer \ bool \ uint8" where [code del]: "uint8_set_bit x n b = (if n < 0 \ 7 < n then undefined (set_bit :: uint8 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint8_code [code]: "set_bit x n b = (if n < 8 then uint8_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint8_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint8_set_bit_code [code]: "Rep_uint8 (uint8_set_bit w n b) = (if n < 0 \ 7 < n then Rep_uint8 (undefined (set_bit :: uint8 \ _) w n b) else set_bit (Rep_uint8 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint8_set_bit_def by transfer simp code_printing constant uint8_set_bit \ (SML) "Uint8.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (Scala) "Uint8.set'_bit" and (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_set'_bit out of bounds\") else Uint8.set'_bit x i b)" definition uint8_shiftl :: "uint8 \ integer \ uint8" where [code del]: "uint8_shiftl x n = (if n < 0 \ 8 \ n then undefined (push_bit :: nat \ uint8 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint8_code [code]: "push_bit n x = (if n < 8 then uint8_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint8_shiftl_def by transfer simp lemma uint8_shiftl_code [code]: "Rep_uint8 (uint8_shiftl w n) = (if n < 0 \ 8 \ n then Rep_uint8 (undefined (push_bit :: nat \ uint8 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint8 w))" including undefined_transfer unfolding uint8_shiftl_def by transfer simp code_printing constant uint8_shiftl \ (SML) "Uint8.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (Scala) "Uint8.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftl out of bounds\") else Uint8.shiftl x i)" definition uint8_shiftr :: "uint8 \ integer \ uint8" where [code del]: "uint8_shiftr x n = (if n < 0 \ 8 \ n then undefined (drop_bit :: _ \ _ \ uint8) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint8_code [code]: "drop_bit n x = (if n < 8 then uint8_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint8_shiftr_def by transfer simp lemma uint8_shiftr_code [code]: "Rep_uint8 (uint8_shiftr w n) = (if n < 0 \ 8 \ n then Rep_uint8 (undefined (drop_bit :: _ \ _ \ uint8) w n) else drop_bit (nat_of_integer n) (Rep_uint8 w))" including undefined_transfer unfolding uint8_shiftr_def by transfer simp code_printing constant uint8_shiftr \ (SML) "Uint8.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (Scala) "Uint8.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftr out of bounds\") else Uint8.shiftr x i)" definition uint8_sshiftr :: "uint8 \ integer \ uint8" where [code del]: "uint8_sshiftr x n = (if n < 0 \ 8 \ n then undefined signed_drop_bit_uint8 n x else signed_drop_bit_uint8 (nat_of_integer n) x)" lemma sshiftr_uint8_code [code]: "signed_drop_bit_uint8 n x = (if n < 8 then uint8_sshiftr x (integer_of_nat n) else if bit x 7 then -1 else 0)" including undefined_transfer integer.lifting unfolding uint8_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond word_size) lemma uint8_sshiftr_code [code]: "Rep_uint8 (uint8_sshiftr w n) = (if n < 0 \ 8 \ n then Rep_uint8 (undefined signed_drop_bit_uint8 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint8 w))" including undefined_transfer unfolding uint8_sshiftr_def by transfer simp code_printing constant uint8_sshiftr \ (SML) "Uint8.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Int8) _)) :: Uint8.Word8)" and (Scala) "Uint8.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_sshiftr out of bounds\") else Uint8.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint8_msb_test_bit: "msb x \ bit (x :: uint8) 7" by transfer (simp add: msb_word_iff_bit) lemma msb_uint16_code [code]: "msb x \ uint8_test_bit x 7" by (simp add: uint8_test_bit_def uint8_msb_test_bit) lemma uint8_of_int_code [code]: "uint8_of_int i = Uint8 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint8_code [code]: "int_of_uint8 x = int_of_integer (integer_of_uint8 x)" by (simp add: int_of_uint8.rep_eq integer_of_uint8_def) lemma uint8_of_nat_code [code]: "uint8_of_nat = uint8_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint8_code [code]: "nat_of_uint8 x = nat_of_integer (integer_of_uint8 x)" unfolding integer_of_uint8_def including integer.lifting by transfer simp definition integer_of_uint8_signed :: "uint8 \ integer" where "integer_of_uint8_signed n = (if bit n 7 then undefined integer_of_uint8 n else integer_of_uint8 n)" lemma integer_of_uint8_signed_code [code]: "integer_of_uint8_signed n = (if bit n 7 then undefined integer_of_uint8 n else integer_of_int (uint (Rep_uint8' n)))" by (simp add: integer_of_uint8_signed_def integer_of_uint8_def) lemma integer_of_uint8_code [code]: "integer_of_uint8 n = (if bit n 7 then integer_of_uint8_signed (n AND 0x7F) OR 0x80 else integer_of_uint8_signed n)" proof - have \integer_of_uint8_signed (n AND 0x7F) OR 0x80 = Bit_Operations.set_bit 7 (integer_of_uint8_signed (take_bit 7 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint8 n = Bit_Operations.set_bit 7 (integer_of_uint8 (take_bit 7 n))\ if \bit n 7\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint8 n) m = bit (Bit_Operations.set_bit 7 (integer_of_uint8 (take_bit 7 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint8_signed_def bit_simps) qed end code_printing constant "integer_of_uint8" \ (SML) "IntInf.fromLarge (Word8.toLargeInt _)" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint8_signed" \ (Scala) "BigInt" section \Quickcheck setup\ definition uint8_of_natural :: "natural \ uint8" where "uint8_of_natural x \ Uint8 (integer_of_natural x)" instantiation uint8 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint8 \ qc_random_cnv uint8_of_natural" definition "exhaustive_uint8 \ qc_exhaustive_cnv uint8_of_natural" definition "full_exhaustive_uint8 \ qc_full_exhaustive_cnv uint8_of_natural" instance .. end instantiation uint8 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint8 i in (x, 0xFF - x)" "0" "Typerep.Typerep (STR ''Uint8.uint8'') []" . definition "narrowing_uint8 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint8 itself \ _"]] lemmas partial_term_of_uint8 [code] = partial_term_of_code instance .. end end diff --git a/thys/Polynomial_Interpolation/Improved_Code_Equations.thy b/thys/Polynomial_Interpolation/Improved_Code_Equations.thy --- a/thys/Polynomial_Interpolation/Improved_Code_Equations.thy +++ b/thys/Polynomial_Interpolation/Improved_Code_Equations.thy @@ -1,73 +1,73 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) section \Improved Code Equations\ text \This theory contains improved code equations for certain algorithms.\ theory Improved_Code_Equations imports "HOL-Computational_Algebra.Polynomial" "HOL-Library.Code_Target_Nat" begin subsection \@{const divmod_integer}.\ text \We improve @{thm divmod_integer_code} by deleting @{const sgn}-expressions.\ text \We guard the application of divmod-abs' with the condition @{term "x \ 0 \ y \ 0"}, so that application can be ensured on non-negative values. Hence, one can drop "abs" in target language setup.\ definition divmod_abs' where "x \ 0 \ y \ 0 \ divmod_abs' x y = Code_Numeral.divmod_abs x y" (* led to an another 10 % improvement on factorization example *) lemma divmod_integer_code''[code]: "divmod_integer k l = (if k = 0 then (0, 0) else if l > 0 then (if k > 0 then divmod_abs' k l else case divmod_abs' (- k) l of (r, s) \ if s = 0 then (- r, 0) else (- r - 1, l - s)) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then divmod_abs' (-k) (-l) else case divmod_abs' k (-l) of (r, s) \ if s = 0 then (- r, 0) else (- r - 1, - l - s)))" unfolding divmod_integer_code by (cases "l = 0"; cases "l < 0"; cases "l > 0"; auto split: prod.splits simp: divmod_abs'_def divmod_abs_def) code_printing \ \FIXME illusion of partiality\ constant divmod_abs' \ (SML) "IntInf.divMod/ ( _,/ _ )" and (Eval) "Integer.div'_mod/ ( _ )/ ( _ )" and (OCaml) "Z.div'_rem" and (Haskell) "divMod/ ( _ )/ ( _ )" - and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k '/% l))" + and (Scala) "!((k: BigInt) => (l: BigInt) => l == 0 match { case true => (BigInt(0), k) case false => (k '/% l) })" subsection \@{const Euclidean_Rings.divmod_nat}.\ text \We implement @{const Euclidean_Rings.divmod_nat} via @{const divmod_integer} instead of invoking both division and modulo separately, and we further simplify the case-analysis which is performed in @{thm divmod_integer_code''}.\ lemma divmod_nat_code'[code]: "Euclidean_Rings.divmod_nat m n = ( let k = integer_of_nat m; l = integer_of_nat n in map_prod nat_of_integer nat_of_integer (if k = 0 then (0, 0) else if l = 0 then (0,k) else divmod_abs' k l))" using divmod_nat_code [of m n] by (simp add: divmod_abs'_def integer_of_nat_eq_of_nat Let_def) subsection \@{const binomial}\ lemma binomial_code[code]: "n choose k = (if k \ n then fact n div (fact k * fact (n - k)) else 0)" using binomial_eq_0[of n k] binomial_altdef_nat[of k n] by simp end diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy --- a/thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy +++ b/thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy @@ -1,193 +1,193 @@ section \Bit Block Transfer and Other Array Optimizations\ theory Array_Blit imports "../Sep_Main" "HOL-Library.Code_Target_Numeral" begin subsection "Definition" (* TODO/FIXME: Does not work with same arrays and overlapping ranges. Currently, the generated code will throw an exception if the arrays are the same. If only used with blit_rule, separation logic guarantees that arrays will be disjoint. *) primrec blit :: "_ array \ nat \ _ array \ nat \ nat \ unit Heap" where "blit _ _ _ _ 0 = return ()" | "blit src si dst di (Suc l) = do { x \ Array.nth src si; Array.upd di x dst; blit src (si+1) dst (di+1) l }" lemma blit_rule[sep_heap_rules]: assumes LEN: "si+len \ length lsrc" "di+len \ length ldst" shows "< src \\<^sub>a lsrc * dst \\<^sub>a ldst > blit src si dst di len <\_. src \\<^sub>a lsrc * dst \\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst) >" using LEN proof (induction len arbitrary: si di ldst) case 0 thus ?case by sep_auto next case (Suc len) note [sep_heap_rules] = Suc.IH have [simp]: "\x. lsrc ! si # take len (drop (Suc si) lsrc) @ x = take (Suc len) (drop si lsrc) @ x" apply simp by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc less_Suc_eq_le add.commute not_less_eq take_Suc_Cons Nat.trans_le_add2) from Suc.prems show ?case by (sep_auto simp: take_update_last drop_upd_irrelevant) qed definition nth_oo where "nth_oo v a i \ do { l\Array.len a; if i do { l\Array.len a; if i (SML) \ fun array_blit src si dst di len = ( src=dst andalso raise Fail ("array_blit: Same arrays"); ArraySlice.copy { di = IntInf.toInt di, src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)), dst = dst}) fun array_nth_oo v a i () = Array.sub(a,IntInf.toInt i) handle Subscript => v | Overflow => v fun array_upd_oo f i x a () = (Array.update(a,IntInf.toInt i,x); a) handle Subscript => f () | Overflow => f () \ definition blit' where [code del]: "blit' src si dst di len = blit src (nat_of_integer si) dst (nat_of_integer di) (nat_of_integer len)" lemma [code]: "blit src si dst di len = blit' src (integer_of_nat si) dst (integer_of_nat di) (integer_of_nat len)" by (simp add: blit'_def) (* TODO: Export to other languages: OCaml, Haskell *) code_printing constant blit' \ (SML) "(fn/ ()/ => /array'_blit _ _ _ _ _)" and (Scala) "{ ('_: Unit)/=>/ def safecopy(src: Array['_], srci: Int, dst: Array['_], dsti: Int, len: Int) = { - if (src eq dst) - sys.error(\"array'_blit: Same arrays\") - else - System.arraycopy(src, srci, dst, dsti, len) + src eq dst match { + case true => sys.error(\"array'_blit: Same arrays\") + case false => System.arraycopy(src, srci, dst, dsti, len) + } } safecopy(_.array,_.toInt,_.array,_.toInt,_.toInt) }" definition [code del]: "nth_oo' v a == nth_oo v a o nat_of_integer" definition [code del]: "upd_oo' f == upd_oo f o nat_of_integer" lemma [code]: "nth_oo v a == nth_oo' v a o integer_of_nat" "upd_oo f == upd_oo' f o integer_of_nat" by (simp_all add: nth_oo'_def upd_oo'_def o_def) text \Fallbacks\ lemmas [code] = nth_oo'_def[unfolded nth_oo_def[abs_def]] lemmas [code] = upd_oo'_def[unfolded upd_oo_def[abs_def]] code_printing constant nth_oo' \ (SML) "array'_nth'_oo _ _ _" | constant upd_oo' \ (SML) "array'_upd'_oo _ _ _ _" subsection \Derived Functions\ definition "array_shrink a s \ do { \ \Avoiding the need for default value\ l\Array.len a; if l=s then return a else if l=0 then Array.of_list [] else do { x\Array.nth a 0; a'\Array.new s x; blit a 0 a' 0 s; return a' } }" lemma array_shrink_rule[sep_heap_rules]: assumes "s\length la" shows "< a\\<^sub>ala > array_shrink a s <\a'. a'\\<^sub>atake s la >\<^sub>t" using assms unfolding array_shrink_def by sep_auto definition "array_grow a s x \ do { l\Array.len a; if l=s then return a else do { a'\Array.new s x; blit a 0 a' 0 l; return a' } }" lemma array_grow_rule[sep_heap_rules]: assumes "s\length la" shows " < a\\<^sub>ala > array_grow a s x <\a'. a'\\<^sub>a (la @ replicate (s-length la) x)>\<^sub>t" using assms unfolding array_grow_def by sep_auto export_code array_grow checking SML Scala (* TODO: Are there system-calls for array-copy? *) definition "array_copy a \ do { l\Array.len a; if l=0 then Array.of_list [] else do { s \ Array.nth a 0; a'\Array.new l s; blit a 0 a' 0 l; return a' } }" lemma array_copy_rule[sep_heap_rules]: " < a\\<^sub>al> array_copy a <\a'. a\\<^sub>al * a'\\<^sub>a l>" unfolding array_copy_def by sep_auto export_code array_copy checking SML Scala end