goofy implementation of λ-calculus

Visitor.ml

let ( let+ ) = Option.bind

module Expr = struct
  type app = A
  type fun' = F
  type name = N
  type 'variant reducible = A : app reducible

  type 'variant irreducible =
    | F : fun' irreducible
    | N : name irreducible

  type 'variant t =
    | App : (erased * erased) -> app reducible t
    | Fun : (string * erased) -> fun' irreducible t
    | Name : string -> name irreducible t

  and erased = Erased : 'variant t -> erased
  and final = Final : 'variant irreducible t -> final

  let final_to_erased : final -> erased =
    fun (Final expr) -> Erased expr
  ;;

  let app f a = Erased (App (f, a))
  let fun' p b = Erased (Fun (p, b))
  let name n = Erased (Name n)
  let ( ~@ ) = name
  let ( @-> ) = fun'
end

module Show = struct
  let () = Random.self_init ()
  let color = Random.full_int 256

  let lambda =
    Printf.sprintf "\x1b[1;38;5;%dm\u{3bb}\x1b[22;39m" color
  ;;

  let paren_left = "\x1b[2m(\x1b[22m"
  let paren_right = "\x1b[2m)\x1b[22m"
  let period = "\x1b[2m.\x1b[22m"

  let rec show_app : Expr.(app reducible t) -> string = function
    | App (f, a) -> Printf.sprintf "%s %s" (show f) (show a)

  and show_fun : Expr.(fun' irreducible t) -> string = function
    | Fun (p, b) ->
      Printf.sprintf
        "%s%s%s%s %s%s"
        paren_left
        lambda
        p
        period
        (show b)
        paren_right

  and show_name : Expr.(name irreducible t) -> string = function
    | Name name -> name

  and show : Expr.erased -> string = function
    | Erased (App (_, _) as app) -> show_app app
    | Erased (Fun _ as fun') -> show_fun fun'
    | Erased (Name _ as name) -> show_name name
  ;;

  let show_final : Expr.final -> string =
    fun final -> show (Expr.final_to_erased final)
  ;;
end

module Eval = struct
  let rec substitute
            ~(name : string)
            ~with_expr:(replacer : Expr.final)
            ~inside:(body : Expr.erased)
    : Expr.erased
    =
    match body with
    | Erased (App (func, arg)) ->
      Erased
        (App
           ( substitute ~name ~with_expr:replacer ~inside:func
           , substitute ~name ~with_expr:replacer ~inside:arg ))
    | Erased (Fun (param', body')) when name = param' ->
      substitute
        ~name
        ~with_expr:replacer
        ~inside:
          (Erased
             (Fun
                ( param' ^ "'"
                , substitute
                    ~name:param'
                    ~with_expr:(Final (Name (param' ^ "'")))
                    ~inside:body' )))
    | Erased (Fun (param', body')) ->
      Erased
        (Fun
           ( param'
           , substitute ~name ~with_expr:replacer ~inside:body'
           ))
    | Erased (Name name') when name = name' ->
      Expr.final_to_erased replacer
    | Erased (Name name') -> body
  ;;

  let rec eval_app : Expr.(app reducible t -> final option)
    = function
    | App (func', arg') ->
      let+ func = eval func' in
      let+ arg = eval arg' in
      (match func with
       | Final (Fun (param, body)) ->
         eval
           (substitute ~name:param ~with_expr:arg ~inside:body)
       | Final (Name _) -> None)

  and eval_fun : Expr.(fun' irreducible t -> fun' irreducible t)
    =
    Fun.id

  and eval_name
    : Expr.(name irreducible t -> name irreducible t)
    =
    Fun.id

  and eval : Expr.(erased -> final option) = function
    | Erased (App _ as app) -> eval_app app
    | Erased (Fun _ as fun') -> Some (Final (eval_fun fun'))
    | Erased (Name _ as name) -> Some (Final (eval_name name))
  ;;
end

let id = Expr.("x" @-> ~@"x")
let const = Expr.("x" @-> "y" @-> ~@"x")
let expr = Expr.(app (app (app const id) ~@"a") ~@"b")
let () = Printf.printf "%s\n" (Show.show expr)

let () =
  match Eval.eval expr with
  | None -> Printf.eprintf "failed to eval\n"
  | Some (Final _ as expr) ->
    Printf.printf "%s\n" (Show.show_final expr)
;;