Skip to content

Commit

Permalink
Snapshots
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Oct 30, 2024
1 parent 9baef9a commit 390a82a
Show file tree
Hide file tree
Showing 9 changed files with 192 additions and 115 deletions.
5 changes: 4 additions & 1 deletion test-harness/src/snapshots/toolchain__assert into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,9 @@ From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.



(* NotImplementedYet *)

Definition asserts (_ : unit) : unit :=
let _ := assert (true) in
let _ := assert (t_PartialEq_f_eq (1) (1)) in
Expand All @@ -52,4 +54,5 @@ Definition asserts (_ : unit) : unit :=
| (left_val,right_val) =>
assert (negb (t_PartialEq_f_eq (left_val) (right_val)))
end in
tt.'''
tt.
'''
46 changes: 28 additions & 18 deletions test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,35 +41,45 @@ From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.


Definition discriminant_t_EnumWithRepr_ExplicitDiscr1 : t_u16 :=

Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
1.
Definition discriminant_t_EnumWithRepr_ExplicitDiscr2 : t_u16 :=

Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
5.

Inductive t_EnumWithRepr : Type :=
| t_EnumWithRepr_ExplicitDiscr1
| t_EnumWithRepr_ExplicitDiscr2
| t_EnumWithRepr_ImplicitDiscrEmptyTuple
| t_EnumWithRepr_ImplicitDiscrEmptyStruct.
| EnumWithRepr_ExplicitDiscr1
| EnumWithRepr_ExplicitDiscr2
| EnumWithRepr_ImplicitDiscrEmptyTuple
| EnumWithRepr_ImplicitDiscrEmptyStruct.
Arguments t_EnumWithRepr:clear implicits.
Arguments t_EnumWithRepr.

Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
match x with
| t_EnumWithRepr_ExplicitDiscr1 =>
discriminant_t_EnumWithRepr_ExplicitDiscr1
| t_EnumWithRepr_ExplicitDiscr2 =>
discriminant_t_EnumWithRepr_ExplicitDiscr2
| t_EnumWithRepr_ImplicitDiscrEmptyTuple =>
t_Add_f_add (discriminant_t_EnumWithRepr_ExplicitDiscr2) (1)
| t_EnumWithRepr_ImplicitDiscrEmptyStruct =>
t_Add_f_add (discriminant_t_EnumWithRepr_ExplicitDiscr2) (2)
| EnumWithRepr_ExplicitDiscr1 =>
discriminant_EnumWithRepr_ExplicitDiscr1
| EnumWithRepr_ExplicitDiscr2 =>
discriminant_EnumWithRepr_ExplicitDiscr2
| EnumWithRepr_ImplicitDiscrEmptyTuple =>
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (1)
| EnumWithRepr_ImplicitDiscrEmptyStruct =>
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2)
end.

(* NotImplementedYet *)

Definition f (_ : unit) : t_u32 :=
let v__x := cast (t_Add_f_add (discriminant_t_EnumWithRepr_ExplicitDiscr2) (0)) in
t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (t_EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (t_EnumWithRepr_ImplicitDiscrEmptyStruct))).
let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in
t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).

Definition ff__CONST : t_u16 :=
cast (t_Add_f_add (discriminant_t_EnumWithRepr_ExplicitDiscr1) (0)).
cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)).

Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
cast (t_EnumWithRepr_cast_to_repr (x)).

Definition get_repr (x : t_EnumWithRepr) : t_u16 :=
t_EnumWithRepr_cast_to_repr (x).'''
t_EnumWithRepr_cast_to_repr (x).
'''
90 changes: 48 additions & 42 deletions test-harness/src/snapshots/toolchain__guards into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,117 +40,123 @@ From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.



(* NotImplementedYet *)

Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| t_Option_None =>
| Option_None =>
0
| _ =>
match match x with
| t_Option_Some (v) =>
| Option_Some (v) =>
match v with
| t_Result_Ok (y) =>
t_Option_Some (y)
| Result_Ok (y) =>
Option_Some (y)
| _ =>
t_Option_None
Option_None
end
| _ =>
t_Option_None
Option_None
end with
| t_Option_Some (y) =>
| Option_Some (y) =>
y
| t_Option_None =>
| Option_None =>
match x with
| t_Option_Some (t_Result_Err (y)) =>
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
end
end
end.

Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
match match x with
| t_Option_Some (v) =>
| Option_Some (v) =>
match t_PartialOrd_f_gt (v) (0) with
| true =>
t_Option_Some (v)
Option_Some (v)
| _ =>
t_Option_None
Option_None
end
| _ =>
t_Option_None
Option_None
end with
| t_Option_Some (x) =>
| Option_Some (x) =>
x
| t_Option_None =>
| Option_None =>
0
end.

Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| t_Option_None =>
| Option_None =>
0
| _ =>
match match x with
| t_Option_Some (v) =>
| Option_Some (v) =>
match v with
| t_Result_Ok (y) =>
t_Option_Some (y)
| Result_Ok (y) =>
Option_Some (y)
| _ =>
t_Option_None
Option_None
end
| _ =>
t_Option_None
Option_None
end with
| t_Option_Some (x) =>
| Option_Some (x) =>
x
| t_Option_None =>
| Option_None =>
match x with
| t_Option_Some (t_Result_Err (y)) =>
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
end
end
end.

Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| t_Option_None =>
| Option_None =>
0
| _ =>
match match x with
| t_Option_Some (t_Result_Ok (v)) =>
match t_Option_Some (t_Add_f_add (v) (1)) with
| t_Option_Some (1) =>
t_Option_Some (0)
| Option_Some (Result_Ok (v)) =>
match Option_Some (t_Add_f_add (v) (1)) with
| Option_Some (1) =>
Option_Some (0)
| _ =>
t_Option_None
Option_None
end
| _ =>
t_Option_None
Option_None
end with
| t_Option_Some (x) =>
| Option_Some (x) =>
x
| t_Option_None =>
| Option_None =>
match match x with
| t_Option_Some (v) =>
| Option_Some (v) =>
match v with
| t_Result_Ok (y) =>
t_Option_Some (y)
| Result_Ok (y) =>
Option_Some (y)
| _ =>
t_Option_None
Option_None
end
| _ =>
t_Option_None
Option_None
end with
| t_Option_Some (x) =>
| Option_Some (x) =>
x
| t_Option_None =>
| Option_None =>
match x with
| t_Option_Some (t_Result_Err (y)) =>
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
end
end
end
end.'''
end.
'''
20 changes: 19 additions & 1 deletion test-harness/src/snapshots/toolchain__include-flag into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.



Record t_Foo : Type :=
{
}.
Expand All @@ -48,50 +49,67 @@ Arguments t_Foo.
Arguments Build_t_Foo.
#[export] Instance settable_t_Foo : Settable _ :=
settable! (@Build_t_Foo) <>.

Class t_Trait `{v_Self : Type} : Type :=
{
}.
Arguments t_Trait:clear implicits.
Arguments t_Trait (_).
Instance t_Trait_187936720 : t_Trait ((t_Foo)) :=
{
}.
(* NotImplementedYet *)
Definition main_a_a (_ : unit) : unit :=
tt.
Definition main_a_b (_ : unit) : unit :=
tt.
Definition main_a_c (_ : unit) : unit :=
tt.
Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : unit :=
let _ := main_a_a (tt) in
let _ := main_a_b (tt) in
let _ := main_a_c (tt) in
tt.

Definition main_b_a (_ : unit) : unit :=
tt.

Definition main_b_b (_ : unit) : unit :=
tt.

Definition main_b_c (_ : unit) : unit :=
tt.

Definition main_b (_ : unit) : unit :=
let _ := main_b_a (tt) in
let _ := main_b_b (tt) in
let _ := main_b_c (tt) in
tt.

Definition main_c_a (_ : unit) : unit :=
tt.

Definition main_c_b (_ : unit) : unit :=
tt.

Definition main_c_c (_ : unit) : unit :=
tt.

Definition main_c (_ : unit) : unit :=
let _ := main_c_a (tt) in
let _ := main_c_b (tt) in
let _ := main_c_c (tt) in
tt.

Definition main (_ : unit) : unit :=
let _ := main_a (Build_t_Foo) in
let _ := main_b (tt) in
let _ := main_c (tt) in
tt.'''
tt.
'''
18 changes: 11 additions & 7 deletions test-harness/src/snapshots/toolchain__let-else into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,19 +40,23 @@ From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.



(* NotImplementedYet *)

Definition let_else (opt : t_Option ((t_u32))) : bool :=
run (match opt with
| t_Option_Some (x) =>
t_ControlFlow_Continue (true)
| Option_Some (x) =>
ControlFlow_Continue (true)
| _ =>
t_ControlFlow_Break (false)
ControlFlow_Break (false)
end).

Definition let_else_different_type (opt : t_Option ((t_u32))) : bool :=
run (let hoist1 := match opt with
| t_Option_Some (x) =>
t_ControlFlow_Continue (t_Option_Some (t_Add_f_add (x) (1)))
| Option_Some (x) =>
ControlFlow_Continue (Option_Some (t_Add_f_add (x) (1)))
| _ =>
t_ControlFlow_Break (false)
ControlFlow_Break (false)
end in
t_ControlFlow_Continue (let_else (hoist1))).'''
ControlFlow_Continue (let_else (hoist1))).
'''
Loading

0 comments on commit 390a82a

Please sign in to comment.