← Back to branch summary

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

« back to all changes in this revision

Viewing changes to parsing/g_zsyntax.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:
parsing/g_zsyntax.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: g_zsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
10
 
 
11
open Pcoq
 
12
open Pp
 
13
open Util
 
14
open Names
 
15
open Topconstr
 
16
open Libnames
 
17
open Bigint
 
18
 
 
19
exception Non_closed_number
 
20
 
 
21
(**********************************************************************)
 
22
(* Parsing positive via scopes                                        *)
 
23
(**********************************************************************)
 
24
 
 
25
open Libnames
 
26
open Rawterm
 
27
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
28
let positive_module = ["Coq";"NArith";"BinPos"]
 
29
let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
30
 
 
31
let positive_path = make_path positive_module "positive"
 
32
 
 
33
(* TODO: temporary hack *)
 
34
let make_kn dir id = Libnames.encode_kn dir id
 
35
 
 
36
let positive_kn = 
 
37
  make_kn (make_dir positive_module) (id_of_string "positive")
 
38
let glob_positive = IndRef (positive_kn,0)
 
39
let path_of_xI = ((positive_kn,0),1)
 
40
let path_of_xO = ((positive_kn,0),2)
 
41
let path_of_xH = ((positive_kn,0),3)
 
42
let glob_xI = ConstructRef path_of_xI
 
43
let glob_xO = ConstructRef path_of_xO
 
44
let glob_xH = ConstructRef path_of_xH
 
45
 
 
46
let pos_of_bignat dloc x =
 
47
  let ref_xI = RRef (dloc, glob_xI) in
 
48
  let ref_xH = RRef (dloc, glob_xH) in
 
49
  let ref_xO = RRef (dloc, glob_xO) in
 
50
  let rec pos_of x =
 
51
    match div2_with_rest x with
 
52
      | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
 
53
      | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q])
 
54
      | (q,true) -> ref_xH
 
55
  in 
 
56
  pos_of x
 
57
 
 
58
let error_non_positive dloc = 
 
59
  user_err_loc (dloc, "interp_positive",
 
60
    str "Only strictly positive numbers in type \"positive\".")
 
61
 
 
62
let interp_positive dloc n =
 
63
  if is_strictly_pos n then pos_of_bignat dloc n
 
64
  else error_non_positive dloc
 
65
 
 
66
(**********************************************************************)
 
67
(* Printing positive via scopes                                       *)
 
68
(**********************************************************************)
 
69
 
 
70
let rec bignat_of_pos = function
 
71
  | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
 
72
  | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
 
73
  | RRef (_, a) when a = glob_xH -> Bigint.one
 
74
  | _ -> raise Non_closed_number
 
75
 
 
76
let uninterp_positive p =
 
77
  try 
 
78
    Some (bignat_of_pos p)
 
79
  with Non_closed_number -> 
 
80
    None
 
81
 
 
82
(************************************************************************)
 
83
(* Declaring interpreters and uninterpreters for positive *)
 
84
(************************************************************************)
 
85
 
 
86
let _ = Notation.declare_numeral_interpreter "positive_scope"
 
87
  (positive_path,positive_module)
 
88
  interp_positive
 
89
  ([RRef (dummy_loc, glob_xI);
 
90
    RRef (dummy_loc, glob_xO); 
 
91
    RRef (dummy_loc, glob_xH)],
 
92
   uninterp_positive,
 
93
   true)
 
94
 
 
95
(**********************************************************************)
 
96
(* Parsing N via scopes                                               *)
 
97
(**********************************************************************)
 
98
 
 
99
let binnat_module = ["Coq";"NArith";"BinNat"]
 
100
let n_kn = make_kn (make_dir binnat_module) (id_of_string "N")
 
101
let glob_n = IndRef (n_kn,0)
 
102
let path_of_N0 = ((n_kn,0),1)
 
103
let path_of_Npos = ((n_kn,0),2)
 
104
let glob_N0 = ConstructRef path_of_N0
 
105
let glob_Npos = ConstructRef path_of_Npos
 
106
 
 
107
let n_path = make_path binnat_module "N"
 
108
 
 
109
let n_of_binnat dloc pos_or_neg n = 
 
110
  if n <> zero then
 
111
    RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n])
 
112
  else 
 
113
    RRef (dloc, glob_N0)
 
114
 
 
115
let error_negative dloc =
 
116
  user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
 
117
 
 
118
let n_of_int dloc n =
 
119
  if is_pos_or_zero n then n_of_binnat dloc true n
 
120
  else error_negative dloc
 
121
 
 
122
(**********************************************************************)
 
123
(* Printing N via scopes                                              *)
 
124
(**********************************************************************)
 
125
 
 
126
let bignat_of_n = function
 
127
  | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
 
128
  | RRef (_, a) when a = glob_N0 -> Bigint.zero
 
129
  | _ -> raise Non_closed_number
 
130
 
 
131
let uninterp_n p =
 
132
  try Some (bignat_of_n p)
 
133
  with Non_closed_number -> None
 
134
 
 
135
(************************************************************************)
 
136
(* Declaring interpreters and uninterpreters for N *)
 
137
 
 
138
let _ = Notation.declare_numeral_interpreter "N_scope"
 
139
  (n_path,binnat_module)
 
140
  n_of_int
 
141
  ([RRef (dummy_loc, glob_N0); 
 
142
    RRef (dummy_loc, glob_Npos)],
 
143
  uninterp_n,
 
144
  true)
 
145
   
 
146
(**********************************************************************)
 
147
(* Parsing Z via scopes                                               *)
 
148
(**********************************************************************)
 
149
 
 
150
let binint_module = ["Coq";"ZArith";"BinInt"]
 
151
let z_path = make_path binint_module "Z"
 
152
let z_kn = make_kn (make_dir binint_module) (id_of_string "Z")
 
153
let glob_z = IndRef (z_kn,0)
 
154
let path_of_ZERO = ((z_kn,0),1)
 
155
let path_of_POS = ((z_kn,0),2)
 
156
let path_of_NEG = ((z_kn,0),3)
 
157
let glob_ZERO = ConstructRef path_of_ZERO
 
158
let glob_POS = ConstructRef path_of_POS
 
159
let glob_NEG = ConstructRef path_of_NEG
 
160
 
 
161
let z_of_int dloc n = 
 
162
  if n <> zero then
 
163
    let sgn, n =
 
164
      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
 
165
    RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
 
166
  else 
 
167
    RRef (dloc, glob_ZERO)
 
168
 
 
169
(**********************************************************************)
 
170
(* Printing Z via scopes                                              *)
 
171
(**********************************************************************)
 
172
 
 
173
let bigint_of_z = function
 
174
  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
 
175
  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
 
176
  | RRef (_, a) when a = glob_ZERO -> Bigint.zero
 
177
  | _ -> raise Non_closed_number
 
178
 
 
179
let uninterp_z p =
 
180
  try
 
181
    Some (bigint_of_z p)
 
182
  with Non_closed_number -> None
 
183
 
 
184
(************************************************************************)
 
185
(* Declaring interpreters and uninterpreters for Z *)
 
186
 
 
187
let _ = Notation.declare_numeral_interpreter "Z_scope"
 
188
  (z_path,binint_module)
 
189
  z_of_int
 
190
  ([RRef (dummy_loc, glob_ZERO); 
 
191
    RRef (dummy_loc, glob_POS); 
 
192
    RRef (dummy_loc, glob_NEG)],
 
193
  uninterp_z,
 
194
  true)