Skip to content

Commit b6e4a99

Browse files
SkySkimmerSkySkimmer
authored
Merge pull request #1060 from ppedrot/genredexpr-open-api
Adapt to rocq-prover/rocq#21287.
2 parents 81babef + 58e9524 commit b6e4a99

File tree

7 files changed

+129
-41
lines changed

7 files changed

+129
-41
lines changed

‎serlib/plugins/ltac/ser_tacarg.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ module EConstr = Ser_eConstr
3434
module Hints = Ser_hints
3535
module Ltac_pretype = Ser_ltac_pretype
3636
module Genredexpr = Ser_genredexpr
37+
module Redexpr = Ser_redexpr
3738
module Gentactic = Ser_gentactic
3839

3940
module Ltac_plugin = struct

‎serlib/plugins/ltac/ser_tacexpr.ml‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,7 @@ module Namegen = Ser_namegen
7676
module Genarg = Ser_genarg
7777
module Stdarg = Ser_stdarg
7878
module Genredexpr = Ser_genredexpr
79+
module Redexpr = Ser_redexpr
7980
module Genintern = Ser_genintern
8081
module Goal_select = Ser_goal_select
8182
module Pattern = Ser_pattern
@@ -167,7 +168,7 @@ type ml_tactic_entry =
167168
[%import: Ltac_plugin.Tacexpr.ml_tactic_entry]
168169
[@@deriving sexp,yojson,hash,compare]
169170

170-
type ('a, 'b, 'c, 'd) may_eval = [%import: ('a,'b,'c,'d) Ltac_plugin.Tacexpr.may_eval]
171+
type ('a, 'b, 'c, 'd, 'e) may_eval = [%import: ('a,'b,'c,'d,'e) Ltac_plugin.Tacexpr.may_eval]
171172
[@@deriving sexp,yojson,hash,compare]
172173

173174
(* type dyn = Ser_Dyn [@@deriving sexp] *)
@@ -197,7 +198,7 @@ type ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen
197198
Namegen.intro_pattern_naming_expr CAst.t option
198199
| TacInductionDestruct of
199200
rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
200-
| TacReduce of ('trm,'cst,'redpat,'occvar) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
201+
| TacReduce of ('trm,'cst,'redpat,'occvar,'lev Redexpr.user_red_expr) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
201202
| TacChange of check_flag * 'redpat option * 'dtrm * 'nam Locus.clause_expr
202203
| TacRewrite of evars_flag *
203204
(bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam Locus.clause_expr *
@@ -206,7 +207,7 @@ type ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen
206207

207208
and ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen_tactic_arg =
208209
| TacGeneric of string option * 'lev Genarg.generic_argument
209-
| ConstrMayEval of ('trm,'cst,'redpat,'occvar) may_eval
210+
| ConstrMayEval of ('trm,'cst,'redpat,'occvar,'lev Redexpr.user_red_expr) may_eval
210211
| Reference of 'ref
211212
| TacCall of ('ref *
212213
('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen_tactic_arg list) CAst.t

‎serlib/ser_genredexpr.ml‎

Lines changed: 8 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -45,12 +45,12 @@ type ('a,'b,'c) red_context =
4545
[%import: ('a,'b,'c) Genredexpr.red_context]
4646
[@@deriving sexp,yojson,hash,compare]
4747

48-
type ('a,'b,'c,'d, 'e) red_expr_gen0 =
49-
[%import: ('a,'b,'c,'d, 'e) Genredexpr.red_expr_gen0]
48+
type ('a,'b,'c,'d,'e,'f) red_expr_gen0 =
49+
[%import: ('a,'b,'c,'d,'e,'f) Genredexpr.red_expr_gen0]
5050
[@@deriving sexp,yojson,hash,compare]
5151

52-
type ('a,'b,'c,'d) red_expr_gen =
53-
[%import: ('a,'b,'c,'d) Genredexpr.red_expr_gen]
52+
type ('a,'b,'c,'d,'e) red_expr_gen =
53+
[%import: ('a,'b,'c,'d,'e) Genredexpr.red_expr_gen]
5454
[@@deriving sexp,yojson,hash,compare]
5555

5656
(* Helpers for raw_red_expr *)
@@ -66,8 +66,8 @@ type r_pat =
6666
[%import: Genredexpr.r_pat]
6767
[@@deriving sexp,yojson,hash,compare]
6868

69-
type raw_red_expr =
70-
[%import: Genredexpr.raw_red_expr]
69+
type 'a raw_red_expr =
70+
[%import: 'a Genredexpr.raw_red_expr]
7171
[@@deriving sexp,yojson,hash,compare]
7272

7373
(* glob_red_expr *)
@@ -88,33 +88,6 @@ type g_pat =
8888
[%import: Genredexpr.g_pat]
8989
[@@deriving sexp,yojson,hash,compare]
9090

91-
type glob_red_expr =
92-
[%import: Genredexpr.glob_red_expr]
91+
type 'a glob_red_expr =
92+
[%import: 'a Genredexpr.glob_red_expr]
9393
[@@deriving sexp,yojson,hash,compare]
94-
95-
module A = struct
96-
97-
type raw =
98-
[%import: Genredexpr.raw_red_expr]
99-
[@@deriving sexp,yojson,hash,compare]
100-
101-
type glb =
102-
[%import: Genredexpr.glob_red_expr]
103-
[@@deriving sexp,yojson,hash,compare]
104-
105-
type top =
106-
(Ser_eConstr.constr,
107-
Ser_evaluable.t,
108-
Ser_pattern.constr_pattern,
109-
int) red_expr_gen
110-
[@@deriving sexp,yojson,hash,compare]
111-
end
112-
113-
let ser_wit_red_expr = let module M = Ser_genarg.GS(A) in M.genser
114-
115-
let register () =
116-
Ser_genarg.register_genser Redexpr.wit_red_expr ser_wit_red_expr;
117-
()
118-
119-
let _ =
120-
register ()

‎serlib/ser_genredexpr.mli‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,13 @@ type 'a red_atom = 'a Genredexpr.red_atom
2222
type 'a glob_red_flag = 'a Genredexpr.glob_red_flag
2323
[@@deriving sexp,yojson,hash,compare]
2424

25-
type ('a, 'b, 'c, 'd) red_expr_gen = ('a, 'b, 'c, 'd) Genredexpr.red_expr_gen
25+
type ('a, 'b, 'c, 'd, 'e) red_expr_gen = ('a, 'b, 'c, 'd, 'e) Genredexpr.red_expr_gen
2626
[@@deriving sexp,yojson,hash,compare]
2727

28-
type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]
28+
type 'a raw_red_expr = 'a Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]
2929

3030
type 'a and_short_name = 'a Genredexpr.and_short_name
3131
[@@deriving sexp,yojson,hash,compare]
3232

33-
type glob_red_expr = Genredexpr.glob_red_expr
33+
type 'a glob_red_expr = 'a Genredexpr.glob_red_expr
3434
[@@deriving sexp,yojson,hash,compare]

‎serlib/ser_redexpr.ml‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
(************************************************************************)
12+
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
13+
(************************************************************************)
14+
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
15+
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
16+
(* Written by: Emilio J. Gallego Arias and others *)
17+
(************************************************************************)
18+
19+
open Ppx_hash_lib.Std.Hash.Builtin
20+
open Ppx_compare_lib.Builtin
21+
open Sexplib.Std
22+
23+
module Loc = Ser_loc
24+
module Names = Ser_names
25+
module Util = Ser_util
26+
module Locus = Ser_locus
27+
module Libnames = Ser_libnames
28+
module Constrexpr = Ser_constrexpr
29+
module Genintern = Ser_genintern
30+
module Evaluable = Ser_evaluable
31+
module EConstr = Ser_eConstr
32+
module Pattern = Ser_pattern
33+
module Genarg = Ser_genarg
34+
module Genredexpr = Ser_genredexpr
35+
36+
module BO =
37+
struct
38+
let name = "Redexpr.user_red_expr"
39+
type 'a t = 'a Redexpr.user_red_expr
40+
end
41+
module B = SerType.Opaque1(BO)
42+
43+
type 'a user_red_expr = 'a B.t
44+
[@@deriving sexp,yojson,hash,compare]
45+
46+
type raw_red_expr =
47+
[%import: Redexpr.raw_red_expr]
48+
[@@deriving sexp,yojson,hash,compare]
49+
50+
type glob_red_expr =
51+
[%import: Redexpr.glob_red_expr]
52+
[@@deriving sexp,yojson,hash,compare]
53+
54+
module A = struct
55+
56+
type raw =
57+
[%import: Redexpr.raw_red_expr]
58+
[@@deriving sexp,yojson,hash,compare]
59+
60+
type glb =
61+
[%import: Redexpr.glob_red_expr]
62+
[@@deriving sexp,yojson,hash,compare]
63+
64+
type top =
65+
[%import: Redexpr.red_expr]
66+
[@@deriving sexp,yojson,hash,compare]
67+
end
68+
69+
let ser_wit_red_expr = let module M = Ser_genarg.GS(A) in M.genser
70+
71+
let register () =
72+
Ser_genarg.register_genser Redexpr.wit_red_expr ser_wit_red_expr;
73+
()
74+
75+
let _ =
76+
register ()

‎serlib/ser_redexpr.mli‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
(************************************************************************)
12+
(* SerAPI: Coq interaction protocol with bidirectional serialization *)
13+
(************************************************************************)
14+
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *)
15+
(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *)
16+
(* Written by: Emilio J. Gallego Arias and others *)
17+
(************************************************************************)
18+
19+
(*type 'a red_atom = 'a Genredexpr.red_atom
20+
[@@deriving sexp,yojson,hash,compare]
21+
22+
type 'a glob_red_flag = 'a Genredexpr.glob_red_flag
23+
[@@deriving sexp,yojson,hash,compare]
24+
25+
type ('a, 'b, 'c, 'd, 'e) red_expr_gen = ('a, 'b, 'c, 'd, 'e) Genredexpr.red_expr_gen
26+
[@@deriving sexp,yojson,hash,compare]
27+
*)
28+
29+
type 'l user_red_expr = 'l Redexpr.user_red_expr
30+
[@@deriving sexp,yojson,hash,compare]
31+
32+
type raw_red_expr = Redexpr.raw_red_expr
33+
[@@deriving sexp,yojson,hash,compare]
34+
35+
type glob_red_expr = Redexpr.glob_red_expr
36+
[@@deriving sexp,yojson,hash,compare]

‎serlib/ser_vernacexpr.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ module Notation_term = Ser_notation_term
4646
module Hints = Ser_hints
4747
module Goptions = Ser_goptions
4848
module Genredexpr = Ser_genredexpr
49+
module Redexpr = Ser_redexpr
4950
module Universes = Ser_universes
5051
module Attributes = Ser_attributes
5152
module Gramlib = Ser_gramlib

0 commit comments

Comments
 (0)