Created
July 18, 2023 10:00
-
-
Save yallop/34f2adf63d0c0b82ab849b7fda7ff3ee to your computer and use it in GitHub Desktop.
Code accompanying "Safe and efficient generic functions with MacoCaml" (OCaml 2023)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment