← Back to branch summary

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

« back to all changes in this revision

Viewing changes to library/nameops.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/nameops.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: nameops.ml 9433 2006-12-12 09:38:53Z herbelin $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
open Names
 
14
 
 
15
(* Identifiers *)
 
16
 
 
17
let pr_id id = str (string_of_id id)
 
18
 
 
19
let pr_name = function
 
20
  | Anonymous -> str "_"
 
21
  | Name id -> pr_id id
 
22
 
 
23
(* Utilities *)
 
24
 
 
25
let code_of_0 = Char.code '0'
 
26
let code_of_9 = Char.code '9'
 
27
 
 
28
let cut_ident skip_quote s =
 
29
  let s = string_of_id s in
 
30
  let slen = String.length s in
 
31
  (* [n'] is the position of the first non nullary digit *)
 
32
  let rec numpart n n' =
 
33
    if n = 0 then 
 
34
      (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
 
35
      slen
 
36
    else 
 
37
      let c = Char.code (String.get s (n-1)) in
 
38
      if c = code_of_0 && n <> slen then 
 
39
        numpart (n-1) n' 
 
40
      else if code_of_0 <= c && c <= code_of_9 then 
 
41
        numpart (n-1) (n-1)
 
42
      else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
 
43
        numpart (n-1) (n-1)
 
44
      else
 
45
        n'
 
46
  in
 
47
  numpart slen slen
 
48
 
 
49
let repr_ident s =
 
50
  let numstart = cut_ident false s in
 
51
  let s = string_of_id s in
 
52
  let slen = String.length s in
 
53
  if numstart = slen then 
 
54
    (s, None)
 
55
  else
 
56
    (String.sub s 0 numstart,
 
57
     Some (int_of_string (String.sub s numstart (slen - numstart))))
 
58
 
 
59
let make_ident sa = function
 
60
  | Some n -> 
 
61
      let c = Char.code (String.get sa (String.length sa -1)) in
 
62
      let s =
 
63
        if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
 
64
        else sa ^ "_" ^ (string_of_int n) in
 
65
      id_of_string s
 
66
  | None -> id_of_string (String.copy sa)
 
67
 
 
68
let root_of_id id =
 
69
  let suffixstart = cut_ident true id in
 
70
  id_of_string (String.sub (string_of_id id) 0 suffixstart)
 
71
 
 
72
(* Rem: semantics is a bit different, if an ident starts with toto00 then
 
73
  after successive renamings it comes to toto09, then it goes on with toto10 *)
 
74
let lift_subscript id =
 
75
  let id = string_of_id id in
 
76
  let len = String.length id in
 
77
  let rec add carrypos =
 
78
    let c = id.[carrypos] in
 
79
    if is_digit c then
 
80
      if c = '9' then begin
 
81
        assert (carrypos>0);
 
82
        add (carrypos-1)
 
83
      end
 
84
      else begin
 
85
        let newid = String.copy id in
 
86
        String.fill newid (carrypos+1) (len-1-carrypos) '0';
 
87
        newid.[carrypos] <- Char.chr (Char.code c + 1);
 
88
        newid
 
89
      end
 
90
    else begin
 
91
      let newid = id^"0" in
 
92
      if carrypos < len-1 then begin
 
93
        String.fill newid (carrypos+1) (len-1-carrypos) '0';
 
94
        newid.[carrypos+1] <- '1'
 
95
      end;
 
96
      newid
 
97
    end
 
98
  in id_of_string (add (len-1))
 
99
 
 
100
let has_subscript id =
 
101
  let id = string_of_id id in
 
102
  is_digit (id.[String.length id - 1])
 
103
 
 
104
let forget_subscript id =
 
105
  let numstart = cut_ident false id in
 
106
  let newid = String.make (numstart+1) '0' in
 
107
  String.blit (string_of_id id) 0 newid 0 numstart;
 
108
  (id_of_string newid)
 
109
 
 
110
let add_suffix id s = id_of_string (string_of_id id ^ s)
 
111
let add_prefix s id = id_of_string (s ^ string_of_id id)
 
112
 
 
113
let atompart_of_id id = fst (repr_ident id)
 
114
 
 
115
(* Fresh names *)
 
116
 
 
117
let lift_ident = lift_subscript
 
118
 
 
119
let next_ident_away id avoid = 
 
120
  if List.mem id avoid then
 
121
    let id0 = if not (has_subscript id) then id else 
 
122
    (* Ce serait sans doute mieux avec quelque chose inspir� de 
 
123
       *** make_ident id (Some 0) *** mais �a brise la compatibilit�... *)
 
124
    forget_subscript id in
 
125
    let rec name_rec id =
 
126
      if List.mem id avoid then name_rec (lift_ident id) else id in 
 
127
    name_rec id0
 
128
  else id
 
129
 
 
130
let next_ident_away_from id avoid = 
 
131
  let rec name_rec id =
 
132
    if List.mem id avoid then name_rec (lift_ident id) else id in 
 
133
  name_rec id 
 
134
 
 
135
(* Names *)
 
136
 
 
137
let out_name = function
 
138
  | Name id -> id
 
139
  | Anonymous -> failwith "out_name: expects a defined name"
 
140
 
 
141
let name_fold f na a =
 
142
  match na with
 
143
  | Name id -> f id a
 
144
  | Anonymous -> a
 
145
 
 
146
let name_cons na l =
 
147
  match na with
 
148
  | Anonymous -> l 
 
149
  | Name id -> id::l
 
150
 
 
151
let name_app f = function
 
152
  | Name id -> Name (f id)
 
153
  | Anonymous -> Anonymous
 
154
 
 
155
let name_fold_map f e = function
 
156
  | Name id -> let (e,id) = f e id in (e,Name id)
 
157
  | Anonymous -> e,Anonymous
 
158
 
 
159
let next_name_away_with_default default name l = 
 
160
  match name with
 
161
    | Name str  -> next_ident_away str l
 
162
    | Anonymous -> next_ident_away (id_of_string default) l
 
163
 
 
164
let next_name_away = next_name_away_with_default "H"
 
165
 
 
166
let pr_lab l = str (string_of_label l)
 
167
 
 
168
let default_library = Names.initial_dir (* = ["Top"] *)
 
169
 
 
170
(*s Roots of the space of absolute names *)
 
171
let coq_root = id_of_string "Coq"
 
172
let default_root_prefix = make_dirpath []
 
173
 
 
174
(* Metavariables *)
 
175
let pr_meta = Pp.int
 
176
let string_of_meta = string_of_int