Merge pull request #402 from SkySkimmer/redexpr-clean

Adapt to coq/coq#18852 (interp_red_expr can be done without ltac)

serlib/plugins/ltac/ser_tacexpr.mli

@@ -148,105 +148,121 @@ val sexp_of_gen_atomic_tactic_expr :
   ('a -> Sexplib.Sexp.t) ->
   ('c -> Sexplib.Sexp.t) ->
   ('d -> Sexplib.Sexp.t) ->
+  ('rp -> Sexplib.Sexp.t) ->
   ('e -> Sexplib.Sexp.t) ->
   ('f -> Sexplib.Sexp.t) ->
   ('g -> Sexplib.Sexp.t) ->
+  ('occvar -> Sexplib.Sexp.t) ->
   ('h -> Sexplib.Sexp.t) ->
   ('i -> Sexplib.Sexp.t) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_atomic_tactic_expr -> Sexplib.Sexp.t
 val sexp_of_gen_tactic_expr :
   ('a -> Sexplib.Sexp.t) ->
   ('c -> Sexplib.Sexp.t) ->
   ('d -> Sexplib.Sexp.t) ->
+  ('rp -> Sexplib.Sexp.t) ->
   ('e -> Sexplib.Sexp.t) ->
   ('f -> Sexplib.Sexp.t) ->
   ('g -> Sexplib.Sexp.t) ->
+  ('occvar -> Sexplib.Sexp.t) ->
   ('h -> Sexplib.Sexp.t) ->
   ('i -> Sexplib.Sexp.t) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_expr -> Sexplib.Sexp.t
 val sexp_of_gen_tactic_arg :
   ('a -> Sexplib.Sexp.t) ->
   ('c -> Sexplib.Sexp.t) ->
   ('d -> Sexplib.Sexp.t) ->
+  ('rp -> Sexplib.Sexp.t) ->
   ('e -> Sexplib.Sexp.t) ->
   ('f -> Sexplib.Sexp.t) ->
   ('g -> Sexplib.Sexp.t) ->
+  ('occvar -> Sexplib.Sexp.t) ->
   ('h -> Sexplib.Sexp.t) ->
   ('i -> Sexplib.Sexp.t) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_arg -> Sexplib.Sexp.t
 val sexp_of_gen_fun_ast :
   ('a -> Sexplib.Sexp.t) ->
   ('c -> Sexplib.Sexp.t) ->
   ('d -> Sexplib.Sexp.t) ->
+  ('rp -> Sexplib.Sexp.t) ->
   ('e -> Sexplib.Sexp.t) ->
   ('f -> Sexplib.Sexp.t) ->
   ('g -> Sexplib.Sexp.t) ->
+  ('occvar -> Sexplib.Sexp.t) ->
   ('h -> Sexplib.Sexp.t) ->
   ('i -> Sexplib.Sexp.t) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_fun_ast -> Sexplib.Sexp.t
 
 val gen_atomic_tactic_expr_of_sexp :
   Sexplib.Sexp.t ->
   (Sexplib.Sexp.t -> 'a) ->
   (Sexplib.Sexp.t -> 'c) ->
   (Sexplib.Sexp.t -> 'd) ->
+  (Sexplib.Sexp.t -> 'rp) ->
   (Sexplib.Sexp.t -> 'e) ->
   (Sexplib.Sexp.t -> 'f) ->
   (Sexplib.Sexp.t -> 'g) ->
+  (Sexplib.Sexp.t -> 'occvar) ->
   (Sexplib.Sexp.t -> 'h) ->
   (Sexplib.Sexp.t -> 'i) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_atomic_tactic_expr
 
 val gen_tactic_expr_of_sexp :
   Sexplib.Sexp.t ->
   (Sexplib.Sexp.t -> 'a) ->
   (Sexplib.Sexp.t -> 'c) ->
   (Sexplib.Sexp.t -> 'd) ->
+  (Sexplib.Sexp.t -> 'rp) ->
   (Sexplib.Sexp.t -> 'e) ->
   (Sexplib.Sexp.t -> 'f) ->
   (Sexplib.Sexp.t -> 'g) ->
+  (Sexplib.Sexp.t -> 'occvar) ->
   (Sexplib.Sexp.t -> 'h) ->
   (Sexplib.Sexp.t -> 'i) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_expr
 
 val gen_tactic_arg_of_sexp :
   Sexplib.Sexp.t ->
   (Sexplib.Sexp.t -> 'a) ->
   (Sexplib.Sexp.t -> 'c) ->
   (Sexplib.Sexp.t -> 'd) ->
+  (Sexplib.Sexp.t -> 'rp) ->
   (Sexplib.Sexp.t -> 'e) ->
   (Sexplib.Sexp.t -> 'f) ->
   (Sexplib.Sexp.t -> 'g) ->
+  (Sexplib.Sexp.t -> 'occvar) ->
   (Sexplib.Sexp.t -> 'h) ->
   (Sexplib.Sexp.t -> 'i) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a  >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_arg
 
 val gen_fun_ast_of_sexp :
   Sexplib.Sexp.t ->
   (Sexplib.Sexp.t -> 'a) ->
   (Sexplib.Sexp.t -> 'c) ->
   (Sexplib.Sexp.t -> 'd) ->
+  (Sexplib.Sexp.t -> 'rp) ->
   (Sexplib.Sexp.t -> 'e) ->
   (Sexplib.Sexp.t -> 'f) ->
   (Sexplib.Sexp.t -> 'g) ->
+  (Sexplib.Sexp.t -> 'occvar) ->
   (Sexplib.Sexp.t -> 'h) ->
   (Sexplib.Sexp.t -> 'i) ->
-  < constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
-    reference : 'f; tacexpr : 'h; term : 'a >
+  < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd;
+    reference : 'f; tacexpr : 'h; term : 'a; >
   Tacexpr.gen_tactic_fun_ast
 
 type glob_tactic_expr = Tacexpr.glob_tactic_expr

serlib/ser_genredexpr.ml

@@ -41,16 +41,20 @@ type 'a glob_red_flag =
   [%import: 'a Genredexpr.glob_red_flag]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a,'b,'c,'d) red_expr_gen0 =
-  [%import: ('a,'b,'c,'d) Genredexpr.red_expr_gen0]
+type ('a,'b,'c) red_context =
+  [%import: ('a,'b,'c) Genredexpr.red_context]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a,'b,'c) red_expr_gen =
-  [%import: ('a,'b,'c) Genredexpr.red_expr_gen]
+type ('a,'b,'c,'d, 'e) red_expr_gen0 =
+  [%import: ('a,'b,'c,'d, 'e) Genredexpr.red_expr_gen0]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a,'b,'c) may_eval =
-  [%import: ('a,'b,'c) Genredexpr.may_eval]
+type ('a,'b,'c,'d) red_expr_gen =
+  [%import: ('a,'b,'c,'d) Genredexpr.red_expr_gen]
+  [@@deriving sexp,yojson,hash,compare]
+
+type ('a,'b,'c,'d) may_eval =
+  [%import: ('a,'b,'c,'d) Genredexpr.may_eval]
   [@@deriving sexp,yojson,hash,compare]
 
 (* Helpers for raw_red_expr *)
@@ -95,21 +99,18 @@ type glob_red_expr =
 module A = struct
 
   type raw =
-    (Ser_constrexpr.constr_expr,
-     Ser_libnames.qualid Ser_constrexpr.or_by_notation,
-     Ser_constrexpr.constr_expr) red_expr_gen
+    [%import: Genredexpr.raw_red_expr]
   [@@deriving sexp,yojson,hash,compare]
 
   type glb =
-    (Ser_genintern.glob_constr_and_expr,
-     Ser_evaluable.t and_short_name Ser_locus.or_var,
-     Ser_genintern.glob_constr_pattern_and_expr) red_expr_gen
+    [%import: Genredexpr.glob_red_expr]
   [@@deriving sexp,yojson,hash,compare]
 
   type top =
     (Ser_eConstr.constr,
      Ser_evaluable.t,
-     Ser_pattern.constr_pattern) red_expr_gen
+     Ser_pattern.constr_pattern,
+     int) red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 end
 

serlib/ser_genredexpr.mli

@@ -30,10 +30,10 @@ val sexp_of_glob_red_flag : ('a -> Sexp.t) -> 'a glob_red_flag -> Sexp.t
 val glob_red_flag_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a glob_red_flag, string) Result.result
 val glob_red_flag_to_yojson : ('a -> Yojson.Safe.t) -> 'a glob_red_flag -> Yojson.Safe.t
 
-type ('a, 'b, 'c) red_expr_gen =  ('a, 'b, 'c) Genredexpr.red_expr_gen
+type ('a, 'b, 'c, 'd) red_expr_gen =  ('a, 'b, 'c, 'd) Genredexpr.red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a, 'b, 'c) may_eval =  ('a, 'b, 'c) Genredexpr.may_eval
+type ('a, 'b, 'c, 'd) may_eval =  ('a, 'b, 'c, 'd) Genredexpr.may_eval
   [@@deriving sexp,yojson,hash,compare]
 
 type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]

serlib/ser_locus.ml

@@ -34,13 +34,17 @@ type occurrences_expr =
   [%import: Locus.occurrences_expr]
   [@@deriving sexp,yojson,hash,compare]
 
-type 'a with_occurrences =
-  [%import: 'a Locus.with_occurrences]
+type 'a with_occurrences_expr =
+  [%import: 'a Locus.with_occurrences_expr]
   [@@deriving sexp,yojson,hash,compare]
 
 type occurrences =
   [%import: Locus.occurrences]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,hash,compare]
+
+type 'a with_occurrences =
+  [%import: 'a Locus.with_occurrences]
+  [@@deriving sexp,yojson,hash,compare]
 
 type hyp_location_flag =
   [%import: Locus.hyp_location_flag]

serlib/ser_locus.mli

@@ -22,19 +22,18 @@ type 'a or_var = 'a Locus.or_var
   [@@deriving sexp,yojson,hash,compare]
 
 type 'a occurrences_gen = 'a Locus.occurrences_gen
-val occurrences_gen_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a occurrences_gen
-val sexp_of_occurrences_gen : ('a -> Sexp.t) -> 'a occurrences_gen -> Sexp.t
+[@@deriving sexp, yojson, hash,compare]
 
 type occurrences_expr = Locus.occurrences_expr
 
 val occurrences_expr_of_sexp : Sexp.t -> occurrences_expr
 val sexp_of_occurrences_expr : occurrences_expr -> Sexp.t
 
+type 'a with_occurrences_expr = 'a Locus.with_occurrences_expr [@@deriving sexp, yojson, hash,compare]
 type 'a with_occurrences = 'a Locus.with_occurrences [@@deriving sexp, yojson, hash,compare]
 
 type occurrences = Locus.occurrences
-val occurrences_of_sexp : Sexp.t -> occurrences
-val sexp_of_occurrences : occurrences -> Sexp.t
+[@@deriving sexp, yojson, hash,compare]
 
 type hyp_location_flag = Locus.hyp_location_flag
   [@@deriving sexp,hash,compare]