[sertop] Add sername program for serialization of terms

.travis.yml

@@ -31,9 +31,9 @@ env:
   - COMPILER="4.07.1"
   # Main test suites
   matrix:
-  - TEST_TARGET="build"   COMPILER="4.07.1"       EXTRA_OPAM="coq"
-  - TEST_TARGET="test"    COMPILER="4.07.1"       EXTRA_OPAM="coq coq-mathcomp-ssreflect"
-  - TEST_TARGET="js-dune" COMPILER="4.07.1+32bit" EXTRA_OPAM="coq js_of_ocaml js_of_ocaml-lwt"
+  - TEST_TARGET="build"   COMPILER="4.07.1"       EXTRA_OPAM="coq.8.10.2"
+  - TEST_TARGET="test"    COMPILER="4.07.1"       EXTRA_OPAM="coq.8.10.2 coq-mathcomp-ssreflect"
+  - TEST_TARGET="js-dune" COMPILER="4.07.1+32bit" EXTRA_OPAM="coq.8.10.2 js_of_ocaml js_of_ocaml-lwt"
   # Don't test opam in 8.10 [yet]
   - TEST_TARGET="test"    SERAPI_COQ_HOME="$HOME/coq-$COQ_VERSION/_build/install/default/lib/"
 

CHANGES.md

@@ -1,3 +1,13 @@
+## Version 0.7.1:
+
+ * [sertop ] Add `sername` program for batch serialization elaborated terms
+             Note that this utility will be deprecated in future versions,
+             to be subsumed by `Query`.
+             (#207, @palmskog, with help from @ejgallego)
+ * [serlib ] Expose `QueryUtil.info_of_id` and `gen_pp_obj` in `serapi_protocol.mli` to enable
+             using them in `sername` to retrieve serialized body-type pairs (@palmskog)
+ * [serlib ] Only use `ssreflect` from Coq in tests (@ejgallego)
+
 ## Version 0.7.0:
 
  * [general] (!) support Coq 8.10,

coq-serapi.opam

@@ -28,7 +28,7 @@ depends: [
   "cmdliner"            {           >= "1.0.0"             }
   "ocamlfind"           {           >= "1.8.0"             }
   "sexplib"             {           >= "v0.11.0"           }
-  "dune"                {           >= "1.2.0"             }
+  "dune"                {           >= "1.4.0"             }
   "ppx_import"          { build   & >= "1.5-3"             }
   "ppx_deriving"        {           >= "4.2.1"             }
   "ppx_sexp_conv"       {           >= "v0.11.0"           }

dune-project

@@ -1,4 +1,4 @@
-(lang dune 1.2)
+(lang dune 1.4)
 (using fmt 1.0)
 (name coq-serapi)
 

serapi/serapi_protocol.ml

@@ -385,7 +385,7 @@ type query_opt =
     pp    : format_opt [@default { pp_format = PpSer; pp_depth = 0; pp_elide = "..."; pp_margin = 72 } ];
     (* Legacy/Deprecated *)
     route : Feedback.route_id [@default 0];
-  }
+  } [@@ocaml.warning "-3"]
 
 (** XXX: This should be in sync with the object tag!  *)
 type query_cmd =
@@ -656,14 +656,14 @@ let coq_protect e =
     (* Richpp.richpp_of_pp msg *)
 
 type parse_opt =
-  { ontop  : Stateid.t sexp_option }
+  { ontop  : Stateid.t sexp_option } [@@ocaml.warning "-3"]
 
 type add_opts = {
   lim    : int       sexp_option;
   ontop  : Stateid.t sexp_option;
   newtip : Stateid.t sexp_option;
   verb   : bool      [@default false];
-}
+} [@@ocaml.warning "-3"]
 
 module ControlUtil = struct
 
@@ -773,7 +773,7 @@ type newdoc_opts =
   ; iload_path   : Mltop.coq_path list sexp_option
   (* Libs to require in STM init *)
   ; require_libs : (string * string option * bool option) list sexp_option
-  }
+  } [@@ocaml.warning "-3"]
 
 (******************************************************************************)
 (* Help                                                                       *)

serapi/serapi_protocol.mli

@@ -268,6 +268,8 @@ type print_opt =
     (** Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form. *)
   }
 
+val gen_pp_obj : Environ.env -> Evd.evar_map -> coq_object -> Pp.t
+
 (******************************************************************************)
 (* Parsing Sub-Protocol                                                       *)
 (******************************************************************************)
@@ -298,7 +300,7 @@ type query_opt =
     (** Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form. *)
     route : Feedback.route_id [@default 0];
     (** Legacy/Deprecated STM query method *)
-  }
+  } [@@ocaml.warning "-3"]
 
 (** Query commands are mostly a tag and some arguments determining the result type.
 
@@ -348,6 +350,10 @@ type query_cmd =
   | Complete of string
   (** Naïve but efficient prefix-based completion of identifiers *)
 
+module QueryUtil : sig
+  val info_of_id : Environ.env -> string -> coq_object list * coq_object list
+end
+
 (******************************************************************************)
 (* Control Sub-Protocol                                                       *)
 (******************************************************************************)
@@ -359,8 +365,7 @@ type query_cmd =
 type parse_opt =
   { ontop  : Stateid.t sexp_option
   (** parse [ontop] of the given sentence *)
-  }
-
+  } [@@ocaml.warning "-3"]
 
 (** [Add] will take a string and parse all the sentences on it, until an error of the end is found.
     Options for [Add] are: *)
@@ -373,7 +378,7 @@ type add_opts = {
   (** Make [newtip] the new sentence id, very useful to avoid synchronous operations *)
   verb   : bool      [@default false];
   (** [verb] internal Coq parameter, be verbose on parsing *)
-}
+} [@@ocaml.warning "-3"]
 
 (******************************************************************************)
 (* Init / new document                                                        *)
@@ -389,7 +394,7 @@ type newdoc_opts =
   (** Initial LoadPath for the document *) (* [XXX: Use the coq_pkg record?] *)
   ; require_libs : (string * string option * bool option) list sexp_option
   (** Libraries to load in the initial document state *)
-  }
+  } [@@ocaml.warning "-3"]
 
 (******************************************************************************)
 (* Help                                                                       *)

sertop/dune

@@ -1,14 +1,14 @@
 (library
  (name sertoplib)
  (public_name coq-serapi.sertop_v8_10)
- (modules :standard \ sertop sercomp sertok sertop_js sertop_async)
+ (modules :standard \ sertop sercomp sertok sername sertop_js sertop_async)
  (wrapped false)
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries findlib.dynload cmdliner serapi serlib serlib_ltac))
 
 (executables
- (public_names sertop sercomp sertok)
- (modules sertop sercomp sertok)
+ (public_names sertop sercomp sertok sername)
+ (modules sertop sercomp sertok sername)
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (link_flags -linkall)
  (libraries sertoplib num))

sertop/sername.ml

@@ -0,0 +1,211 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq serialization API/Plugin                                         *)
+(* Written by: Karl Palmskog                                            *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+let fatal_exn exn info =
+  let loc = Loc.get_loc info in
+  let msg = Pp.(pr_opt_no_spc Topfmt.pr_loc loc ++ fnl ()
+                ++ CErrors.iprint (exn, info)) in
+  Format.eprintf "Error: @[%a@]@\n%!" Pp.pp_with msg;
+  exit 1
+
+let create_document ~require_lib ~in_file ~async ~async_workers ~quick ~iload_path ~debug =
+
+  let open Sertop_init in
+
+  (* coq initialization *)
+  coq_init
+    { fb_handler = (fun _ -> ())  (* XXXX *)
+    ; ml_load    = None
+    ; debug
+    };
+
+  (* document initialization *)
+
+  let stm_options = process_stm_flags
+      { enable_async  = async
+      ; deep_edits    = false
+      ; async_workers = async_workers
+      } in
+
+  (* Disable due to https://github.com/ejgallego/coq-serapi/pull/94 *)
+  let stm_options =
+    { stm_options with
+      async_proofs_tac_error_resilience = `None
+    ; async_proofs_cmd_error_resilience = false
+    } in
+
+  let stm_options =
+    if quick
+    then { stm_options with async_proofs_mode = APonLazy }
+    else stm_options
+  in
+
+  (*
+  let require_libs =
+    let prelude = ["Coq.Init.Prelude", None, Some false] in
+    match require_lib with
+    | Some l -> prelude @ [l, None, Some false]
+    | None -> prelude
+  in
+  *)
+  let require_libs = ["Coq.Init.Prelude", None, Some false] in
+
+  let ndoc = { Stm.doc_type = Stm.VoDoc in_file
+             ; require_libs
+             ; iload_path
+             ; stm_options
+             } in
+
+  (* Workaround, see
+     https://github.com/ejgallego/coq-serapi/pull/101 *)
+  if quick || async <> None
+  then Safe_typing.allow_delayed_constants := true;
+
+  match require_lib with
+  | None -> Stm.new_doc ndoc
+  | Some l ->
+     (*
+     let sdoc = Stm.new_doc ndoc in
+     let dir,from,exp = l,None,Some false in
+     let mp = Libnames.qualid_of_string dir in
+     let mfrom = Option.map Libnames.qualid_of_string from in
+     Flags.silently (Vernacentries.vernac_require mfrom exp) [mp];
+     sdoc
+     *)
+     let doc,sid = Stm.new_doc ndoc in
+     let sent = Printf.sprintf "Require %s." l in
+     let in_strm = Stream.of_string sent in
+     let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile in_file)) in_strm in
+     match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry sid in_pa with
+     | Some ast ->
+	let doc, sid, tip = Stm.add ~doc ~ontop:sid false ast in
+	if tip <> `NewTip then CErrors.user_err ?loc:ast.loc Pp.(str "fatal, got no `NewTip`");
+	doc, sid
+     | None -> assert false
+
+exception End_of_input
+
+let input_doc ~in_chan ~process ~doc ~sid =
+  try while true; do
+      let line = input_line in_chan in
+      if String.trim line <> "" then process ~doc ~sid line
+    done
+  with End_of_file -> ()
+
+let context_of_st m = match m with
+  | `Valid (Some { Vernacstate.proof = Some pstate; _ } ) ->
+    Pfedit.get_current_context pstate
+  | _ ->
+    let env = Global.env () in Evd.from_env env, env
+
+let str_pp_obj env sigma fmt (obj : Serapi_protocol.coq_object) : unit =
+  Format.fprintf fmt "%a" Pp.pp_with (Serapi_protocol.gen_pp_obj env sigma obj)
+
+let process_line ~pp ~str_pp ~de_bruijn ~body ~doc ~sid line =
+  let open Serapi_protocol in
+  let st = Stm.state_of_id ~doc sid in
+  let sigma, env = context_of_st st in
+  let info = QueryUtil.info_of_id env line in
+  let def = if body then fst info else snd info in
+  match def with
+  | [CoqConstr def_term] ->
+     let evd = Evd.from_env env in
+     let edef_term = EConstr.of_constr def_term in
+     let gdef_term = Detyping.detype Detyping.Now false Names.Id.Set.empty env evd edef_term in
+     Format.pp_set_margin Format.std_formatter 100000;
+     Format.printf "%s: %!" line;
+     if str_pp then Format.fprintf Format.std_formatter "\"@[%a@]\" %!" (str_pp_obj env sigma) (CoqConstr def_term);
+     if de_bruijn then Format.printf "@[%a@] %!" pp (Serlib.Ser_constr.sexp_of_constr def_term);
+     Format.printf "@[%a@]@\n%!" pp (Serlib.Ser_glob_term.sexp_of_glob_constr gdef_term)
+  | _ -> ()
+
+let check_pending_proofs ~pstate =
+  Option.iter (fun pstate ->
+  let pfs = Proof_global.get_all_proof_names pstate in
+  if not CList.(is_empty pfs) then
+    let msg = let open Pp in
+      seq [ str "There are pending proofs: "
+          ; pfs |> List.rev |> prlist_with_sep pr_comma Names.Id.print; str "."] in
+    CErrors.user_err msg
+  ) pstate
+
+let close_document ~doc ~pstate =
+  let _doc = Stm.join ~doc in
+  check_pending_proofs ~pstate
+
+let sername_version = Ser_version.ser_git_version
+
+let sername_man =
+  [
+    `S "DESCRIPTION";
+    `P "Experimental Coq name serializer.";
+    `S "USAGE";
+    `P "To serialize names listed in `names.txt` in module `Funs.mod`:";
+    `Pre "sername -Q fs,Funs --require-lib=Funs.mod names.txt";
+    `P "See the documentation on the project's webpage for more information."
+  ]
+
+let sername_doc = "sername Coq tool"
+
+open Cmdliner
+
+let driver debug printer async async_workers quick coq_path ml_path load_path rload_path require_lib str_pp de_bruijn body in_file omit_loc omit_att exn_on_opaque =
+
+  (* closures *)
+  let pp = Sertop_ser.select_printer printer in
+  let process = process_line ~pp ~str_pp ~de_bruijn ~body in
+
+  (* initialization *)
+  let options = Serlib.Serlib_init.{ omit_loc; omit_att; exn_on_opaque } in
+  Serlib.Serlib_init.init ~options;
+
+  let iload_path = Serapi_paths.coq_loadpath_default ~implicit:true ~coq_path @ ml_path @ load_path @ rload_path in
+  let doc, sid = create_document ~require_lib ~in_file:"file.v" ~async ~async_workers ~quick ~iload_path ~debug in
+
+  (* main loop *)
+  let in_chan = open_in in_file in
+  let () = input_doc ~in_chan ~process ~doc ~sid in (* XX *)
+  let pstate = match Stm.state_of_id ~doc sid with
+    | `Valid (Some { Vernacstate.proof; _ }) -> proof
+    | _ -> None
+  in
+  let () = close_document ~doc ~pstate in
+  ()
+
+let main () =
+  let input_file =
+    let doc = "Input file." in
+    Arg.(required & pos 0 (some string) None & info [] ~docv:("FILE") ~doc)
+  in
+
+  let sername_cmd =
+    let open Sertop_arg in
+    Term.(const driver
+          $ debug $ printer $ async $ async_workers $ quick $ prelude
+          $ ml_include_path $ load_path $ rload_path $ require_lib $ str_pp $ de_bruijn $ body $ input_file $ omit_loc $ omit_att $ exn_on_opaque
+         ),
+    Term.info "sername" ~version:sername_version ~doc:sername_doc ~man:sername_man
+  in
+
+  try match Term.eval ~catch:false sername_cmd with
+    | `Error _ -> exit 1
+    | _        -> exit 0
+  with exn ->
+    let (e, info) = CErrors.push exn in
+    fatal_exn e info
+
+let _ = main ()

sertop/sertop_arg.ml

@@ -23,6 +23,22 @@ let prelude =
   let doc = "Load Coq.Init.Prelude from $(docv); plugins/ and theories/ should live there." in
   Arg.(value & opt string Coq_config.coqlib & info ["coqlib"] ~docv:"COQPATH" ~doc)
 
+let require_lib =
+  let doc = "Coq module to require." in
+  Arg.(value & opt (some string) None & info ["require-lib"] ~doc)
+
+let str_pp =
+  let doc = "Pretty-print constr strings." in
+  Arg.(value & flag & info ["str-pp"] ~doc)
+
+let de_bruijn =
+  let doc = "Print constrs with de Bruijn indices." in
+  Arg.(value & flag & info ["de-bruijn"] ~doc)
+
+let body =
+  let doc = "Print bodies of constrs." in
+  Arg.(value & flag & info ["body"] ~doc)
+
 let async =
   let doc = "Enable async support using Coq binary $(docv) (experimental)." in
   Arg.(value & opt (some string) None & info ["async"] ~doc ~docv:"COQTOP")

sertop/sertop_arg.mli

@@ -19,6 +19,10 @@
 open Cmdliner
 
 val prelude         : string Term.t
+val require_lib     : string option Term.t
+val str_pp          : bool Term.t
+val de_bruijn       : bool Term.t
+val body            : bool Term.t
 val async           : string option Term.t
 val quick           : bool Term.t
 val async_full      : bool Term.t