We need to activate autolifting for this:

#(mode autolift) #(mode unfold)

We start with a generic representation:

type 'a gen = | Pair of 'a gen * 'a gen | Value of 'a | Unit

We define a map function:

let rec gen_map f x = match x with | Pair(u,v) -> Pair(gen_map f u, gen_map f v) | Value x -> Value (f x) | Unit -> Unit

Then we define lists:

type 'a list = | Nil | Cons of 'a * 'a list

Lists are a specialization of the generic representation:

type ornament 'a gen_list : 'a gen => 'a list with | Unit => Nil | Pair(x, xs) => Cons(x, xs) when x : 'a gen_elem, xs : 'a gen_list | Value x => ~ and 'a gen_elem : 'a gen => 'a with | Value x => x | Unit => ~ | Pair(x, y) => ~

Then we can derive a map function:

#(push_env) let map_list = lifting gen_map : ('a -> 'b) -> 'a gen_list -> 'b gen_list #(pop_env)

We get this result, with an intermediate function:

let rec map_list f x = match x with | Nil -> Nil | Cons (x, x1) -> Cons (gen_map_auto1 f x, map_list f x1) and gen_map_auto1 f x = f x

We can also request the intermediate functions to be inlined:

#(mode inline) let map_list = lifting gen_map : ('a -> 'b) -> 'a gen_list -> 'b gen_list #(mode noinline)
let rec map_list f x = match x with | Nil -> Nil | Cons (x, x1) -> Cons (f x, map_list f x1)

We can do the same with trees:

type 'a tree = | Leaf | Node of 'a * 'a tree * 'a tree
type ornament 'a gen_tree : 'a gen => 'a tree with | Unit => Leaf | Pair(v : 'a gen_value, (l, r) : 'a gen_treepair) => Node(v,l,r) | Value x => ~ and 'a gen_value : 'a gen => 'a with | Value x => x | Unit => ~ | Pair(x,y) => ~ and 'a gen_treepair : 'a gen => 'a tree * 'a tree with | Unit => ~ | Pair(l : 'a gen_tree, r : 'a gen_tree) => (l, r) | Value x => ~
#(push_env) let map_tree = lifting gen_map : ('a -> 'b) -> 'a gen_tree -> 'b gen_tree #(pop_env)

We get the expected result:

let rec map_tree f x = match x with | Leaf -> Leaf | Node(x, l, r) -> begin match gen_map_auto3 f (l, r) with | (l, r) -> Node(gen_map_auto4 f x, l, r) end and gen_map_auto3 f x = match x with | (x, x1) -> (map_tree f x, map_tree f x1) and gen_map_auto4 f x = f x

Again, we can request inlining of the definition:

#(mode inline) let map_tree = lifting gen_map : ('a -> 'b) -> 'a gen_tree -> 'b gen_tree #(mode noinline)
let rec map_tree f x = match x with | Leaf -> Leaf | Node (x, l, r) -> Node (f x, map_tree f l, map_tree f r)