%export game
        is_surreal
        g_greateq g_lesseq g_equals g_diff g_greater_than g_less_than
        g_lessfuzz g_greatfuzz g_fuzzy_against
        g_plus g_negative g_minus g_times g_ordinal_sum
        g_LR star up down
        int_to_game

        surreal
        s_greateq s_lesseq s_equals s_diff s_greater_than s_less_than
        s_plus s_negative s_minus s_times s_ordinal_sum
        s_LR
        int_to_surreal surreal_to_game game_to_surreal

        nimber
        n_plus n_negative n_minus n_times
        int_to_nimber nimber_to_int

        nimplus nimtimes

|| SET-BASED IMPLEMENTATION OF GAMES, SURREALS AND NIMBERS

|| This package implements games, surreals and nimbers as directly as
|| possible from Conway's original definitions. It serves
|| as a "canonical" implementation, more akin to an
|| executable specification.









|| ABSTRACT TYPE DECLARATIONS

|| declaration of type "game"---includes all the surreals

abstype game
with

     || test function for whether a game is a surreal

     is_surreal :: game -> bool

     || fundamental operations on games

     || comparison operations

     g_greateq       :: game -> game -> bool
     g_lesseq        :: game -> game -> bool
     g_equals        :: game -> game -> bool
     g_diff          :: game -> game -> bool
     g_greater_than  :: game -> game -> bool
     g_less_than     :: game -> game -> bool
     g_lessfuzz      :: game -> game -> bool
     g_greatfuzz     :: game -> game -> bool
     g_fuzzy_against :: game -> game -> bool

     || arithmetical operations

     g_plus        :: game -> game -> game
     g_negative    :: game -> game
     g_minus       :: game -> game -> game
     g_times       :: game -> game -> game
     g_ordinal_sum :: game -> game -> game

     || useful game generators

     g_LR :: [game] -> [game] -> game
     star :: num -> game
     up   :: game
     down :: game

     || conversion facilities

     || conversion from integers to games

     int_to_game :: num -> game

     || print-representation for type game

     showgame :: game -> [char]



|| declaration of type "surreal"

abstype surreal
with

     || fundamental operations on surreals

     || comparison operations

     s_greateq       :: surreal -> surreal -> bool
     s_lesseq        :: surreal -> surreal -> bool
     s_equals        :: surreal -> surreal -> bool
     s_diff          :: surreal -> surreal -> bool
     s_greater_than  :: surreal -> surreal -> bool
     s_less_than     :: surreal -> surreal -> bool

     || arithmetical operations

     s_plus        :: surreal -> surreal -> surreal
     s_negative    :: surreal -> surreal
     s_minus       :: surreal -> surreal -> surreal
     s_times       :: surreal -> surreal -> surreal
     s_ordinal_sum :: surreal -> surreal -> surreal

     || useful surreal generator

     s_LR :: [surreal] -> [surreal] -> surreal

     || conversion facilities

     || conversion from integers to surreals

     int_to_surreal :: num -> surreal

     || conversion between surreals and games

     surreal_to_game :: surreal -> game
     game_to_surreal :: game -> surreal

     || print-representation for type surreal

     showsurreal :: surreal -> [char]



|| impartial games with normal disjunctive sum---"nimbers"

abstype nimber
with

     || fundamental operations on nimbers

     || arithmetical operations

     n_plus     :: nimber -> nimber -> nimber
     n_negative :: nimber -> nimber
     n_minus    :: nimber -> nimber -> nimber
     n_times    :: nimber -> nimber -> nimber

     || conversion facilities

     || conversion between nimbers and integers

     int_to_nimber :: num -> nimber
     nimber_to_int :: nimber -> num

     || print-representation for type nimber

     shownimber :: nimber -> [char]






|| OTHER USER-LEVEL FUNCTIONS

|| Nim-arithmetic on top of nimbers!

nimplus  :: num -> num -> num
nimtimes :: num -> num -> num









|| CONCRETE TYPE DECLARATIONS

|| concrete representation of game

game     == rep_game
rep_game ::= [rep_game] $LR [rep_game]

  || rewrite rules for simplifying the syntax of a game

  || delete dominated option on left side
  (first:second:rest) $LR xR
    => (second:rest) $LR xR, first $rep_g_lesseq second
    => (first:rest) $LR xR, second $rep_g_lesseq first

  || delete dominated option on right side
  xL $LR (first:second:rest)
    => xL $LR (second:rest), first $rep_g_greateq second
    => xL $LR (first:rest), second $rep_g_greateq first

  || replace reversible left option with corresponding
  || left-right-left options
  [xLL $LR [xLRL $LR xLRR]] $LR xR
    => xLRL $LR xR,
       (map sAFE xLRL $SAFE_LR map sAFE xLRR)
       $sAFE_g_lesseq
       ([map sAFE xLL
         $SAFE_LR
         [map sAFE xLRL $SAFE_LR map sAFE xLRR]]
        $SAFE_LR
        map sAFE xR)

  || replace reversible right option with corresponding
  || right-left-right options
  xL $LR [[xRLL $LR xRLR] $LR xRR]
    => xL $LR xRLR,
       (map sAFE xRLL $SAFE_LR map sAFE xRLR)
       $sAFE_g_greateq
       (map sAFE xL
        $SAFE_LR
        [[map sAFE xRLL $SAFE_LR map sAFE xRLR]
         $SAFE_LR
         map sAFE xRR])

|| special version of the type "game" made SAFE by having no
|| rewrite rules; this is a Miranda technique to avoid
|| infinite cycling in certain cases of the recursive
|| definitions of the operators

sAFE_game ::= [sAFE_game] $SAFE_LR [sAFE_game]


|| concrete representation of surreal

|| surreals are a subclass of games, but for Miranda's
|| purposes, the declaration is identical

surreal == game


|| concrete representation of nimber

nimber     == rep_nimber
rep_nimber ::= SET [rep_nimber]

  || rewrite rule for nimbers (the mex rule)

  SET x' => mex x', ~(sAFE_n_canonical
                      (SAFE_SET (map sAFE_n x')))

|| safe version of nimbers [as for games]

sAFE_nimber ::= SAFE_SET [sAFE_nimber]









|| IMPLEMENTATION OF USER-LEVEL FUNCTIONS

|| These functions are the essentially the arithmetic and
|| comparison operators, a check for whether a game is a
|| surreal, and some simple generators of, and conversion
|| facilities between, games, surreals
|| and nimbers. There's also Nim-arithmetic on integers,
|| implemented on top of the nimber-handling functions.




|| user-level functions on games

|| test function for whether a game is a surreal

|| is_surreal :: game -> bool
|| Applies Conway's recursive definition for the subclass of
|| surreals to a given game, and reports whether it is or
|| isn't a surreal. Operating within surreals never takes
|| you out, but sometimes operating on non-surreals brings
|| you back in (eg, star + star = zero).
  is_surreal x = (all (xL++xR) is_surreal)
                 & (no [(xl,xr)|xl<-xL; xr<-xR]
                       special_g_greateq)
                 where xL $LR xR = x
                       special_g_greateq (a,b) = a $g_greateq b

|| fundamental operations on games

|| comparison operations

|| g_greateq :: game -> game -> bool
|| greater than or equal to
  g_greateq = rep_g_greateq

rep_g_greateq :: rep_game -> rep_game -> bool
|| concrete representation of greater than or equal to
|| (necessary for rep_game's rewrite rules)
  x $rep_g_greateq y = no xR ($rep_g_lesseq y) & no yL ($rep_g_greateq x)
                       where xL $LR xR = x
                             yL $LR yR = y

|| g_lesseq :: game -> game -> bool
|| less than or equal to
  g_lesseq = rep_g_lesseq

rep_g_lesseq :: rep_game -> rep_game -> bool
|| concrete representation of less than or equal to
|| (necessary for rep_game's rewrite rules)
  x $rep_g_lesseq y = y $rep_g_greateq x

|| g_equals :: game -> game -> bool
|| two syntactically different games can be equal, so a test
|| for equality is needed
  x $g_equals y = x $g_lesseq y & x $g_greateq y

|| g_diff :: game -> game -> bool
|| different from: negated "g_equals"
  x $g_diff y = ~(x $g_equals y)

|| g_greater_than :: game -> game -> bool
  x $g_greater_than y = x $g_greateq y & ~(y $g_greateq x)

|| g_less_than :: game -> game -> bool
  x $g_less_than y = y $g_greater_than x

|| g_lessfuzz :: game -> game -> bool
|| less than or fuzzy against
  x $g_lessfuzz y = ~(x $g_greateq y)

|| g_greatfuzz :: game -> game -> bool
|| greater than or fuzzy against
  x $g_greatfuzz y = ~(x $g_lesseq y)

|| g_fuzzy_against :: game -> game -> bool
|| Note: x is fuzzy against y iff x-y has a first-player
|| winning strategy no matter who starts, where we use the
|| two-player game interpretation of Conway's system. It can
|| also be taken to mean "traditional" comparison operators
|| (<, =, >) all give false.

|| [For surreals compared with surreals, fuzzy results never
||  occur, but for general games they do.]
  x $g_fuzzy_against y = x $g_lessfuzz y & x $g_greatfuzz y

|| arithmetical operations

|| g_plus :: game -> game -> game
  x $g_plus y = ((map ($g_plus y) xL) ++ (map (g_plus x) yL))
                $LR
                ((map ($g_plus y) xR) ++ (map (g_plus x) yR))
                where xL $LR xR = x
                      yL $LR yR = y

|| g_negative :: game -> game
  g_negative x = (map g_negative xR) $LR (map g_negative xL)
                 where xL $LR xR = x

|| g_minus :: game -> game -> game
  x $g_minus y = x $g_plus g_negative y

|| g_times :: game -> game -> game
  x $g_times y = ([(xL' $g_times y)
                   $g_plus (x $g_times yL')
                   $g_minus (xL' $g_times yL') |
                     xL'<-xL ; yL'<-yL]
                  ++
                  [(xR' $g_times y)
                   $g_plus (x $g_times yR')
                   $g_minus (xR' $g_times yR') |
                     xR'<-xR ; yR'<-yR])
                 $LR
                 ([(xL' $g_times y)
                   $g_plus (x $g_times yR')
                   $g_minus (xL' $g_times yR') |
                     xL'<-xL ; yR'<-yR]
                  ++
                  [(xR' $g_times y)
                   $g_plus (x $g_times yL')
                   $g_minus (xR' $g_times yL') |
                     xR'<-xR ; yL'<-yL])
                 where xL $LR xR = x
                       yL $LR yR = y

|| g_ordinal_sum :: game -> game -> game
  x $g_ordinal_sum y = (xL ++ (map (g_ordinal_sum x) yL))
                       $LR
                       (xR ++ (map (g_ordinal_sum x) yR))
                       where xL $LR xR = x
                             yL $LR yR = y

|| useful game generators

|| g_LR :: [game] -> [game] -> game
|| creates a game from its left and right sets
  g_LR = LR
  
|| star :: num -> game
|| The game often called "star" is star 1. This function
|| gives the game "*n" for a given n.
  star n = n' $LR n'
           where
           n' = [star m | m<-[0..n-1]], integer n & n>=0

|| up :: game
  up = [int_to_game 0] $LR [star 1]

|| down :: game
  down = g_negative up

|| conversion facilities

|| conversion from integers to games

|| int_to_game :: num -> game
|| produces the game corresponding to a given integer
  int_to_game = int_to_rep_game

int_to_rep_game :: num -> rep_game
|| concrete representation of int_to_game
  int_to_rep_game n = [] $LR [], n=0
                    = [int_to_rep_game (n-1)] $LR [], integer n & n>0
                    = [] $LR [int_to_rep_game (n+1)], integer n & n<0





|| user-level functions on surreals

|| fundamental operations on surreals

|| comparison operations

|| s_greateq :: surreal -> surreal -> bool
|| greater than or equal to
  s_greateq = g_greateq

|| s_lesseq :: surreal -> surreal -> bool
|| less than or equal to
  s_lesseq = g_lesseq

|| s_equals :: surreal -> surreal -> bool
|| two syntactically different surreals can be equal, so a test
|| for equality is needed
  s_equals = g_equals

|| s_diff :: surreal -> surreal -> bool
|| different from: negated "s_equals"
  s_diff = g_diff

|| s_greater_than :: surreal -> surreal -> bool
  s_greater_than = g_greater_than

|| s_less_than :: surreal -> surreal -> bool
  s_less_than = g_less_than

|| arithmetical operations

|| s_plus :: surreal -> surreal -> surreal
  s_plus = g_plus

|| s_negative :: surreal -> surreal
  s_negative = g_negative

|| s_minus :: surreal -> surreal -> surreal
  s_minus = g_minus

|| s_times :: surreal -> surreal -> surreal
  s_times = g_times

|| s_ordinal_sum :: surreal -> surreal -> surreal
  s_ordinal_sum = g_ordinal_sum

|| useful surreal generator

|| s_LR :: [surreal] -> [surreal] -> surreal
|| creates a surreal from its left and right sets, if valid
|| (otherwise gives an error message)
  xL $s_LR xR = g, is_surreal g
              = error "s_LR: sets do not form a surreal", otherwise
                 where g = xL $g_LR xR

|| conversion facilities

|| conversion from integers to surreals

|| int_to_surreal :: num -> surreal
|| produces the surreal corresponding to a given integer
  int_to_surreal = int_to_game

|| conversion between surreals and games

|| surreal_to_game :: surreal -> game
|| produces the game corresponding to a given surreal
  surreal_to_game = id

|| game_to_surreal :: game -> surreal
|| produces the surreal corresponding to a given game, if this exists
|| (otherwise gives an error message)
  game_to_surreal x = x, is_surreal x
                    = error "game_to_surreal: game given is not a surreal",
                       otherwise






|| user-level functions on nimbers

|| fundamental operations on nimbers

|| no comparison operations: any two distinct nimbers are
|| fuzzy against each other!

|| arithmetical operations

|| n_plus :: nimber -> nimber -> nimber
  x $n_plus y = SET ((map ($n_plus y) x')
                     ++ (map (n_plus x) y'))
                where SET x' = x
                      SET y' = y

|| n_negative :: nimber -> nimber
|| included for completeness, though all nimbers are their
|| own negatives
  n_negative = id

|| n_minus :: nimber -> nimber -> nimber
|| again, included for completeness, though it's just the
|| same as addition when done on nimbers
  x $n_minus y = x $n_plus n_negative y

|| n_times :: nimber -> nimber -> nimber
  x $n_times y = SET [(x'' $n_times y)
                      $n_plus (x $n_times y'')
                      $n_minus (x'' $n_times y'') |
                        x''<-x' ; y''<-y']
                 where SET x' = x
                       SET y' = y

|| conversion facilities

|| conversion between nimbers and integers

|| int_to_nimber :: num -> nimber
|| produces the nimber corresponding to a given integer
  int_to_nimber = int_to_rep_nimber

int_to_rep_nimber :: num -> rep_nimber
|| concrete representation of int_to_nimber
|| (necessary for rep_nimber's rewrite rules)
  int_to_rep_nimber n = SET [int_to_rep_nimber m | m<-[0..n-1]],
                         integer n & n>=0

|| nimber_to_int :: nimber -> num
|| produces the integer corresponding to a given nimber
  nimber_to_int x = # x' where SET x' = x







|| user-level functions for Nim-arithmetic

|| Nim-arithmetic on top of nimbers!

|| nimplus :: num -> num -> num
  x $nimplus y = nimber_to_int (int_to_nimber x $n_plus int_to_nimber y)

|| nimtimes :: num -> num -> num
  x $nimtimes y = nimber_to_int (int_to_nimber x $n_times int_to_nimber y)










|| SUPPORTING AND AUXILIARY FUNCTIONS TO BACK UP 
|| THE USER-LEVEL FUNCTIONS

|| minimal-excludent function for nimbers---used in the
|| rewrite rule
|| the mex of a set is the simplest nimber NOT in the set!

mex :: [rep_nimber] -> rep_nimber
  mex options = hd [int_to_rep_nimber n | n<-[0..] ;
                                          ~(member (map sAFE_n options)
                                                   (int_to_sAFE_nimber n))]

|| safe operators for non-looping comparisons
|| these are otherwise identical to the normal operators, 
|| but they use the special safe type with no rewrite rules
|| (ie, a Miranda trick and not part of the pure theory).

|| safe game-handling operators

sAFE :: rep_game -> sAFE_game
|| converts a game to safe form
  sAFE x = map sAFE xL $SAFE_LR map sAFE xR
           where xL $LR xR = x

sAFE_g_greateq :: sAFE_game -> sAFE_game -> bool
  x $sAFE_g_greateq y = no xR ($sAFE_g_lesseq y)
                        & no yL ($sAFE_g_greateq x)
                        where xL $SAFE_LR xR = x
                              yL $SAFE_LR yR = y

sAFE_g_lesseq :: sAFE_game -> sAFE_game -> bool
  x $sAFE_g_lesseq y = y $sAFE_g_greateq x

|| safe nimber-handling operators

sAFE_n :: rep_nimber -> sAFE_nimber
|| converts a nimber to safe form
  sAFE_n x = SAFE_SET (map sAFE_n x') where SET x' = x

sAFE_n_canonical :: sAFE_nimber -> bool
|| checks a nimber for canonical form, ie, all redundant
|| options chopped
  sAFE_n_canonical (SAFE_SET x')
    = x' $prefix_of all_the_sAFE_nimbers

all_the_sAFE_nimbers :: [sAFE_nimber]
|| a useful infinite object, the stream of all (safe)
|| nimbers. Used to check a nimber for canonical form.
  all_the_sAFE_nimbers = map int_to_sAFE_nimber [0..]

int_to_sAFE_nimber :: num -> sAFE_nimber
|| produces the safe nimber corresponding to a given integer
  int_to_sAFE_nimber n = SAFE_SET [int_to_sAFE_nimber m | m<-[0..n-1]],
                          integer n & n>=0









|| LOW-LEVEL OPERATIONS

no :: [*] -> (* -> bool) -> bool
|| tests if no members of a list satisfy a predicate
  no things like_this = ~(some things like_this)

some :: [*] -> (* -> bool) -> bool
|| tests if at least one member of a list satisfies a
|| predicate
  some things like_this = or (map like_this things)

all :: [*] -> (* -> bool) -> bool
|| tests if all members of a list satisfy a predicate
  all things like_this = and (map like_this things)

prefix_of :: [*] -> [*] -> bool
|| checks if one list is a prefix of another
  [] $prefix_of list2 = True
  (head1:tail1) $prefix_of [] = False
  (head1:tail1) $prefix_of (head2:tail2)
    = (head1 = head2) & (tail1 $prefix_of tail2)





|| PRINT-REPRESENTATIONS FOR ABSTRACT DATA TYPES
|| Miranda interface to built-in function "show"

|| pretty-printing functions: these output a game, surreal
|| or nimber in Conway's set-notation.

|| print-representation for type game

|| showgame :: game -> [char]
  showgame x = "GAME " ++ show_game_or_surreal x

|| print-representation for type surreal

|| showsurreal :: surreal -> [char]
  showsurreal x = "SURREAL "
                  ++ drop 5 (showgame x)

|| print-representation for type nimber

|| shownimber :: nimber -> [char]
  shownimber x = "NIMBER " ++ show_naked_nimber x



|| supporting functions for print-representations

show_game_or_surreal :: rep_game -> [char]
|| prints a game or surreal without identifying which type it is
  show_game_or_surreal x = "{"
                           ++ showgame_set xL
                           ++ "|"
                           ++ showgame_set xR
                           ++ "}"
                              where xL $LR xR = x

showgame_set :: [rep_game] -> [char]
|| prints out all the members of a set of games, with commas
|| in between
  showgame_set [] = ""
  showgame_set (head:tail) = show_game_or_surreal head
                             ++ showgame_rest tail

showgame_rest :: [rep_game] -> [char]
|| prints out members on behalf of "showgame_set" with a comma
|| immediately before each member
  showgame_rest [] = ""
  showgame_rest (head:tail) = ","
                              ++ show_game_or_surreal head
                              ++ showgame_rest tail

show_naked_nimber :: rep_nimber -> [char]
|| prints a nimber without identifying the type
  show_naked_nimber x = "{"
                        ++ shownimber_set x'
                        ++ "}"
                           where SET x' = x

shownimber_set :: [rep_nimber] -> [char]
|| prints out all the members of a set of nimbers, with
|| commas in between
  shownimber_set [] = ""
  shownimber_set (head:tail) = show_naked_nimber head
                               ++ shownimber_rest tail

shownimber_rest :: [rep_nimber] -> [char]
|| prints out members on behalf of "shownimber_set" with a comma
|| immediately before each member
  shownimber_rest [] = ""
  shownimber_rest (head:tail) = "," ++ show_naked_nimber head
                                    ++ shownimber_rest tail
