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