← Back to branch summary

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

« back to all changes in this revision

Viewing changes to library/libobject.ml

  • 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.ml
 
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
(* $Id: libobject.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
 
10
 
 
11
open Util
 
12
open Names
 
13
open Libnames
 
14
open Mod_subst
 
15
 
 
16
(* The relax flag is used to make it possible to load files while ignoring
 
17
   failures to incorporate some objects.  This can be useful when one
 
18
   wants to work with restricted Coq programs that have only parts of
 
19
   the full capabilities, but may still be able to work correctly for
 
20
   limited purposes.  One example is for the graphical interface, that uses
 
21
   such a limite coq process to do only parsing.  It loads .vo files, but
 
22
   is only interested in loading the grammar rule definitions. *)
 
23
 
 
24
let relax_flag = ref false;;
 
25
 
 
26
let relax b = relax_flag := b;;
 
27
 
 
28
type 'a substitutivity = 
 
29
    Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
30
 
 
31
type 'a object_declaration = {
 
32
  object_name : string;
 
33
  cache_function : object_name * 'a -> unit;
 
34
  load_function : int -> object_name * 'a -> unit;
 
35
  open_function : int -> object_name * 'a -> unit;
 
36
  classify_function : object_name * 'a -> 'a substitutivity;
 
37
  subst_function : object_name * substitution * 'a -> 'a;
 
38
  discharge_function : object_name * 'a -> 'a option;
 
39
  rebuild_function : 'a -> 'a;
 
40
  export_function : 'a -> 'a option }
 
41
 
 
42
let yell s = anomaly s
 
43
 
 
44
let default_object s = {
 
45
  object_name = s;
 
46
  cache_function = (fun _ -> ());
 
47
  load_function = (fun _ _ -> ());
 
48
  open_function = (fun _ _ -> ());
 
49
  subst_function = (fun _ -> 
 
50
    yell ("The object "^s^" does not know how to substitute!"));
 
51
  classify_function = (fun (_,obj) -> Keep obj);
 
52
  discharge_function = (fun _ -> None);
 
53
  rebuild_function = (fun x -> x);
 
54
  export_function = (fun _ -> None)} 
 
55
 
 
56
 
 
57
(* The suggested object declaration is the following:
 
58
 
 
59
   declare_object { (default_object "MY OBJECT") with
 
60
       cache_function = fun (sp,a) -> Mytbl.add sp a}
 
61
 
 
62
   and the listed functions are only those which definitions accually 
 
63
   differ from the default.
 
64
 
 
65
   This helps introducing new functions in objects.
 
66
*)
 
67
 
 
68
let ident_subst_function (_,_,a) = a
 
69
 
 
70
type obj = Dyn.t (* persistent dynamic objects *)
 
71
 
 
72
type dynamic_object_declaration = {
 
73
  dyn_cache_function : object_name * obj -> unit;
 
74
  dyn_load_function : int -> object_name * obj -> unit;
 
75
  dyn_open_function : int -> object_name * obj -> unit;
 
76
  dyn_subst_function : object_name * substitution * obj -> obj;
 
77
  dyn_classify_function : object_name * obj -> obj substitutivity;
 
78
  dyn_discharge_function : object_name * obj -> obj option;
 
79
  dyn_rebuild_function : obj -> obj;
 
80
  dyn_export_function : obj -> obj option }
 
81
 
 
82
let object_tag lobj = Dyn.tag lobj
 
83
 
 
84
let cache_tab = 
 
85
  (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
86
 
 
87
let declare_object odecl =
 
88
  let na = odecl.object_name in
 
89
  let (infun,outfun) = Dyn.create na in
 
90
  let cacher (oname,lobj) =
 
91
    if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj)
 
92
    else anomaly "somehow we got the wrong dynamic object in the cachefun"
 
93
  and loader i (oname,lobj) =
 
94
    if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj)
 
95
    else anomaly "somehow we got the wrong dynamic object in the loadfun"
 
96
  and opener i (oname,lobj) =
 
97
    if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
 
98
    else anomaly "somehow we got the wrong dynamic object in the openfun"
 
99
  and substituter (oname,sub,lobj) = 
 
100
    if Dyn.tag lobj = na then 
 
101
      infun (odecl.subst_function (oname,sub,outfun lobj))
 
102
    else anomaly "somehow we got the wrong dynamic object in the substfun"
 
103
  and classifier (spopt,lobj) = 
 
104
    if Dyn.tag lobj = na then 
 
105
      match odecl.classify_function (spopt,outfun lobj) with
 
106
        | Dispose -> Dispose
 
107
        | Substitute obj -> Substitute (infun obj)
 
108
        | Keep obj -> Keep (infun obj)
 
109
        | Anticipate (obj) -> Anticipate (infun obj)
 
110
    else 
 
111
      anomaly "somehow we got the wrong dynamic object in the classifyfun"
 
112
  and discharge (oname,lobj) = 
 
113
    if Dyn.tag lobj = na then 
 
114
      Option.map infun (odecl.discharge_function (oname,outfun lobj))
 
115
    else 
 
116
      anomaly "somehow we got the wrong dynamic object in the dischargefun"
 
117
  and rebuild lobj = 
 
118
    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
 
119
    else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
 
120
  and exporter lobj = 
 
121
    if Dyn.tag lobj = na then 
 
122
      Option.map infun (odecl.export_function (outfun lobj))
 
123
    else 
 
124
      anomaly "somehow we got the wrong dynamic object in the exportfun"
 
125
 
 
126
  in 
 
127
  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 
128
                             dyn_load_function = loader;
 
129
                             dyn_open_function = opener;
 
130
                             dyn_subst_function = substituter;
 
131
                             dyn_classify_function = classifier;
 
132
                             dyn_discharge_function = discharge;
 
133
                             dyn_rebuild_function = rebuild;
 
134
                             dyn_export_function = exporter };
 
135
  (infun,outfun)
 
136
 
 
137
(* this function describes how the cache, load, open, and export functions
 
138
   are triggered.  In relaxed mode, this function just return a meaningless
 
139
   value instead of raising an exception when they fail. *)
 
140
 
 
141
let apply_dyn_fun deflt f lobj =
 
142
  let tag = object_tag lobj in
 
143
    try
 
144
      let dodecl =
 
145
        try
 
146
          Hashtbl.find cache_tab tag
 
147
        with Not_found -> 
 
148
          if !relax_flag then
 
149
            failwith "local to_apply_dyn_fun"
 
150
          else
 
151
            error
 
152
              ("Cannot find library functions for an object with tag "^tag^
 
153
               " (maybe a plugin is missing)") in 
 
154
        f dodecl
 
155
    with
 
156
        Failure "local to_apply_dyn_fun" -> deflt;;
 
157
 
 
158
let cache_object ((_,lobj) as node) =
 
159
  apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
 
160
 
 
161
let load_object i ((_,lobj) as node) = 
 
162
  apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
 
163
 
 
164
let open_object i ((_,lobj) as node) = 
 
165
  apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
 
166
 
 
167
let subst_object ((_,_,lobj) as node) = 
 
168
  apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
 
169
 
 
170
let classify_object ((_,lobj) as node) = 
 
171
  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
 
172
 
 
173
let discharge_object ((_,lobj) as node) = 
 
174
  apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
175
 
 
176
let rebuild_object (lobj as node) =
 
177
  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
 
178
 
 
179
let export_object lobj =
 
180
  apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj