diff --git a/CHANGES.md b/CHANGES.md index 6d258abc..cbe16f4c 100644 --- a/CHANGES.md +++ b/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 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 ".