Merge pull request #276 from ejgallego/sertac

[serlib] Large refactoring, ppx_hash/compare support, better yojson

CHANGES.md

@@ -12,9 +12,14 @@
             (@ejgallego)
  - [deps]   Require cmdliner >= 1.1.0 (@ejgallego)
  - [deps]   Support Jane Street libraries v0.15.0 (@ejgallego)
- - [serlib] Coq AST now support compare and hash (ignoring locations)
-            (@ejgallego)
  - [serapi] New query `Objects` to dump Coq's libobject (@ejgallego)
+ - [serlib] Much improved yojson / json support (@ejgallego)
+ - [serlib] Coq AST now supports ppx_hash intf (ignoring locations by default)
+            (@ejgallego)
+ - [serlib] Coq AST now supports ppx_compare intf (ignoring locations by default)
+            (@ejgallego)
+ - [serlib] Large refactoring on Serlib, using functors, see serlib/README.md
+            (@ejgallego)
 
 ## Version 0.15.1:
 

serlib/README.md

@@ -0,0 +1,5 @@
+## Serlib README
+
+### Builtins
+
+### 

serlib/plugins/firstorder/dune

@@ -2,5 +2,5 @@
  (name serlib_firstorder)
  (public_name coq-serapi.serlib.firstorder)
  (synopsis "Serialization Library for Coq Firstorder Plugin")
- (preprocess (staged_pps ppx_import ppx_sexp_conv))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare))
  (libraries coq-core.plugins.firstorder serlib sexplib))

serlib/plugins/firstorder/ser_g_ground.ml

@@ -1,34 +1,43 @@
-open Sexplib.Conv
 open Serlib
 
+open Sexplib.Conv
+open Ppx_compare_lib.Builtin
+open Ppx_hash_lib.Std.Hash.Builtin
+
 module Loc = Ser_loc
 module Names = Ser_names
 module Libnames = Ser_libnames
 module Locus = Ser_locus
 (* module Globnames = Ser_globnames *)
 
 type h1 = Libnames.qualid list
-[@@deriving sexp]
+  [@@deriving sexp, hash, compare]
 
 type h2 = Names.GlobRef.t Loc.located Locus.or_var list
-[@@deriving sexp]
+[@@deriving sexp, hash, compare]
 
 type h3 = Names.GlobRef.t list
-[@@deriving sexp]
+[@@deriving sexp,hash,compare]
 
 let ser_wit_firstorder_using :
   (Libnames.qualid list,
    Names.GlobRef.t Loc.located Locus.or_var list,
    Names.GlobRef.t list) Ser_genarg.gen_ser =
   Ser_genarg.{
-    raw_ser = sexp_of_h1;
-    raw_des = h1_of_sexp;
-
-    glb_ser = sexp_of_h2;
-    glb_des = h2_of_sexp;
-
-    top_ser = sexp_of_h3;
-    top_des = h3_of_sexp;
+    raw_ser = sexp_of_h1
+  ; raw_des = h1_of_sexp
+  ; raw_hash = hash_fold_h1
+  ; raw_compare = compare_h1
+
+  ; glb_ser = sexp_of_h2
+  ; glb_des = h2_of_sexp
+  ; glb_hash = hash_fold_h2
+  ; glb_compare = compare_h2
+
+  ; top_ser = sexp_of_h3
+  ; top_des = h3_of_sexp
+  ; top_hash = hash_fold_h3
+  ; top_compare = compare_h3
   }
 
 let register () =

serlib/plugins/funind/dune

@@ -2,5 +2,5 @@
  (name serlib_funind)
  (public_name coq-serapi.serlib.funind)
  (synopsis "Serialization Library for Coq Fundind Plugin")
- (preprocess (staged_pps ppx_import ppx_sexp_conv))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare))
  (libraries coq-core.plugins.funind serlib serlib_ltac sexplib))

serlib/plugins/funind/ser_g_indfun.ml

@@ -1,7 +1,13 @@
-open Sexplib.Conv
 open Serlib
 
+open Ppx_compare_lib.Builtin
+open Ppx_hash_lib.Std.Hash.Builtin
+open Sexplib.Conv
+
 module CAst       = Ser_cAst
+module Names      = Ser_names
+module Sorts      = Ser_sorts
+module Libnames   = Ser_libnames
 module Constrexpr = Ser_constrexpr
 module Tactypes   = Ser_tactypes
 module Genintern  = Ser_genintern
@@ -11,87 +17,76 @@ module Tacexpr    = Serlib_ltac.Ser_tacexpr
 module A1 = struct
 
 type h1 = Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option
-[@@deriving sexp]
+[@@deriving sexp,hash,compare]
 type h2 = Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option
-[@@deriving sexp]
+[@@deriving sexp,hash,compare]
 type h3 = Tacexpr.intro_pattern option
-[@@deriving sexp]
+[@@deriving sexp,hash,compare]
 
 end
 
 let ser_wit_with_names =
   let open A1 in
   Ser_genarg.{
-    raw_ser = sexp_of_h1;
-    raw_des = h1_of_sexp;
-
-    glb_ser = sexp_of_h2;
-    glb_des = h2_of_sexp;
-
-    top_ser = sexp_of_h3;
-    top_des = h3_of_sexp;
+    raw_ser = sexp_of_h1
+  ; raw_des = h1_of_sexp
+  ; raw_hash = hash_fold_h1
+  ; raw_compare = compare_h1
+
+  ; glb_ser = sexp_of_h2
+  ; glb_des = h2_of_sexp
+  ; glb_hash = hash_fold_h2
+  ; glb_compare = compare_h2
+
+  ; top_ser = sexp_of_h3
+  ; top_des = h3_of_sexp
+  ; top_hash = hash_fold_h3
+  ; top_compare = compare_h3
   }
 
-module A2 = struct
-type h1 = Constrexpr.constr_expr Tactypes.with_bindings option
-[@@deriving sexp]
-type h2 = Genintern.glob_constr_and_expr Tactypes.with_bindings option
-[@@deriving sexp]
-type h3 = EConstr.t Tactypes.with_bindings Ser_tactypes.delayed_open option
-[@@deriving sexp]
+module WitFI = struct
+  type raw = Constrexpr.constr_expr Tactypes.with_bindings option
+  [@@deriving sexp,hash,compare]
+  type glb = Genintern.glob_constr_and_expr Tactypes.with_bindings option
+  [@@deriving sexp,hash,compare]
+  type top = EConstr.t Tactypes.with_bindings Ser_tactypes.delayed_open option
+  [@@deriving sexp,hash,compare]
 end
 
-let ser_wit_fun_ind_using :
-  (Constrexpr.constr_expr Tactypes.with_bindings option,
-   Genintern.glob_constr_and_expr Tactypes.with_bindings option,
-   EConstr.t Tactypes.with_bindings Tactypes.delayed_open option)
-    Ser_genarg.gen_ser =
-  let open A2 in
-  Ser_genarg.{
-    raw_ser = sexp_of_h1;
-    raw_des = h1_of_sexp;
-
-    glb_ser = sexp_of_h2;
-    glb_des = h2_of_sexp;
+let ser_wit_fun_ind_using = let module M = Ser_genarg.GS(WitFI) in M.genser
 
-    top_ser = sexp_of_h3;
-    top_des = h3_of_sexp;
-  }
-
-let ser_wit_fun_scheme_arg :
-  (Names.variable * Libnames.qualid * Sorts.family, unit, unit)
-    Ser_genarg.gen_ser =
-  Ser_genarg.{
-    raw_ser = sexp_of_triple Ser_names.sexp_of_variable Ser_libnames.sexp_of_qualid Ser_sorts.sexp_of_family;
-    raw_des = triple_of_sexp Ser_names.variable_of_sexp Ser_libnames.qualid_of_sexp Ser_sorts.family_of_sexp;
-
-    glb_ser = sexp_of_unit;
-    glb_des = unit_of_sexp;
+module WitFS = struct
+  type raw = Names.variable * Libnames.qualid * Sorts.family
+  [@@deriving sexp,hash,compare]
+  type glb = unit
+  [@@deriving sexp,hash,compare]
+  type top = unit
+  [@@deriving sexp,hash,compare]
+end
 
-    top_ser = sexp_of_unit;
-    top_des = unit_of_sexp;
-  }
+let ser_wit_fun_scheme_arg = let module M = Ser_genarg.GS(WitFS) in M.genser
 
 module Loc = Ser_loc
 module Vernacexpr = Ser_vernacexpr
 
-type function_fix_definition_loc_argtype = Vernacexpr.fixpoint_expr Loc.located
-  [@@deriving sexp]
+module WFFD = struct
+  type t = Vernacexpr.fixpoint_expr Loc.located
+  [@@deriving sexp,hash,compare]
+end
 
 let ser_wit_function_fix_definition =
-  Ser_genarg.mk_uniform sexp_of_function_fix_definition_loc_argtype function_fix_definition_loc_argtype_of_sexp
-
-let ser_wit_auto_using' =
-  Ser_genarg.{
-    raw_ser = sexp_of_list Ser_constrexpr.sexp_of_constr_expr
-  ; raw_des = list_of_sexp Ser_constrexpr.constr_expr_of_sexp
-
-  ; glb_ser = sexp_of_list Ser_genintern.sexp_of_glob_constr_and_expr
-  ; glb_des = list_of_sexp Ser_genintern.glob_constr_and_expr_of_sexp
+  let module M = Ser_genarg.GS0(WFFD) in M.genser
+
+module WAU = struct
+  type raw = Constrexpr.constr_expr list
+  [@@deriving sexp,hash,compare]
+  type glb = Genintern.glob_constr_and_expr list
+  [@@deriving sexp,hash,compare]
+  type top = EConstr.constr list
+  [@@deriving sexp,hash,compare]
+end
 
-  ; top_ser = sexp_of_list Ser_eConstr.sexp_of_constr
-  ; top_des = list_of_sexp Ser_eConstr.constr_of_sexp
-  }
+let ser_wit_auto_using' = let module M = Ser_genarg.GS(WAU) in M.genser
 
 let register () =
   Ser_genarg.register_genser Funind_plugin.G_indfun.wit_auto_using' ser_wit_auto_using';

serlib/plugins/ltac/dune

@@ -2,5 +2,5 @@
  (name serlib_ltac)
  (public_name coq-serapi.serlib.ltac)
  (synopsis "Serialization Library for Coq [LTAC plugin]")
- (preprocess (staged_pps ppx_import ppx_sexp_conv))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare))
  (libraries coq-core.plugins.ltac serlib sexplib))

serlib/plugins/ltac/ser_rewrite.ml

@@ -13,25 +13,30 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Ppx_hash_lib.Std.Hash.Builtin
+open Ppx_compare_lib.Builtin
 open Sexplib.Conv
 
 type unary_strategy =
   [%import: Rewrite.unary_strategy]
-  [@@deriving sexp]
+  [@@deriving sexp,hash,compare]
 
 type binary_strategy =
   [%import: Rewrite.binary_strategy]
-  [@@deriving sexp]
+  [@@deriving sexp,hash,compare]
 
 type nary_strategy =
   [%import: Rewrite.nary_strategy]
-  [@@deriving sexp]
+  [@@deriving sexp,hash,compare]
 
 type ('a,'b) strategy_ast =
   [%import: ('a,'b) Rewrite.strategy_ast]
-  [@@deriving sexp]
+  [@@deriving sexp,hash,compare]
 
 type strategy = Rewrite.strategy
 
 let strategy_of_sexp = Serlib.Serlib_base.opaque_of_sexp ~typ:"rewrite/strategy"
 let sexp_of_strategy = Serlib.Serlib_base.sexp_of_opaque ~typ:"rewrite/strategy"
+let hash_strategy = Hashtbl.hash
+let hash_fold_strategy st d = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int st (Hashtbl.hash d)
+let compare_strategy = Stdlib.compare

serlib/plugins/ltac/ser_rewrite.mli

@@ -13,21 +13,14 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-open Sexplib
-
 type unary_strategy = Rewrite.unary_strategy
-val unary_strategy_of_sexp : Sexp.t -> unary_strategy
-val sexp_of_unary_strategy : unary_strategy -> Sexp.t
+  [@@deriving sexp, hash, compare]
 
 type binary_strategy = Rewrite.binary_strategy
-val binary_strategy_of_sexp : Sexp.t -> binary_strategy
-val sexp_of_binary_strategy : binary_strategy -> Sexp.t
+  [@@deriving sexp, hash, compare]
 
 type ('a,'b) strategy_ast = ('a,'b) Rewrite.strategy_ast
-
-val strategy_ast_of_sexp : (Sexp.t -> 'a) -> (Sexp.t -> 'b) -> Sexp.t -> ('a,'b) strategy_ast
-val sexp_of_strategy_ast : ('a -> Sexp.t) -> ('b -> Sexp.t) -> ('a,'b) strategy_ast -> Sexp.t
+  [@@deriving sexp, hash, compare]
 
 type strategy = Rewrite.strategy
-val strategy_of_sexp : Sexp.t -> strategy
-val sexp_of_strategy : strategy -> Sexp.t
+  [@@deriving sexp, hash, compare]