Merge pull request #1208 from hacspec/ascribe-match-scrutinees

fix(engine) Add ascription to match scrutinees.
hacspec · Dec 24, 2024 · f47b2ae · f47b2ae
2 parents 08057f7 + 45d7cde
commit f47b2ae
Show file tree

Hide file tree

Showing 13 changed files with 107 additions and 81 deletions.
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -270,22 +270,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
 '''
@@ -325,7 +325,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
 

diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__guards into-fstar.snap b/test-harness/src/snapshots/toolchain__guards into-fstar.snap
@@ -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
 '''
diff --git a/test-harness/src/snapshots/toolchain__let-else into-fstar.snap b/test-harness/src/snapshots/toolchain__let-else into-fstar.snap
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -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 _ ->
@@ -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
@@ -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
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
@@ -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

diff --git a/test-harness/src/snapshots/toolchain__patterns into-fstar.snap b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap
@@ -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
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
@@ -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