diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9e13b225..cc1f678a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -41,7 +41,7 @@ jobs: strategy: fail-fast: false matrix: - ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x] + ocaml-compiler: [4.12.x, 4.13.x, 4.14.x] test-target: [test] extra-opam: [coq.dev] include: @@ -60,6 +60,8 @@ jobs: steps: - uses: actions/checkout@v4 + with: + submodules: true - name: Install apt dependencies run: | sudo apt-get install aptitude @@ -100,7 +102,9 @@ jobs: if: ${{ matrix.extra-opam != '' }} run: opam install ${{ matrix.extra-opam }} - name: Install SerAPI deps - run: opam install --ignore-constraints-on=coq --deps-only . + run: | + opam install --ignore-constraints-on=coq --deps-only vendor/coq-lsp/coq-lsp.opam + opam install --ignore-constraints-on=coq,coq-lsp --deps-only . - name: Build SerAPI run: | opam exec -- make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..15928c53 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,4 @@ +[submodule "vendor/coq-lsp"] + path = vendor/coq-lsp + url = https://github.com/ejgallego/coq-lsp.git + branch = serlib_merge diff --git a/CHANGES.md b/CHANGES.md index 5a1f2a8b..30a077ed 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,8 @@ - [serlib] Support `micromega_core` plugin (@ejgallego) - [serlib] Compat with ppx_deriving 6 (@ejgallego) + - [serlib] Move `serlib` sources to `coq-lsp` (@ejgallego, #409) + - [general] Drop support for OCaml 4.09-4.11 (@ejgallego, #409) ## Version 0.19.3 diff --git a/Makefile b/Makefile index 39b741b7..2ac921ed 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ GITDEPS=$(ls .git/HEAD .git/index) sertop/ser_version.ml: $(GITDEPS) echo "let ser_git_version = \"$(shell git describe --tags || cat VERSION)\";;" > $@ -build: +build: vendor/coq-lsp dune build --root . --only-packages=$(SP_PKGS) @install check: @@ -40,6 +40,23 @@ browser: sertop: build dune exec -- rlwrap sertop +vendor/coq-lsp: + $(error Submodules not initialized, please do "make submodules-init") + +.PHONY: submodules-init +submodules-init: + git submodule update --init + +# Deinitialize submodules +.PHONY: submodules-deinit +submodules-deinit: + git submodule deinit -f --all + +# Update submodules from upstream +.PHONY: submodules-update +submodules-update: + (cd vendor/coq-lsp && git checkout main && git pull upstream main) + ##################################################### # Misc diff --git a/README.md b/README.md index e09f9ccf..dc1fd0e4 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,15 @@ -**Note**: Coq SerAPI is now in maintenance mode, and has been -succeeded by [coq-lsp](https://github.com/ejgallego/coq-lsp/), which -solves many longstanding issues and feature requests. +**Note**: Coq SerAPI has now stopped development, the 0.20 release for +Coq 8.20 will be the last managed by us. Coq SerAPI has been succeeded +by [coq-lsp](https://github.com/ejgallego/coq-lsp/), which solves many +longstanding issues and feature requests. See https://github.com/ejgallego/coq-serapi/issues/252 for more -information. The `serlib` component of this repository is still -active, pending its integration in Coq at some point. +information. The `serlib` component of this repository now lives in +the `coq-lsp` repository.. + +We'd like to thanks all the people that have contributed in one way or +another to SerAPI after all these years, without you neither SerAPI or +`coq-lsp` would have been possible. ## SerAPI: Machine-Friendly, Data-Centric Serialization for Coq diff --git a/coq-serapi.opam b/coq-serapi.opam index 51358f17..48df42cf 100644 --- a/coq-serapi.opam +++ b/coq-serapi.opam @@ -23,19 +23,21 @@ authors: [ ] depends: [ - "ocaml" { >= "4.09.0" } + "dune" { >= "2.0.1" } + "ocaml" { >= "4.12.0" } "coq" { >= "8.20" & < "8.21" | = "dev" } + # We vendor this for now + # "coq-lsp" { >= "0.2.0" } "cmdliner" { >= "1.1.0" } "ocamlfind" { >= "1.8.0" } "sexplib" { >= "v0.13.0" } "dune" { >= "2.0.1" } + "cmdliner" { >= "1.1.0" } + "ocamlfind" { >= "1.8.0" } "ppx_import" { build & >= "1.5-3" & < "2.0" } "ppx_deriving" { >= "4.2.1" } + "sexplib" { >= "v0.13.0" } "ppx_sexp_conv" { >= "v0.13.0" } - "ppx_compare" { >= "v0.13.0" } - "ppx_hash" { >= "v0.13.0" } - "yojson" { >= "1.7.0" } - "ppx_deriving_yojson" { >= "3.4" } ] conflicts: [ diff --git a/dune b/dune new file mode 100644 index 00000000..c558f9f2 --- /dev/null +++ b/dune @@ -0,0 +1,2 @@ +(vendored_dirs vendor) + diff --git a/dune-project b/dune-project index 5020b417..8c084356 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,3 @@ (lang dune 2.0) (formatting (enabled_for ocaml)) (name coq-serapi) - diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index c8161898..6aa5277f 100644 --- a/serapi/serapi_protocol.ml +++ b/serapi/serapi_protocol.ml @@ -584,7 +584,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object | TypeOf id -> snd (QueryUtil.info_of_id env id) | Search -> [CoqString "Not Implemented"] (* XXX: should set printing options in all queries *) - | Vernac q -> let pa = Pcoq.Parsable.make (Ser_stream.of_string q) in + | Vernac q -> let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string q) in Stm.query ~doc ~at:opt.sid ~route:opt.route pa; [] (* XXX: Should set the proper sid state *) | Env -> [CoqEnv env] @@ -700,12 +700,12 @@ module ControlUtil = struct parsing_state_of_st (Stm.state_of_id ~doc ontop) |> Option.map (fun pstate -> let entry = Pcoq.Constr.lconstr in - let pa = Pcoq.Parsable.make (Ser_stream.of_string str) in + let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string str) in Vernacstate.Parser.parse pstate entry pa) let parse_sentence ~doc ~ontop sent = let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in - let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in + let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in let entry = Pvernac.main_entry in Stm.parse_sentence ~doc ontop ~entry pa @@ -718,7 +718,7 @@ module ControlUtil = struct exception End_of_input let add_sentences ~doc opts sent = - let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in + let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in let i = ref 1 in let acc = ref [] in let stt = ref (Extra.value opts.ontop ~default:(Stm.get_current_state ~doc)) in @@ -943,7 +943,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t = | Tokenize input -> let st = CLexer.Lexer.State.get () in begin try - let istr = Ser_stream.of_string input in + let istr = Gramlib.Stream.of_string input in let lex = CLexer.Lexer.tok_func istr in CLexer.Lexer.State.set st; let objs = Extra.stream_tok 0 [] lex in diff --git a/serlib/README.md b/serlib/README.md deleted file mode 100644 index 383b971b..00000000 --- a/serlib/README.md +++ /dev/null @@ -1,142 +0,0 @@ -## Serlib README - -Welcome to `coq-serlib` README. - -`coq-serlib` is a library that declares missing serialization -functions (from/to JSON, sexp), comparison, and hash functions for -most Coq datatypes, allowing users to serialize full ASTs faithfully -for example, and many other interesting use cases. - -`coq-serlib` also includes support for [Coq's extensible syntax]() and -plugins. - -### Builtins and Configuration - -`serlib` provides some builtins and configuration values in the -`Serlib_base` and `Serlib_init` modules. - -### Serializing regular Coq types - -The standard recipe is to use a combination of `ppx_import` and -several ppx-based "derivers" to make `serlib` generate the -corresponding serializers. - -The pattern for a Coq module `Foo` exporting the datatype `bar` and -their constructors is: - -1. create a new OCaml module named `ser_foo.ml` -2. get the corresponding serializers for existing types in scope, this is unusually done in two steps: - - serializers for OCaml Stdlib: -```ocaml -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin -open Sexplib.Std -``` - - serializers for types that `Foo.bar` depends on, for example: -```ocaml -module Names = Ser_names -module EConstr = Ser_eConstr -... -``` -3. implement the serializers for your type. Add to `ser_foo.ml`: -```ocaml -type bar = - [%import: Foo.bar] - [@@deriving sexp,yojson,hash,compare] -``` - -Additionally, you can add an `.mli` file, with the same contents as -above, but in this case, `[@@deriving ...]` will generate the right -interface declarations. - -If `Foo.bar` has no public constructors, `Obj.magic` will be -needed. `serlib` provides helpers for this, see below. - -### Serializing opaque and private types - -`serlib` uses `ppx_import` to retrieve the original type definitions -from Coq; when these are not available, we provide some helpers in the -`SerType` module. Current helpers are: - -- `Biject`: use when it is convenient to provide an isomorphic type to - the one that is "opaque". -- `Pierce`: use when it is not possible to access the type, you really - want to use a copy + `Obj.magic` -- `Opaque`: when you want to declare the type as non-serializable - -**note**: use of `Obj.magic` is now prohibited, all the type piercings -need to use the `Pierce` functor. - -### Serializing GADTS - -Unfortunately, it is not possible to easily serialize GADTS. For now, -we use a very ugly workaround: we basically copy the original Coq -datatype, in non-GADT version, then we pierce the type as their -representation is isomorphic. - -We will use an example from https://github.com/coq/coq/pull/17667#issuecomment-1714473449 : - -```ocaml -type _ gen_pattern = GPat : Genarg.glob_generic_argument -> [ `uninstantiated ] gen_pattern -``` - -In this case, we could indeed derive a serialization function (try -`[@@deriving of_sexp]` for example), however full serialization is -harder, so we may need to provide an alternative data-type: - -```ocaml -module GenPatternRep : SerType.Pierceable1 = struct - - type 'a t = 'a Pattern.gen_pattern - - type _ _t = GPat of Genarg.glob_generic_argument - [@@deriving sexp,yojson,hash,compare] -end - -module GenPatternSer = SerType.Pierce1(GenPatternRep) -type 'a gen_pattern = GenPatternSer.t [@@deriving sexp,yojson,hash,compare] -``` - -and here you go! The main problem with this approach is that it -requires a manual check for each use of `Pierce` and each Coq -version. Fortunately the numbers of `Pierce`'s so far have been very -low. - -### Pre-release checks - -Due to the above, when updating SerAPI for a new release to OPAM, we -must check that the definitions we are piercing are up to date. - -I perform this check with Emacs + Merlin for OCaml: - -- I do `vc-git-grep` for `Pierce(` and `Pierce1(` -- For each use, I use merlin to jump to the original type -- I compare update these types - -That's painful, but takes like 10 minutes, so for now it is doable a -couple of times a year. To illustrate, these are the current -occurrences to check: - -``` -serlib/plugins/ltac2/ser_tac2expr.ml:module T2E = Serlib.SerType.Pierce(T2ESpec) -serlib/plugins/ltac2/ser_tac2expr.ml:module GT2E = Serlib.SerType.Pierce(GT2ESpec) -serlib/ser_cooking.ml:module B_ = SerType.Pierce(CIP) -serlib/ser_environ.ml: include SerType.Pierce(PierceSpec) -serlib/ser_float64.ml:include SerType.Pierce(PierceSpec) -serlib/ser_impargs.ml:module B_ = SerType.Pierce(ISCPierceSpec) -serlib/ser_names.ml:include SerType.Pierce(MBIdBij) -serlib/ser_names.ml: include SerType.Pierce(PierceSpec) -serlib/ser_names.ml: include SerType.Pierce(PierceSpec) -serlib/ser_numTok.ml: include SerType.Pierce(PierceSpec) -serlib/ser_opaqueproof.ml:module B_ = SerType.Pierce(OP) -serlib/ser_opaqueproof.ml:module C_ = SerType.Pierce(OTSpec) -serlib/ser_rtree.ml:include SerType.Pierce1(RTreePierce) -serlib/ser_sList.ml:include SerType.Pierce1(SL) -serlib/ser_safe_typing.ml:module B_ = SerType.Pierce(PC) -serlib/ser_sorts.ml:include SerType.Pierce(PierceSpec) -serlib/ser_stateid.ml:include SerType.Pierce(SId) -serlib/ser_univ.ml: module PierceImp = SerType.Pierce(PierceSpec) -serlib/ser_univ.ml: include SerType.Pierce(PierceSpec) -serlib/ser_univ.ml: include SerType.Pierce(ACPierceDef) -serlib/ser_vmemitcodes.ml:module B = SerType.Pierce(PierceToPatch) -``` diff --git a/serlib/dune b/serlib/dune deleted file mode 100644 index ea8e95a0..00000000 --- a/serlib/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name serlib) - (public_name coq-serapi.serlib) - (synopsis "Serialization Library for Coq") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson)) - (libraries coq-core.stm sexplib)) - diff --git a/serlib/ide/ser_richpp.ml b/serlib/ide/ser_richpp.ml deleted file mode 100644 index df057313..00000000 --- a/serlib/ide/ser_richpp.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Richpp.richpp -val sexp_of_richpp : Richpp.richpp -> Sexp.t - -type 'a located = 'a Richpp.located - -val located_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a Richpp.located -val sexp_of_located : ('a -> Sexp.t) -> 'a Richpp.located -> Sexp.t diff --git a/serlib/plugins/btauto/dune b/serlib/plugins/btauto/dune deleted file mode 100644 index 32b6cc6c..00000000 --- a/serlib/plugins/btauto/dune +++ /dev/null @@ -1,6 +0,0 @@ -(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)) diff --git a/serlib/plugins/cc/dune b/serlib/plugins/cc/dune deleted file mode 100644 index f5b1c520..00000000 --- a/serlib/plugins/cc/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_cc) - (public_name coq-serapi.serlib.cc) - (synopsis "Serialization Library for Coq Congruence Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.cc serlib sexplib)) diff --git a/serlib/plugins/extraction/dune b/serlib/plugins/extraction/dune deleted file mode 100644 index ddff288a..00000000 --- a/serlib/plugins/extraction/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_extraction) - (public_name coq-serapi.serlib.extraction) - (synopsis "Serialization Library for Coq Fundind Plugin") - (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 deleted file mode 100644 index 69cad774..00000000 --- a/serlib/plugins/extraction/ser_g_extraction.ml +++ /dev/null @@ -1,56 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -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.GSV(WitII) in M.genser - -module WitL = struct - type t = Extraction_plugin.Table.lang - [@@deriving sexp,yojson,hash,compare] -end - -let ser_wit_language = let module M = Ser_genarg.GSV(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.GSV(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/serlib/plugins/firstorder/dune b/serlib/plugins/firstorder/dune deleted file mode 100644 index 884e5c8f..00000000 --- a/serlib/plugins/firstorder/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_firstorder) - (public_name coq-serapi.serlib.firstorder) - (synopsis "Serialization Library for Coq Firstorder Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) - (libraries coq-core.plugins.firstorder serlib sexplib)) diff --git a/serlib/plugins/firstorder/ser_g_ground.ml b/serlib/plugins/firstorder/ser_g_ground.ml deleted file mode 100644 index 06d54743..00000000 --- a/serlib/plugins/firstorder/ser_g_ground.ml +++ /dev/null @@ -1,55 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -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, hash, compare] - -type h2 = Names.GlobRef.t Loc.located Locus.or_var list -[@@deriving sexp, hash, compare] - -type h3 = Names.GlobRef.t list -[@@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 - ; 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 () = - Ser_genarg.register_genser Firstorder_plugin.G_ground.wit_firstorder_using ser_wit_firstorder_using; - () - -let _ = register () diff --git a/serlib/plugins/funind/dune b/serlib/plugins/funind/dune deleted file mode 100644 index fb7dcb19..00000000 --- a/serlib/plugins/funind/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_funind) - (public_name coq-serapi.serlib.funind) - (synopsis "Serialization Library for Coq Fundind Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) - (libraries coq-core.plugins.funind serlib serlib_ltac sexplib)) diff --git a/serlib/plugins/funind/ser_g_indfun.ml b/serlib/plugins/funind/ser_g_indfun.ml deleted file mode 100644 index c8dffca9..00000000 --- a/serlib/plugins/funind/ser_g_indfun.ml +++ /dev/null @@ -1,104 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -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 -module EConstr = Ser_eConstr -module Tacexpr = Serlib_ltac.Ser_tacexpr - -module A1 = struct - -type h1 = Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option -[@@deriving sexp,hash,compare] -type h2 = Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option -[@@deriving sexp,hash,compare] -type h3 = Tacexpr.intro_pattern option -[@@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 - ; 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 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 = let module M = Ser_genarg.GS(WitFI) in M.genser - -module WitFS = struct - type t = Names.variable * Libnames.qualid * Sorts.family - [@@deriving sexp,hash,compare] -end - -let ser_wit_fun_scheme_arg = let module M = Ser_genarg.GSV(WitFS) in M.genser - -module Loc = Ser_loc -module Vernacexpr = Ser_vernacexpr - -module WFFD = struct - type t = Vernacexpr.fixpoint_expr Loc.located - [@@deriving sexp,hash,compare] -end - -let ser_wit_function_fix_definition = - 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 - -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'; - Ser_genarg.register_genser Funind_plugin.G_indfun.wit_constr_comma_sequence' ser_wit_auto_using'; - Ser_genarg.register_genser Funind_plugin.G_indfun.wit_with_names ser_wit_with_names; - Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_ind_using ser_wit_fun_ind_using; - Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_scheme_arg ser_wit_fun_scheme_arg; - Ser_genarg.register_genser Funind_plugin.G_indfun.wit_function_fix_definition ser_wit_function_fix_definition; - () - -let _ = register () diff --git a/serlib/plugins/ltac/dune b/serlib/plugins/ltac/dune deleted file mode 100644 index 16d06c8a..00000000 --- a/serlib/plugins/ltac/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_ltac) - (public_name coq-serapi.serlib.ltac) - (synopsis "Serialization Library for Coq [LTAC plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.ltac serlib sexplib)) diff --git a/serlib/plugins/ltac/ser_rewrite.ml b/serlib/plugins/ltac/ser_rewrite.ml deleted file mode 100644 index 299b88b6..00000000 --- a/serlib/plugins/ltac/ser_rewrite.ml +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ITac.TacIntroPattern(a,b) - | Ltac_plugin.Tacexpr.TacApply (a,b,c,d) -> ITac.TacApply (a,b,c,d) - | Ltac_plugin.Tacexpr.TacElim (a,b,c) -> ITac.TacElim (a,b,c) - | Ltac_plugin.Tacexpr.TacCase (a,b) -> ITac.TacCase (a,b) - | Ltac_plugin.Tacexpr.TacMutualFix (a,b,c) -> ITac.TacMutualFix (a,b,c) - | Ltac_plugin.Tacexpr.TacMutualCofix (a,b) -> ITac.TacMutualCofix (a,b) - | Ltac_plugin.Tacexpr.TacAssert (a,b,c,d,e) -> ITac.TacAssert (a,b,c,d,e) - | Ltac_plugin.Tacexpr.TacGeneralize a -> ITac.TacGeneralize a - | Ltac_plugin.Tacexpr.TacLetTac (a,b,c,d,e,f) -> ITac.TacLetTac (a,b,c,d,e,f) - | Ltac_plugin.Tacexpr.TacInductionDestruct (a,b,c) -> ITac.TacInductionDestruct (a,b,c) - | Ltac_plugin.Tacexpr.TacReduce (a,b) -> ITac.TacReduce (a,b) - | Ltac_plugin.Tacexpr.TacChange (a,b,c,d) -> ITac.TacChange (a,b,c,d) - | Ltac_plugin.Tacexpr.TacRewrite (a,b,c,d) -> ITac.TacRewrite (a,b,c,d) - | Ltac_plugin.Tacexpr.TacInversion (a,b) -> ITac.TacInversion (a,b) -and _gen_tactic_arg_put (t : 'a Ltac_plugin.Tacexpr.gen_tactic_arg) : - ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_arg = match t with - | Ltac_plugin.Tacexpr.TacGeneric (a,b) -> ITac.TacGeneric (a,b) - | Ltac_plugin.Tacexpr.ConstrMayEval a -> ITac.ConstrMayEval a - | Ltac_plugin.Tacexpr.Reference a -> ITac.Reference a - | Ltac_plugin.Tacexpr.TacCall l -> ITac.TacCall C.(map (fun (b,c) -> (b, List.map _gen_tactic_arg_put c)) l) - | Ltac_plugin.Tacexpr.TacFreshId a -> ITac.TacFreshId a - | Ltac_plugin.Tacexpr.Tacexp a -> ITac.Tacexp a - | Ltac_plugin.Tacexpr.TacPretype a -> ITac.TacPretype a - | Ltac_plugin.Tacexpr.TacNumgoals -> ITac.TacNumgoals -and _gen_tactic_expr_r_put (t : 'a Ltac_plugin.Tacexpr.gen_tactic_expr_r) : - ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_expr_r = - let u x = _gen_tactic_expr_put x in - let uu x = List.map u x in - let ua x = Array.map u x in - match t with - | Ltac_plugin.Tacexpr.TacAtom l -> ITac.TacAtom (_gen_atomic_tactic_expr_put l) - | Ltac_plugin.Tacexpr.TacThen (a,b) -> ITac.TacThen (u a, u b) - | Ltac_plugin.Tacexpr.TacDispatch a -> ITac.TacDispatch (uu a) - | Ltac_plugin.Tacexpr.TacExtendTac (a,b,c) -> ITac.TacExtendTac (ua a, u b, ua c) - | Ltac_plugin.Tacexpr.TacThens (a,b) -> ITac.TacThens (u a, uu b) - | Ltac_plugin.Tacexpr.TacThens3parts (a,b,c,d) -> ITac.TacThens3parts (u a, ua b, u c, ua d) - | Ltac_plugin.Tacexpr.TacFirst a -> ITac.TacFirst (uu a) - | Ltac_plugin.Tacexpr.TacSolve a -> ITac.TacSolve (uu a) - | Ltac_plugin.Tacexpr.TacTry a -> ITac.TacTry (u a) - | Ltac_plugin.Tacexpr.TacOr (a,b) -> ITac.TacOr (u a, u b) - | Ltac_plugin.Tacexpr.TacOnce a -> ITac.TacOnce (u a) - | Ltac_plugin.Tacexpr.TacExactlyOnce a -> ITac.TacExactlyOnce (u a) - | Ltac_plugin.Tacexpr.TacIfThenCatch (a,b,c) -> ITac.TacIfThenCatch (u a,u b,u c) - | Ltac_plugin.Tacexpr.TacOrelse (a,b) -> ITac.TacOrelse (u a,u b) - | Ltac_plugin.Tacexpr.TacDo (a,b) -> ITac.TacDo (a,u b) - | Ltac_plugin.Tacexpr.TacTimeout (a,b) -> ITac.TacTimeout (a,u b) - | Ltac_plugin.Tacexpr.TacTime (a,b) -> ITac.TacTime (a,u b) - | Ltac_plugin.Tacexpr.TacRepeat a -> ITac.TacRepeat (u a) - | Ltac_plugin.Tacexpr.TacProgress a -> ITac.TacProgress (u a) - (* | Ltac_plugin.Tacexpr.TacShowHyps a -> ITac.TacShowHyps (u a) *) - | Ltac_plugin.Tacexpr.TacAbstract (a,b) -> ITac.TacAbstract (u a,b) - | Ltac_plugin.Tacexpr.TacId a -> ITac.TacId a - | Ltac_plugin.Tacexpr.TacFail (a,b,c) -> ITac.TacFail (a,b,c) - (* | Ltac_plugin.Tacexpr.TacInfo a -> ITac.TacInfo (u a) *) - (* | TacLetIn of rec_flag * *) - (* (Names.Id.t located * 'a gen_tactic_arg) list * *) - (* 'a gen_tactic_expr *) - | Ltac_plugin.Tacexpr.TacLetIn (a, l, t) -> - let _pt = List.map (fun (a,t) -> (a,_gen_tactic_arg_put t)) in - ITac.TacLetIn (a, _pt l, _gen_tactic_expr_put t) - (* | TacMatch of lazy_flag * *) - (* 'a gen_tactic_expr * *) - (* ('p,'a gen_tactic_expr) match_rule list *) - (* type ('a,'t) match_rule = *) - (* | Pat of 'a match_context_hyps list * 'a match_pattern * 't *) - (* | All of 't *) - | Ltac_plugin.Tacexpr.TacMatch (a, e, mr) -> - let _pmr = List.map (function - | Ltac_plugin.Tacexpr.Pat (a,b,t) -> Ltac_plugin.Tacexpr.Pat (a,b,_gen_tactic_expr_put t) - | Ltac_plugin.Tacexpr.All e -> Ltac_plugin.Tacexpr.All (_gen_tactic_expr_put e) - ) in - ITac.TacMatch(a, _gen_tactic_expr_put e, _pmr mr) - | Ltac_plugin.Tacexpr.TacMatchGoal (e, d, t) -> - let _pmr = List.map (function - | Ltac_plugin.Tacexpr.Pat (a,b,t) -> Ltac_plugin.Tacexpr.Pat (a,b,_gen_tactic_expr_put t) - | Ltac_plugin.Tacexpr.All e -> Ltac_plugin.Tacexpr.All (_gen_tactic_expr_put e) - ) in - ITac.TacMatchGoal(e, d, _pmr t) - | Ltac_plugin.Tacexpr.TacFun a -> ITac.TacFun (_gen_tactic_fun_ast_put a) - | Ltac_plugin.Tacexpr.TacArg l -> ITac.TacArg (_gen_tactic_arg_put l) - | Ltac_plugin.Tacexpr.TacSelect(gs,te) -> ITac.TacSelect(gs, _gen_tactic_expr_put te) - | Ltac_plugin.Tacexpr.TacML (l,m) -> ITac.TacML (l, List.map _gen_tactic_arg_put m) - | Ltac_plugin.Tacexpr.TacAlias (l,m) -> ITac.TacAlias (l, List.map _gen_tactic_arg_put m) -and _gen_tactic_expr_put (t : _ Ltac_plugin.Tacexpr.gen_tactic_expr) = - C.map _gen_tactic_expr_r_put t - -and _gen_tactic_fun_ast_put (t : 'a Ltac_plugin.Tacexpr.gen_tactic_fun_ast) : - ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_fun_ast = - match t with - | (a,b) -> (a, _gen_tactic_expr_put b) - -let rec _gen_atom_tactic_expr_get (t : ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_atomic_tactic_expr) : - 'a Ltac_plugin.Tacexpr.gen_atomic_tactic_expr = match t with - | ITac.TacIntroPattern(a,b) -> Ltac_plugin.Tacexpr.TacIntroPattern(a,b) - | ITac.TacApply (a,b,c,d) -> Ltac_plugin.Tacexpr.TacApply (a,b,c,d) - | ITac.TacElim (a,b,c) -> Ltac_plugin.Tacexpr.TacElim (a,b,c) - | ITac.TacCase (a,b) -> Ltac_plugin.Tacexpr.TacCase (a,b) - | ITac.TacMutualFix (a,b,c) -> Ltac_plugin.Tacexpr.TacMutualFix (a,b,c) - | ITac.TacMutualCofix (a,b) -> Ltac_plugin.Tacexpr.TacMutualCofix (a,b) - | ITac.TacAssert (a,b,c,d,e) -> Ltac_plugin.Tacexpr.TacAssert (a,b,c,d,e) - | ITac.TacGeneralize a -> Ltac_plugin.Tacexpr.TacGeneralize a - | ITac.TacLetTac (a,b,c,d,e,f) -> Ltac_plugin.Tacexpr.TacLetTac (a,b,c,d,e,f) - | ITac.TacInductionDestruct (a,b,c) -> Ltac_plugin.Tacexpr.TacInductionDestruct (a,b,c) - | ITac.TacReduce (a,b) -> Ltac_plugin.Tacexpr.TacReduce (a,b) - | ITac.TacChange (a,b,c,d) -> Ltac_plugin.Tacexpr.TacChange (a,b,c,d) - | ITac.TacRewrite (a,b,c,d) -> Ltac_plugin.Tacexpr.TacRewrite (a,b,c,d) - | ITac.TacInversion (a,b) -> Ltac_plugin.Tacexpr.TacInversion (a,b) -and _gen_tactic_arg_get (t : ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_arg) : - 'a Ltac_plugin.Tacexpr.gen_tactic_arg = match t with - | ITac.TacGeneric(a,b) -> Ltac_plugin.Tacexpr.TacGeneric (a,b) - | ITac.ConstrMayEval a -> Ltac_plugin.Tacexpr.ConstrMayEval a - | ITac.Reference a -> Ltac_plugin.Tacexpr.Reference a - | ITac.TacCall l -> Ltac_plugin.Tacexpr.TacCall C.(map (fun (b,c) -> (b, List.map _gen_tactic_arg_get c)) l) - | ITac.TacFreshId a -> Ltac_plugin.Tacexpr.TacFreshId a - | ITac.Tacexp a -> Ltac_plugin.Tacexpr.Tacexp a - | ITac.TacPretype a -> Ltac_plugin.Tacexpr.TacPretype a - | ITac.TacNumgoals -> Ltac_plugin.Tacexpr.TacNumgoals -and _gen_tactic_expr_r_get (t : ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_expr_r) : - 'a Ltac_plugin.Tacexpr.gen_tactic_expr_r = - let u x = _gen_tactic_expr_get x in - let uu x = List.map u x in - let ua x = Array.map u x in - match t with - | ITac.TacAtom l -> Ltac_plugin.Tacexpr.TacAtom (_gen_atom_tactic_expr_get l) - | ITac.TacThen (a,b) -> Ltac_plugin.Tacexpr.TacThen (u a, u b) - | ITac.TacDispatch a -> Ltac_plugin.Tacexpr.TacDispatch (uu a) - | ITac.TacExtendTac (a,b,c) -> Ltac_plugin.Tacexpr.TacExtendTac (ua a, u b, ua c) - | ITac.TacThens (a,b) -> Ltac_plugin.Tacexpr.TacThens (u a, uu b) - | ITac.TacThens3parts (a,b,c,d) -> Ltac_plugin.Tacexpr.TacThens3parts (u a, ua b, u c, ua d) - | ITac.TacFirst a -> Ltac_plugin.Tacexpr.TacFirst (uu a) - | ITac.TacSolve a -> Ltac_plugin.Tacexpr.TacSolve (uu a) - | ITac.TacTry a -> Ltac_plugin.Tacexpr.TacTry (u a) - | ITac.TacOr (a,b) -> Ltac_plugin.Tacexpr.TacOr (u a, u b) - | ITac.TacOnce a -> Ltac_plugin.Tacexpr.TacOnce (u a) - | ITac.TacExactlyOnce a -> Ltac_plugin.Tacexpr.TacExactlyOnce (u a) - | ITac.TacIfThenCatch (a,b,c) -> Ltac_plugin.Tacexpr.TacIfThenCatch (u a,u b,u c) - | ITac.TacOrelse (a,b) -> Ltac_plugin.Tacexpr.TacOrelse (u a,u b) - | ITac.TacDo (a,b) -> Ltac_plugin.Tacexpr.TacDo (a,u b) - | ITac.TacTimeout (a,b) -> Ltac_plugin.Tacexpr.TacTimeout (a,u b) - | ITac.TacTime (a,b) -> Ltac_plugin.Tacexpr.TacTime (a,u b) - | ITac.TacRepeat a -> Ltac_plugin.Tacexpr.TacRepeat (u a) - | ITac.TacProgress a -> Ltac_plugin.Tacexpr.TacProgress (u a) - (* | ITac.TacShowHyps a -> Ltac_plugin.Tacexpr.TacShowHyps (u a) *) - | ITac.TacAbstract (a,b) -> Ltac_plugin.Tacexpr.TacAbstract (u a,b) - | ITac.TacId a -> Ltac_plugin.Tacexpr.TacId a - | ITac.TacFail (a,b,c) -> Ltac_plugin.Tacexpr.TacFail (a,b,c) - (* | ITac.TacInfo a -> Ltac_plugin.Tacexpr.TacInfo (u a) *) - | ITac.TacLetIn (a, l, t) -> - let _pt = List.map (fun (a,t) -> (a,_gen_tactic_arg_get t)) in - Ltac_plugin.Tacexpr.TacLetIn (a, _pt l, _gen_tactic_expr_get t) - | ITac.TacMatch (a,e,mr) -> - let _gmr = List.map (function - | Ltac_plugin.Tacexpr.Pat (a,b,t) -> Ltac_plugin.Tacexpr.Pat (a,b,_gen_tactic_expr_get t) - | Ltac_plugin.Tacexpr.All e -> Ltac_plugin.Tacexpr.All (_gen_tactic_expr_get e) - ) in - Ltac_plugin.Tacexpr.TacMatch(a, _gen_tactic_expr_get e, _gmr mr) - | ITac.TacMatchGoal (a,d,t) -> - let _gmr = List.map (function - | Ltac_plugin.Tacexpr.Pat (a,b,t) -> Ltac_plugin.Tacexpr.Pat (a,b,_gen_tactic_expr_get t) - | Ltac_plugin.Tacexpr.All e -> Ltac_plugin.Tacexpr.All (_gen_tactic_expr_get e) - ) in - Ltac_plugin.Tacexpr.TacMatchGoal(a,d, _gmr t) - | ITac.TacFun a -> Ltac_plugin.Tacexpr.TacFun (_gen_tactic_fun_ast_get a) - | ITac.TacArg l -> Ltac_plugin.Tacexpr.TacArg (_gen_tactic_arg_get l) - | ITac.TacSelect(gs,te) -> Ltac_plugin.Tacexpr.TacSelect(gs, _gen_tactic_expr_get te) - | ITac.TacML (l,m) -> Ltac_plugin.Tacexpr.TacML (l, List.map _gen_tactic_arg_get m) - | ITac.TacAlias (l,m) -> Ltac_plugin.Tacexpr.TacAlias (l, List.map _gen_tactic_arg_get m) - -and _gen_tactic_expr_get (t : ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_expr) : - 'a Ltac_plugin.Tacexpr.gen_tactic_expr = - C.map _gen_tactic_expr_r_get t - -and _gen_tactic_fun_ast_get (t : ('t, 'dtrm, 'p, 'rp, 'c, 'r, 'n, 'occvar, 'tacexpr, 'l) ITac.gen_tactic_fun_ast) : - 'a Ltac_plugin.Tacexpr.gen_tactic_fun_ast = - match t with - | (a,b) -> (a, _gen_tactic_expr_get b) - -type 'd gen_atomic_tactic_expr = 'd Ltac_plugin.Tacexpr.gen_atomic_tactic_expr - -(* Sexp part for generic functions *) - -let sexp_of_gen_atomic_tactic_expr - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_atomic_tactic_expr) : Sexp.t = - ITac.sexp_of_gen_atomic_tactic_expr t d p rp c r n ov te l (_gen_atomic_tactic_expr_put tac) - -let sexp_of_gen_tactic_expr - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_tactic_expr) : Sexp.t = - ITac.sexp_of_gen_tactic_expr t d p rp c r n ov te l (_gen_tactic_expr_put tac) - -let sexp_of_gen_tactic_arg - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_tactic_arg) : Sexp.t = - ITac.sexp_of_gen_tactic_arg t d p rp c r n ov te l (_gen_tactic_arg_put tac) - -let sexp_of_gen_fun_ast - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_tactic_fun_ast) : Sexp.t = - ITac.sexp_of_gen_tactic_fun_ast t d p rp c r n ov te l (_gen_tactic_fun_ast_put tac) - -let gen_atomic_tactic_expr_of_sexp (tac : Sexp.t) - t d p rp c r n ov te l : 'a Ltac_plugin.Tacexpr.gen_atomic_tactic_expr = - _gen_atom_tactic_expr_get (ITac.gen_atomic_tactic_expr_of_sexp t d p rp c r n ov te l tac) - -let gen_tactic_expr_of_sexp (tac : Sexp.t) - t d p rp c r n ov te l : 'a Ltac_plugin.Tacexpr.gen_tactic_expr = - _gen_tactic_expr_get (ITac.gen_tactic_expr_of_sexp t d p rp c r n ov te l tac) - -let gen_tactic_arg_of_sexp (tac : Sexp.t) - t d p rp c r n ov te l : 'a Ltac_plugin.Tacexpr.gen_tactic_arg = - _gen_tactic_arg_get (ITac.gen_tactic_arg_of_sexp t d p rp c r n ov te l tac) - -let gen_fun_ast_of_sexp (tac : Sexp.t) - t d p rp c r n ov te l : 'a Ltac_plugin.Tacexpr.gen_tactic_fun_ast = - _gen_tactic_fun_ast_get (ITac.gen_tactic_fun_ast_of_sexp t d p rp c r n ov te l tac) - -(* Yojson part for generic functions *) - -let gen_atomic_tactic_expr_to_yojson - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_atomic_tactic_expr) : _ = - ITac.gen_atomic_tactic_expr_to_yojson t d p rp c r n ov te l (_gen_atomic_tactic_expr_put tac) - -let gen_tactic_expr_to_yojson - t d p rp c r n ov te l (tac : 'a Ltac_plugin.Tacexpr.gen_tactic_expr) : Yojson.Safe.t = - ITac.gen_tactic_expr_to_yojson t d p rp c r n ov te l (_gen_tactic_expr_put tac) - -let gen_tactic_expr_of_yojson tac - t d p rp c r n ov te l : ('a Ltac_plugin.Tacexpr.gen_tactic_expr, _) result = - Result.map _gen_tactic_expr_get (ITac.gen_tactic_expr_of_yojson t d p rp c r n ov te l tac) - -let gen_atomic_tactic_expr_of_yojson tac - t d p rp c r n ov te l : ('a Ltac_plugin.Tacexpr.gen_atomic_tactic_expr, _) result = - Result.map _gen_atom_tactic_expr_get (ITac.gen_atomic_tactic_expr_of_yojson t d p rp c r n ov te l tac) - -(* Hash part for generic functions *) - -let hash_fold_gen_tactic_expr t d p rp c r n ov te l st tac = - ITac.hash_fold_gen_tactic_expr t d p rp c r n ov te l st (_gen_tactic_expr_put tac) - -let hash_fold_gen_atomic_tactic_expr t d p rp c r n ov te l st tac = - ITac.hash_fold_gen_atomic_tactic_expr t d p rp c r n ov te l st (_gen_atomic_tactic_expr_put tac) - -(* Compare part for generic functions *) - -let compare_gen_tactic_expr t d p rp c r n ov te l t1 t2 : int = - ITac.compare_gen_tactic_expr t d p rp c r n ov te l (_gen_tactic_expr_put t1) (_gen_tactic_expr_put t2) - -let compare_gen_atomic_tactic_expr t d p rp c r n ov te l t1 t2 = - ITac.compare_gen_atomic_tactic_expr t d p rp c r n ov te l (_gen_atomic_tactic_expr_put t1) (_gen_atomic_tactic_expr_put t2) - -(************************************************************************) -(* Main tactics types, we follow tacexpr and provide glob,raw, and *) -(* atomic *) -(************************************************************************) - -(* Glob *) -type glob_tactic_expr = Ltac_plugin.Tacexpr.glob_tactic_expr -type glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr - -let rec glob_tactic_expr_of_sexp tac = - gen_tactic_expr_of_sexp - tac - Genintern.glob_constr_and_expr_of_sexp - Genintern.glob_constr_and_expr_of_sexp - Genintern.glob_constr_pattern_and_expr_of_sexp - Genintern.glob_constr_and_expr_of_sexp - (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Evaluable.t_of_sexp)) - (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp)) - Names.lident_of_sexp - (Locus.or_var_of_sexp int_of_sexp) - glob_tactic_expr_of_sexp - Genarg.glevel_of_sexp -and glob_atomic_tactic_expr_of_sexp tac = - gen_atomic_tactic_expr_of_sexp - tac - Genintern.glob_constr_and_expr_of_sexp - Genintern.glob_constr_and_expr_of_sexp - Genintern.glob_constr_pattern_and_expr_of_sexp - Genintern.glob_constr_and_expr_of_sexp - (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Evaluable.t_of_sexp)) - (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp)) - Names.lident_of_sexp - (Locus.or_var_of_sexp int_of_sexp) - glob_tactic_expr_of_sexp - Genarg.glevel_of_sexp - -let rec sexp_of_glob_tactic_expr (tac : glob_tactic_expr) = - sexp_of_gen_tactic_expr - Genintern.sexp_of_glob_constr_and_expr - Genintern.sexp_of_glob_constr_and_expr - Genintern.sexp_of_glob_constr_pattern_and_expr - Genintern.sexp_of_glob_constr_and_expr - (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Evaluable.sexp_of_t)) - (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant)) - Names.sexp_of_lident - (Locus.sexp_of_or_var sexp_of_int) - sexp_of_glob_tactic_expr - Genarg.sexp_of_glevel - tac -and sexp_of_glob_atomic_tactic_expr (tac : glob_atomic_tactic_expr) = - sexp_of_gen_atomic_tactic_expr - Genintern.sexp_of_glob_constr_and_expr - Genintern.sexp_of_glob_constr_and_expr - Genintern.sexp_of_glob_constr_pattern_and_expr - Genintern.sexp_of_glob_constr_and_expr - (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Evaluable.sexp_of_t)) - (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant)) - Names.sexp_of_lident - (Locus.sexp_of_or_var sexp_of_int) - sexp_of_glob_tactic_expr - Genarg.sexp_of_glevel - tac - -let rec glob_tactic_expr_of_yojson tac = - gen_tactic_expr_of_yojson - tac - Genintern.glob_constr_and_expr_of_yojson - Genintern.glob_constr_and_expr_of_yojson - Genintern.glob_constr_pattern_and_expr_of_yojson - Genintern.glob_constr_and_expr_of_yojson - (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Evaluable.of_yojson)) - (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson)) - Names.lident_of_yojson - (Locus.or_var_of_yojson Ser_int.of_yojson) - glob_tactic_expr_of_yojson - Genarg.glevel_of_yojson -and glob_atomic_tactic_expr_of_yojson tac = - gen_atomic_tactic_expr_of_yojson - tac - Genintern.glob_constr_and_expr_of_yojson - Genintern.glob_constr_and_expr_of_yojson - Genintern.glob_constr_pattern_and_expr_of_yojson - Genintern.glob_constr_and_expr_of_yojson - (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Evaluable.of_yojson)) - (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson)) - Names.lident_of_yojson - (Locus.or_var_of_yojson Ser_int.of_yojson) - glob_tactic_expr_of_yojson - Genarg.glevel_of_yojson - -let rec glob_tactic_expr_to_yojson tac = - gen_tactic_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - Genintern.glob_constr_pattern_and_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Evaluable.to_yojson)) - (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson)) - Names.lident_to_yojson - (Locus.or_var_to_yojson Ser_int.to_yojson) - glob_tactic_expr_to_yojson - Genarg.glevel_to_yojson - tac -and glob_atomic_tactic_expr_to_yojson tac = - gen_atomic_tactic_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - Genintern.glob_constr_pattern_and_expr_to_yojson - Genintern.glob_constr_and_expr_to_yojson - (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Evaluable.to_yojson)) - (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson)) - Names.lident_to_yojson - (Locus.or_var_to_yojson Ser_int.to_yojson) - glob_tactic_expr_to_yojson - Genarg.glevel_to_yojson - tac - -let rec hash_fold_glob_tactic_expr st tac = - hash_fold_gen_tactic_expr - Genintern.hash_fold_glob_constr_and_expr - Genintern.hash_fold_glob_constr_and_expr - Genintern.hash_fold_glob_constr_pattern_and_expr - Genintern.hash_fold_glob_constr_and_expr - (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Evaluable.hash_fold_t)) - (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant)) - Names.hash_fold_lident - (Locus.hash_fold_or_var Ser_int.hash_fold_t) - hash_fold_glob_tactic_expr - Genarg.hash_fold_glevel - st tac -and hash_fold_glob_atomic_tactic_expr st tac = - hash_fold_gen_atomic_tactic_expr - Genintern.hash_fold_glob_constr_and_expr - Genintern.hash_fold_glob_constr_and_expr - Genintern.hash_fold_glob_constr_pattern_and_expr - Genintern.hash_fold_glob_constr_and_expr - (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Evaluable.hash_fold_t)) - (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant)) - Names.hash_fold_lident - (Locus.hash_fold_or_var Ser_int.hash_fold_t) - hash_fold_glob_tactic_expr - Genarg.hash_fold_glevel - st tac - -let hash_glob_tactic_expr = Ppx_hash_lib.Std.Hash.of_fold hash_fold_glob_tactic_expr -let hash_glob_atomic_tactic_expr = Ppx_hash_lib.Std.Hash.of_fold hash_fold_glob_atomic_tactic_expr - -let rec compare_glob_tactic_expr tac = - compare_gen_tactic_expr - Genintern.compare_glob_constr_and_expr - Genintern.compare_glob_constr_and_expr - Genintern.compare_glob_constr_pattern_and_expr - Genintern.compare_glob_constr_and_expr - (Locus.compare_or_var (Genredexpr.compare_and_short_name Evaluable.compare)) - (Locus.compare_or_var (Loc.compare_located compare_ltac_constant)) - Names.compare_lident - (Locus.compare_or_var Ser_int.compare) - compare_glob_tactic_expr - Genarg.compare_glevel - tac -and compare_glob_atomic_tactic_expr tac = - compare_gen_atomic_tactic_expr - Genintern.compare_glob_constr_and_expr - Genintern.compare_glob_constr_and_expr - Genintern.compare_glob_constr_pattern_and_expr - Genintern.compare_glob_constr_and_expr - (Locus.compare_or_var (Genredexpr.compare_and_short_name Evaluable.compare)) - (Locus.compare_or_var (Loc.compare_located compare_ltac_constant)) - Names.compare_lident - (Locus.compare_or_var Ser_int.compare) - compare_glob_tactic_expr - Genarg.compare_glevel - tac - -(* Raw *) -type raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr -type raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr - -let rec raw_tactic_expr_of_sexp tac = - gen_tactic_expr_of_sexp - tac - Constrexpr.constr_expr_of_sexp - Constrexpr.constr_expr_of_sexp - Constrexpr.constr_pattern_expr_of_sexp - Constrexpr.constr_expr_of_sexp - (Constrexpr.or_by_notation_of_sexp Libnames.qualid_of_sexp) - Libnames.qualid_of_sexp - Names.lident_of_sexp - (Locus.or_var_of_sexp Ser_int.t_of_sexp) - raw_tactic_expr_of_sexp - Genarg.rlevel_of_sexp -and raw_atomic_tactic_expr_of_sexp tac = - gen_atomic_tactic_expr_of_sexp - tac - Constrexpr.constr_expr_of_sexp - Constrexpr.constr_expr_of_sexp - Constrexpr.constr_pattern_expr_of_sexp - Constrexpr.constr_expr_of_sexp - (Constrexpr.or_by_notation_of_sexp Libnames.qualid_of_sexp) - Libnames.qualid_of_sexp - Names.lident_of_sexp - (Locus.or_var_of_sexp Ser_int.t_of_sexp) - raw_tactic_expr_of_sexp - Genarg.rlevel_of_sexp - -let rec sexp_of_raw_tactic_expr (tac : raw_tactic_expr) = - sexp_of_gen_tactic_expr - Constrexpr.sexp_of_constr_expr - Constrexpr.sexp_of_constr_expr - Constrexpr.sexp_of_constr_pattern_expr - Constrexpr.sexp_of_constr_expr - (Constrexpr.sexp_of_or_by_notation Libnames.sexp_of_qualid) - Libnames.sexp_of_qualid - Names.sexp_of_lident - (Locus.sexp_of_or_var Ser_int.sexp_of_t) - sexp_of_raw_tactic_expr - Genarg.sexp_of_rlevel - tac -and sexp_of_raw_atomic_tactic_expr tac = - sexp_of_gen_atomic_tactic_expr - Constrexpr.sexp_of_constr_expr - Constrexpr.sexp_of_constr_expr - Constrexpr.sexp_of_constr_pattern_expr - Constrexpr.sexp_of_constr_expr - (Constrexpr.sexp_of_or_by_notation Libnames.sexp_of_qualid) - Libnames.sexp_of_qualid - Names.sexp_of_lident - (Locus.sexp_of_or_var Ser_int.sexp_of_t) - sexp_of_raw_tactic_expr - Genarg.sexp_of_rlevel - tac - -(* Yojson *) -let rec raw_tactic_expr_of_yojson tac = - gen_tactic_expr_of_yojson - tac - Constrexpr.constr_expr_of_yojson - Constrexpr.constr_expr_of_yojson - Constrexpr.constr_pattern_expr_of_yojson - Constrexpr.constr_expr_of_yojson - (Constrexpr.or_by_notation_of_yojson Libnames.qualid_of_yojson) - Libnames.qualid_of_yojson - Names.lident_of_yojson - (Locus.or_var_of_yojson Ser_int.of_yojson) - raw_tactic_expr_of_yojson - Genarg.rlevel_of_yojson -and raw_atomic_tactic_expr_of_yojson tac = - gen_atomic_tactic_expr_of_yojson - tac - Constrexpr.constr_expr_of_yojson - Constrexpr.constr_expr_of_yojson - Constrexpr.constr_pattern_expr_of_yojson - Constrexpr.constr_expr_of_yojson - (Constrexpr.or_by_notation_of_yojson Libnames.qualid_of_yojson) - Libnames.qualid_of_yojson - Names.lident_of_yojson - (Locus.or_var_of_yojson Ser_int.of_yojson) - raw_tactic_expr_of_yojson - Genarg.rlevel_of_yojson - -let rec raw_tactic_expr_to_yojson (tac : raw_tactic_expr) = - gen_tactic_expr_to_yojson - Constrexpr.constr_expr_to_yojson - Constrexpr.constr_expr_to_yojson - Constrexpr.constr_pattern_expr_to_yojson - Constrexpr.constr_expr_to_yojson - (Constrexpr.or_by_notation_to_yojson Libnames.qualid_to_yojson) - Libnames.qualid_to_yojson - Names.lident_to_yojson - (Locus.or_var_to_yojson Ser_int.to_yojson) - raw_tactic_expr_to_yojson - Genarg.rlevel_to_yojson - tac -and raw_atomic_tactic_expr_to_yojson tac = - gen_atomic_tactic_expr_to_yojson - Constrexpr.constr_expr_to_yojson - Constrexpr.constr_expr_to_yojson - Constrexpr.constr_pattern_expr_to_yojson - Constrexpr.constr_expr_to_yojson - (Constrexpr.or_by_notation_to_yojson Libnames.qualid_to_yojson) - Libnames.qualid_to_yojson - Names.lident_to_yojson - (Locus.or_var_to_yojson Ser_int.to_yojson) - raw_tactic_expr_to_yojson - Genarg.rlevel_to_yojson - tac - -let rec hash_fold_raw_tactic_expr st tac = - hash_fold_gen_tactic_expr - Constrexpr.hash_fold_constr_expr - Constrexpr.hash_fold_constr_expr - Constrexpr.hash_fold_constr_pattern_expr - Constrexpr.hash_fold_constr_expr - (Constrexpr.hash_fold_or_by_notation Libnames.hash_fold_qualid) - Libnames.hash_fold_qualid - Names.hash_fold_lident - (Locus.hash_fold_or_var Ser_int.hash_fold_t) - hash_fold_raw_tactic_expr - Genarg.hash_fold_rlevel - st tac -and hash_fold_raw_atomic_tactic_expr st tac = - hash_fold_gen_atomic_tactic_expr - Constrexpr.hash_fold_constr_expr - Constrexpr.hash_fold_constr_expr - Constrexpr.hash_fold_constr_pattern_expr - Constrexpr.hash_fold_constr_expr - (Constrexpr.hash_fold_or_by_notation Libnames.hash_fold_qualid) - Libnames.hash_fold_qualid - Names.hash_fold_lident - (Locus.hash_fold_or_var Ser_int.hash_fold_t) - hash_fold_raw_tactic_expr - Genarg.hash_fold_rlevel - st tac - -let hash_raw_tactic_expr = Ppx_hash_lib.Std.Hash.of_fold hash_fold_raw_tactic_expr -let hash_raw_atomic_tactic_expr = Ppx_hash_lib.Std.Hash.of_fold hash_fold_raw_atomic_tactic_expr - -let rec compare_raw_tactic_expr tac = - compare_gen_tactic_expr - Constrexpr.compare_constr_expr - Constrexpr.compare_constr_expr - Constrexpr.compare_constr_pattern_expr - Constrexpr.compare_constr_expr - (Constrexpr.compare_or_by_notation Libnames.compare_qualid) - Libnames.compare_qualid - Names.compare_lident - (Locus.compare_or_var Ser_int.compare) - compare_raw_tactic_expr - Genarg.compare_rlevel - tac -and compare_raw_atomic_tactic_expr tac = - compare_gen_atomic_tactic_expr - Constrexpr.compare_constr_expr - Constrexpr.compare_constr_expr - Constrexpr.compare_constr_pattern_expr - Constrexpr.compare_constr_expr - (Constrexpr.compare_or_by_notation Libnames.compare_qualid) - Libnames.compare_qualid - Names.compare_lident - (Locus.compare_or_var Ser_int.compare) - compare_raw_tactic_expr - Genarg.compare_rlevel - tac - -(* Atomic *) -type atomic_tactic_expr = Ltac_plugin.Tacexpr.atomic_tactic_expr - -let atomic_tactic_expr_of_sexp tac = - gen_atomic_tactic_expr_of_sexp tac - EConstr.t_of_sexp - Genintern.glob_constr_and_expr_of_sexp - Pattern.constr_pattern_of_sexp - Pattern.constr_pattern_of_sexp - Evaluable.t_of_sexp - (Loc.located_of_sexp ltac_constant_of_sexp) - Names.Id.t_of_sexp - Ser_int.t_of_sexp - unit_of_sexp - Genarg.tlevel_of_sexp - -let sexp_of_atomic_tactic_expr tac = - sexp_of_gen_atomic_tactic_expr - EConstr.sexp_of_t - Genintern.sexp_of_glob_constr_and_expr - Pattern.sexp_of_constr_pattern - Pattern.sexp_of_constr_pattern - Evaluable.sexp_of_t - (Loc.sexp_of_located sexp_of_ltac_constant) - Names.Id.sexp_of_t - Ser_int.sexp_of_t - sexp_of_unit - Genarg.sexp_of_tlevel - tac - -(* Helpers for raw_red_expr *) -type tacdef_body = - [%import: Ltac_plugin.Tacexpr.tacdef_body] - [@@deriving sexp,yojson,hash,compare] - -(* Unsupported serializers *) -type intro_pattern = - [%import: Ltac_plugin.Tacexpr.intro_pattern] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/plugins/ltac/ser_tacexpr.mli b/serlib/plugins/ltac/ser_tacexpr.mli deleted file mode 100644 index 1ec73a81..00000000 --- a/serlib/plugins/ltac/ser_tacexpr.mli +++ /dev/null @@ -1,288 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* direction_flag -val sexp_of_direction_flag : direction_flag -> Sexp.t - -type lazy_flag = Tacexpr.lazy_flag = General | Select | Once -val lazy_flag_of_sexp : Sexp.t -> lazy_flag -val sexp_of_lazy_flag : lazy_flag -> Sexp.t - -type global_flag = Tacexpr.global_flag = TacGlobal | TacLocal -val global_flag_of_sexp : Sexp.t -> global_flag -val sexp_of_global_flag : global_flag -> Sexp.t - -type evars_flag = bool -val evars_flag_of_sexp : Sexp.t -> evars_flag -val sexp_of_evars_flag : evars_flag -> Sexp.t - -type rec_flag = bool -val rec_flag_of_sexp : Sexp.t -> rec_flag -val sexp_of_rec_flag : rec_flag -> Sexp.t - -type advanced_flag = bool -val advanced_flag_of_sexp : Sexp.t -> advanced_flag -val sexp_of_advanced_flag : advanced_flag -> Sexp.t - -type letin_flag = bool -val letin_flag_of_sexp : Sexp.t -> letin_flag -val sexp_of_letin_flag : letin_flag -> Sexp.t - -type clear_flag = bool option -val clear_flag_of_sexp : Sexp.t -> clear_flag -val sexp_of_clear_flag : clear_flag -> Sexp.t - -(* type debug = Tacexpr.debug = Debug | Info | Off *) -(* val debug_of_sexp : Sexp.t -> debug *) -(* val sexp_of_debug : debug -> Sexp.t *) - -(* type goal_selector = Tacexpr.goal_selector *) -(* val goal_selector_of_sexp : Sexp.t -> goal_selector *) -(* val sexp_of_goal_selector : goal_selector -> Sexp.t *) - -type ('c, 'd, 'id) inversion_strength = ('c, 'd, 'id) Tacexpr.inversion_strength - -val inversion_strength_of_sexp : - (Sexp.t -> 'c) -> - (Sexp.t -> 'd) -> - (Sexp.t -> 'id) -> - Sexp.t -> ('c, 'd, 'id) inversion_strength - -val sexp_of_inversion_strength : - ('c -> Sexp.t) -> - ('d -> Sexp.t) -> - ('id -> Sexp.t) -> - ('c, 'd, 'id) inversion_strength -> Sexp.t - -type 'id message_token = 'id Tacexpr.message_token - -val message_token_of_sexp : - (Sexp.t -> 'id) -> Sexp.t -> 'id message_token - -val sexp_of_message_token : - ('id -> Sexp.t) -> 'id message_token -> Sexp.t - -type ('dconstr, 'id) induction_clause = ('dconstr, 'id) Tacexpr.induction_clause - -val induction_clause_of_sexp : - (Sexp.t -> 'dconstr) -> - (Sexp.t -> 'id) -> - Sexp.t -> ('dconstr, 'id) induction_clause - -val sexp_of_induction_clause : - ('dconstr -> Sexp.t) -> - ('id -> Sexp.t) -> - ('dconstr, 'id) induction_clause -> Sexp.t - - -type ('constr, 'dconstr, 'id) induction_clause_list = - ('constr, 'dconstr, 'id) Tacexpr.induction_clause_list - -val induction_clause_list_of_sexp : - (Sexp.t -> 'constr) -> - (Sexp.t -> 'dconstr) -> - (Sexp.t -> 'id) -> - Sexp.t -> ('constr, 'dconstr, 'id) induction_clause_list - -val sexp_of_induction_clause_list : - ('constr -> Sexp.t) -> - ('dconstr -> Sexp.t) -> - ('id -> Sexp.t) -> - ('constr, 'dconstr, 'id) induction_clause_list -> Sexp.t - -type 'a with_bindings_arg = 'a Tacexpr.with_bindings_arg - -val with_bindings_arg_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a with_bindings_arg -val sexp_of_with_bindings_arg : ('a -> Sexp.t) -> 'a with_bindings_arg -> Sexp.t - -(* type multi = Tacexpr.multi *) -(* val multi_of_sexp : Sexp.t -> multi *) -(* val sexp_of_multi : multi -> Sexp.t *) - -type 'a match_pattern = 'a Tacexpr.match_pattern - -val match_pattern_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a match_pattern -val sexp_of_match_pattern : ('a -> Sexp.t) -> 'a match_pattern -> Sexp.t - -type 'a match_context_hyps = 'a Tacexpr.match_context_hyps - -val match_context_hyps_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a match_context_hyps -val sexp_of_match_context_hyps : ('a -> Sexp.t) -> 'a match_context_hyps -> Sexp.t - -type ('a, 't) match_rule = ('a, 't) Tacexpr.match_rule - -val match_rule_of_sexp : - (Sexp.t -> 'a) -> - (Sexp.t -> 't) -> Sexp.t -> ('a, 't) match_rule -val sexp_of_match_rule : - ('a -> Sexp.t) -> - ('t -> Sexp.t) -> ('a, 't) match_rule -> Sexp.t - -type ml_tactic_name = Tacexpr.ml_tactic_name - -val ml_tactic_name_of_sexp : Sexp.t -> ml_tactic_name -val sexp_of_ml_tactic_name : ml_tactic_name -> Sexp.t - -type 'd gen_atomic_tactic_expr = 'd Tacexpr.gen_atomic_tactic_expr - -val sexp_of_gen_atomic_tactic_expr : - ('a -> Sexplib.Sexp.t) -> - ('c -> Sexplib.Sexp.t) -> - ('d -> Sexplib.Sexp.t) -> - ('rp -> Sexplib.Sexp.t) -> - ('e -> Sexplib.Sexp.t) -> - ('f -> Sexplib.Sexp.t) -> - ('g -> Sexplib.Sexp.t) -> - ('occvar -> Sexplib.Sexp.t) -> - ('h -> Sexplib.Sexp.t) -> - ('i -> Sexplib.Sexp.t) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_atomic_tactic_expr -> Sexplib.Sexp.t -val sexp_of_gen_tactic_expr : - ('a -> Sexplib.Sexp.t) -> - ('c -> Sexplib.Sexp.t) -> - ('d -> Sexplib.Sexp.t) -> - ('rp -> Sexplib.Sexp.t) -> - ('e -> Sexplib.Sexp.t) -> - ('f -> Sexplib.Sexp.t) -> - ('g -> Sexplib.Sexp.t) -> - ('occvar -> Sexplib.Sexp.t) -> - ('h -> Sexplib.Sexp.t) -> - ('i -> Sexplib.Sexp.t) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_expr -> Sexplib.Sexp.t -val sexp_of_gen_tactic_arg : - ('a -> Sexplib.Sexp.t) -> - ('c -> Sexplib.Sexp.t) -> - ('d -> Sexplib.Sexp.t) -> - ('rp -> Sexplib.Sexp.t) -> - ('e -> Sexplib.Sexp.t) -> - ('f -> Sexplib.Sexp.t) -> - ('g -> Sexplib.Sexp.t) -> - ('occvar -> Sexplib.Sexp.t) -> - ('h -> Sexplib.Sexp.t) -> - ('i -> Sexplib.Sexp.t) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_arg -> Sexplib.Sexp.t -val sexp_of_gen_fun_ast : - ('a -> Sexplib.Sexp.t) -> - ('c -> Sexplib.Sexp.t) -> - ('d -> Sexplib.Sexp.t) -> - ('rp -> Sexplib.Sexp.t) -> - ('e -> Sexplib.Sexp.t) -> - ('f -> Sexplib.Sexp.t) -> - ('g -> Sexplib.Sexp.t) -> - ('occvar -> Sexplib.Sexp.t) -> - ('h -> Sexplib.Sexp.t) -> - ('i -> Sexplib.Sexp.t) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_fun_ast -> Sexplib.Sexp.t - -val gen_atomic_tactic_expr_of_sexp : - Sexplib.Sexp.t -> - (Sexplib.Sexp.t -> 'a) -> - (Sexplib.Sexp.t -> 'c) -> - (Sexplib.Sexp.t -> 'd) -> - (Sexplib.Sexp.t -> 'rp) -> - (Sexplib.Sexp.t -> 'e) -> - (Sexplib.Sexp.t -> 'f) -> - (Sexplib.Sexp.t -> 'g) -> - (Sexplib.Sexp.t -> 'occvar) -> - (Sexplib.Sexp.t -> 'h) -> - (Sexplib.Sexp.t -> 'i) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_atomic_tactic_expr - -val gen_tactic_expr_of_sexp : - Sexplib.Sexp.t -> - (Sexplib.Sexp.t -> 'a) -> - (Sexplib.Sexp.t -> 'c) -> - (Sexplib.Sexp.t -> 'd) -> - (Sexplib.Sexp.t -> 'rp) -> - (Sexplib.Sexp.t -> 'e) -> - (Sexplib.Sexp.t -> 'f) -> - (Sexplib.Sexp.t -> 'g) -> - (Sexplib.Sexp.t -> 'occvar) -> - (Sexplib.Sexp.t -> 'h) -> - (Sexplib.Sexp.t -> 'i) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_expr - -val gen_tactic_arg_of_sexp : - Sexplib.Sexp.t -> - (Sexplib.Sexp.t -> 'a) -> - (Sexplib.Sexp.t -> 'c) -> - (Sexplib.Sexp.t -> 'd) -> - (Sexplib.Sexp.t -> 'rp) -> - (Sexplib.Sexp.t -> 'e) -> - (Sexplib.Sexp.t -> 'f) -> - (Sexplib.Sexp.t -> 'g) -> - (Sexplib.Sexp.t -> 'occvar) -> - (Sexplib.Sexp.t -> 'h) -> - (Sexplib.Sexp.t -> 'i) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_arg - -val gen_fun_ast_of_sexp : - Sexplib.Sexp.t -> - (Sexplib.Sexp.t -> 'a) -> - (Sexplib.Sexp.t -> 'c) -> - (Sexplib.Sexp.t -> 'd) -> - (Sexplib.Sexp.t -> 'rp) -> - (Sexplib.Sexp.t -> 'e) -> - (Sexplib.Sexp.t -> 'f) -> - (Sexplib.Sexp.t -> 'g) -> - (Sexplib.Sexp.t -> 'occvar) -> - (Sexplib.Sexp.t -> 'h) -> - (Sexplib.Sexp.t -> 'i) -> - < occvar : 'occvar; red_pattern : 'rp; constant : 'e; dterm : 'c; level : 'i; name : 'g; pattern : 'd; - reference : 'f; tacexpr : 'h; term : 'a; > - Tacexpr.gen_tactic_fun_ast - -type glob_tactic_expr = Tacexpr.glob_tactic_expr - [@@deriving sexp,yojson,hash,compare] - -type glob_atomic_tactic_expr = Tacexpr.glob_atomic_tactic_expr - [@@deriving sexp,yojson,hash,compare] - -type raw_tactic_expr = Tacexpr.raw_tactic_expr - [@@deriving sexp,yojson,hash,compare] - -type raw_atomic_tactic_expr = Tacexpr.raw_atomic_tactic_expr - [@@deriving sexp,yojson,hash,compare] - -type atomic_tactic_expr = Tacexpr.atomic_tactic_expr -val atomic_tactic_expr_of_sexp : Sexp.t -> atomic_tactic_expr -val sexp_of_atomic_tactic_expr : atomic_tactic_expr -> Sexp.t - -type tacdef_body = Tacexpr.tacdef_body - [@@deriving sexp,hash,compare] - -type intro_pattern = Tacexpr.intro_pattern - [@@deriving sexp,hash,compare] diff --git a/serlib/plugins/ltac2/dune b/serlib/plugins/ltac2/dune deleted file mode 100644 index 4b21a743..00000000 --- a/serlib/plugins/ltac2/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_ltac2) - (public_name coq-serapi.serlib.ltac2) - (synopsis "Serialization Library for Coq [LTAC2 plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.ltac2 serlib sexplib)) diff --git a/serlib/plugins/ltac2/ser_g_ltac2.ml b/serlib/plugins/ltac2/ser_g_ltac2.ml deleted file mode 100644 index 5498267d..00000000 --- a/serlib/plugins/ltac2/ser_g_ltac2.ml +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -open Serlib -open Ltac2_plugin - -module Tac2expr = Ser_tac2expr - -(* val Ltac2_plugin.G_ltac2.wit_ltac2_entry: - (Ltac2_plugin.Tac2expr.strexpr, unit, unit) Genarg.genarg_type *) -module L2Entry = struct - type t = Tac2expr.strexpr - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2_entry = let module M = Ser_genarg.GSV(L2Entry) in M.genser - -module L2Expr = struct - type t = Tac2expr.raw_tacexpr - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2_expr = let module M = Ser_genarg.GSV(L2Expr) in M.genser - -let register () = - Ser_genarg.register_genser G_ltac2.wit_ltac2_entry ser_wit_ltac2_entry; - Ser_genarg.register_genser G_ltac2.wit_ltac2_expr ser_wit_ltac2_expr; - () - -let () = register () diff --git a/serlib/plugins/ltac2/ser_tac2env.ml b/serlib/plugins/ltac2/ser_tac2env.ml deleted file mode 100644 index c5d5dd0c..00000000 --- a/serlib/plugins/ltac2/ser_tac2env.ml +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -open Serlib -open Ltac2_plugin - -open Sexplib.Std -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin - -module Util = Ser_util -module Loc = Ser_loc -module CAst = Ser_cAst -module Names = Ser_names -module Tac2expr = Ser_tac2expr - -module WL2in1 = struct - type raw = Tac2expr.uid CAst.t list * Tac2expr.raw_tacexpr - [@@deriving sexp,hash,compare] - type glb = Tac2expr.uid list * Tac2expr.glb_tacexpr - [@@deriving sexp,hash,compare] - type top = Util.Empty.t - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2in1 = let module M = Ser_genarg.GS(WL2in1) in M.genser - -module WL2in1V = struct - type raw = Tac2expr.uid CAst.t list * Tac2expr.raw_tacexpr - [@@deriving sexp,hash,compare] - type glb = Tac2expr.glb_tacexpr - [@@deriving sexp,hash,compare] - type top = Util.Empty.t - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2in1_val = let module M = Ser_genarg.GS(WL2in1V) in M.genser - -module WLC2 = struct - type raw = Tac2expr.raw_tacexpr - [@@deriving sexp,hash,compare] - type glb = Names.Id.Set.t * Tac2expr.glb_tacexpr - [@@deriving sexp,hash,compare] - type top = Util.Empty.t - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2_constr = let module M = Ser_genarg.GS(WLC2) in M.genser - -type var_quotation_kind = - [%import: Ltac2_plugin.Tac2env.var_quotation_kind] - [@@deriving sexp,yojson,hash,compare] - -module WLQ2 = struct - type raw = Names.lident option * Names.lident - [@@deriving sexp,hash,compare] - type glb = var_quotation_kind * Names.Id.t - [@@deriving sexp,hash,compare] - type top = Util.Empty.t - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2_var_quotation = let module M = Ser_genarg.GS(WLQ2) in M.genser - -module WLV2 = struct - type raw = Util.Empty.t - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = Util.Empty.t - [@@deriving sexp,hash,compare] -end - -let ser_wit_ltac2_val = let module M = Ser_genarg.GS(WLV2) in M.genser - -let register () = - Ser_genarg.register_genser Tac2env.wit_ltac2in1 ser_wit_ltac2in1; - Ser_genarg.register_genser Tac2env.wit_ltac2in1_val ser_wit_ltac2in1_val; - Ser_genarg.register_genser Tac2env.wit_ltac2_constr ser_wit_ltac2_constr; - Ser_genarg.register_genser Tac2env.wit_ltac2_var_quotation ser_wit_ltac2_var_quotation; - Ser_genarg.register_genser Tac2env.wit_ltac2_val ser_wit_ltac2_val; - () - -let () = register () diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml deleted file mode 100644 index 65eb5a41..00000000 --- a/serlib/plugins/ltac2/ser_tac2expr.ml +++ /dev/null @@ -1,202 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -open Serlib - -module Loc = Ser_loc -module CAst = Ser_cAst -module Names = Ser_names -module Libnames = Ser_libnames - -open Sexplib.Std -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin - -let hash_fold_array = hash_fold_array_frozen - -type mutable_flag = - [%import: Ltac2_plugin.Tac2expr.mutable_flag] - [@@deriving sexp,yojson,hash,compare] - -type uid = - [%import: Ltac2_plugin.Tac2expr.uid] - [@@deriving sexp,yojson,hash,compare] - -type lid = - [%import: Ltac2_plugin.Tac2expr.lid] - [@@deriving sexp,yojson,hash,compare] - -type rec_flag = - [%import: Ltac2_plugin.Tac2expr.rec_flag] - [@@deriving sexp,yojson,hash,compare] - -type redef_flag = - [%import: Ltac2_plugin.Tac2expr.redef_flag] - [@@deriving sexp,yojson,hash,compare] - -type 'a or_relid = - [%import: 'a Ltac2_plugin.Tac2expr.or_relid] - [@@deriving sexp,yojson,hash,compare] - -type 'a or_tuple = - [%import: 'a Ltac2_plugin.Tac2expr.or_tuple] - [@@deriving sexp,yojson,hash,compare] - -type type_constant = - [%import: Ltac2_plugin.Tac2expr.type_constant] - [@@deriving sexp,yojson,hash,compare] - -type raw_typexpr_r = - [%import: Ltac2_plugin.Tac2expr.raw_typexpr_r] - [@@deriving sexp,yojson,hash,compare] -and raw_typexpr = - [%import: Ltac2_plugin.Tac2expr.raw_typexpr] - [@@deriving sexp,yojson,hash,compare] - -type raw_typedef = - [%import: Ltac2_plugin.Tac2expr.raw_typedef] - [@@deriving sexp,yojson,hash,compare] - -type raw_quant_typedef = - [%import: Ltac2_plugin.Tac2expr.raw_quant_typedef] - [@@deriving sexp,yojson,hash,compare] - -type 'a glb_typexpr = - [%import: 'a Ltac2_plugin.Tac2expr.glb_typexpr] - [@@deriving sexp,yojson,hash,compare] - -type atom = - [%import: Ltac2_plugin.Tac2expr.atom] - [@@deriving sexp,yojson,hash,compare] - -type ltac_constant = - [%import: Ltac2_plugin.Tac2expr.ltac_constant] - [@@deriving sexp,yojson,hash,compare] - -type ltac_alias = - [%import: Ltac2_plugin.Tac2expr.ltac_alias] - [@@deriving sexp,yojson,hash,compare] - -type ltac_constructor = - [%import: Ltac2_plugin.Tac2expr.ltac_constructor] - [@@deriving sexp,yojson,hash,compare] - -type ltac_projection = - [%import: Ltac2_plugin.Tac2expr.ltac_projection] - [@@deriving sexp,yojson,hash,compare] - -type raw_patexpr = - [%import: Ltac2_plugin.Tac2expr.raw_patexpr] - [@@deriving sexp,yojson,hash,compare] -and raw_patexpr_r = - [%import: Ltac2_plugin.Tac2expr.raw_patexpr_r] - [@@deriving sexp,yojson,hash,compare] - -type tacref = - [%import: Ltac2_plugin.Tac2expr.tacref] - [@@deriving sexp,yojson,hash,compare] - -type ml_tactic_name = - [%import: Ltac2_plugin.Tac2expr.ml_tactic_name] - [@@deriving sexp,yojson,hash,compare] - -type sexpr = - [%import: Ltac2_plugin.Tac2expr.sexpr] - [@@deriving sexp,yojson,hash,compare] - -type ctor_indx = - [%import: Ltac2_plugin.Tac2expr.ctor_indx] - [@@deriving sexp,yojson,hash,compare] - -type ctor_data_for_patterns = - [%import: Ltac2_plugin.Tac2expr.ctor_data_for_patterns] - [@@deriving sexp,yojson,hash,compare] - -type glb_pat = - [%import: Ltac2_plugin.Tac2expr.glb_pat] - [@@deriving sexp,yojson,hash,compare] - -type case_info = - [%import: Ltac2_plugin.Tac2expr.case_info] - [@@deriving sexp,yojson,hash,compare] - -type 'a open_match = - [%import: 'a Ltac2_plugin.Tac2expr.open_match] - [@@deriving sexp,yojson,hash,compare] - -module ObjS = struct type t = Obj.t let name = "Obj.t" end -module Obj = SerType.Opaque(ObjS) - -module GT2ESpec = struct - type t = Ltac2_plugin.Tac2expr.glb_tacexpr - open Ltac2_plugin.Tac2expr - type _t = - | GTacAtm of atom - | GTacVar of Names.Id.t - | GTacRef of ltac_constant - | GTacFun of Names.Name.t list * _t - | GTacApp of _t * _t list - | GTacLet of rec_flag * (Names.Name.t * _t) list * _t - | GTacCst of case_info * int * _t list - | GTacCse of _t * case_info * _t array * (Names.Name.t array * _t) array - | GTacPrj of type_constant * _t * int - | GTacSet of type_constant * _t * int * _t - | GTacOpn of ltac_constructor * _t list - | GTacWth of _t open_match - | GTacFullMatch of _t * (glb_pat * _t) list - | GTacExt of int * Obj.t - | GTacPrm of ml_tactic_name - [@@deriving sexp,yojson,hash,compare] - -end - -module GT2E = Serlib.SerType.Pierce(GT2ESpec) -type glb_tacexpr = GT2E.t - [@@deriving sexp,yojson,hash,compare] - -module T2ESpec = struct - type t = Ltac2_plugin.Tac2expr.raw_tacexpr_r - open Ltac2_plugin.Tac2expr - type _t = - | CTacAtm of atom - | CTacRef of tacref or_relid - | CTacCst of ltac_constructor or_tuple or_relid - | CTacFun of raw_patexpr list * raw_tacexpr - | CTacApp of raw_tacexpr * raw_tacexpr list - | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t - | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * Names.KerName.t - | CTacCnv of raw_tacexpr * raw_typexpr - | CTacSeq of raw_tacexpr * raw_tacexpr - | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr - | CTacCse of raw_tacexpr * raw_taccase list - | CTacRec of raw_tacexpr option * raw_recexpr - | CTacPrj of raw_tacexpr * ltac_projection or_relid - | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr - | CTacExt of int * Obj.t - | CTacGlb of int * (Names.lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr - - and raw_tacexpr = _t CAst.t - and raw_taccase = - [%import: Ltac2_plugin.Tac2expr.raw_taccase] - and raw_recexpr = - [%import: Ltac2_plugin.Tac2expr.raw_recexpr] - [@@deriving sexp,yojson,hash,compare] - -end - -module T2E = Serlib.SerType.Pierce(T2ESpec) -type raw_tacexpr_r = T2E.t - [@@deriving sexp,yojson,hash,compare] - -type raw_tacexpr = - [%import: Ltac2_plugin.Tac2expr.raw_tacexpr] - [@@deriving sexp,yojson,hash,compare] - -type strexpr = - [%import: Ltac2_plugin.Tac2expr.strexpr] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/plugins/ltac2/ser_tac2quote.ml b/serlib/plugins/ltac2/ser_tac2quote.ml deleted file mode 100644 index 39008770..00000000 --- a/serlib/plugins/ltac2/ser_tac2quote.ml +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -(* open Sexplib.Std *) -(* open Ppx_hash_lib.Std.Hash.Builtin *) -(* open Ppx_compare_lib.Builtin *) - -(* let b x = Obj.magic x *) - -(* These are all special ltac2 extensible objects, brrrr... *) -let register () = - (* Ser_genarg.register_genser Tac2quote.wit_constr (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_ident (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_ltac1 (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_ltac1val (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_open_constr (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_pattern (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_preterm (b()); *) - (* Ser_genarg.register_genser Tac2quote.wit_reference (b()); *) - () - -let () = register () diff --git a/serlib/plugins/micromega/dune b/serlib/plugins/micromega/dune deleted file mode 100644 index 61adb236..00000000 --- a/serlib/plugins/micromega/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_micromega) - (public_name coq-serapi.serlib.micromega) - (synopsis "Serialization Library for Coq Congruence Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.micromega serlib sexplib)) diff --git a/serlib/plugins/micromega_core/dune b/serlib/plugins/micromega_core/dune deleted file mode 100644 index deae7af9..00000000 --- a/serlib/plugins/micromega_core/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_micromega_core) - (public_name coq-serapi.serlib.micromega_core) - (synopsis "Serialization Library for Coq Micromega_core Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.micromega_core serlib sexplib)) diff --git a/serlib/plugins/ring/dune b/serlib/plugins/ring/dune deleted file mode 100644 index 9d053960..00000000 --- a/serlib/plugins/ring/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_ring) - (public_name coq-serapi.serlib.ring) - (synopsis "Serialization Library for Coq Setoid Newring Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) - (libraries coq-core.plugins.ring serlib serlib_ltac sexplib)) diff --git a/serlib/plugins/ring/ser_g_ring.ml b/serlib/plugins/ring/ser_g_ring.ml deleted file mode 100644 index 28f18c29..00000000 --- a/serlib/plugins/ring/ser_g_ring.ml +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* SerAPI: Coq interaction protocol with bidirectional serialization *) -(************************************************************************) -(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) -(* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) -(* Written by: Emilio J. Gallego Arias and others *) -(************************************************************************) - -open Sexplib.Conv -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin -open Serlib - -module CAst = Ser_cAst -module Libnames = Ser_libnames -module Constrexpr = Ser_constrexpr -module Tactypes = Ser_tactypes -module Genintern = Ser_genintern -module EConstr = Ser_eConstr -module Tacexpr = Serlib_ltac.Ser_tacexpr - -module Ltac_plugin = struct - module Tacexpr = Serlib_ltac.Ser_tacexpr -end - -type 'constr coeff_spec = - [%import: 'constr Ring_plugin.Ring_ast.coeff_spec] - [@@deriving sexp,hash,compare] - -type cst_tac_spec = - [%import: Ring_plugin.Ring_ast.cst_tac_spec] - [@@deriving sexp,hash,compare] - -type 'constr ring_mod = - [%import: 'constr Ring_plugin.Ring_ast.ring_mod] - [@@deriving sexp,hash,compare] - -type 'a field_mod = - [%import: 'a Ring_plugin.Ring_ast.field_mod] - [@@deriving sexp,hash,compare] - -module A0 = struct - type t = Constrexpr.constr_expr field_mod - [@@deriving sexp,hash,compare] -end - -let ser_wit_field_mod = let module M = Ser_genarg.GSV(A0) in M.genser - -module A1 = struct - type t = Constrexpr.constr_expr field_mod list - [@@deriving sexp,hash,compare] -end - -let ser_wit_field_mods = let module M = Ser_genarg.GSV(A1) in M.genser - -module A2 = struct - type t = Constrexpr.constr_expr ring_mod - [@@deriving sexp,hash,compare] -end - -let ser_wit_ring_mod = let module M = Ser_genarg.GSV(A2) in M.genser - -module A3 = struct - type t = Constrexpr.constr_expr ring_mod list - [@@deriving sexp,hash,compare] -end - -let ser_wit_ring_mods = let module M = Ser_genarg.GSV(A3) in M.genser - -let register () = - Ser_genarg.register_genser Ring_plugin.G_ring.wit_field_mod ser_wit_field_mod; - Ser_genarg.register_genser Ring_plugin.G_ring.wit_field_mods ser_wit_field_mods; - Ser_genarg.register_genser Ring_plugin.G_ring.wit_ring_mod ser_wit_ring_mod; - Ser_genarg.register_genser Ring_plugin.G_ring.wit_ring_mods ser_wit_ring_mods; - () - -let _ = register () diff --git a/serlib/plugins/ssr/dune b/serlib/plugins/ssr/dune deleted file mode 100644 index 2ba2ecf8..00000000 --- a/serlib/plugins/ssr/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name serlib_ssr) - (public_name coq-serapi.serlib.ssreflect) - (synopsis "Serialization Library for Coq [SSR plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.ssreflect serlib serlib_ltac serlib_ssrmatching sexplib)) diff --git a/serlib/plugins/ssr/ser_ssrast.ml b/serlib/plugins/ssr/ser_ssrast.ml deleted file mode 100644 index 794c354b..00000000 --- a/serlib/plugins/ssr/ser_ssrast.ml +++ /dev/null @@ -1,221 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* t - val of_t : t -> _t - -end - -module Biject(M : Bijectable) : SJHC with type t = M.t = struct - - type t = M.t - - let sexp_of_t x = M.sexp_of__t (M.of_t x) - let t_of_sexp s = M.to_t (M._t_of_sexp s) - - let to_yojson p = M._t_to_yojson (M.of_t p) - let of_yojson p = M._t_of_yojson p |> Result.map M.to_t - - let hash x = M.hash__t (M.of_t x) - let hash_fold_t st x = M.hash_fold__t st (M.of_t x) - - let compare x1 x2 = M.compare__t (M.of_t x1) (M.of_t x2) -end - -(* Bijection with serializable types *) -module type Bijectable1 = sig - - (* Base Type *) - type 'a t - - (* Representation type *) - type 'a _t [@@deriving sexp,yojson,hash,compare] - - (* Need to be bijetive *) - val to_t : 'a _t -> 'a t - val of_t : 'a t -> 'a _t - -end - -module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t = struct - - type 'a t = 'a M.t - - let sexp_of_t f x = M.sexp_of__t f (M.of_t x) - let t_of_sexp f s = M.to_t (M._t_of_sexp f s) - - let to_yojson f p = M._t_to_yojson f (M.of_t p) - let of_yojson f p = M._t_of_yojson f p |> Result.map M.to_t - - let hash_fold_t f st x = M.hash_fold__t f st (M.of_t x) - - let compare f x1 x2 = M.compare__t f (M.of_t x1) (M.of_t x2) -end - -(* We do our own alias as to have better control *) -let _sercast = Obj.magic - -(* Obj.magic piercing *) -module type Pierceable = sig - - (* Type to pierce *) - type t - - (* Representation type *) - type _t [@@deriving sexp,yojson,hash,compare] -end - -module type Pierceable1 = sig - - (* Type to pierce *) - type 'a t - - (* Representation type *) - type 'a _t [@@deriving sexp,yojson,hash,compare] -end - -module Pierce(M : Pierceable) : SJHC with type t = M.t = struct - - type t = M.t - - let sexp_of_t x = M.sexp_of__t (_sercast x) - let t_of_sexp s = _sercast (M._t_of_sexp s) - - let to_yojson p = M._t_to_yojson (_sercast p) - let of_yojson p = M._t_of_yojson p |> Result.map _sercast - - let hash x = M.hash__t (_sercast x) - let hash_fold_t st x = M.hash_fold__t st (_sercast x) - - let compare x1 x2 = M.compare__t (_sercast x1) (_sercast x2) - -end - -module Pierce1(M : Pierceable1) : SJHC1 with type 'a t = 'a M.t = struct - - type 'a t = 'a M.t - - let sexp_of_t f x = M.sexp_of__t f (_sercast x) - let t_of_sexp f s = _sercast (M._t_of_sexp f s) - - let to_yojson f p = M._t_to_yojson f (_sercast p) - let of_yojson f p = M._t_of_yojson f p |> Result.map _sercast - - (* let hash x = M.hash__t (_sercast x) *) - let hash_fold_t f st x = M.hash_fold__t f st (_sercast x) - - let compare f x1 x2 = M.compare__t f (_sercast x1) (_sercast x2) - -end - -(* Unfortunately this doesn't really work for types that are named as - the functions would have to be sexp_of_name etc... Maybe fixme in - the future *) -module PierceAlt(M : Pierceable) : SJHC with type t := M.t = struct - - let sexp_of_t x = M.sexp_of__t (_sercast x) - let t_of_sexp s = _sercast (M._t_of_sexp s) - - let to_yojson p = M._t_to_yojson (_sercast p) - let of_yojson p = M._t_of_yojson p |> Result.map _sercast - - let hash x = M.hash__t (_sercast x) - let hash_fold_t st x = M.hash_fold__t st (_sercast x) - - let compare x1 x2 = M.compare__t (_sercast x1) (_sercast x2) - -end - -module type OpaqueDesc = sig type t val name : string end - -module Opaque(M : OpaqueDesc) : SJHC with type t = M.t = struct - - type t = M.t - let typ = M.name - - let sexp_of_t x = Serlib_base.sexp_of_opaque ~typ x - let t_of_sexp s = Serlib_base.opaque_of_sexp ~typ s - - let to_yojson p = Serlib_base.opaque_to_yojson ~typ p - let of_yojson p = Serlib_base.opaque_of_yojson ~typ p - - let hash x = Serlib_base.hash_opaque ~typ x - let hash_fold_t st x = Serlib_base.hash_fold_opaque ~typ st x - - let compare x1 x2 = Serlib_base.compare_opaque ~typ x1 x2 - -end - -module type OpaqueDesc1 = sig type 'a t val name : string end - -module Opaque1(M : OpaqueDesc1) : SJHC1 with type 'a t = 'a M.t = struct - - type 'a t = 'a M.t - let typ = M.name - - let sexp_of_t _ x = Serlib_base.sexp_of_opaque ~typ x - let t_of_sexp _ s = Serlib_base.opaque_of_sexp ~typ s - - let to_yojson _ p = Serlib_base.opaque_to_yojson ~typ p - let of_yojson _ p = Serlib_base.opaque_of_yojson ~typ p - - let hash_fold_t _ st x = Serlib_base.hash_fold_opaque ~typ st x - - let compare _ x1 x2 = Serlib_base.compare_opaque ~typ x1 x2 - -end diff --git a/serlib/serType.mli b/serlib/serType.mli deleted file mode 100644 index 5adb4980..00000000 --- a/serlib/serType.mli +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* t - val of_t : t -> _t - -end - -module Biject(M : Bijectable) : SJHC with type t = M.t - -(* Bijection with serializable types *) -module type Bijectable1 = sig - - (* Base Type *) - type 'a t - - (* Representation type *) - type 'a _t [@@deriving sexp,yojson,hash,compare] - - (* Need to be bijetive *) - val to_t : 'a _t -> 'a t - val of_t : 'a t -> 'a _t - -end - -module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t - -module type Pierceable = sig - - (** Type to pierce *) - type t - - (** Representation type *) - type _t [@@deriving sexp,yojson,hash,compare] - -end - -module type Pierceable1 = sig - - (** Type to pierce *) - type 'a t - - (** Representation type *) - type 'a _t [@@deriving sexp,yojson,hash,compare] -end - -module Pierce(M : Pierceable) : SJHC with type t = M.t -module Pierce1(M : Pierceable1) : SJHC1 with type 'a t = 'a M.t - -module type OpaqueDesc = sig type t val name : string end -module Opaque(M : OpaqueDesc) : SJHC with type t = M.t - -module type OpaqueDesc1 = sig type 'a t val name : string end -module Opaque1(M : OpaqueDesc1) : SJHC1 with type 'a t = 'a M.t diff --git a/serlib/ser_attributes.ml b/serlib/ser_attributes.ml deleted file mode 100644 index 538f19de..00000000 --- a/serlib/ser_attributes.ml +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= fun { L.v; loc } -> CAst.make ?loc:loc v) -let to_yojson f { CAst.v ; loc } = L.to_yojson f { L.v ; loc } - -let hash_fold_t f st { CAst.v; loc } = L.hash_fold_t f st { L.v; loc } - -let compare f { CAst.v = v1; loc = l1 } { CAst.v = v2; loc = l2 } = L.compare f { L.v = v1; loc = l1 } { L.v = v2; loc = l2 } - -let omit_att = ref false - -let sexp_of_t f x = - if !omit_att then f x.CAst.v else sexp_of_t f x - -(* let to_yojson f x = - if !omit_att then ... *) - diff --git a/serlib/ser_cAst.mli b/serlib/ser_cAst.mli deleted file mode 100644 index 60ea445a..00000000 --- a/serlib/ser_cAst.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* M.add k s e) M.empty l - let of_t = M.bindings - end - - include SerType.Biject1(BijectSpec) - -end diff --git a/serlib/ser_cMap.mli b/serlib/ser_cMap.mli deleted file mode 100644 index 7f7bd948..00000000 --- a/serlib/ser_cMap.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* NoInvert - | CaseInvert { indices } -> - CaseInvert { indices = Array.map f indices } - -type ('constr, 'r) pcase_branch = - [%import: ('constr, 'r) Constr.pcase_branch] - [@@deriving sexp,yojson,hash,compare] - -let map_pcase_branch f (bi, c) = (bi, f c) - -type ('types, 'r) pcase_return = - [%import: ('types, 'r) Constr.pcase_return] - [@@deriving sexp,yojson,hash,compare] - -let map_pcase_return f (bi, c) = (bi, f c) - -type _constr = - | Rel of int - | Var of Names.Id.t - | Meta of int - | Evar of _constr pexistential - | Sort of Sorts.t - | Cast of _constr * cast_kind * _constr - | Prod of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr - | Lambda of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr - | LetIn of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr * _constr - | App of _constr * _constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor - | Case of case_info * UVars.Instance.t * _constr array * (_constr, Sorts.relevance) pcase_return * _constr pcase_invert * _constr * (_constr, Sorts.relevance) pcase_branch array - | Fix of (_constr, _constr, Sorts.relevance) pfixpoint - | CoFix of (_constr, _constr, Sorts.relevance) pcofixpoint - | Proj of Names.Projection.t * Sorts.relevance * _constr - | Int of Uint63.t - | Float of Float64.t - | Array of UVars.Instance.t * _constr array * _constr * _constr -[@@deriving sexp,yojson,hash,compare] - -let rec _constr_put (c : Constr.t) : _constr = - let cr = _constr_put in - let crl = SList.map _constr_put in - let cra = Array.map _constr_put in - let crci = map_pcase_invert _constr_put in - let crcb = map_pcase_branch _constr_put in - let crcr = map_pcase_return _constr_put in - let module C = Constr in - match C.kind c with - | C.Rel i -> Rel(i) - | C.Var v -> Var(v) - | C.Meta(mv) -> Meta mv - | C.Evar(ek, csa) -> Evar (ek, crl csa) - | C.Sort(st) -> Sort (st) - | C.Cast(cs,k,ty) -> Cast(cr cs, k, cr ty) - | C.Prod(n,tya,tyr) -> Prod(n, cr tya, cr tyr) - | C.Lambda(n,ab,bd) -> Lambda(n, cr ab, cr bd) - | C.LetIn(n,u,ab,bd) -> LetIn(n, cr u, cr ab, cr bd) - | C.App(hd, al) -> App(cr hd, cra al) - | C.Const p -> Const p - | C.Ind(p,q) -> Ind (p,q) - | C.Construct(p) -> Construct (p) - | C.Case(ci, u, ca, (pr,r), pi, c, pb) -> - Case(ci, u, cra ca, (crcr pr,r), crci pi, cr c, Array.map crcb pb) - (* (int array * int) * (Name.t array * 'types array * 'constr array)) *) - | C.Fix(p,(na,u1,u2)) -> Fix(p, (na, cra u1, cra u2)) - | C.CoFix(p,(na,u1,u2)) -> CoFix(p, (na, cra u1, cra u2)) - | C.Proj(p,r,c) -> Proj(p, r, cr c) - | C.Int i -> Int i - | C.Float i -> Float i - | C.Array (u,a,e,t) -> Array(u, cra a, cr e, cr t) - -let rec _constr_get (c : _constr) : Constr.t = - let cr = _constr_get in - let crl = SList.map _constr_get in - let cra = Array.map _constr_get in - let crci = map_pcase_invert _constr_get in - let crcb = map_pcase_branch _constr_get in - let crcr = map_pcase_return _constr_get in - let module C = Constr in - match c with - | Rel i -> C.mkRel i - | Var v -> C.mkVar v - | Meta(mv) -> C.mkMeta mv - | Evar(ek, csa) -> C.mkEvar (ek, crl csa) - | Sort(st) -> C.mkSort (st) - | Cast(cs,k,ty) -> C.mkCast(cr cs, k, cr ty) - | Prod(n,tya,tyr) -> C.mkProd(n, cr tya, cr tyr) - | Lambda(n,ab,bd) -> C.mkLambda(n, cr ab, cr bd) - | LetIn(n,u,ab,bd) -> C.mkLetIn(n, cr u, cr ab, cr bd) - | App(hd, al) -> C.mkApp(cr hd, cra al) - | Const p -> C.mkConstU(p) - | Ind(p,q) -> C.mkIndU(p, q) - | Construct(p) -> C.mkConstructU(p) - | Case(ci, u, ca, (pr,r), pi, c, pb) -> C.mkCase (ci, u, cra ca, (crcr pr,r), crci pi, cr c, Array.map crcb pb) - | Fix (p,(na,u1,u2)) -> C.mkFix(p, (na, cra u1, cra u2)) - | CoFix(p,(na,u1,u2)) -> C.mkCoFix(p, (na, cra u1, cra u2)) - | Proj(p,r,c) -> C.mkProj(p, r, cr c) - | Int i -> C.mkInt i - | Float f -> C.mkFloat f - | Array (u,a,e,t) -> C.mkArray(u, cra a, cr e, cr t) - -module ConstrBij = struct - - type t = Constr.t - - type _t = _constr - [@@deriving sexp,yojson,hash,compare] - - let to_t = _constr_get - let of_t = _constr_put - -end - -module CC = SerType.Biject(ConstrBij) -type constr = CC.t - [@@deriving sexp,yojson,hash,compare] -type types = CC.t - [@@deriving sexp,yojson,hash,compare] - -type t = constr - [@@deriving sexp,yojson,hash,compare] - -type case_invert = - [%import: Constr.case_invert] - [@@deriving sexp,yojson] - -type rec_declaration = - [%import: Constr.rec_declaration] - [@@deriving sexp] - -type fixpoint = - [%import: Constr.fixpoint] - [@@deriving sexp] - -type cofixpoint = - [%import: Constr.cofixpoint] - [@@deriving sexp] - -type existential = - [%import: Constr.existential] - [@@deriving sexp] - -type sorts_family = Sorts.family -let sorts_family_of_sexp = Sorts.family_of_sexp -let sexp_of_sorts_family = Sorts.sexp_of_family - -type named_declaration = - [%import: Constr.named_declaration] - [@@deriving sexp,yojson,hash,compare] - -type named_context = - [%import: Constr.named_context] - [@@deriving sexp,yojson,hash,compare] - -type rel_declaration = - [%import: Constr.rel_declaration] - [@@deriving sexp,yojson,hash,compare] - -type rel_context = - [%import: Constr.rel_context] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_constr.mli b/serlib/ser_constr.mli deleted file mode 100644 index 82811d13..00000000 --- a/serlib/ser_constr.mli +++ /dev/null @@ -1,132 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* metavariable -val sexp_of_metavariable : metavariable -> Sexp.t - -type pconstant = Constr.pconstant - -val pconstant_of_sexp : Sexp.t -> pconstant -val sexp_of_pconstant : pconstant -> Sexp.t - -type pinductive = Constr.pinductive - -val pinductive_of_sexp : Sexp.t -> pinductive -val sexp_of_pinductive : pinductive -> Sexp.t - -type pconstructor = Constr.pconstructor - -val pconstructor_of_sexp : Sexp.t -> pconstructor -val sexp_of_pconstructor : pconstructor -> Sexp.t - -type cast_kind = Constr.cast_kind [@@deriving sexp, yojson, hash,compare] -type case_style = Constr.case_style [@@deriving sexp, yojson, hash,compare] - -type case_printing = Constr.case_printing - -val case_printing_of_sexp : Sexp.t -> case_printing -val sexp_of_case_printing : case_printing -> Sexp.t - -type case_info = Constr.case_info - -val case_info_of_sexp : Sexp.t -> case_info -val sexp_of_case_info : case_info -> Sexp.t - -type rec_declaration = Constr.rec_declaration - -val rec_declaration_of_sexp : Sexp.t -> rec_declaration -val sexp_of_rec_declaration : rec_declaration -> Sexp.t - -type fixpoint = Constr.fixpoint - -val fixpoint_of_sexp : Sexp.t -> fixpoint -val sexp_of_fixpoint : fixpoint -> Sexp.t - -type cofixpoint = Constr.cofixpoint - -val cofixpoint_of_sexp : Sexp.t -> cofixpoint -val sexp_of_cofixpoint : cofixpoint -> Sexp.t - -type 'constr pexistential = 'constr Constr.pexistential - [@@deriving sexp, yojson, hash, compare] - -type ('constr, 'types, 'r) prec_declaration = ('constr, 'types, 'r) Constr.prec_declaration - -val prec_declaration_of_sexp : - (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) -> - Sexp.t -> ('constr, 'types, 'r) prec_declaration -val sexp_of_prec_declaration : - ('constr -> Sexp.t) -> ('types -> Sexp.t) -> ('r -> Sexp.t) -> - ('constr, 'types, 'r) prec_declaration -> Sexp.t - -type ('constr, 'types, 'r) pfixpoint = ('constr, 'types, 'r) Constr.pfixpoint - -val pfixpoint_of_sexp : - (Sexp.t -> 'constr) -> - (Sexp.t -> 'types) -> - (Sexp.t -> 'r) -> Sexp.t -> ('constr, 'types, 'r) pfixpoint - -val sexp_of_pfixpoint : - ('constr -> Sexp.t) -> - ('types -> Sexp.t) -> - ('r -> Sexp.t) -> ('constr, 'types, 'r) pfixpoint -> Sexp.t - -type ('constr, 'types, 'r) pcofixpoint = ('constr, 'types, 'r) Constr.pcofixpoint - -val pcofixpoint_of_sexp : - (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) -> - Sexp.t -> ('constr, 'types, 'r) pcofixpoint - -val sexp_of_pcofixpoint : - ('constr -> Sexp.t) -> ('types -> Sexp.t) -> ('r -> Sexp.t) -> - ('constr, 'types, 'r) pcofixpoint -> Sexp.t - -type t = Constr.t - [@@deriving sexp,yojson,hash,compare] - -type constr = t - [@@deriving sexp,yojson,hash,compare] - -type types = constr - [@@deriving sexp,yojson,hash,compare] - -type existential = Constr.existential -val existential_of_sexp : Sexp.t -> existential -val sexp_of_existential : existential -> Sexp.t - -type sorts_family = Sorts.family -val sorts_family_of_sexp : Sexp.t -> sorts_family -val sexp_of_sorts_family : sorts_family -> Sexp.t - -type named_declaration = Constr.named_declaration -val named_declaration_of_sexp : Sexp.t -> named_declaration -val sexp_of_named_declaration : named_declaration -> Sexp.t - -type named_context = Constr.named_context - [@@deriving sexp,yojson,hash,compare] - -type rel_declaration = Constr.rel_declaration -val rel_declaration_of_sexp : Sexp.t -> rel_declaration -val sexp_of_rel_declaration : rel_declaration -> Sexp.t - -type rel_context = Constr.rel_context - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_constr_matching.ml b/serlib/ser_constr_matching.ml deleted file mode 100644 index b5b4771a..00000000 --- a/serlib/ser_constr_matching.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* binding_bound_vars -val sexp_of_binding_bound_vars : binding_bound_vars -> Sexp.t diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml deleted file mode 100644 index 9a30b09f..00000000 --- a/serlib/ser_constrexpr.ml +++ /dev/null @@ -1,194 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 'c) -> (Sexp.t -> 't) -> (Sexp.t -> 'r) -> Sexp.t -> ('c, 't, 'r) pt - val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('r -> Sexp.t) -> ('c, 't, 'r) pt -> Sexp.t - - end - - type ('c, 't, 'r) pt = ('c, 't, 'r) Context.Compacted.pt - val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> (Sexp.t -> 'r) -> Sexp.t -> ('c, 't, 'r) pt - val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('r -> Sexp.t) -> ('c, 't, 'r) pt -> Sexp.t - -end diff --git a/serlib/ser_conv_oracle.ml b/serlib/ser_conv_oracle.ml deleted file mode 100644 index 113b1670..00000000 --- a/serlib/ser_conv_oracle.ml +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t) -> (b -> Sexp.t) -> (a,b) thunk -> Sexp.t = - fun f _ t -> match t with - | Value v -> f v - | Thunk t -> f (Lazy.force t) - -let thunk_of_sexp : type a b. (Sexp.t -> a) -> (Sexp.t -> b) -> Sexp.t -> (a,b) thunk = - fun f _ s -> Value (f s) - -let thunk_of_yojson : type a b. (Yojson.Safe.t -> (a, string) Result.t) -> (Yojson.Safe.t -> (b, string) Result.t) -> Yojson.Safe.t -> ((a,b) thunk, string) Result.t = - fun f _ s -> Result.map (fun s -> Value s) (f s) - -let thunk_to_yojson : type a b. (a -> Yojson.Safe.t) -> (b -> Yojson.Safe.t) -> (a,b) thunk -> Yojson.Safe.t = - fun f _ t -> match t with - | Value v -> f v - | Thunk t -> f (Lazy.force t) - -let _hash : type a b. (a -> int) -> (b -> int) -> (a,b) thunk -> int = - fun f _ t -> match t with - | Value v -> f v - | Thunk t -> f (Lazy.force t) - -let hash_fold_thunk : type a b. (a Ppx_hash_lib.Std.Hash.folder) -> (b Ppx_hash_lib.Std.Hash.folder) -> (a,b) thunk Ppx_hash_lib.Std.Hash.folder = - fun f _ st t -> match t with - | Value v -> f st v - | Thunk t -> f st (Lazy.force t) - -let compare_thunk : type a b. (a Ppx_compare_lib.compare) -> (b Ppx_compare_lib.compare) -> (a,b) thunk Ppx_compare_lib.compare = - fun f _ t1 t2 -> match t1,t2 with - | Value v1, Value v2 -> f v1 v2 - | Thunk t1, Value v2 -> f (Lazy.force t1) v2 - | Value v1, Thunk t2 -> f v1 (Lazy.force t2) - | Thunk t1, Thunk t2 -> f (Lazy.force t1) (Lazy.force t2) - -type ('a, 'b) t = - [%import: ('a, 'b) DAst.t] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_dAst.mli b/serlib/ser_dAst.mli deleted file mode 100644 index 20b7a1a3..00000000 --- a/serlib/ser_dAst.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* template_arity -val sexp_of_template_arity : template_arity -> Sexp.t - -type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity - -val declaration_arity_of_sexp : - (Sexp.t -> 'a) -> - (Sexp.t -> 'b) -> - Sexp.t -> ('a, 'b) declaration_arity - -val sexp_of_declaration_arity : - ('a -> Sexp.t) -> - ('b -> Sexp.t) -> - ('a, 'b) declaration_arity -> Sexp.t - -type recarg = Declarations.recarg - [@@deriving sexp,yojson,hash,compare] - -type wf_paths = recarg Rtree.t - [@@deriving sexp,yojson,hash,compare] - -type regular_inductive_arity = Declarations.regular_inductive_arity - [@@deriving sexp,yojson,hash,compare] - -type inductive_arity = Declarations.inductive_arity - [@@deriving sexp,yojson,hash,compare] - -type one_inductive_body = Declarations.one_inductive_body - [@@deriving sexp,yojson,hash,compare] - -(* type set_predicativity = Declarations.set_predicativity - * val set_predicativity_of_sexp : Sexp.t -> set_predicativity - * val sexp_of_set_predicativity : set_predicativity -> Sexp.t *) - -(* type engagement = Declarations.engagement - * val engagement_of_sexp : Sexp.t -> engagement - * val sexp_of_engagement : engagement -> Sexp.t *) - -type typing_flags = Declarations.typing_flags - [@@deriving sexp,yojson,hash,compare] - -type inline = Declarations.inline - [@@deriving sexp,yojson,hash,compare] - -(* type work_list = Declarations.work_list *) - -(* type abstr_info = Declarations.abstr_info = { - * abstr_ctx : Constr.named_context; - * abstr_subst : Univ.Instance.t; - * abstr_uctx : Univ.AbstractContext.t; - * } - * - * type cooking_info = Declarations.cooking_info - * val sexp_of_cooking_info : cooking_info -> Sexp.t - * val cooking_info_of_sexp : Sexp.t -> cooking_info *) - -type ('a, 'b) pconstant_body = ('a, 'b) Declarations.pconstant_body - [@@deriving sexp,yojson,hash,compare] - -type constant_body = Declarations.constant_body - [@@deriving sexp,yojson,hash,compare] - -(* type record_body = Declarations.record_body - * val record_body_of_sexp : Sexp.t -> record_body - * val sexp_of_record_body : record_body -> Sexp.t *) - -type recursivity_kind = Declarations.recursivity_kind - [@@deriving sexp,yojson,hash,compare] - -type mutual_inductive_body = Declarations.mutual_inductive_body - [@@deriving sexp,yojson,hash,compare] - -type rewrite_rule = Declarations.rewrite_rule - [@@deriving sexp,yojson,hash,compare] - -type 'a module_alg_expr = 'a Declarations.module_alg_expr - [@@deriving sexp,yojson,hash,compare] - -type structure_body = Declarations.structure_body - [@@deriving sexp,yojson,hash,compare] - -type module_body = Declarations.module_body - [@@deriving sexp,yojson,hash,compare] - -type module_type_body = Declarations.module_type_body - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_declaremods.ml b/serlib/ser_declaremods.ml deleted file mode 100644 index faab1f64..00000000 --- a/serlib/ser_declaremods.ml +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* env val sexp_of_env : env -> Sexp.t - -type ('constr, 'types) punsafe_judgment = ('constr, 'types) - Environ.punsafe_judgment - -val punsafe_judgment_of_sexp : (Sexp.t -> 'constr) -> (Sexp.t -> - 'types) -> Sexp.t -> ('constr, 'types) punsafe_judgment val - sexp_of_punsafe_judgment : ('constr -> Sexplib.Sexp.t) -> ('types - -> Sexplib.Sexp.t) -> ('constr, 'types) punsafe_judgment -> Sexp.t - -type unsafe_judgment = Environ.unsafe_judgment val - unsafe_judgment_of_sexp : Sexp.t -> unsafe_judgment val - sexp_of_unsafe_judgment : unsafe_judgment -> Sexp.t diff --git a/serlib/ser_equality.ml b/serlib/ser_equality.ml deleted file mode 100644 index d0780a00..00000000 --- a/serlib/ser_equality.ml +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= _t_get) -let to_yojson level = _t_to_yojson (_t_put level) - -let hash x = hash__t (_t_put x) -let hash_fold_t st id = hash_fold__t st (_t_put id) - -let compare x y = compare__t (_t_put x) (_t_put y) - -end - -include Self - -module Set = Ser_cSet.Make(Evar.Set)(Self) diff --git a/serlib/ser_evar.mli b/serlib/ser_evar.mli deleted file mode 100644 index 131d0371..00000000 --- a/serlib/ser_evar.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* conv_pb -val sexp_of_conv_pb : conv_pb -> Sexp.t - -type evar_constraint = Evd.evar_constraint - -val evar_constraint_of_sexp : Sexp.t -> evar_constraint -val sexp_of_evar_constraint : evar_constraint -> Sexp.t - -type unsolvability_explanation = Evd.unsolvability_explanation - -val unsolvability_explanation_of_sexp : Sexp.t -> unsolvability_explanation -val sexp_of_unsolvability_explanation : unsolvability_explanation -> Sexp.t diff --git a/serlib/ser_extend.ml b/serlib/ser_extend.ml deleted file mode 100644 index 365f7511..00000000 --- a/serlib/ser_extend.ml +++ /dev/null @@ -1,55 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* production_position -val sexp_of_production_position : production_position -> Sexp.t - -type production_level = Extend.production_level [@@deriving sexp,yojson,hash,compare] - -type binder_entry_kind = Extend.binder_entry_kind -val binder_entry_kind_of_sexp : Sexp.t -> binder_entry_kind -val sexp_of_binder_entry_kind : binder_entry_kind -> Sexp.t - -type 'lev constr_entry_key_gen = 'lev Extend.constr_entry_key_gen -val constr_entry_key_gen_of_sexp : (Sexp.t -> 'lev) -> - Sexp.t -> 'lev constr_entry_key_gen -val sexp_of_constr_entry_key_gen : ('lev -> Sexp.t) -> - 'lev constr_entry_key_gen -> Sexp.t - -type constr_entry_key = Extend.constr_entry_key -val constr_entry_key_of_sexp : Sexp.t -> constr_entry_key -val sexp_of_constr_entry_key : constr_entry_key -> Sexp.t - -type constr_prod_entry_key = Extend.constr_prod_entry_key -val constr_prod_entry_key_of_sexp : Sexp.t -> constr_prod_entry_key -val sexp_of_constr_prod_entry_key : constr_prod_entry_key -> Sexp.t - -type simple_constr_prod_entry_key = Extend.simple_constr_prod_entry_key [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_feedback.ml b/serlib/ser_feedback.ml deleted file mode 100644 index 23fb4edc..00000000 --- a/serlib/ser_feedback.ml +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t = fun at -> - match at with - | Rawwit w -> List [Atom "Rawwit"; sexp_of_genarg_type w] - | Glbwit w -> List [Atom "Glbwit"; sexp_of_genarg_type w] - | Topwit w -> List [Atom "Topwit"; sexp_of_genarg_type w] - -let rec argument_type_of_sexp : Sexp.t -> argument_type = fun sexp -> - match sexp with - | List [Atom "ExtraArg"; Atom tag] -> - begin match ArgT.name tag with - | None -> raise (Failure "SEXP Exception in argument_type") - | Some (ArgT.Any t) -> ArgumentType (ExtraArg t) - end - | List [Atom "ListArg"; s1] -> - let (ArgumentType t) = argument_type_of_sexp s1 in - ArgumentType (ListArg t) - | List [Atom "OptArg"; s1] -> - let (ArgumentType t) = argument_type_of_sexp s1 in - ArgumentType (OptArg t) - | List [Atom "PairArg"; s1; s2] -> - let (ArgumentType t1) = argument_type_of_sexp s1 in - let (ArgumentType t2) = argument_type_of_sexp s2 in - ArgumentType (PairArg(t1,t2)) - | _ -> raise (Failure "SEXP Exception") - -let hash_fold_abstract_argument_type : type lvl. ('o, lvl) abstract_argument_type Hash.folder = fun st at -> - match at with - | Rawwit w -> hash_tagged hash_fold_genarg_type st "raw" w - | Glbwit w -> hash_tagged hash_fold_genarg_type st "glb" w - | Topwit w -> hash_tagged hash_fold_genarg_type st "top" w - -type ('raw, 'glb, 'top) gen_ser = - { raw_ser : 'raw -> Sexp.t - ; raw_des : Sexp.t -> 'raw - ; raw_hash : 'raw Hash.folder - ; raw_compare : 'raw -> 'raw -> int - - ; glb_ser : 'glb -> Sexp.t - ; glb_des : Sexp.t -> 'glb - ; glb_hash : 'glb Hash.folder - ; glb_compare : 'glb -> 'glb -> int - - ; top_ser : 'top -> Sexp.t - ; top_des : Sexp.t -> 'top - ; top_hash : 'top Ppx_hash_lib.Std.Hash.folder - ; top_compare : 'top -> 'top -> int - } - -module T2_ = struct - type ('a, 'b) t = 'a * 'b [@@deriving hash, compare] -end - -let gen_ser_list : - ('raw, 'glb, 'top) gen_ser -> - ('raw list, 'glb list, 'top list) gen_ser = fun g -> - let open Sexplib.Conv in - { raw_ser = sexp_of_list g.raw_ser - ; raw_des = list_of_sexp g.raw_des - ; raw_hash = Hash.Builtin.hash_fold_list g.raw_hash - ; raw_compare = compare_list g.raw_compare - - ; glb_ser = sexp_of_list g.glb_ser - ; glb_des = list_of_sexp g.glb_des - ; glb_hash = Hash.Builtin.hash_fold_list g.glb_hash - ; glb_compare = compare_list g.glb_compare - - ; top_ser = sexp_of_list g.top_ser - ; top_des = list_of_sexp g.top_des - ; top_hash = Hash.Builtin.hash_fold_list g.top_hash - ; top_compare = compare_list g.top_compare - } - -let gen_ser_opt : - ('raw, 'glb, 'top) gen_ser -> - ('raw option, 'glb option, 'top option) gen_ser = fun g -> - let open Sexplib.Conv in - { raw_ser = sexp_of_option g.raw_ser - ; raw_des = option_of_sexp g.raw_des - ; raw_hash = Hash.Builtin.hash_fold_option g.raw_hash - ; raw_compare = compare_option g.raw_compare - - ; glb_ser = sexp_of_option g.glb_ser - ; glb_des = option_of_sexp g.glb_des - ; glb_hash = Hash.Builtin.hash_fold_option g.glb_hash - ; glb_compare = compare_option g.glb_compare - - ; top_ser = sexp_of_option g.top_ser - ; top_des = option_of_sexp g.top_des - ; top_hash = Hash.Builtin.hash_fold_option g.top_hash - ; top_compare = compare_option g.top_compare - } - -let gen_ser_pair : - ('raw1, 'glb1, 'top1) gen_ser -> - ('raw2, 'glb2, 'top2) gen_ser -> - (('raw1 * 'raw2), ('glb1 * 'glb2), ('top1 * 'top2)) gen_ser = fun g1 g2 -> - let open Sexplib.Conv in - { raw_ser = sexp_of_pair g1.raw_ser g2.raw_ser - ; raw_des = pair_of_sexp g1.raw_des g2.raw_des - ; raw_hash = T2_.hash_fold_t g1.raw_hash g2.raw_hash - ; raw_compare = T2_.compare g1.raw_compare g2.raw_compare - - ; glb_ser = sexp_of_pair g1.glb_ser g2.glb_ser - ; glb_des = pair_of_sexp g1.glb_des g2.glb_des - ; glb_hash = T2_.hash_fold_t g1.glb_hash g2.glb_hash - ; glb_compare = T2_.compare g1.glb_compare g2.glb_compare - - ; top_ser = sexp_of_pair g1.top_ser g2.top_ser - ; top_des = pair_of_sexp g1.top_des g2.top_des - ; top_hash = T2_.hash_fold_t g1.top_hash g2.top_hash - ; top_compare = T2_.compare g1.top_compare g2.top_compare - } - -module SerObj = struct - - type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) gen_ser - - let sexp_of_gen typ ga = - let typ = typ ^ ": " ^ Sexp.to_string (sexp_of_genarg_type ga) in - Serlib_base.sexp_of_opaque ~typ - - let name = "ser_arg" - let default _ga = - Some - { - (* raw_ser = (fun _ -> Sexp.(List [Atom "[XXX ser_gen]"; Atom "raw"; sexp_of_genarg_type ga])); *) - raw_ser = sexp_of_gen "raw" _ga - ; raw_des = (Sexplib.Conv_error.no_matching_variant_found "raw_arg") - ; raw_hash = (fun st a -> Hash.fold_int st (Hashtbl.hash a)) - ; raw_compare = Stdlib.compare - - (* glb_ser = (fun _ -> Sexp.(List [Atom "[XXX ser_gen]"; Atom "glb"; sexp_of_genarg_type ga])); *) - ; glb_ser = sexp_of_gen "glb" _ga - ; glb_des = (Sexplib.Conv_error.no_matching_variant_found "glb_arg") - ; glb_hash = (fun st a -> Hash.fold_int st (Hashtbl.hash a)) - ; glb_compare = Stdlib.compare - - (* top_ser = (fun _ -> Sexp.(List [Atom "[XXX ser_gen]"; Atom "top"; sexp_of_genarg_type ga])); *) - ; top_ser = sexp_of_gen "top" _ga - ; top_des = (Sexplib.Conv_error.no_matching_variant_found "top_arg") - ; top_hash = (fun st a -> Hash.fold_int st (Hashtbl.hash a)) - ; top_compare = Stdlib.compare - } -end - -module SerGen = Register(SerObj) -let register_genser ty obj = SerGen.register0 ty obj - -let rec get_gen_ser_ty : type r g t. (r,g,t) Genarg.genarg_type -> (r,g,t) gen_ser = - fun gt -> match gt with - | Genarg.ExtraArg _ -> SerGen.obj gt - | Genarg.ListArg t -> gen_ser_list (get_gen_ser_ty t) - | Genarg.OptArg t -> gen_ser_opt (get_gen_ser_ty t) - | Genarg.PairArg(t1, t2) -> gen_ser_pair (get_gen_ser_ty t1) (get_gen_ser_ty t2) - -let get_gen_ser : type lvl. ('o,lvl) abstract_argument_type -> ('o -> 't) = fun aty -> - match aty with - | Genarg.Rawwit ty -> (get_gen_ser_ty ty).raw_ser - | Genarg.Glbwit ty -> (get_gen_ser_ty ty).glb_ser - | Genarg.Topwit ty -> (get_gen_ser_ty ty).top_ser - -let generic_des : type lvl. ('o,lvl) abstract_argument_type -> Sexp.t -> lvl generic_argument = fun ty s -> - match ty with - | Genarg.Rawwit w -> GenArg(ty, (get_gen_ser_ty w).raw_des s) - | Genarg.Glbwit w -> GenArg(ty, (get_gen_ser_ty w).glb_des s) - | Genarg.Topwit w -> GenArg(ty, (get_gen_ser_ty w).top_des s) - -let hash_fold_generic : type lvl. ('o,lvl) abstract_argument_type -> 'o Ppx_hash_lib.Std.Hash.folder = fun aty -> - match aty with - | Genarg.Rawwit ty -> (get_gen_ser_ty ty).raw_hash - | Genarg.Glbwit ty -> (get_gen_ser_ty ty).glb_hash - | Genarg.Topwit ty -> (get_gen_ser_ty ty).top_hash - -let compare_generic : type lvl. ('o,lvl) abstract_argument_type -> 'o Ppx_compare_lib.compare = fun aty -> - match aty with - | Genarg.Rawwit ty -> (get_gen_ser_ty ty).raw_compare - | Genarg.Glbwit ty -> (get_gen_ser_ty ty).glb_compare - | Genarg.Topwit ty -> (get_gen_ser_ty ty).top_compare - -(* We need to generalize this to use the proper printers for opt *) -let mk_sexparg st so = - Sexp.List [Atom "GenArg"; st; so] - -(* XXX: There is still some duplication here in the traversal of g_ty, but - we can live with that for now. *) -let sexp_of_genarg_val : type a. a generic_argument -> Sexp.t = - fun g -> match g with - | GenArg (g_ty, g_val) -> - mk_sexparg (sexp_of_abstract_argument_type g_ty) (get_gen_ser g_ty g_val) - -let sexp_of_generic_argument : type a. (a -> Sexp.t) -> a generic_argument -> Sexp.t = - fun _level_tag g -> - sexp_of_genarg_val g - -type rgen_argument = RG : 'lvl generic_argument -> rgen_argument - -let hash_fold_genarg_val : type a. a generic_argument Hash.folder = - fun st g -> match g with - | GenArg (g_ty, g_val) -> - let st = hash_fold_abstract_argument_type st g_ty in - hash_fold_generic g_ty st g_val - -let hash_fold_generic_argument : type a. a Hash.folder -> a generic_argument Hash.folder = - fun _level_tag g -> hash_fold_genarg_val g - -let compare_genarg_val : type a. a generic_argument Ppx_compare_lib.compare = - fun g1 g2 -> match g1 with - | GenArg (g1_ty, g1_val) -> - match g2 with - | GenArg (g2_ty, g2_val) -> - match Genarg.abstract_argument_type_eq g1_ty g2_ty with - | Some Refl -> - compare_generic g1_ty g1_val g2_val - (* XXX: Technically, we should implement our own compare so ordering works *) - | None -> 1 - -let compare_generic_argument : type a. a Ppx_compare_lib.compare -> a generic_argument Ppx_compare_lib.compare = - fun _level_tag g -> compare_genarg_val g - -let gen_abstype_of_sexp : Sexp.t -> rgen_argument = fun s -> - match s with - | List [Atom "GenArg"; List [ Atom "Rawwit"; sty]; sobj] -> - let (ArgumentType ty) = argument_type_of_sexp sty in - RG (generic_des (Rawwit ty) sobj) - | List [Atom "GenArg"; List [ Atom "Glbwit"; sty]; sobj] -> - let (ArgumentType ty) = argument_type_of_sexp sty in - RG (generic_des (Glbwit ty) sobj) - | List [Atom "GenArg"; List [ Atom "Topwit"; sty]; sobj] -> - let (ArgumentType ty) = argument_type_of_sexp sty in - RG (generic_des (Topwit ty) sobj) - | _ -> raise (Failure "SEXP Exception in abstype") - -let generic_argument_of_sexp _lvl sexp : 'a Genarg.generic_argument = - let (RG ga) = gen_abstype_of_sexp sexp in - Obj.magic ga - -let rec yojson_to_sexp json = match json with - | `String s -> Sexp.Atom s - | `List s -> Sexp.List (List.map yojson_to_sexp s) - | _ -> raise (Failure "ser_genarg: yojson_to_sexp") - -let rec sexp_to_yojson sexp : Yojson.Safe.t = - match sexp with - | Sexp.Atom s -> `String s - | List l -> `List (List.map sexp_to_yojson l) - -let generic_argument_of_yojson lvl json = - let sexp = yojson_to_sexp json in - Result.Ok (generic_argument_of_sexp lvl sexp) - -let generic_argument_to_yojson : type a. (a -> Yojson.Safe.t) -> a generic_argument -> Yojson.Safe.t = - fun _level_tag g -> - sexp_of_generic_argument (fun _ -> Atom "") g |> sexp_to_yojson - -type 'a generic_argument = 'a Genarg.generic_argument - -type glob_generic_argument = - [%import: Genarg.glob_generic_argument] - [@@deriving sexp,yojson,hash,compare] - -type raw_generic_argument = - [%import: Genarg.raw_generic_argument] - [@@deriving sexp,yojson,hash,compare] - -type typed_generic_argument = - [%import: Genarg.typed_generic_argument] - [@@deriving sexp,yojson,hash,compare] - -let mk_uniform pin pout phash pcompare = - { raw_ser = pin - ; raw_des = pout - ; raw_hash = phash - ; raw_compare = pcompare - - ; glb_ser = pin - ; glb_des = pout - ; glb_hash = phash - ; glb_compare = pcompare - - ; top_ser = pin - ; top_des = pout - ; top_hash = phash - ; top_compare = pcompare - } - -let mk_vernac_arg pin pout phash pcompare = - { raw_ser = pin - ; raw_des = pout - ; raw_hash = phash - ; raw_compare = pcompare - - ; glb_ser = Ser_util.Empty.sexp_of_t - ; glb_des = Ser_util.Empty.t_of_sexp - ; glb_hash = Ser_util.Empty.hash_fold_t - ; glb_compare = Ser_util.Empty.compare - - - ; top_ser = Ser_util.Empty.sexp_of_t - ; top_des = Ser_util.Empty.t_of_sexp - ; top_hash = Ser_util.Empty.hash_fold_t - ; top_compare = Ser_util.Empty.compare - } - -module type GenSer0 = sig - type t [@@deriving sexp,hash,compare] -end - -module GS0 (M : GenSer0) = struct - let genser = mk_uniform M.sexp_of_t M.t_of_sexp M.hash_fold_t M.compare -end - -module GSV (M : GenSer0) = struct - let genser = mk_vernac_arg M.sexp_of_t M.t_of_sexp M.hash_fold_t M.compare -end - -module type GenSer = sig - type raw [@@deriving sexp,hash,compare] - type glb [@@deriving sexp,hash,compare] - type top [@@deriving sexp,hash,compare] -end - -module GS (M : GenSer) = struct - let genser = - { raw_ser = M.sexp_of_raw - ; raw_des = M.raw_of_sexp - ; raw_hash = M.hash_fold_raw - ; raw_compare = M.compare_raw - - ; glb_ser = M.sexp_of_glb - ; glb_des = M.glb_of_sexp - ; glb_hash = M.hash_fold_glb - ; glb_compare = M.compare_glb - - ; top_ser = M.sexp_of_top - ; top_des = M.top_of_sexp - ; top_hash = M.hash_fold_top - ; top_compare = M.compare_top - } -end diff --git a/serlib/ser_genarg.mli b/serlib/ser_genarg.mli deleted file mode 100644 index 4cac1409..00000000 --- a/serlib/ser_genarg.mli +++ /dev/null @@ -1,103 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t) ref *) -(* val sexp_of_tacdef_body : (Tacexpr.tacdef_body -> Sexp.t) ref *) - -(**********************************************************************) -(* GenArg *) -(**********************************************************************) - -type rlevel = Genarg.rlevel - [@@deriving sexp,yojson,hash,compare] -type glevel = Genarg.glevel - [@@deriving sexp,yojson,hash,compare] -type tlevel = Genarg.tlevel - [@@deriving sexp,yojson,hash,compare] - -type 'a generic_argument = 'a Genarg.generic_argument - [@@deriving sexp,yojson,hash,compare] - -type glob_generic_argument = Genarg.glob_generic_argument -[@@deriving sexp,yojson,hash,compare] - -type raw_generic_argument = Genarg.raw_generic_argument -[@@deriving sexp,yojson,hash,compare] - -type typed_generic_argument = Genarg.typed_generic_argument -val typed_generic_argument_of_sexp : Sexp.t -> Genarg.typed_generic_argument -val sexp_of_typed_generic_argument : Genarg.typed_generic_argument -> Sexp.t - -(* Registering serializing functions *) -type ('raw, 'glb, 'top) gen_ser = - { raw_ser : 'raw -> Sexp.t - ; raw_des : Sexp.t -> 'raw - ; raw_hash : 'raw Ppx_hash_lib.Std.Hash.folder - ; raw_compare : 'raw -> 'raw -> int - - ; glb_ser : 'glb -> Sexp.t - ; glb_des : Sexp.t -> 'glb - ; glb_hash : 'glb Ppx_hash_lib.Std.Hash.folder - ; glb_compare : 'glb -> 'glb -> int - - ; top_ser : 'top -> Sexp.t - ; top_des : Sexp.t -> 'top - ; top_hash : 'top Ppx_hash_lib.Std.Hash.folder - ; top_compare : 'top -> 'top -> int - } - -val register_genser : - ('raw, 'glb, 'top) Genarg.genarg_type -> - ('raw, 'glb, 'top) gen_ser -> unit - -val gen_ser_pair : - ('raw1, 'glb1, 'top1) gen_ser -> - ('raw2, 'glb2, 'top2) gen_ser -> - (('raw1 * 'raw2), ('glb1 * 'glb2), ('top1 * 'top2)) gen_ser - -val gen_ser_list : - ('raw, 'glb, 'top) gen_ser -> - ('raw list, 'glb list, 'top list) gen_ser - -val mk_uniform : ('t -> Sexp.t) -> (Sexp.t -> 't) -> - 't Ppx_hash_lib.Std.Hash.folder -> - 't Ppx_compare_lib.compare -> - ('t,'t,'t) gen_ser - -val mk_vernac_arg : ('t -> Sexp.t) -> (Sexp.t -> 't) -> - 't Ppx_hash_lib.Std.Hash.folder -> - 't Ppx_compare_lib.compare -> - ('t,Util.Empty.t,Util.Empty.t) gen_ser - -module type GenSer0 = sig - type t [@@deriving sexp,hash,compare] -end - -module GS0 (M : GenSer0) : sig val genser : (M.t,M.t,M.t) gen_ser end - -module GSV (M : GenSer0) : sig val genser : (M.t,Util.Empty.t,Util.Empty.t) gen_ser end - -module type GenSer = sig - type raw [@@deriving sexp,hash,compare] - type glb [@@deriving sexp,hash,compare] - type top [@@deriving sexp,hash,compare] -end - -module GS (M : GenSer) : sig val genser : (M.raw,M.glb,M.top) gen_ser end diff --git a/serlib/ser_genintern.ml b/serlib/ser_genintern.ml deleted file mode 100644 index eef19d39..00000000 --- a/serlib/ser_genintern.ml +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* glob_sign -val sexp_of_glob_sign : glob_sign -> Sexp.t - -type glob_constr_and_expr = Genintern.glob_constr_and_expr - [@@deriving sexp, yojson, hash, compare] - -type glob_constr_pattern_and_expr = Genintern.glob_constr_pattern_and_expr - [@@deriving sexp, yojson, hash, compare] diff --git a/serlib/ser_geninterp.ml b/serlib/ser_geninterp.ml deleted file mode 100644 index 5075a82b..00000000 --- a/serlib/ser_geninterp.ml +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t -> 'a Glob_term.cast_type - * val sexp_of_cast_type : ('a -> Sexp.t) -> 'a Glob_term.cast_type -> Sexp.t - * val cast_type_of_yojson : (Yojson.Safe.t -> ('a,string) result ) -> Yojson.Safe.t -> ('a cast_type, string) Result.t - * val cast_type_to_yojson : ('a -> Yojson.Safe.t) -> 'a cast_type -> Yojson.Safe.t *) - -type glob_constraint = Glob_term.glob_constraint - [@@deriving sexp,yojson,hash,compare] - -type existential_name = Glob_term.existential_name [@@deriving sexp,yojson,hash,compare] -type cases_pattern = Glob_term.cases_pattern - -type glob_constr = Glob_term.glob_constr -and glob_decl = Glob_term.glob_decl -and predicate_pattern = Glob_term.predicate_pattern -and tomatch_tuple = Glob_term.tomatch_tuple -and tomatch_tuples = Glob_term.tomatch_tuples -and cases_clause = Glob_term.cases_clause -and cases_clauses = Glob_term.cases_clauses - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_globnames.ml b/serlib/ser_globnames.ml deleted file mode 100644 index c0ee9569..00000000 --- a/serlib/ser_globnames.ml +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= _t_get) -let qualid_r_to_yojson level = _t_to_yojson (_t_put level) - -(* let hash_qualid_r x = hash__t (_t_put x) *) -let hash_fold_qualid_r st x = hash_fold__t st (_t_put x) -let compare_qualid_r x y = compare__t (_t_put x) (_t_put y) - -(* qualid: private *) -type qualid = - [%import: Libnames.qualid] - [@@deriving sexp,yojson,hash,compare] - -module FP = struct - type _t = - { dirpath : Names.DirPath.t - ; basename : Names.Id.t } - [@@deriving sexp,yojson,hash,compare] - - let _t_get { dirpath; basename } = Libnames.make_path dirpath basename - let _t_put fp = let dirpath, basename = Libnames.repr_path fp in { dirpath; basename } -end - -open FP - -type full_path = Libnames.full_path -let full_path_of_sexp sexp = _t_get (_t_of_sexp sexp) -let sexp_of_full_path qid = sexp_of__t (_t_put qid) - -let full_path_of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) -let full_path_to_yojson level = _t_to_yojson (_t_put level) - -let hash_full_path x = hash__t (_t_put x) -let hash_fold_full_path st x = hash_fold__t st (_t_put x) - -let compare_full_path x y = compare__t (_t_put x) (_t_put y) diff --git a/serlib/ser_libnames.mli b/serlib/ser_libnames.mli deleted file mode 100644 index 616c7e6a..00000000 --- a/serlib/ser_libnames.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t -> 'a hyp_location_expr -val sexp_of_hyp_location_expr : ('a -> Sexp.t) -> 'a hyp_location_expr -> Sexp.t - -type 'id clause_expr = 'id Locus.clause_expr - [@@deriving sexp,yojson,hash,compare] - -type clause = Locus.clause - -val clause_of_sexp : Sexp.t -> clause -val sexp_of_clause : clause -> Sexp.t - -type clause_atom = Locus.clause_atom - -val clause_atom_of_sexp : Sexp.t -> clause_atom -val sexp_of_clause_atom : clause_atom -> Sexp.t - -type concrete_clause = Locus.concrete_clause - -val concrete_clause_of_sexp : Sexp.t -> concrete_clause -val sexp_of_concrete_clause : concrete_clause -> Sexp.t - -type hyp_location = Locus.hyp_location - [@@deriving sexp,yojson,hash,compare] - -type goal_location = Locus.goal_location - -val goal_location_of_sexp : Sexp.t -> goal_location -val sexp_of_goal_location : goal_location -> Sexp.t - -type simple_clause = Locus.simple_clause -val simple_clause_of_sexp : Sexp.t -> simple_clause -val sexp_of_simple_clause : simple_clause -> Sexp.t - -type 'id or_like_first = 'id Locus.or_like_first - -val or_like_first_of_sexp : (Sexp.t -> 'id) -> Sexp.t -> 'id or_like_first -val sexp_of_or_like_first : ('id -> Sexp.t) -> 'id or_like_first -> Sexp.t diff --git a/serlib/ser_ltac_pretype.ml b/serlib/ser_ltac_pretype.ml deleted file mode 100644 index 6428150a..00000000 --- a/serlib/ser_ltac_pretype.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* closure -val sexp_of_closure : closure -> Sexp.t - -type closed_glob_constr = Ltac_pretype.closed_glob_constr - [@@deriving sexp,hash,compare] - -type constr_under_binders = Ltac_pretype.constr_under_binders - -val constr_under_binders_of_sexp : Sexp.t -> constr_under_binders -val sexp_of_constr_under_binders : constr_under_binders -> Sexp.t diff --git a/serlib/ser_mod_subst.ml b/serlib/ser_mod_subst.ml deleted file mode 100644 index 9dbb71ed..00000000 --- a/serlib/ser_mod_subst.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t) -> 'a substituted -> Sexp.t - * val substituted_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a substituted *) diff --git a/serlib/ser_namegen.ml b/serlib/ser_namegen.ml deleted file mode 100644 index c21d37a0..00000000 --- a/serlib/ser_namegen.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= _kername_get) -let to_yojson kn = _t_to_yojson (_t_put kn) - -let hash x = hash__t (_t_put x) -let hash_fold_t st id = hash_fold__t st (_t_put id) - -let compare x y = compare__t (_t_put x) (_t_put y) - -let equal = KerName.equal - -end - -module KNmap = Ser_cMap.Make(Names.KNmap)(KerName) - -module Constant = struct - -(* Constant.t: private *) -type t = [%import: Names.Constant.t] - -type _t = Constant of KerName.t * KerName.t option - [@@deriving sexp,yojson,hash,compare] - -let _t_put cs = - let cu, cc = Constant.(user cs, canonical cs) in - if KerName.equal cu cc then Constant (cu, None) else Constant (cu, Some cc) -let _t_get = function - | Constant (cu, None) -> Constant.make1 cu - | Constant (cu, Some cc) -> Constant.make cu cc - -let t_of_sexp sexp = _t_get (_t_of_sexp sexp) -let sexp_of_t dp = sexp_of__t (_t_put dp) - -let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) -let to_yojson level = _t_to_yojson (_t_put level) - -let hash x = hash__t (_t_put x) -let hash_fold_t st id = hash_fold__t st (_t_put id) - -let compare x y = compare__t (_t_put x) (_t_put y) - -end - -module Cset_env = Ser_cSet.Make(Cset_env)(Constant) - -module Cmap = Ser_cMap.Make(Cmap)(Constant) -module Cmap_env = Ser_cMap.Make(Cmap_env)(Constant) - -module MutInd = struct - -(* MutInd.t: private *) - module BijectSpec = struct - type t = [%import: Names.MutInd.t] - type _t = MutInd of KerName.t * KerName.t option - [@@deriving sexp,yojson,hash,compare] - - let of_t cs = - let cu, cc = MutInd.(user cs, canonical cs) in - if KerName.equal cu cc then MutInd (cu, None) else MutInd (cu, Some cc) - - let to_t = function - | MutInd (cu, None) -> MutInd.make1 cu - | MutInd (cu, Some cc) -> MutInd.make cu cc - end - - include SerType.Biject(BijectSpec) -end - -module Mindmap = Ser_cMap.Make(Mindmap)(MutInd) -module Mindmap_env = Ser_cMap.Make(Mindmap_env)(MutInd) - -type 'a tableKey = - [%import: 'a Names.tableKey] - [@@deriving sexp] - -type variable = - [%import: Names.variable] - [@@deriving sexp,yojson,hash,compare] - -(* Inductive and constructor = public *) -module Ind = struct - type t = - [%import: Names.Ind.t] - [@@deriving sexp,yojson,hash,compare] -end - -module Indset_env = Ser_cSet.Make(Indset_env)(Ind) -module Indmap_env = Ser_cMap.Make(Indmap_env)(Ind) - -type inductive = - [%import: Names.inductive] - [@@deriving sexp,yojson,hash,compare] - -module Construct = struct - type t = - [%import: Names.Construct.t] - [@@deriving sexp,yojson,hash,compare] - -end -type constructor = - [%import: Names.constructor] - [@@deriving sexp,yojson,hash,compare] - -(* Projection: private *) -module Projection = struct - - module Repr = struct - module PierceSpec = struct - type t = Names.Projection.Repr.t - type _t = - { proj_ind : inductive - ; proj_relevant : bool - ; proj_npars : int - ; proj_arg : int - ; proj_name : Label.t - } [@@deriving sexp,yojson,hash,compare] - end - include SerType.Pierce(PierceSpec) - end - - module PierceSpec = struct - type t = [%import: Names.Projection.t] - type _t = Repr.t * bool - [@@deriving sexp,yojson,hash,compare] - end - include SerType.Pierce(PierceSpec) -end - -module GlobRef = struct - -type t = [%import: Names.GlobRef.t] - [@@deriving sexp,yojson,hash,compare] - -end - -type lident = - [%import: Names.lident] - [@@deriving sexp,yojson,hash,compare] - -type lname = - [%import: Names.lname] - [@@deriving sexp,yojson,hash,compare] - -type lstring = - [%import: Names.lstring] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli deleted file mode 100644 index 41ccfd79..00000000 --- a/serlib/ser_names.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t -> 'a tableKey -val sexp_of_tableKey : ('a -> Sexp.t) -> 'a tableKey -> Sexp.t - -type variable = Names.variable [@@deriving sexp, yojson, hash, compare] -type inductive = Names.inductive [@@deriving sexp, yojson, hash, compare] -type constructor = Names.constructor [@@deriving sexp, yojson, hash, compare] - -module Projection : sig - - include SerType.SJHC with type t = Projection.t - - module Repr : sig - include SerType.SJHC with type t = Projection.Repr.t - end - -end - -module GlobRef : SerType.SJHC with type t = Names.GlobRef.t - -type lident = Names.lident [@@deriving sexp,yojson,hash,compare] -type lname = Names.lname [@@deriving sexp,yojson,hash,compare] -type lstring = Names.lstring [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_nametab.ml b/serlib/ser_nametab.ml deleted file mode 100644 index 12ab6da4..00000000 --- a/serlib/ser_nametab.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* parenRelation - * val sexp_of_parenRelation : parenRelation -> Sexp.t - * - * type precedence = Notation_gram.precedence - * - * val precedence_of_sexp : Sexp.t -> precedence - * val sexp_of_precedence : precedence -> Sexp.t - * - * type tolerability = Notation_gram.tolerability - * - * val tolerability_of_sexp : Sexp.t -> tolerability - * val sexp_of_tolerability : tolerability -> Sexp.t *) - -type grammar_constr_prod_item = Notation_gram.grammar_constr_prod_item -val grammar_constr_prod_item_of_sexp : Sexp.t -> grammar_constr_prod_item -val sexp_of_grammar_constr_prod_item : grammar_constr_prod_item -> Sexp.t - -type notation_grammar = Notation_gram.notation_grammar -val notation_grammar_of_sexp : Sexp.t -> notation_grammar -val sexp_of_notation_grammar : notation_grammar -> Sexp.t - diff --git a/serlib/ser_notation_term.ml b/serlib/ser_notation_term.ml deleted file mode 100644 index 88cf6af6..00000000 --- a/serlib/ser_notation_term.ml +++ /dev/null @@ -1,57 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* case_info_pattern -val sexp_of_case_info_pattern : case_info_pattern -> Sexp.t - -type constr_pattern = Pattern.constr_pattern - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_pp.ml b/serlib/ser_pp.ml deleted file mode 100644 index 3ff76fa8..00000000 --- a/serlib/ser_pp.ml +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Pp_empty - | Ppcmd_string s -> Pp_string s - | Ppcmd_glue l -> Pp_glue (List.map of_t l) - | Ppcmd_box (bt,d) -> Pp_box(bt, of_t d) - | Ppcmd_tag (t,d) -> Pp_tag(t, of_t d) - | Ppcmd_print_break (n,m) -> Pp_print_break(n,m) - | Ppcmd_force_newline -> Pp_force_newline - | Ppcmd_comment s -> Pp_comment s - - let rec to_t (d : _t) : t = unrepr (match d with - | Pp_empty -> Ppcmd_empty - | Pp_string s -> Ppcmd_string s - | Pp_glue l -> Ppcmd_glue (List.map to_t l) - | Pp_box (bt,d) -> Ppcmd_box(bt, to_t d) - | Pp_tag (t,d) -> Ppcmd_tag(t, to_t d) - | Pp_print_break (n,m) -> Ppcmd_print_break(n,m) - | Pp_force_newline -> Ppcmd_force_newline - | Pp_comment s -> Ppcmd_comment s) - -end - -include SerType.Biject(P) - -type doc_view = - [%import: Pp.doc_view] - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_pp.mli b/serlib/ser_pp.mli deleted file mode 100644 index 512dfdfc..00000000 --- a/serlib/ser_pp.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* ppbox -val sexp_of_ppbox : ppbox -> Sexp.t - -type ppcut = Ppextend.ppcut - -val ppcut_of_sexp : Sexp.t -> ppcut -val sexp_of_ppcut : ppcut -> Sexp.t - -(* type unparsing = Ppextend.unparsing - * val unparsing_of_sexp : Sexp.t -> unparsing - * val sexp_of_unparsing : unparsing -> Sexp.t *) - -type unparsing_rule = Ppextend.unparsing_rule -val unparsing_rule_of_sexp : Sexp.t -> unparsing_rule -val sexp_of_unparsing_rule : unparsing_rule -> Sexp.t - -type notation_printing_rules = Ppextend.notation_printing_rules -val notation_printing_rules_of_sexp : Sexp.t -> notation_printing_rules -val sexp_of_notation_printing_rules : notation_printing_rules -> Sexp.t diff --git a/serlib/ser_pretype_errors.ml b/serlib/ser_pretype_errors.ml deleted file mode 100644 index 1f2dfbc3..00000000 --- a/serlib/ser_pretype_errors.ml +++ /dev/null @@ -1,75 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - NotClean (e, ee, c) - | ConversionFailed (_, c1, c2) -> - ConversionFailed (ee, c1, c2) - | IncompatibleInstances (_, e, c1, c2) -> - IncompatibleInstances (ee, e, c1, c2) - | InstanceNotSameType (e, _, t1, t2) -> - InstanceNotSameType (e, ee, t1, t2) - | CannotSolveConstraint (e, ue) -> - CannotSolveConstraint (e, (filter_ue ue)) - | ue -> ue - -let sexp_of_unification_error ue = - filter_ue ue |> sexp_of_unification_error - -type position = - [%import: Pretype_errors.position] - [@@deriving sexp] - -type position_reporting = - [%import: Pretype_errors.position_reporting] - [@@deriving sexp] - -type subterm_unification_error = - [%import: Pretype_errors.subterm_unification_error] - [@@deriving sexp] - -type type_error = - [%import: Pretype_errors.type_error] - [@@deriving sexp] - -type pretype_error = - [%import: Pretype_errors.pretype_error] - [@@deriving sexp] diff --git a/serlib/ser_pretype_errors.mli b/serlib/ser_pretype_errors.mli deleted file mode 100644 index fb783695..00000000 --- a/serlib/ser_pretype_errors.mli +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unification_error -val sexp_of_unification_error : unification_error -> Sexp.t - -type position = Pretype_errors.position -val position_of_sexp : Sexp.t -> position -val sexp_of_position : position -> Sexp.t - -type position_reporting = Pretype_errors.position_reporting -val position_reporting_of_sexp : Sexp.t -> position_reporting -val sexp_of_position_reporting : position_reporting -> Sexp.t - -type subterm_unification_error = Pretype_errors.subterm_unification_error -val subterm_unification_error_of_sexp : Sexp.t -> subterm_unification_error -val sexp_of_subterm_unification_error : subterm_unification_error -> Sexp.t - -type pretype_error = Pretype_errors.pretype_error -val pretype_error_of_sexp : Sexp.t -> pretype_error -val sexp_of_pretype_error : pretype_error -> Sexp.t diff --git a/serlib/ser_printer.ml b/serlib/ser_printer.ml deleted file mode 100644 index c8164b50..00000000 --- a/serlib/ser_printer.ml +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 'b) (x : 'a SList.t) : 'b SList.t = Obj.magic (_map f (Obj.magic x)) diff --git a/serlib/ser_safe_typing.ml b/serlib/ser_safe_typing.ml deleted file mode 100644 index 4f5cdb03..00000000 --- a/serlib/ser_safe_typing.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 'a) (x : Sexp.t) : 'a effect_entry = - let open Sexp in - match x with - | Atom "PureEntry" -> - Obj__magic PureEntry - | Atom "EffectEntry" -> - Obj__magic EffectEntry - | _ -> - Sexplib.Conv_error.no_variant_match () -*) - -type global_declaration = - [%import: Safe_typing.global_declaration] - [@@deriving sexp] diff --git a/serlib/ser_safe_typing.mli b/serlib/ser_safe_typing.mli deleted file mode 100644 index 1613aad1..00000000 --- a/serlib/ser_safe_typing.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* global_declaration -val sexp_of_global_declaration : global_declaration -> Sexp.t diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml deleted file mode 100644 index 5b3c022d..00000000 --- a/serlib/ser_sorts.ml +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* t -val sexp_of_t : t -> Sexp.t - -type 'c p = 'c Tok.p -val p_of_sexp : (Sexp.t -> 'c) -> Sexp.t -> 'c p -val sexp_of_p : ('c -> Sexp.t) -> 'c p -> Sexp.t diff --git a/serlib/ser_type_errors.ml b/serlib/ser_type_errors.ml deleted file mode 100644 index ccd8141c..00000000 --- a/serlib/ser_type_errors.ml +++ /dev/null @@ -1,59 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* guard_error -val sexp_of_guard_error : guard_error -> Sexp.t - -type ('c,'t) pcant_apply_bad_type = ('c, 't) Type_errors.pcant_apply_bad_type - -val pcant_apply_bad_type_of_sexp : - (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> - Sexp.t -> ('constr, 'types) pcant_apply_bad_type - -val sexp_of_pcant_apply_bad_type : - ('constr -> Sexp.t) -> - ('types -> Sexp.t) -> - ('constr, 'types) pcant_apply_bad_type -> Sexp.t - -type ('c, 't, 'r) ptype_error = ('c, 't, 'r) Type_errors.ptype_error -val ptype_error_of_sexp : - (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) -> - Sexp.t -> ('constr, 'types, 'r) ptype_error - -val sexp_of_ptype_error : - ('constr -> Sexp.t) -> - ('types -> Sexp.t) -> - ('r -> Sexp.t) -> - ('constr, 'types, 'r) ptype_error -> Sexp.t - -type type_error = Type_errors.type_error -val type_error_of_sexp : Sexp.t -> type_error -val sexp_of_type_error : type_error -> Sexp.t - diff --git a/serlib/ser_typeclasses.ml b/serlib/ser_typeclasses.ml deleted file mode 100644 index c22cf055..00000000 --- a/serlib/ser_typeclasses.ml +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= _t_get) -let to_yojson level = _t_to_yojson (_t_put level) - -let hash_fold_t st i = - Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int64 st (Uint63.to_int64 i) - -let compare i1 i2 = - Ppx_compare_lib.Builtin.compare_int64 (Uint63.to_int64 i1) (Uint63.to_int64 i2) diff --git a/serlib/ser_univ.ml b/serlib/ser_univ.ml deleted file mode 100644 index 160f470d..00000000 --- a/serlib/ser_univ.ml +++ /dev/null @@ -1,102 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* univ_constraint -val sexp_of_univ_constraint : univ_constraint -> Sexp.t - -module Constraints : SerType.SJHC with type t = Univ.Constraints.t - -module ContextSet : SerType.SJHC with type t = Univ.ContextSet.t - -type 'a in_universe_context_set = 'a Univ.in_universe_context_set -val in_universe_context_set_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a in_universe_context_set -val sexp_of_in_universe_context_set : ('a -> Sexp.t) -> 'a in_universe_context_set -> Sexp.t diff --git a/serlib/ser_univNames.ml b/serlib/ser_univNames.ml deleted file mode 100644 index 21b0683f..00000000 --- a/serlib/ser_univNames.ml +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* |= _instance_get) -let to_yojson level = _t_to_yojson (_instance_put level) - -let hash i = hash__t (Instance (UVars.Instance.to_array i)) -let hash_fold_t st i = hash_fold__t st (Instance (UVars.Instance.to_array i)) -let compare i1 i2 = compare__t (Instance (UVars.Instance.to_array i1)) (Instance (UVars.Instance.to_array i2)) - -end - -module UContext = struct - - module I = struct - type t = UVars.UContext.t - type _t = (Names.Name.t array * Names.Name.t array) * (Instance.t * Constraints.t) - [@@deriving sexp,yojson,hash,compare] - - let to_t (un, cs) = UVars.UContext.make un cs - let of_t uc = UVars.UContext.(names uc, (instance uc, constraints uc)) - end - - include SerType.Biject(I) - -end - -module AbstractContext = struct - - let hash_fold_array = hash_fold_array_frozen - module ACPierceDef = struct - - type t = UVars.AbstractContext.t - type _t = (Names.Name.t array * Names.Name.t array) * Constraints.t - [@@deriving sexp,yojson,hash,compare] - end - - include SerType.Pierce(ACPierceDef) - -end - -type 'a in_universe_context = - [%import: 'a UVars.in_universe_context] - [@@deriving sexp] - -type 'a puniverses = - [%import: 'a UVars.puniverses] - [@@deriving sexp, yojson, hash, compare] diff --git a/serlib/ser_uvars.mli b/serlib/ser_uvars.mli deleted file mode 100644 index c17f2fbb..00000000 --- a/serlib/ser_uvars.mli +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t -> 'a in_universe_context -val sexp_of_in_universe_context : ('a -> Sexp.t) -> 'a in_universe_context -> Sexp.t - -type 'a puniverses = 'a * Instance.t - [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml deleted file mode 100644 index fe0a76e9..00000000 --- a/serlib/ser_vernacexpr.ml +++ /dev/null @@ -1,353 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Sexp.t -val opaque_of_sexp : typ:string -> Sexp.t -> 'a - -val opaque_of_yojson : typ:string -> Yojson.Safe.t -> ('a, string) Result.t -val opaque_to_yojson : typ:string -> 'a -> Yojson.Safe.t - -val hash_opaque : typ:string -> 'a -> Ppx_hash_lib.Std.Hash.hash_value -val hash_fold_opaque : typ:string -> Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state - -val compare_opaque : typ:string -> 'a -> 'a -> int diff --git a/serlib/serlib_init.ml b/serlib/serlib_init.ml deleted file mode 100644 index d80ff40a..00000000 --- a/serlib/serlib_init.ml +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unit - diff --git a/serlib_extra/dune b/serlib_extra/dune new file mode 100644 index 00000000..b0bf3b04 --- /dev/null +++ b/serlib_extra/dune @@ -0,0 +1,7 @@ +(library + (name serlib_extra) + (public_name coq-serapi.serlib_extra) + (synopsis "Serialization Library for Coq (Extra / Deprecated)") + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson)) + (libraries coq-core.stm sexplib coq-lsp.serlib)) + diff --git a/serlib/ser_coqargs.ml b/serlib_extra/ser_coqargs.ml similarity index 97% rename from serlib/ser_coqargs.ml rename to serlib_extra/ser_coqargs.ml index 8d933eae..bebfadb7 100644 --- a/serlib/ser_coqargs.ml +++ b/serlib_extra/ser_coqargs.ml @@ -18,12 +18,13 @@ open Sexplib.Std +open Serlib module Names = Ser_names module Lib = Ser_lib type top = [%import: Coqargs.top] - [@@deriving sexp,yojson] + [@@deriving sexp] type require_injection = [%import: Coqargs.require_injection] diff --git a/serlib/ser_stm.ml b/serlib_extra/ser_stm.ml similarity index 89% rename from serlib/ser_stm.ml rename to serlib_extra/ser_stm.ml index 5f481359..ba9d500a 100644 --- a/serlib/ser_stm.ml +++ b/serlib_extra/ser_stm.ml @@ -16,13 +16,10 @@ (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) +open Serlib module Stateid = Ser_stateid module Names = Ser_names -(* type interactive_top = - * [%import: Stm.interactive_top] - * [@@deriving sexp] *) - type focus = [%import: Stm.focus] [@@deriving sexp] @@ -30,6 +27,3 @@ type focus = type add_focus = [%import: Stm.add_focus] [@@deriving sexp] - - (* { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } *) - diff --git a/serapi/ser_stream.ml b/serlib_extra/ser_stm.mli similarity index 93% rename from serapi/ser_stream.ml rename to serlib_extra/ser_stm.mli index 16b091b5..571cc885 100644 --- a/serapi/ser_stream.ml +++ b/serlib_extra/ser_stm.mli @@ -16,5 +16,5 @@ (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) -let of_string = Gramlib.Stream.of_string -let of_channel = Gramlib.Stream.of_channel +type focus = Stm.focus [@@deriving sexp] +type add_focus = Stm.add_focus [@@deriving sexp] diff --git a/serlib/ser_xml_datatype.ml b/serlib_extra/ser_xml_datatype.ml similarity index 100% rename from serlib/ser_xml_datatype.ml rename to serlib_extra/ser_xml_datatype.ml diff --git a/serlib/ser_xml_datatype.mli b/serlib_extra/ser_xml_datatype.mli similarity index 100% rename from serlib/ser_xml_datatype.mli rename to serlib_extra/ser_xml_datatype.mli diff --git a/sertop/dune b/sertop/dune index 1ee2dc9b..7a9e3f84 100644 --- a/sertop/dune +++ b/sertop/dune @@ -3,7 +3,7 @@ (public_name coq-serapi.sertop_v8_12) (modules :standard \ sertop_bin sercomp sertok sername) (preprocess (staged_pps ppx_import ppx_sexp_conv)) - (libraries findlib.dynload cmdliner serapi serlib serlib_ltac)) + (libraries findlib.dynload cmdliner serapi coq-lsp.serlib coq-lsp.serlib.ltac serlib_extra)) (executables (public_names sertop sercomp sertok sername) diff --git a/sertop/sercomp.ml b/sertop/sercomp.ml index befb8ac9..cfdf8bae 100644 --- a/sertop/sercomp.ml +++ b/sertop/sercomp.ml @@ -24,7 +24,7 @@ let input_doc ~input ~in_file ~in_chan ~process ~doc ~sid = match input with | I_vernac -> begin - let in_strm = Serapi.Ser_stream.of_channel in_chan in + let in_strm = Gramlib.Stream.of_channel in_chan in let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in try while true do let doc, sid = !stt in diff --git a/sertop/sername.ml b/sertop/sername.ml index ee9c32f2..54928234 100644 --- a/sertop/sername.ml +++ b/sertop/sername.ml @@ -74,7 +74,7 @@ let sername_doc = "sername Coq tool" (* EJGA: XXX process as regular require at create doc time... *) let do_require ~doc ~sid ~require_lib ~in_file = let sent = Printf.sprintf "Require %s." require_lib in - let in_strm = Serapi.Ser_stream.of_string sent in + let in_strm = Gramlib.Stream.of_string sent in let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry sid in_pa with | Some ast -> diff --git a/sertop/sertok.ml b/sertop/sertok.ml index da5818d3..1eb08a75 100644 --- a/sertop/sertok.ml +++ b/sertop/sertok.ml @@ -46,7 +46,7 @@ exception End_of_input let input_doc ~pp ~in_file ~in_chan ~doc ~sid = let open Format in let stt = ref (doc, sid) in - let in_strm = Serapi.Ser_stream.of_channel in_chan in + let in_strm = Gramlib.Stream.of_channel in_chan in let source = Loc.InFile { dirpath = None; file = in_file } in let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial source) in_strm in let in_bytes = load_file in_file in @@ -65,7 +65,7 @@ let input_doc ~pp ~in_file ~in_chan ~doc ~sid = Bytes.sub_string in_bytes begin_char (end_char - begin_char) in let l_post_st = CLexer.Lexer.State.get () in - let sstr = Serapi.Ser_stream.of_string istr in + let sstr = Gramlib.Stream.of_string istr in try CLexer.Lexer.State.set l_pre_st; let lex = CLexer.Lexer.tok_func sstr in diff --git a/sertop/sertop_loader.ml b/sertop/sertop_loader.ml index 8e605c98..ced1e0e4 100644 --- a/sertop/sertop_loader.ml +++ b/sertop/sertop_loader.ml @@ -47,7 +47,7 @@ let map_serlib fl_pkg = if supported then let plugin_name = String.split_on_char '.' fl_pkg |> list_last in - Some ("coq-serapi.serlib." ^ plugin_name) + Some ("coq-lsp.serlib." ^ plugin_name) else None let plugin_handler user_handler = diff --git a/sertop/sertop_ser.ml b/sertop/sertop_ser.ml index 58971d6e..4a4bc783 100644 --- a/sertop/sertop_ser.ml +++ b/sertop/sertop_ser.ml @@ -80,7 +80,6 @@ module Pp = Ser_pp module Names = Ser_names module Environ = Ser_environ module Goptions = Ser_goptions -module Coqargs = Ser_coqargs module Stateid = Ser_stateid module Evar = Ser_evar module Context = Ser_context @@ -102,8 +101,8 @@ module Printer = Ser_printer module Profile_tactic = Ser_profile_tactic (* Alias fails due to the [@@default in protocol] *) -(* module Stm = Ser_stm *) -module Ser_stm = Ser_stm +module Ser_stm = Serlib_extra.Ser_stm +module Coqargs = Serlib_extra.Ser_coqargs module Ltac_plugin = struct module Tacenv = Serlib_ltac.Ser_tacenv diff --git a/tests/genarg/dune b/tests/genarg/dune index f3326f1a..bf948241 100644 --- a/tests/genarg/dune +++ b/tests/genarg/dune @@ -3,14 +3,16 @@ (targets test_roundtrip) (deps (:input test_roundtrip.in) - (package coq-serapi)) + ; For the plugins to be built, it'd be greater if we could only + ; specify a few libs, but that's still not possible in Dune. + (package coq-lsp)) (action (progn (copy test_roundtrip.in test_roundtrip) (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 "for i in ../../sertop/sercomp.exe ../../serlib/plugins/*/*.cmxs; do echo \"# $(md5sum $i)\"; done >> test_roundtrip")))) + (bash "for i in ../../sertop/sercomp.exe ../../vendor/coq-lsp/serlib/plugins/*/*.cmxs; do echo \"# $(md5sum $i)\"; done >> test_roundtrip")))) (rule (alias runtest) diff --git a/tests/quick/dune b/tests/quick/dune index d8f1962e..a2fde69d 100644 --- a/tests/quick/dune +++ b/tests/quick/dune @@ -1,23 +1,31 @@ (rule (alias runtest) - (deps (:input ab.v)) + (deps + (package coq-lsp) + (:input ab.v)) (action (ignore-outputs (bash "%{bin:sercomp} --quick %{input}")))) (rule (alias runtest) - (deps (:input assoc.v)) + (deps + (package coq-lsp) + (:input assoc.v)) (action (ignore-outputs (bash "%{bin:sercomp} --quick %{input}")))) (rule (alias runtest) - (deps (:input ordered.v)) + (deps + (package coq-lsp) + (:input ordered.v)) (action (ignore-outputs (bash "%{bin:sercomp} --quick %{input}")))) (rule (alias runtest) - (deps (:input reserved.v)) + (deps + (package coq-lsp) + (:input reserved.v)) (action (ignore-outputs (bash "%{bin:sercomp} --quick %{input}")))) diff --git a/tests/sername/dune b/tests/sername/dune index 48b5e897..d445410a 100644 --- a/tests/sername/dune +++ b/tests/sername/dune @@ -1,4 +1,5 @@ (rule + (deps (package coq-lsp)) (action (with-stdout-to nat_add.log (run sername --de-bruijn --str-pp %{dep:nat_add.sername})))) diff --git a/vendor/coq-lsp b/vendor/coq-lsp new file mode 160000 index 00000000..46342ed5 --- /dev/null +++ b/vendor/coq-lsp @@ -0,0 +1 @@ +Subproject commit 46342ed520d275f591e672a755341ec735ffa80b