Update snapshot

.github/workflows/extract_and_run_coq.yml

@@ -24,6 +24,6 @@ jobs:
       - name: run coq
         working-directory: hax/examples/coverage/proofs/coq/extraction
         run: |
-          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v
+          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
           nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
           nix-shell --packages coq coqPackages.coq-record-update --run "make"

engine/backends/coq/coq/coq_backend.ml

@@ -119,7 +119,8 @@ let hardcoded_coq_headers =
    (* From Core Require Import Core. *)\n"
 
 let dummy_lib =
-  "Class t_Sized (T : Type) := { }.\n\
+  "(* TODO: Replace this dummy lib with core lib *)\n\
+   Class t_Sized (T : Type) := { }.\n\
    Definition t_u8 := Z.\n\
    Definition t_u16 := Z.\n\
    Definition t_u32 := Z.\n\
@@ -140,7 +141,8 @@ let dummy_lib =
    Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x \
    => x}.\n\
    Definition t_Slice (T : Type) := list T.\n\
-   Definition unsize {T : Type} : list T -> t_Slice T := id.\n"
+   Definition unsize {T : Type} : list T -> t_Slice T := id.\n\
+   (* / dummy lib *)\n"
 
 module BasePrinter = Generic_printer.Make (InputLanguage)
 
@@ -805,7 +807,7 @@ struct
           ^^ string "|}"
         else
           constructor#p
-          ^^ concat_map_with ~pre:space (fun (ident, exp) -> exp#p) fields
+          ^^ concat_map_with ~pre:space (fun (ident, exp) -> parens(exp#p)) fields
 
       method pat'_PConstruct_tuple ~super:_ ~components =
         (* TODO: Only add `'` if you are a top-level pattern *)

engine/lib/concrete_ident/concrete_ident.ml

@@ -560,8 +560,6 @@ let to_debug_string = T.show
 let map_path_strings ~(f : string -> string) (cid : t) : t =
   { cid with def_id = Imported.map_path_strings ~f cid.def_id }
 
-let parent (cid : t) : t = { cid with def_id = Imported.parent cid.def_id }
-
 module DefaultNamePolicy = struct
   let reserved_words = Hash_set.create (module String)
   let index_field_transform = Fn.id

test-harness/src/snapshots/toolchain__assert into-coq.snap

@@ -39,11 +39,37 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
 
-Definition asserts (_ : unit) : unit :=
+Definition asserts '(_ : unit) : unit :=
   let _ := assert (true) in
   let _ := assert (t_PartialEq_f_eq (1) (1)) in
   let _ := match (2,2) with
@@ -56,3 +82,9 @@ Definition asserts (_ : unit) : unit :=
   end in
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Assert.v'''

test-harness/src/snapshots/toolchain__enum-repr into-coq.snap

@@ -40,6 +40,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
@@ -53,8 +79,10 @@ Inductive t_EnumWithRepr : Type :=
 | EnumWithRepr_ExplicitDiscr2
 | EnumWithRepr_ImplicitDiscrEmptyTuple
 | EnumWithRepr_ImplicitDiscrEmptyStruct.
-Arguments t_EnumWithRepr:clear implicits.
-Arguments t_EnumWithRepr.
+Arguments EnumWithRepr_ExplicitDiscr1.
+Arguments EnumWithRepr_ExplicitDiscr2.
+Arguments EnumWithRepr_ImplicitDiscrEmptyTuple.
+Arguments EnumWithRepr_ImplicitDiscrEmptyStruct.
 
 Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
   match x with
@@ -70,7 +98,7 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
 
 (* NotImplementedYet *)
 
-Definition f (_ : unit) : t_u32 :=
+Definition f '(_ : unit) : t_u32 :=
   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))).
 
@@ -83,3 +111,9 @@ Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
 Definition get_repr (x : t_EnumWithRepr) : t_u16 :=
   t_EnumWithRepr_cast_to_repr (x).
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Enum_repr.v'''

test-harness/src/snapshots/toolchain__guards into-coq.snap

@@ -39,6 +39,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
@@ -160,3 +186,9 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
     end
   end.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Guards.v'''

test-harness/src/snapshots/toolchain__include-flag into-coq.snap

@@ -39,21 +39,44 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 Record t_Foo : Type :=
   {
   }.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
 Arguments Build_t_Foo.
-#[export] Instance settable_t_Foo : Settable _ :=
-  settable! (@Build_t_Foo) <>.
+#[export]
+Notation "'Foo'" := Build_t_Foo.
 
-Class t_Trait `{v_Self : Type} : Type :=
+Class t_Trait (v_Self : Type) : Type :=
   {
   }.
-Arguments t_Trait:clear implicits.
 Arguments t_Trait (_).
 
 Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
@@ -62,13 +85,13 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
 
 (* NotImplementedYet *)
 
-Definition main_a_a (_ : unit) : unit :=
+Definition main_a_a '(_ : unit) : unit :=
   tt.
 
-Definition main_a_b (_ : unit) : unit :=
+Definition main_a_b '(_ : unit) : unit :=
   tt.
 
-Definition main_a_c (_ : unit) : unit :=
+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 :=
@@ -77,39 +100,45 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un
   let _ := main_a_c (tt) in
   tt.
 
-Definition main_b_a (_ : unit) : unit :=
+Definition main_b_a '(_ : unit) : unit :=
   tt.
 
-Definition main_b_b (_ : unit) : unit :=
+Definition main_b_b '(_ : unit) : unit :=
   tt.
 
-Definition main_b_c (_ : unit) : unit :=
+Definition main_b_c '(_ : unit) : unit :=
   tt.
 
-Definition main_b (_ : unit) : unit :=
+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 :=
+Definition main_c_a '(_ : unit) : unit :=
   tt.
 
-Definition main_c_b (_ : unit) : unit :=
+Definition main_c_b '(_ : unit) : unit :=
   tt.
 
-Definition main_c_c (_ : unit) : unit :=
+Definition main_c_c '(_ : unit) : unit :=
   tt.
 
-Definition main_c (_ : unit) : unit :=
+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 :=
+Definition main '(_ : unit) : unit :=
   let _ := main_a (Build_t_Foo) in
   let _ := main_b (tt) in
   let _ := main_c (tt) in
   tt.
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Include_flag.v'''

test-harness/src/snapshots/toolchain__let-else into-coq.snap

@@ -39,6 +39,32 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
+(* From Core Require Import Core. *)
+
+(* TODO: Replace this dummy lib with core lib *)
+Class t_Sized (T : Type) := { }.
+Definition t_u8 := Z.
+Definition t_u16 := Z.
+Definition t_u32 := Z.
+Definition t_u64 := Z.
+Definition t_u128 := Z.
+Definition t_usize := Z.
+Definition t_i8 := Z.
+Definition t_i16 := Z.
+Definition t_i32 := Z.
+Definition t_i64 := Z.
+Definition t_i128 := Z.
+Definition t_isize := Z.
+Definition t_Array T (x : t_usize) := list T.
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) := x.
+Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
+Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
+Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
+Definition t_Slice (T : Type) := list T.
+Definition unsize {T : Type} : list T -> t_Slice T := id.
+(* / dummy lib *)
+
 
 
 (* NotImplementedYet *)
@@ -60,3 +86,9 @@ Definition let_else_different_type (opt : t_Option ((t_u32))) : bool :=
   end in
   ControlFlow_Continue (let_else (hoist1))).
 '''
+_CoqProject = '''
+-R ./ TODO
+-arg -w
+-arg all
+
+Let_else.v'''