diff --git a/test-harness/src/snapshots/toolchain__assert into-coq.snap b/test-harness/src/snapshots/toolchain__assert into-coq.snap index 9f6ecd8fa..a000cc9f9 100644 --- a/test-harness/src/snapshots/toolchain__assert into-coq.snap +++ b/test-harness/src/snapshots/toolchain__assert into-coq.snap @@ -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 @@ -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. +''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap index e01bebf01..bfe3bcc0a 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap @@ -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). +''' diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap index 387dbbcf9..abd2a3274 100644 --- a/test-harness/src/snapshots/toolchain__guards into-coq.snap +++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap @@ -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. +''' diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index 9122c374c..7cc86205b 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -40,6 +40,7 @@ From RecordUpdate Require Import RecordSet. Import RecordSetNotations. + Record t_Foo : Type := { }. @@ -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. +''' diff --git a/test-harness/src/snapshots/toolchain__let-else into-coq.snap b/test-harness/src/snapshots/toolchain__let-else into-coq.snap index a705d6542..330c601b3 100644 --- a/test-harness/src/snapshots/toolchain__let-else into-coq.snap +++ b/test-harness/src/snapshots/toolchain__let-else into-coq.snap @@ -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))). +''' diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index e2203f3fb..77d4150c3 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -41,20 +41,25 @@ From RecordUpdate Require Import RecordSet. Import RecordSetNotations. + From Literals Require Import Hax_lib (t_int). Export Hax_lib (t_int). + Record t_Foo : Type := { - t_Foo_f_field : t_u8; + f_field : t_u8; }. Arguments t_Foo:clear implicits. Arguments t_Foo. Arguments Build_t_Foo. #[export] Instance settable_t_Foo : Settable _ := - settable! (@Build_t_Foo) . + settable! (@Build_t_Foo) . + (* NotImplementedYet *) + Definition v_CONSTANT : t_Foo := Build_t_Foo (3). + Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit := let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in @@ -65,22 +70,24 @@ Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_u let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in tt. + Definition fn_pointer_cast (_ : unit) : unit := let f : t_u32 -> t_u32 := fun x => x in tt. -Definition math_integers (x : t_Int) `{andb (t_PartialOrd_f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (t_PartialOrd_f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := - let _ : t_Int := t_Abstraction_f_lift (3) in - let _ := t_PartialOrd_f_gt (impl__Int___unsafe_from_str ("-340282366920938463463374607431768211455000"%string)) (impl__Int___unsafe_from_str ("340282366920938463463374607431768211455000"%string)) in - let _ := t_PartialOrd_f_lt (x) (x) in - let _ := t_PartialOrd_f_ge (x) (x) in - let _ := t_PartialOrd_f_le (x) (x) in - let _ := t_PartialEq_f_ne (x) (x) in - let _ := t_PartialEq_f_eq (x) (x) in - let _ := t_Add_f_add (x) (x) in - let _ := t_Sub_f_sub (x) (x) in - let _ := t_Mul_f_mul (x) (x) in - let _ := t_Div_f_div (x) (x) in + +Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := + let _ : t_Int := f_lift (3) in + let _ := f_gt (impl__Int___unsafe_from_str ("-340282366920938463463374607431768211455000"%string)) (impl__Int___unsafe_from_str ("340282366920938463463374607431768211455000"%string)) in + let _ := f_lt (x) (x) in + let _ := f_ge (x) (x) in + let _ := f_le (x) (x) in + let _ := f_ne (x) (x) in + let _ := f_eq (x) (x) in + let _ := f_add (x) (x) in + let _ := f_sub (x) (x) in + let _ := f_mul (x) (x) in + let _ := f_div (x) (x) in let _ : t_i16 := impl__Int__to_i16 (x) in let _ : t_i32 := impl__Int__to_i32 (x) in let _ : t_i64 := impl__Int__to_i64 (x) in @@ -91,14 +98,16 @@ Definition math_integers (x : t_Int) `{andb (t_PartialOrd_f_gt (x) (impl__Int___ let _ : t_u64 := impl__Int__to_u64 (x) in let _ : t_u128 := impl__Int__to_u128 (x) in let _ : t_usize := impl__Int__to_usize (x) in - impl__Int__to_u8 (t_Add_f_add (x) (t_Mul_f_mul (x) (x))). + impl__Int__to_u8 (f_add (x) (f_mul (x) (x))). + Definition numeric (_ : unit) : unit := let _ : t_usize := 123 in + let _ : t_isize := -42 in let _ : t_isize := 42 in - let _ : t_isize := 42 in - let _ : t_i32 := 42 in + let _ : t_i32 := -42 in let _ : t_u128 := 22222222222222222222 in tt. + Definition patterns (_ : unit) : unit := let _ := match 1 with | 2 => @@ -119,8 +128,11 @@ Definition patterns (_ : unit) : unit := tt end in tt. + Definition panic_with_msg (_ : unit) : unit := never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))). + Definition empty_array (_ : unit) : unit := let _ : t_Slice t_u8 := unsize ([]) in - tt.''' + tt. +''' diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap index 6f121c290..f4b3cbfe0 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap @@ -41,62 +41,71 @@ From RecordUpdate Require Import RecordSet. Import RecordSetNotations. + Inductive t_E : Type := -| t_E_A -| t_E_B. +| E_A +| E_B. Arguments t_E:clear implicits. Arguments t_E. + Definition t_E_cast_to_repr (x : t_E) : t_isize := match x with - | t_E_A => + | E_A => 0 - | t_E_B => + | E_B => 1 end. + (* NotImplementedYet *) + Definition bar (x : t_E) : unit := match x with - | t_E_A - | t_E_B => + | E_A + | E_B => tt end. + Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 := match x with | (1 - | 2,t_Option_Some (3 + | 2,Option_Some (3 | 4)) => 0 | (x,_) => x end. + Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 := match x with - | t_Result_Ok ((1 + | Result_Ok ((1 | 2,x)) - | t_Result_Err ((3 + | Result_Err ((3 | 4,x)) => x - | t_Result_Ok ((x,_)) - | t_Result_Err ((x,_)) => + | Result_Ok ((x,_)) + | Result_Err ((x,_)) => x end. + Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 := match x with - | (1,t_Option_Some (3)) - | (1,t_Option_Some (4)) - | (2,t_Option_Some (3)) - | (2,t_Option_Some (4)) => + | (1,Option_Some (3)) + | (1,Option_Some (4)) + | (2,Option_Some (3)) + | (2,Option_Some (4)) => 0 | (x,_) => x end. + Definition nested (x : t_Option ((t_i32))) : t_i32 := match x with - | t_Option_Some (1 + | Option_Some (1 | 2) => 1 - | t_Option_Some (x) => + | Option_Some (x) => x - | t_Option_None => + | Option_None => 0 - end.''' + end. +''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index ddbd8546e..d3b0567d8 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap @@ -40,33 +40,42 @@ From RecordUpdate Require Import RecordSet. Import RecordSetNotations. + Inductive t_Foo : Type := -| t_Foo_A -| t_Foo_B. +| Foo_A +| Foo_B. Arguments t_Foo:clear implicits. Arguments t_Foo. + Record t_Bar : Type := { - t_Bar_0 : t_Foo; + 0 : t_Foo; }. Arguments t_Bar:clear implicits. Arguments t_Bar. Arguments Build_t_Bar. #[export] Instance settable_t_Bar : Settable _ := - settable! (@Build_t_Bar) . + settable! (@Build_t_Bar) <0>. + Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize := match x with - | t_Foo_A => + | Foo_A => 0 - | t_Foo_B => + | Foo_B => 1 end. + (* NotImplementedYet *) + Definition f (_ : t_u32) : t_Foo := - t_Foo_A. + Foo_A. + Definition g (_ : unit) : t_Bar := Build_t_Bar (f (32)). + Definition no_dependency_1_ (_ : unit) : unit := tt. + Definition no_dependency_2_ (_ : unit) : unit := - tt.''' + tt. +''' diff --git a/test-harness/src/snapshots/toolchain__slices into-coq.snap b/test-harness/src/snapshots/toolchain__slices into-coq.snap index 2846fe70d..93fa425b0 100644 --- a/test-harness/src/snapshots/toolchain__slices into-coq.snap +++ b/test-harness/src/snapshots/toolchain__slices into-coq.snap @@ -41,12 +41,18 @@ From RecordUpdate Require Import RecordSet. Import RecordSetNotations. + (* NotImplementedYet *) + Definition v_VERSION : t_Slice t_u8 := unsize ([118; 49]). + Definition do_something (_ : t_Slice t_u8) : unit := tt. + Definition r#unsized (_ : t_Array (t_Slice t_u8) (1)) : unit := tt. + Definition sized (x : t_Array (t_Array (t_u8) (4)) (1)) : unit := - r#unsized ([unsize (index (x) (0))]).''' + r#unsized ([unsize (index (x) (0))]). +'''