[serlib] Properly support the extraction plugin

We add a test that is complete w.r.t. the 3 genargs as of today.

Co-authored-by: Emilio Jesus Gallego Arias <[email protected]>

CHANGES.md

@@ -1,6 +1,8 @@
 ## unreleased
 
  - [serlib] Support `btauto` Coq plugin (@ejgallego, #362)
+ - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n,
+            #375, fixes #371)
 
 ## Version 0.19.0
 

serlib/plugins/extraction/dune

@@ -2,5 +2,5 @@
  (name serlib_extraction)
  (public_name coq-serapi.serlib.extraction)
  (synopsis "Serialization Library for Coq Fundind 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.extraction serlib))

serlib/plugins/extraction/ser_g_extraction.ml

@@ -1,4 +1,52 @@
+open Serlib
+
+open Sexplib.Conv
+open Ppx_compare_lib.Builtin
+open Ppx_hash_lib.Std.Hash.Builtin
+
+module Names = Ser_names
+
+module Extraction_plugin = struct
+  module G_extraction = Extraction_plugin.G_extraction
+  module Table = struct
+    type int_or_id =
+      [%import: Extraction_plugin.Table.int_or_id]
+      [@@deriving sexp,yojson,hash,compare]
+    type lang =
+      [%import: Extraction_plugin.Table.lang]
+      [@@deriving sexp,yojson,hash,compare]
+  end
+end
+
+module WitII = struct
+  type t = Extraction_plugin.Table.int_or_id
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_int_or_id = let module M = Ser_genarg.GS0(WitII) in M.genser
+
+module WitL = struct
+  type raw = Extraction_plugin.Table.lang
+    [@@deriving sexp,yojson,hash,compare]
+  type glb = unit
+    [@@deriving sexp,yojson,hash,compare]
+  type top = unit
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_language = let module M = Ser_genarg.GS(WitL) in M.genser
+
+module WitMN = struct
+  type t = string
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_mlname = let module M = Ser_genarg.GS0(WitMN) in M.genser
+
 let register () =
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_int_or_id ser_wit_int_or_id;
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_language ser_wit_language;
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_mlname ser_wit_mlname;
   ()
 
 let _ = register ()

tests/genarg/dune

@@ -57,6 +57,11 @@
  (deps (:input exists.v))
  (action (run ./test_roundtrip %{input})))
 
+(rule
+ (alias runtest)
+ (deps (:input extraction.v))
+ (action (run ./test_roundtrip %{input})))
+
 (rule
  (alias runtest)
  (deps (:input firstorder.v))

tests/genarg/extraction.v

@@ -0,0 +1,8 @@
+Require Coq.extraction.Extraction.
+
+Extraction Language Haskell.
+
+Extraction Implicit pred [1].
+
+Axiom Y : Set -> Set -> Set.
+Extract Constant Y "'a" "'b" => " 'a * 'b ".