We need to activate autolifting for this:
| #(mode autolift) #(mode unfold) |
We define lists:
| type 'a list = | Nil | Cons of 'a * 'a list |
And a map function:
| let rec map f x = match x with | Nil -> Nil | Cons(x,xs) -> Cons(f x, map f xs) |
We want to use vectors of three elements:
| type 'a vec3 = Vec3 of 'a * 'a * 'a |
They are a specialization of lists:
| type ornament 'a list3 : 'a list => 'a vec3 with | Nil => ~ | Cons(x, (y, z) : 'a list2) => Vec3(x, y, z) and 'a list2 : 'a list => 'a * 'a with | Nil => ~ | Cons(y, z : 'a list1) => (y, z) and 'a list1 : 'a list => 'a with | Nil => ~ | Cons(z, () : 'a list0) => z and 'a list0 : 'a list => () with | Nil => () | Cons(x, xs) => ~ |
| #(push_env) let map_tuple = lifting map : ('a -> 'b) -> 'a list3 -> 'b list3 #(pop_env) |
| let rec map_tuple f x = match x with | Vec3(x, y, z) -> begin match map_auto1 f (y, z) with | (y, z) -> Vec3(f x, y, z) end and map_auto1 f x = match x with | (x, x1) -> (f x, map_auto2 f x1) and map_auto2 f x = match map_auto3 f () with | () -> f x and map_auto3 f x = match x with | () -> () |
We can request inlining for this definition:
| #(mode inline) let map_tuple = lifting map : ('a -> 'b) -> 'a list3 -> 'b list3 |
| let map_tuple f x = match x with | Vec3(x, y, z) -> Vec3(f x, f y, f z) |