Skip to content

Commit

Permalink
Fix a minor issue with the extraction
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Nov 29, 2023
1 parent dc4b116 commit 3aa9c53
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions compiler/ExtractTypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 3aa9c53

Please sign in to comment.