%export rep_real
        rep_plus rep_negative rep_minus
        rep_create_real rep_trit_expansion
        rep_showreal
%include "~ids/misc/lib/miralib/stdenv.def"

|| REALS IMPLEMENTED AS FLOATING-POINT TRITSTREAMS: IMPLEMENTATION MODULE

|| TYPES

rep_real ::= rewrite_tag $RR rep_real_structure
  Ready $RR (e $EM m)
    => Rewritten___WARNING_Don't_Set_This___Always_Set_Ready
       $RR
       (new_e $EM new_m)
       where
       (new_e, new_m) = rewrite_real (e, m)

rewrite_tag ::= Ready | Rewritten___WARNING_Don't_Set_This___Always_Set_Ready
rep_real_structure ::= exponent $EM mantissa

exponent == int
mantissa == tritstream

int ::= ZMinus nat1up | ZZero | ZPlus nat1up      
tritstream == stream trit

nat1up ::= N1One | N1Succ nat1up

stream * ::= * $Attach stream *

trit ::= TMinus | TZero | TPlus
tritsign == char || '-' | '0' | '+'

|| auxiliary types

nat ::= NZero | NSucc nat

tritstream_with_halves == stream trit_with_halves
trit_with_halves ::= THMinus | THMinusHalf | THZero | THPlusHalf | THPlus






|| USER-LEVEL FUNCTIONS

|| arithmetical operations

rep_plus :: rep_real -> rep_real -> rep_real
|| adds two reals

  || unravel exponents to find which if either is greater

  || both exponents >= 3, mantissas begin with same sign
  (tag $RR (ZPlus (N1Succ (N1Succ e1)) $EM (t $Attach m1)))
  $rep_plus
  (tag $RR (ZPlus (N1Succ (N1Succ e2)) $EM (t $Attach m2)))
    = Ready $RR (ZPlus (N1Succ esum) $EM msum)
      where newtag $RR (ZPlus esum $EM msum)
        = (tag $RR (ZPlus (N1Succ e1) $EM (t $Attach m1)))
          $rep_plus
          (tag $RR (ZPlus (N1Succ e2) $EM (t $Attach m2)))

  || both exponents >= 3, mantissas begin with opposite signs
  (tag $RR (ZPlus (N1Succ (N1Succ e1)) $EM (t $Attach m1)))
  $rep_plus
  (tag $RR (ZPlus (N1Succ (N1Succ e2)) $EM (u $Attach m2)))
    = Ready $RR (zsucc esum $EM msum)
      where newtag $RR (esum $EM msum)
        = (tag $RR (ZPlus (N1Succ e1) $EM (t $Attach m1)))
          $rep_plus
          (tag $RR (ZPlus (N1Succ e2) $EM (u $Attach m2)))

  || first exponent >= 3, second exponent not
  (tag $RR (ZPlus (N1Succ (N1Succ e1)) $EM m1)) $rep_plus (tag $RR (e2 $EM m2))
    = Ready
      $RR
      (ZPlus (N1Succ (N1Succ (N1Succ e1)))
       $EM
       (m1
        $mantissa_mean
        (pad (ZPlus (N1Succ (N1Succ e1)) $int_to_nat_minus e2) m2)))

  || second exponent >= 3, first exponent not
  (tag $RR (e1 $EM m1)) $rep_plus (tag $RR (ZPlus (N1Succ (N1Succ e2)) $EM m2))
    = Ready
      $RR
      (ZPlus (N1Succ (N1Succ (N1Succ e2)))
       $EM
       ((pad (ZPlus (N1Succ (N1Succ e2)) $int_to_nat_minus e1) m1)
        $mantissa_mean
        m2))

  || both exponents <= -3
  (tag $RR (ZMinus (N1Succ (N1Succ e1)) $EM m1))
  $rep_plus
  (tag $RR (ZMinus (N1Succ (N1Succ e2)) $EM m2))
    = Ready $RR (ZMinus (N1Succ esum) $EM msum)
      where newtag $RR (ZMinus esum $EM msum)
        = (tag $RR (ZMinus (N1Succ e1) $EM m1))
          $rep_plus
          (tag $RR (ZMinus (N1Succ e2) $EM m2))

  || first exponent <= -3, second exponent not
  (tag $RR (ZMinus (N1Succ (N1Succ e1)) $EM m1)) $rep_plus (tag $RR (e2 $EM m2))
    = Ready
      $RR
      (zsucc e2
       $EM
       ((pad (e2 $int_to_nat_minus ZMinus (N1Succ (N1Succ e1))) m1)
        $mantissa_mean
        m2))

  || second exponent <= -3, first exponent not
  (tag $RR (e1 $EM m1)) $rep_plus (tag $RR (ZMinus (N1Succ (N1Succ e2)) $EM m2))
    = Ready
      $RR
      (zsucc e1
       $EM
       (m1
        $mantissa_mean
        (pad (e1 $int_to_nat_minus ZMinus (N1Succ (N1Succ e2))) m2)))

  || remaining case: both exponents are -2, -1, 0, 1 or 2
  (tag $RR (e1 $EM m1)) $rep_plus (tag $RR (e2 $EM m2))
    = iff (e1 $int_greateq e2)
      then (Ready $RR (zsucc e1
                       $EM
                       (m1 $mantissa_mean (pad (e1 $int_to_nat_minus e2) m2))))
      else (Ready $RR (zsucc e2
                       $EM
                       ((pad (e2 $int_to_nat_minus e1) m1) $mantissa_mean m2)))




rep_negative :: rep_real -> rep_real
|| negates a real
  rep_negative (tag $RR (e $EM m)) = tag $RR (e $EM (mantissa_negate m))

rep_minus :: rep_real -> rep_real -> rep_real
|| binary subtraction on reals
  x $rep_minus y = x $rep_plus rep_negative y


|| conversion facilities

|| conversion between reals and explicit exponent-mantissa pairs

rep_create_real :: (num, [tritsign]) -> rep_real
|| constructs a real from an exponent and a mantissa
  rep_create_real (e, m) = Ready $RR ((create_exponent e)
                                      $EM
                                      (create_mantissa m))

rep_trit_expansion :: rep_real -> (num, [tritsign])
|| gives a real in floating point form
  rep_trit_expansion (tag $RR (e $EM m))
    = (exponent_value e, mantissa_trit_expansion m)






|| AUXILIARY FUNCTIONS

|| rewrite rule for reals
rewrite_real :: (exponent, mantissa) -> (exponent, mantissa)
  rewrite_real (e, m) = rewrite_zeroes_into_exponent (e, rewrite_mantissa m)

rewrite_zeroes_into_exponent :: (exponent, mantissa) -> (exponent, mantissa)
  rewrite_zeroes_into_exponent (ZPlus (N1Succ e), TZero $Attach m)
    = rewrite_zeroes_into_exponent (ZPlus e, m)
  rewrite_zeroes_into_exponent (ZPlus N1One, TZero $Attach m)
    = rewrite_zeroes_into_exponent (ZZero, m)
  rewrite_zeroes_into_exponent (ZZero, TZero $Attach m)
    = rewrite_zeroes_into_exponent (ZMinus N1One, m)
  rewrite_zeroes_into_exponent (ZMinus n1up, m)
    = (ZMinus new_n1up, new_m)
      where (new_n1up, new_m) = rewrite_zeroes_into_nat1up (n1up, m)
  rewrite_zeroes_into_exponent (e, m) = (e, m)

rewrite_zeroes_into_nat1up :: (nat1up, mantissa) -> (nat1up, mantissa)
  rewrite_zeroes_into_nat1up (N1Succ n, m)
    = (N1Succ new_n, new_m)
      where (new_n, new_m) = rewrite_zeroes_into_nat1up (n, m)
  rewrite_zeroes_into_nat1up (N1One, TZero $Attach m)
    = (N1Succ new_n, new_m)
      where (new_n, new_m) = rewrite_zeroes_into_nat1up (N1One, m)
  rewrite_zeroes_into_nat1up (N1One, m) = (N1One, m)

rewrite_mantissa :: mantissa -> mantissa
  rewrite_mantissa (TZero $Attach m)
    = TZero $Attach rewrite_mantissa m
  rewrite_mantissa (TPlus $Attach TMinus $Attach m)
    = TZero $Attach rewrite_mantissa (TPlus $Attach m)
  rewrite_mantissa (TMinus $Attach TPlus $Attach m)
    = TZero $Attach rewrite_mantissa (TMinus $Attach m)
  rewrite_mantissa (head $Attach tail)
    = head $Attach rewrite_mantissa tail



|| supporting operations for addition

pad :: nat -> mantissa -> mantissa
|| pads out a mantissa with leading zeroes
  pad NZero m = m
  pad (NSucc n) m = TZero $Attach (pad n m)

mantissa_mean :: mantissa -> mantissa -> mantissa
|| computes the arithmetic mean of two mantissas
  m1 $mantissa_mean m2
    = purge_halves (stream_map trit_mean (m1 $stream_zip2 m2))

purge_halves :: tritstream_with_halves -> tritstream
|| decontaminates a tritstream of halves while preserving its value
  purge_halves x = newhead $Attach (purge_halves newtail)
                   where
                   (newhead, newtail) = purge_one_step x

purge_one_step :: tritstream_with_halves -> (trit, tritstream_with_halves)
|| peels off one guaranteed trit from its contaminated input stream
  purge_one_step (first $Attach second $Attach rest)
    = (newfirst, newsecond $Attach rest)
      where (newfirst, newsecond) = rewrite_one_step (first, second)


|| supporting operations for negation

mantissa_negate :: mantissa -> mantissa
|| negates a mantissa
  mantissa_negate = stream_map trit_negate

|| supporting operations for the conversion facilities

create_exponent :: num -> exponent
|| builds an exponent from a system integer
  create_exponent e
    = error "exponent must be an integer", ~integer e
    = num_to_int e, otherwise

create_mantissa :: [tritsign] -> mantissa
|| builds a mantissa from a list of tritsigns
  create_mantissa [] = stream_repeat TZero
  create_mantissa (head:tail) = trit_called head $Attach create_mantissa tail

exponent_value :: exponent -> num
|| expresses an exponent as a system integer
  exponent_value = int_to_num

mantissa_trit_expansion :: mantissa -> [tritsign]
|| gives a mantissa in tritsign form
  mantissa_trit_expansion (head $Attach tail)
    = tritsign_name head : mantissa_trit_expansion tail








|| LOW-LEVEL OPERATIONS

|| trit operations

trit_called :: tritsign -> trit
|| produces the named trit
  trit_called '-' = TMinus
  trit_called '0' = TZero
  trit_called '+' = TPlus
  trit_called anything_else
    = error ("'" ++ [anything_else] ++ "' is not a valid tritsign")


tritsign_name :: trit -> tritsign
|| gives the tritsign for a trit
  tritsign_name TMinus = '-'
  tritsign_name TZero  = '0'
  tritsign_name TPlus  = '+'


trit_mean :: (trit, trit) -> trit_with_halves
|| takes the mean of two trits
  trit_mean (TMinus, TMinus) = THMinus
  trit_mean (TMinus, TZero ) = THMinusHalf
  trit_mean (TMinus, TPlus ) = THZero 

  trit_mean (TZero , TMinus) = THMinusHalf
  trit_mean (TZero , TZero ) = THZero 
  trit_mean (TZero , TPlus ) = THPlusHalf

  trit_mean (TPlus , TMinus) = THZero 
  trit_mean (TPlus , TZero ) = THPlusHalf
  trit_mean (TPlus , TPlus ) = THPlus 


trit_negate :: trit -> trit
|| negates a trit
  trit_negate TMinus = TPlus
  trit_negate TZero  = TZero
  trit_negate TPlus  = TMinus


rewrite_one_step :: (trit_with_halves, trit_with_halves)
                      -> (trit, trit_with_halves)
|| decontaminates the left trit by rewriting both if necessary
  || purge a plus half
  rewrite_one_step (THMinusHalf, THMinus    ) = (TMinus, THZero     )
  rewrite_one_step (THMinusHalf, THMinusHalf) = (TMinus, THPlusHalf )
  rewrite_one_step (THMinusHalf, THZero     ) = (TZero , THMinus    )
  rewrite_one_step (THMinusHalf, THPlusHalf ) = (TZero , THMinusHalf)
  rewrite_one_step (THMinusHalf, THPlus     ) = (TZero , THZero     )

  || purge a minus half
  rewrite_one_step (THPlusHalf , THMinus    ) = (TZero , THZero     )
  rewrite_one_step (THPlusHalf , THMinusHalf) = (TZero , THPlusHalf )
  rewrite_one_step (THPlusHalf , THZero     ) = (TZero , THPlus     )
  rewrite_one_step (THPlusHalf , THPlusHalf ) = (TPlus , THMinusHalf)
  rewrite_one_step (THPlusHalf , THPlus     ) = (TPlus , THZero     )

  || otherwise leave well alone
  rewrite_one_step (THMinus, y) = (TMinus, y)
  rewrite_one_step (THZero , y) = (TZero , y)
  rewrite_one_step (THPlus , y) = (TPlus , y)



|| stream operations

stream_map :: (* -> **) -> stream * -> stream **
|| analogue of "map" for streams
  stream_map f (head $Attach tail) = (f head) $Attach (stream_map f tail)

stream_zip2 :: stream * -> stream ** -> stream (*, **)
|| analogue of "zip2" for streams
  (head1 $Attach tail1) $stream_zip2 (head2 $Attach tail2)
    = (head1, head2) $Attach (tail1 $stream_zip2 tail2)

stream_repeat :: * -> stream *
|| analogue of "repeat" for streams
  stream_repeat x = fix (x $Attach)



|| int, nat, nat1up operations

zsucc :: int -> int
  zsucc (ZPlus  x         ) = ZPlus  (N1Succ x)
  zsucc (ZZero            ) = ZPlus  N1One
  zsucc (ZMinus N1One     ) = ZZero
  zsucc (ZMinus (N1Succ x)) = ZMinus x

zpred :: int -> int
  zpred (ZMinus x         ) = ZMinus (N1Succ x)
  zpred (ZZero            ) = ZMinus N1One
  zpred (ZPlus  N1One     ) = ZZero
  zpred (ZPlus  (N1Succ x)) = ZPlus  x

int_greateq :: int -> int -> bool
  ZPlus (N1Succ x) $int_greateq ZPlus (N1Succ y)
    = ZPlus x $int_greateq ZPlus y
  ZPlus (N1Succ x) $int_greateq anything_else = True
  anything_else $int_greateq ZPlus (N1Succ y) = False
  ZMinus (N1Succ x) $int_greateq ZMinus (N1Succ y)
    = ZMinus x $int_greateq ZMinus y
  ZMinus (N1Succ x) $int_greateq anything_else = False
  anything_else $int_greateq ZMinus (N1Succ y) = True

  || from here on down, both inputs are -1, 0 or 1
  ZPlus N1One $int_greateq y = True
  ZZero $int_greateq y = y=ZZero \/ y=ZMinus N1One
  ZMinus N1One $int_greateq y = y=ZMinus N1One



num_to_int :: num -> int
  num_to_int x = error "input to num_to_int is not an integer", ~integer x
               = ZZero, x=0
               = ZPlus  (num_to_nat1up_shifted ( x-1)), x >= 1
               = ZMinus (num_to_nat1up_shifted (-x-1)), x <= -1

num_to_nat1up_shifted :: num -> nat1up
|| produces the nat1up version of one more than the input
  num_to_nat1up_shifted 0     = N1One
  num_to_nat1up_shifted (x+1) = N1Succ (num_to_nat1up_shifted x)

int_to_num :: int -> num
  int_to_num (ZMinus (N1Succ x)) = int_to_num (ZMinus x) - 1
  int_to_num (ZMinus N1One     ) = -1
  int_to_num (ZZero            ) = 0
  int_to_num (ZPlus  N1One     ) = 1
  int_to_num (ZPlus  (N1Succ x)) = int_to_num (ZPlus  x) + 1

int_to_nat_minus :: int -> int -> nat
  ZPlus (N1Succ x) $int_to_nat_minus ZPlus (N1Succ y)
    = ZPlus x $int_to_nat_minus ZPlus y
  ZPlus (N1Succ x) $int_to_nat_minus y
    = NSucc (ZPlus x $int_to_nat_minus y)
  ZPlus N1One $int_to_nat_minus y
    = ZZero $int_to_nat_minus zpred y
  ZZero $int_to_nat_minus ZZero = NZero
  ZZero $int_to_nat_minus ZMinus N1One = NSucc NZero
  ZZero $int_to_nat_minus ZMinus (N1Succ y)
    = NSucc (ZZero $int_to_nat_minus ZMinus y)
  ZMinus N1One $int_to_nat_minus y
    = ZZero $int_to_nat_minus zsucc y
  ZMinus (N1Succ x) $int_to_nat_minus ZMinus (N1Succ y)
    = ZMinus x $int_to_nat_minus ZMinus y

showint :: int -> [char]
  showint (ZMinus x) = "-" ++ shownat1up x
  showint (ZZero   ) = "0"
  showint (ZPlus  x) = "+" ++ shownat1up x

shownat1up :: nat1up -> [char]
  shownat1up N1One = "1"
  shownat1up (N1Succ x) = "s" ++ shownat1up x









|| PRINT-REPRESENTATIONS FOR ABSTRACT DATA TYPES

|| print-representation for type real

rep_showreal :: rep_real -> [char]
  rep_showreal (tag $RR (e $EM m))
    = "REAL WITH (BINARY) EXPONENT="
      ++ showexponent e
      ++ ", MANTISSA=."
      ++ showmantissa m

|| auxiliary functions for print-representations

showexponent :: exponent -> [char]
  showexponent = showint

showmantissa :: mantissa -> [char]
  showmantissa = mantissa_trit_expansion