(* Carsten Schuermann 
   Printing Roman numerals *)

datatype RomanDigit 
  = I | V | X | D | L | C | M
  
datatype RomanNumber
  = Empty
  | Cons of RomanDigit * RomanNumber
  
(* digitToString D = s 
 
   Invariant:
   If D is a Roman digit then s is a string of the digit.
*)
fun digitToString I = "I"
  | digitToString V = "V"
  | digitToString X = "X"
  | digitToString D = "D"
  | digitToString L = "L"
  | digitToString C = "C"
  | digitToString M = "M"

(* numberToString N = s 
 
   Invariant:
   If N is a Roman number then s is a string of the number.
*)
fun numberToString Empty = ""
  | numberToString (Cons (d, n)) =
      digitToString d ^ numberToString n

(* charToDigit c = D 
 
   Invariant:
   If   c is a character among "XIVDLCM"
   then D is the corresponding character.
*)
fun charToDigit #"X" = X
  | charToDigit #"I" = I
  | charToDigit #"V" = V
  | charToDigit #"D" = D
  | charToDigit #"L" = L
  | charToDigit #"C" = C
  | charToDigit #"M" = M

(* stringToNumber s = N 
 
   Invariant:
   If   s is a string with characters among "XIVDLCM"
   then N is the Roman numeral that corresponds to s.
*)
fun stringToNumber s =
    let
      fun charsToNumber [] = Empty
	| charsToNumber (c :: l) = Cons (charToDigit c, charsToNumber l)
    in
      charsToNumber (String.explode s)
    end