diff options
| author | Alasdair Armstrong | 2018-12-21 12:33:21 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-21 13:17:15 +0000 |
| commit | 06a6c63388bfdb0b31363a5fc09b7ead5d32d1cf (patch) | |
| tree | f1da88d6500a483d5bb1cde9057b68debb6a2d17 /src | |
| parent | 367f72900fd24bf51b135f04f6fd301f3e8efb15 (diff) | |
Expand synonyms in generated mapping val-specs
This ensures that mappings round-trip through the pretty-printer and
parser unchanged
Remove guarded_pats rewrite from C compilation. It causes a large
increase in compilation time due to how it interacts with flow
typing/pattern literal re-writing/and sizeof-rewriting
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index ea8ccaf9..8df5ce02 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5108,7 +5108,6 @@ let rewrite_defs_c = [ ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); - ("guarded_pats", rewrite_defs_guarded_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("constraint", rewrite_constraint); ("trivial_sizeof", rewrite_trivial_sizeof); diff --git a/src/type_check.ml b/src/type_check.ml index cb20ae2e..4d8c3bcf 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4327,7 +4327,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md typ_debug (lazy ("Checking mapdef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ))); let vs_def, env = if not have_val_spec then - [mk_val_spec env quant typ id], Env.add_val_spec id (quant, typ) env + [mk_val_spec env quant (Env.expand_synonyms env typ) id], Env.add_val_spec id (quant, typ) env else [], env in |