Merge pull request #473 from hacspec/fstar-shallow-disj-pats

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

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,11 @@ 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 } when shallow ->
+        F.pat @@ F.AST.PatOr (List.map ~f:ppat subpats)
+    | POr _ ->
+        Error.unimplemented p.span ~issue_id:463
+          ~details:"The F* backend doesn't support nested disjuntive patterns"
     | 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

test-harness/src/snapshots/toolchain__pattern-or into-coq.snap

@@ -0,0 +1,48 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: coq
+  info:
+    name: pattern-or
+    manifest: pattern-or/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+---
+exit = 0
+stderr = '''
+Compiling pattern-or v0.1.0 (WORKSPACE_ROOT/pattern-or)
+    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Pattern_or.v" = '''
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Inductive t_E : Type :=
+| E_At_E
+| E_Bt_E.
+
+(*Not implemented yet? todo(item)*)
+
+Definition bar (x : t_E_t) : unit :=
+  match x with
+  | E_A  | E_B  => tt
+  end.
+'''

test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap

@@ -0,0 +1,41 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: pattern-or
+    manifest: pattern-or/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+---
+exit = 0
+stderr = '''
+Compiling pattern-or v0.1.0 (WORKSPACE_ROOT/pattern-or)
+    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Pattern_or.fst" = '''
+module Pattern_or
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_E =
+  | E_A : t_E
+  | E_B : t_E
+
+let bar (x: t_E) : Prims.unit = match x with | E_A  | E_B  -> () <: Prims.unit
+'''

tests/pattern-or/Cargo.toml

@@ -6,4 +6,5 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.hax-tests]
-into."coq" = { broken = false, snapshot = "none", issue_id = "161" }
+into."coq" = { issue_id = "161" }
+into."fstar" = { }