aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/summary.ml
blob: 9b229459196abccf3e4348e004682df4c51d508a (plain)
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
(************************************************************************)
(*         *   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)         *)
(************************************************************************)

open Pp
open CErrors
open Util

module Dyn = Dyn.Make ()

type marshallable = [ `Yes | `No | `Shallow ]

type 'a summary_declaration = {
  freeze_function : marshallable -> 'a;
  unfreeze_function : 'a -> unit;
  init_function : unit -> unit }

let sum_mod = ref None
let sum_map = ref String.Map.empty

let mangle id = id ^ "-SUMMARY"
let unmangle id = String.(sub id 0 (length id - 8))

let ml_modules = "ML-MODULES"

let internal_declare_summary fadd sumname sdecl =
  let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
  let dyn_freeze b = infun (sdecl.freeze_function b)
  and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
  and dyn_init = sdecl.init_function in
  let ddecl = {
    freeze_function = dyn_freeze;
    unfreeze_function = dyn_unfreeze;
    init_function = dyn_init }
  in
  fadd sumname ddecl;
  tag

let declare_ml_modules_summary decl =
  let ml_add _ ddecl = sum_mod := Some ddecl in
  internal_declare_summary ml_add ml_modules decl

let declare_ml_modules_summary decl =
  ignore(declare_ml_modules_summary decl)

let declare_summary_tag sumname decl =
  let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
  let () = if String.Map.mem sumname !sum_map then
      anomaly ~label:"Summary.declare_summary"
        (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
  in
  internal_declare_summary fadd sumname decl

let declare_summary sumname decl =
  ignore(declare_summary_tag sumname decl)

type frozen = {
  summaries : Dyn.t String.Map.t;
  (** Ordered list w.r.t. the first component. *)
  ml_module : Dyn.t option;
  (** Special handling of the ml_module summary. *)
}

let empty_frozen = { summaries = String.Map.empty; ml_module = None }

let freeze_summaries ~marshallable : frozen =
  let smap decl = decl.freeze_function marshallable in
  { summaries = String.Map.map smap !sum_map;
    ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
  }

let warn_summary_out_of_scope =
  let name = "summary-out-of-scope" in
  let category = "dev" in
  let default = CWarnings.Disabled in
  CWarnings.create ~name ~category ~default (fun name ->
    Pp.str (Printf.sprintf
      "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
      name)
    )

let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
  (* The unfreezing of [ml_modules_summary] has to be anticipated since it
   * may modify the content of [summaries] by loading new ML modules *)
  begin match !sum_mod with
  | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
  | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
  end;
  (** We must be independent on the order of the map! *)
  let ufz name decl =
    try decl.unfreeze_function String.Map.(find name summaries)
    with Not_found ->
      if not partial then begin
        warn_summary_out_of_scope name;
        decl.init_function ()
      end;
  in
  (* String.Map.iter unfreeze_single !sum_map *)
  String.Map.iter ufz !sum_map

let init_summaries () =
  String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map

(** For global tables registered statically before the end of coqtop
    launch, the following empty [init_function] could be used. *)

let nop () = ()

(** Summary projection *)
let project_from_summary { summaries } tag =
  let id = unmangle (Dyn.repr tag) in
  let state = String.Map.find id summaries in
  Option.get (Dyn.Easy.prj state tag)

let modify_summary st tag v =
  let id = unmangle (Dyn.repr tag) in
  let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
  {st with summaries}

let remove_from_summary st tag =
  let id = unmangle (Dyn.repr tag) in
  let summaries = String.Map.remove id st.summaries in
  {st with summaries}

(** All-in-one reference declaration + registration *)

let ref_tag ?(freeze=fun _ r -> r) ~name x =
  let r = ref x in
  let tag = declare_summary_tag name
    { freeze_function = (fun b -> freeze b !r);
      unfreeze_function = ((:=) r);
      init_function = (fun () -> r := x) } in
  r, tag

let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x

module Local = struct

type 'a local_ref = ('a CEphemeron.key * string) ref

let (:=) r v = r := (CEphemeron.create v, snd !r)

let (!) r =
  let key, name = !r in
  try CEphemeron.get key
  with CEphemeron.InvalidKey ->
    let { init_function } = String.Map.find name !sum_map in
    init_function ();
    CEphemeron.get (fst !r)

let ref ?(freeze=fun x -> x) ~name init =
  let r = Pervasives.ref (CEphemeron.create init, name) in
  declare_summary name
    { freeze_function = (fun _ -> freeze !r);
      unfreeze_function = ((:=) r);
      init_function = (fun () -> r := init) };
  r

end

let dump = Dyn.dump