From 2ee041ed2d3dae29d90149ec8ba0238c843d6432 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 11 Apr 2024 17:52:56 +0200 Subject: [PATCH 1/4] fix(engine/f*): better error for #464 --- engine/backends/fstar/fstar_backend.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index ba830aace..672d42a4c 100644 --- 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 From 862afa4b2cf61d78d095b62c54562f35a7c0b560 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Sat, 13 Apr 2024 16:08:38 +0200 Subject: [PATCH 2/4] Update engine/backends/fstar/fstar_backend.ml Co-authored-by: Franziskus Kiefer --- engine/backends/fstar/fstar_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 672d42a4c..78ad2df7c 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -133,7 +133,7 @@ struct | SSize -> Error.unimplemented ~issue_id:464 ~details: - "Matching on usize or isize literals is unsupported. As a \ + "Matching on usize or isize literals is not yet supported. As a \ work-around, instead of `match expr { 0 => ... }`, please \ cast for instance to `u64` before: `match expr as u64 { 0 \ => ... }`." From b27824cbb87c8e6636f5165b33ff7b2db27e84ad Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Sat, 13 Apr 2024 16:08:45 +0200 Subject: [PATCH 3/4] Update engine/backends/fstar/fstar_backend.ml Co-authored-by: Franziskus Kiefer --- engine/backends/fstar/fstar_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 78ad2df7c..d015c27e9 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -128,7 +128,7 @@ struct | S64 -> Int64 | S128 -> Error.unimplemented ~issue_id:464 - ~details:"Matching on u128 or i128 literals is unsupported." + ~details:"Matching on u128 or i128 literals is not yet supported." span | SSize -> Error.unimplemented ~issue_id:464 From 4bbeac0b08df1ffe17dbb7af9ec3369097768343 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 15 Apr 2024 13:57:59 +0200 Subject: [PATCH 4/4] chore: `dune fmt` --- engine/backends/fstar/fstar_backend.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index d015c27e9..b49966631 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -128,15 +128,15 @@ struct | S64 -> Int64 | S128 -> Error.unimplemented ~issue_id:464 - ~details:"Matching on u128 or i128 literals is not yet supported." - span + ~details: + "Matching on u128 or i128 literals is not yet supported." span | SSize -> Error.unimplemented ~issue_id:464 ~details: - "Matching on usize or isize literals is not yet supported. As a \ - work-around, instead of `match expr { 0 => ... }`, please \ - cast for instance to `u64` before: `match expr as u64 { 0 \ - => ... }`." + "Matching on usize or isize literals is not yet supported. \ + 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