diff options
| -rw-r--r-- | src/toFromInterp_backend.ml | 4 | ||||
| -rw-r--r-- | src/toFromInterp_lib_bitlist.ml | 13 |
2 files changed, 15 insertions, 2 deletions
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index b787fad4..30b93d90 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -87,7 +87,7 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = in let fromValueKid (Kid_aux ((Var name), _)) = string ("typq_" ^ name) - in + in let fromValueNexp ((Nexp_aux (nexp_aux, annot)) as nexp) = match nexp_aux with | Nexp_constant num -> parens (separate space [string "Big_int.of_string"; dquotes (string (Nat_big_num.to_string num))]) | Nexp_var var -> fromValueKid var @@ -122,7 +122,7 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = (string " -> ") ^^ parens (separate comma_sp (List.mapi (fun i t -> fromValueTyp t (arg_name ^ "_tup" ^ string_of_int i)) typs))) | Typ_internal_unknown -> failwith "escaped Typ_internal_unknown" - in + in let fromValueVals ((Typ_aux (typ_aux, l)) as typ) = match typ_aux with | Typ_tup typs -> parens (separate comma_sp (List.mapi (fun i typ -> fromValueTyp typ ("v" ^ (string_of_int i))) typs)) | _ -> fromValueTyp typ "v0" diff --git a/src/toFromInterp_lib_bitlist.ml b/src/toFromInterp_lib_bitlist.ml index d47beca3..13912722 100644 --- a/src/toFromInterp_lib_bitlist.ml +++ b/src/toFromInterp_lib_bitlist.ml @@ -106,6 +106,19 @@ let zvectorToInterpValue typq_'n typq_'ord typq_'a v = let vectorFromInterpValue = zvectorFromInterpValue let vectorToInterpValue = zvectorToInterpValue +let zbitvectorFromInterpValue typq_'n typq_'ord v = match v with + | V_vector vs -> + assert (Big_int.of_int (List.length vs) = typq_'n); + vs + | _ -> failwith "invalid interpreter value for vector" + +let zbitvectorToInterpValue typq_'n typq_'ord v = + assert (Big_int.of_int (List.length v) = typq_'n); + V_vector v + +let bitvectorFromInterpValue = zvectorFromInterpValue +let bitvectorToInterpValue = zvectorToInterpValue + let zbitFromInterpValue v = match v with | V_bit b -> (match b with | Sail_lib.B0 -> BitT.b0 |