diff options
Diffstat (limited to 'src/ast_util.ml')
| -rw-r--r-- | src/ast_util.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index d26e12ed..7d2d320b 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -612,8 +612,8 @@ let rec string_of_exp (E_aux (exp, _)) = | E_comment _ -> "INTERNAL COMMENT" | E_comment_struc _ -> "INTERNAL COMMENT STRUC" | E_internal_let _ -> "INTERNAL LET" - | E_internal_return _ -> "INTERNAL RETURN" - | E_internal_plet _ -> "INTERNAL PLET" + | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")" + | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body | _ -> "INTERNAL" and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) = string_of_id field ^ " = " ^ string_of_exp exp @@ -704,6 +704,14 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) = | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id)) | LEXP_memory (id, exps) -> rewrap (E_app (id, exps)) +let destruct_range (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]) + when string_of_id f = "atom" -> Some (n, n) + | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) + when string_of_id f = "range" -> Some (n1, n2) + | _ -> None + let rec is_number (Typ_aux (t,_)) = match t with | Typ_id (Id_aux (Id "int", _)) @@ -819,6 +827,8 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = wrap (E_app (mk_id "undefined_bitvector", undefined_of_typ_args mwords l annot start @ undefined_of_typ_args mwords l annot size)) typ + | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp i, _)]) when string_of_id atom = "atom" -> + wrap (E_sizeof i) typ | Typ_app (id, args) -> wrap (E_app (prepend_id "undefined_" id, List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ |