From 5405ff0f5275a07309e1e7c8a6cc85ac6eaeecdc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20Jes=C3=BAs=20Gallego=20Arias?= Date: Wed, 21 Feb 2024 19:09:37 +0100 Subject: [PATCH 1/3] Merge pull request #391 from ejgallego/btauto [serlib] Support btauto Coq plugin --- CHANGES.md | 4 ++++ serlib/plugins/btauto/dune | 6 ++++++ 2 files changed, 10 insertions(+) create mode 100644 serlib/plugins/btauto/dune diff --git a/CHANGES.md b/CHANGES.md index 32ee780d..af09d165 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,7 @@ +## Version 0.19.1 + + - [serlib] Support `btauto` Coq plugin (@ejgallego, #362) + ## Version 0.19.0 - [serapi] (!) support for Coq 8.19, thanks to all the developers diff --git a/serlib/plugins/btauto/dune b/serlib/plugins/btauto/dune new file mode 100644 index 00000000..32b6cc6c --- /dev/null +++ b/serlib/plugins/btauto/dune @@ -0,0 +1,6 @@ +(library + (name serlib_btauto) + (public_name coq-serapi.serlib.btauto) + (synopsis "Serialization Library for Coq BTauto Plugin") + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (libraries coq-core.plugins.btauto serlib sexplib)) From 40a2a7a1ac0eb8b2af09f381676d090ea5da65e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emilio=20Jes=C3=BAs=20Gallego=20Arias?= Date: Wed, 21 Feb 2024 21:03:36 +0100 Subject: [PATCH 2/3] 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 ". From a8e2aa5d72b96bceba3ced0df8d0b004d3453046 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 29 Sep 2023 17:31:27 +0200 Subject: [PATCH 3/3] [doc] [license] Improve licensing situation. Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers to a single uniform header - Move JS file to its own file, note that on license. --- CHANGES.md | 2 + LICENSE | 18 +-- coq-serapi.opam | 2 +- serapi/dune | 2 +- serapi/ser_stream.ml | 18 ++- serapi/serapi_assumptions.ml | 14 +- serapi/serapi_assumptions.mli | 14 +- serapi/serapi_doc.ml | 16 +-- serapi/serapi_doc.mli | 15 +-- serapi/serapi_goals.ml | 14 +- serapi/serapi_goals.mli | 14 +- serapi/serapi_paths.ml | 18 +-- serapi/serapi_paths.mli | 15 +-- serapi/serapi_pp.ml | 19 +-- serapi/serapi_pp.mli | 19 +-- serapi/serapi_protocol.ml | 52 ++------ serapi/serapi_protocol.mli | 19 +-- serlib/ide/ser_richpp.ml | 7 +- serlib/ide/ser_richpp.mli | 7 +- serlib/plugins/extraction/ser_g_extraction.ml | 8 ++ serlib/plugins/firstorder/ser_g_ground.ml | 8 ++ serlib/plugins/funind/ser_g_indfun.ml | 8 ++ serlib/plugins/ltac/ser_profile_ltac.ml | 19 +-- serlib/plugins/ltac/ser_profile_ltac.mli | 19 +-- serlib/plugins/ltac/ser_rewrite.ml | 7 +- serlib/plugins/ltac/ser_rewrite.mli | 7 +- serlib/plugins/ltac/ser_tacarg.ml | 7 +- serlib/plugins/ltac/ser_tacarg.mli | 7 +- serlib/plugins/ltac/ser_tacentries.ml | 7 +- serlib/plugins/ltac/ser_tacentries.mli | 7 +- serlib/plugins/ltac/ser_tacenv.ml | 7 +- serlib/plugins/ltac/ser_tacenv.mli | 7 +- serlib/plugins/ltac/ser_tacexpr.ml | 7 +- serlib/plugins/ltac/ser_tacexpr.mli | 17 ++- serlib/plugins/ltac2/ser_g_ltac2.ml | 8 ++ serlib/plugins/ltac2/ser_tac2env.ml | 8 ++ serlib/plugins/ltac2/ser_tac2expr.ml | 8 ++ serlib/plugins/ltac2/ser_tac2quote.ml | 9 +- serlib/plugins/ring/ser_g_ring.ml | 8 ++ serlib/plugins/ssr/ser_ssrast.ml | 13 +- serlib/plugins/ssr/ser_ssrequality.ml | 7 +- serlib/plugins/ssr/ser_ssrparser.ml | 7 +- serlib/plugins/ssr/wrap_ssrast.ml | 8 +- serlib/plugins/ssrmatching/ser_ssrmatching.ml | 7 +- serlib/plugins/syntax/ser_g_number_syntax.ml | 8 ++ serlib/plugins/syntax/ser_number.ml | 8 ++ serlib/serType.ml | 14 +- serlib/serType.mli | 14 +- serlib/ser_attributes.ml | 14 +- serlib/ser_cAst.ml | 20 +-- serlib/ser_cAst.mli | 19 +-- serlib/ser_cEphemeron.ml | 19 +-- serlib/ser_cMap.ml | 14 +- serlib/ser_cMap.mli | 14 +- serlib/ser_cPrimitives.ml | 19 +-- serlib/ser_cSet.ml | 14 +- serlib/ser_cSet.mli | 14 +- serlib/ser_cUnix.ml | 19 +-- serlib/ser_class_tactics.ml | 19 +-- serlib/ser_class_tactics.mli | 19 +-- serlib/ser_constr.ml | 20 +-- serlib/ser_constr.mli | 20 +-- serlib/ser_constr_matching.ml | 20 +-- serlib/ser_constr_matching.mli | 19 +-- serlib/ser_constrexpr.ml | 19 +-- serlib/ser_constrexpr.mli | 19 +-- serlib/ser_context.ml | 20 +-- serlib/ser_context.mli | 20 +-- serlib/ser_conv_oracle.ml | 19 +-- serlib/ser_conv_oracle.mli | 19 +-- serlib/ser_cooking.ml | 14 +- serlib/ser_cooking.mli | 14 +- serlib/ser_coqargs.ml | 19 ++- serlib/ser_dAst.ml | 21 +-- serlib/ser_dAst.mli | 18 +++ serlib/ser_declarations.ml | 20 +-- serlib/ser_declarations.mli | 20 +-- serlib/ser_declaremods.ml | 13 +- serlib/ser_declaremods.mli | 13 +- serlib/ser_decls.ml | 19 +-- serlib/ser_deprecation.ml | 13 +- serlib/ser_eConstr.ml | 23 ++-- serlib/ser_eConstr.mli | 20 +-- serlib/ser_entries.ml | 14 +- serlib/ser_environ.ml | 19 +-- serlib/ser_environ.mli | 19 +-- serlib/ser_equality.ml | 18 +++ serlib/ser_evar.ml | 20 +-- serlib/ser_evar.mli | 20 +-- serlib/ser_evar_kinds.ml | 19 +-- serlib/ser_evar_kinds.mli | 22 +-- serlib/ser_evd.ml | 19 +-- serlib/ser_evd.mli | 19 +-- serlib/ser_extend.ml | 19 +-- serlib/ser_extend.mli | 19 +-- serlib/ser_feedback.ml | 19 +-- serlib/ser_feedback.mli | 19 +-- serlib/ser_flags.ml | 20 +-- serlib/ser_flags.mli | 20 +-- serlib/ser_float64.ml | 14 +- serlib/ser_future.ml | 18 +++ serlib/ser_genarg.ml | 19 +-- serlib/ser_genarg.mli | 19 +-- serlib/ser_genintern.ml | 13 +- serlib/ser_genintern.mli | 13 +- serlib/ser_geninterp.ml | 19 +-- serlib/ser_geninterp.mli | 19 +-- serlib/ser_genredexpr.ml | 19 +-- serlib/ser_genredexpr.mli | 19 +-- serlib/ser_glob_term.ml | 19 +-- serlib/ser_glob_term.mli | 19 +-- serlib/ser_globnames.ml | 19 +-- serlib/ser_goal_select.ml | 17 +-- serlib/ser_goptions.ml | 13 +- serlib/ser_goptions.mli | 13 +- serlib/ser_gramlib.ml | 19 +-- serlib/ser_hints.ml | 19 +-- serlib/ser_hints.mli | 19 +-- serlib/ser_impargs.ml | 19 +-- serlib/ser_impargs.mli | 19 +-- serlib/ser_int.ml | 20 +-- serlib/ser_int.mli | 20 +-- serlib/ser_inv.ml | 19 +-- serlib/ser_inv.mli | 19 +-- serlib/ser_lib.ml | 20 +-- serlib/ser_libnames.ml | 21 +-- serlib/ser_libnames.mli | 19 +-- serlib/ser_libobject.ml | 20 +-- serlib/ser_loadpath.ml | 13 +- serlib/ser_loc.ml | 23 ++-- serlib/ser_loc.mli | 23 ++-- serlib/ser_locality.ml | 19 +-- serlib/ser_locus.ml | 19 +-- serlib/ser_locus.mli | 19 +-- serlib/ser_ltac_pretype.ml | 19 +-- serlib/ser_ltac_pretype.mli | 19 +-- serlib/ser_mod_subst.ml | 21 +-- serlib/ser_mod_subst.mli | 19 +-- serlib/ser_namegen.ml | 21 +-- serlib/ser_names.ml | 14 +- serlib/ser_names.mli | 14 +- serlib/ser_nametab.ml | 19 +-- serlib/ser_nametab.mli | 19 +-- serlib/ser_nativevalues.ml | 13 +- serlib/ser_notation.ml | 22 +-- serlib/ser_notation.mli | 19 +-- serlib/ser_notation_gram.ml | 19 +-- serlib/ser_notation_gram.mli | 19 +-- serlib/ser_notation_term.ml | 21 +-- serlib/ser_notation_term.mli | 19 +-- serlib/ser_notationextern.ml | 19 +-- serlib/ser_notationextern.mli | 19 +-- serlib/ser_numTok.ml | 19 +-- serlib/ser_opaqueproof.ml | 19 +-- serlib/ser_opaqueproof.mli | 19 +-- serlib/ser_pattern.ml | 19 +-- serlib/ser_pattern.mli | 19 +-- serlib/ser_pp.ml | 19 +-- serlib/ser_pp.mli | 19 +-- serlib/ser_ppextend.ml | 19 +-- serlib/ser_ppextend.mli | 19 +-- serlib/ser_pretype_errors.ml | 19 +-- serlib/ser_pretype_errors.mli | 19 +-- serlib/ser_printer.ml | 14 +- serlib/ser_proof.ml | 23 ---- serlib/ser_proof.mli | 21 --- serlib/ser_proof_bullet.ml | 13 +- serlib/ser_range.ml | 19 +-- serlib/ser_reduction.ml | 20 +-- serlib/ser_reduction.mli | 20 +-- serlib/ser_retroknowledge.ml | 19 +-- serlib/ser_retroknowledge.mli | 22 +-- serlib/ser_rtree.ml | 20 +-- serlib/ser_sList.ml | 19 ++- serlib/ser_safe_typing.ml | 14 +- serlib/ser_safe_typing.mli | 14 +- serlib/ser_sorts.ml | 19 +-- serlib/ser_sorts.mli | 19 +-- serlib/ser_stateid.ml | 19 +-- serlib/ser_stateid.mli | 19 +-- serlib/ser_stdarg.ml | 19 +-- serlib/ser_stdarg.mli | 21 +-- serlib/ser_stdlib.ml | 19 +-- serlib/ser_stm.ml | 21 +-- serlib/ser_stm.mli | 19 +-- serlib/ser_summary.ml | 18 +++ serlib/ser_tactics.ml | 19 +-- serlib/ser_tactics.mli | 19 +-- serlib/ser_tactypes.ml | 19 +-- serlib/ser_tok.ml | 19 +-- serlib/ser_tok.mli | 19 +-- serlib/ser_type_errors.ml | 19 +-- serlib/ser_type_errors.mli | 19 +-- serlib/ser_typeclasses.ml | 13 +- serlib/ser_typeclasses.mli | 13 +- serlib/ser_uGraph.ml | 19 +-- serlib/ser_uGraph.mli | 19 +-- serlib/ser_uState.ml | 19 +-- serlib/ser_uint63.ml | 20 +-- serlib/ser_univ.ml | 19 +-- serlib/ser_univ.mli | 19 +-- serlib/ser_univNames.ml | 19 +-- serlib/ser_universes.ml | 13 +- serlib/ser_util.ml | 19 +-- serlib/ser_util.mli | 19 +-- serlib/ser_uvars.ml | 19 +-- serlib/ser_uvars.mli | 19 +-- serlib/ser_vernacexpr.ml | 19 +-- serlib/ser_vernacexpr.mli | 19 +-- serlib/ser_vernacextend.ml | 18 +++ serlib/ser_vmbytecodes.ml | 21 +-- serlib/ser_vmemitcodes.ml | 14 +- serlib/ser_vmemitcodes.mli | 14 +- serlib/ser_vmvalues.ml | 20 +-- serlib/ser_vmvalues.mli | 20 +-- serlib/ser_xml_datatype.ml | 19 +-- serlib/ser_xml_datatype.mli | 19 +-- serlib/serlib_base.ml | 19 +-- serlib/serlib_base.mli | 19 +-- serlib/serlib_init.ml | 18 +++ serlib/serlib_init.mli | 18 +++ sertop/comp_common.ml | 15 ++- sertop/comp_common.mli | 15 ++- sertop/js_sexp_printer.ml | 121 +++++++++++++++++ sertop/js_sexp_printer.mli | 19 +++ sertop/sercomp.ml | 14 +- sertop/sercomp_stats.ml | 14 +- sertop/sercomp_stats.mli | 14 +- sertop/sername.ml | 13 +- sertop/sertok.ml | 13 +- sertop/sertop_arg.ml | 14 +- sertop/sertop_arg.mli | 14 +- sertop/sertop_bin.ml | 14 +- sertop/sertop_init.ml | 14 +- sertop/sertop_init.mli | 14 +- sertop/sertop_loader.ml | 13 +- sertop/sertop_loader.mli | 13 +- sertop/sertop_ser.ml | 17 ++- sertop/sertop_ser.mli | 14 +- sertop/sertop_sexp.ml | 14 +- sertop/sertop_sexp.mli | 18 +-- sertop/sertop_util.ml | 126 +----------------- sertop/sertop_util.mli | 17 +-- 243 files changed, 2428 insertions(+), 1852 deletions(-) delete mode 100644 serlib/ser_proof.ml delete mode 100644 serlib/ser_proof.mli create mode 100644 sertop/js_sexp_printer.ml create mode 100644 sertop/js_sexp_printer.mli diff --git a/CHANGES.md b/CHANGES.md index 33715428..23d34b3d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,8 @@ - [serlib] Support `btauto` Coq plugin (@ejgallego, #362) - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n, #375, fixes #371) + - [general] Make licensing clearer (@ejgallego, @palmskog, + @SnarkBoojum, #361, closes #266) ## Version 0.19.0 diff --git a/LICENSE b/LICENSE index 8b88e2c9..54458aa3 100644 --- a/LICENSE +++ b/LICENSE @@ -3,22 +3,24 @@ Upstream-Name: coq-serapi Upstream-Contact: Emilio J. Gallego Arias Source: https://github.com/ejgallego/coq-serapi License: LGPL-2.1+ -Copyright: 2016-2022, MINES ParisTech / Inria +Copyright: 2016-2023, MINES ParisTech / Inria / others +Authors: Emilio J. Gallego Arias, Karl Palmskog, Clément Pit-Claudel, Kaiyu Yang -Authors: Emilio J. Gallego Arias +Files: sertop/js_sexp_printer.ml* +License: MIT +Copyright: Copyright (c) 2005--2023 Jane Street Group, LLC + +Files: serlib/* serapi/* sertop/ser* sertop/comp* +License: LGPL-2.1+ +Copyright: 2016-2023, MINES ParisTech / Inria / others Files: notes/* License: LGPL-2.1+ / CC-BY-SA 3.0 -Files: jscoq/* -License: GPL-3+ - Files: tests/genarg/* Authors: Karl Palmskog Licence: Derived from many projects as test cases, falls into fair-use Comment: the intent is to be compatible with Coq's license. Note that -the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor -that. In some cases, like when linking with jsCoq's code or other code -that is GPL-3 only, the resulting .js or binaries files will be GPL-3. +the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor that. diff --git a/coq-serapi.opam b/coq-serapi.opam index a0cb06f8..e0d9d626 100644 --- a/coq-serapi.opam +++ b/coq-serapi.opam @@ -3,7 +3,7 @@ maintainer: "e@x80.org" homepage: "https://github.com/ejgallego/coq-serapi" bug-reports: "https://github.com/ejgallego/coq-serapi/issues" dev-repo: "git+https://github.com/ejgallego/coq-serapi.git" -license: "GPL-3.0-or-later" +license: "LGPL-2.1-or-later" doc: "https://ejgallego.github.io/coq-serapi/" synopsis: "Serialization library and protocol for machine interaction with the Coq proof assistant" diff --git a/serapi/dune b/serapi/dune index 8a2044b4..a8e6698b 100644 --- a/serapi/dune +++ b/serapi/dune @@ -2,4 +2,4 @@ (name serapi) (public_name coq-serapi.serapi_v8_14) (synopsis "Serialization Protocol for Coq") - (libraries coq-core.stm coq-core.plugins.ltac sexplib)) + (libraries coq-core.stm coq-core.plugins.ltac sexplib base)) diff --git a/serapi/ser_stream.ml b/serapi/ser_stream.ml index 56cae70b..16b091b5 100644 --- a/serapi/ser_stream.ml +++ b/serapi/ser_stream.ml @@ -1,4 +1,20 @@ -(* Compat_code *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* (* let pfs = Proof_global.get_all_proof_names pstate in *) diff --git a/serapi/serapi_doc.mli b/serapi/serapi_doc.mli index 267c9a88..68cf69fe 100644 --- a/serapi/serapi_doc.mli +++ b/serapi/serapi_doc.mli @@ -1,20 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2021 *) -(* unit diff --git a/serapi/serapi_goals.ml b/serapi/serapi_goals.ml index 1eac1ff6..2c362b35 100644 --- a/serapi/serapi_goals.ml +++ b/serapi/serapi_goals.ml @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* coq_path:string -> string list * Loadpath.vo_path list (* Generate a module name given a file, to be removed in 8.10 *) diff --git a/serapi/serapi_pp.ml b/serapi/serapi_pp.ml index 1834db61..d9412edd 100644 --- a/serapi/serapi_pp.ml +++ b/serapi/serapi_pp.ml @@ -1,16 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let prefix_len = String.length prefix in - String.length s >= prefix_len && loop s ~prefix ~char_equal (prefix_len - 1) - - let is_prefix s ~prefix = is_prefix_gen s ~prefix ~char_equal:(fun x y -> x = y) - - let split_while xs ~f = - let rec loop acc = function - | hd :: tl when f hd -> loop (hd :: acc) tl - | t -> (List.rev acc, t) - in - loop [] xs - - (* End of Core_kernel code, (c) Jane Street *) - (******************************************************************************) + let is_prefix = Base.String.is_prefix + let split_while = Base.List.split_while + (* Custom tokenizer *) let rec stream_tok n_tok acc lstr = let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) lstr in let loc = Gramlib.LStream.get_loc n_tok lstr in diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli index 036e93d4..e3484366 100644 --- a/serapi/serapi_protocol.mli +++ b/serapi/serapi_protocol.mli @@ -1,24 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sexp.t -> 'a data - * val sexp_of_data : ('a -> Sexp.t) -> 'a data -> Sexp.t *) diff --git a/serlib/ser_proof_bullet.ml b/serlib/ser_proof_bullet.ml index 48afa5d2..09ac0803 100644 --- a/serlib/ser_proof_bullet.ml +++ b/serlib/ser_proof_bullet.ml @@ -1,18 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Exninfo.info -> 'a diff --git a/sertop/js_sexp_printer.ml b/sertop/js_sexp_printer.ml new file mode 100644 index 00000000..f4fbfed6 --- /dev/null +++ b/sertop/js_sexp_printer.ml @@ -0,0 +1,121 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* true + (* Avoid unquoted comma at the beggining of the string *) + | ',' -> ix = 0 || loop (ix - 1) + | '|' -> ix > 0 && let next = ix - 1 in str.[next] = '#' || loop next + | '#' -> ix > 0 && let next = ix - 1 in str.[next] = '|' || loop next + | '\000' .. '\032' -> true + | '\248' .. '\255' -> true + | _ -> ix > 0 && loop (ix - 1) + in + loop (len - 1) + +(* XXX: Be faithful to UTF-8 *) +let st_escaped (s : string) = + let sget = String.unsafe_get in + let open Bytes in + let n = ref 0 in + for i = 0 to String.length s - 1 do + n := !n + + (match sget s i with + | '\"' | '\\' | '\n' | '\t' | '\r' | '\b' -> 2 + | ' ' .. '~' -> 1 + (* UTF-8 are valid between \033 -- \247 *) + | '\000' .. '\032' -> 4 + | '\248' .. '\255' -> 4 + | _ -> 1) + done; + if !n = String.length s then Bytes.of_string s else begin + let s' = create !n in + n := 0; + for i = 0 to String.length s - 1 do + begin match sget s i with + | ('\"' | '\\') as c -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n c + | '\n' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'n' + | '\t' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 't' + | '\r' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'r' + | '\b' -> + unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'b' + | (' ' .. '~') as c -> unsafe_set s' !n c + (* Valid UTF-8 are valid between \033 -- \247 *) + | '\000' .. '\032' + | '\248' .. '\255' as c -> + let a = Char.code c in + unsafe_set s' !n '\\'; + incr n; + unsafe_set s' !n (Char.chr (48 + a / 100)); + incr n; + unsafe_set s' !n (Char.chr (48 + (a / 10) mod 10)); + incr n; + unsafe_set s' !n (Char.chr (48 + a mod 10)); + | c -> unsafe_set s' !n c + end; + incr n + done; + s' + end + +let esc_str (str : string) = + let open Bytes in + let estr = st_escaped str in + let elen = length estr in + let res = create (elen + 2) in + blit estr 0 res 1 elen; + set res 0 '"'; + set res (elen + 1) '"'; + to_string res + +let sertop_maybe_esc_str str = + if must_escape str then esc_str str else str + +let rec pp_sertop_internal may_need_space ppf = function + | Atom str -> + let str' = sertop_maybe_esc_str str in + let new_may_need_space = str' == str in + if may_need_space && new_may_need_space then pp_print_string ppf " "; + pp_print_string ppf str'; + new_may_need_space + | List (h :: t) -> + pp_print_string ppf "("; + let may_need_space = pp_sertop_internal false ppf h in + pp_sertop_rest may_need_space ppf t; + false + | List [] -> pp_print_string ppf "()"; false + +and pp_sertop_rest may_need_space ppf = function + | h :: t -> + let may_need_space = pp_sertop_internal may_need_space ppf h in + pp_sertop_rest may_need_space ppf t + | [] -> pp_print_string ppf ")" + +let pp_sertop ppf sexp = ignore (pp_sertop_internal false ppf sexp) diff --git a/sertop/js_sexp_printer.mli b/sertop/js_sexp_printer.mli new file mode 100644 index 00000000..8e8cc0f6 --- /dev/null +++ b/sertop/js_sexp_printer.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Sexplib.Sexp.t -> unit diff --git a/sertop/sercomp.ml b/sertop/sercomp.ml index 9397b9e6..befb8ac9 100644 --- a/sertop/sercomp.ml +++ b/sertop/sercomp.ml @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* unit diff --git a/sertop/sername.ml b/sertop/sername.ml index 6b50b661..ee9c32f2 100644 --- a/sertop/sername.ml +++ b/sertop/sername.ml @@ -1,18 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sertop_util.pp_sertop + | SP_Sertop -> Js_sexp_printer.pp_sertop | SP_Mach -> Sexp.pp | SP_Human -> Sexp.pp_hum @@ -93,7 +93,6 @@ module Impargs = Ser_impargs module Constr = Ser_constr module EConstr = Ser_eConstr module Constrexpr = Ser_constrexpr -module Proof = Ser_proof module Tok = Ser_tok module Ppextend = Ser_ppextend module Notation_gram = Ser_notation_gram diff --git a/sertop/sertop_ser.mli b/sertop/sertop_ser.mli index c86e2948..d06be1bd 100644 --- a/sertop/sertop_ser.mli +++ b/sertop/sertop_ser.mli @@ -1,19 +1,19 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* true - (* Avoid unquoted comma at the beggining of the string *) - | ',' -> ix = 0 || loop (ix - 1) - | '|' -> ix > 0 && let next = ix - 1 in str.[next] = '#' || loop next - | '#' -> ix > 0 && let next = ix - 1 in str.[next] = '|' || loop next - | '\000' .. '\032' -> true - | '\248' .. '\255' -> true - | _ -> ix > 0 && loop (ix - 1) - in - loop (len - 1) - -(* XXX: Be faithful to UTF-8 *) -let st_escaped (s : string) = - let sget = String.unsafe_get in - let open Bytes in - let n = ref 0 in - for i = 0 to String.length s - 1 do - n := !n + - (match sget s i with - | '\"' | '\\' | '\n' | '\t' | '\r' | '\b' -> 2 - | ' ' .. '~' -> 1 - (* UTF-8 are valid between \033 -- \247 *) - | '\000' .. '\032' -> 4 - | '\248' .. '\255' -> 4 - | _ -> 1) - done; - if !n = String.length s then Bytes.of_string s else begin - let s' = create !n in - n := 0; - for i = 0 to String.length s - 1 do - begin match sget s i with - | ('\"' | '\\') as c -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n c - | '\n' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'n' - | '\t' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 't' - | '\r' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'r' - | '\b' -> - unsafe_set s' !n '\\'; incr n; unsafe_set s' !n 'b' - | (' ' .. '~') as c -> unsafe_set s' !n c - (* Valid UTF-8 are valid between \033 -- \247 *) - | '\000' .. '\032' - | '\248' .. '\255' as c -> - let a = Char.code c in - unsafe_set s' !n '\\'; - incr n; - unsafe_set s' !n (Char.chr (48 + a / 100)); - incr n; - unsafe_set s' !n (Char.chr (48 + (a / 10) mod 10)); - incr n; - unsafe_set s' !n (Char.chr (48 + a mod 10)); - | c -> unsafe_set s' !n c - end; - incr n - done; - s' - end - -let esc_str (str : string) = - let open Bytes in - let estr = st_escaped str in - let elen = length estr in - let res = create (elen + 2) in - blit estr 0 res 1 elen; - set res 0 '"'; - set res (elen + 1) '"'; - to_string res - -let sertop_maybe_esc_str str = - if must_escape str then esc_str str else str - -let rec pp_sertop_internal may_need_space ppf = function - | Atom str -> - let str' = sertop_maybe_esc_str str in - let new_may_need_space = str' == str in - if may_need_space && new_may_need_space then pp_print_string ppf " "; - pp_print_string ppf str'; - new_may_need_space - | List (h :: t) -> - pp_print_string ppf "("; - let may_need_space = pp_sertop_internal false ppf h in - pp_sertop_rest may_need_space ppf t; - false - | List [] -> pp_print_string ppf "()"; false - -and pp_sertop_rest may_need_space ppf = function - | h :: t -> - let may_need_space = pp_sertop_internal may_need_space ppf h in - pp_sertop_rest may_need_space ppf t - | [] -> pp_print_string ppf ")" - -let pp_sertop ppf sexp = ignore (pp_sertop_internal false ppf sexp) - -(* XXX: This is terrible and doesn't work yet *) let rec coq_pp_opt (d : Pp.t) = let open Pp in let rec flatten_glue l = match l with | [] -> [] diff --git a/sertop/sertop_util.mli b/sertop/sertop_util.mli index d0509add..8ee77c7e 100644 --- a/sertop/sertop_util.mli +++ b/sertop/sertop_util.mli @@ -1,24 +1,21 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Sexp.t -> unit - val coq_pp_opt : Pp.t -> Pp.t val feedback_pos_filter : string -> Feedback.feedback -> Feedback.feedback