diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 5 |
4 files changed, 10 insertions, 0 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 396d72a3..03031767 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -374,6 +374,8 @@ let app_typ id args = mk_typ (Typ_app (id, args)) let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (A_typ typ)])) let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp (nexp_simp nexp))])) +let implicit_typ nexp = + mk_typ (Typ_app (mk_id "implicit", [mk_typ_arg (A_nexp (nexp_simp nexp))])) let range_typ nexp1 nexp2 = mk_typ (Typ_app (mk_id "range", [mk_typ_arg (A_nexp (nexp_simp nexp1)); mk_typ_arg (A_nexp (nexp_simp nexp2))])) diff --git a/src/ast_util.mli b/src/ast_util.mli index 7100cde7..4cbea3dc 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -124,6 +124,7 @@ val unknown_typ : typ val int_typ : typ val nat_typ : typ val atom_typ : nexp -> typ +val implicit_typ : nexp -> typ val range_typ : nexp -> nexp -> typ val bit_typ : typ val bool_typ : typ diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 3d5bd479..f30d5135 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -92,6 +92,8 @@ let rec doc_nexp = let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = match n_aux with | Nexp_constant c -> string (Big_int.to_string c) + | Nexp_app (Id_aux (DeIid op, _), [n1; n2]) -> + separate space [atomic_nexp n1; string op; atomic_nexp n2] | Nexp_app (id, nexps) -> string (string_of_nexp nexp) (* This segfaults??!!!! doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps)) diff --git a/src/type_check.ml b/src/type_check.ml index 77e45752..f31da5f4 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2025,6 +2025,11 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) = let exp2 = rewrite_sizeof' env nexp2 in mk_exp (E_app (mk_id "div", [exp1; exp2])) + | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "mod" -> + let exp1 = rewrite_sizeof' env nexp1 in + let exp2 = rewrite_sizeof' env nexp2 in + mk_exp (E_app (mk_id "mod", [exp1; exp2])) + | Nexp_app _ | Nexp_id _ -> typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")") |