Code accompanying "Safe and efficient generic functions with MacoCaml" (OCaml 2023)

tyrep.ml

type _ prim =
  Int : int prim
| Int32 : int32 prim
| Int64 : int64 prim
| Nativeint : nativeint prim
| Float : float prim
| Unit : unit prim

type ('a,'b) iso = {
    out: 'a expr -> 'b expr;
    in_: 'b expr -> 'a expr;
  }

type ('a,'b) either = Left of 'a | Right of 'b

type (_,_) eql = Refl : ('a,'a) eql
type _ id = ..
type 'a var = { id: 'a id; eq : 'b. 'b id -> ('a,'b) eql option }
macro var : type a. unit -> a var =
  fun () ->
  let module M = struct type _ id += Id : a id end in
  let eq : type b. b id -> (a,b) eql option =
    function M.Id -> Some Refl | _ -> None in
  { id = M.Id; eq }

type 'a t =
  Primitive of 'a prim
| Var of 'a var
| Sum : 'a t * 'b t -> ('a,'b) either t 
| Prod : 'a t * 'b t -> ('a * 'b) t 
| Iso :  ('a,'b) iso * 'a t -> 'b t

type 'a ty = Ty of 'a var * 'a t

macro tyname : 'a ty -> 'a var =
  fun (Ty (x,_)) -> x

let rec outList = function
  | Left () -> []
  | Right (x,xs) -> x :: xs
let rec inList_ = function
  | [] -> Left ()
  | x :: xs -> Right (x, xs)

macro list elem =
  let self = var () in
  Ty (self, Iso ({out=(fun x -> << outList $x>>); in_ = (fun x -> <<inList_ $x>>)}, Sum (Primitive Unit, Prod (Var (tyname elem), Var self))))

macro eqprim : type a. a prim -> a expr -> a expr -> bool expr =
  fun p x y ->
  match p with
  | Int -> << $x = $y >>
  | Int32 -> << Int32.equal $x $y >>
  | Int64 -> << Int64.equal $x $y >>
  | Nativeint -> << Nativeint.equal $x $y >>
  | Float -> << $x = $y >> 
  | Unit -> << true >> 

type eqenv =
  Nil : eqenv
| Bind : 'a var * ('a -> 'a -> bool) expr * eqenv -> eqenv

macro rec lookup : type a. a var -> eqenv -> (a -> a -> bool) expr =
  fun x env ->
  match env with
  | Nil -> ~Pervasives.raise Not_found
  | Bind (y,v,env') ->
     match x.eq y.id with
     | Some Refl -> v
     | None -> lookup x env'

macro rec eqt : type a. eqenv -> a t -> a expr -> a expr -> bool expr =
  fun env t x y ->
  match t with
  | Primitive p -> eqprim p x y
  | Var v -> << $(lookup v env) $x $y >>
  | Sum (l,r) -> << match $x, $y with
                    | Left a, Left b -> $(eqt env l <<a>> <<b>>)
                    | Right a, Right b -> $(eqt env r <<a>> <<b>>)
                    | _ -> false >>
  | Prod (l,r) -> << let (a,b) = $x in
                     let (c,d) = $y in
                     $(eqt env l <<a>> <<c>>)
                  && $(eqt env r <<b>> <<d>>) >>
  | Iso ({out; in_}, i) -> eqt env i (in_ x) (in_ y)

macro eqty : type a. eqenv -> a ty -> (a -> a -> bool) expr =
  fun env (Ty (v,ty)) -> << let rec eq x y = $(eqt (Bind (v,<<eq>>,env)) ty <<x>> <<y>>) in eq >>


static int32 = Ty (var (), Primitive Int32)
let eq_int32 : int32 -> int32 -> bool =
  $(eqty Nil int32)

static int32_list = list int32
let eq_int32_list : int32 list -> int32 list -> bool =
  $(eqty (Bind (tyname int32, <<eq_int32>>, Nil)) int32_list)

let test =
  begin
    assert (eq_int32_list [1l; 2l; 3l] [1l; 2l; 3l]);
    assert (not (eq_int32_list [1l; 2l; 3l] [1l; 2l]));
    assert (not (eq_int32_list [] [1l; 2l]));
    assert (eq_int32_list [] []);
  end