gadt_using_fcm.ml

module type Kind_1 = sig
  type _ t
  type content
  type content_t

  val to_a_t : content t -> content_t
  val of_a_t : content_t -> content t
end
type 'a kind_1 = (module Kind_1 with type content = 'a)

module type Eq = sig
  type a
  type b

  val to_b : a kind_1 -> b kind_1
  val to_a : b kind_1 -> a kind_1
end
type ('a, 'b) eq = (module Eq with type a = 'a and type b = 'b)

let eq (type t) : (t, t) eq =
  (module struct
    type a = t
    type b = t
    let to_a x = x
    let to_b x = x
  end)

(* only needed because OCaml doesn't have recursive module type *)
module rec Nat_wrapper : sig
  type o = |
  type _ s = |

  module type Nat = sig
    type t

    val match_ :
      if_zero:(unit -> 'a) ->
      if_succ:(unit -> (module Nat_wrapper.Succ with type t = t) -> 'a) ->
      'a
  end
  type 'a nat = (module Nat with type t = 'a)

  module type Succ = sig
    type content
    type t

    val eq : (t, content s) eq
    val content : (module Nat with type t = content)
  end
  type 'a succ = (module Succ with type t = 'a)
end =
  Nat_wrapper
open Nat_wrapper

let zero : o nat =
  (module struct
    type t = o
    let match_ ~if_zero ~if_succ:_ = if_zero ()
  end)

let succ (type a) (n : (module Nat with type t = a)) : a s nat =
  (module struct
    type t = a s
    let match_ :
        if_zero:(unit -> 'a) ->
        if_succ:(unit -> (module Succ with type t = t) -> 'a) ->
        'a =
     fun ~if_zero:_ ~if_succ ->
      if_succ ()
        (module struct
          type content = a
          type nonrec t = t
          let eq = eq
          let content = n
        end)
  end)

let rec to_int : type a. a nat -> int =
 fun (module N) ->
  N.match_
    ~if_zero:(fun () -> 0)
    ~if_succ:(fun () (module Content) -> 1 + to_int Content.content)

let is_succ (type a) ((module N) : a nat) =
  N.match_ ~if_zero:(fun () -> None) ~if_succ:(fun () succ -> Some succ)

let one = succ zero
let two = succ one

let () =
  match is_succ zero with
  | None -> print_endline "zero is not succ"
  | Some _ -> print_endline "zero is succ???"

let () =
  match is_succ two with
  | None -> print_endline "two is not succ???"
  | Some _ -> print_endline "two is succ"