From 514810c33a2b7c8bf008b66157dafca23f209c81 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Mon, 29 Jan 2024 16:20:24 +0100
Subject: [PATCH] chore: update tests

---
 .../toolchain__pattern-or into-coq.snap       | 48 +++++++++++++++++++
 .../toolchain__pattern-or into-fstar.snap     | 41 ++++++++++++++++
 2 files changed, 89 insertions(+)
 create mode 100644 test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
 create mode 100644 test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap

diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
new file mode 100644
index 000000000..82e366f35
--- /dev/null
+++ b/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.
+'''
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
new file mode 100644
index 000000000..71a3d94b7
--- /dev/null
+++ b/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
+'''