Skip to content

fix(engine) Add ascription to match scrutinees. #1208

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 24, 2024
Merged

fix(engine) Add ascription to match scrutinees. #1208

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions engine/lib/ast_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,6 +367,10 @@ module Make (F : Features.T) = struct
bounds_impls;
};
}
(* Match scrutinees need to be ascribed as well
(see https://github.com/hacspec/hax/issues/1207).*)
| Match { scrutinee; arms } ->
{ e with e = Match { scrutinee = ascribe scrutinee; arms } }
| _ ->
(* Ascribe the return type of a function application & constructors *)
if (ascribe_app && is_app e.e) || [%matches? Construct _] e.e
Expand Down
10 changes: 5 additions & 5 deletions test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,22 +254,22 @@ type t_T =
| T_t2 : t_T

let t_T_cast_to_repr (x: t_T) : isize =
match x with
match x <: t_T with
| T_t1 -> isz 0
| T_t2 -> isz 1

let rec hf (x: t_T) : t_T =
match x with
match x <: t_T with
| T_t1 -> hf (T_t2 <: t_T)
| T_t2 -> x

let rec g1 (x: t_T) : t_T =
match x with
match x <: t_T with
| T_t1 -> g2 x
| T_t2 -> T_t1 <: t_T

and g2 (x: t_T) : t_T =
match x with
match x <: t_T with
| T_t1 -> g1 x
| T_t2 -> hf x
'''
Expand Down Expand Up @@ -341,7 +341,7 @@ type t_T1 = | T1_T1 : t_T1

type t_T = | T_T : t_T1 -> t_T

let t_T1_cast_to_repr (x: t_T1) : isize = match x with | T1_T1 -> isz 0
let t_T1_cast_to_repr (x: t_T1) : isize = match x <: t_T1 with | T1_T1 -> isz 0

type t_T2 = | T2_T2 : t_T -> t_T2

Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ type t_EnumWithRepr =
| EnumWithRepr_ImplicitDiscrEmptyStruct : t_EnumWithRepr

let t_EnumWithRepr_cast_to_repr (x: t_EnumWithRepr) : u16 =
match x with
match x <: t_EnumWithRepr with
| EnumWithRepr_ExplicitDiscr1 -> discriminant_EnumWithRepr_ExplicitDiscr1
| EnumWithRepr_ExplicitDiscr2 -> discriminant_EnumWithRepr_ExplicitDiscr2
| EnumWithRepr_ImplicitDiscrEmptyTuple -> discriminant_EnumWithRepr_ExplicitDiscr2 +! 1us
Expand Down
82 changes: 46 additions & 36 deletions test-harness/src/snapshots/toolchain__guards into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,78 +33,88 @@ open Core
open FStar.Mul

let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_None -> 0l
| _ ->
match
match x with
| Core.Option.Option_Some v ->
(match v with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32
(match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some v ->
(match v <: Core.Result.t_Result i32 i32 with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
<:
Core.Option.t_Option i32
with
| Core.Option.Option_Some y -> y
| Core.Option.Option_None ->
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some (Core.Result.Result_Err y) -> y
| _ -> 1l

let if_guard (x: Core.Option.t_Option i32) : i32 =
match
match x with
| Core.Option.Option_Some v ->
(match v >. 0l with
| true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32
(match x <: Core.Option.t_Option i32 with
| Core.Option.Option_Some v ->
(match v >. 0l <: bool with
| true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
<:
Core.Option.t_Option i32
with
| Core.Option.Option_Some x -> x
| Core.Option.Option_None -> 0l

let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_None -> 0l
| _ ->
match
match x with
| Core.Option.Option_Some v ->
(match v with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32
(match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some v ->
(match v <: Core.Result.t_Result i32 i32 with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
<:
Core.Option.t_Option i32
with
| Core.Option.Option_Some x -> x
| Core.Option.Option_None ->
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some (Core.Result.Result_Err y) -> y
| _ -> 1l

let multiple_guards (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_None -> 0l
| _ ->
match
match x with
| Core.Option.Option_Some (Core.Result.Result_Ok v) ->
(match Core.Option.Option_Some (v +! 1l) <: Core.Option.t_Option i32 with
| Core.Option.Option_Some 1l -> Core.Option.Option_Some 0l <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32
(match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some (Core.Result.Result_Ok v) ->
(match Core.Option.Option_Some (v +! 1l) <: Core.Option.t_Option i32 with
| Core.Option.Option_Some 1l -> Core.Option.Option_Some 0l <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
<:
Core.Option.t_Option i32
with
| Core.Option.Option_Some x -> x
| Core.Option.Option_None ->
match
match x with
| Core.Option.Option_Some v ->
(match v with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32
(match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some v ->
(match v <: Core.Result.t_Result i32 i32 with
| Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
| _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
<:
Core.Option.t_Option i32
with
| Core.Option.Option_Some x -> x
| Core.Option.Option_None ->
match x with
match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
| Core.Option.Option_Some (Core.Result.Result_Err y) -> y
| _ -> 1l
'''
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__let-else into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,12 @@ open Core
open FStar.Mul

let let_else (opt: Core.Option.t_Option u32) : bool =
match opt with
match opt <: Core.Option.t_Option u32 with
| Core.Option.Option_Some x -> true
| _ -> false

let let_else_different_type (opt: Core.Option.t_Option u32) : bool =
match opt with
match opt <: Core.Option.t_Option u32 with
| Core.Option.Option_Some x ->
let_else (Core.Option.Option_Some (x +! 1ul <: u32) <: Core.Option.t_Option u32)
| _ -> false
Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__literals into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ let numeric (_: Prims.unit) : Prims.unit =

let patterns (_: Prims.unit) : Prims.unit =
let _:Prims.unit =
match 1uy with
match 1uy <: u8 with
| 2uy -> () <: Prims.unit
| _ -> () <: Prims.unit
in
Expand Down
9 changes: 9 additions & 0 deletions test-harness/src/snapshots/toolchain__loops into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,9 @@ let impl__M__decoded_message (self: t_M)
(Core.Ops.Control_flow.t_ControlFlow
(Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
(Prims.unit & Prims.unit)) Prims.unit)
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) Prims.unit
with
| Core.Ops.Control_flow.ControlFlow_Break ret -> ret
| Core.Ops.Control_flow.ControlFlow_Continue _ ->
Expand Down Expand Up @@ -188,6 +191,8 @@ let double_sum2_return (v: t_Slice i32) : i32 =
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & (i32 & i32))) (i32 & i32))
<:
Core.Ops.Control_flow.t_ControlFlow i32 (i32 & i32)
with
| Core.Ops.Control_flow.ControlFlow_Break ret -> ret
| Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2) -> sum +! sum2
Expand Down Expand Up @@ -218,6 +223,8 @@ let double_sum_return (v: t_Slice i32) : i32 =
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
<:
Core.Ops.Control_flow.t_ControlFlow i32 i32
with
| Core.Ops.Control_flow.ControlFlow_Break ret -> ret
| Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
Expand Down Expand Up @@ -314,6 +321,8 @@ let nested_return (_: Prims.unit) : i32 =
<:
Core.Ops.Control_flow.t_ControlFlow
(Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
<:
Core.Ops.Control_flow.t_ControlFlow i32 i32
with
| Core.Ops.Control_flow.ControlFlow_Break ret -> ret
| Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
Expand Down
12 changes: 6 additions & 6 deletions test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,38 +38,38 @@ type t_E =
| E_B : t_E

let t_E_cast_to_repr (x: t_E) : isize =
match x with
match x <: t_E with
| E_A -> isz 0
| E_B -> isz 1

let bar (x: t_E) : Prims.unit = match x with | E_A | E_B -> () <: Prims.unit
let bar (x: t_E) : Prims.unit = match x <: t_E with | E_A | E_B -> () <: Prims.unit

let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
match x with
match x <: (i32 & Core.Option.t_Option i32) with
| 1l, Core.Option.Option_Some 3l
| 1l, Core.Option.Option_Some 4l
| 2l, Core.Option.Option_Some 3l
| 2l, Core.Option.Option_Some 4l -> 0l
| x, _ -> x

let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
match x with
match x <: Core.Result.t_Result (i32 & i32) (i32 & i32) with
| Core.Result.Result_Ok (1l, x)
| Core.Result.Result_Ok (2l, x)
| Core.Result.Result_Err (3l, x)
| Core.Result.Result_Err (4l, x) -> x
| Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x

let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
match x with
match x <: (i32 & Core.Option.t_Option i32) with
| 1l, Core.Option.Option_Some 3l
| 1l, Core.Option.Option_Some 4l
| 2l, Core.Option.Option_Some 3l
| 2l, Core.Option.Option_Some 4l -> 0l
| x, _ -> x

let nested (x: Core.Option.t_Option i32) : i32 =
match x with
match x <: Core.Option.t_Option i32 with
| Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
| Core.Option.Option_Some x -> x
| Core.Option.Option_None -> 0l
Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__patterns into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,5 +37,5 @@ type t_Other = | Other : i32 -> t_Other

type t_Test = | Test_C1 : t_Other -> t_Test

let impl__test (self: t_Test) : i32 = match self with | Test_C1 c -> c._0
let impl__test (self: t_Test) : i32 = match self <: t_Test with | Test_C1 c -> c._0
'''
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__reordering into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ type t_Foo =
type t_Bar = | Bar : t_Foo -> t_Bar

let t_Foo_cast_to_repr (x: t_Foo) : isize =
match x with
match x <: t_Foo with
| Foo_A -> isz 0
| Foo_B -> isz 1

Expand Down
Loading
Loading