Theory RegistersOps

section‹Register Operations›
theory RegistersOps
imports Main "../lib/WordDecl" "Word_Lib.Bit_Shifts_Infix_Syntax"
begin

context
  includes bit_operations_syntax
begin

text‹
 This theory provides operations to get, set and clear bits in registers
›

section "Getting Fields"
  
text‹
  Get a field of type @{typ "'b::len word"} 
  starting at @{term "index"} from @{term "addr"} of type @{typ "'a::len word"}
›
definition get_field_from_word_a_b:: "'a::len word ⇒ nat ⇒ 'b::len word"
 where
  "get_field_from_word_a_b addr index 
    ≡ let off = (size addr - LENGTH('b)) 
       in ucast ((addr << (off-index)) >> off)"

text‹
  Obtain, from addr of type @{typ "'a::len word"}, 
  another @{typ "'a::len word"} containing the field of length ‹len›
  starting at ‹index› in ‹addr›. 
›
definition get_field_from_word_a_a:: "'a::len word ⇒ nat ⇒ nat ⇒ 'a::len word"
 where
  "get_field_from_word_a_a addr index len 
    ≡ (addr << (size addr - (index+len)) >> (size addr - len))"

section "Setting Fields"

text‹
  Set the field of type @{typ "'b::len word"} 
  at ‹index› from ‹record›
  of type @{typ "'a::len word"}. 
›
definition set_field :: "'a::len word ⇒ 'b::len word ⇒ nat ⇒ 'a::len word"
 where 
  "set_field record field index 
    ≡ let mask:: ('a::len word) = (mask (size field)) << index 
      in  (record AND (NOT mask)) OR ((ucast field) << index)"


section "Clearing Fields"

text‹
  Zero the ‹n› initial bits of ‹addr›.
›
definition clear_n_bits:: "'a::len word ⇒ nat ⇒ 'a::len word" 
 where
   "clear_n_bits addr n ≡ addr AND (NOT (mask n))"

text‹
  Gets the natural value of a 32 bit mask 
›

definition get_nat_from_mask::"word32 ⇒ nat ⇒ nat ⇒ (word32 × nat)" 
where
"
get_nat_from_mask w m v ≡ if (w AND (mask m) =0) then (w>>m, v+m)
                          else (w,m)
"

definition get_nat_from_mask32::"word32⇒ nat"
where
"get_nat_from_mask32 w ≡ 
                            if (w=0) then len_of TYPE (word_length32)
                            else
                                let (w,res) = get_nat_from_mask w 16 0 in
                                     let (w,res)= get_nat_from_mask w 8 res in
                                          let (w,res) = get_nat_from_mask w 4 res in
                                              let (w,res) = get_nat_from_mask w 2 res in
                                                  let (w,res) = get_nat_from_mask w 1 res in
                                                        res
"

end

end