package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file persistent_counter.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
(*
 * This file defines our persistent counter, which we use in the
 * CountPersistent command.
 *)

(*
 * At its core, our persistent counter looks exactly the same as
 * our non-persistent counter (with a different name to prevent collisions):
 *)
let counter = Summary.ref ~name:"persistent_counter" 0

(*
 * The difference is that we need to declare it as a persistent object
 * using Libobject.declare_object. To do that, we define a function that
 * saves the value that is passed to it into the reference we have just defined:
 *)
let cache_count (_, v) =
  counter := v

(*
 * We then use declare_object to create a function that takes an integer value
 * (the type our counter refers to) and creates a persistent object from that
 * value:
 *)
let declare_counter : int -> Libobject.obj =
  let open Libobject in
  declare_object
    {
      (default_object "COUNTER") with
      cache_function = cache_count;
      load_function = (fun _ -> cache_count);
    }
(*
 * See Libobject for more information on what other information you
 * can pass here, and what all of these functions mean.
 *
 * For example, if we passed the same thing that we pass to load_function
 * to open_function, then our last call to Count Persistent in Count.v
 * would return 4 and not 6.
 *)

(*
 * Incrementing our counter looks almost identical:
 *)
let increment () =
  Lib.add_anonymous_leaf (declare_counter (succ !counter))
(*
 * except that we must call our declare_counter function to get a persistent
 * object. We then pass this object to Lib.add_anonymous_leaf.
 *)

(*
 * Reading a value does not change at all:
 *)
let value () =
  !counter
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct