gadt_print3.ml

open Printf

module Type = struct
  type _ t =
    | Unit : unit t
    | Bool : bool t
    | Int : int t
    | Sum : 's sum -> 's t

  and 's sum = {
    sum_name : string;
    sum_op : 'a . ('a, 's) poly_op -> 's -> 'a;
  }

  and (_, 'r) app =
    | Nil : ('r, 'r) app
    | Arg : 'a t * ('b, 'r) app -> (('a -> 'b), 'r) app

  and ('r, 's) poly_op = {
    f : 'f . 's con -> ('f, 'r) app -> 'f;
  }

  and 's con = {
    con_name : string;
    con_func : 's con_func;
  }

  and 's con_func = Con : ('f, 's) app * 'f -> 's con_func
end

let rec print : type a . a -> a Type.t -> unit =
  let open Type in
  fun value -> function
    | Unit -> print_string "()"
    | Int -> print_int value
    | Bool -> printf "%b" value
    | Sum sum ->
      print_char '(';
      print_sum value sum;
      print_char ')'

and print_sum : type s . s -> s Type.sum -> unit =
  let open Type in
  fun value sum ->
    let rec args : type f . (f, unit) app -> f = function
      | Nil -> ()
      | Arg (arg_ty, rest) ->
        (fun arg ->
           print_char ' ';
           print arg arg_ty;
           args rest)
    and f con = print_string con.con_name; args in
    sum.sum_op {f} value

let rec copy : type a . a -> a Type.t -> a =
  let open Type in
  fun value -> function
    | Unit -> value
    | Int -> value
    | Bool -> value
    | Sum sum -> copy_sum value sum

and copy_sum : type s . s -> s Type.sum -> s =
  let open Type in
  fun value sum ->
    assert false

type t =
  | Foo
  | Bar of int * bool
  | Rec of t

let rec t_op : 'a . ('a, t) Type.poly_op -> t -> 'a =
  fun f value ->
    let open Type in
    match value with
    | Foo -> f.f t_foo Nil
    | Bar (i, b) -> f.f t_bar (Arg (Int, Arg (Bool, Nil))) i b
    | Rec t -> f.f t_rec (Arg (t_type, Nil)) t

and t_type = Type.(Sum {
    sum_name = "t";
    sum_op = t_op
  })

and t_foo = Type.{
    con_name = "Foo";
    con_func = Con (Nil, Foo);
  }

and t_bar = Type.{
    con_name = "Bar";
    con_func = Con (Arg (Int, Arg (Bool, Nil)),
                    fun i b -> Bar (i, b));
  }

and t_rec = Type.{
    con_name = "Rec";
    con_func = Con (Arg (t_type, Nil),
                    fun t -> Rec t);
  }