Rev 20 | Details | Compare with Previous | Last modification | View Log | RSS feed
Rev | Author | Line No. | Line |
---|---|---|---|
20 | reyssat | 1 | condtest1=0 |
2 | |||
3 | goal=!trim $m_goal |
||
4 | !if $goal=$empty |
||
16204 | bpr | 5 | goal=!trim $m_equivalence |
6 | eqgoal=yes |
||
20 | reyssat | 7 | !endif |
8 | |||
9 | !if $goal=$empty |
||
16204 | bpr | 10 | condtest1=1 |
11 | !exit |
||
20 | reyssat | 12 | !endif |
13 | |||
14 | context= |
||
15 | cont=!nonempty lines $m_context |
||
16 | gt=> |
||
17 | lt=< |
||
18 | eq== |
||
19 | !if $gt isin $cont |
||
16204 | bpr | 20 | ff=!exec mathexp extract inequality\ |
20 | reyssat | 21 | $cont |
16204 | bpr | 22 | nn=!linecnt $ff |
23 | !for n=1 to $nn |
||
24 | l=!line $n of $ff |
||
25 | !if $gt isin $l |
||
26 | !distribute item $l into data,left,sign,right |
||
27 | !distribute words $data into l_,s_,e_ |
||
28 | !if $sign iswordof $gt $gt$eq |
||
29 | ss=!translate internal > to < in $sign |
||
30 | new=$right $ss $left |
||
31 | L=!line $l_ of $cont |
||
32 | !reset l1,l2 |
||
33 | !if $s_>0 |
||
34 | l1=!char 1 to $s_ of $L |
||
35 | !endif |
||
36 | v_=!charcnt $L |
||
37 | !if $e_<$v_ |
||
38 | l2=!char $e_+1 to -1 of $L |
||
39 | !endif |
||
40 | cont=!replace line number $l_ by $l1$new$l2 in $cont |
||
41 | !endif |
||
20 | reyssat | 42 | !endif |
16204 | bpr | 43 | !next n |
20 | reyssat | 44 | !endif |
45 | n=!linecnt $cont |
||
46 | !if $n<1 |
||
16204 | bpr | 47 | !if contradiction iswordof $m_goal |
48 | condtest1=-1 |
||
49 | !endif |
||
50 | !exit |
||
20 | reyssat | 51 | !endif |
52 | !for i=1 to $n |
||
16204 | bpr | 53 | l=!line $i of $cont |
54 | !if $i=1 |
||
55 | context=($l) |
||
56 | !else |
||
57 | context=$context And ($l) |
||
58 | !endif |
||
20 | reyssat | 59 | !next i |
60 | |||
61 | !if $context=$empty |
||
16204 | bpr | 62 | # error=check_fail |
63 | !exit |
||
20 | reyssat | 64 | !endif |
65 | |||
66 | !if $gt isin $goal |
||
16204 | bpr | 67 | ff=!exec mathexp extract inequality\ |
20 | reyssat | 68 | $goal |
16204 | bpr | 69 | nn=!linecnt $ff |
70 | !for n=1 to $nn |
||
71 | l=!line $n of $ff |
||
72 | !if $gt isin $l |
||
73 | !distribute item $l into data,left,sign,right |
||
74 | !distribute words $data into l_,s_,e_ |
||
75 | !if $sign iswordof $gt $gt$eq |
||
76 | ss=!translate internal > to < in $sign |
||
77 | new=$right $ss $left |
||
78 | L=!line $l_ of $goal |
||
79 | !reset l1,l2 |
||
80 | !if $s_>0 |
||
81 | l1=!char 1 to $s_ of $L |
||
82 | !endif |
||
83 | v_=!charcnt $L |
||
84 | !if $e_<$v_ |
||
85 | l2=!char $e_+1 to -1 of $L |
||
86 | !endif |
||
87 | goal=!replace line number $l_ by $l1$new$l2 in $goal |
||
88 | !endif |
||
20 | reyssat | 89 | !endif |
16204 | bpr | 90 | !next n |
20 | reyssat | 91 | !endif |
92 | goalcnt=!linecnt $goal |
||
93 | yinp= |
||
94 | !for i=1 to $goalcnt |
||
16204 | bpr | 95 | l=!line $i of $goal |
96 | yinp=!append line CanProve(($context) => ($l)); to $yinp |
||
20 | reyssat | 97 | !next i |
98 | |||
99 | yinp=!replace internal = by == in $yinp |
||
100 | yinp=!replace internal <== by <= in $yinp |
||
101 | yinp=!replace internal >== by >= in $yinp |
||
102 | yinp=!replace internal ==> by => in $yinp |
||
103 | out=!exec yacas $yinp |
||
104 | |||
105 | !if true notlineof $out and false notlineof $out |
||
16204 | bpr | 106 | !exit |
20 | reyssat | 107 | !endif |
108 | |||
109 | !for i=1 to $goalcnt |
||
16204 | bpr | 110 | l=!line $i of $out |
111 | !if $l issametext false |
||
112 | condtest1=-1 |
||
113 | !exit |
||
114 | !endif |
||
115 | !if $l issametext true |
||
116 | goal=!replace line number $i by $ in $goal |
||
117 | !endif |
||
20 | reyssat | 118 | !next i |
119 | goal=!nonempty lines $goal |
||
120 | goal=!trim $goal |
||
121 | |||
122 | !if $goal=$empty |
||
16204 | bpr | 123 | condtest1=1 |
124 | !exit |
||
20 | reyssat | 125 | !endif |
126 | |||
127 | !if $eqgoal=yes |
||
16204 | bpr | 128 | m_equivalence=$goal |
129 | m_goal= |
||
20 | reyssat | 130 | !else |
16204 | bpr | 131 | m_goal=$goal |
132 | m_equivalence= |
||
20 | reyssat | 133 | !endif |
134 | |||
135 | !read deduc/objects.combine |
||
136 | !read deduc/objects.put $[$currstep-1] |