diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 37 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | src/state.ml | 30 |
3 files changed, 42 insertions, 27 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index d28a2b6e..83b6901a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -225,14 +225,18 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) = | Typ_tup ts -> List.fold_left (fun s t -> NexpSet.union s (trec t)) NexpSet.empty ts + | Typ_app(Id_aux (Id "bitvector", _), [ + A_aux (A_nexp m, _); + A_aux (A_order ord, _)]) -> + let m = nexp_simp m in + if !opt_mwords && not (is_nexp_constant m) then + NexpSet.singleton (orig_nexp m) + else trec bit_typ | Typ_app(Id_aux (Id "vector", _), [ A_aux (A_nexp m, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)]) -> - let m = nexp_simp m in - if !opt_mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then - NexpSet.singleton (orig_nexp m) - else trec elem_typ + trec elem_typ | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) -> trec etyp | Typ_app(Id_aux (Id "range", _),_) @@ -280,15 +284,17 @@ let doc_typ_lem, doc_atomic_typ_lem = A_aux (A_nexp m, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)]) -> - let tpp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when !opt_mwords -> + let tpp = string "list" ^^ space ^^ typ elem_typ in + if atyp_needed then parens tpp else tpp + | Typ_app(Id_aux (Id "bitvector", _), [ + A_aux (A_nexp m, _); + A_aux (A_order ord, _)]) -> + let tpp = + if !opt_mwords then string "mword " ^^ doc_nexp_lem (nexp_simp m) - (* (match nexp_simp m with - | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i - | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m] - | _ -> raise (Reporting.err_unreachable l __POS__ - "cannot pretty-print bitvector type with non-constant length")) *) - | _ -> string "list" ^^ space ^^ typ elem_typ in + else + string "list" ^^ space ^^ typ bit_typ + in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in @@ -458,9 +464,8 @@ let rec typeclass_nexps (Typ_aux(t,l)) = -> NexpSet.empty | Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) - | Typ_app (Id_aux (Id "vector",_), - [A_aux (A_nexp size_nexp,_); - _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) + | Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp size_nexp,_)]) | Typ_app (Id_aux (Id "itself",_), [A_aux (A_nexp size_nexp,_)]) -> let size_nexp = nexp_simp size_nexp in @@ -865,7 +870,7 @@ let doc_exp_lem, doc_let_lem = | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = - if is_vector_typ t then vector_start_index t, vector_typ_args_of t + if is_vector_typ t || is_bitvector_typ t then vector_start_index t, vector_typ_args_of t else raise (Reporting.err_unreachable l __POS__ "E_vector of non-vector type") in let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in diff --git a/src/rewrites.ml b/src/rewrites.ml index 41319b45..6c38c689 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2070,7 +2070,7 @@ let rewrite_vector_concat_assignments env defs = match e_aux with | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) -> let typ = Env.base_typ_of env (typ_of exp) in - if is_vector_typ typ then + if is_vector_typ typ || is_bitvector_typ typ then (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) let start = vector_start_index typ in let (_, ord, etyp) = vector_typ_args_of typ in diff --git a/src/state.ml b/src/state.ml index 86fd8395..9d79fef0 100644 --- a/src/state.ml +++ b/src/state.ml @@ -106,20 +106,30 @@ let generate_initial_regstate defs = string_of_nexp nexp | Typ_app (id, [A_aux (A_nexp nexp, _); _]) when string_of_id id = "range" -> string_of_nexp nexp + | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant len, _)), _); _]) + when string_of_id id = "bitvector" -> + (* Output a literal binary zero value if this is a bitvector + and the environment has a default indexing order (required + by the typechecker for binary and hex literals) *) + let literal_bitvec = has_default_order defs in + let init_elem = if literal_bitvec then "0" else lookup_init_val vals bit_typ in + let rec elems len = + if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else + init_elem :: elems (Nat_big_num.pred len) + in + if literal_bitvec then + "0b" ^ (String.concat "" (elems len)) + else + "[" ^ (String.concat ", " (elems len)) ^ "]" | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ; A_aux (A_typ etyp, _)]) when string_of_id id = "vector" -> - (* Output a list of initial values of the vector elements, or a - literal binary zero value if this is a bitvector and the - environment has a default indexing order (required by the - typechecker for binary and hex literals) *) - let literal_bitvec = is_bit_typ etyp && has_default_order defs in - let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in + (* Output a list of initial values of the vector elements. *) + let init_elem = lookup_init_val vals etyp in let rec elems len = if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else init_elem :: elems (Nat_big_num.pred len) in - if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else "[" ^ (String.concat ", " (elems len)) ^ "]" | Typ_app (id, args) -> Bindings.find id vals args | Typ_tup typs -> @@ -188,7 +198,7 @@ let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with | _ -> raise (Reporting.err_typ l "Unsupported register type") in - let builtins = IdSet.of_list (List.map mk_id ["vector"; "list"; "option"]) in + let builtins = IdSet.of_list (List.map mk_id ["vector"; "bitvector"; "list"; "option"]) in if IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) then id else append_id id (String.concat "_" ("" :: List.map name_arg args)) | _ -> raise (Reporting.err_typ l "Unsupported register type") @@ -207,7 +217,7 @@ let register_base_types mwords typs = List.fold_left add_typ_arg typs args | _ -> Bindings.add (regval_constr_id mwords typ) typ typs in - List.fold_left add_base_typs Bindings.empty typs + List.fold_left add_base_typs Bindings.empty (bit_typ :: typs) let generate_regval_typ typs = let constr (constr_id, typ) = @@ -241,7 +251,7 @@ let add_regval_conv id typ (Defs defs) = append_ast (Defs defs) cdefs let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with - | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) -> + | Typ_app _ when (is_vector_typ typ || is_bitvector_typ typ) && not (mwords && is_bitvector_typ typ) -> let size, ord, etyp = vector_typ_args_of typ in let size = string_of_nexp (nexp_simp size) in let is_inc = if is_order_inc ord then "true" else "false" in |