lavoisier.ml

module Peano = struct
  type z = Zero
  type 'a s = Succ

  type 'a t =
    | Z : z t
    | S : 'a t -> 'a s t
  and zero = z t

  let zero : z t = Z
  let one : z s t = S Z
end

module Plus = struct
  type ('a, 'b, 'r) t =
    | Z : (Peano.z, 'a, 'a) t
    | S : ('p, 'q, 'r) t -> ('p Peano.s, 'q, 'r Peano.s) t
end

module Eq = struct
  type ('a, 'b) refl = Refl : ('a, 'a) refl
end

module Ordinal = struct
  type u = unit

  type ('a, 'n) t =
    | Z : (u, Peano.z) t
    | S : ('e, 'n) t -> ('e * u, 'n Peano.s) t

  module N = struct
    type ('a, 'n) t =
      | Z : ('e * u, Peano.z) t
      | S : ('e, 'n) t -> ('e * u, 'n Peano.s) t
  end

  let rec in_range : type e n m. (e, n) N.t -> (e, m) t -> (e, e) Eq.refl
    = fun v r -> match v, r with
      | N.Z, S _ -> Eq.Refl
      | N.S v, S r -> match in_range v r with
        | Eq.Refl -> Eq.Refl
end

type ('e, 'l, 'h, 'r) t =
  | Z : ('e, 'h) Ordinal.t -> ('e, Peano.z, 'h, 'h) t
  | S : ('e, 'l, 'h, 'r) t -> ('e * Ordinal.u, 'l Peano.s, 'h, 'r Peano.s) t

module N = struct
  type ('e, 'l, 'm, 'h) t =
    | Z : ('e, 'm) Ordinal.N.t -> ('e, Peano.z, 'm, 'h) t
    | S : ('e, 'l, 'm, 'h) t -> ('e * Ordinal.u, 'l Peano.s, 'm Peano.s, 'h) t
end

let rec in_range
  : type e h0 h1 l m n. (e, l, m, h0) N.t -> (e, l, n, h1) t -> (e, e) Eq.refl
  = fun v t -> match v, t with
    | N.Z v, Z o -> Ordinal.in_range v o
    | N.S v, S o -> match in_range v o with
      | Eq.Refl -> Eq.Refl

let range_2_4 = S (S (Z Ordinal.(S (S Z))))
let _ = in_range N.(S (S (Z Ordinal.N.(S Z)))) range_2_4