Subversion Repositories wimsdev

Rev

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]