Mayank Manjrekar (Jun 26 2024 at 21:48): Mayank Manjrekar (Jun 26 2024 at 21:48):Hi! new Isabelle/HOL user here. I am mainly using the Bit operations library. I have defined a bit-vector concatenate (concat2) operation as follows, but I would like to develop a convenient macro for concatenating arbitrary number of bit-vectors, while hopefully using an input syntax that is as close to Verilog concatenation operator as possible (E.g {2'd3, 2'd3, 2'd3} := (3 << 4) + (3 << 2) + 3). Can this be done using syntax and translations commands? I have made the following attempt -- how can I fix this example, or do something better?
theory Concat
imports Complex_Main
begin
context semiring_bit_operations
begin
definition concat2 :: "'a ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a" where
"concat2 x m y n ≡ (push_bit n (take_bit m x)) + take_bit n y"
end
nonterminal "bvs" and "bv"
syntax "_bv" :: "logic ⇒ logic ⇒ bv" ("(_)$d(_)" [101, 100] 99)
syntax "_bvs" :: "bv ⇒ bvs ⇒ bvs" ("(_) , (_)")
syntax "_bvs" :: "bv ⇒ bv ⇒ bvs" ("(_) , (_)")
syntax "_cat" :: "bvs ⇒ logic" ("{{(_)}}")
find_consts name:"concat2"
translations
"_cat (_bv n x) rst" ⇀ "CONST Concat.semiring_bit_operations_class.concat2 x n rst" (* need to compute length of rst here *)
"_cat (_bvs (_bv m x) (_bv n y))" ⇀ "CONST Concat.semiring_bit_operations_class.concat2 x m y n"
(* {2'd3, 2'd3} = 4'd15 *)
value "concat2 3 2 3 2 :: int" (* "15" :: "int" *)
value "{{2$d3, 2$d3}} :: int" (* "15" :: "int" *)
(* {2'd3, 2'd3, 2'd3} = 6'd63 *)
value "concat2 3 2 (concat2 3 2 3 2) 4 :: int" (* "63" :: "int" *)
value "{{2$d3, 2$d3, 2$d3}} :: int" (* Undefined constant: "_cat" *)
end
This works for me:
theory Concat
imports Complex_Main
begin
context semiring_bit_operations
begin
definition concat2 :: "'a ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a" where
"concat2 x m y n ≡ (push_bit n (take_bit m x)) + take_bit n y"
primrec concat_size :: "('a × nat) list ⇒ nat" where
"concat_size [] = 0" |
"concat_size (x # y) = (snd x) + (concat_size y)"
primrec concat :: "('a × nat) list ⇒ 'a" where
"concat [] = 0" |
"concat (x # y) = (concat2 (fst x) (snd x) (concat y) (concat_size y))"
end
nonterminal "bvs" and "bv"
syntax "_bv" :: "logic ⇒ logic ⇒ bv" ("(_)$d(_)" [101, 100] 99)
syntax "_bvs" :: "bv ⇒ bvs ⇒ bvs" ("(_) , (_)")
syntax "_bvs" :: "bv ⇒ bvs" ("(_)}}")
syntax "_cat" :: "bvs ⇒ logic" ("{{(_)")
translations
"_cat x" ⇀ "CONST Concat.semiring_bit_operations_class.concat x"
"_bvs (_bv n x) y" ⇀ "(x,n) # y"
"_bvs (_bv n x)" ⇀ "(x,n) # []"
value "concat [(3, 2), (3, 2)] :: int" (* "15" :: "int" *)
value "{{2$d3, 2$d3}} :: int" (* "15" :: "int" *)
value "{{2$d3, 2$d3, 2$d3}} :: int" (* "63" :: "int" *)
end
Last updated: Dec 21 2024 at 16:20 UTC