Remove uid module #1253
Remove uid module #1253
Conversation
Halbaroth
force-pushed
the
remove-uid-module
branch
from
902243a to
da5d51c
Compare
This PR removes the interface Uid. We know use `term_cst` and `ty_cst` of Dolmen directly!
|
Strangely, it seems that the test |
There was a problem hiding this comment.
testfile-qfbv-timeout.unix.smt2 is known to be flaky at times. Although #1245 might have made it worse; I will look into it.
On the PR itself — nothing to say except a small nitpick on tcst_of_rounding_mode, looks good to me.
src/lib/frontend/translate.ml
Outdated
| @@ -748,14 +744,14 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = | |||
| match term_descr with | |||
| | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) -> | |||
| let ty = dty_to_ty id_ty in | |||
| let v = Var.of_string @@ Uid.show id in | |||
| let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in | |||
There was a problem hiding this comment.
| let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in | |
| let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in |
src/lib/frontend/translate.ml
Outdated
| let sy = Sy.Var v in | ||
| Cache.store_sy ty_c sy; | ||
| v, id, ty | ||
|
|
||
| | Var ({ builtin = B.Base; id_ty; _ } as ty_v) -> | ||
| let ty = dty_to_ty id_ty in | ||
| let v = Var.of_string @@ Uid.show id in | ||
| let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in |
There was a problem hiding this comment.
| let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in | |
| let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in |
src/lib/frontend/translate.ml
Outdated
| @@ -924,10 +920,9 @@ let mk_add translate sy ty l = | |||
| E.mk_term sy args ty | |||
|
|
|||
| let mk_rounding fpar = | |||
| let name = Hstring.make @@ Fpa_rounding.string_of_rounding_mode fpar in | |||
| let tcst = Fpa_rounding.tcst_of_rounding_mode fpar in | |||
There was a problem hiding this comment.
tcst_of_rounding_mode is a confusing name — the t before cst implies we want to distinguish with other kinds of constructors, but does t mean "term" or "type"?
I think this should be called either term_cst_of_rounding_mode (what a mouthful!) or cst_of_rounding_mode, which is as expressive as tcst_of_rounding_mode due to the ambiguity but less confusing.
This PR removes the interface Uid. We now use
term_cstandty_cstof Dolmen directly!