← Back to branch summary

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

« back to all changes in this revision

Viewing changes to library/libnames.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/libnames.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: libnames.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
10
 
 
11
(*i*)
 
12
open Pp
 
13
open Util
 
14
open Names
 
15
open Term
 
16
open Mod_subst
 
17
(*i*)
 
18
 
 
19
(*s Global reference is a kernel side type for all references together *)
 
20
type global_reference =
 
21
  | VarRef of variable
 
22
  | ConstRef of constant
 
23
  | IndRef of inductive
 
24
  | ConstructRef of constructor
 
25
 
 
26
val isVarRef : global_reference -> bool
 
27
 
 
28
val subst_constructor : substitution -> constructor -> constructor * constr
 
29
val subst_global : substitution -> global_reference -> global_reference * constr
 
30
 
 
31
(* Turn a global reference into a construction *)
 
32
val constr_of_global : global_reference -> constr
 
33
 
 
34
(* Turn a construction denoting a global reference into a global reference;
 
35
   raise [Not_found] if not a global reference *)
 
36
val global_of_constr : constr -> global_reference
 
37
 
 
38
(* Obsolete synonyms for constr_of_global and global_of_constr *)
 
39
val constr_of_reference : global_reference -> constr
 
40
val reference_of_constr : constr -> global_reference
 
41
 
 
42
module Refset : Set.S with type elt = global_reference 
 
43
module Refmap : Map.S with type key = global_reference
 
44
 
 
45
(*s Dirpaths *)
 
46
val pr_dirpath : dir_path -> Pp.std_ppcmds
 
47
 
 
48
val dirpath_of_string : string -> dir_path
 
49
 
 
50
(* Give the immediate prefix of a [dir_path] *)
 
51
val dirpath_prefix : dir_path -> dir_path 
 
52
 
 
53
(* Give the immediate prefix and basename of a [dir_path] *)
 
54
val split_dirpath : dir_path -> dir_path * identifier
 
55
 
 
56
val extend_dirpath : dir_path -> module_ident -> dir_path
 
57
val add_dirpath_prefix : module_ident -> dir_path -> dir_path
 
58
 
 
59
val chop_dirpath : int -> dir_path -> dir_path * dir_path
 
60
val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
 
61
val extract_dirpath_prefix : int -> dir_path -> dir_path
 
62
val is_dirpath_prefix_of : dir_path -> dir_path -> bool
 
63
val append_dirpath : dir_path -> dir_path -> dir_path
 
64
 
 
65
module Dirset : Set.S with type elt = dir_path
 
66
module Dirmap : Map.S with type key = dir_path
 
67
 
 
68
(*s Section paths are {\em absolute} names *)
 
69
type section_path
 
70
 
 
71
(* Constructors of [section_path] *)
 
72
val make_path : dir_path -> identifier -> section_path
 
73
 
 
74
(* Destructors of [section_path] *)
 
75
val repr_path : section_path -> dir_path * identifier
 
76
val dirpath : section_path -> dir_path
 
77
val basename : section_path -> identifier
 
78
 
 
79
(* Parsing and printing of section path as ["coq_root.module.id"] *)
 
80
val path_of_string : string -> section_path
 
81
val string_of_path : section_path -> string
 
82
val pr_sp : section_path -> std_ppcmds
 
83
 
 
84
module Sppred : Predicate.S with type elt = section_path
 
85
module Spmap  : Map.S with type key = section_path
 
86
 
 
87
val restrict_path : int -> section_path -> section_path
 
88
 
 
89
type extended_global_reference =
 
90
  | TrueGlobal of global_reference
 
91
  | SyntacticDef of kernel_name
 
92
 
 
93
(*s Temporary function to brutally form kernel names from section paths *)
 
94
 
 
95
val encode_kn : dir_path -> identifier -> kernel_name
 
96
val decode_kn : kernel_name -> dir_path * identifier
 
97
val encode_con : dir_path -> identifier -> constant
 
98
val decode_con : constant -> dir_path * identifier
 
99
 
 
100
 
 
101
(*s A [qualid] is a partially qualified ident; it includes fully
 
102
    qualified names (= absolute names) and all intermediate partial
 
103
    qualifications of absolute names, including single identifiers *)
 
104
type qualid
 
105
 
 
106
val make_qualid : dir_path -> identifier -> qualid
 
107
val repr_qualid : qualid -> dir_path * identifier
 
108
 
 
109
val string_of_qualid : qualid -> string
 
110
val pr_qualid : qualid -> std_ppcmds
 
111
 
 
112
val qualid_of_string : string -> qualid
 
113
 
 
114
(* Turns an absolute name into a qualified name denoting the same name *)
 
115
val qualid_of_sp : section_path -> qualid
 
116
 
 
117
val qualid_of_dirpath : dir_path -> qualid
 
118
 
 
119
val make_short_qualid : identifier -> qualid
 
120
 
 
121
(* Both names are passed to objects: a "semantic" [kernel_name], which
 
122
   can be substituted and a "syntactic" [section_path] which can be printed
 
123
*)
 
124
 
 
125
type object_name = section_path * kernel_name
 
126
 
 
127
type object_prefix = dir_path * (module_path * dir_path)
 
128
 
 
129
val make_oname : object_prefix -> identifier -> object_name
 
130
 
 
131
(* to this type are mapped [dir_path]'s in the nametab *)
 
132
type global_dir_reference = 
 
133
  | DirOpenModule of object_prefix
 
134
  | DirOpenModtype of object_prefix
 
135
  | DirOpenSection of object_prefix
 
136
  | DirModule of object_prefix
 
137
  | DirClosedSection of dir_path
 
138
      (* this won't last long I hope! *)
 
139
 
 
140
type reference = 
 
141
  | Qualid of qualid located
 
142
  | Ident of identifier located
 
143
 
 
144
val qualid_of_reference : reference -> qualid located
 
145
val string_of_reference : reference -> string
 
146
val pr_reference : reference -> std_ppcmds
 
147
val loc_of_reference : reference -> loc
 
148
 
 
149
(* popping one level of section in global names *)
 
150
 
 
151
val pop_con : constant -> constant
 
152
val pop_kn : kernel_name -> kernel_name
 
153
val pop_global_reference : global_reference -> global_reference