diff options
| author | Alasdair Armstrong | 2017-08-21 16:57:23 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-21 16:57:23 +0100 |
| commit | 8f9f30172204d75ff36d4c491802f460472cfa85 (patch) | |
| tree | 8f6848d36c365dad36e31e1556afa668bd8636bd /src/pretty_print_sail.ml | |
| parent | c310ad77dee2bec75c272556e4ec843f5d9f2715 (diff) | |
Modified sizeof rewriting pass so it can correctly deal with existentials.
Basically we needed to make the rewriting step for E_sizeof and
E_constraint more aggressively try to rewrite those expressions from
variables in scope, without adding new parameters to pass the type
variables at runtime, as this can break in the presence of existential
quantification. Still some cleanup to do in this code, but tests on
the arm spec show that it now introduces the minimal amount of new
parameters.
Diffstat (limited to 'src/pretty_print_sail.ml')
| -rw-r--r-- | src/pretty_print_sail.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index b6d33d6d..b0b63ec1 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -345,6 +345,7 @@ let doc_exp, doc_let = | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false *) + | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr) and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> (match ts with |