← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/romega/const_omega.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:
contrib/romega/const_omega.mli
 
1
(*************************************************************************
 
2
 
 
3
   PROJET RNRT Calife - 2001
 
4
   Author: Pierre Cr�gut - France T�l�com R&D
 
5
   Licence : LGPL version 2.1
 
6
 
 
7
 *************************************************************************)
 
8
 
 
9
 
 
10
(** Coq objects used in romega *)
 
11
 
 
12
(* from Logic *)
 
13
val coq_refl_equal : Term.constr lazy_t
 
14
val coq_and : Term.constr lazy_t
 
15
val coq_not : Term.constr lazy_t
 
16
val coq_or : Term.constr lazy_t
 
17
val coq_True : Term.constr lazy_t
 
18
val coq_False : Term.constr lazy_t
 
19
val coq_I : Term.constr lazy_t
 
20
 
 
21
(* from ReflOmegaCore/ZOmega *)
 
22
val coq_h_step : Term.constr lazy_t
 
23
val coq_pair_step : Term.constr lazy_t
 
24
val coq_p_left : Term.constr lazy_t
 
25
val coq_p_right : Term.constr lazy_t
 
26
val coq_p_invert : Term.constr lazy_t
 
27
val coq_p_step : Term.constr lazy_t
 
28
 
 
29
val coq_t_int : Term.constr lazy_t
 
30
val coq_t_plus : Term.constr lazy_t
 
31
val coq_t_mult : Term.constr lazy_t
 
32
val coq_t_opp : Term.constr lazy_t
 
33
val coq_t_minus : Term.constr lazy_t
 
34
val coq_t_var : Term.constr lazy_t
 
35
 
 
36
val coq_proposition : Term.constr lazy_t
 
37
val coq_p_eq : Term.constr lazy_t
 
38
val coq_p_leq : Term.constr lazy_t
 
39
val coq_p_geq : Term.constr lazy_t
 
40
val coq_p_lt : Term.constr lazy_t
 
41
val coq_p_gt : Term.constr lazy_t
 
42
val coq_p_neq : Term.constr lazy_t
 
43
val coq_p_true : Term.constr lazy_t
 
44
val coq_p_false : Term.constr lazy_t
 
45
val coq_p_not : Term.constr lazy_t
 
46
val coq_p_or : Term.constr lazy_t
 
47
val coq_p_and : Term.constr lazy_t
 
48
val coq_p_imp : Term.constr lazy_t
 
49
val coq_p_prop : Term.constr lazy_t
 
50
 
 
51
val coq_f_equal : Term.constr lazy_t
 
52
val coq_f_cancel : Term.constr lazy_t
 
53
val coq_f_left : Term.constr lazy_t
 
54
val coq_f_right : Term.constr lazy_t
 
55
 
 
56
val coq_c_do_both : Term.constr lazy_t
 
57
val coq_c_do_left : Term.constr lazy_t
 
58
val coq_c_do_right : Term.constr lazy_t
 
59
val coq_c_do_seq : Term.constr lazy_t
 
60
val coq_c_nop : Term.constr lazy_t
 
61
val coq_c_opp_plus : Term.constr lazy_t
 
62
val coq_c_opp_opp : Term.constr lazy_t
 
63
val coq_c_opp_mult_r : Term.constr lazy_t
 
64
val coq_c_opp_one : Term.constr lazy_t
 
65
val coq_c_reduce : Term.constr lazy_t
 
66
val coq_c_mult_plus_distr : Term.constr lazy_t
 
67
val coq_c_opp_left : Term.constr lazy_t
 
68
val coq_c_mult_assoc_r : Term.constr lazy_t
 
69
val coq_c_plus_assoc_r : Term.constr lazy_t
 
70
val coq_c_plus_assoc_l : Term.constr lazy_t
 
71
val coq_c_plus_permute : Term.constr lazy_t
 
72
val coq_c_plus_comm : Term.constr lazy_t
 
73
val coq_c_red0 : Term.constr lazy_t
 
74
val coq_c_red1 : Term.constr lazy_t
 
75
val coq_c_red2 : Term.constr lazy_t
 
76
val coq_c_red3 : Term.constr lazy_t
 
77
val coq_c_red4 : Term.constr lazy_t
 
78
val coq_c_red5 : Term.constr lazy_t
 
79
val coq_c_red6 : Term.constr lazy_t
 
80
val coq_c_mult_opp_left : Term.constr lazy_t
 
81
val coq_c_mult_assoc_reduced : Term.constr lazy_t
 
82
val coq_c_minus : Term.constr lazy_t
 
83
val coq_c_mult_comm : Term.constr lazy_t
 
84
 
 
85
val coq_s_constant_not_nul : Term.constr lazy_t
 
86
val coq_s_constant_neg : Term.constr lazy_t
 
87
val coq_s_div_approx : Term.constr lazy_t
 
88
val coq_s_not_exact_divide : Term.constr lazy_t
 
89
val coq_s_exact_divide : Term.constr lazy_t
 
90
val coq_s_sum : Term.constr lazy_t
 
91
val coq_s_state : Term.constr lazy_t
 
92
val coq_s_contradiction : Term.constr lazy_t
 
93
val coq_s_merge_eq : Term.constr lazy_t
 
94
val coq_s_split_ineq : Term.constr lazy_t
 
95
val coq_s_constant_nul : Term.constr lazy_t
 
96
val coq_s_negate_contradict : Term.constr lazy_t
 
97
val coq_s_negate_contradict_inv : Term.constr lazy_t
 
98
 
 
99
val coq_direction : Term.constr lazy_t
 
100
val coq_d_left : Term.constr lazy_t
 
101
val coq_d_right : Term.constr lazy_t
 
102
val coq_d_mono : Term.constr lazy_t
 
103
 
 
104
val coq_e_split : Term.constr lazy_t
 
105
val coq_e_extract : Term.constr lazy_t
 
106
val coq_e_solve : Term.constr lazy_t
 
107
 
 
108
val coq_interp_sequent : Term.constr lazy_t
 
109
val coq_do_omega : Term.constr lazy_t
 
110
 
 
111
(** Building expressions *)
 
112
 
 
113
val do_left : Term.constr -> Term.constr
 
114
val do_right : Term.constr -> Term.constr
 
115
val do_both : Term.constr -> Term.constr -> Term.constr
 
116
val do_seq : Term.constr -> Term.constr -> Term.constr
 
117
val do_list : Term.constr list -> Term.constr
 
118
 
 
119
val mk_nat : int -> Term.constr
 
120
val mk_list : Term.constr -> Term.constr list -> Term.constr
 
121
val mk_plist : Term.types list -> Term.types
 
122
val mk_shuffle_list : Term.constr list -> Term.constr
 
123
 
 
124
(** Analyzing a coq term *)
 
125
 
 
126
(* The generic result shape of the analysis of a term.
 
127
   One-level depth, except when a number is found *)
 
128
type parse_term =
 
129
    Tplus of Term.constr * Term.constr
 
130
  | Tmult of Term.constr * Term.constr
 
131
  | Tminus of Term.constr * Term.constr
 
132
  | Topp of Term.constr
 
133
  | Tsucc of Term.constr
 
134
  | Tnum of Bigint.bigint
 
135
  | Tother
 
136
 
 
137
(* The generic result shape of the analysis of a relation.
 
138
   One-level depth. *)
 
139
type parse_rel =
 
140
    Req of Term.constr * Term.constr
 
141
  | Rne of Term.constr * Term.constr
 
142
  | Rlt of Term.constr * Term.constr
 
143
  | Rle of Term.constr * Term.constr
 
144
  | Rgt of Term.constr * Term.constr
 
145
  | Rge of Term.constr * Term.constr
 
146
  | Rtrue
 
147
  | Rfalse
 
148
  | Rnot of Term.constr
 
149
  | Ror of Term.constr * Term.constr
 
150
  | Rand of Term.constr * Term.constr
 
151
  | Rimp of Term.constr * Term.constr
 
152
  | Riff of Term.constr * Term.constr
 
153
  | Rother
 
154
 
 
155
(* A module factorizing what we should now about the number representation *)
 
156
module type Int =
 
157
  sig
 
158
    (* the coq type of the numbers *)
 
159
    val typ : Term.constr Lazy.t
 
160
    (* the operations on the numbers *)
 
161
    val plus : Term.constr Lazy.t
 
162
    val mult : Term.constr Lazy.t
 
163
    val opp : Term.constr Lazy.t
 
164
    val minus : Term.constr Lazy.t
 
165
    (* building a coq number *)
 
166
    val mk : Bigint.bigint -> Term.constr
 
167
    (* parsing a term (one level, except if a number is found) *)
 
168
    val parse_term : Term.constr -> parse_term
 
169
    (* parsing a relation expression, including = < <= >= > *)
 
170
    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
 
171
    (* Is a particular term only made of numbers and + * - ? *) 
 
172
    val is_scalar : Term.constr -> bool
 
173
  end
 
174
 
 
175
(* Currently, we only use Z numbers *)
 
176
module Z : Int