diff options
| author | Thomas Bauereiss | 2018-04-26 16:57:52 +0100 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-04-26 09:54:31 -0700 |
| commit | ea9c4452b2eb8aa255af911ef3cc1088fb80b1f8 (patch) | |
| tree | 9f45d4b5a41e316d86ed339b01dc6eaf31cb0797 /src | |
| parent | 4f46c33c21b70117cd6c93953ba9bf08c4cc72b9 (diff) | |
Lem: Add Size class annotations for nested bitvector types
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 15cd0512..f58c3fa6 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -439,7 +439,13 @@ let rec typeclass_nexps (Typ_aux(t,_)) = let size_nexp = nexp_simp size_nexp in if is_nexp_constant size_nexp then NexpSet.empty else NexpSet.singleton (orig_nexp size_nexp) - | Typ_app _ -> NexpSet.empty + | Typ_app (id, args) -> + let add_arg_nexps nexps = function + | Typ_arg_aux (Typ_arg_typ typ, _) -> + NexpSet.union nexps (typeclass_nexps typ) + | _ -> nexps + in + List.fold_left add_arg_nexps NexpSet.empty args | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) else NexpSet.empty |