Loading ...
Sorry, an error occurred while loading the content.

CC Machine, call for comments

Expand Messages
  • dvanhorn_at_uvm
    Hello, This is my first attempt at writing an OCaml program and I d like to hear any comments or feedback on the attempt. For the formal specification of this
    Message 1 of 3 , Sep 7, 2003
    • 0 Attachment
      Hello,

      This is my first attempt at writing an OCaml program and I'd like to
      hear any comments or feedback on the attempt.

      For the formal specification of this machine, see

      http://www.cs.utah.edu/classes/cs6520/notes.pdf

      Thanks.

      -d



      (*
      dvanhorn@...
      Released under the terms of the GNU Lesser General Public License.

      The CC Machine -- an ISWIM interpreter

      The specification of this eval_cc function comes from Felleisen &
      Flatt --Programming Languages and Lambda Calculi.

      TODO: Make delta and base types parameterizable.
      *)

      open List ;;

      type context =
      | CEmptyHole
      | CInHole of context * context
      | CAppV of value * context
      | CAppE of context * term
      | CAppPrim of primop * value list * context * term list
      and term =
      | Value of value
      | App of term * term
      | AppPrim of primop * term list
      and value =
      | Base of base
      | Var of var
      | Lambda of var * term
      and var = string
      and base = Int of int | False | True
      and primop = Add1 | Sub1 | Plus | Minus | Times | Exp
      and result = Result of base | Function
      ;;

      (*
      span : ('a -> bool) -> 'a list -> 'a list * 'a list
      An old scheme friend

      Span splits the list into the longest initial prefix whose
      elements all satisfy the predicate f, and the remaining tail. Cf.
      Olin Shivers's SRFI-1.
      *)
      let span f ls =
      let rec recur = function
      | [] -> [], []
      | x::rest ->
      if f x then let (prefix, suffix) = recur rest in
      x::prefix, suffix
      else [], x::rest
      in
      recur ls
      ;;

      (* delta : primop -> term list -> term *)
      let delta op args =
      match args with
      Value(Base(Int x))::rest ->
      let y =
      match rest with
      | [Value(Base(Int y))] -> y
      | [] -> 1
      in
      let result =
      match op with
      | Add1 | Plus -> x+y
      | Sub1 | Minus ->
      let sum = x-y in
      if sum <= 0 then 0 else sum
      in
      Value(Base (Int result)) ;;

      let is_value = function
      | Value v -> true
      | _ -> false
      ;;

      let is_base = function
      | Value (Base b) -> true
      | _ -> false
      ;;

      (*
      gen_var : unit -> string

      Returns a fresh variable name of the form "zn" where n is an
      integer (so don't use variable of this form!).
      *)
      let gen_var =
      let i = ref 0 in
      fun () ->
      i := !i+1;
      "z" ^ (string_of_int !i)
      ;;

      (*
      substitute : term -> var -> value -> term

      Substitutes v for x in m.
      *)
      let rec substitute m x v =
      match m with
      | Value(Base b) -> Value(Base b)
      | Value(Var y) ->
      if x=y then Value v
      else Value(Var y)
      | Value(Lambda(y,n)) ->
      if x=y then Value(Lambda(y,n))
      else let z = gen_var () in
      Value(Lambda(z, (substitute (substitute n y (Var z)) x v)))
      | App(n,p) ->
      App(substitute n x v, substitute p x v)
      | AppPrim(o, tlist) ->
      AppPrim(o, (map (fun t -> substitute t x v) tlist))
      ;;


      (*
      cc : term * context -> term * context

      The machine state transition function.
      *)
      (*
      let cc = function
      | App(m,n), e
      when not (is_value m) ->
      m, CInHole(e, CAppE(CEmptyHole, n))
      | App(Value(v), m), e
      when not (is_value m) ->
      m, CInHole(e, CAppV(v, CEmptyHole))
      | AppPrim(o, args), e
      when for_all is_base args ->
      delta o args, e
      | AppPrim(o, args), e ->
      let (vlist, m::tlist) = span is_value args in
      let vlist = map (fun (Value v) -> v) vlist in
      m, CInHole(e, CAppPrim(o, vlist, CEmptyHole, tlist))
      | App(Value(Lambda(x,m)), Value v), e ->
      substitute m x v, e
      | Value v, CInHole(e, CAppV(u, CEmptyHole)) ->
      App(Value u, Value v), e
      | Value v, CInHole(e, CAppE(CEmptyHole, n)) ->
      App(Value v, n), e
      | Value v, CInHole(e, CAppPrim(o, vlist, CEmptyHole, tlist)) ->
      let vlist = map (fun x -> (Value x)) vlist in
      AppPrim(o, vlist@[(Value v)]@tlist), e
      ;;
      *)

      (*
      Simplified version of CC state transitions.
      *)
      let cc = function
      | App(m,n), e ->
      m, CInHole(e, CAppE(CEmptyHole, n))
      | AppPrim(o, m::tlist), e ->
      m, CInHole(e, CAppPrim(o, [], CEmptyHole, tlist))
      | Value v, CInHole(e, CAppV(Lambda (x,m), CEmptyHole)) ->
      substitute m x v, e
      | Value v, CInHole(e, CAppE(CEmptyHole, n)) ->
      n, CInHole(e, CAppV(v, CEmptyHole))
      | Value v, CInHole(e, CAppPrim(o, blist, CEmptyHole, []))
      when is_base (Value v) ->
      delta o (map (fun x -> (Value x)) blist@[(Value v)]), e
      | Value v, CInHole(e, CAppPrim(o, vlist, CEmptyHole, n::tlist)) ->
      n, CInHole(e, CAppPrim(o, vlist@[v], CEmptyHole, tlist))
      ;;


      (* eval_cc : term -> result *)
      let eval_cc term =
      let rec loop = function
      | Value(Base b), CEmptyHole -> (Result b)
      | Value(Lambda (x,m)), CEmptyHole -> Function
      | term, context -> loop (cc (term, context))
      in
      loop (term, CEmptyHole)
      ;;


      (* ((lambda (x) x) ((lambda (x) x) 5)) *)
      eval_cc (App (Value (Lambda ("x", Value (Var "x"))),
      App (Value (Lambda ("x", Value (Var "x"))),
      Value (Base (Int 5)))));;

      (* - : result = Result (Int 5) *)
    • Remi Vanicat
      ... Well, I haven t read every things, but some more sharing can be useful : [...] ... became : let span f ls = let rec recur = function ... if f x then let
      Message 2 of 3 , Sep 7, 2003
      • 0 Attachment
        "dvanhorn_at_uvm" <david@...> writes:

        > Hello,
        >
        > This is my first attempt at writing an OCaml program and I'd like to
        > hear any comments or feedback on the attempt.

        Well, I haven't read every things, but some more sharing can be
        useful :


        [...]


        > (*
        > span : ('a -> bool) -> 'a list -> 'a list * 'a list
        > An old scheme friend
        >
        > Span splits the list into the longest initial prefix whose
        > elements all satisfy the predicate f, and the remaining tail. Cf.
        > Olin Shivers's SRFI-1.
        > *)

        example 1 :

        > let span f ls =
        > let rec recur = function
        > | [] -> [], []
        > | x::rest ->
        > if f x then let (prefix, suffix) = recur rest in
        > x::prefix, suffix
        > else [], x::rest
        > in
        > recur ls
        > ;;

        became :

        let span f ls =
        let rec recur = function
        | [] -> [], []
        | x::rest as l ->
        if f x then let (prefix, suffix) = recur rest in
        x::prefix, suffix
        else [], l
        in
        recur ls


        [...]

        example 2 :
        > (*
        > substitute : term -> var -> value -> term
        >
        > Substitutes v for x in m.
        > *)
        > let rec substitute m x v =
        > match m with
        > | Value(Base b) -> Value(Base b)
        > | Value(Var y) ->
        > if x=y then Value v
        > else Value(Var y)
        > | Value(Lambda(y,n)) ->
        > if x=y then Value(Lambda(y,n))
        > else let z = gen_var () in
        > Value(Lambda(z, (substitute (substitute n y (Var z)) x v)))
        > | App(n,p) ->
        > App(substitute n x v, substitute p x v)
        > | AppPrim(o, tlist) ->
        > AppPrim(o, (map (fun t -> substitute t x v) tlist))
        > ;;

        became :

        let rec substitute m x v =
        match m with
        | Value(Base b) -> m
        | Value(Var y) ->
        if x=y then Value v
        else m
        | Value(Lambda(y,n)) ->
        if x=y then m
        else let z = gen_var () in
        Value(Lambda(z, (substitute (substitute n y (Var z)) x v)))
        | App(n,p) ->
        App(substitute n x v, substitute p x v)
        | AppPrim(o, tlist) ->
        AppPrim(o, (map (fun t -> substitute t x v) tlist))
        ;;

        [...]


        The advantage of such things :

        You will use less memory and trigger less garbage collection.

        But this is optimization, and optimization is the last thing you
        should do.

        --
        Rémi Vanicat
        vanicat@labri.u-bordeaux.fr
        http://dept-info.labri.u-bordeaux.fr/~vanicat
      • dvanhorn_at_uvm
        ... Thanks Rémi, I ve worked these changes in. Apparently posting from yahoo groups will eat all whitespace in a message, for an indented copy of the code
        Message 3 of 3 , Sep 7, 2003
        • 0 Attachment
          --- In ocaml_beginners@yahoogroups.com, Remi Vanicat
          <vanicat+egroups@l...> wrote:
          > Well, I haven't read every things, but some more sharing can be
          > useful :

          Thanks Rémi,

          I've worked these changes in. Apparently posting from yahoo groups
          will eat all whitespace in a message, for an indented copy of the code
          see:

          http://www.cs.uvm.edu/~dvanhorn/ocaml/cc.ml

          Thanks.

          -d
        Your message has been successfully submitted and would be delivered to recipients shortly.