← Back to branch summary

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

« back to all changes in this revision

Viewing changes to parsing/g_rsyntax.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_rsyntax.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
(*i $Id: g_rsyntax.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
10
 
 
11
open Pp
 
12
open Util
 
13
open Names
 
14
open Pcoq
 
15
open Topconstr
 
16
open Libnames
 
17
 
 
18
exception Non_closed_number
 
19
 
 
20
(**********************************************************************)
 
21
(* Parsing R via scopes                                               *)
 
22
(**********************************************************************)
 
23
 
 
24
open Libnames
 
25
open Rawterm
 
26
open Bigint
 
27
 
 
28
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
29
let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
 
30
let make_path dir id = Libnames.make_path dir (id_of_string id)
 
31
 
 
32
let r_path = make_path rdefinitions "R"
 
33
 
 
34
(* TODO: temporary hack *)
 
35
let make_path dir id = Libnames.encode_con dir (id_of_string id)
 
36
 
 
37
let r_kn = make_path rdefinitions "R"
 
38
let glob_R = ConstRef r_kn
 
39
let glob_R1 = ConstRef (make_path rdefinitions "R1")
 
40
let glob_R0 = ConstRef (make_path rdefinitions "R0")
 
41
let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
 
42
let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
 
43
let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
 
44
 
 
45
let two = mult_2 one
 
46
let three = add_1 two
 
47
let four = mult_2 two
 
48
 
 
49
(* Unary representation of strictly positive numbers *)
 
50
let rec small_r dloc n =
 
51
  if equal one n then RRef (dloc, glob_R1)
 
52
  else RApp(dloc,RRef (dloc,glob_Rplus),
 
53
            [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
 
54
 
 
55
let r_of_posint dloc n =
 
56
  let r1 = RRef (dloc, glob_R1) in
 
57
  let r2 = small_r dloc two in
 
58
  let rec r_of_pos n =
 
59
    if less_than n four then small_r dloc n
 
60
    else
 
61
      let (q,r) = div2_with_rest n in
 
62
      let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
 
63
      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
 
64
  if n <> zero then r_of_pos n else RRef(dloc,glob_R0)
 
65
 
 
66
let r_of_int dloc z =
 
67
  if is_strictly_neg z then
 
68
    RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) 
 
69
  else
 
70
    r_of_posint dloc z
 
71
 
 
72
(**********************************************************************)
 
73
(* Printing R via scopes                                              *)
 
74
(**********************************************************************)
 
75
 
 
76
let bignat_of_r =
 
77
(* for numbers > 1 *)
 
78
let rec bignat_of_pos = function
 
79
  (* 1+1 *)
 
80
  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
 
81
      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
 
82
  (* 1+(1+1) *)
 
83
  | RApp (_,RRef (_,p1), [RRef (_,o1);
 
84
      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
 
85
      when p1 = glob_Rplus & p2 = glob_Rplus &
 
86
           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
 
87
  (* (1+1)*b *)
 
88
  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
 
89
      if bignat_of_pos a <> two then raise Non_closed_number;
 
90
      mult_2 (bignat_of_pos b)
 
91
  (* 1+(1+1)*b *)
 
92
  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
 
93
      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  -> 
 
94
      if bignat_of_pos a <> two then raise Non_closed_number;
 
95
        add_1 (mult_2 (bignat_of_pos b))
 
96
  | _ -> raise Non_closed_number
 
97
in
 
98
let bignat_of_r = function
 
99
  | RRef (_,a) when a = glob_R0 -> zero
 
100
  | RRef (_,a) when a = glob_R1 -> one
 
101
  | r -> bignat_of_pos r
 
102
in
 
103
bignat_of_r
 
104
 
 
105
let bigint_of_r = function
 
106
  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp ->
 
107
      let n = bignat_of_r a in
 
108
      if n = zero then raise Non_closed_number;
 
109
      neg n
 
110
  | a -> bignat_of_r a
 
111
 
 
112
let uninterp_r p =
 
113
  try
 
114
    Some (bigint_of_r p)
 
115
  with Non_closed_number ->
 
116
    None
 
117
 
 
118
let _ = Notation.declare_numeral_interpreter "R_scope"
 
119
  (r_path,["Coq";"Reals";"Rdefinitions"])
 
120
  r_of_int
 
121
  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
 
122
    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);
 
123
    RRef(dummy_loc,glob_R1)],
 
124
    uninterp_r,
 
125
    false)