Skip to content

Commit

Permalink
chore: update tests
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Jan 30, 2024
1 parent ad559f1 commit 514810c
Show file tree
Hide file tree
Showing 2 changed files with 89 additions and 0 deletions.
48 changes: 48 additions & 0 deletions test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
Original file line number Diff line number Diff line change
@@ -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.
'''
41 changes: 41 additions & 0 deletions test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
Original file line number Diff line number Diff line change
@@ -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
'''

0 comments on commit 514810c

Please sign in to comment.