diff options
author | Son Ho | 2023-11-29 15:47:42 +0100 |
---|---|---|
committer | Son Ho | 2023-11-29 15:47:42 +0100 |
commit | 3aa9c531db4e9cde25a4a149a64e3ff730ed798b (patch) | |
tree | 3da4856892cf72d4182395bbacade06062b76aac | |
parent | dc4b11689131bdb41a43e5aca76538556a3a120c (diff) |
Fix a minor issue with the extraction
-rw-r--r-- | compiler/ExtractTypes.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 66418410..3657627b 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -192,12 +192,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit) F.pp_print_space fmt (); extract_expr false arg1 | _ -> + let binop_is_shift = match binop with Shl | Shr -> true | _ -> false in let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; - (* In the case of F*, because machine integers are simply integers - with a refinement, if the second argument is a constant we - need to provide the second implicit type argument *) - if !backend = FStar && is_const arg1 then ( + (* In the case of F*, for shift operations, because machine integers + are simply integers with a refinement, if the second argument is a + constant we need to provide the second implicit type argument *) + if binop_is_shift && !backend = FStar && is_const arg1 then ( F.pp_print_space fmt (); let ty = ty_as_integer arg1.ty in F.pp_print_string fmt |