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 t => Cons t when t : ('a gen_elem * 'a gen_list) | Value x => ~ and 'a gen_elem : 'a gen => 'a with | Value x => x | Unit => ~ | Pair t => ~ when t : ('a gen_elem * 'a gen_list) |
Then we can derive a map function:
| let map_list = lifting gen_map : ('a -> 'b) -> 'a gen_list -> 'b gen_list |
We get this result, with an intermediate function:
| let rec map_list f x = match x with | Cons (u, v) -> Cons (gen_map_auto1 f u, map_list f v) | Nil -> Nil and gen_map_auto1 f x = f x |
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 t => Node t when t : ('a gen_value * 'a gen_treepair) | Value x => ~ and 'a gen_value : 'a gen => 'a with | Value x => x | Unit => ~ | Pair t => ~ when t : ('a gen_tree * 'a gen_tree) and 'a gen_treepair : 'a gen => 'a tree * 'a tree with | Unit => ~ | Pair t => t when t : ('a gen_tree * 'a gen_tree) | Value x => ~ |
| let map_tree = lifting gen_map : ('a -> 'b) -> 'a gen_tree -> 'b gen_tree |
We get the expected result:
| let rec map_tree f x = match x with | Node (u, v) -> Node (gen_map_auto3 f u, gen_map_auto2 f v) | Leaf -> Leaf and gen_map_auto2 f x = match x with | (u, v) -> (map_tree f u, map_tree f v) and gen_map_auto3 f x = f x |