src/HOL/Word/Tools/word_lib.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Tools/word_lib.ML	Tue Apr 17 16:21:47 2012 +1000
@@ -0,0 +1,40 @@
+(*  Title:      HOL/Word/Tools/word_lib.ML
+    Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
+
+Helper routines for operating on the word type at the ML level.
+*)
+
+
+structure Word_Lib = struct
+
+fun dest_binT T =
+  (case T of
+    Type (@{type_name "Numeral_Type.num0"}, _) => 0
+  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
+  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
+  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
+  | _ => raise TYPE ("dest_binT", [T], []))
+
+fun is_wordT (Type (@{type_name word}, _)) = true
+  | is_wordT _ = false
+
+fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
+  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
+
+local
+  fun mk_bitT i T =
+    if i = 0
+    then Type (@{type_name "Numeral_Type.bit0"}, [T])
+    else Type (@{type_name "Numeral_Type.bit1"}, [T])
+
+  fun mk_binT size = 
+    if size = 0 then @{typ "Numeral_Type.num0"}
+    else if size = 1 then @{typ "Numeral_Type.num1"}
+    else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
+in
+fun mk_wordT size =
+  if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
+  else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], [])
+end
+
+end