fix(engine/f*): better error for #464

cryspen · Apr 11, 2024 · 2ee041e · 2ee041e
1 parent e8140e4
commit 2ee041e
Showing 1 changed file with 8 additions and 5 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -127,13 +127,16 @@ struct
           | S32 -> Int32
           | S64 -> Int64
           | S128 ->
-              Error.unimplemented
-                ~details:
-                  "128 literals (fail if pattern maching, otherwise TODO)" span
+              Error.unimplemented ~issue_id:464
+                ~details:"Matching on u128 or i128 literals is unsupported."
+                span
           | SSize ->
-              Error.unimplemented
+              Error.unimplemented ~issue_id:464
                 ~details:
-                  "usize literals (fail if pattern maching, otherwise TODO)"
+                  "Matching on usize or isize literals is unsupported. As a \
+                   work-around, instead of `match expr { 0 => ... }`, please \
+                   cast for instance to `u64` before: `match expr as u64 { 0 \
+                   => ... }`."
                 span
         in
         F.Const.Const_int