diff options
| author | Thomas Bauereiss | 2017-12-05 17:05:22 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-06 14:54:28 +0000 |
| commit | c3c3c40a1d4f81448d8356317e88be2b04363df7 (patch) | |
| tree | 4caeea3f28af968a59241df7a7ebd1828fd61086 /src/ast_util.mli | |
| parent | 4a7d6e6d7e9221a19bc50c627b5714e45b1748bc (diff) | |
Make AST after rewriting for Lem backend type-checkable
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
Diffstat (limited to 'src/ast_util.mli')
| -rw-r--r-- | src/ast_util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli index 2059bb7f..7e22a6e7 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -248,6 +248,7 @@ val is_bitvector_typ : typ -> bool val typ_app_args_of : typ -> string * typ_arg_aux list * Ast.l val vector_typ_args_of : typ -> nexp * nexp * order * typ +val destruct_range : typ -> (nexp * nexp) option val is_order_inc : order -> bool |