From 33c2e4da77cc155dd0bcb46e4335053c821546dd Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 2 Oct 2024 13:54:47 +0200 Subject: [PATCH] fix(engine/f*): convert an unimplemented to an assertion failure Thus this PR removes the unimplemented error in favor of an assertion failure. --- engine/backends/fstar/fstar_backend.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 667db2f41..ba3cc0c14 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -405,8 +405,9 @@ struct | POr { subpats } when shallow -> F.pat @@ F.AST.PatOr (List.map ~f:ppat subpats) | POr _ -> - Error.unimplemented ~issue_id:463 p.span - ~details:"The F* backend doesn't support nested disjuntive patterns" + Error.assertion_failure p.span + "Nested disjuntive patterns should have been eliminated by phase \ + `HoistDisjunctions` (see PR #830)." | PArray { args } -> F.pat @@ F.AST.PatList (List.map ~f:ppat args) | PConstruct { name = `TupleCons 0; args = [] } -> F.pat @@ F.AST.PatConst F.Const.Const_unit