(* val replace : char -> char -> string -> string *)
fun replace _ _ "" = ""
  | replace x y str =
    let val head = String.sub (str, 0)
	val tail = String.substring (str, 1, String.size(str) - 1)
	val tail' = replace x y tail
    in
	if head = x then String.str(y) ^ tail'
	else String.str(head) ^ tail'
    end

(*
Notation: [y/x] s means substitute the character y for each
occurrence of x in string s.  [] is common substitution notation,
though not as often in the case of strings.

Theorem: replace x y str ==> [y/x] str

Proof: By mathematical induction on the size of str

Base Case: size = 0.  Therefore, str = ""
   replace x y ""
   ==> "" = [y/x] ""

Inductive Step: Assume for given n >= 0 that for all str of size n
                replace x y str ==> [y/x] str
                To prove: For any string s of size n+1,
		replace x y s ==> [y/x] s

 Let s be a string of size n+1 >= 1.  To ease the notation, we
 represent the string consisting of the first character of s
 by c and the string consisting of the rest of s by ctail.
   replace x y s
   ==> let val head = String.sub (str, 0) ...
   ==> let val head = c
           val tail = String.substring (str, 1, String.size(str) - 1) ...
   ==> let val head = c
	   val tail = ctail
	   val tail' = replace x y tail in ... end
   ==> let val head = c
	   val tail = ctail
	   val tail' = [y/x] ctail
       in ... end  (By inductive hypothesis on tail of size n)
   ==> if c = x then String.str(y) ^ ([y/x] ctail)
	  else String.str(c) ^ ([y/x] ctail)
   Case c is x: ==> String.str(y) ^ ([y/x] ctail)
                = ([y/x] c) ^ ([y/x] ctail)
                = [y/x] (c ^ ctail)
                = [y/x] s
   Case c is not x ==> String.str(c) ^ ([y/x] tail)
                   = ([y/x] c) ^ ([y/x] ctail)
                   = [y/x] (c ^ ctail)
                   = [y/x] s
*)

(* This version reduces the number of parameters in the
   recursive call.  *)
(* val replace2 : char -> char -> string -> string *)
fun replace2 x y str =
    let fun repl "" = ""
	  | repl s =
	let val head = String.sub (s, 0)
	    val tail = String.substring (s, 1, String.size(s) - 1)
	    val tail' = repl tail
	in
	    if head = x then String.str(y) ^ tail'
	    else String.str(head) ^ tail'
	end
    in
	repl str
    end

(* Some ideas from class:
   - tail is only used once, so no need to have let val tail = ...
   - we might consider trying to stay with all strings and
     avoid characters as much as possible *)