1
(*************************************************************************
3
PROJET RNRT Calife - 2001
4
Author: Pierre Cr�gut - France T�l�com R&D
5
Licence : LGPL version 2.1
7
*************************************************************************)
11
module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
14
(* \section{Useful functions and flags} *)
15
(* Especially useful debugging functions *)
19
if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
21
let pp i = print_int i; print_newline (); flush stdout
23
(* More readable than the prefix notation *)
24
let (>>) = Tacticals.tclTHEN
26
let mkApp = Term.mkApp
29
\subsection{How to walk in a term}
30
To represent how to get to a proposition. Only choice points are
31
kept (branch to choose in a disjunction and identifier of the disjunctive
33
type direction = Left of int | Right of int
35
(* Step to find a proposition (operators are at most binary). A list is
37
type occ_step = O_left | O_right | O_mono
38
type occ_path = occ_step list
40
(* chemin identifiant une proposition sous forme du nom de l'hypoth�se et
41
d'une liste de pas � partir de la racine de l'hypoth�se *)
42
type occurence = {o_hyp : Names.identifier; o_path : occ_path}
44
(* \subsection{refiable formulas} *)
47
| Oint of Bigint.bigint
48
(* recognized binary and unary operations *)
49
| Oplus of oformula * oformula
50
| Omult of oformula * oformula
51
| Ominus of oformula * oformula
53
(* an atome in the environment *)
55
(* weird expression that cannot be translated *)
58
(* Operators for comparison recognized by Omega *)
59
type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
61
(* Type des pr�dicats r�ifi�s (fragment de calcul propositionnel. Les
62
* quantifications sont externes au langage) *)
64
Pequa of Term.constr * oequation
67
| Pnot of oproposition
68
| Por of int * oproposition * oproposition
69
| Pand of int * oproposition * oproposition
70
| Pimp of int * oproposition * oproposition
71
| Pprop of Term.constr
73
(* Les �quations ou proposiitions atomiques utiles du calcul *)
75
e_comp: comparaison; (* comparaison *)
76
e_left: oformula; (* formule brute gauche *)
77
e_right: oformula; (* formule brute droite *)
78
e_trace: Term.constr; (* tactique de normalisation *)
79
e_origin: occurence; (* l'hypoth�se dont vient le terme *)
80
e_negated: bool; (* vrai si apparait en position ni�
81
apr�s normalisation *)
82
e_depends: direction list; (* liste des points de disjonction dont
83
d�pend l'acc�s � l'�quation avec la
84
direction (branche) pour y acc�der *)
85
e_omega: afine (* la fonction normalis�e *)
88
(* \subsection{Proof context}
89
This environment codes
91
\item the terms and propositions that are given as
92
parameters of the reified proof (and are represented as variables in the
94
\item translation functions linking the decision procedure and the Coq proof
98
(* La liste des termes non reifies constituant l'environnement global *)
99
mutable terms : Term.constr list;
100
(* La meme chose pour les propositions *)
101
mutable props : Term.constr list;
102
(* Les variables introduites par omega *)
103
mutable om_vars : (oformula * int) list;
104
(* Traduction des indices utilis�s ici en les indices finaux utilis�s par
105
* la tactique Omega apr�s d�nombrement des variables utiles *)
106
real_indices : (int,int) Hashtbl.t;
107
mutable cnt_connectors : int;
108
equations : (int,oequation) Hashtbl.t;
109
constructors : (int, occurence) Hashtbl.t
112
(* \subsection{Solution tree}
113
D�finition d'une solution trouv�e par Omega sous la forme d'un identifiant,
114
d'un ensemble d'�quation dont d�pend la solution et d'une trace *)
115
(* La liste des d�pendances est tri�e et sans redondance *)
118
s_equa_deps : int list;
119
s_trace : action list }
121
(* Arbre de solution r�solvant compl�tement un ensemble de syst�mes *)
124
(* un noeud interne repr�sente un point de branchement correspondant �
125
l'�limination d'un connecteur g�n�rant plusieurs buts
126
(typ. disjonction). Le premier argument
127
est l'identifiant du connecteur *)
128
| Tree of int * solution_tree * solution_tree
130
(* Repr�sentation de l'environnement extrait du but initial sous forme de
131
chemins pour extraire des equations ou d'hypoth�ses *)
133
type context_content =
137
(* \section{Specific utility functions to handle base types} *)
138
(* Nom arbitraire de l'hypoth�se codant la n�gation du but final *)
139
let id_concl = Names.id_of_string "__goal__"
141
(* Initialisation de l'environnement de r�ification de la tactique *)
142
let new_environment () = {
143
terms = []; props = []; om_vars = []; cnt_connectors = 0;
144
real_indices = Hashtbl.create 7;
145
equations = Hashtbl.create 7;
146
constructors = Hashtbl.create 7;
149
(* G�n�ration d'un nom d'�quation *)
150
let new_connector_id env =
151
env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors
153
(* Calcul de la branche compl�mentaire *)
154
let barre = function Left x -> Right x | Right x -> Left x
156
(* Identifiant associ� � une branche *)
157
let indice = function Left x | Right x -> x
159
(* Affichage de l'environnement de r�ification (termes et propositions) *)
160
let print_env_reification env =
161
let rec loop c i = function
162
[] -> Printf.printf " ===============================\n\n"
164
Printf.printf " (%c%02d) := " c i;
165
Pp.ppnl (Printer.pr_lconstr t);
169
Printf.printf " ENVIRONMENT OF PROPOSITIONS :\n\n"; loop 'P' 0 env.props;
170
Printf.printf " ENVIRONMENT OF TERMS :\n\n"; loop 'V' 0 env.terms
173
(* \subsection{Gestion des environnements de variable pour Omega} *)
174
(* generation d'identifiant d'equation pour Omega *)
176
let new_omega_eq, rst_omega_eq =
178
(function () -> incr cpt; !cpt),
179
(function () -> cpt:=0)
181
(* generation d'identifiant de variable pour Omega *)
183
let new_omega_var, rst_omega_var =
185
(function () -> incr cpt; !cpt),
186
(function () -> cpt:=0)
188
(* Affichage des variables d'un syst�me *)
190
let display_omega_var i = Printf.sprintf "OV%d" i
192
(* Recherche la variable codant un terme pour Omega et cr�e la variable dans
193
l'environnement si il n'existe pas. Cas ou la variable dans Omega repr�sente
194
le terme d'un monome (le plus souvent un atome) *)
196
let intern_omega env t =
197
begin try List.assoc t env.om_vars
199
let v = new_omega_var () in
200
env.om_vars <- (t,v) :: env.om_vars; v
203
(* Ajout forc� d'un lien entre un terme et une variable Cas o� la
204
variable est cr��e par Omega et o� il faut la lier apr�s coup � un atome
205
r�ifi� introduit de force *)
206
let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
208
(* R�cup�re le terme associ� � une variable *)
209
let unintern_omega env id =
210
let rec loop = function
211
[] -> failwith "unintern"
212
| ((t,j)::l) -> if id = j then t else loop l in
215
(* \subsection{Gestion des environnements de variable pour la r�flexion}
216
Gestion des environnements de traduction entre termes des constructions
217
non r�ifi�s et variables des termes reifies. Attention il s'agit de
218
l'environnement initial contenant tout. Il faudra le r�duire apr�s
219
calcul des variables utiles. *)
221
let add_reified_atom t env =
222
try list_index0 t env.terms
224
let i = List.length env.terms in
225
env.terms <- env.terms @ [t]; i
227
let get_reified_atom env =
228
try List.nth env.terms with _ -> failwith "get_reified_atom"
230
(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
231
(* ajout d'une proposition *)
233
try list_index0 t env.props
235
let i = List.length env.props in env.props <- env.props @ [t]; i
237
(* acc�s a une proposition *)
238
let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
240
(* \subsection{Gestion du nommage des �quations} *)
241
(* Ajout d'une equation dans l'environnement de reification *)
242
let add_equation env e =
243
let id = e.e_omega.id in
244
try let _ = Hashtbl.find env.equations id in ()
245
with Not_found -> Hashtbl.add env.equations id e
247
(* acc�s a une equation *)
248
let get_equation env id =
249
try Hashtbl.find env.equations id
250
with e -> Printf.printf "Omega Equation %d non trouv�e\n" id; raise e
252
(* Affichage des termes r�ifi�s *)
253
let rec oprint ch = function
254
| Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n)
255
| Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2
256
| Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2
257
| Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2
258
| Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1
259
| Oatom n -> Printf.fprintf ch "V%02d" n
260
| Oufo x -> Printf.fprintf ch "?"
262
let rec pprint ch = function
263
Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) ->
266
Eq -> "=" | Leq -> "<=" | Geq -> ">="
267
| Gt -> ">" | Lt -> "<" | Neq -> "!=" in
268
Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2
269
| Ptrue -> Printf.fprintf ch "TT"
270
| Pfalse -> Printf.fprintf ch "FF"
271
| Pnot t -> Printf.fprintf ch "not(%a)" pprint t
272
| Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2
273
| Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2
274
| Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2
275
| Pprop c -> Printf.fprintf ch "Prop"
277
let rec weight env = function
279
| Oopp c -> weight env c
280
| Omult(c,_) -> weight env c
281
| Oplus _ -> failwith "weight"
282
| Ominus _ -> failwith "weight minus"
284
| Oatom _ as c -> (intern_omega env c)
286
(* \section{Passage entre oformules et repr�sentation interne de Omega} *)
288
(* \subsection{Oformula vers Omega} *)
290
let omega_of_oformula env kind =
291
let rec loop accu = function
292
| Oplus(Omult(v,Oint n),r) ->
293
loop ({v=intern_omega env v; c=n} :: accu) r
295
let id = new_omega_eq () in
296
(*i tag_equation name id; i*)
297
{kind = kind; body = List.rev accu;
298
constant = n; id = id}
299
| t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
302
(* \subsection{Omega vers Oformula} *)
304
let rec oformula_of_omega env af =
305
let rec loop = function
307
Oplus(Omult(unintern_omega env v,Oint n),loop r)
308
| [] -> Oint af.constant in
311
let app f v = mkApp(Lazy.force f,v)
313
(* \subsection{Oformula vers COQ reel} *)
315
let rec coq_of_formula env t =
316
let rec loop = function
317
| Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |]
318
| Oopp t -> app Z.opp [| loop t |]
319
| Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |]
323
(* attention ne traite pas les nouvelles variables si on ne les
324
* met pas dans env.term *)
325
get_reified_atom env var
326
| Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in
329
(* \subsection{Oformula vers COQ reifi�} *)
331
let reified_of_atom env i =
332
try Hashtbl.find env.real_indices i
334
Printf.printf "Atome %d non trouv�\n" i;
335
Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
338
let rec reified_of_formula env = function
340
app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |]
342
app coq_t_opp [| reified_of_formula env t |]
344
app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |]
345
| Oint v -> app coq_t_int [| Z.mk v |]
346
| Oufo t -> reified_of_formula env t
347
| Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
349
app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
351
let reified_of_formula env f =
352
begin try reified_of_formula env f with e -> oprint stderr f; raise e end
354
let rec reified_of_proposition env = function
355
Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
356
app coq_p_eq [| reified_of_formula env t1; reified_of_formula env t2 |]
357
| Pequa (_,{ e_comp=Leq; e_left=t1; e_right=t2 }) ->
358
app coq_p_leq [| reified_of_formula env t1; reified_of_formula env t2 |]
359
| Pequa(_,{ e_comp=Geq; e_left=t1; e_right=t2 }) ->
360
app coq_p_geq [| reified_of_formula env t1; reified_of_formula env t2 |]
361
| Pequa(_,{ e_comp=Gt; e_left=t1; e_right=t2 }) ->
362
app coq_p_gt [| reified_of_formula env t1; reified_of_formula env t2 |]
363
| Pequa(_,{ e_comp=Lt; e_left=t1; e_right=t2 }) ->
364
app coq_p_lt [| reified_of_formula env t1; reified_of_formula env t2 |]
365
| Pequa(_,{ e_comp=Neq; e_left=t1; e_right=t2 }) ->
366
app coq_p_neq [| reified_of_formula env t1; reified_of_formula env t2 |]
367
| Ptrue -> Lazy.force coq_p_true
368
| Pfalse -> Lazy.force coq_p_false
370
app coq_p_not [| reified_of_proposition env t |]
373
[| reified_of_proposition env t1; reified_of_proposition env t2 |]
376
[| reified_of_proposition env t1; reified_of_proposition env t2 |]
379
[| reified_of_proposition env t1; reified_of_proposition env t2 |]
380
| Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
382
let reified_of_proposition env f =
383
begin try reified_of_proposition env f
384
with e -> pprint stderr f; raise e end
386
(* \subsection{Omega vers COQ r�ifi�} *)
388
let reified_of_omega env body constant =
390
app coq_t_int [| Z.mk constant |] in
391
let mk_coeff {c=c; v=v} t =
394
[| reified_of_formula env (unintern_omega env v);
395
app coq_t_int [| Z.mk c |] |] in
396
app coq_t_plus [|coef; t |] in
397
List.fold_right mk_coeff body coeff_constant
399
let reified_of_omega env body c =
401
reified_of_omega env body c
403
display_eq display_omega_var (body,c); raise e
406
(* \section{Op�rations sur les �quations}
407
Ces fonctions pr�parent les traces utilis�es par la tactique r�fl�chie
408
pour faire des op�rations de normalisation sur les �quations. *)
410
(* \subsection{Extractions des variables d'une �quation} *)
411
(* Extraction des variables d'une �quation. *)
412
(* Chaque fonction retourne une liste tri�e sans redondance *)
414
let (@@) = list_merge_uniq compare
416
let rec vars_of_formula = function
418
| Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
419
| Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
420
| Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
421
| Oopp e -> vars_of_formula e
425
let rec vars_of_equations = function
428
(vars_of_formula e.e_left) @@
429
(vars_of_formula e.e_right) @@
430
(vars_of_equations l)
432
let rec vars_of_prop = function
433
| Pequa(_,e) -> vars_of_equations [e]
434
| Pnot p -> vars_of_prop p
435
| Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
436
| Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
437
| Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
438
| Pprop _ | Ptrue | Pfalse -> []
440
(* \subsection{Multiplication par un scalaire} *)
442
let rec scalar n = function
444
let tac1,t1' = scalar n t1 and
445
tac2,t2' = scalar n t2 in
446
do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2],
449
do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(Bigint.neg n))
450
| Omult(t1,Oint x) ->
451
do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
453
Util.error "Omega: Can't solve a goal with non-linear products"
454
| (Oatom _ as t) -> do_list [], Omult(t,Oint n)
455
| Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
456
| (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
457
| Ominus _ -> failwith "scalar minus"
459
(* \subsection{Propagation de l'inversion} *)
461
let rec negate = function
463
let tac1,t1' = negate t1 and
464
tac2,t2' = negate t2 in
465
do_list [Lazy.force coq_c_opp_plus ; (do_both tac1 tac2)],
468
do_list [Lazy.force coq_c_opp_opp], t
469
| Omult(t1,Oint x) ->
470
do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
472
Util.error "Omega: Can't solve a goal with non-linear products"
474
do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
475
| Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
476
| Oufo c -> do_list [], Oufo (Oopp c)
477
| Ominus _ -> failwith "negate minus"
479
let rec norm l = (List.length l)
481
(* \subsection{M�lange (fusion) de deux �quations} *)
482
(* \subsubsection{Version avec coefficients} *)
483
let rec shuffle_path k1 e1 k2 e2 =
484
let rec loop = function
485
(({c=c1;v=v1}::l1) as l1'),
486
(({c=c2;v=v2}::l2) as l2') ->
488
if k1*c1 + k2 * c2 = zero then (
489
Lazy.force coq_f_cancel :: loop (l1,l2))
491
Lazy.force coq_f_equal :: loop (l1,l2) )
492
else if v1 > v2 then (
493
Lazy.force coq_f_left :: loop(l1,l2'))
495
Lazy.force coq_f_right :: loop(l1',l2))
496
| ({c=c1;v=v1}::l1), [] ->
497
Lazy.force coq_f_left :: loop(l1,[])
498
| [],({c=c2;v=v2}::l2) ->
499
Lazy.force coq_f_right :: loop([],l2)
500
| [],[] -> flush stdout; [] in
501
mk_shuffle_list (loop (e1,e2))
503
(* \subsubsection{Version sans coefficients} *)
504
let rec shuffle env (t1,t2) =
506
Oplus(l1,r1), Oplus(l2,r2) ->
507
if weight env l1 > weight env l2 then
508
let l_action,t' = shuffle env (r1,t2) in
509
do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action], Oplus(l1,t')
511
let l_action,t' = shuffle env (t1,r2) in
512
do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
513
| Oplus(l1,r1), t2 ->
514
if weight env l1 > weight env t2 then
515
let (l_action,t') = shuffle env (r1,t2) in
516
do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t')
517
else do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1)
519
if weight env l2 > weight env t1 then
520
let (l_action,t') = shuffle env (t1,r2) in
521
do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
522
else do_list [],Oplus(t1,t2)
524
do_list [Lazy.force coq_c_reduce], Oint(t1+t2)
526
if weight env t1 < weight env t2 then
527
do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1)
528
else do_list [],Oplus(t1,t2)
530
(* \subsection{Fusion avec r�duction} *)
532
let shrink_pair f1 f2 =
533
begin match f1,f2 with
535
Lazy.force coq_c_red1, Omult(Oatom v,Oint two)
536
| Oatom v, Omult(_,c2) ->
537
Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint one))
538
| Omult (v1,c1),Oatom v ->
539
Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint one))
540
| Omult (Oatom v,c1),Omult (v2,c2) ->
541
Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
543
oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
544
flush Pervasives.stdout; Util.error "shrink.1"
547
(* \subsection{Calcul d'une sous formule constante} *)
549
let reduce_factor = function
551
let r = Omult(Oatom v,Oint one) in
552
[Lazy.force coq_c_red0],r
553
| Omult(Oatom v,Oint n) as f -> [],f
554
| Omult(Oatom v,c) ->
555
let rec compute = function
557
| Oplus(t1,t2) -> compute t1 + compute t2
558
| _ -> Util.error "condense.1" in
559
[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
560
| t -> Util.error "reduce_factor.1"
562
(* \subsection{R�ordonnancement} *)
564
let rec condense env = function
565
Oplus(f1,(Oplus(f2,r) as t)) ->
566
if weight env f1 = weight env f2 then begin
567
let shrink_tac,t = shrink_pair f1 f2 in
568
let assoc_tac = Lazy.force coq_c_plus_assoc_l in
569
let tac_list,t' = condense env (Oplus(t,r)) in
570
assoc_tac :: do_left (do_list [shrink_tac]) :: tac_list, t'
572
let tac,f = reduce_factor f1 in
573
let tac',t' = condense env t in
574
[do_both (do_list tac) (do_list tac')], Oplus(f,t')
576
| Oplus(f1,Oint n) ->
577
let tac,f1' = reduce_factor f1 in
578
[do_left (do_list tac)],Oplus(f1',Oint n)
580
if weight env f1 = weight env f2 then begin
581
let tac_shrink,t = shrink_pair f1 f2 in
582
let tac,t' = condense env t in
585
let tac,f = reduce_factor f1 in
586
let tac',t' = condense env f2 in
587
[do_both (do_list tac) (do_list tac')],Oplus(f,t')
589
| (Oint _ as t)-> [],t
591
let tac,t' = reduce_factor t in
592
let final = Oplus(t',Oint zero) in
593
tac @ [Lazy.force coq_c_red6], final
595
(* \subsection{Elimination des z�ros} *)
597
let rec clear_zero = function
598
Oplus(Omult(Oatom v,Oint n),r) when n=zero ->
599
let tac',t = clear_zero r in
600
Lazy.force coq_c_red5 :: tac',t
602
let tac,t = clear_zero r in
603
(if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t)
606
(* \subsection{Transformation des hypoth�ses} *)
608
let rec reduce env = function
610
let t1', trace1 = reduce env t1 in
611
let t2', trace2 = reduce env t2 in
612
let trace3,t' = shuffle env (t1',t2') in
613
t', do_list [do_both trace1 trace2; trace3]
615
let t,trace = reduce env (Oplus(t1, Oopp t2)) in
616
t, do_list [Lazy.force coq_c_minus; trace]
617
| Omult(t1,t2) as t ->
618
let t1', trace1 = reduce env t1 in
619
let t2', trace2 = reduce env t2 in
620
begin match t1',t2' with
622
let tac,t' = scalar n t1' in
623
t', do_list [do_both trace1 trace2; tac]
625
let tac,t' = scalar n t2' in
626
t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_comm; tac]
627
| _ -> Oufo t, Lazy.force coq_c_nop
630
let t',trace = reduce env t in
631
let trace',t'' = negate t' in
632
t'', do_list [do_left trace; trace']
633
| (Oint _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop
635
let normalize_linear_term env t =
636
let t1,trace1 = reduce env t in
637
let trace2,t2 = condense env t1 in
638
let trace3,t3 = clear_zero t2 in
639
do_list [trace1; do_list trace2; do_list trace3], t3
641
(* Cette fonction reproduit tr�s exactement le comportement de [p_invert] *)
642
let negate_oper = function
643
Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq
645
let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
646
let mk_step t1 t2 f kind =
648
let trace, oterm = normalize_linear_term env t in
649
let equa = omega_of_oformula env kind oterm in
650
{ e_comp = oper; e_left = t1; e_right = t2;
651
e_negated = negated; e_depends = depends;
652
e_origin = { o_hyp = origin; o_path = List.rev path };
653
e_trace = trace; e_omega = equa } in
654
try match (if negated then (negate_oper oper) else oper) with
655
| Eq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) EQUA
656
| Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) DISE
657
| Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) INEQ
658
| Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) INEQ
660
mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint negone),Oopp o1))
663
mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2))
665
with e when Logic.catchable_exception e -> raise e
667
(* \section{Compilation des hypoth�ses} *)
669
let rec oformula_of_constr env t =
670
match Z.parse_term t with
671
| Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2
672
| Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2
673
| Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 ->
674
binop env (fun x y -> Omult(x,y)) t1 t2
675
| Topp t -> Oopp(oformula_of_constr env t)
676
| Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
678
| _ -> Oatom (add_reified_atom t env)
680
and binop env c t1 t2 =
681
let t1' = oformula_of_constr env t1 in
682
let t2' = oformula_of_constr env t2 in
685
and binprop env (neg2,depends,origin,path)
686
add_to_depends neg1 gl c t1 t2 =
687
let i = new_connector_id env in
688
let depends1 = if add_to_depends then Left i::depends else depends in
689
let depends2 = if add_to_depends then Right i::depends else depends in
690
if add_to_depends then
691
Hashtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path};
693
oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in
695
oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in
696
(* On num�rote le connecteur dans l'environnement. *)
699
and mk_equation env ctxt c connector t1 t2 =
700
let t1' = oformula_of_constr env t1 in
701
let t2' = oformula_of_constr env t2 in
702
(* On ajoute l'equation dans l'environnement. *)
703
let omega = normalize_equation env ctxt (connector,t1',t2') in
704
add_equation env omega;
707
and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
708
match Z.parse_rel gl c with
709
| Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2
710
| Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2
711
| Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2
712
| Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2
713
| Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2
714
| Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2
719
oproposition_of_constr
720
env (not negated, depends, origin,(O_mono::path)) gl t in
723
binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
725
binprop env ctxt negated negated gl
726
(fun i x y -> Pand(i,x,y)) t1 t2
728
binprop env ctxt (not negated) (not negated) gl
729
(fun i x y -> Pimp(i,x,y)) t1 t2
731
binprop env ctxt negated negated gl
732
(fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
735
(* Destructuration des hypoth�ses et de la conclusion *)
737
let reify_gl env gl =
738
let concl = Tacmach.pf_concl gl in
740
Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
742
Printf.printf "REIFED PROBLEM\n\n";
743
Printf.printf " CONCL: "; pprint stdout t_concl; Printf.printf "\n"
745
let rec loop = function
747
let t' = oproposition_of_constr env (false,[],i,[]) gl t in
749
Printf.printf " %s: " (Names.string_of_id i);
755
if !debug then print_env_reification env;
757
let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
758
(id_concl,t_concl) :: t_lhyps
760
let rec destructurate_pos_hyp orig list_equations list_depends = function
761
| Pequa (_,e) -> [e :: list_equations]
762
| Ptrue | Pfalse | Pprop _ -> [list_equations]
763
| Pnot t -> destructurate_neg_hyp orig list_equations list_depends t
766
destructurate_pos_hyp orig list_equations (i::list_depends) t1 in
768
destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
772
destructurate_pos_hyp orig list_equations (list_depends) t1 in
773
let rec loop = function
774
le1 :: ll -> destructurate_pos_hyp orig le1 list_depends t2 @ loop ll
779
destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
781
destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
784
and destructurate_neg_hyp orig list_equations list_depends = function
785
| Pequa (_,e) -> [e :: list_equations]
786
| Ptrue | Pfalse | Pprop _ -> [list_equations]
787
| Pnot t -> destructurate_pos_hyp orig list_equations list_depends t
790
destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
792
destructurate_neg_hyp orig list_equations (i::list_depends) t2 in
796
destructurate_neg_hyp orig list_equations list_depends t1 in
797
let rec loop = function
798
le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
803
destructurate_pos_hyp orig list_equations list_depends t1 in
804
let rec loop = function
805
le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
809
let destructurate_hyps syst =
810
let rec loop = function
812
let l_syst1 = destructurate_pos_hyp i [] [] t in
813
let l_syst2 = loop l in
814
list_cartesian (@) l_syst1 l_syst2
818
(* \subsection{Affichage d'un syst�me d'�quation} *)
820
(* Affichage des d�pendances de syst�me *)
821
let display_depend = function
822
Left i -> Printf.printf " L%d" i
823
| Right i -> Printf.printf " R%d" i
825
let display_systems syst_list =
826
let display_omega om_e =
827
Printf.printf " E%d : %a %s 0\n"
829
(fun _ -> display_eq display_omega_var)
830
(om_e.body, om_e.constant)
831
(operator_of_eq om_e.kind) in
833
let display_equation oformula_eq =
834
pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline ();
835
display_omega oformula_eq.e_omega;
836
Printf.printf " Depends on:";
837
List.iter display_depend oformula_eq.e_depends;
838
Printf.printf "\n Path: %s"
840
(List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M")
841
oformula_eq.e_origin.o_path));
842
Printf.printf "\n Origin: %s (negated : %s)\n\n"
843
(Names.string_of_id oformula_eq.e_origin.o_hyp)
844
(if oformula_eq.e_negated then "yes" else "no") in
846
let display_system syst =
847
Printf.printf "=SYSTEM===================================\n";
848
List.iter display_equation syst in
849
List.iter display_system syst_list
851
(* Extraction des pr�dicats utilis�es dans une trace. Permet ensuite le
852
calcul des hypoth�ses *)
854
let rec hyps_used_in_trace = function
857
| HYP e -> [e.id] @@ (hyps_used_in_trace l)
858
| SPLIT_INEQ (_,(_,act1),(_,act2)) ->
859
hyps_used_in_trace act1 @@ hyps_used_in_trace act2
860
| _ -> hyps_used_in_trace l
864
(* Extraction des variables d�clar�es dans une �quation. Permet ensuite
865
de les d�clarer dans l'environnement de la proc�dure r�flexive et
866
�viter les cr�ations de variable au vol *)
868
let rec variable_stated_in_trace = function
872
(*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
873
(*i coef: int, var:int i*)
874
action :: variable_stated_in_trace l
875
| SPLIT_INEQ (_,(_,act1),(_,act2)) ->
876
variable_stated_in_trace act1 @ variable_stated_in_trace act2
877
| _ -> variable_stated_in_trace l
882
let add_stated_equations env tree =
883
(* Il faut trier les variables par ordre d'introduction pour ne pas risquer
884
de d�finir dans le mauvais ordre *)
885
let stated_equations =
886
let cmpvar x y = Pervasives.(-) x.st_var y.st_var in
887
let rec loop = function
888
| Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2)
889
| Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace)
893
(* On retransforme la d�finition de v en formule reifi�e *)
894
let v_def = oformula_of_omega env st.st_def in
895
(* Notez que si l'ordre de cr�ation des variables n'est pas respect�,
897
let coq_v = coq_of_formula env v_def in
898
let v = add_reified_atom coq_v env in
899
(* Le terme qu'il va falloir introduire *)
900
let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in
901
(* sa repr�sentation sous forme d'�quation mais non r�ifi� car on n'a pas
902
* l'environnement pour le faire correctement *)
903
let term_to_reify = (v_def,Oatom v) in
904
(* enregistre le lien entre la variable omega et la variable Coq *)
905
intern_omega_force env (Oatom v) st.st_var;
906
(v, term_to_generalize,term_to_reify,st.st_def.id) in
907
List.map add_env stated_equations
909
(* Calcule la liste des �clatements � r�aliser sur les hypoth�ses
910
n�cessaires pour extraire une liste d'�quations donn�e *)
912
(* PL: experimentally, the result order of the following function seems
913
_very_ crucial for efficiency. No idea why. Do not remove the List.rev
914
or modify the current semantics of Util.list_union (some elements of first
915
arg, then second arg), unless you know what you're doing. *)
917
let rec get_eclatement env = function
919
let l = try (get_equation env i).e_depends with Not_found -> [] in
920
list_union (List.rev l) (get_eclatement env r)
923
let select_smaller l =
924
let comp (_,x) (_,y) = Pervasives.(-) (List.length x) (List.length y) in
925
try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller"
927
let filter_compatible_systems required systems =
928
let rec select = function
930
if List.mem x required then select l
931
else if List.mem (barre x) required then failwith "Exit"
934
map_succeed (function (sol,splits) -> (sol,select splits)) systems
936
let rec equas_of_solution_tree = function
937
Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
938
| Leaf s -> s.s_equa_deps
940
(* [really_useful_prop] pushes useless props in a new Pprop variable *)
941
(* Things get shorter, but may also get wrong, since a Prop is considered
942
to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance
943
Pfalse is decidable. So should not be used on conclusion (??) *)
945
let really_useful_prop l_equa c =
946
let rec real_of = function
948
| Ptrue -> app coq_True [||]
949
| Pfalse -> app coq_False [||]
950
| Pnot t1 -> app coq_not [|real_of t1|]
951
| Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|]
952
| Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|]
953
(* Attention : implications sur le lifting des variables � comprendre ! *)
954
| Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2)
959
if List.mem e.e_omega.id l_equa then Some c else None
963
begin match loop t1 with None -> None | Some t1' -> Some (Pnot t1') end
964
| Por(i,t1,t2) -> binop (fun (t1,t2) -> Por(i,t1,t2)) t1 t2
965
| Pand(i,t1,t2) -> binop (fun (t1,t2) -> Pand(i,t1,t2)) t1 t2
966
| Pimp(i,t1,t2) -> binop (fun (t1,t2) -> Pimp(i,t1,t2)) t1 t2
969
begin match loop t1, loop t2 with
971
| Some t1',Some t2' -> Some (f(t1',t2'))
972
| Some t1',None -> Some (f(t1',Pprop (real_of t2)))
973
| None,Some t2' -> Some (f(Pprop (real_of t1),t2'))
976
None -> Pprop (real_of c)
979
let rec display_solution_tree ch = function
982
(Printf.sprintf "%d[%s]"
984
(String.concat " " (List.map string_of_int t.s_equa_deps)))
986
Printf.fprintf ch "S%d(%a,%a)" i
987
display_solution_tree t1 display_solution_tree t2
989
let rec solve_with_constraints all_solutions path =
990
let rec build_tree sol buf = function
992
| (Left i :: remainder) ->
994
build_tree sol (Left i :: buf) remainder,
995
solve_with_constraints all_solutions (List.rev(Right i :: buf)))
996
| (Right i :: remainder) ->
998
solve_with_constraints all_solutions (List.rev (Left i :: buf)),
999
build_tree sol (Right i :: buf) remainder) in
1000
let weighted = filter_compatible_systems path all_solutions in
1001
let (winner_sol,winner_deps) =
1002
try select_smaller weighted
1004
Printf.printf "%d - %d\n"
1005
(List.length weighted) (List.length all_solutions);
1006
List.iter display_depend path; raise e in
1007
build_tree winner_sol (List.rev path) winner_deps
1009
let find_path {o_hyp=id;o_path=p} env =
1010
let rec loop_path = function
1012
| (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2)
1014
let rec loop_id i = function
1015
CCHyp{o_hyp=id';o_path=p'} :: l when id = id' ->
1016
begin match loop_path (p',p) with
1018
| None -> loop_id (succ i) l
1020
| _ :: l -> loop_id (succ i) l
1021
| [] -> failwith "find_path" in
1024
let mk_direction_list l =
1025
let trans = function
1026
O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in
1027
mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l)
1030
(* \section{Rejouer l'historique} *)
1032
let get_hyp env_hyp i =
1033
try list_index0 (CCEqua i) env_hyp
1034
with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
1036
let replay_history env env_hyp =
1037
let rec loop env_hyp t =
1039
| CONTRADICTION (e1,e2) :: l ->
1040
let trace = mk_nat (List.length e1.body) in
1041
mkApp (Lazy.force coq_s_contradiction,
1042
[| trace ; mk_nat (get_hyp env_hyp e1.id);
1043
mk_nat (get_hyp env_hyp e2.id) |])
1044
| DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
1045
mkApp (Lazy.force coq_s_div_approx,
1047
reified_of_omega env e2.body e2.constant;
1048
mk_nat (List.length e2.body);
1049
loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
1050
| NOT_EXACT_DIVIDE (e1,k) :: l ->
1051
let e2_constant = floor_div e1.constant k in
1052
let d = e1.constant - e2_constant * k in
1053
let e2_body = map_eq_linear (fun c -> c / k) e1.body in
1054
mkApp (Lazy.force coq_s_not_exact_divide,
1056
reified_of_omega env e2_body e2_constant;
1057
mk_nat (List.length e2_body);
1058
mk_nat (get_hyp env_hyp e1.id)|])
1059
| EXACT_DIVIDE (e1,k) :: l ->
1061
map_eq_linear (fun c -> c / k) e1.body in
1062
let e2_constant = floor_div e1.constant k in
1063
mkApp (Lazy.force coq_s_exact_divide,
1065
reified_of_omega env e2_body e2_constant;
1066
mk_nat (List.length e2_body);
1067
loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
1068
| (MERGE_EQ(e3,e1,e2)) :: l ->
1069
let n1 = get_hyp env_hyp e1.id and n2 = get_hyp env_hyp e2 in
1070
mkApp (Lazy.force coq_s_merge_eq,
1071
[| mk_nat (List.length e1.body);
1072
mk_nat n1; mk_nat n2;
1073
loop (CCEqua e3:: env_hyp) l |])
1074
| SUM(e3,(k1,e1),(k2,e2)) :: l ->
1075
let n1 = get_hyp env_hyp e1.id
1076
and n2 = get_hyp env_hyp e2.id in
1077
let trace = shuffle_path k1 e1.body k2 e2.body in
1078
mkApp (Lazy.force coq_s_sum,
1079
[| Z.mk k1; mk_nat n1; Z.mk k2;
1080
mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
1081
| CONSTANT_NOT_NUL(e,k) :: l ->
1082
mkApp (Lazy.force coq_s_constant_not_nul,
1083
[| mk_nat (get_hyp env_hyp e) |])
1084
| CONSTANT_NEG(e,k) :: l ->
1085
mkApp (Lazy.force coq_s_constant_neg,
1086
[| mk_nat (get_hyp env_hyp e) |])
1087
| STATE {st_new_eq=new_eq; st_def =def;
1088
st_orig=orig; st_coef=m;
1089
st_var=sigma } :: l ->
1090
let n1 = get_hyp env_hyp orig.id
1091
and n2 = get_hyp env_hyp def.id in
1092
let v = unintern_omega env sigma in
1093
let o_def = oformula_of_omega env def in
1094
let o_orig = oformula_of_omega env orig in
1096
Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in
1097
let trace,_ = normalize_linear_term env body in
1098
mkApp (Lazy.force coq_s_state,
1099
[| Z.mk m; trace; mk_nat n1; mk_nat n2;
1100
loop (CCEqua new_eq.id :: env_hyp) l |])
1101
| HYP _ :: l -> loop env_hyp l
1102
| CONSTANT_NUL e :: l ->
1103
mkApp (Lazy.force coq_s_constant_nul,
1104
[| mk_nat (get_hyp env_hyp e) |])
1105
| NEGATE_CONTRADICT(e1,e2,true) :: l ->
1106
mkApp (Lazy.force coq_s_negate_contradict,
1107
[| mk_nat (get_hyp env_hyp e1.id);
1108
mk_nat (get_hyp env_hyp e2.id) |])
1109
| NEGATE_CONTRADICT(e1,e2,false) :: l ->
1110
mkApp (Lazy.force coq_s_negate_contradict_inv,
1111
[| mk_nat (List.length e2.body);
1112
mk_nat (get_hyp env_hyp e1.id);
1113
mk_nat (get_hyp env_hyp e2.id) |])
1114
| SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
1115
let i = get_hyp env_hyp e.id in
1116
let r1 = loop (CCEqua e1 :: env_hyp) l1 in
1117
let r2 = loop (CCEqua e2 :: env_hyp) l2 in
1118
mkApp (Lazy.force coq_s_split_ineq,
1119
[| mk_nat (List.length e.body); mk_nat i; r1 ; r2 |])
1120
| (FORGET_C _ | FORGET _ | FORGET_I _) :: l ->
1122
| (WEAKEN _ ) :: l -> failwith "not_treated"
1123
| [] -> failwith "no contradiction"
1126
let rec decompose_tree env ctxt = function
1127
Tree(i,left,right) ->
1129
try Hashtbl.find env.constructors i
1131
failwith (Printf.sprintf "Cannot find constructor %d" i) in
1132
let (index,path) = find_path org ctxt in
1133
let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in
1134
let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in
1137
mk_direction_list path;
1138
decompose_tree env (left_hyp::ctxt) left;
1139
decompose_tree env (right_hyp::ctxt) right |]
1141
decompose_tree_hyps s.s_trace env ctxt s.s_equa_deps
1142
and decompose_tree_hyps trace env ctxt = function
1143
[] -> app coq_e_solve [| replay_history env ctxt trace |]
1146
try Hashtbl.find env.equations i
1148
failwith (Printf.sprintf "Cannot find equation %d" i) in
1149
let (index,path) = find_path equation.e_origin ctxt in
1150
let full_path = if equation.e_negated then path @ [O_mono] else path in
1152
decompose_tree_hyps trace env
1153
(CCEqua equation.e_omega.id :: ctxt) l in
1154
app coq_e_extract [|mk_nat index;
1155
mk_direction_list full_path;
1158
(* \section{La fonction principale} *)
1159
(* Cette fonction construit la
1160
trace pour la proc�dure de d�cision r�flexive. A partir des r�sultats
1161
de l'extraction des syst�mes, elle lance la r�solution par Omega, puis
1162
l'extraction d'un ensemble minimal de solutions permettant la
1163
r�solution globale du syst�me et enfin construit la trace qui permet
1164
de faire rejouer cette solution par la tactique r�flexive. *)
1166
let resolution env full_reified_goal systems_list =
1168
let solve_system list_eq =
1170
let system = List.map (fun eq -> eq.e_omega) list_eq in
1173
(new_omega_eq,new_omega_var,display_omega_var)
1175
(* calcule les hypotheses utilis�es pour la solution *)
1176
let vars = hyps_used_in_trace trace in
1177
let splits = get_eclatement env vars in
1178
if !debug then begin
1179
Printf.printf "SYSTEME %d\n" index;
1180
display_action display_omega_var trace;
1181
print_string "\n Depend :";
1182
List.iter (fun i -> Printf.printf " %d" i) vars;
1183
print_string "\n Split points :";
1184
List.iter display_depend splits;
1185
Printf.printf "\n------------------------------------\n"
1188
{s_index = index; s_trace = trace; s_equa_deps = vars}, splits in
1189
if !debug then Printf.printf "\n====================================\n";
1190
let all_solutions = List.map solve_system systems_list in
1191
let solution_tree = solve_with_constraints all_solutions [] in
1192
if !debug then begin
1193
display_solution_tree stdout solution_tree;
1196
(* calcule la liste de toutes les hypoth�ses utilis�es dans l'arbre de solution *)
1197
let useful_equa_id = equas_of_solution_tree solution_tree in
1198
(* recupere explicitement ces equations *)
1199
let equations = List.map (get_equation env) useful_equa_id in
1200
let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
1201
let l_hyps = id_concl :: list_remove id_concl l_hyps' in
1203
List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
1205
let really_useful_vars = vars_of_equations equations in
1206
let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in
1207
really_useful_vars @@ concl_vars
1209
(* variables a introduire *)
1210
let to_introduce = add_stated_equations env solution_tree in
1211
let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in
1212
let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
1213
let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
1214
(* L'environnement de base se construit en deux morceaux :
1215
- les variables des �quations utiles (et de la conclusion)
1216
- les nouvelles variables declar�es durant les preuves *)
1217
let all_vars_env = useful_vars @ stated_vars in
1219
let rec loop i = function
1221
let t = get_reified_atom env var in
1222
Hashtbl.add env.real_indices var i; t :: loop (succ i) l
1224
loop 0 all_vars_env in
1225
let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
1226
(* On peut maintenant g�n�raliser le but : env est a jour *)
1227
let l_reified_stated =
1228
List.map (fun (_,_,(l,r),_) ->
1229
app coq_p_eq [| reified_of_formula env l;
1230
reified_of_formula env r |])
1233
match useful_hyps with
1234
(Pnot p) :: _ -> reified_of_proposition env p
1235
| _ -> reified_of_proposition env Pfalse in
1236
let l_reified_terms =
1239
reified_of_proposition env (really_useful_prop useful_equa_id p))
1240
(List.tl useful_hyps)) in
1241
let env_props_reified = mk_plist env.props in
1243
mk_list (Lazy.force coq_proposition)
1244
(l_reified_stated @ l_reified_terms) in
1246
app coq_interp_sequent
1247
[| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in
1248
let normalize_equation e =
1249
let rec loop = function
1250
[] -> app (if e.e_negated then coq_p_invert else coq_p_step)
1252
| ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
1253
| (O_right :: l) -> app coq_p_right [| loop l |] in
1255
let i = list_index0 e.e_origin.o_hyp l_hyps in
1256
(* PL: it seems that additionnally introduced hyps are in the way during
1257
normalization, hence this index shifting... *)
1258
if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
1260
app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
1261
let normalization_trace =
1262
mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in
1264
let initial_context =
1265
List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in
1267
CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
1268
let decompose_tactic = decompose_tree env context solution_tree in
1271
(l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
1272
Tactics.change_in_concl None reified >>
1273
Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
1275
Tactics.normalise_vm_in_concl >>
1276
(*i Alternatives to the previous line:
1277
- Normalisation without VM:
1278
Tactics.normalise_in_concl
1279
- Skip the conversion check and rely directly on the QED:
1280
Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
1282
Tactics.apply (Lazy.force coq_I)
1284
let total_reflexive_omega_tactic gl =
1285
Coqlib.check_required_library ["Coq";"romega";"ROmega"];
1289
let env = new_environment () in
1290
let full_reified_goal = reify_gl env gl in
1291
let systems_list = destructurate_hyps full_reified_goal in
1292
if !debug then display_systems systems_list;
1293
resolution env full_reified_goal systems_list gl
1294
with NO_CONTRADICTION -> Util.error "ROmega can't solve this system"
1297
(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
added
removed
contrib/romega/refl_omega.ml
