diff options
| author | Alasdair Armstrong | 2018-01-17 18:51:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-18 16:13:11 +0000 |
| commit | 952fcb88797a1771eb018e63e8446055e944e035 (patch) | |
| tree | 12cdc5f1054dfad02fa76abd22247564eb133a21 /src/pretty_print_sail.ml | |
| parent | 254b72f60388271058c6d259d5a98424e94cafc7 (diff) | |
Modified unification so Type_check.instantiation_of works after sizeof rewriting
This change allows the AST to be type-checked after sizeof
re-writing. It modifies the unification algorithm to better support
checking multiplication in constraints, by using division and modulus
SMT operators if they are defined.
Also made sure the typechecker doesn't re-introduce E_constraint
nodes, otherwise re-checking after sizeof-rewriting will re-introduce
constraint nodes.
Diffstat (limited to 'src/pretty_print_sail.ml')
| -rw-r--r-- | src/pretty_print_sail.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 887b15a0..43be7a00 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -74,6 +74,10 @@ 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, nexps) -> string (string_of_nexp nexp) + (* This segfaults??!!!! + doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps)) + *) | Nexp_id id -> doc_id id | Nexp_var kid -> doc_kid kid | _ -> parens (nexp0 nexp) |