From b866a7fb07d9455d33ceb4ff8d600e61cd993a78 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Jan 2024 17:27:31 +0100 Subject: [PATCH] [serlib] Expose some more functions related to Require's AST. --- CHANGES.md | 10 ++ serlib/ser_vernacexpr.mli | 338 ++++++++++++++++++-------------------- 2 files changed, 169 insertions(+), 179 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index a34ea4d7..caee44cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,8 @@ +## Version 0.18.2: + + - [serlib] Expose some more Ast functions required by coq-lsp's + auto-build support (@ejgallego, #383) + ## Version 0.18.1: - [serlib] Fix a few 8.18 piercings (!) (@ejgallego, #357) @@ -10,6 +15,11 @@ - [serlib] Fix ltac2 plugin wrong piercing due to missing constructor (@ejgallego, reported by @quarkcool, #349). +## Version 0.17.2: + + - [serlib] Expose some more Ast functions required by coq-lsp's + auto-build support (@ejgallego, #383) + ## Version 0.17.1: - [sertop] Don't initialize `CoqworkmgrApi` (@ejgallego, #340) diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli index 21100a18..a8be83f3 100644 --- a/serlib/ser_vernacexpr.mli +++ b/serlib/ser_vernacexpr.mli @@ -13,297 +13,277 @@ (* Status: Very Experimental *) (************************************************************************) -open Sexplib - type infix_flag = [%import: Vernacexpr.infix_flag] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] + +type opacity_flag = + [%import: Vernacexpr.opacity_flag] + [@@deriving sexp,yojson,hash,compare] type scope_name = [%import: Vernacexpr.scope_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] + +(* type scope_delimiter = *) +(* [%import: Vernacexpr.scope_delimiter] *) +(* [@@deriving sexp,yojson,hash,compare] *) type notation_format = [%import: Vernacexpr.notation_format] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type syntax_modifier = [%import: Vernacexpr.syntax_modifier] - [@@deriving sexp,yojson] - -type coercion_class = Vernacexpr.coercion_class -val coercion_class_of_sexp : Sexp.t -> coercion_class -val sexp_of_coercion_class : coercion_class -> Sexp.t - -(* type goal_identifier = Vernacexpr.goal_identifier - * val goal_identifier_of_sexp : Sexp.t -> goal_identifier - * val sexp_of_goal_identifier : goal_identifier -> Sexp.t *) - -type goal_reference = Vernacexpr.goal_reference -val goal_reference_of_sexp : Sexp.t -> goal_reference -val sexp_of_goal_reference : goal_reference -> Sexp.t - -type printable = Vernacexpr.printable -val printable_of_sexp : Sexp.t -> printable -val sexp_of_printable : printable -> Sexp.t - -type search_item = Vernacexpr.search_item -val search_item_of_sexp : Sexp.t -> search_item -val sexp_of_search_item : search_item -> Sexp.t - -type searchable = Vernacexpr.searchable -val searchable_of_sexp : Sexp.t -> searchable -val sexp_of_searchable : searchable -> Sexp.t - -type locatable = Vernacexpr.locatable -val locatable_of_sexp : Sexp.t -> locatable -val sexp_of_locatable : locatable -> Sexp.t - -type showable = Vernacexpr.showable -val showable_of_sexp : Sexp.t -> showable -val sexp_of_showable : showable -> Sexp.t - -type comment = Vernacexpr.comment -val comment_of_sexp : Sexp.t -> comment -val sexp_of_comment : comment -> Sexp.t - -type search_restriction = Vernacexpr.search_restriction -val search_restriction_of_sexp : Sexp.t -> search_restriction -val sexp_of_search_restriction : search_restriction -> Sexp.t - -(* type rec_flag = Vernacexpr.rec_flag - * val rec_flag_of_sexp : Sexp.t -> rec_flag - * val sexp_of_rec_flag : rec_flag -> Sexp.t *) - -type verbose_flag = Vernacexpr.verbose_flag -val verbose_flag_of_sexp : Sexp.t -> verbose_flag -val sexp_of_verbose_flag : verbose_flag -> Sexp.t - -type coercion_flag = Vernacexpr.coercion_flag -val coercion_flag_of_sexp : Sexp.t -> coercion_flag -val sexp_of_coercion_flag : coercion_flag -> Sexp.t - -(* type inductive_flag = Vernacexpr.inductive_flag - * val inductive_flag_of_sexp : Sexp.t -> inductive_flag - * val sexp_of_inductive_flag : inductive_flag -> Sexp.t *) + [@@deriving sexp,yojson,hash,compare] -type instance_flag = Vernacexpr.instance_flag -val instance_flag_of_sexp : Sexp.t -> instance_flag -val sexp_of_instance_flag : instance_flag -> Sexp.t +type coercion_class = + [%import: Vernacexpr.coercion_class] + [@@deriving sexp,yojson,hash,compare] -type export_flag = Vernacexpr.export_flag -val export_flag_of_sexp : Sexp.t -> export_flag -val sexp_of_export_flag : export_flag -> Sexp.t +type goal_reference = + [%import: Vernacexpr.goal_reference] + [@@deriving sexp,yojson,hash,compare] -(* type onlyparsing_flag = Vernacexpr.onlyparsing_flag - * val onlyparsing_flag_of_sexp : Sexp.t -> onlyparsing_flag - * val sexp_of_onlyparsing_flag : onlyparsing_flag -> Sexp.t *) +type printable = + [%import: Vernacexpr.printable] + [@@deriving sexp,yojson,hash,compare] -type locality_flag = Vernacexpr.locality_flag -val locality_flag_of_sexp : Sexp.t -> locality_flag -val sexp_of_locality_flag : locality_flag -> Sexp.t +type glob_search_where = + [%import: Vernacexpr.glob_search_where] + [@@deriving sexp,yojson,hash,compare] -(* type obsolete_locality = Vernacexpr.obsolete_locality - * val obsolete_locality_of_sexp : Sexp.t -> obsolete_locality - * val sexp_of_obsolete_locality : obsolete_locality -> Sexp.t *) +type search_item = + [%import: Vernacexpr.search_item] + [@@deriving sexp,yojson,hash,compare] -(* type option_value = Vernacexpr.option_value - * val option_value_of_sexp : Sexp.t -> option_value - * val sexp_of_option_value : option_value -> Sexp.t *) +type search_request = + [%import: Vernacexpr.search_request] + [@@deriving sexp,yojson,hash,compare] -(* type option_ref_value = Vernacexpr.option_ref_value - * val option_ref_value_of_sexp : Sexp.t -> option_ref_value - * val sexp_of_option_ref_value : option_ref_value -> Sexp.t *) +type searchable = + [%import: Vernacexpr.searchable] + [@@deriving sexp,yojson,hash,compare] -(* type plident = Vernacexpr.plident - * val plident_of_sexp : Sexp.t -> plident - * val sexp_of_plident : plident -> Sexp.t *) +type locatable = + [%import: Vernacexpr.locatable] + [@@deriving sexp,yojson,hash,compare] -(* type sort_expr = Vernacexpr.sort_expr - * val sort_expr_of_sexp : Sexp.t -> sort_expr - * val sexp_of_sort_expr : sort_expr -> Sexp.t *) +type showable = + [%import: Vernacexpr.showable] + [@@deriving sexp,yojson,hash,compare] -type definition_expr = Vernacexpr.definition_expr -val definition_expr_of_sexp : Sexp.t -> definition_expr -val sexp_of_definition_expr : definition_expr -> Sexp.t +type comment = + [%import: Vernacexpr.comment] + [@@deriving sexp,yojson,hash,compare] -type fixpoint_expr = Vernacexpr.fixpoint_expr - [@@deriving sexp,hash,compare] +type search_restriction = + [%import: Vernacexpr.search_restriction] + [@@deriving sexp,yojson,hash,compare] -type cofixpoint_expr = Vernacexpr.cofixpoint_expr -val cofixpoint_expr_of_sexp : Sexp.t -> cofixpoint_expr -val sexp_of_cofixpoint_expr : cofixpoint_expr -> Sexp.t +type verbose_flag = + [%import: Vernacexpr.verbose_flag] + [@@deriving sexp,yojson,hash,compare] -type local_decl_expr = Vernacexpr.local_decl_expr -val local_decl_expr_of_sexp : Sexp.t -> local_decl_expr -val sexp_of_local_decl_expr : local_decl_expr -> Sexp.t +type coercion_flag = + [%import: Vernacexpr.coercion_flag] + [@@deriving sexp,yojson,hash,compare] -type inductive_kind = Vernacexpr.inductive_kind -val inductive_kind_of_sexp : Sexp.t -> inductive_kind -val sexp_of_inductive_kind : inductive_kind -> Sexp.t +type instance_flag = + [%import: Vernacexpr.instance_flag] + [@@deriving sexp,yojson,hash,compare] -type notation_declaration = Vernacexpr.notation_declaration -val notation_declaration_of_sexp : Sexp.t -> notation_declaration -val sexp_of_notation_declaration : notation_declaration -> Sexp.t +type export_flag = + [%import: Vernacexpr.export_flag] + [@@deriving sexp,yojson,hash,compare] -type simple_binder = Vernacexpr.simple_binder -val simple_binder_of_sexp : Sexp.t -> simple_binder -val sexp_of_simple_binder : simple_binder -> Sexp.t +type locality_flag = + [%import: Vernacexpr.locality_flag] + [@@deriving sexp,yojson,hash,compare] -type class_binder = Vernacexpr.class_binder +type definition_expr = + [%import: Vernacexpr.definition_expr] + [@@deriving sexp,yojson,hash,compare] -val class_binder_of_sexp : Sexp.t -> class_binder -val sexp_of_class_binder : class_binder -> Sexp.t +type notation_declaration = + [%import: Vernacexpr.notation_declaration] + [@@deriving sexp,yojson,hash,compare] -type 'a with_coercion = 'a Vernacexpr.with_coercion +type 'a fix_expr_gen = + [%import: 'a Vernacexpr.fix_expr_gen] + [@@deriving sexp,yojson,hash,compare] -val with_coercion_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a with_coercion -val sexp_of_with_coercion : ('a -> Sexp.t) -> 'a with_coercion -> Sexp.t +type fixpoint_expr = + [%import: Vernacexpr.fixpoint_expr] + [@@deriving sexp,yojson,hash,compare] -type constructor_expr = Vernacexpr.constructor_expr -val constructor_expr_of_sexp : Sexp.t -> constructor_expr -val sexp_of_constructor_expr : constructor_expr -> Sexp.t +type cofixpoint_expr = + [%import: Vernacexpr.cofixpoint_expr] + [@@deriving sexp,yojson,hash,compare] -type constructor_list_or_record_decl_expr = Vernacexpr.constructor_list_or_record_decl_expr +type local_decl_expr = + [%import: Vernacexpr.local_decl_expr] + [@@deriving sexp,yojson,hash,compare] -val constructor_list_or_record_decl_expr_of_sexp : - Sexp.t -> constructor_list_or_record_decl_expr -val sexp_of_constructor_list_or_record_decl_expr : - constructor_list_or_record_decl_expr -> Sexp.t +type inductive_kind = + [%import: Vernacexpr.inductive_kind] + [@@deriving sexp,yojson,hash,compare] -type inductive_expr = Vernacexpr.inductive_expr +type simple_binder = + [%import: Vernacexpr.simple_binder] + [@@deriving sexp,yojson,hash,compare] -val inductive_expr_of_sexp : Sexp.t -> inductive_expr -val sexp_of_inductive_expr : inductive_expr -> Sexp.t +type class_binder = + [%import: Vernacexpr.class_binder] + [@@deriving sexp,yojson,hash,compare] -type one_inductive_expr = Vernacexpr.one_inductive_expr +type 'a with_coercion = + [%import: 'a Vernacexpr.with_coercion] + [@@deriving sexp,yojson,hash,compare] -val one_inductive_expr_of_sexp : Sexp.t -> one_inductive_expr -val sexp_of_one_inductive_expr : one_inductive_expr -> Sexp.t +type 'a with_coercion_instance = + [%import: 'a Vernacexpr.with_coercion_instance] + [@@deriving sexp,yojson,hash,compare] -type proof_expr = Vernacexpr.proof_expr +type constructor_expr = + [%import: Vernacexpr.constructor_expr] + [@@deriving sexp,yojson,hash,compare] -val proof_expr_of_sexp : Sexp.t -> proof_expr -val sexp_of_proof_expr : proof_expr -> Sexp.t +type record_field_attr_unparsed = + [%import: Vernacexpr.record_field_attr_unparsed] + [@@deriving sexp,yojson,hash,compare] -(* type grammar_tactic_prod_item_expr = Vernacexpr.grammar_tactic_prod_item_expr *) -(* val grammar_tactic_prod_item_expr_of_sexp : Sexp.t -> grammar_tactic_prod_item_expr *) -(* val sexp_of_grammar_tactic_prod_item_expr : grammar_tactic_prod_item_expr -> Sexp.t *) +type constructor_list_or_record_decl_expr = + [%import: Vernacexpr.constructor_list_or_record_decl_expr] + [@@deriving sexp,yojson,hash,compare] -(* type syntax_modifier = Vernacexpr.syntax_modifier *) +type inductive_params_expr = + [%import: Vernacexpr.inductive_params_expr] + [@@deriving sexp,yojson,hash,compare] -(* val syntax_modifier_of_sexp : Sexp.t -> syntax_modifier *) -(* val sexp_of_syntax_modifier : syntax_modifier -> Sexp.t *) +type inductive_expr = + [%import: Vernacexpr.inductive_expr] + [@@deriving sexp,yojson,hash,compare] -type proof_end = Vernacexpr.proof_end -val proof_end_of_sexp : Sexp.t -> proof_end -val sexp_of_proof_end : proof_end -> Sexp.t +type one_inductive_expr = + [%import: Vernacexpr.one_inductive_expr] + [@@deriving sexp,yojson,hash,compare] -type scheme = Vernacexpr.scheme -val scheme_of_sexp : Sexp.t -> scheme -val sexp_of_scheme : scheme -> Sexp.t +type proof_expr = + [%import: Vernacexpr.proof_expr] + [@@deriving sexp,yojson,hash,compare] -type section_subset_expr = Vernacexpr.section_subset_expr -val section_subset_expr_of_sexp : Sexp.t -> section_subset_expr -val sexp_of_section_subset_expr : section_subset_expr -> Sexp.t +type proof_end = + [%import: Vernacexpr.proof_end] + [@@deriving sexp,yojson,hash,compare] -type extend_name = Vernacexpr.extend_name -val extend_name_of_sexp : Sexp.t -> extend_name -val sexp_of_extend_name : extend_name -> Sexp.t +type scheme_type = + [%import: Vernacexpr.scheme_type] + [@@deriving sexp,yojson,hash,compare] -type register_kind = Vernacexpr.register_kind -val register_kind_of_sexp : Sexp.t -> register_kind -val sexp_of_register_kind : register_kind -> Sexp.t +type scheme = + [%import: Vernacexpr.scheme] + [@@deriving sexp,yojson,hash,compare] -type module_ast_inl = Vernacexpr.module_ast_inl +type section_subset_expr = + [%import: Vernacexpr.section_subset_expr] + [@@deriving sexp,yojson,hash,compare] -val module_ast_inl_of_sexp : Sexp.t -> module_ast_inl -val sexp_of_module_ast_inl : module_ast_inl -> Sexp.t +type extend_name = + [%import: Vernacexpr.extend_name] + [@@deriving sexp,yojson,hash,compare] -type module_binder = Vernacexpr.module_binder +type register_kind = + [%import: Vernacexpr.register_kind] + [@@deriving sexp,yojson,hash,compare] -val module_binder_of_sexp : Sexp.t -> module_binder -val sexp_of_module_binder : module_binder -> Sexp.t +type module_ast_inl = + [%import: Vernacexpr.module_ast_inl] + [@@deriving sexp,yojson,hash,compare] type discharge = [%import: Vernacexpr.discharge] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type equality_scheme_type = [%import: Vernacexpr.equality_scheme_type] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type import_categories = [%import: Vernacexpr.import_categories] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type export_with_cats = [%import: Vernacexpr.export_with_cats] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] + +type module_binder = + [%import: Vernacexpr.module_binder] + [@@deriving sexp,yojson,hash,compare] type one_import_filter_name = [%import: Vernacexpr.one_import_filter_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type import_filter_expr = [%import: Vernacexpr.import_filter_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type hint_info_expr = [%import: Vernacexpr.hint_info_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type reference_or_constr = [%import: Vernacexpr.reference_or_constr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type hints_expr = [%import: Vernacexpr.hints_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_one_argument_status = [%import: Vernacexpr.vernac_one_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_argument_status = [%import: Vernacexpr.vernac_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type arguments_modifier = [%import: Vernacexpr.arguments_modifier] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type option_setting = [%import: Vernacexpr.option_setting] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type notation_enable_modifier = [%import: Vernacexpr.notation_enable_modifier] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson,hash,compare] type synterp_vernac_expr = [%import: Vernacexpr.synterp_vernac_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type synpure_vernac_expr = [%import: Vernacexpr.synpure_vernac_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type 'a vernac_expr_gen = [%import: 'a Vernacexpr.vernac_expr_gen] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,hash,compare] type control_flag = [%import: Vernacexpr.control_flag] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,hash,compare] type ('a, 'b) vernac_control_gen_r = [%import: ('a, 'b) Vernacexpr.vernac_control_gen_r] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type 'a vernac_control_gen = [%import: 'a Vernacexpr.vernac_control_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,hash,compare] type vernac_control = [%import: Vernacexpr.vernac_control]