From 2e0afd36cae8e66fd88732d3981b102b0206e2b2 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Mon, 11 Nov 2024 10:12:09 +0100 Subject: [PATCH] CI for coq coverage --- .github/workflows/extract_and_run_coq.yml | 29 ++++++++++ engine/backends/coq/coq/coq_backend.ml | 33 ++++++----- engine/lib/concrete_ident/concrete_ident.ml | 16 ++++- engine/lib/concrete_ident/concrete_ident.mli | 3 + examples/Cargo.lock | 4 ++ examples/Cargo.toml | 3 +- .../coverage/proofs/coq/extraction/Coverage.v | 9 ++- .../coq/extraction/Coverage_Test_closures.v | 44 -------------- .../coq/extraction/Coverage_Test_enum.v | 56 ++++++++++++------ .../coq/extraction/Coverage_Test_enum_Test.v | 10 ++-- .../coq/extraction/Coverage_Test_functions.v | 7 ++- .../coq/extraction/Coverage_Test_instance.v | 58 +++++++++++++++++++ .../coq/extraction/Coverage_Test_primitives.v | 7 ++- .../coq/extraction/Coverage_Test_sequence.v | 7 ++- .../coq/extraction/Coverage_Test_struct.v | 7 ++- .../proofs/coq/extraction/_CoqProject | 11 ---- examples/coverage/src/lib.rs | 2 + examples/coverage/src/test_enum.rs | 28 +++++---- examples/coverage/src/test_instance.rs | 21 +++++++ 19 files changed, 238 insertions(+), 117 deletions(-) create mode 100644 .github/workflows/extract_and_run_coq.yml delete mode 100644 examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v create mode 100644 examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v delete mode 100644 examples/coverage/proofs/coq/extraction/_CoqProject create mode 100644 examples/coverage/src/test_instance.rs diff --git a/.github/workflows/extract_and_run_coq.yml b/.github/workflows/extract_and_run_coq.yml new file mode 100644 index 000000000..9de74dad6 --- /dev/null +++ b/.github/workflows/extract_and_run_coq.yml @@ -0,0 +1,29 @@ +name: Extract and Run - Coq + +on: [pull_request] +jobs: + extract-bertie: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + path: hax + + - uses: DeterminateSystems/nix-installer-action@main + - uses: DeterminateSystems/magic-nix-cache-action@main + + - name: ⤵ Install hax + run: | + nix profile install --verbose ./hax + + - name: build coverage example + working-directory: hax/examples/coverage + run: | + nix run . into coq + + - 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 + 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" diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index ad0bb345c..ec8327d63 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -116,7 +116,7 @@ let hardcoded_coq_headers = Require Import Coq.Floats.Floats.\n\ From RecordUpdate Require Import RecordSet.\n\ Import RecordSetNotations.\n\n\ - From Core Require Import Core.\n" + (* From Core Require Import Core. *)\n" let dummy_lib = "Class t_Sized (T : Type) := { }.\n\ @@ -136,8 +136,11 @@ let dummy_lib = Definition t_String := string.\n\ Definition ToString_f_to_string (x : string) := x.\n\ Instance Sized_any : forall {t_A}, t_Sized t_A := {}.\n\ - Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x \ - => x}.\n" + Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.\n\ + 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" module BasePrinter = Generic_printer.Make (InputLanguage) @@ -435,7 +438,7 @@ struct method impl_ident ~goal ~name:_ = goal#p method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v ~ii_ident ~ii_attrs:_ = - string (String.chop_prefix_exn ~prefix:"impl_" (U.Concrete_ident_view.to_definition_name ii_ident#v)) ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi + ii_ident#p ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi method impl_item'_IIFn ~body ~params = if List.length params == 0 then body#p @@ -527,7 +530,13 @@ struct (braces (nest 2 (concat_map_with - ~pre:(break 1 ^^ string (String.drop_prefix (U.Concrete_ident_view.to_definition_name name#v) 2) ^^ !^"_") + ~pre: + (break 1 + ^^ string + (String.drop_prefix + (U.Concrete_ident_view.to_definition_name name#v) + 2) + ^^ !^"_") (fun x -> x#p) items) ^^ break 1)) @@ -539,12 +548,10 @@ struct method item'_Trait ~super:_ ~name ~generics ~items ~safety:_ = let _, params, constraints = generics#v in - CoqNotation.class_ name#p (concat_map_with ~pre:space - (fun x -> parens x#p) - params - ^^ concat_map_with ~pre:space - (fun x -> x#p) - constraints) [] !^"Type" + CoqNotation.class_ name#p + (concat_map_with ~pre:space (fun x -> parens x#p) params + ^^ concat_map_with ~pre:space (fun x -> x#p) constraints) + [] !^"Type" (braces (nest 2 (concat_map_with ~pre:(break 1) (fun x -> x#p) items) ^^ break 1)) @@ -989,9 +996,7 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = { path = mod_name ^ ".v"; contents = - hardcoded_coq_headers ^ "\n" - (* ^ dummy_lib ^ "\n" *) - ^ contents; + hardcoded_coq_headers ^ "\n" ^ dummy_lib ^ "\n" ^ contents; sourcemap = None; })) @ [ diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index b5a5fc67e..ddf13d62e 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -244,7 +244,7 @@ module View = struct let string_of_def_path_item : Imported.def_path_item -> string option = function | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s - | Impl -> Some "impl" + | Impl -> Some "impl" | AnonConst -> Some "anon_const" | _ -> None @@ -560,6 +560,8 @@ 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 @@ -649,3 +651,15 @@ let parent_impl (id : t) : t option = module DefaultViewAPI = MakeViewAPI (DefaultNamePolicy) include DefaultViewAPI + +let remove_impl old = + let new_parent = (parent (parent old)).def_id in + { + kind = Macro; + (* Field; *) + def_id = + { + new_parent with + path = new_parent.path @ [ List.last_exn old.def_id.path ]; + }; + } diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index e87f71b22..5fcd7dae2 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -74,3 +74,6 @@ identifier points to an [Impl] block. *) val parent_impl : t -> t option (** Returns the identifier pointing to the parent `impl` block, if it exists. *) + +val remove_impl : t -> t +(** Returns the parent *) diff --git a/examples/Cargo.lock b/examples/Cargo.lock index af90ddc48..668d60c74 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -151,6 +151,10 @@ dependencies = [ "hax-lib", ] +[[package]] +name = "coverage" +version = "0.1.0" + [[package]] name = "cpufeatures" version = "0.2.11" diff --git a/examples/Cargo.toml b/examples/Cargo.toml index 9b7eceb41..4aea4b684 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -6,7 +6,8 @@ members = [ "barrett", "kyber_compress", "proverif-psk", - "coq-example"] + "coq-example", + "coverage"] resolver = "2" [workspace.dependencies] diff --git a/examples/coverage/proofs/coq/extraction/Coverage.v b/examples/coverage/proofs/coq/extraction/Coverage.v index 73677f973..b3041e007 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage.v +++ b/examples/coverage/proofs/coq/extraction/Coverage.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,7 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. +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. @@ -46,3 +49,5 @@ Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x (* NotImplementedYet *) (* NotImplementedYet *) + +(* NotImplementedYet *) diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v deleted file mode 100644 index a085ed82d..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v +++ /dev/null @@ -1,44 +0,0 @@ -(* File automatically generated by Hacspec *) -From Coq Require Import ZArith. -Require Import List. -Import List.ListNotations. -Open Scope Z_scope. -Open Scope bool_scope. -Require Import Ascii. -Require Import String. -Require Import Coq.Floats.Floats. -From RecordUpdate Require Import RecordSet. -Import RecordSetNotations. - -From Core Require Import Core. - -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -(* Definition test__f `{v_F : Type} `{t_Sized (v_F)} `{t_FnOnce (v_F) (unit)} `{_.(t_FnOnce_f_Output) = t_u8} (g : v_F) : t_u8 := *) -(* t_Add_f_add (t_Add := _) (t_FnOnce_f_call_once (t_FnOnce := _) (g) (tt)) (Build_t_u8 (Build_t_U8 2)). *) - -(* Definition test '(_ : unit) : unit := *) -(* let add : t_i32 -> t_i32 -> t_i32 := fun x y => *) -(* t_Add_f_add (x) (y) in *) -(* let _ := Fn_f_call (fun x => *) -(* Add_f_add (x) (x)) ((2)) in *) -(* let _ := test__f (fun _ => *) -(* 23) in *) -(* tt. *) diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v index d32fd0595..619874948 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,28 +29,16 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -Record Foo_Qux_record (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type := - { - Qux_f_x : v_T; - Qux_f_y : t_Array (v_T) (v_N); - Qux_f_z : t_u8; - }. -Arguments Build_Foo_Qux_record (_) (_) {_}. -Arguments Qux_f_x {_} {_} {_}. -Arguments Qux_f_y {_} {_} {_}. -Arguments Qux_f_z {_} {_} {_}. -#[export] Instance settable_Foo_Qux_record `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ := - settable! (Build_Foo_Qux_record v_T v_N) . -Inductive t_Foo `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Type := -| Foo_Bar : t_u8 -> _ -| Foo_Baz -| Foo_Qux : Foo_Qux_record v_T v_N -> _. +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. Inductive t_test__AnimalA : Type := | test__AnimalA_Dog | test__AnimalA_Cat. +Arguments test__AnimalA_Dog. +Arguments test__AnimalA_Cat. Definition t_test__AnimalA_cast_to_repr (x : t_test__AnimalA) : t_isize := match x with @@ -73,6 +61,8 @@ Arguments Cat_f_weight. Inductive t_test__AnimalB : Type := | test__AnimalB_Dog : t_String -> float -> _ | test__AnimalB_Cat : test__AnimalB_Cat_record -> _. +Arguments test__AnimalB_Dog. +Arguments test__AnimalB_Cat. Record test__Enum_Struct_record : Type := { @@ -88,6 +78,9 @@ Inductive t_test__Enum : Type := | test__Enum_Unit | test__Enum_Tuple : t_u16 -> _ | test__Enum_Struct : test__Enum_Struct_record -> _. +Arguments test__Enum_Unit. +Arguments test__Enum_Tuple. +Arguments test__Enum_Struct. Record test__Examples_StructLike_record : Type := { @@ -101,8 +94,33 @@ Inductive t_test__Examples : Type := | test__Examples_UnitLike | test__Examples_TupleLike : t_i32 -> _ | test__Examples_StructLike : test__Examples_StructLike_record -> _. +Arguments test__Examples_UnitLike. +Arguments test__Examples_TupleLike. +Arguments test__Examples_StructLike. + +Record test__Foo_Qux_record (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type := + { + Qux_f_x : v_T; + Qux_f_y : t_Array (v_T) (v_N); + Qux_f_z : t_u8; + }. +Arguments Build_test__Foo_Qux_record (_) (_) {_}. +Arguments Qux_f_x {_} {_} {_}. +Arguments Qux_f_y {_} {_} {_}. +Arguments Qux_f_z {_} {_} {_}. +#[export] Instance settable_test__Foo_Qux_record `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ := + settable! (Build_test__Foo_Qux_record v_T v_N) . +Inductive t_test__Foo (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type := +| test__Foo_Bar : t_u8 -> _ +| test__Foo_Baz +| test__Foo_Qux : test__Foo_Qux_record v_T v_N -> _. +Arguments test__Foo_Bar {_} {_} {_}. +Arguments test__Foo_Baz {_} {_} {_}. +Arguments test__Foo_Qux {_} {_} {_}. Definition test '(_ : unit) : unit := + let x : t_test__Foo ((t_u8)) (12) := test__Foo_Baz in + let _ := tt in let a : t_test__AnimalA := test__AnimalA_Dog in let a := test__AnimalA_Cat in let _ := tt in diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v index d2c30d4c9..946d186d1 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,10 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -From Coverage Require Import Examples. -Export Examples. +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. Definition discriminant_test__Enum_Struct : t_u8 := 1. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v index 6b18c8c9e..01103b49c 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,7 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. +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. Definition first `{v_A : Type} `{v_B : Type} `{t_Sized (v_A)} `{t_Sized (v_B)} `{t_Clone (v_B)} '((value,_) : (v_A*t_i32)) (y : v_B) : v_A := value. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v new file mode 100644 index 000000000..723497058 --- /dev/null +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v @@ -0,0 +1,58 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Require Import List. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import Ascii. +Require Import String. +Require Import Coq.Floats.Floats. +From RecordUpdate Require Import RecordSet. +Import RecordSetNotations. + +(* From Core Require Import Core. *) + +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. + +Inductive t_SomeEnum (v_T : Type) `{t_Sized (v_T)} : Type := +| SomeEnum_None +| SomeEnum_Some : v_T -> _. +Arguments SomeEnum_None {_} {_}. +Arguments SomeEnum_Some {_} {_}. + +Class t_SomeTrait (v_Self : Type) : Type := + { + SomeTrait_f_some_fun : v_Self -> v_Self; + }. +Arguments t_SomeTrait (_). + +Instance t_SomeTrait_153652929 `{v_T : Type} `{t_Sized (v_T)} `{t_SomeTrait (v_T)} : t_SomeTrait ((t_SomeEnum ((v_T)))) := + { + SomeTrait_impl_f_some_fun := fun (self : t_SomeEnum ((v_T)))=> + match self with + | SomeEnum_Some x => + SomeEnum_Some (SomeTrait_f_some_fun (x)) + | SomeEnum_None => + SomeEnum_None + end; + }. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v index 4aa5c8a02..f0ce9d790 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,7 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. +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. Definition test '(_ : unit) : unit := let _ : bool := false in diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v index dd8ecb148..f660f5434 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,7 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. +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. Definition test '(_ : unit) : unit := let _ : unit := tt in diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v index 984908e8b..e57490a49 100644 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v +++ b/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v @@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. -From Core Require Import Core. +(* From Core Require Import Core. *) Class t_Sized (T : Type) := { }. Definition t_u8 := Z. @@ -29,7 +29,10 @@ 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. +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. Record t_foo (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type := { diff --git a/examples/coverage/proofs/coq/extraction/_CoqProject b/examples/coverage/proofs/coq/extraction/_CoqProject deleted file mode 100644 index 636260f7a..000000000 --- a/examples/coverage/proofs/coq/extraction/_CoqProject +++ /dev/null @@ -1,11 +0,0 @@ --R ./ Core --arg -w --arg all - -./Coverage_Test_closures.v -./Coverage_Test_enum.v -./Coverage_Test_functions.v -./Coverage_Test_primitives.v -./Coverage_Test_sequence.v -./Coverage_Test_struct.v -./Coverage.v diff --git a/examples/coverage/src/lib.rs b/examples/coverage/src/lib.rs index c0aeec187..2ce2b500b 100644 --- a/examples/coverage/src/lib.rs +++ b/examples/coverage/src/lib.rs @@ -7,3 +7,5 @@ mod test_enum; mod test_functions; mod test_closures; + +mod test_instance; diff --git a/examples/coverage/src/test_enum.rs b/examples/coverage/src/test_enum.rs index bef41a8ab..9e2b63ff0 100644 --- a/examples/coverage/src/test_enum.rs +++ b/examples/coverage/src/test_enum.rs @@ -1,10 +1,14 @@ -enum Foo<'a, T, const N : usize> { - Bar(u8), - Baz, - Qux {x : &'a T, y : [T; N], z : u8}, -} - fn test() { + { + enum Foo<'a, T, const N : usize> { + Bar(u8), + Baz, + Qux {x : &'a T, y : [T; N], z : u8}, + } + + let x : Foo = Foo::Baz; + } + { enum AnimalA { Dog, @@ -31,12 +35,12 @@ fn test() { StructLike { value: i32 }, } - use Examples::*; // Creates aliases to all variants. - let x = UnitLike; // Path expression of the const item. - let x = UnitLike {}; // Struct expression. - let y = TupleLike(123); // Call expression. - let y = TupleLike { 0: 123 }; // Struct expression using integer field names. - let z = StructLike { value: 123 }; // Struct expression. + // use Examples::*; // Creates aliases to all variants. + let x = Examples::UnitLike; // Path expression of the const item. + let x = Examples::UnitLike {}; // Struct expression. + let y = Examples::TupleLike(123); // Call expression. + let y = Examples::TupleLike { 0: 123 }; // Struct expression using integer field names. + let z = Examples::StructLike { value: 123 }; // Struct expression. } { #[repr(u8)] diff --git a/examples/coverage/src/test_instance.rs b/examples/coverage/src/test_instance.rs new file mode 100644 index 000000000..bee6c8ff8 --- /dev/null +++ b/examples/coverage/src/test_instance.rs @@ -0,0 +1,21 @@ +enum SomeEnum { + None, + Some(T), +} + +trait SomeTrait { + fn some_fun(&self) -> Self; +} + +impl SomeTrait for SomeEnum +where + T: SomeTrait, +{ + #[inline] + fn some_fun(&self) -> Self { + match self { + SomeEnum::Some(x) => SomeEnum::Some(x.some_fun()), + SomeEnum::None => SomeEnum::None, + } + } +}