← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to library/libobject.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
library/libobject.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: libobject.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
10
 
 
11
(*i*)
 
12
open Names
 
13
open Libnames
 
14
open Mod_subst
 
15
(*i*)
 
16
 
 
17
(* [Libobject] declares persistent objects, given with methods:
 
18
 
 
19
   * a caching function specifying how to add the object in the current
 
20
     scope;
 
21
     If the object wishes to register its visibility in the Nametab, 
 
22
     it should do so for all possible sufixes.
 
23
 
 
24
   * a loading function, specifying what to do when the module 
 
25
     containing the object is loaded; 
 
26
     If the object wishes to register its visibility in the Nametab, 
 
27
     it should do so for all sufixes no shorter then the "int" argument
 
28
 
 
29
   * an opening function, specifying what to do when the module 
 
30
     containing the object is opened (imported);
 
31
     If the object wishes to register its visibility in the Nametab, 
 
32
     it should do so for the sufix of the length the "int" argument
 
33
 
 
34
   * a classification function, specyfying what to do with the object,
 
35
     when the current module (containing the object) is ended;
 
36
     The possibilities are:
 
37
     Dispose   - the object dies at the end of the module
 
38
     Substitue - meaning the object is substitutive and 
 
39
                 the module name must be updated
 
40
     Keep      - the object is not substitutive, but survives module 
 
41
                 closing
 
42
     Anticipate - this is for objects which have to be explicitely 
 
43
                 managed by the [end_module] function (like Require 
 
44
                 and Read markers)
 
45
 
 
46
     The classification function is also an occasion for a cleanup
 
47
     (if this function returns Keep or Substitute of some object, the 
 
48
     cache method is never called for it)
 
49
 
 
50
   * a substitution function, performing the substitution; 
 
51
     this function should be declared for substitutive objects 
 
52
     only (see obove)
 
53
 
 
54
   * a discharge function, that is applied at section closing time to
 
55
     collect the data necessary to rebuild the discharged form of the
 
56
     non volatile objects
 
57
 
 
58
   * a rebuild function, that is applied after section closing to
 
59
     rebuild the non volatile content of a section from the data
 
60
     collected by the discharge function
 
61
 
 
62
   * an export function, to enable optional writing of its contents 
 
63
     to disk (.vo). This function is also the oportunity to remove 
 
64
     redundant information in order to keep .vo size small 
 
65
 
 
66
     The export function is a little obsolete and will be removed 
 
67
     in the near future... 
 
68
 
 
69
*)
 
70
 
 
71
type 'a substitutivity = 
 
72
    Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
73
 
 
74
type 'a object_declaration = {
 
75
  object_name : string;
 
76
  cache_function : object_name * 'a -> unit;
 
77
  load_function : int -> object_name * 'a -> unit;
 
78
  open_function : int -> object_name * 'a -> unit;
 
79
  classify_function : object_name * 'a -> 'a substitutivity;
 
80
  subst_function : object_name * substitution * 'a -> 'a;
 
81
  discharge_function : object_name * 'a -> 'a option;
 
82
  rebuild_function : 'a -> 'a;
 
83
  export_function : 'a -> 'a option }
 
84
 
 
85
(* The default object is a "Keep" object with empty methods. 
 
86
   Object creators are advised to use the construction
 
87
   [{(default_object "MY_OBJECT") with
 
88
      cache_function = ...
 
89
   }]
 
90
   and specify only these functions which are not empty/meaningless
 
91
 
 
92
*)
 
93
 
 
94
val default_object : string -> 'a object_declaration
 
95
 
 
96
(* the identity substitution function *)
 
97
val ident_subst_function : object_name * substitution * 'a -> 'a
 
98
 
 
99
(*s Given an object declaration, the function [declare_object]
 
100
   will hand back two functions, the "injection" and "projection"
 
101
   functions for dynamically typed library-objects. *)
 
102
 
 
103
type obj
 
104
 
 
105
val declare_object : 
 
106
  'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
107
 
 
108
val object_tag : obj -> string
 
109
 
 
110
val cache_object : object_name * obj -> unit
 
111
val load_object : int -> object_name * obj -> unit
 
112
val open_object : int -> object_name * obj -> unit
 
113
val subst_object : object_name * substitution * obj -> obj
 
114
val classify_object : object_name * obj -> obj substitutivity
 
115
val export_object : obj -> obj option
 
116
val discharge_object : object_name * obj -> obj option
 
117
val rebuild_object : obj -> obj
 
118
val relax : bool -> unit