How exactly this code works?

Question

I know how the code works except the x variable here: SOME y => SOME (x::y)

fun same_string(s1 : string, s2 : string) =
    s1 = s2

fun all_except_option (str, xs) = 
    case xs of 
    [] => NONE 
     | (x::xs') => case (same_string(str,x)) of 
               true => SOME xs' 
            | false => case all_except_option(str,xs') of 
                   NONE => NONE 
                    | SOME y=> SOME (x::y) 

How "x" holds ["a","b"] elements when you return SOME(x::y)?

val test1 = all_except_option("string", ["a","b","string","c"]) = SOME ["a","b","c"]

Answer 1

It doesn't. y has the list ["b","c"] bound to it, and x has "a" bound to it.

Taking x::y then gives the list "a"::["b","c"] = ["a","b","c"].

Stepping through the code from the beginning:

"string" <> "a", so a recursive call is made.
"string" <> "b", so another recursive call is made.
"string = "string", so SOME ["c"] is returned from the first recursive call.
Now, x holds "b" and y holds ["c"] in the first recursive call, and so SOME "b"::["c"] = SOME ["b","c"] is returned.
Finally, x holds "a" and y holds ["b","c"] in the top-level call, and so SOME "a"::["b","c"] = SOME ["a","b","c"] is returned from that call to be the final result.