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]