From 8c2ee915ba221b569bc751ba3f6307d66ba66c8b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 19 Feb 2024 04:02:12 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590 (#1821) --- src/Algebra/Group.v | 16 +++++----- src/Assembly/Equivalence.v | 10 +++--- src/Bedrock/Field/Common/Types.v | 8 ++--- src/CLI.v | 54 ++++++++++++++++---------------- src/Stringification/Language.v | 6 ++-- 5 files changed, 47 insertions(+), 47 deletions(-) diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 02d923b778..ca4d76f59c 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -97,10 +97,10 @@ Section GroupByIsomorphism. Class isomorphic_groups := { - isomorphic_groups_group_G :> @group G EQ OP ID INV; - isomorphic_groups_group_H :> @group H eq op id inv; - isomorphic_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi; - isomorphic_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi'; + #[global] isomorphic_groups_group_G :: @group G EQ OP ID INV; + #[global] isomorphic_groups_group_H :: @group H eq op id inv; + #[global] isomorphic_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi; + #[global] isomorphic_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi'; }. Lemma group_by_isomorphism @@ -144,10 +144,10 @@ Section CommutativeGroupByIsomorphism. Class isomorphic_commutative_groups := { - isomorphic_commutative_groups_group_G :> @commutative_group G EQ OP ID INV; - isomorphic_commutative_groups_group_H :> @commutative_group H eq op id inv; - isomorphic_commutative_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi; - isomorphic_commutative_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi'; + #[global] isomorphic_commutative_groups_group_G :: @commutative_group G EQ OP ID INV; + #[global] isomorphic_commutative_groups_group_H :: @commutative_group H eq op id inv; + #[global] isomorphic_commutative_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi; + #[global] isomorphic_commutative_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi'; }. Lemma commutative_group_by_isomorphism diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index ef3ba41cdb..86985327b2 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -135,11 +135,11 @@ Definition assembly_stack_size {calling_convention : assembly_callee_saved_regis end. Class assembly_conventions_opt := - { assembly_calling_registers_ :> assembly_calling_registers_opt - ; assembly_stack_size_ :> assembly_stack_size_opt - ; assembly_output_first_ :> assembly_output_first_opt - ; assembly_argument_registers_left_to_right_ :> assembly_argument_registers_left_to_right_opt - ; assembly_callee_saved_registers_ :> assembly_callee_saved_registers_opt + { #[global] assembly_calling_registers_ :: assembly_calling_registers_opt + ; #[global] assembly_stack_size_ :: assembly_stack_size_opt + ; #[global] assembly_output_first_ :: assembly_output_first_opt + ; #[global] assembly_argument_registers_left_to_right_ :: assembly_argument_registers_left_to_right_opt + ; #[global] assembly_callee_saved_registers_ :: assembly_callee_saved_registers_opt }. Definition default_assembly_conventions : assembly_conventions_opt := {| assembly_calling_registers_ := None diff --git a/src/Bedrock/Field/Common/Types.v b/src/Bedrock/Field/Common/Types.v index fac2dbeefb..9c0ec00837 100644 --- a/src/Bedrock/Field/Common/Types.v +++ b/src/Bedrock/Field/Common/Types.v @@ -48,10 +48,10 @@ Section WithParameters. Class ok {parameters_sentinel : parameters} := { (* semantics_ok : Semantics.parameters_ok semantics *) - word_ok :> word.ok word; - mem_ok :> map.ok mem; - locals_ok :> map.ok locals; - ext_spec_ok :> Semantics.ext_spec.ok ext_spec; + #[global] word_ok :: word.ok word; + #[global] mem_ok :: map.ok mem; + #[global] locals_ok :: map.ok locals; + #[global] ext_spec_ok :: Semantics.ext_spec.ok ext_spec; varname_gen_unique : forall i j : nat, varname_gen i = varname_gen j <-> i = j; diff --git a/src/CLI.v b/src/CLI.v index 2e9d71f955..059ac24d4e 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -587,57 +587,57 @@ Module ForExtraction. Class ParsedSynthesizeOptions := { (** Is the code static / private *) - static :> static_opt + #[global] static :: static_opt (** Is the internal code static / private *) - ; internal_static :> internal_static_opt + ; #[global] internal_static :: internal_static_opt (** Is the code inlined *) - ; inline :> inline_opt + ; #[global] inline :: inline_opt (** Is the internal code inlined *) - ; inline_internal :> inline_internal_opt + ; #[global] inline_internal :: inline_internal_opt (** Should we only use signed integers *) - ; only_signed :> only_signed_opt + ; #[global] only_signed :: only_signed_opt (** Should we emit expressions requiring cmov *) - ; no_select :> no_select_opt + ; #[global] no_select :: no_select_opt (** Should we emit primitive operations *) - ; emit_primitives :> emit_primitives_opt + ; #[global] emit_primitives :: emit_primitives_opt (** Various output options including: *) (** Should we skip emitting typedefs for field elements *) (** Should we relax the bounds on the return carry type of sbb/adc operations? *) - ; output_options :> output_options_opt + ; #[global] output_options :: output_options_opt (** Should we use the alternate implementation of cmovznz *) - ; use_mul_for_cmovznz :> use_mul_for_cmovznz_opt + ; #[global] use_mul_for_cmovznz :: use_mul_for_cmovznz_opt (** Various abstract interpretation options *) (** Should we avoid uint1 at the output of shiftr *) - ; abstract_interpretation_options :> AbstractInterpretation.Options + ; #[global] abstract_interpretation_options :: AbstractInterpretation.Options (** Should we split apart oversized operations? *) - ; should_split_mul :> should_split_mul_opt + ; #[global] should_split_mul :: should_split_mul_opt (** Should we split apart multi-return operations? *) - ; should_split_multiret :> should_split_multiret_opt + ; #[global] should_split_multiret :: should_split_multiret_opt (** Should we remove use of value_barrier? *) - ; unfold_value_barrier :> unfold_value_barrier_opt + ; #[global] unfold_value_barrier :: unfold_value_barrier_opt (** Should we widen the carry to the full bitwidth? *) - ; widen_carry :> widen_carry_opt + ; #[global] widen_carry :: widen_carry_opt (** Should we widen the byte type to the full bitwidth? *) - ; widen_bytes :> widen_bytes_opt + ; #[global] widen_bytes :: widen_bytes_opt (** Should we ignore function-name mismatch errors when there's only one assembly function and only one actual function requested? *) - ; ignore_unique_asm_names :> ignore_unique_asm_names_opt + ; #[global] ignore_unique_asm_names :: ignore_unique_asm_names_opt (** What method should we use for rewriting? *) - ; low_level_rewriter_method :> low_level_rewriter_method_opt + ; #[global] low_level_rewriter_method :: low_level_rewriter_method_opt := default_low_level_rewriter_method (** What's the bitwidth? *) - ; machine_wordsize :> machine_wordsize_opt + ; #[global] machine_wordsize :: machine_wordsize_opt (** What's the package name *) - ; internal_package_name :> package_name_opt + ; #[global] internal_package_name :: package_name_opt (** What's the class name *) - ; internal_class_name :> class_name_opt + ; #[global] internal_class_name :: class_name_opt (** What's are the naming conventions to use? *) - ; language_naming_conventions :> language_naming_conventions_opt + ; #[global] language_naming_conventions :: language_naming_conventions_opt (** Documentation options *) - ; documentation_options :> documentation_options_opt + ; #[global] documentation_options :: documentation_options_opt (** assembly equivalence checker options *) - ; equivalence_checker_options :> equivalence_checker_options_opt + ; #[global] equivalence_checker_options :: equivalence_checker_options_opt (** error if there are un-requested assembly functions *) - ; error_on_unused_assembly_functions :> error_on_unused_assembly_functions_opt + ; #[global] error_on_unused_assembly_functions :: error_on_unused_assembly_functions_opt (** don't prepend fiat to prefix *) ; no_prefix_fiat : bool (** Extra lines before the documentation header *) @@ -645,15 +645,15 @@ Module ForExtraction. (** Extra lines at the beginning of the documentation header *) ; extra_early_header_lines : list string (** Debug rewriting *) - ; debug_rewriting :> debug_rewriting_opt + ; #[global] debug_rewriting :: debug_rewriting_opt (** Print debug info on success too *) ; debug_on_success : bool }. Class SynthesizeOptions := { - parsed_synthesize_options :> ParsedSynthesizeOptions + #[global] parsed_synthesize_options :: ParsedSynthesizeOptions (** Lines of assembly hints *) - ; assembly_hints_lines :> assembly_hints_lines_opt + ; #[global] assembly_hints_lines :: assembly_hints_lines_opt }. (** We define a class for holding the various options about file interaction that we don't pass to [Synthesize] *) diff --git a/src/Stringification/Language.v b/src/Stringification/Language.v index 9bf756120d..423d1ce3f9 100644 --- a/src/Stringification/Language.v +++ b/src/Stringification/Language.v @@ -154,9 +154,9 @@ Module Compilers. |}. Class output_options_opt := - { skip_typedefs_ :> skip_typedefs_opt - ; relax_adc_sbb_return_carry_to_bitwidth_ :> relax_adc_sbb_return_carry_to_bitwidth_opt - ; language_specific_cast_adjustment_ :> language_specific_cast_adjustment_opt + { #[global] skip_typedefs_ :: skip_typedefs_opt + ; #[global] relax_adc_sbb_return_carry_to_bitwidth_ :: relax_adc_sbb_return_carry_to_bitwidth_opt + ; #[global] language_specific_cast_adjustment_ :: language_specific_cast_adjustment_opt }. Definition default_output_options : output_options_opt