Scrap_Your_Boilerplate_2

syb2.ml

type (_, _) eql = Refl : ('a, 'a) eql

type _ type_rep = ..

module type TYPEABLE =
  sig
    type t
    val type_rep : unit -> t type_rep
    val eqty : 's type_rep -> (t, 's) eql option
  end

let (=~~=) {A: TYPEABLE} {B: TYPEABLE} = A.eqty (B.type_rep ())

module rec R :
  sig
    type    genericT  = {T: R.DATA} -> T.t      -> T.t
    type 'u genericQ  = {T: R.DATA} -> T.t      -> 'u

    module type DATA =
      sig
        type t
        module Typeable : TYPEABLE with type t = t
        val gmapT  : genericT  -> t      -> t
        val gmapQ  : 'u genericQ  -> t      -> 'u list
      end
  end = R
include R

let app (type a) (type b)
    (module A : TYPEABLE with type t = a)
    (module B : TYPEABLE with type t = b)
    (g : b -> b) (x : a) : a =
  match (=~~=) {A} {B} with
  | Some Refl -> g x
  | _ -> x

let app' (type a) (type b) (type u)
    (module A : TYPEABLE with type t = a)
    (module B : TYPEABLE with type t = b)
    (u:  u) (g : b -> u) (x: a) : u =
  match (=~~=) {A} {B} with
  | Some Refl -> g x
  | _         -> u

let mkT {T:TYPEABLE} g : genericT =
  fun {D:DATA} -> app (module D.Typeable) (module T) g

let mkQ {T:TYPEABLE} u g : 'u genericQ =
  fun {D: DATA} x -> app' (module D.Typeable) (module T) u g x

module Typeable0_make(T: sig type t end) =
  struct
    type _ type_rep += T : T.t type_rep
    type t = T.t
    let eqty : type b. b type_rep -> (t, b) eql option =
      function T -> Some Refl | _ -> None
    let type_rep () = T
  end

type exp =
  | Add of exp * exp
  | Sub of exp * exp
  | Val of int


implicit module Typeable_int = Typeable0_make(struct type t = int end)
implicit module Typeable_exp = Typeable0_make(struct type t = exp end)

implicit module Data_int =
  struct
    type t = int
    module Typeable = Typeable_int
    let gmapT _ x = x
    let gmapQ _ _ = []
  end

implicit module Data_exp : DATA with type t = exp =
  struct
    module rec R : DATA with type t = exp =
      struct
        type t = exp
        module Typeable = Typeable_exp
        let gmapT (f : genericT) (e : t) =
          match e with
          | Add (e0, e1) -> Add (f {R} e0, f {R} e1)
          | Sub (e0, e1) -> Sub (f {R} e0, f {R} e1)
          | Val n0       -> Val (f n0)
        let gmapQ (f : _ genericQ) (e : t) =
          match e with
          | Add (e0, e1) | Sub (e0, e1) -> [f {R} e0; f {R} e1]
          | Val n0                      -> [f n0]
      end
    include R
end

let gmapT f {D: DATA} = D.gmapT f

let gmapQ f {D: DATA} = D.gmapQ f

let rec everywhere : genericT -> genericT =
  fun (f : genericT) {X:DATA} x -> f ((gmapT (everywhere f) : genericT) x)

let rec eval' = function
  | Add (Val n0, Val n1) -> Val (n0 + n1)
  | Sub (Val n0, Val n1) -> Val (n0 - n1)
  | e0                   -> e0

let eval = everywhere (mkT eval')