diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/c_backend.ml | 13 | ||||
| -rw-r--r-- | src/sail_lib.ml | 2 | ||||
| -rw-r--r-- | src/value.ml | 2 |
3 files changed, 16 insertions, 1 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2b144d35..7491b3e3 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1844,6 +1844,9 @@ let codegen_list_clear id ctyp = ^^ string " sail_free(*rop);" ^^ string "}" +let codegen_list_recreate id = + string (Printf.sprintf "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id)) + let codegen_list_set id ctyp = string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ string " if (op == NULL) { *rop = NULL; return; };\n" @@ -1879,6 +1882,14 @@ let codegen_pick id ctyp = else string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) +let codegen_list_equal id ctyp = + let open Printf in + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n" + ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n" + ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) + ^^ string "}" + let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in if IdSet.mem id !generated then @@ -1889,9 +1900,11 @@ let codegen_list ctx ctyp = codegen_node id ctyp ^^ twice hardline ^^ codegen_list_init id ^^ twice hardline ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_recreate id ^^ twice hardline ^^ codegen_list_set id ctyp ^^ twice hardline ^^ codegen_cons id ctyp ^^ twice hardline ^^ codegen_pick id ctyp ^^ twice hardline + ^^ codegen_list_equal id ctyp ^^ twice hardline end (* Generate functions for working with non-bit vectors of some specific type. *) diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 03994657..90fc8aba 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -114,6 +114,8 @@ let rec undefined_vector (len, item) = then [] else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item) +let undefined_list _ = [] + let rec undefined_bitvector len = if Big_int.equal len Big_int.zero then [] diff --git a/src/value.ml b/src/value.ml index 3a9a071f..b166e99b 100644 --- a/src/value.ml +++ b/src/value.ml @@ -123,7 +123,7 @@ let rec string_of_value = function let rec eq_value v1 v2 = match v1, v2 with | V_vector v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s - | V_list v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s + | V_list v1s, V_list v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s | V_int n, V_int m -> Big_int.equal n m | V_real n, V_real m -> Rational.equal n m | V_bool b1, V_bool b2 -> b1 = b2 |