Untyped Lambda Calculus to SKI Combinator Calculus

SKI.sml

datatype lambdaExpr =
         Var of string
         | Abs of string * lambdaExpr
         | App of lambdaExpr * lambdaExpr;

datatype skiExpr =
         S
       | K
       | I
       | SKIApp of skiExpr * skiExpr;

fun skiToString (e:skiExpr) =
    case e of
        S => "S"
      | K => "K"
      | I => "I"
      | SKIApp (SKIApp (e1, e2), e3) =>
        let val left = skiToString (SKIApp (e1, e2))
        in substring (left, 0, ((size left) - 1)) ^ " " ^ skiToString e3 ^ ")"
        end
      | SKIApp (e1, e2) => "(" ^ skiToString e1 ^ " " ^ skiToString e2 ^ ")"

exception iDoneFucked;

fun convert (e:lambdaExpr) :skiExpr =
    let
        datatype intermediate =
                 SInter
                 | KInter
                 | IInter
                 | VarInter of string
                 | AbsInter of string * intermediate
                 | AppInter of intermediate * intermediate

        fun ILtoString (e:intermediate) :string =
            case e of
                SInter => "S"
              | KInter => "K"
              | IInter => "I"
              | VarInter v => v
              | AbsInter (v, e) => "\\" ^ v ^ "." ^ (ILtoString e)
              | AppInter (e1, e2) => "(" ^ (ILtoString e1) ^ " " ^ (ILtoString e2) ^ ")"

        fun varIn (v:string) (e:intermediate) :bool =
            case e of
                VarInter v2 => v = v2
              | AbsInter (v2, e) => v <> v2 andalso varIn v e
              | AppInter (e1, e2) => varIn v e1 orelse varIn v e2
              | _ => false

        fun lambdaToIL (e:lambdaExpr) :intermediate =
            case e of
                Var v => VarInter v
              | Abs (v, e) => AbsInter (v, lambdaToIL e)
              | App (e1, e2) => AppInter (lambdaToIL e1, lambdaToIL e2)

        fun transform (e:intermediate) :intermediate =
            case e of
                SInter => SInter
              | KInter => KInter
              | IInter => IInter
              | VarInter v => VarInter v
              | AppInter (e1, e2) => AppInter (transform e1, transform e2)
              | AbsInter (v1, AbsInter (v2, e)) =>
                if varIn v1 e
                then transform (AbsInter (v1, transform (AbsInter (v2, e))))
                else AppInter (KInter, (transform (AbsInter (v2, e))))
              | AbsInter (v, AppInter (e1, e2)) =>
                if varIn v e1 orelse varIn v e2
                then AppInter(
                        AppInter(
                            SInter,
                            (transform (AbsInter (v, e1)))),
                        (transform (AbsInter (v, e2))))
                else AppInter (KInter, transform (AppInter (e1, e2)))
              | AbsInter (v, e) =>
                if VarInter v = e
                then IInter
                else AppInter (KInter, transform e)

        fun ILToSKI (e:intermediate) :skiExpr =
            case e of
                SInter => S
              | KInter => K
              | IInter => I
              | VarInter _ => raise iDoneFucked
              | AbsInter (v, e) => raise iDoneFucked
              | AppInter (e1, e2) => SKIApp (ILToSKI e1, ILToSKI e2)
    in
        ILToSKI (transform (lambdaToIL e))
    end;

val SII = convert (Abs ("x", (App (Var "x", Var "x"))));
val K_KI = convert (Abs ("x", (Abs ("y", Abs ("z", Var "z")))));
val S_K_SI__S_KK_I = convert (Abs ("x", Abs ("y", App (Var "y", Var "x"))));

val fxx = Abs ("x", App (Var "f", App (Var "x", Var "x")));
val Y = convert (Abs ("f", App (fxx, fxx)));

print ("Y = " ^ skiToString Y ^ "\n");

trace.txt

- Control.Print.printDepth := 30;
...
- use "SKI.sml";
[opening ./SKI.sml]
datatype lambdaExpr
  = Abs of string * lambdaExpr
  | App of lambdaExpr * lambdaExpr
  | Var of string
datatype skiExpr = I | K | S | SKIApp of skiExpr * skiExpr
val skiToString = fn : skiExpr -> string
exception iDoneFucked
val convert = fn : lambdaExpr -> skiExpr
val SII = SKIApp (SKIApp (S,I),I) : skiExpr
val KKI = SKIApp (K,SKIApp (K,I)) : skiExpr
val S_K_SI__S_KK_I =
  SKIApp
    (SKIApp (S,SKIApp (K,SKIApp (S,I))),SKIApp (SKIApp (S,SKIApp (K,K)),I))
  : skiExpr
val fxx = Abs ("x",App (Var "f",App (Var "x",Var "x"))) : lambdaExpr
val Y =
  SKIApp
    (SKIApp
       (S,
        SKIApp
          (SKIApp
             (S,
              SKIApp
                (SKIApp (S,SKIApp (K,S)),SKIApp (SKIApp (S,SKIApp (K,K)),I))),
           SKIApp (K,SKIApp (SKIApp (S,I),I)))),
     SKIApp
       (SKIApp
          (S,
           SKIApp (SKIApp (S,SKIApp (K,S)),SKIApp (SKIApp (S,SKIApp (K,K)),I))),
        SKIApp (K,SKIApp (SKIApp (S,I),I)))) : skiExpr
Y = (S (S (S (K S) (S (K K) I)) (K (S I I))) (S (S (K S) (S (K K) I)) (K (S I I))))
val it = () : unit