Subversion Repositories wimsdev

condtest1=0

goal=!trim $m_goal
!if $goal=$empty
 goal=!trim $m_equivalence
 eqgoal=yes
!endif

!if $goal=$empty
 condtest1=1
 !exit
!endif

context=
cont=!nonempty lines $m_context
gt=>
lt=<
eq==
!if $gt isin $cont
 ff=!exec mathexp extract inequality\
$cont
 nn=!linecnt $ff
 !for n=1 to $nn
  l=!line $n of $ff
  !if $gt isin $l
   !distribute item $l into data,left,sign,right
   !distribute words $data into l_,s_,e_
   !if $sign iswordof $gt $gt$eq
    ss=!translate internal > to < in $sign
    new=$right $ss $left
    L=!line $l_ of $cont
    !reset l1,l2
    !if $s_>0
     l1=!char 1 to $s_ of $L
    !endif
    v_=!charcnt $L
    !if $e_<$v_
     l2=!char $e_+1 to -1 of $L
    !endif
    cont=!replace line number $l_ by $l1$new$l2 in $cont
   !endif
  !endif
 !next n 
!endif
n=!linecnt $cont
!if $n<1
 !if contradiction iswordof $m_goal
  condtest1=-1
 !endif
 !exit
!endif
!for i=1 to $n
 l=!line $i of $cont
 !if $i=1
  context=($l)
 !else
  context=$context And ($l)
 !endif
!next i

!if $context=$empty
# error=check_fail
 !exit
!endif

!if $gt isin $goal
 ff=!exec mathexp extract inequality\
$goal
 nn=!linecnt $ff
 !for n=1 to $nn
  l=!line $n of $ff
  !if $gt isin $l
   !distribute item $l into data,left,sign,right
   !distribute words $data into l_,s_,e_
   !if $sign iswordof $gt $gt$eq
    ss=!translate internal > to < in $sign
    new=$right $ss $left
    L=!line $l_ of $goal
    !reset l1,l2
    !if $s_>0
     l1=!char 1 to $s_ of $L
    !endif
    v_=!charcnt $L
    !if $e_<$v_
     l2=!char $e_+1 to -1 of $L
    !endif
    goal=!replace line number $l_ by $l1$new$l2 in $goal
   !endif
  !endif
 !next n 
!endif
goalcnt=!linecnt $goal
yinp=
!for i=1 to $goalcnt
 l=!line $i of $goal
 yinp=!append line CanProve(($context) => ($l)); to $yinp
!next i

yinp=!replace internal = by == in $yinp
yinp=!replace internal <== by <= in $yinp
yinp=!replace internal >== by >= in $yinp
yinp=!replace internal ==> by => in $yinp
out=!exec yacas $yinp

!if true notlineof $out and false notlineof $out
 !exit
!endif

!for i=1 to $goalcnt
 l=!line $i of $out
 !if $l issametext false
  condtest1=-1
  !exit
 !endif
 !if $l issametext true
  goal=!replace line number $i by $ in $goal
 !endif
!next i
goal=!nonempty lines $goal
goal=!trim $goal

!if $goal=$empty
 condtest1=1
 !exit
!endif

!if $eqgoal=yes
 m_equivalence=$goal
 m_goal=
!else
 m_goal=$goal
 m_equivalence=
!endif

!read deduc/objects.combine
!read deduc/objects.put $[$currstep-1]