feat(backend/fstar): patterns: allow shallow POr

Fixes #462
cryspen · Jan 29, 2024 · 327729d · 327729d
1 parent 7a7fcf9
commit 327729d
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -331,7 +331,10 @@ struct
     | GConst e -> pexpr e
     | GLifetime _ -> .
 
-  and ppat (p : pat) =
+  and ppat (p : pat) = ppat' true p
+
+  and ppat' (shallow : bool) (p : pat) =
+    let ppat = ppat' false in
     match p.p with
     | PWild -> F.wild
     | PAscription { typ; pat } ->
@@ -345,8 +348,7 @@ struct
           typ = _ (* we skip type annot here *);
         } ->
         F.pat @@ F.AST.PatVar (plocal_ident var, None, [])
-    | POr { subpats } ->
-        Error.unimplemented p.span ~details:"ppat:Disjuntive patterns"
+    | POr { subpats } -> F.pat @@ F.AST.PatOr (List.map ~f:ppat subpats)
     | 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