Skip to content

Commit

Permalink
New snapshots for coq
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Feb 12, 2024
1 parent 92a30ee commit 5c33d72
Show file tree
Hide file tree
Showing 3 changed files with 86 additions and 94 deletions.
167 changes: 79 additions & 88 deletions test-harness/src/snapshots/toolchain__naming into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,55 +24,6 @@ exit = 0
diagnostics = []

[stdout.files]
"Naming.Ambiguous_names.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.

(*Not implemented yet? todo(item)*)

Definition debug (label : int32) (value : int32) : unit :=
let _ := (v__print (impl_2__new_v1 (unsize (array_from_list [[;
] a=;

])) (unsize (array_from_list [impl_1__new_display label;
impl_1__new_display value])))) : unit in
tt.

Definition f (_ : unit) : unit :=
let a_1 := ((@repr WORDSIZE32 104)) : int32 in
let a_2 := ((@repr WORDSIZE32 205)) : int32 in
let a_3 := ((@repr WORDSIZE32 306)) : int32 in
let a := ((@repr WORDSIZE32 123)) : int32 in
let _ := (debug (@repr WORDSIZE32 3) a_3) : unit in
let _ := (debug (@repr WORDSIZE32 2) a_2) : unit in
let _ := (debug (@repr WORDSIZE32 1) a_1) : unit in
debug (@repr WORDSIZE32 4) a.

Definition ff_expand (_ : unit) : unit :=
let a := ((@repr WORDSIZE32 104)) : int32 in
let a := ((@repr WORDSIZE32 205)) : int32 in
let a := ((@repr WORDSIZE32 306)) : int32 in
let a := ((@repr WORDSIZE32 123)) : int32 in
let _ := (debug (@repr WORDSIZE32 3) a) : unit in
let _ := (debug (@repr WORDSIZE32 2) a) : unit in
let _ := (debug (@repr WORDSIZE32 1) a) : unit in
debug (@repr WORDSIZE32 0) a.
'''
"Naming.F.G.Impl_1.G.Hello.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.

Definition h (_ : unit) : unit :=
tt.
'''
"Naming.v" = '''
(* File automatically generated by Hacspec *)
From Hacspec Require Import Hacspec_Lib MachineIntegers.
Expand All @@ -81,43 +32,37 @@ Import List.ListNotations.
Open Scope Z_scope.
Open Scope bool_scope.

Record Foo_B : Type :={
f_x : uint_size;
}.
Inductive t_Foo : Type :=
| Foo_At_Foo
| Foo_A : t_Foo
| Foo_B : Foo_B -> t_Foo.

Definition impl__Foo__f (self : t_Foo_t) : t_Foo_t :=
Foo_At_Foo_t.

Record Foo2_B : Type :={
f_x : uint_size;
}.
Inductive t_Foo2 : Type :=
| Foo2_At_Foo2
| Foo2_A : t_Foo2
| Foo2_B : Foo2_B -> t_Foo2.

Class t_FooTrait Self := {
f_ASSOCIATED_CONSTANT:uint_size ;
Class t_FooTrait (Self : Type) := {
f_ASSOCIATED_CONSTANT : uint_size ;
}.

Class t_T1 Self := {
Class t_T1 (Self : Type) := {
}.

Instance t_Foo_t_t_T1 : t_T1 t_Foo_t := {
#[global] Instance t_Foo_t_t_T1 : t_T1 t_Foo_t := {
}.

Instance (t_Foo_t × int8)_t_T1 : t_T1 (t_Foo_t × int8) := {
#[global] Instance (t_Foo_t × int8)_t_T1 : t_T1 (t_Foo_t × int8) := {
}.

Class t_T2_for_a Self := {
Class t_T2_for_a (Self : Type) := {
}.

Class t_T3_e_for_a Self := {
Class t_T3_e_for_a (Self : Type) := {
}.

Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := {
#[global] Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := {
}.

(*Not implemented yet? todo(item)*)
Expand All @@ -133,11 +78,8 @@ Definition constants (_ : unit) : uint_size :=
Definition ff__g (_ : unit) : unit :=
tt.

Record C_f__g__impl__g__Foo_B : Type :={
f_x : uint_size;
}.
Inductive t_f__g__impl__g__Foo : Type :=
| C_f__g__impl__g__Foo_At_f__g__impl__g__Foo
| C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
| C_f__g__impl__g__Foo_B : C_f__g__impl__g__Foo_B -> t_f__g__impl__g__Foo.

Definition ff__g__impl_1__g (self : t_Foo_t) : uint_size :=
Expand All @@ -148,53 +90,53 @@ Definition ff__g__impl_1__g (self : t_Foo_t) : uint_size :=
Definition reserved_names (val : int8) (noeq : int8) (of : int8) : int8 :=
(val.+noeq).+of.

Record t_Arity1 : Type :={
Record t_Arity1 (T : _) : Type := {
0 : T;
}.

Instance t_Arity1_t (t_Foo_t × int8)_t_T2_for_a : t_T2_for_a t_Arity1_t (t_Foo_t × int8) := {
#[global] Instance t_Arity1_t ((t_Foo_t × int8))_t_T2_for_a : t_T2_for_a t_Arity1_t ((t_Foo_t × int8)) := {
}.

Record t_B : Type :={
Record t_B : Type := {
}.

Definition impl__B__f (self : t_B_t) : t_B_t :=
Bt_B_t.

Record t_C : Type :={
Record t_C : Type := {
f_x : uint_size;
}.

Record t_Foobar : Type :={
Record t_Foobar : Type := {
f_a : t_Foo_t;
}.

Record t_StructA : Type :={
Record t_StructA : Type := {
f_a : uint_size;
}.

Record t_StructB : Type :={
f_b : uint_size;
Record t_StructB : Type := {
f_a : uint_size;
f_b : uint_size;
}.

Record t_StructC : Type :={
Record t_StructC : Type := {
f_a : uint_size;
}.

Record t_StructD : Type :={
f_b : uint_size;
Record t_StructD : Type := {
f_a : uint_size;
f_b : uint_size;
}.

Record t_X : Type :={
Record t_X : Type := {
}.

Definition construct_structs (a : uint_size) (b : uint_size) : unit :=
let _ := (Build_StructA a) : t_StructA_t in
let _ := (Build_StructB ab) : t_StructB_t in
let _ := (Build_StructC a) : t_StructC_t in
let _ := (Build_StructD ab) : t_StructD_t in
let _ := Build_StructA (f_a := a) : t_StructA_t in
let _ := Build_StructB (f_a := a) (f_b := b) : t_StructB_t in
let _ := Build_StructC (f_a := a) : t_StructC_t in
let _ := Build_StructD (f_a := a) (f_b := b) : t_StructD_t in
tt.

Definition f (x : t_Foobar_t) : uint_size :=
Expand All @@ -204,7 +146,56 @@ Definition ff__g__impl__g (self : t_B_t) : uint_size :=
(@repr WORDSIZE32 0).

Definition mk_c (_ : unit) : t_C_t :=
let _ := (Build_Foo_B (@repr WORDSIZE32 3)) : t_Foo_t in
let _ := (Xt_X_t) : t_X_t in
Build_C (@repr WORDSIZE32 3).
let _ := Build_Foo_B (f_x := (@repr WORDSIZE32 3)) : t_Foo_t in
let _ := Xt_X_t : t_X_t in
Build_C (f_x := (@repr WORDSIZE32 3)).
'''
"Naming_Ambiguous_names.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.

(*Not implemented yet? todo(item)*)

Definition debug (label : int32) (value : int32) : unit :=
let _ := v__print (impl_2__new_v1 (unsize (array_from_list [[;
] a=;

])) (unsize (array_from_list [impl_1__new_display label;
impl_1__new_display value]))) : unit in
tt.

Definition f (_ : unit) : unit :=
let a_1 := (@repr WORDSIZE32 104) : int32 in
let a_2 := (@repr WORDSIZE32 205) : int32 in
let a_3 := (@repr WORDSIZE32 306) : int32 in
let a := (@repr WORDSIZE32 123) : int32 in
let _ := debug (@repr WORDSIZE32 3) a_3 : unit in
let _ := debug (@repr WORDSIZE32 2) a_2 : unit in
let _ := debug (@repr WORDSIZE32 1) a_1 : unit in
debug (@repr WORDSIZE32 4) a.

Definition ff_expand (_ : unit) : unit :=
let a := (@repr WORDSIZE32 104) : int32 in
let a := (@repr WORDSIZE32 205) : int32 in
let a := (@repr WORDSIZE32 306) : int32 in
let a := (@repr WORDSIZE32 123) : int32 in
let _ := debug (@repr WORDSIZE32 3) a : unit in
let _ := debug (@repr WORDSIZE32 2) a : unit in
let _ := debug (@repr WORDSIZE32 1) a : unit in
debug (@repr WORDSIZE32 0) a.
'''
"Naming_F_G_Impl_1_G_Hello.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.

Definition h (_ : unit) : unit :=
tt.
'''
7 changes: 4 additions & 3 deletions test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,14 @@ Open Scope Z_scope.
Open Scope bool_scope.

Inductive t_E : Type :=
| E_At_E
| E_Bt_E.
| E_A : t_E
| E_B : t_E.

(*Not implemented yet? todo(item)*)

Definition bar (x : t_E_t) : unit :=
match x with
| E_A | E_B => tt
| E_A | E_B =>
tt
end.
'''
6 changes: 3 additions & 3 deletions test-harness/src/snapshots/toolchain__reordering into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ Open Scope Z_scope.
Open Scope bool_scope.

Inductive t_Foo : Type :=
| Foo_At_Foo
| Foo_Bt_Foo.
| Foo_A : t_Foo
| Foo_B : t_Foo.

(*Not implemented yet? todo(item)*)

Expand All @@ -47,7 +47,7 @@ Definition no_dependency_1_ (_ : unit) : unit :=
Definition no_dependency_2_ (_ : unit) : unit :=
tt.

Record t_Bar : Type :={
Record t_Bar : Type := {
0 : t_Foo_t;
}.

Expand Down

0 comments on commit 5c33d72

Please sign in to comment.