Re: CC Machine in OCaml

dvanhorn wrote:
> (*
>    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:

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))
;;

-d