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
|
% -----------------------------------------------------------------------------
% (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
%
% The SPARK toolset is free software; you can redistribute it and/or modify it
% under terms of the GNU General Public License as published by the Free
% Software Foundation; either version 3, or (at your option) any later
% version. The SPARK toolset is distributed in the hope that it will be
% useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
% Public License for more details. You should have received a copy of the GNU
% General Public License distributed with the SPARK toolset; see file
% COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
% the license.
%
% =============================================================================
/*** do_replace_all(OLD, NEW) -- replace OLD by New in all hyps & concs ***/
do_replace_all(OLD, NEW) :-
max_hyp_no(MAX),
replace_all_hyps(OLD, NEW, 1, MAX),
fail.
do_replace_all(OLD, NEW) :-
max_conc_no(MAX),
replace_all_concs(OLD, NEW, 1, MAX),
fail.
do_replace_all(_, _) :- !.
replace_all_hyps(OLD, NEW, MAX, MAX) :-
!,
replace_in_hyp(MAX, OLD, NEW),
!.
replace_all_hyps(_OLD, _NEW, MIN, MAX) :-
MIN > MAX,
!. /* shouldn't get here... */
replace_all_hyps(OLD, NEW, MIN, MAX) :-
replace_in_hyp(MIN, OLD, NEW),
!,
NEWMIN is MIN + 1,
replace_all_hyps(OLD, NEW, NEWMIN, MAX),
!.
replace_in_hyp(HYP, _OLD, _NEW) :- /* CFR019 */
\+ command_arg(expression, all), /* CFR019 */
\+ hyp_to_replace(HYP), /* CFR019 */
!. /* CFR019 */
replace_in_hyp(HYP, OLD, NEW) :-
(
hyp(HYP, OLDEXPR),
!,
handle_quantifiers_in(OLDEXPR, OLDTEMPEXPR), /* CFR027 */
subst_vbl(OLD, NEW, OLDTEMPEXPR, NEWTEMPEXPR), /* CFR027 */
unhandle_quantifiers_in(NEWTEMPEXPR, NEWEXPR), /* CFR027 */
!,
(
OLDEXPR = NEWEXPR
;
assertz(hyp(HYP, NEWEXPR)),
assertz(logfact(newhyp, hyp(HYP, NEWEXPR))),
new_hyp_message(HYP, NEWEXPR), /* CFR018 */
retract(hyp(HYP, OLDEXPR))
)
;
true /* for case when no hyp: e.g. simplify cmnd.! */
),
!.
replace_all_concs(OLD, NEW, MAX, MAX) :-
!,
replace_in_conc(MAX, OLD, NEW),
!.
replace_all_concs(_OLD, _NEW, MIN, MAX) :-
MIN > MAX,
!. /* shouldn't get here... */
replace_all_concs(OLD, NEW, MIN, MAX) :-
replace_in_conc(MIN, OLD, NEW),
!,
NEWMIN is MIN + 1,
replace_all_concs(OLD, NEW, NEWMIN, MAX),
!.
replace_in_conc(CONC, _OLD, _NEW) :- /* CFR019 */
\+ command_arg(expression, all), /* CFR019 */
\+ conc_to_replace(CONC), /* CFR019 */
!. /* CFR019 */
replace_in_conc(CONC, OLD, NEW) :-
conc(CONC, OLDEXPR),
!,
handle_quantifiers_in(OLDEXPR, OLDTEMPEXPR), /* CFR027 */
subst_vbl(OLD, NEW, OLDTEMPEXPR, NEWTEMPEXPR), /* CFR027 */
unhandle_quantifiers_in(NEWTEMPEXPR, NEWEXPR), /* CFR027 */
!,
(
OLDEXPR = NEWEXPR
;
assertz(conc(CONC, NEWEXPR)),
assertz(logfact(newconc, conc(CONC, NEWEXPR))),
new_conc_message(CONC, NEWEXPR), /* CFR018 */
retract(conc(CONC, OLDEXPR))
),
!.
replace_in_conc(_CONC, _OLD, _NEW) :- !. /* when no conclusion left */
%###############################################################################
%END-OF-FILE
|
