Call-by-value λ-calculus interpreter in Cool

cbv.cl

-- Call-by-value lambda calculus in cool
(*
data Expr = Var Str
          | Abs Str Expr
          | App Expr Expr
          | Sub1 Expr
          | Mul Expr Expr
          | Add Expr Expr
          | Ifz Expr Expr Expr
*)

class ExprD {
  v() : String { { abort(); v(); } };
  lbound() : String { { abort(); lbound(); } };
  lbody() : ExprD { { abort(); lbody(); } };
  lapp() : ExprD { { abort(); lapp(); } };
  rapp() : ExprD { { abort(); rapp(); } };
  -- for general binary operators
  l() : ExprD { { abort(); l(); } };
  r() : ExprD { { abort(); r(); } };
  -- for if
  p() : ExprD { { abort(); p(); } };
  c() : ExprD { { abort(); c(); } };
  a() : ExprD { { abort(); a(); } };
  -- for unary operators
  arg() : ExprD { { abort(); arg(); } };
};

class Var inherits ExprD {
  v : String; v() : String { v };
  var(x : String) : Var { { v <- x; self; } };
};

class Abs inherits ExprD {
  lbound : String; lbound() : String { lbound };
  lbody : ExprD; lbody() : ExprD { lbody };
  abs(x : String, b : ExprD) : Abs { { lbound <- x; lbody <- b; self; } };
};

class App inherits ExprD {
  lapp : ExprD; lapp() : ExprD { lapp };
  rapp : ExprD; rapp() : ExprD { rapp };
  app(l : ExprD, r : ExprD) : App { { lapp <- l; rapp <- r; self; } };
};

class Add inherits ExprD {
  l : ExprD; l() : ExprD { l };
  r : ExprD; r() : ExprD { r };
  add(x : ExprD, y : ExprD) : Add { { l <- x; r <- y; self; } };
};

class Mul inherits ExprD {
  l : ExprD; l() : ExprD { l };
  r : ExprD; r() : ExprD { r };
  mul(x : ExprD, y : ExprD) : Mul { { l <- x; r <- y; self; } };
};


-- if (n+1) a b => a
-- if 0 a b => b
class Ifz inherits ExprD {
  p : ExprD; p() : ExprD { p };
  c : ExprD; c() : ExprD { c };
  a : ExprD; a() : ExprD { a };
  ifz(x : ExprD, y : ExprD, z : ExprD) : Ifz {
    {
    p <- x;
    c <- y;
    a <- z;
    self;
    }
  };
};

class Sub1 inherits ExprD {
  arg : ExprD; arg() : ExprD { arg };
  sub1(e : ExprD) : Sub1 { { arg <- e; self; } };
};

class Eval {
  eval(e : ExprD, env : EnvD) : ValD {
    case e of
      e : Var => new Env.env(env).lookup(e.v()).v(); -- lookup in env
      e : Abs => new Clos.clos(env,e.lbound(),e.lbody());
      e : App =>
        let r : ValD <- eval(e.rapp(),env) in
        case eval(e.lapp(),env) of
          v : Clos => eval(v.expr(), new ExtEnv.extenv(v.var(),r,v.env()));
        esac;
      e : Add =>
        case eval(e.l(),env) of
          e1 : IntV =>
            case eval(e.r(),env) of
              e2 : IntV => new IntV.int(e1.v() + e2.v());
            esac;
        esac;
      e : Mul =>
        case eval(e.l(),env) of
          e1 : IntV =>
            case eval(e.r(),env) of
              e2 : IntV => new IntV.int(e1.v() * e2.v());
            esac;
        esac;
      e : Ifz =>
        case eval(e.p(),env) of
          v : IntV => eval(if v.v() = 0 then e.c() else e.a() fi,env);
        esac;
      e : Sub1 =>
        case eval(e.arg(),env) of
          v : IntV => new IntV.int(v.v()-1);
        esac;
      esac
  };
};

class Expr {
  e : ExprD;
  expr(x : ExprD) : Expr { { e <- x; self; } };
  show_aux(e : ExprD) : String {
    case e of
      e : Var => "Var(".concat(e.v()).concat(")");
      e : Abs => "(\\".concat(e.lbound())
                      .concat(". ")
                      .concat(new Expr.expr(e.lbody()).show())
                      .concat(")");
      e : Int => "Int";
    esac
  };
  show() : String { show_aux(e) };
};

-- Value types
(*
data Val = Clos Env String Expr
         | Int i
*)
class ValD {
  var() : String { { abort(); var(); } };
  v() : Int { { abort(); v(); } };
  env() : EnvD { { abort(); env(); } };
  expr() : ExprD { { abort(); expr(); } };
};

class IntV inherits ValD {
  v : Int; v() : Int { v };
  int(x : Int) : IntV { { v <- x; self; } };
};

class Clos inherits ValD {
  var : String; var() : String { var };
  env : EnvD; env() : EnvD { env };
  expr : ExprD; expr() : ExprD { expr };

  clos(a : EnvD, b : String, c : ExprD) : Clos { { env <- a; var <- b; expr <- c; self; } };
};

class Val inherits IO {
  v : ValD; v() : ValD { v };
  print() : IO {
    case v of
      v : IntV => out_int(v.v());
      v : Clos => out_string("<LAM>");
    esac
  };
  val(x : ValD) : Val { { v <- x; self; } };
};

(*
data Env = EmptyEnv
         | ExtEnv String Val Env
*)
class EnvD {
  k() : String { { abort(); k(); } };
  v() : ValD { { abort(); v(); } };
  t() : EnvD { { abort(); t(); } };
};

class EmptyEnv inherits EnvD {};

class ExtEnv inherits EnvD {
  k : String; k() : String { k };
  v : ValD; v() : ValD { v };
  t : EnvD; t() : EnvD { t };

  extenv(a : String, b : ValD, r : EnvD) : EnvD { { k <- a; v <- b; t <- r; self; } };
};

-- Optional values
(*
data Optional = None | Some ValD
*)
class OptionalD {
  v() : ValD { { abort(); v(); }};
};

class None inherits OptionalD {};
class Some inherits OptionalD {
  v : ValD; v() : ValD { v };
  some(x : ValD) : OptionalD { { v <- x; self; } };
};

class Env inherits IO {
  m : EnvD <- new EmptyEnv;

  lookup_aux(m : EnvD, s : String) : OptionalD {
    case m of
      m : EmptyEnv => {out_string("unbound var ".concat(s).concat("\n")); new None;};
      m : ExtEnv => if m.k() = s then new Some.some(m.v()) else lookup_aux(m.t(),s) fi;
    esac
  };
  lookup(s : String) : OptionalD { lookup_aux(m,s) };

  add(k : String, v : ValD) : Env {
    { m <- new ExtEnv.extenv(k,v,m); self; }
  };
  env(x : EnvD) : Env { { m <- x; self; } };
  v() : EnvD { m };
};

(*
Y = \f. (\x. f (\v. (x x v))) (\x. f (\v. (x x v)))
fact = Y (\rec. \n. ifz n 1 (n * sub1(rec n)))
*)
class Main inherits IO {
  var(s : String) : Var { new Var.var(s) };
  app(a : ExprD, b : ExprD) : App { new App.app(a,b) };
  abs(s : String, b : ExprD) : Abs { new Abs.abs(s,b) };

  main() : IO {
    let
      x : ExprD <- new Var.var("x"),
      f : ExprD <- new Var.var("f"),
      n : ExprD <- new Var.var("n"),
      v : ExprD <- new Var.var("v"),
      rec : ExprD <- new Var.var("rec"),
      o : ExprD <- abs("x",app(f,abs("v",app(app(x,x),v)))),
      -- y combinator
      y : ExprD <- abs("f",app(o,o)),
      -- factorial body
      fact_body : ExprD <- abs("rec",abs("n",
                           new Ifz.ifz(n,
                                       var("one"),
                                       new Mul.mul(n, app(rec,new Sub1.sub1(n)))))),
      fact : ExprD <- new App.app(y,fact_body),
      e : ExprD <- app(fact,x),
      s : EnvD <- new Env.add("x",new IntV.int(10))
                         .add("one", new IntV.int(1))
                         .v()
    in new Val.val(new Eval.eval(e,s)).print()
  };
};