Merge branch 'main' into support-extraction

.github/workflows/ci.yml

@@ -84,7 +84,6 @@ jobs:
         if: ${{ matrix.coq-from-git }}
         run: |
           eval $(opam env)
-          opam pin add -k version dune 3.3.1
           # First we update SERAPI_COQ_HOME for future steps as per https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable
           echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV
           # Update to coq-core some day

CHANGES.md

@@ -1,6 +1,6 @@
 ## unreleased
 
- - [general] Cleanup old / unused code (@ejgallego, #)
+ - [general] Cleanup old / unused code (@ejgallego, #362)
 
 ## Version 0.18.1:
 
@@ -14,6 +14,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)

serapi/serapi_protocol.ml

@@ -130,7 +130,7 @@ type coq_object =
   | CoqGlobRef   of Names.GlobRef.t
   | CoqGlobRefExt of Globnames.extended_global_reference
   | CoqImplicit  of Impargs.implicits_list
-  | CoqProfData  of Profile_ltac.treenode
+  | CoqProfData  of Profile_tactic.treenode
   | CoqNotation  of Constrexpr.notation
   | CoqUnparsing of Ppextend.notation_printing_rules * Notation_gram.notation_grammar
   | CoqGoal      of Constr.t               Serapi_goals.reified_goal Serapi_goals.ser_goals
@@ -600,7 +600,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
   | Tactics prefix -> List.map (fun (i,t) -> CoqTactic(i,t)) @@ QueryUtil.query_tactics prefix
   | Locate  id     -> List.map (fun qid -> CoqQualId qid) @@ QueryUtil.locate id
   | Implicits id   -> List.map (fun ii -> CoqImplicit ii ) @@ QueryUtil.implicits id
-  | ProfileData    -> [CoqProfData (Profile_ltac.get_local_profiling_results ())]
+  | ProfileData    -> [CoqProfData (Profile_tactic.get_local_profiling_results ())]
   | Proof          -> QueryUtil.get_proof ~pstate
   | Unparsing ntn  -> (* Unfortunately this will produce an anomaly if the notation is not found...
                        * To keep protocol promises we need to special wrap it.

serapi/serapi_protocol.mli

@@ -215,7 +215,7 @@ type coq_object =
   (** "Extended Global Reference", as they can contain syntactic definitions too *)
   | CoqImplicit  of Impargs.implicits_list
   (** Implicit status for a constant *)
-  | CoqProfData  of Profile_ltac.treenode
+  | CoqProfData  of Profile_tactic.treenode
   (** Ltac Profiler data *)
   | CoqNotation  of Constrexpr.notation
   (** Representation of a notation (usually a string) *)

serlib/plugins/ltac/ser_rewrite.ml

@@ -29,8 +29,8 @@ type nary_strategy =
   [%import: Rewrite.nary_strategy]
   [@@deriving sexp,hash,compare]
 
-type ('a,'b) strategy_ast =
-  [%import: ('a,'b) Rewrite.strategy_ast]
+type ('a,'b,'c) strategy_ast =
+  [%import: ('a,'b,'c) Rewrite.strategy_ast]
   [@@deriving sexp,hash,compare]
 
 type strategy = Rewrite.strategy

serlib/plugins/ltac/ser_rewrite.mli

@@ -19,7 +19,7 @@ type unary_strategy = Rewrite.unary_strategy
 type binary_strategy = Rewrite.binary_strategy
   [@@deriving sexp, hash, compare]
 
-type ('a,'b) strategy_ast = ('a,'b) Rewrite.strategy_ast
+type ('a,'b,'c) strategy_ast = ('a,'b,'c) Rewrite.strategy_ast
   [@@deriving sexp, hash, compare]
 
 type strategy = Rewrite.strategy

serlib/plugins/ltac/ser_tacarg.ml

@@ -275,17 +275,17 @@ let wit_rewstrategy = Ltac_plugin.G_rewrite.wit_rewstrategy
 
 module GT2 = struct
   type raw =
-    [%import: Ltac_plugin.G_rewrite.raw_strategy]
+    [%import: Ltac_plugin.Tacexpr.raw_strategy]
   [@@deriving sexp,hash,compare]
   type glb =
-    [%import: Ltac_plugin.G_rewrite.glob_strategy]
+    [%import: Ltac_plugin.Tacexpr.glob_strategy]
   [@@deriving sexp,hash,compare]
   type top = Ltac_plugin.Rewrite.strategy
   [@@deriving sexp,hash,compare]
 end
 
 
-(* (G_rewrite.raw_strategy, G_rewrite.glob_strategy, Rewrite.strategy) *)
+(* (Tacexpr.raw_strategy, Tacexpr.glob_strategy, Rewrite.strategy) *)
 
 let ser_wit_rewstrategy = let module M = Ser_genarg.GS(GT2) in M.genser
 

serlib/plugins/ltac/ser_tacexpr.ml

@@ -44,7 +44,6 @@ module Goal_select = Ser_goal_select
 module Pattern    = Ser_pattern
 module Constrexpr = Ser_constrexpr
 module Vernacexpr = Ser_vernacexpr
-module Tacred     = Ser_tacred
 module Tactypes   = Ser_tactypes
 module Tactics    = Ser_tactics
 module Equality   = Ser_equality
@@ -509,7 +508,7 @@ let rec glob_tactic_expr_of_sexp tac =
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_pattern_and_expr_of_sexp
-    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Tacred.evaluable_global_reference_of_sexp))
+    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp))
     (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp))
     Names.lident_of_sexp
     glob_tactic_expr_of_sexp
@@ -520,7 +519,7 @@ and glob_atomic_tactic_expr_of_sexp tac =
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_pattern_and_expr_of_sexp
-    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Tacred.evaluable_global_reference_of_sexp))
+    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp))
     (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp))
     Names.lident_of_sexp
     glob_tactic_expr_of_sexp
@@ -531,7 +530,7 @@ let rec sexp_of_glob_tactic_expr (tac : glob_tactic_expr) =
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_pattern_and_expr
-    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Tacred.sexp_of_evaluable_global_reference))
+    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t))
     (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant))
     Names.sexp_of_lident
     sexp_of_glob_tactic_expr
@@ -542,7 +541,7 @@ and sexp_of_glob_atomic_tactic_expr (tac : glob_atomic_tactic_expr) =
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_pattern_and_expr
-    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Tacred.sexp_of_evaluable_global_reference))
+    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t))
     (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant))
     Names.sexp_of_lident
     sexp_of_glob_tactic_expr
@@ -555,7 +554,7 @@ let rec glob_tactic_expr_of_yojson tac =
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_pattern_and_expr_of_yojson
-    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Tacred.evaluable_global_reference_of_yojson))
+    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson))
     (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson))
     Names.lident_of_yojson
     glob_tactic_expr_of_yojson
@@ -566,7 +565,7 @@ and glob_atomic_tactic_expr_of_yojson tac =
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_pattern_and_expr_of_yojson
-    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Tacred.evaluable_global_reference_of_yojson))
+    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson))
     (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson))
     Names.lident_of_yojson
     glob_tactic_expr_of_yojson
@@ -577,7 +576,7 @@ let rec glob_tactic_expr_to_yojson tac =
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_pattern_and_expr_to_yojson
-    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Tacred.evaluable_global_reference_to_yojson))
+    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson))
     (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson))
     Names.lident_to_yojson
     glob_tactic_expr_to_yojson
@@ -588,7 +587,7 @@ and glob_atomic_tactic_expr_to_yojson tac =
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_pattern_and_expr_to_yojson
-    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Tacred.evaluable_global_reference_to_yojson))
+    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson))
     (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson))
     Names.lident_to_yojson
     glob_tactic_expr_to_yojson
@@ -600,7 +599,7 @@ let rec hash_fold_glob_tactic_expr st tac =
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_pattern_and_expr
-    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Tacred.hash_fold_evaluable_global_reference))
+    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t))
     (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant))
     Names.hash_fold_lident
     hash_fold_glob_tactic_expr
@@ -611,7 +610,7 @@ and hash_fold_glob_atomic_tactic_expr st tac =
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_pattern_and_expr
-    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Tacred.hash_fold_evaluable_global_reference))
+    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t))
     (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant))
     Names.hash_fold_lident
     hash_fold_glob_tactic_expr
@@ -626,7 +625,7 @@ let rec compare_glob_tactic_expr tac =
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_pattern_and_expr
-    (Locus.compare_or_var (Genredexpr.compare_and_short_name Tacred.compare_evaluable_global_reference))
+    (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare))
     (Locus.compare_or_var (Loc.compare_located compare_ltac_constant))
     Names.compare_lident
     compare_glob_tactic_expr
@@ -637,7 +636,7 @@ and compare_glob_atomic_tactic_expr tac =
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_pattern_and_expr
-    (Locus.compare_or_var (Genredexpr.compare_and_short_name Tacred.compare_evaluable_global_reference))
+    (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare))
     (Locus.compare_or_var (Loc.compare_located compare_ltac_constant))
     Names.compare_lident
     compare_glob_tactic_expr
@@ -798,7 +797,7 @@ let atomic_tactic_expr_of_sexp tac =
     EConstr.t_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Pattern.constr_pattern_of_sexp
-    Tacred.evaluable_global_reference_of_sexp
+    Names.Evaluable.t_of_sexp
     (Loc.located_of_sexp ltac_constant_of_sexp)
     Names.Id.t_of_sexp
     unit_of_sexp
@@ -809,7 +808,7 @@ let sexp_of_atomic_tactic_expr tac =
     EConstr.sexp_of_t
     Genintern.sexp_of_glob_constr_and_expr
     Pattern.sexp_of_constr_pattern
-    Tacred.sexp_of_evaluable_global_reference
+    Names.Evaluable.sexp_of_t
     (Loc.sexp_of_located sexp_of_ltac_constant)
     Names.Id.sexp_of_t
     sexp_of_unit

serlib/ser_constrexpr.ml

@@ -52,6 +52,14 @@ type quality_expr =
   [%import: Constrexpr.quality_expr]
   [@@deriving sexp,yojson,hash,compare]
 
+type relevance_expr =
+  [%import: Constrexpr.relevance_expr]
+  [@@deriving sexp,yojson,hash,compare]
+
+type relevance_info_expr =
+  [%import: Constrexpr.relevance_info_expr]
+  [@@deriving sexp,yojson,hash,compare]
+
 type sort_expr =
   [%import: Constrexpr.sort_expr]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_declarations.ml

@@ -42,8 +42,8 @@ type ('a, 'b) declaration_arity =
   [%import: ('a, 'b) Declarations.declaration_arity]
   [@@deriving sexp,yojson,hash,compare]
 
-type nested_type =
-  [%import: Declarations.nested_type]
+type recarg_type =
+  [%import: Declarations.recarg_type]
   [@@deriving sexp,yojson,hash,compare]
 
 type recarg =
@@ -63,6 +63,10 @@ type inductive_arity =
   [%import: Declarations.inductive_arity]
   [@@deriving sexp,yojson,hash,compare]
 
+type squash_info =
+  [%import: Declarations.squash_info]
+  [@@deriving sexp,yojson,hash,compare]
+
 type one_inductive_body =
   [%import: Declarations.one_inductive_body]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_genredexpr.ml

@@ -24,7 +24,6 @@ module Locus = Ser_locus
 module Libnames = Ser_libnames
 module Constrexpr = Ser_constrexpr
 module Genintern = Ser_genintern
-module Tacred = Ser_tacred
 
 type 'a red_atom =
   [%import: 'a Genredexpr.red_atom]
@@ -99,13 +98,13 @@ module A = struct
 
   type glb =
     (Ser_genintern.glob_constr_and_expr,
-     Ser_tacred.evaluable_global_reference and_short_name Ser_locus.or_var,
+     Ser_names.Evaluable.t and_short_name Ser_locus.or_var,
      Ser_genintern.glob_constr_pattern_and_expr) red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 
   type top =
     (Ser_eConstr.constr,
-     Ser_tacred.evaluable_global_reference,
+     Ser_names.Evaluable.t,
      Ser_pattern.constr_pattern) red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 end

serlib/ser_glob_term.ml

@@ -78,6 +78,10 @@ type glob_qvar =
   [%import: Glob_term.glob_qvar]
   [@@deriving sexp,yojson,hash,compare]
 
+type glob_relevance =
+  [%import: Glob_term.glob_relevance]
+  [@@deriving sexp,yojson,hash,compare]
+
 type glob_quality =
   [%import: Glob_term.glob_quality]
   [@@deriving sexp,yojson,hash,compare]
@@ -114,6 +118,11 @@ type glob_fix_kind =
   [%import: Glob_term.glob_fix_kind]
   [@@deriving sexp,yojson,hash,compare]
 
+type relevance_info =
+  [%import: Glob_term.relevance_info]
+  [@@deriving sexp,yojson,hash,compare]
+
+
 type glob_evar_kind = Evar_kinds.glob_evar_kind
   [@@deriving sexp,yojson,hash,compare]
 

serlib/ser_names.ml

@@ -218,6 +218,7 @@ module Ind = struct
 end
 
 module Indset_env = Ser_cSet.Make(Indset_env)(Ind)
+module Indmap_env = Ser_cMap.Make(Indmap_env)(Ind)
 
 type inductive =
   [%import: Names.inductive]
@@ -266,9 +267,11 @@ type t = [%import: Names.GlobRef.t]
 end
 
 (* Evaluable global reference: public *)
-(* type evaluable_global_reference =
- *   [%import: Names.evaluable_global_reference]
- *   [@@deriving sexp] *)
+module Evaluable = struct
+  type t =
+    [%import: Names.Evaluable.t]
+    [@@deriving sexp,yojson,hash,compare]
+end
 
 type lident =
   [%import: Names.lident]

serlib/ser_names.mli

@@ -51,6 +51,7 @@ module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindm
 module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap_env.t
 
 module Indset_env : Ser_cSet.ExtS with type elt = inductive and type t = Indset_env.t
+module Indmap_env : Ser_cMap.ExtS with type key = inductive and type 'a t = 'a Indmap_env.t
 
 type 'a tableKey = 'a Names.tableKey
 
@@ -73,6 +74,8 @@ end
 
 module GlobRef : SerType.SJHC with type t = Names.GlobRef.t
 
+module Evaluable : SerType.SJHC with type t = Names.Evaluable.t
+
 type lident = Names.lident [@@deriving sexp,yojson,hash,compare]
 type lname = Names.lname [@@deriving sexp,yojson,hash,compare]
 type lstring = Names.lstring [@@deriving sexp,yojson,hash,compare]

serlib/plugins/ltac/ser_profile_ltac.ml → serlib/ser_profile_tactic.ml

@@ -33,7 +33,7 @@ let sexp_of_cstring_map f m =
   sexp_of_list s_f l
 
 type treenode =
-  [%import: Ltac_plugin.Profile_ltac.treenode
+  [%import: Profile_tactic.treenode
   [@with CString.Map.t   := cstring_map;
          CString.Map.key := string
   ]]

serlib/plugins/ltac/ser_profile_ltac.mli → serlib/ser_profile_tactic.mli

@@ -15,9 +15,7 @@
 
 open Sexplib
 
-open Ltac_plugin
-
-type treenode = Profile_ltac.treenode
+type treenode = Profile_tactic.treenode
 
 val treenode_of_sexp : Sexp.t -> treenode
 val sexp_of_treenode : treenode -> Sexp.t

serlib/ser_sorts.ml

@@ -38,7 +38,11 @@ end
 
 module Quality = struct
   type constant = [%import: Sorts.Quality.constant] [@@deriving sexp,yojson,hash,compare]
-  type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare]
+  module Self = struct
+    type t = [%import: Sorts.Quality.t] [@@deriving sexp,yojson,hash,compare]
+  end
+  include Self
+  module Set = Ser_cSet.Make(Sorts.Quality.Set)(Self)
 end
 
 module PierceSpec = struct

serlib/ser_sorts.mli

@@ -27,6 +27,7 @@ module Quality : sig
   type constant = Sorts.Quality.constant [@@deriving sexp,yojson,hash,compare]
 
   include SerType.SJHC with type t = Sorts.Quality.t
+  module Set : SerType.SJHC with type t = Sorts.Quality.Set.t
 end
 
 module QConstraints : SerType.SJHC with type t = Sorts.QConstraints.t