diff options
| author | Thomas Bauereiss | 2019-12-03 17:06:20 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-12-03 17:06:20 +0000 |
| commit | dc0eb7b8a6fb3f000cd3b7249a7d5aae050ff918 (patch) | |
| tree | cced680f955cc550e3ffccd552accb86301b7718 /src/rewrites.ml | |
| parent | c8dc80c02cd32ccfb3609d5a5de30e3f8bbd5bf5 (diff) | |
Prover backends: Expand Int type synonyms in type definitions
... not just in type abbreviations.
Fixes an error in the RV32 build of CHERI-RISC-V.
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 4a78b5ba..20a1b336 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -257,11 +257,22 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a)) | DEF_type (TD_aux (TD_abbrev (id, typq, typ_arg), a)) -> DEF_type (TD_aux (TD_abbrev (id, typq, rewrite_typ_arg env typ_arg), a)) + | DEF_type (TD_aux (TD_record (id, typq, fields, b), a)) -> + let fields' = List.map (fun (t, id) -> (rewrite_typ env t, id)) fields in + DEF_type (TD_aux (TD_record (id, typq, fields', b), a)) + | DEF_type (TD_aux (TD_variant (id, typq, constrs, b), a)) -> + let constrs' = + List.map (fun (Tu_aux (Tu_ty_id (t, id), l)) -> + Tu_aux (Tu_ty_id (rewrite_typ env t, id), l)) + constrs + in + DEF_type (TD_aux (TD_variant (id, typq, constrs', b), a)) | d -> Rewriter.rewrite_def rewriters d in (fun env defs -> rewrite_defs_base { rewriters_base with - rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def env + rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); + rewrite_def = rewrite_def env } defs), rewrite_typ |