src/HOL/Word/Tools/word_lib.ML
changeset 59806 d3d4ec6c21ef
parent 47567 407cabf66f21
child 69597 ff784d5a5bfb
equal deleted inserted replaced
59805:a162f779925a 59806:d3d4ec6c21ef
     1 (*  Title:      HOL/Word/Tools/word_lib.ML
     1 (*  Title:      HOL/Word/Tools/word_lib.ML
     2     Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
     2     Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
     3 
     3 
     4 Helper routines for operating on the word type at the ML level.
     4 Helper routines for operating on the word type.
     5 *)
     5 *)
     6 
     6 
       
     7 signature WORD_LIB =
       
     8 sig
       
     9   val dest_binT: typ -> int
       
    10   val is_wordT: typ -> bool
       
    11   val dest_wordT: typ -> int
       
    12   val mk_wordT: int -> typ
       
    13 end
     7 
    14 
     8 structure Word_Lib = struct
    15 structure Word_Lib: WORD_LIB =
       
    16 struct
     9 
    17 
    10 fun dest_binT T =
    18 fun dest_binT T =
    11   (case T of
    19   (case T of
    12     Type (@{type_name "Numeral_Type.num0"}, _) => 0
    20     Type (@{type_name "Numeral_Type.num0"}, _) => 0
    13   | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    21   | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    19   | is_wordT _ = false
    27   | is_wordT _ = false
    20 
    28 
    21 fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
    29 fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
    22   | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
    30   | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
    23 
    31 
    24 local
       
    25   fun mk_bitT i T =
       
    26     if i = 0
       
    27     then Type (@{type_name "Numeral_Type.bit0"}, [T])
       
    28     else Type (@{type_name "Numeral_Type.bit1"}, [T])
       
    29 
    32 
    30   fun mk_binT size = 
    33 fun mk_bitT i T =
    31     if size = 0 then @{typ "Numeral_Type.num0"}
    34   if i = 0
    32     else if size = 1 then @{typ "Numeral_Type.num1"}
    35   then Type (@{type_name "Numeral_Type.bit0"}, [T])
    33     else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
    36   else Type (@{type_name "Numeral_Type.bit1"}, [T])
    34 in
    37 
       
    38 fun mk_binT size = 
       
    39   if size = 0 then @{typ "Numeral_Type.num0"}
       
    40   else if size = 1 then @{typ "Numeral_Type.num1"}
       
    41   else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
       
    42 
    35 fun mk_wordT size =
    43 fun mk_wordT size =
    36   if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
    44   if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
    37   else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], [])
    45   else raise TYPE ("mk_wordT: " ^ string_of_int size, [], [])
    38 end
       
    39 
    46 
    40 end
    47 end