1 files changed, 79 insertions, 0 deletions
diff --git a/src/bitfield.ml b/src/bitfield.ml
new file mode 100644
index 00000000..0a32654d
--- /dev/null
+++ b/src/bitfield.ml
@@ -0,0 +1,79 @@
+
+module Big_int = Nat_big_num
+
+open Initial_check
+open Ast
+open Ast_util
+
+let bitvec size order =
+  Printf.sprintf "vector(%i, %s, bit)" size (string_of_order order)
+
+let rec combine = function
+  | [] -> Defs []
+  | (Defs defs) :: ast ->
+     let (Defs defs') = combine ast in
+     Defs (defs @ defs')
+
+let newtype name size order =
+  let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
+  ast_of_def_string order nt
+
+let full_getter name size order =
+  let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
+  let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
+  combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function]
+
+let full_setter name size order =
+  let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in
+  let fs_function = String.concat "\n"
+    [ Printf.sprintf "function _set_%s (r_ref, v) = {" name;
+                     "  r = _reg_deref(r_ref);";
+      Printf.sprintf "  r = Mk_%s(v);" name;
+                     "  (*r_ref) = r";
+                     "}"
+    ]
+  in
+  combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function]
+
+let full_overload name order =
+  ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name)
+
+let full_accessor name size order =
+  combine [full_getter name size order; full_setter name size order; full_overload name order]
+
+let index_range_getter' name field order start stop =
+  let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+  let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
+  let irg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v[%i .. %i]" field name start stop in
+  combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
+
+let index_range_setter' name field order start stop =
+  let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+  let irs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" field name (bitvec size order) in
+  let irs_function = String.concat "\n"
+    [ Printf.sprintf "function _set_%s (r_ref, v) = {" field;
+      Printf.sprintf "  r = _get_%s(_reg_deref(r_ref));" name;
+      Printf.sprintf "  r[%i .. %i] = v;" start stop;
+      Printf.sprintf "  (*r_ref) = Mk_%s(r)" name;
+                     "}"
+    ]
+  in
+  combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
+
+let index_range_overload field order =
+  ast_of_def_string order (Printf.sprintf "overload _mod_%s = {_get_%s, _set_%s}" field field field)
+
+let index_range_accessor name field order (BF_aux (bf_aux, l)) =
+  let getter n m = index_range_getter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+  let setter n m = index_range_setter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+  let overload = index_range_overload field order in
+  match bf_aux with
+  | BF_single n -> combine [getter n n; setter n n; overload]
+  | BF_range (n, m) -> combine [getter n m; setter n m; overload]
+  | BF_concat _ -> failwith "Unimplemented"
+
+let field_accessor name order (id, ir) = index_range_accessor name (string_of_id id) order ir
+
+let macro id size order ranges =
+  let name = string_of_id id in
+  combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges)