package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

Maintainers

E

e@x80.org

Sources

coq-serapi-8.18.0.0.18.1.tbz

sha256=3958ec27603e3f927a74f11d02d98390e8ecda942bb23f37ff6fa575b31a8158

sha512=d33f9340de6e1426a42192da3610a7636b0201baa166cf788926b866738ae299219439bc22112cc81591c565dd857f66e53a41a3cfe420844f31fb6077abe57b

doc/src/coq-serapi.serapi_v8_14/serapi_pp.ml.html

Source file `serapi_pp.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin                                         *)
(* Copyright 2016 MINES ParisTech                                       *)
(************************************************************************)
(* Status: Very Experimental                                            *)
(************************************************************************)

open Format

(** This module includes all of sertop custom Format-based printers
    for Coq datatypes *)

type 'a pp = formatter -> 'a -> unit

(************************************************************************)
(* Print Helpers                                                        *)
(************************************************************************)

let pp_str fmt str = fprintf fmt "%s" str

let pp_opt pp fmt opt = match opt with
  | None   -> ()
  | Some x -> fprintf fmt "%a" pp x

let rec pp_list ?sep pp fmt l = match l with
    []         -> fprintf fmt ""
  | csx :: []  -> fprintf fmt "@[%a@]" pp csx
  | csx :: csl -> fprintf fmt "@[%a@]%a@;%a" pp csx (pp_opt pp_str) sep (pp_list ?sep pp) csl

(************************************************************************)
(* Statid                                                               *)
(************************************************************************)
let pp_stateid fmt id = fprintf fmt "%d" (Stateid.to_int id)

(************************************************************************)
(* Feedback                                                             *)
(************************************************************************)
let pp_feedback_content fmt fb =
  let open Feedback in
  match fb with
  (* STM mandatory data (must be displayed) *)
  | Processed       -> fprintf fmt "Processed"
  | Incomplete      -> fprintf fmt "Incomplete"
  | Complete        -> fprintf fmt "Complete"

  (* STM optional data *)
  | ProcessingIn s       -> fprintf fmt "ProcessingIn: %s" s
  | InProgress d         -> fprintf fmt "InProgress: %d" d
  | WorkerStatus(w1, w2) -> fprintf fmt "WorkerStatus: %s, %s" w1 w2

  (* Generally useful metadata *)
  | AddedAxiom     -> fprintf fmt "AddedAxiom"

  | GlobRef (_loc, s1, s2, s3, s4) -> fprintf fmt "GlobRef: %s,%s,%s,%s" s1 s2 s3 s4
  | GlobDef (_loc, s1, s2, s3)     -> fprintf fmt "GlobDef: %s,%s,%s"    s1 s2 s3

  | FileDependency (os, s) -> fprintf fmt "FileDep: %a, %s" (pp_opt pp_str) os s
  | FileLoaded (s1, s2)    -> fprintf fmt "FileLoaded: %s, %s" s1 s2

  (* Extra metadata *)
  | Custom(_loc, msg, _xml) -> fprintf fmt "Custom: %s" msg

  (* Old generic messages *)
  | Message(_lvl, _loc, m) -> fprintf fmt "Msg: @[%a@]" Pp.pp_with m

let pp_feedback fmt (fb : Feedback.feedback) =
  let open Feedback in
  fprintf fmt "feedback for [%a]: @[%a@]" pp_stateid fb.span_id pp_feedback_content fb.Feedback.contents

(************************************************************************)
(* Xml                                                                  *)
(************************************************************************)
let pp_attr fmt (xtag, att) =
  fprintf fmt "%s = %s" xtag att

let rec pp_xml fmt (xml : Xml_datatype.xml) = match xml with
  | Xml_datatype.Element (tag, att, more) ->
    fprintf fmt "@[<%s @[%a@]>@,%a@,</%s>@]" tag (pp_list pp_attr) att (pp_list pp_xml) more tag
  | Xml_datatype.PCData str -> fprintf fmt "%s" str