%export real trit small_real small_real_digit
        plus small_plus
%include "~ids/misc/lib/miralib/stdenv.def"

|| USER-LEVEL TYPE DECLARATIONS

real ::= [trit] $POINT [trit]
  || before point is in ascending order, finite; after point
  ||  is in descending order, infinite
  ||  eg, in decimal, 37.46 would be [7,3] $POINT [4,6,0,0,0,.....]
  ||  see Grue's paper for further details
trit == num || {-1,0,1}

small_real == [small_real_digit]
small_real_digit == num || {0,1,2}






|| USER-LEVEL FUNCTIONS

plus :: real -> real -> real || not obvious from program structure!
  x $plus y = untwist (combine1 (x $newsum1 y))
              where
              untwist (xi $TWISTED_POINT xf) = xi $POINT xf

small_plus :: small_real -> small_real -> small_real
|| again, not obvious from syntax!
  x $small_plus y = ((x $sum1 y) $twisted_minus twisted_double carry_result) 
                    $twisted_plus 
                    twice_correct_to_mod_1 carry_result
                    where
                    carry_result = x $carry1 y








|| AUXILIARY TYPE DECLARATIONS

twisted_real ::= [twisted_trit] $TWISTED_POINT [twisted_trit]
twisted_trit == num || {-2,-1,0,1,2}

twisted_small_real == [twisted_small_real_digit]
twisted_small_real_digit == num || {-2,-1,0,1,2,3,4}






|| AUXILIARY FUNCTIONS

twisted_plus :: small_real -> small_real -> twisted_small_real
  (xh:xt) $twisted_plus (yh:yt)
    = (xh+yh):(xt $twisted_plus yt)

twisted_minus :: small_real -> small_real -> twisted_small_real
  (xh:xt) $twisted_minus (yh:yt)
    = (xh-yh):(xt $twisted_minus yt)

twisted_double :: small_real -> twisted_small_real
  twisted_double = map (2*)

twice_correct_to_mod_1 :: small_real -> small_real
  twice_correct_to_mod_1 = tl




carry :: twisted_small_real -> small_real
  carry = map high_bit
          where
          high_bit d = iff (d<=1) then 0 else 1

sum0 :: small_real -> small_real -> twisted_small_real
  sum0 = twisted_plus

carry0 :: small_real -> small_real -> small_real
  x $carry0 y = carry (x $sum0 y)

sum1 :: small_real -> small_real -> twisted_small_real
  x $sum1 y = ((x $sum0 y) $twisted_minus twisted_double carry_result) 
                           $twisted_plus twice_correct_to_mod_1 carry_result 
              where
              carry_result = x $carry0 y

carry1 :: small_real -> small_real -> small_real
  x $carry1 y = carry (x $sum1 y)








semihead :: [num] -> num
  semihead [] = 0
  semihead (h:t) = h

semitail :: [*] -> [*]
  semitail [] = []
  semitail (h:t) = t

semiattach :: num -> [num] -> [num]
  x $semiattach y = iff (x=0 & y=[]) then [] else (x:y)

finiteplus :: [trit] -> [trit] -> [twisted_trit]
  x $finiteplus y
    = iff (x=[] & y=[])
      then []
      else ((semihead x + semihead y)
            $semiattach
            (semitail x $finiteplus semitail y)
           )

new_twisted_plus :: real -> real -> twisted_real
  (xi $POINT xf) $new_twisted_plus (yi $POINT yf)
    = (xi $finiteplus yi) $TWISTED_POINT (xf $twisted_plus yf)

new_stay_twisted_plus :: twisted_real -> twisted_real -> twisted_real
  (xi $TWISTED_POINT xf) $new_stay_twisted_plus (yi $TWISTED_POINT yf)
    = (xi $finiteplus yi) $TWISTED_POINT (xf $twisted_plus yf)

coord :: (twisted_trit -> twisted_trit) -> twisted_real -> twisted_real
  coord f (xi $TWISTED_POINT xf)
    = map f xi $TWISTED_POINT map f xf

new_twisted_double_and_negate :: twisted_real -> twisted_real
  new_twisted_double_and_negate = coord ((-2)*)

newtwice :: twisted_real -> twisted_real
  newtwice (xi $TWISTED_POINT (xfh:xft)) = (xfh:xi) $TWISTED_POINT xft




combine :: twisted_real -> twisted_real -> twisted_real
  x $combine y
    = (x $new_stay_twisted_plus new_twisted_double_and_negate y)
      $new_stay_twisted_plus
      newtwice y

combine0 :: twisted_real -> twisted_real
  combine0 x = x $combine coord detect_negative x
               where
               detect_negative d = iff (d<0) then (-1) else 0

newsum0 :: real -> real -> twisted_real
  newsum0 = new_twisted_plus

newsum1 :: real -> real -> twisted_real
  x $newsum1 y = combine0 (x $newsum0 y)

combine1 :: twisted_real -> twisted_real
  combine1 x = x $combine coord detect_positive x
               where 
               detect_positive d = iff (d>0) then 1 else 0