From 40a2a7a1ac0eb8b2af09f381676d090ea5da65e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Emilio=20Jes=C3=BAs=20Gallego=20Arias?= <e+git@x80.org>
Date: Wed, 21 Feb 2024 21:03:36 +0100
Subject: [PATCH] Merge pull request #375 from toku-sa-n/support-extraction

Support the extraction plugin
---
 CHANGES.md                                    |  2 +
 serlib/plugins/extraction/dune                |  2 +-
 serlib/plugins/extraction/ser_g_extraction.ml | 48 +++++++++++++++++++
 tests/genarg/dune                             |  7 ++-
 tests/genarg/extraction.v                     |  8 ++++
 5 files changed, 65 insertions(+), 2 deletions(-)
 create mode 100644 tests/genarg/extraction.v

diff --git a/CHANGES.md b/CHANGES.md
index af09d165..33715428 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,8 @@
 ## Version 0.19.1
 
  - [serlib] Support `btauto` Coq plugin (@ejgallego, #362)
+ - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n,
+            #375, fixes #371)
 
 ## Version 0.19.0
 
diff --git a/serlib/plugins/extraction/dune b/serlib/plugins/extraction/dune
index 112a5b96..ddff288a 100644
--- a/serlib/plugins/extraction/dune
+++ b/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))
diff --git a/serlib/plugins/extraction/ser_g_extraction.ml b/serlib/plugins/extraction/ser_g_extraction.ml
index 4fb1019e..62ddb8e5 100644
--- a/serlib/plugins/extraction/ser_g_extraction.ml
+++ b/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 ()
diff --git a/tests/genarg/dune b/tests/genarg/dune
index 0ed6b41d..11ec5940 100644
--- a/tests/genarg/dune
+++ b/tests/genarg/dune
@@ -10,7 +10,7 @@
    (run chmod +w test_roundtrip)
    ; We insert the digest of the binaries to force a rebuild of the
    ; test cases if the binary has been modified.
-   (bash "echo \"# $(md5sum ../../sertop/sercomp.exe)\" >> test_roundtrip"))))
+   (bash "for i in ../../sertop/sercomp.exe ../../serlib/plugins/*/*.cmxs; do echo \"# $(md5sum $i)\"; done >> test_roundtrip"))))
 
 (rule
  (alias runtest)
@@ -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))
diff --git a/tests/genarg/extraction.v b/tests/genarg/extraction.v
new file mode 100644
index 00000000..ec92c845
--- /dev/null
+++ b/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 ".