module Math.Ordinals.MultiSet where
import Data.List (groupBy, intersperse)
newtype Ordinal = O [Ordinal] deriving Eq
w o = O [o]
instance Show Ordinal where
show o@(O os)
| o < O[1] = show (length os)
| otherwise = "("
++ (concat . intersperse " + ")
["w "++ show o' ++ showFactor(length os') | os'@(o':_)<-oss ]
++ ")"
where showFactor k = if k==1 then "" else (" *"++show k)
oss = groupBy (==) os
instance Ord Ordinal where
compare 0 0 = EQ
compare 0 _ = LT
compare _ 0 = GT
compare (O(a:as)) (O(b:bs)) = case compare a b of
EQ -> compare as bs
r -> r
wf (O []) = True
wf (O [o]) = wf o
wf (O (o:os@(o':_))) = o >= o' && wf (O os)
instance Enum Ordinal where
toEnum = fromInt
fromEnum = toInt
instance Real Ordinal where
instance Integral Ordinal where
toInteger o@(O as) | all (0 ==) as = fromIntegral (toInt o)
toInteger _ = error "ordinal not less than omega"
div a b = fst (divMod a b)
mod a b = snd (divMod a b)
divMod = quotRem
quotRem _ _ = error "Ordinal quotRem not yet defined"
instance Num Ordinal where
fromInteger k = fromInt (fromIntegral k)
abs = id
signum 0 = 0
signum (O(o:os)) = O[o]
o + 0 = o
O as + O bs@(b:_) = O (takeWhile (>=b) as ++ bs)
o 0 = o
0 _ = 0
o1@(O(a:as)) o2@(O(b:bs)) = case compare a b of
LT -> 0
EQ -> O as O bs
GT -> o1
0 * _ = 0
o1@(O(a:as)) * O bs
| null bs' = sum [o1 | _ <- zs]
| null zs = O [a+b | b<-bs']
| otherwise = o1 * O bs' + o1 * O zs
where (bs',zs) = span (>0) bs
(as1,as2) = span (a==) (a:as)
infixr 8 ^:
_ ^: 0 = 1
0 ^: _ = 0
1 ^: _ = 1
o1@(O osA@(a:_)) ^: o2@(O osB@(b:_))
| finiteB = o1^: (o2 1) * o1
| mB > 0 = o1^: O osB' * o1^: mB
| finiteA = O [o2]
| otherwise = O [a * o2]
where
(osA',zsA) = span (>0) osA
(osB',zsB) = span (>0) osB
mA = O zsA
mB = O zsB
finiteB = null osB'
finiteA = null osA'
toInt (O as) | all (0 ==) as = length as
toInt _ = error "ordinal not less than omega"
fromInt k = O (replicate k (O []))
infixr 5 .:
o .: O os = O (o:os)
infixr 5 ++.
as ++. O bs = O (as++bs)
infixr 5 .++.
O as .++. O bs = O (as++bs)