Snapshot update

.github/workflows/extract_and_run_coq.yml

@@ -37,8 +37,8 @@ jobs:
 
       - name: build and run coq on tests
         env:
-          FILES: assert attribute-opaque constructor-as-closure enum-repr enum-struct-variant even
-          NOT_SUPPORTED_FILES: attributes cli conditional-match cyclic-modules dyn functions
+          FILES: assert attribute-opaque enum-struct-variant
+          NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions
         run: |
           for f in $FILES; do \
             cd hax/tests/$f && \

engine/backends/coq/coq/coq_backend.ml

@@ -984,15 +984,15 @@ struct
         string
           (match id.definition with
           | "not" -> "negb"
-          | "eq" -> "t_PartialEq_f_eq"
-          | "lt" -> "t_PartialOrd_f_lt"
-          | "gt" -> "t_PartialOrd_f_gt"
-          | "le" -> "t_PartialOrd_f_le"
-          | "ge" -> "t_PartialOrd_f_ge"
-          | "rem" -> "t_Rem_f_rem"
-          | "add" -> "t_Add_f_add"
-          | "mul" -> "t_Mul_f_mul"
-          | "div" -> "t_Div_f_div"
+          | "eq" -> "PartialEq_f_eq"
+          | "lt" -> "PartialOrd_f_lt"
+          | "gt" -> "PartialOrd_f_gt"
+          | "le" -> "PartialOrd_f_le"
+          | "ge" -> "PartialOrd_f_ge"
+          | "rem" -> "Rem_f_rem"
+          | "add" -> "Add_f_add"
+          | "mul" -> "Mul_f_mul"
+          | "div" -> "Div_f_div"
           | x -> x)
     end
 

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

@@ -46,14 +46,14 @@ From Core Require Import Core.
 
 Definition asserts '(_ : unit) : unit :=
   let _ := assert ((true : bool)) in
-  let _ := assert (t_PartialEq_f_eq ((1 : t_i32)) ((1 : t_i32))) in
+  let _ := assert (PartialEq_f_eq ((1 : t_i32)) ((1 : t_i32))) in
   let _ := match ((2 : t_i32),(2 : t_i32)) with
   | (left_val,right_val) =>
-    assert (t_PartialEq_f_eq (left_val) (right_val))
+    assert (PartialEq_f_eq (left_val) (right_val))
   end in
   let _ := match ((1 : t_i32),(2 : t_i32)) with
   | (left_val,right_val) =>
-    assert (negb (t_PartialEq_f_eq (left_val) (right_val)))
+    assert (negb (PartialEq_f_eq (left_val) (right_val)))
   end in
   tt.
 '''

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

@@ -66,19 +66,19 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
   | EnumWithRepr_ExplicitDiscr2 =>
     discriminant_EnumWithRepr_ExplicitDiscr2
   | EnumWithRepr_ImplicitDiscrEmptyTuple =>
-    t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((1 : t_u16))
+    Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((1 : t_u16))
   | EnumWithRepr_ImplicitDiscrEmptyStruct =>
-    t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((2 : t_u16))
+    Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((2 : t_u16))
   end.
 
 (* NotImplementedYet *)
 
 Definition f '(_ : unit) : t_u32 :=
-  let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((0 : t_u16))) in
-  t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).
+  let v__x := cast (Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((0 : t_u16))) in
+  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_EnumWithRepr_ExplicitDiscr1) ((0 : t_u16))).
+  cast (Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) ((0 : t_u16))).
 
 Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
   cast (t_EnumWithRepr_cast_to_repr (x)).

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

@@ -75,7 +75,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
 Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
   match match x with
   | Option_Some (v) =>
-    match t_PartialOrd_f_gt (v) ((0 : t_i32)) with
+    match PartialOrd_f_gt (v) ((0 : t_i32)) with
     | true =>
       Option_Some (v)
     | _ =>
@@ -125,7 +125,7 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
   | _ =>
     match match x with
     | Option_Some (Result_Ok (v)) =>
-      match Option_Some (t_Add_f_add (v) ((1 : t_i32))) with
+      match Option_Some (Add_f_add (v) ((1 : t_i32))) with
       | Option_Some (1) =>
         Option_Some ((0 : t_i32))
       | _ =>

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

@@ -55,7 +55,7 @@ Definition let_else (opt : t_Option ((t_u32))) : bool :=
 Definition let_else_different_type (opt : t_Option ((t_u32))) : bool :=
   run (let hoist1 := match opt with
   | Option_Some (x) =>
-    ControlFlow_Continue (Option_Some (t_Add_f_add (x) ((1 : t_u32))))
+    ControlFlow_Continue (Option_Some (Add_f_add (x) ((1 : t_u32))))
   | _ =>
     ControlFlow_Break ((false : bool))
   end in

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

@@ -61,14 +61,14 @@ Definition v_CONSTANT : t_Foo :=
   Build_t_Foo ((3 : t_u8)).
 
 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
-  let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i64 := 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_i32 := 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_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
+  let _ : t_u64 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in
+  let _ : t_u32 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in
+  let _ : t_u16 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_u8 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i64 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i32 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i16 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i8 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
   tt.
 
 Definition fn_pointer_cast '(_ : unit) : unit :=